Resolution

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

Statistics

Metric	Count
Definitions `homotopyEquiv`, `iso`, `liftCompHomotopy`, `liftFOne`, `liftFSucc`, `liftFZero`, `liftHomotopy`, `liftHomotopyZero`, `liftHomotopyZeroOne`, `liftHomotopyZeroSucc`, `liftHomotopyZeroZero`, `liftIdHomotopy`, `of`, `ofComplex`, `projectiveResolution`, `projectiveResolutions`	16
Theorems `exact₀`, `homotopyEquiv_hom_π`, `homotopyEquiv_hom_π_assoc`, `homotopyEquiv_inv_π`, `homotopyEquiv_inv_π_assoc`, `instHasProjectiveResolution`, `instHasProjectiveResolutions`, `instProjectiveXNatOfComplex`, `iso_hom_naturality`, `iso_hom_naturality_assoc`, `iso_inv_naturality`, `iso_inv_naturality_assoc`, `liftFOne_zero_comm`, `liftHomotopyZeroOne_comp`, `liftHomotopyZeroOne_comp_assoc`, `liftHomotopyZeroSucc_comp`, `liftHomotopyZeroSucc_comp_assoc`, `liftHomotopyZeroZero_comp`, `liftHomotopyZeroZero_comp_assoc`, `lift_commutes`, `lift_commutes_assoc`, `lift_commutes_zero`, `lift_commutes_zero_assoc`, `ofComplex_d_1_0`, `ofComplex_exactAt_succ`, `of_def`, `exact_d_f`	27
Total	43

CategoryTheory

Definitions

Name	Category	Theorems
`projectiveResolution` 📖	CompOp	—
`projectiveResolutions` 📖	CompOp	4 math math: `ProjectiveResolution.iso_hom_naturality_assoc`, `ProjectiveResolution.iso_hom_naturality`, `ProjectiveResolution.iso_inv_naturality`, `ProjectiveResolution.iso_inv_naturality_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact_d_f` 📖	mathematical	—	`ShortComplex.Exact` `Preadditive.preadditiveHasZeroMorphisms` `Abelian.toPreadditive` `Projective.syzygies` `Limits.HasKernels.has_limit` `Abelian.has_kernels` `Projective.d`	—	`Limits.HasKernels.has_limit` `Abelian.has_kernels` `Category.assoc` `Limits.kernel.condition` `Limits.comp_zero` `Category.comp_id` `Category.id_comp` `ShortComplex.exact_iff_of_epi_of_isIso_of_mono` `Projective.π_epi` `IsIso.id` `instMonoId` `ShortComplex.exact_of_f_is_kernel` `CategoryWithHomology.hasHomology` `categoryWithHomology_of_abelian`

CategoryTheory.ProjectiveResolution

Definitions

