Documentation Verification Report

Decomposition

📁 Source: Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean

Statistics

Metric	Count
Definitions `MorphComponents`, `a`, `b`, `id`, `postComp`, `preComp`, `φ`	7
Theorems `ext`, `ext_iff`, `id_a`, `id_b`, `id_φ`, `postComp_a`, `postComp_b`, `postComp_φ`, `preComp_a`, `preComp_b`, `preComp_φ`, `decomposition_Q`	12
Total	19

AlgebraicTopology.DoldKan

Definitions

Name	Category	Theorems
`MorphComponents` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decomposition_Q` 📖	mathematical	—	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `Q` `Finset.sum` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `Finset.filter` `Finset.univ` `Fin.fintype` `CategoryTheory.CategoryStruct.comp` `P` `CategoryTheory.SimplicialObject.δ` `CategoryTheory.SimplicialObject.σ`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `Q_zero` `Finset.sum_congr` `Finset.filter.congr_simp` `Finset.filter_false` `Q_is_eventually_constant` `Finset.ext` `Q_succ` `HomologicalComplex.sub_f_apply` `HomologicalComplex.comp_f` `sub_eq_add_neg` `add_comm` `Finset.add_sum_erase` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass` `HigherFacesVanish.comp_Hσ_eq` `HigherFacesVanish.of_P` `neg_neg`

AlgebraicTopology.DoldKan.MorphComponents

Definitions

Name	Category	Theorems
`a` 📖	CompOp	4 math math: `preComp_a`, `postComp_a`, `ext_iff`, `id_a`
`b` 📖	CompOp	4 math math: `preComp_b`, `ext_iff`, `postComp_b`, `id_b`
`id` 📖	CompOp	3 math math: `id_φ`, `id_a`, `id_b`
`postComp` 📖	CompOp	3 math math: `postComp_a`, `postComp_b`, `postComp_φ`
`preComp` 📖	CompOp	3 math math: `preComp_a`, `preComp_b`, `preComp_φ`
`φ` 📖	CompOp	3 math math: `id_φ`, `preComp_φ`, `postComp_φ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`a` `b`	—	—	—
`ext_iff` 📖	mathematical	—	`a` `b`	—	`ext`
`id_a` 📖	mathematical	—	`a` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `id` `HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `AlgebraicTopology.DoldKan.PInfty`	—	—
`id_b` 📖	mathematical	—	`b` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `id` `CategoryTheory.SimplicialObject.σ`	—	—
`id_φ` 📖	mathematical	—	`φ` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `AlgebraicTopology.DoldKan.P_add_Q_f` `AlgebraicTopology.DoldKan.P_f_idem` `Finset.sum_congr` `Finset.filter.congr_simp` `Finset.filter_true` `AlgebraicTopology.DoldKan.decomposition_Q`
`postComp_a` 📖	mathematical	—	`a` `postComp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op`	—	—
`postComp_b` 📖	mathematical	—	`b` `postComp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op`	—	—
`postComp_φ` 📖	mathematical	—	`φ` `postComp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op`	—	`Finset.sum_congr` `CategoryTheory.Preadditive.add_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Preadditive.sum_comp`
`preComp_a` 📖	mathematical	—	`a` `preComp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `CategoryTheory.NatTrans.app`	—	—
`preComp_b` 📖	mathematical	—	`b` `preComp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `CategoryTheory.NatTrans.app`	—	—
`preComp_φ` 📖	mathematical	—	`φ` `preComp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `CategoryTheory.NatTrans.app`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.sum_congr` `CategoryTheory.Preadditive.comp_add` `AlgebraicTopology.DoldKan.P_f_naturality_assoc` `CategoryTheory.SimplicialObject.δ_naturality_assoc` `CategoryTheory.Preadditive.comp_sum`

---

← Back to Index