Documentation Verification Report

Augment

📁 Source: Mathlib/Algebra/Homology/Augment.lean

Statistics

Metric	Count
Definitions `augment`, `augmentTruncate`, `toSingle₀AsComplex`, `truncate`, `truncateAugment`, `truncateTo`, `augment`, `augmentTruncate`, `fromSingle₀AsComplex`, `toTruncate`, `truncate`, `truncateAugment`	12
Theorems `augmentTruncate_hom_f_succ`, `augmentTruncate_hom_f_zero`, `augmentTruncate_inv_f_succ`, `augmentTruncate_inv_f_zero`, `augment_X_succ`, `augment_X_zero`, `augment_d_one_zero`, `augment_d_succ_succ`, `chainComplex_d_succ_succ_zero`, `truncateAugment_hom_f`, `truncateAugment_inv_f`, `truncate_map_f`, `truncate_obj_X`, `truncate_obj_d`, `augmentTruncate_hom_f_succ`, `augmentTruncate_hom_f_zero`, `augmentTruncate_inv_f_succ`, `augmentTruncate_inv_f_zero`, `augment_X_succ`, `augment_X_zero`, `augment_d_succ_succ`, `augment_d_zero_one`, `cochainComplex_d_succ_succ_zero`, `truncateAugment_hom_f`, `truncateAugment_inv_f`, `truncate_map_f`, `truncate_obj_X`, `truncate_obj_d`	28
Total	40

ChainComplex

Definitions

