Mathlib Map

Theorems · Definition · category theory

CategoryTheory.ProjectiveResolution.self

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (Z : C) → [CategoryTheory.Projective Z] → CategoryTheory.ProjectiveResolution Z

A projective object admits a trivial projective resolution: itself in degree 0.

Defined in
Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Cited by
4 results in Mathlib
Foundations
Depth 44 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.CategoryCategoryTheory.Limits.HasZeroObjectCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Projective
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ · cited by 3Functor.isZero_leftDerive…isZero_Ext_succ_of_projective · cited by 1isZero_Ext_succ_of_projec…CategoryTheory.ProjectiveResolution.self_complex · cited by 0ProjectiveResolution.self…CategoryTheory.ProjectiveResolution.self_π · cited by 0ProjectiveResolution.self…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryCategoryTheory.Functor.obj · cited by 19642Functor.objCategoryTheory.CategoryStruct.id · cited by 6235CategoryStruct.idCategoryTheory.Limits.HasZeroMorphisms · cited by 3275Limits.HasZeroMorphismsCategoryTheory.Limits.HasZeroObject · cited by 1298Limits.HasZeroObjectCategoryTheory.ProjectiveResolution · cited by 92CategoryTheory.Projective…CategoryTheory.Projective · cited by 78CategoryTheory.ProjectiveChainComplex.single₀ · cited by 69ChainComplex.single₀ProjectiveResolution.selfCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.