Resolution

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

Statistics

Metric	Count
Definitions `shortComplex`, `desc`, `descCompHomotopy`, `descFOne`, `descFSucc`, `descFZero`, `descHomotopy`, `descHomotopyZero`, `descHomotopyZeroOne`, `descHomotopyZeroSucc`, `descHomotopyZeroZero`, `descIdHomotopy`, `homotopyEquiv`, `iso`, `of`, `ofCocomplex`, `injectiveResolution`, `injectiveResolutions`	18
Theorems `shortExact_shortComplex`, `comp_descHomotopyZeroOne`, `comp_descHomotopyZeroOne_assoc`, `comp_descHomotopyZeroSucc`, `comp_descHomotopyZeroSucc_assoc`, `comp_descHomotopyZeroZero`, `comp_descHomotopyZeroZero_assoc`, `descFOne_zero_comm`, `desc_commutes`, `desc_commutes_assoc`, `desc_commutes_zero`, `desc_commutes_zero_assoc`, `exact₀`, `homotopyEquiv_hom_ι`, `homotopyEquiv_hom_ι_assoc`, `homotopyEquiv_inv_ι`, `homotopyEquiv_inv_ι_assoc`, `instHasInjectiveResolution`, `instHasInjectiveResolutions`, `instInjectiveXNatOfCocomplex`, `iso_hom_naturality`, `iso_hom_naturality_assoc`, `iso_inv_naturality`, `iso_inv_naturality_assoc`, `ofCocomplex_d_0_1`, `ofCocomplex_exactAt_succ`, `of_def`, `exact_f_d`	28
Total	46

CategoryTheory

Definitions

