Extend

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

Statistics

Metric	Count
Definitions hom', cochainComplex, cochainComplexXIso, π'	4
Theorems hom'_comp_π', hom'_comp_π'_assoc, hom'_f, hom'_f_assoc, cochainComplex_d, cochainComplex_d_assoc, instIsGECochainComplexOfNatInt, instIsStrictlyLECochainComplexOfNatInt, instProjectiveXIntCochainComplex, instQuasiIsoIntπ', π'_f_zero, π'_f_zero_assoc	12
Total	16

CategoryTheory.ProjectiveResolution

Definitions

Name	Category	Theorems
cochainComplex 📖	CompOp	26 math math: extEquivCohomologyClass_add, extEquivCohomologyClass_symm_sub, cochainComplex_d, extEquivCohomologyClass_sub, extEquivCohomologyClass_symm_mk_hom, extEquivCohomologyClass_zero, extAddEquivCohomologyClass_symm_apply, extMk_hom, instIsKProjectiveCochainComplex, Hom.hom'_f_assoc, π'_f_zero_assoc, Hom.hom'_comp_π', Hom.hom'_f, instIsGECochainComplexOfNatInt, extEquivCohomologyClass_symm_zero, Hom.hom'_comp_π'_assoc, π'_f_zero, instProjectiveXIntCochainComplex, instIsStrictlyLECochainComplexOfNatInt, extAddEquivCohomologyClass_apply, extEquivCohomologyClass_neg, extEquivCohomologyClass_extMk, instQuasiIsoIntπ', extEquivCohomologyClass_symm_add, cochainComplex_d_assoc, extEquivCohomologyClass_symm_neg
cochainComplexXIso 📖	CompOp	8 math math: cochainComplex_d, extMk_hom, Hom.hom'_f_assoc, π'_f_zero_assoc, Hom.hom'_f, π'_f_zero, extEquivCohomologyClass_extMk, cochainComplex_d_assoc
π' 📖	CompOp	7 math math: extEquivCohomologyClass_symm_mk_hom, extMk_hom, π'_f_zero_assoc, Hom.hom'_comp_π', Hom.hom'_comp_π'_assoc, π'_f_zero, instQuasiIsoIntπ'

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 ComplexShape.down AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne complex 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 ComplexShape.down AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne complex CategoryTheory.Iso.hom cochainComplexXIso CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cochainComplex_d
instIsGECochainComplexOfNatInt 📖	mathematical	—	CochainComplex.IsGE 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.instIsStrictlyGEObjIntSingleFunctor
instIsStrictlyLECochainComplexOfNatInt 📖	mathematical	—	CochainComplex.IsStrictlyLE CategoryTheory.Preadditive.preadditiveHasZeroMorphisms cochainComplex	—	CochainComplex.instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat
instProjectiveXIntCochainComplex 📖	mathematical	—	CategoryTheory.Projective 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.Projective.of_iso projective CategoryTheory.Limits.IsZero.projective CochainComplex.isZero_of_isStrictlyLE instIsStrictlyLECochainComplexOfNatInt
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 cochainComplex CategoryTheory.Abelian.hasZeroObject CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor π' 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 HomologicalComplex.instQuasiIsoExtendMap hasHomology quasiIso quasiIso_of_isIso CategoryTheory.Iso.isIso_hom
π'_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 cochainComplex CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor π' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne complex HomologicalComplex HomologicalComplex.single CategoryTheory.Iso.hom cochainComplexXIso ChainComplex ChainComplex.single₀ π CategoryTheory.Iso.inv HomologicalComplex.singleObjXSelf	—	AddRightCancelSemigroup.toIsRightCancelAdd CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero neg_zero HomologicalComplex.extendMap_f HomologicalComplex.extendSingleIso_hom_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 cochainComplex CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.singleFunctor HomologicalComplex.Hom.f π' ComplexShape.down AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne complex CategoryTheory.Iso.hom cochainComplexXIso ChainComplex ChainComplex.single₀ π CategoryTheory.Iso.inv HomologicalComplex HomologicalComplex.single HomologicalComplex.singleObjXSelf	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π'_f_zero

CategoryTheory.ProjectiveResolution.Hom

Definitions

Name	Category	Theorems
hom' 📖	CompOp	4 math math: hom'_f_assoc, hom'_comp_π', hom'_f, hom'_comp_π'_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom'_comp_π' 📖	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.ProjectiveResolution.cochainComplex CategoryTheory.Abelian.hasZeroObject CategoryTheory.Functor.obj CochainComplex.singleFunctor hom' CategoryTheory.ProjectiveResolution.π' CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject HomologicalComplex.to_single_hom_ext AddRightCancelSemigroup.toIsRightCancelAdd hom'_f CategoryTheory.ProjectiveResolution.π'_f_zero CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc hom_f_zero_comp_π_f_zero CategoryTheory.Category.id_comp
hom'_comp_π'_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.ProjectiveResolution.cochainComplex CategoryTheory.Abelian.hasZeroObject hom' CategoryTheory.Functor.obj CochainComplex.singleFunctor CategoryTheory.ProjectiveResolution.π' CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom'_comp_π'
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.ProjectiveResolution.cochainComplex CategoryTheory.Abelian.hasZeroObject hom' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.ProjectiveResolution.complex CategoryTheory.Iso.hom CategoryTheory.ProjectiveResolution.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.ProjectiveResolution.cochainComplex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.Hom.f hom' ComplexShape.down AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.ProjectiveResolution.complex CategoryTheory.Iso.hom CategoryTheory.ProjectiveResolution.cochainComplexXIso hom CategoryTheory.Iso.inv	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom'_f

---

← Back to Index