Extend

📁 Source: Mathlib/CategoryTheory/Abelian/Injective/Extend.lean

Statistics

Metric	Count
Definitions hom', cochainComplex, cochainComplexXIso, ι'	4
Theorems hom'_f, hom'_f_assoc, ι'_comp_hom', ι'_comp_hom'_assoc, cochainComplex_d, cochainComplex_d_assoc, instInjectiveXIntCochainComplex, instIsLECochainComplexOfNatInt, instIsStrictlyGECochainComplexOfNatInt, instIsStrictlyGECochainComplexOfNatInt_1, instQuasiIsoIntι', ι'_f_zero, ι'_f_zero_assoc	13
Total	17

CategoryTheory.InjectiveResolution

Definitions

Name	Category	Theorems
cochainComplex 📖	CompOp	27 math math: Hom.hom'_f, extEquivCohomologyClass_symm_neg, extEquivCohomologyClass_symm_add, ι'_f_zero, instIsLECochainComplexOfNatInt, extEquivCohomologyClass_symm_sub, extEquivCohomologyClass_sub, extEquivCohomologyClass_neg, extEquivCohomologyClass_symm_zero, ι'_f_zero_assoc, Hom.ι'_comp_hom'_assoc, extEquivCohomologyClass_add, Hom.hom'_f_assoc, extMk_hom, cochainComplex_d_assoc, extEquivCohomologyClass_zero, instIsKInjectiveCochainComplex, instQuasiIsoIntι', instIsStrictlyGECochainComplexOfNatInt_1, instIsStrictlyGECochainComplexOfNatInt, extEquivCohomologyClass_extMk, extEquivCohomologyClass_symm_mk_hom, Hom.ι'_comp_hom', extAddEquivCohomologyClass_symm_apply, instInjectiveXIntCochainComplex, extAddEquivCohomologyClass_apply, cochainComplex_d
cochainComplexXIso 📖	CompOp	8 math math: Hom.hom'_f, ι'_f_zero, ι'_f_zero_assoc, Hom.hom'_f_assoc, extMk_hom, cochainComplex_d_assoc, extEquivCohomologyClass_extMk, cochainComplex_d
ι' 📖	CompOp	7 math math: ι'_f_zero, ι'_f_zero_assoc, Hom.ι'_comp_hom'_assoc, extMk_hom, instQuasiIsoIntι', extEquivCohomologyClass_symm_mk_hom, Hom.ι'_comp_hom'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cochainComplex_d 📖	mathematical	—	HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne cocomplex CategoryTheory.Iso.hom cochainComplexXIso CategoryTheory.Iso.inv	—	HomologicalComplex.extend_d_eq AddRightCancelSemigroup.toIsRightCancelAdd
cochainComplex_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex HomologicalComplex.d AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne cocomplex CategoryTheory.Iso.hom cochainComplexXIso CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cochainComplex_d
instInjectiveXIntCochainComplex 📖	mathematical	—	CategoryTheory.Injective HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Injective.of_iso injective CategoryTheory.Limits.IsZero.injective CochainComplex.isZero_of_isStrictlyGE instIsStrictlyGECochainComplexOfNatInt_1
instIsLECochainComplexOfNatInt 📖	mathematical	—	CochainComplex.IsLE CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cochainComplex CategoryTheory.Abelian.hasZeroObject	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.isSupported_iff_of_quasiIso CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian instQuasiIsoIntι' HomologicalComplex.instIsSupportedOfIsStrictlySupported CochainComplex.instIsStrictlyLEObjIntSingleFunctor
instIsStrictlyGECochainComplexOfNatInt 📖	mathematical	—	CochainComplex.IsStrictlyGE CategoryTheory.Preadditive.preadditiveHasZeroMorphisms cochainComplex	—	CochainComplex.instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat
instIsStrictlyGECochainComplexOfNatInt_1 📖	mathematical	—	CochainComplex.IsStrictlyGE CategoryTheory.Preadditive.preadditiveHasZeroMorphisms cochainComplex	—	CochainComplex.instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat
instQuasiIsoIntι' 📖	mathematical	—	QuasiIso CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject cochainComplex ι' CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian quasiIso_comp HomologicalComplex.extend.instHasHomology HomologicalComplex.instHasHomologyObjSingle quasiIso_of_isIso CategoryTheory.Iso.isIso_inv HomologicalComplex.instQuasiIsoExtendMap hasHomology quasiIso
ι'_f_zero 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor cochainComplex ι' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex HomologicalComplex.single CategoryTheory.Iso.hom HomologicalComplex.singleObjXSelf AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne cocomplex CochainComplex.single₀ ι CategoryTheory.Iso.inv cochainComplexXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero HomologicalComplex.extendMap_f HomologicalComplex.extendSingleIso_inv_f CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc
ι'_f_zero_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor cochainComplex HomologicalComplex.Hom.f ι' CategoryTheory.Iso.hom HomologicalComplex HomologicalComplex.single HomologicalComplex.singleObjXSelf AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne cocomplex CochainComplex.single₀ ι CategoryTheory.Iso.inv cochainComplexXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι'_f_zero

CategoryTheory.InjectiveResolution.Hom

Definitions

Name	Category	Theorems
hom' 📖	CompOp	4 math math: hom'_f, ι'_comp_hom'_assoc, hom'_f_assoc, ι'_comp_hom'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom'_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.InjectiveResolution.cochainComplex CategoryTheory.Abelian.hasZeroObject hom' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.InjectiveResolution.cocomplex CategoryTheory.Iso.hom CategoryTheory.InjectiveResolution.cochainComplexXIso hom CategoryTheory.Iso.inv	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.extendMap_f
hom'_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.InjectiveResolution.cochainComplex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.Hom.f hom' AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.InjectiveResolution.cocomplex CategoryTheory.Iso.hom CategoryTheory.InjectiveResolution.cochainComplexXIso hom CategoryTheory.Iso.inv	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom'_f
ι'_comp_hom' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject CategoryTheory.InjectiveResolution.cochainComplex CategoryTheory.InjectiveResolution.ι' hom' CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject HomologicalComplex.from_single_hom_ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.InjectiveResolution.ι'_f_zero CategoryTheory.Category.id_comp hom'_f CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc ι_f_zero_comp_hom_f_zero_assoc CategoryTheory.Category.comp_id
ι'_comp_hom'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject CategoryTheory.InjectiveResolution.cochainComplex CategoryTheory.InjectiveResolution.ι' hom' CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι'_comp_hom'

---

← Back to Index