Name	Category	Theorems
`injectiveResolution` 📖	CompOp	—
`injectiveResolutions` 📖	CompOp	4 math math: `InjectiveResolution.iso_hom_naturality`, `InjectiveResolution.iso_hom_naturality_assoc`, `InjectiveResolution.iso_inv_naturality_assoc`, `InjectiveResolution.iso_inv_naturality`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact_f_d` 📖	mathematical	—	`ShortComplex.Exact` `Preadditive.preadditiveHasZeroMorphisms` `Abelian.toPreadditive` `Injective.syzygies` `Limits.HasCokernels.has_colimit` `Abelian.has_cokernels` `Injective.d`	—	`Limits.HasCokernels.has_colimit` `Abelian.has_cokernels` `Limits.cokernel.condition` `Limits.cokernel.condition_assoc` `Limits.zero_comp` `Category.id_comp` `Category.comp_id` `ShortComplex.exact_iff_of_epi_of_isIso_of_mono` `instEpiId` `IsIso.id` `Injective.ι_mono` `ShortComplex.exact_of_g_is_cokernel` `CategoryWithHomology.hasHomology` `categoryWithHomology_of_abelian`

CategoryTheory.InjectivePresentation

Definitions

Name	Category	Theorems
`shortComplex` 📖	CompOp	1 math math: `shortExact_shortComplex`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`shortExact_shortComplex` 📖	mathematical	—	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `shortComplex`	—	`CategoryTheory.ShortComplex.exact_cokernel` `mono` `CategoryTheory.Limits.coequalizer.π_epi`

CategoryTheory.InjectiveResolution

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	4 math math: `desc_commutes_zero_assoc`, `desc_commutes`, `desc_commutes_assoc`, `desc_commutes_zero`
`descCompHomotopy` 📖	CompOp	—
`descFOne` 📖	CompOp	1 math math: `descFOne_zero_comm`
`descFSucc` 📖	CompOp	—
`descFZero` 📖	CompOp	1 math math: `descFOne_zero_comm`
`descHomotopy` 📖	CompOp	—
`descHomotopyZero` 📖	CompOp	—
`descHomotopyZeroOne` 📖	CompOp	2 math math: `comp_descHomotopyZeroOne_assoc`, `comp_descHomotopyZeroOne`
`descHomotopyZeroSucc` 📖	CompOp	2 math math: `comp_descHomotopyZeroSucc_assoc`, `comp_descHomotopyZeroSucc`
`descHomotopyZeroZero` 📖	CompOp	4 math math: `comp_descHomotopyZeroZero_assoc`, `comp_descHomotopyZeroOne_assoc`, `comp_descHomotopyZeroOne`, `comp_descHomotopyZeroZero`
`descIdHomotopy` 📖	CompOp	—
`homotopyEquiv` 📖	CompOp	4 math math: `homotopyEquiv_inv_ι`, `homotopyEquiv_hom_ι_assoc`, `homotopyEquiv_hom_ι`, `homotopyEquiv_inv_ι_assoc`
`iso` 📖	CompOp	4 math math: `iso_hom_naturality`, `iso_hom_naturality_assoc`, `iso_inv_naturality_assoc`, `iso_inv_naturality`
`of` 📖	CompOp	1 math math: `of_def`
`ofCocomplex` 📖	CompOp	4 math math: `of_def`, `ofCocomplex_d_0_1`, `ofCocomplex_exactAt_succ`, `instInjectiveXNatOfCocomplex`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_descHomotopyZeroOne` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `ι` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instZeroHom_1`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `HomologicalComplex.d` `descHomotopyZeroOne` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `HomologicalComplex.Hom.f` `descHomotopyZeroZero`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ShortComplex.Exact.comp_descToInjective` `HomologicalComplex.d_comp_d` `exact_succ`
`comp_descHomotopyZeroOne_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `ι` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instZeroHom_1`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `HomologicalComplex.d` `descHomotopyZeroOne` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `HomologicalComplex.Hom.f` `descHomotopyZeroZero`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_descHomotopyZeroOne`
`comp_descHomotopyZeroSucc` 📖	mathematical	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.CategoryStruct.comp` `HomologicalComplex.d`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `HomologicalComplex.d` `descHomotopyZeroSucc` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `HomologicalComplex.Hom.f`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ShortComplex.Exact.comp_descToInjective` `HomologicalComplex.d_comp_d` `exact_succ`
`comp_descHomotopyZeroSucc_assoc` 📖	mathematical	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.CategoryStruct.comp` `HomologicalComplex.d`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `HomologicalComplex.d` `descHomotopyZeroSucc` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `HomologicalComplex.Hom.f`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_descHomotopyZeroSucc`
`comp_descHomotopyZeroZero` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `ι` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instZeroHom_1`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `HomologicalComplex.d` `descHomotopyZeroZero` `HomologicalComplex.Hom.f`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ShortComplex.Exact.comp_descToInjective` `ι_f_zero_comp_complex_d` `exact₀`
`comp_descHomotopyZeroZero_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `ι` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instZeroHom_1`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `HomologicalComplex.d` `descHomotopyZeroZero` `HomologicalComplex.Hom.f`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_descHomotopyZeroZero`
`descFOne_zero_comm` 📖	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` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `HomologicalComplex.d` `descFOne` `descFZero`	—	`CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.ShortComplex.Exact.comp_descToInjective` `AddRightCancelSemigroup.toIsRightCancelAdd` `ι_f_zero_comp_complex_d` `exact₀`
`desc_commutes` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `ι` `desc` `CategoryTheory.Functor.map`	—	`CategoryTheory.Abelian.hasZeroObject` `HomologicalComplex.from_single_hom_ext` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Injective.comp_factorThru` `CochainComplex.single₀_map_f_zero`
`desc_commutes_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `ι` `desc` `CategoryTheory.Functor.map`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `desc_commutes`
`desc_commutes_zero` 📖	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` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `HomologicalComplex.Hom.f` `ι` `desc`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.congr_hom` `desc_commutes` `CochainComplex.single₀_map_f_zero`
`desc_commutes_zero_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` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `HomologicalComplex.Hom.f` `ι` `desc`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `desc_commutes_zero`
`exact₀` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.X` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `HomologicalComplex.Hom.f` `ι` `HomologicalComplex.d` `ι_f_zero_comp_complex_d`	—	`CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.ShortComplex.exact_of_f_is_kernel` `AddRightCancelSemigroup.toIsRightCancelAdd` `ι_f_zero_comp_complex_d` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian`
`homotopyEquiv_hom_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `ι` `HomotopyEquiv.hom` `homotopyEquiv`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `desc_commutes` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp`
`homotopyEquiv_hom_ι_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `ι` `HomotopyEquiv.hom` `homotopyEquiv`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homotopyEquiv_hom_ι`
`homotopyEquiv_inv_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `ι` `HomotopyEquiv.inv` `homotopyEquiv`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `desc_commutes` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp`
`homotopyEquiv_inv_ι_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `ι` `HomotopyEquiv.inv` `homotopyEquiv`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homotopyEquiv_inv_ι`
`instHasInjectiveResolution` 📖	mathematical	—	`CategoryTheory.HasInjectiveResolution` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.Abelian.hasZeroObject`
`instHasInjectiveResolutions` 📖	mathematical	—	`CategoryTheory.HasInjectiveResolutions` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.Abelian.hasZeroObject` `instHasInjectiveResolution`
`instInjectiveXNatOfCocomplex` 📖	mathematical	—	`CategoryTheory.Injective` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `ofCocomplex`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Injective.injective_under`
`iso_hom_naturality` 📖	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` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `HomologicalComplex.Hom.f` `ι`	`CategoryTheory.CategoryStruct.comp` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `Nat.instPartialOrder` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Nat.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instAddCommMonoid` `Nat.instPreorder` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instLinearOrder` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `instCategoryHomotopyCategory` `CategoryTheory.Functor.obj` `CategoryTheory.injectiveResolutions` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `iso`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomotopyCategory.eq_of_homotopy` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `desc_commutes_assoc` `homotopyEquiv_hom_ι` `homotopyEquiv_hom_ι_assoc` `HomologicalComplex.from_single_hom_ext` `CochainComplex.single₀_map_f_zero`
`iso_hom_naturality_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` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `HomologicalComplex.Hom.f` `ι`	`CategoryTheory.CategoryStruct.comp` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `Nat.instPartialOrder` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Nat.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instAddCommMonoid` `Nat.instPreorder` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instLinearOrder` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `instCategoryHomotopyCategory` `CategoryTheory.Functor.obj` `CategoryTheory.injectiveResolutions` `CategoryTheory.Functor.map` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Iso.hom` `iso`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_hom_naturality`
`iso_inv_naturality` 📖	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` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `HomologicalComplex.Hom.f` `ι`	`CategoryTheory.CategoryStruct.comp` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `Nat.instPartialOrder` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Nat.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instAddCommMonoid` `Nat.instPreorder` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instLinearOrder` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `instCategoryHomotopyCategory` `CategoryTheory.Functor.obj` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.injectiveResolutions` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Functor.map` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Category.assoc` `iso_hom_naturality` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id`
`iso_inv_naturality_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` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `CochainComplex.single₀` `CategoryTheory.Abelian.hasZeroObject` `cocomplex` `HomologicalComplex.Hom.f` `ι`	`CategoryTheory.CategoryStruct.comp` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `Nat.instPartialOrder` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Nat.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instAddCommMonoid` `Nat.instPreorder` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instLinearOrder` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `instCategoryHomotopyCategory` `CategoryTheory.Functor.obj` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `cocomplex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.injectiveResolutions` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Functor.map` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_inv_naturality`
`ofCocomplex_d_0_1` 📖	mathematical	—	`HomologicalComplex.d` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `ofCocomplex` `CategoryTheory.Injective.d` `CategoryTheory.Injective.under` `CategoryTheory.Injective.ι` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Abelian.has_cokernels`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Abelian.has_cokernels` `CochainComplex.mk'_d_1_0`
`ofCocomplex_exactAt_succ` 📖	mathematical	—	`HomologicalComplex.ExactAt` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `ofCocomplex`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.exactAt_iff'` `CochainComplex.prev_nat_succ` `CochainComplex.next` `HomologicalComplex.d_comp_d` `CochainComplex.of_d` `CategoryTheory.exact_f_d` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Abelian.has_cokernels` `CategoryTheory.Limits.hasCokernel_epi_comp` `CategoryTheory.Limits.coequalizer.π_epi`
`of_def` 📖	mathematical	—	`of` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ofCocomplex` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.CategoryStruct.comp` `HomologicalComplex.d` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CochainComplex` `HomologicalComplex.instCategory` `CategoryTheory.Functor.obj` `CochainComplex.single₀` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CochainComplex.fromSingle₀Equiv` `CategoryTheory.Injective.ι`	—	`CategoryTheory.Abelian.hasZeroObject`

---

← Back to Index