Theorems · Definition · category theory

CategoryTheory.InjectiveResolution.descFZero

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Y Z : C} →
          (Z ⟶ Y) →
            (I : CategoryTheory.InjectiveResolution Y) →
              (J : CategoryTheory.InjectiveResolution Z) → J.cocomplex.X 0 ⟶ I.cocomplex.X 0

Auxiliary construction for desc.

Defined in: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Cited by: 1 results in Mathlib
Foundations: Depth 51 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Limits.HasZeroObject CategoryTheory.Limits.HasZeroMorphisms

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.CategoryStruct.compproof · cited by 17,999
CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
HomologicalComplex.Xstatement · cited by 1,839
CategoryTheory.Limits.HasZeroObjectstatement and proof · cited by 1,298
ComplexShape.upstatement · cited by 1,123
HomologicalComplex.Hom.fproof · cited by 845
CategoryTheory.InjectiveResolutionstatement and proof · cited by 90
CategoryTheory.InjectiveResolution.cocomplexstatement · cited by 73
CategoryTheory.InjectiveResolution.ιproof · cited by 48
CategoryTheory.Injective.factorThruproof · cited by 12

Cited by3

Results whose statement or proof uses this declaration.

CategoryTheory.InjectiveResolution.descproof · cited by 6
CategoryTheory.InjectiveResolution.descFOneproof · cited by 1
CategoryTheory.InjectiveResolution.descFOne_zero_commstatement and proof · cited by 0