Mathlib Map

Theorems · Inductive type · category theory

CategoryTheory.InjectiveResolution.Hom

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

Given injective resolutions I and I' of two objects Z and Z', and a morphism f : Z ⟶ Z', this structure contains the data of a morphism I.cocomplex ⟶ I'.cocomplex which is compatible with f

Defined in
Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Cited by
12 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
CategoryTheory.CategoryCategoryTheory.Limits.HasZeroObjectCategoryTheory.Limits.HasZeroMorphisms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.InjectiveResolution.Hom.hom · cited by 8Hom.homCategoryTheory.InjectiveResolution.Hom.hom' · cited by 5Hom.hom'CategoryTheory.InjectiveResolution.Hom.hom'_f · cited by 3Hom.hom'_fCategoryTheory.InjectiveResolution.Hom.ι'_comp_hom' · cited by 2Hom.ι'_comp_hom'CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero · cited by 2Hom.ι_f_zero_comp_hom_f_z…CategoryTheory.InjectiveResolution.Hom.mk.inj · cited by 1mk.injCategoryTheory.InjectiveResolution.Hom.mk.noConfusion · cited by 1mk.noConfusionCategoryTheory.InjectiveResolution.Hom.ι_comp_hom · cited by 1Hom.ι_comp_homCategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero_assoc · cited by 1Hom.ι_f_zero_comp_hom_f_z…CategoryTheory.InjectiveResolution.Hom.mk.injEq · cited by 0mk.injEqCategoryTheory.InjectiveResolution.Hom.casesOn · cited by 0Hom.casesOnCategoryTheory.InjectiveResolution.Hom.ctorIdx · cited by 0Hom.ctorIdxCategoryTheory.InjectiveResolution.Hom.hom'_f_assoc · cited by 0Hom.hom'_f_assocCategoryTheory.InjectiveResolution.Hom.noConfusion · cited by 0Hom.noConfusionCategoryTheory.InjectiveResolution.Hom.noConfusionType · cited by 0Hom.noConfusionTypeCategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Limits.HasZeroMorphisms · cited by 3275Limits.HasZeroMorphismsCategoryTheory.Limits.HasZeroObject · cited by 1298Limits.HasZeroObjectCategoryTheory.InjectiveResolution · cited by 90CategoryTheory.InjectiveR…InjectiveResolution.HomCITED BYCITES

Cites5

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

Cited by20

Results whose statement or proof uses this declaration.