Name	Category	Theorems
`augment` 📖	CompOp	10 math math: `truncateAugment_inv_f`, `augmentTruncate_inv_f_succ`, `augment_X_succ`, `augmentTruncate_hom_f_succ`, `truncateAugment_hom_f`, `augmentTruncate_hom_f_zero`, `augment_d_succ_succ`, `augmentTruncate_inv_f_zero`, `augment_X_zero`, `augment_d_one_zero`
`augmentTruncate` 📖	CompOp	4 math math: `augmentTruncate_inv_f_succ`, `augmentTruncate_hom_f_succ`, `augmentTruncate_hom_f_zero`, `augmentTruncate_inv_f_zero`
`toSingle₀AsComplex` 📖	CompOp	—
`truncate` 📖	CompOp	9 math math: `truncate_map_f`, `truncateAugment_inv_f`, `augmentTruncate_inv_f_succ`, `augmentTruncate_hom_f_succ`, `truncateAugment_hom_f`, `augmentTruncate_hom_f_zero`, `truncate_obj_d`, `augmentTruncate_inv_f_zero`, `truncate_obj_X`
`truncateAugment` 📖	CompOp	2 math math: `truncateAugment_inv_f`, `truncateAugment_hom_f`
`truncateTo` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`augmentTruncate_hom_f_succ` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `truncate` `HomologicalComplex.X` `HomologicalComplex.d` `HomologicalComplex.d_comp_d` `CategoryTheory.Iso.hom` `augmentTruncate` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.d_comp_d`
`augmentTruncate_hom_f_zero` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `truncate` `HomologicalComplex.X` `HomologicalComplex.d` `HomologicalComplex.d_comp_d` `CategoryTheory.Iso.hom` `augmentTruncate` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.d_comp_d`
`augmentTruncate_inv_f_succ` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `truncate` `HomologicalComplex.X` `HomologicalComplex.d` `HomologicalComplex.d_comp_d` `CategoryTheory.Iso.inv` `augmentTruncate` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.d_comp_d`
`augmentTruncate_inv_f_zero` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `truncate` `HomologicalComplex.X` `HomologicalComplex.d` `HomologicalComplex.d_comp_d` `CategoryTheory.Iso.inv` `augmentTruncate` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.d_comp_d`
`augment_X_succ` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`augment_X_zero` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`augment_d_one_zero` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`HomologicalComplex.d` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`augment_d_succ_succ` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`HomologicalComplex.d` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`chainComplex_d_succ_succ_zero` 📖	mathematical	—	`HomologicalComplex.d` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.shape`
`truncateAugment_hom_f` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`HomologicalComplex.Hom.f` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `truncate` `augment` `CategoryTheory.Iso.hom` `truncateAugment` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`truncateAugment_inv_f` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`HomologicalComplex.Hom.f` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `truncate` `augment` `CategoryTheory.Iso.inv` `truncateAugment` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`truncate_map_f` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.X` `HomologicalComplex.d` `CategoryTheory.Functor.map` `ChainComplex` `HomologicalComplex.instCategory` `AddRightCancelSemigroup.toIsRightCancelAdd` `truncate`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`truncate_obj_X` 📖	mathematical	—	`HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `AddRightCancelSemigroup.toIsRightCancelAdd` `truncate`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`truncate_obj_d` 📖	mathematical	—	`HomologicalComplex.d` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `AddRightCancelSemigroup.toIsRightCancelAdd` `truncate`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

CochainComplex

Definitions

Name	Category	Theorems
`augment` 📖	CompOp	10 math math: `augment_d_succ_succ`, `augmentTruncate_inv_f_zero`, `augment_X_zero`, `augment_X_succ`, `augment_d_zero_one`, `truncateAugment_inv_f`, `augmentTruncate_inv_f_succ`, `augmentTruncate_hom_f_succ`, `truncateAugment_hom_f`, `augmentTruncate_hom_f_zero`
`augmentTruncate` 📖	CompOp	4 math math: `augmentTruncate_inv_f_zero`, `augmentTruncate_inv_f_succ`, `augmentTruncate_hom_f_succ`, `augmentTruncate_hom_f_zero`
`fromSingle₀AsComplex` 📖	CompOp	—
`toTruncate` 📖	CompOp	—
`truncate` 📖	CompOp	9 math math: `augmentTruncate_inv_f_zero`, `truncate_obj_X`, `truncateAugment_inv_f`, `truncate_map_f`, `augmentTruncate_inv_f_succ`, `augmentTruncate_hom_f_succ`, `truncateAugment_hom_f`, `truncate_obj_d`, `augmentTruncate_hom_f_zero`
`truncateAugment` 📖	CompOp	2 math math: `truncateAugment_inv_f`, `truncateAugment_hom_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`augmentTruncate_hom_f_succ` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `truncate` `HomologicalComplex.X` `HomologicalComplex.d` `HomologicalComplex.d_comp_d` `CategoryTheory.Iso.hom` `augmentTruncate` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.d_comp_d`
`augmentTruncate_hom_f_zero` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `truncate` `HomologicalComplex.X` `HomologicalComplex.d` `HomologicalComplex.d_comp_d` `CategoryTheory.Iso.hom` `augmentTruncate` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.d_comp_d`
`augmentTruncate_inv_f_succ` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `truncate` `HomologicalComplex.X` `HomologicalComplex.d` `HomologicalComplex.d_comp_d` `CategoryTheory.Iso.inv` `augmentTruncate` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.d_comp_d`
`augmentTruncate_inv_f_zero` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `truncate` `HomologicalComplex.X` `HomologicalComplex.d` `HomologicalComplex.d_comp_d` `CategoryTheory.Iso.inv` `augmentTruncate` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.d_comp_d`
`augment_X_succ` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`HomologicalComplex.X` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`augment_X_zero` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`HomologicalComplex.X` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`augment_d_succ_succ` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`HomologicalComplex.d` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`augment_d_zero_one` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`HomologicalComplex.d` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `augment`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`cochainComplex_d_succ_succ_zero` 📖	mathematical	—	`HomologicalComplex.d` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.shape` `zero_add` `LT.lt.ne`
`truncateAugment_hom_f` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`HomologicalComplex.Hom.f` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `truncate` `augment` `CategoryTheory.Iso.hom` `truncateAugment` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`truncateAugment_inv_f` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	`HomologicalComplex.Hom.f` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `truncate` `augment` `CategoryTheory.Iso.inv` `truncateAugment` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`truncate_map_f` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.X` `HomologicalComplex.d` `CategoryTheory.Functor.map` `CochainComplex` `HomologicalComplex.instCategory` `AddRightCancelSemigroup.toIsRightCancelAdd` `truncate`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`truncate_obj_X` 📖	mathematical	—	`HomologicalComplex.X` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `AddRightCancelSemigroup.toIsRightCancelAdd` `truncate`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`truncate_obj_d` 📖	mathematical	—	`HomologicalComplex.d` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `AddRightCancelSemigroup.toIsRightCancelAdd` `truncate`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

---

← Back to Index