Theorems · Definition · category theory

CategoryTheory.InjectiveResolution.Hom.casesOn

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} →
          {I : CategoryTheory.InjectiveResolution Z} →
            {Z' : C} →
              {I' : CategoryTheory.InjectiveResolution Z'} →
                {f : Z ⟶ Z'} →
                  {motive : I.Hom I' f → Sort u_1} →
                    (t : I.Hom I' f) →
                      ((hom : I.cocomplex ⟶ I'.cocomplex) →
                          (ι_f_zero_comp_hom_f_zero :
                              CategoryTheory.CategoryStruct.comp (I.ι.f 0) (hom.f 0) =
                                CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0)
                                  (I'.ι.f 0)) →
                            motive { hom := hom, ι_f_zero_comp_hom_f_zero := ι_f_zero_comp_hom_f_zero }) →
                        motive t

Defined in

Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Cited by

0 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroObjectCategoryTheory.Limits.HasZeroMorphisms