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 instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono HomologicalComplex HomologicalComplex.single CategoryTheory.Iso.hom HomologicalComplex.singleObjXSelf AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne cocomplex CochainComplex.single₀ ι CategoryTheory.Iso.inv cochainComplexXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono 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 instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono HomologicalComplex HomologicalComplex.single HomologicalComplex.singleObjXSelf AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne cocomplex CochainComplex.single₀ ι CategoryTheory.Iso.inv cochainComplexXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono 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