Name	Category	Theorems
`homotopyEquiv` 📖	CompOp	4 math math: `homotopyEquiv_inv_π_assoc`, `homotopyEquiv_hom_π`, `homotopyEquiv_inv_π`, `homotopyEquiv_hom_π_assoc`
`iso` 📖	CompOp	4 math math: `iso_hom_naturality_assoc`, `iso_hom_naturality`, `iso_inv_naturality`, `iso_inv_naturality_assoc`
`liftCompHomotopy` 📖	CompOp	—
`liftFOne` 📖	CompOp	1 math math: `liftFOne_zero_comm`
`liftFSucc` 📖	CompOp	—
`liftFZero` 📖	CompOp	1 math math: `liftFOne_zero_comm`
`liftHomotopy` 📖	CompOp	—
`liftHomotopyZero` 📖	CompOp	—
`liftHomotopyZeroOne` 📖	CompOp	2 math math: `liftHomotopyZeroOne_comp_assoc`, `liftHomotopyZeroOne_comp`
`liftHomotopyZeroSucc` 📖	CompOp	2 math math: `liftHomotopyZeroSucc_comp`, `liftHomotopyZeroSucc_comp_assoc`
`liftHomotopyZeroZero` 📖	CompOp	4 math math: `liftHomotopyZeroZero_comp`, `liftHomotopyZeroOne_comp_assoc`, `liftHomotopyZeroZero_comp_assoc`, `liftHomotopyZeroOne_comp`
`liftIdHomotopy` 📖	CompOp	—
`of` 📖	CompOp	1 math math: `of_def`
`ofComplex` 📖	CompOp	4 math math: `ofComplex_d_1_0`, `instProjectiveXNatOfComplex`, `of_def`, `ofComplex_exactAt_succ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact₀` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `HomologicalComplex.d` `HomologicalComplex.Hom.f` `π` `complex_d_comp_π_f_zero`	—	`CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.ShortComplex.exact_of_g_is_cokernel` `AddRightCancelSemigroup.toIsRightCancelAdd` `complex_d_comp_π_f_zero` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian`
`homotopyEquiv_hom_π` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex` `ChainComplex.single₀` `HomotopyEquiv.hom` `homotopyEquiv` `π`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `lift_commutes` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id`
`homotopyEquiv_hom_π_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `complex` `CategoryTheory.Abelian.hasZeroObject` `HomotopyEquiv.hom` `homotopyEquiv` `CategoryTheory.Functor.obj` `ChainComplex` `ChainComplex.single₀` `π`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homotopyEquiv_hom_π`
`homotopyEquiv_inv_π` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex` `ChainComplex.single₀` `HomotopyEquiv.inv` `homotopyEquiv` `π`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `lift_commutes` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id`
`homotopyEquiv_inv_π_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `complex` `CategoryTheory.Abelian.hasZeroObject` `HomotopyEquiv.inv` `homotopyEquiv` `CategoryTheory.Functor.obj` `ChainComplex` `ChainComplex.single₀` `π`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homotopyEquiv_inv_π`
`instHasProjectiveResolution` 📖	mathematical	—	`CategoryTheory.HasProjectiveResolution` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.Abelian.hasZeroObject`
`instHasProjectiveResolutions` 📖	mathematical	—	`CategoryTheory.HasProjectiveResolutions` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.Abelian.hasZeroObject` `instHasProjectiveResolution`
`instProjectiveXNatOfComplex` 📖	mathematical	—	`CategoryTheory.Projective` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `ofComplex`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Projective.projective_over`
`iso_hom_naturality` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `HomologicalComplex.Hom.f` `π`	`HomotopyCategory` `instCategoryHomotopyCategory` `CategoryTheory.projectiveResolutions` `HomologicalComplex` `HomotopyCategory.quotient` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `iso`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv` `iso_inv_naturality_assoc` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id`
`iso_hom_naturality_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `HomologicalComplex.Hom.f` `π`	`HomotopyCategory` `instCategoryHomotopyCategory` `CategoryTheory.projectiveResolutions` `CategoryTheory.Functor.map` `HomologicalComplex` `HomotopyCategory.quotient` `CategoryTheory.Iso.hom` `iso`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `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.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `HomologicalComplex.Hom.f` `π`	`HomotopyCategory` `instCategoryHomotopyCategory` `HomologicalComplex` `HomotopyCategory.quotient` `CategoryTheory.projectiveResolutions` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomotopyCategory.eq_of_homotopy` `CategoryTheory.Category.assoc` `lift_commutes` `homotopyEquiv_inv_π_assoc` `homotopyEquiv_inv_π` `HomologicalComplex.to_single_hom_ext` `ChainComplex.single₀_map_f_zero`
`iso_inv_naturality_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `HomologicalComplex.Hom.f` `π`	`HomotopyCategory` `instCategoryHomotopyCategory` `HomologicalComplex` `HomotopyCategory.quotient` `CategoryTheory.projectiveResolutions` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_inv_naturality`
`liftFOne_zero_comm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `CategoryTheory.Abelian.hasZeroObject` `liftFOne` `HomologicalComplex.d` `liftFZero`	—	`CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.ShortComplex.Exact.liftFromProjective_comp` `AddRightCancelSemigroup.toIsRightCancelAdd` `complex_d_comp_π_f_zero` `exact₀`
`liftHomotopyZeroOne_comp` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex.single₀` `π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instZeroHom_1`	`HomologicalComplex.X` `liftHomotopyZeroOne` `HomologicalComplex.d` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `HomologicalComplex.Hom.f` `liftHomotopyZeroZero`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ShortComplex.Exact.liftFromProjective_comp` `HomologicalComplex.d_comp_d` `exact_succ`
`liftHomotopyZeroOne_comp_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex.single₀` `π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instZeroHom_1`	`HomologicalComplex.X` `liftHomotopyZeroOne` `HomologicalComplex.d` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `HomologicalComplex.Hom.f` `liftHomotopyZeroZero`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `liftHomotopyZeroOne_comp`
`liftHomotopyZeroSucc_comp` 📖	mathematical	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `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`	`liftHomotopyZeroSucc` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ShortComplex.Exact.liftFromProjective_comp` `HomologicalComplex.d_comp_d` `exact_succ`
`liftHomotopyZeroSucc_comp_assoc` 📖	mathematical	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `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`	`liftHomotopyZeroSucc` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `liftHomotopyZeroSucc_comp`
`liftHomotopyZeroZero_comp` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex.single₀` `π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instZeroHom_1`	`HomologicalComplex.X` `liftHomotopyZeroZero` `HomologicalComplex.d` `HomologicalComplex.Hom.f`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ShortComplex.Exact.liftFromProjective_comp` `complex_d_comp_π_f_zero` `exact₀`
`liftHomotopyZeroZero_comp_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex.single₀` `π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instZeroHom_1`	`HomologicalComplex.X` `liftHomotopyZeroZero` `HomologicalComplex.d` `HomologicalComplex.Hom.f`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `liftHomotopyZeroZero_comp`
`lift_commutes` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex.single₀` `lift` `π` `CategoryTheory.Functor.map`	—	`CategoryTheory.Abelian.hasZeroObject` `HomologicalComplex.to_single_hom_ext` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Projective.factorThru_comp` `ChainComplex.single₀_map_f_zero`
`lift_commutes_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `complex` `CategoryTheory.Abelian.hasZeroObject` `lift` `CategoryTheory.Functor.obj` `ChainComplex.single₀` `π` `CategoryTheory.Functor.map`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lift_commutes`
`lift_commutes_zero` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `HomologicalComplex.Hom.f` `lift` `π`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.congr_hom` `lift_commutes` `ChainComplex.single₀_map_f_zero`
`lift_commutes_zero_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `CategoryTheory.Abelian.hasZeroObject` `HomologicalComplex.Hom.f` `lift` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `π`	—	`CategoryTheory.Abelian.hasZeroObject` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lift_commutes_zero`
`ofComplex_d_1_0` 📖	mathematical	—	`HomologicalComplex.d` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `ofComplex` `CategoryTheory.Projective.d` `CategoryTheory.Projective.over` `CategoryTheory.Projective.π` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `ChainComplex.mk'_d_1_0`
`ofComplex_exactAt_succ` 📖	mathematical	—	`HomologicalComplex.ExactAt` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `ofComplex`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.exactAt_iff'` `ChainComplex.prev` `ChainComplex.next_nat_succ` `HomologicalComplex.d_comp_d` `ChainComplex.of_d` `CategoryTheory.exact_d_f`
`of_def` 📖	mathematical	—	`of` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ofComplex` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.CategoryStruct.comp` `HomologicalComplex.d` `CategoryTheory.Limits.HasZeroMorphisms.zero` `ChainComplex` `HomologicalComplex.instCategory` `CategoryTheory.Functor.obj` `ChainComplex.single₀` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `ChainComplex.toSingle₀Equiv` `CategoryTheory.Projective.π`	—	`CategoryTheory.Abelian.hasZeroObject`

---

← Back to Index