Documentation Verification Report

Faces

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

Statistics

Metric	Count
Definitions `HigherFacesVanish`	1
Theorems `comp_Hσ_eq`, `comp_Hσ_eq_zero`, `comp_δ_eq_zero`, `comp_δ_eq_zero_assoc`, `induction`, `of_comp`, `of_succ`	7
Total	8

AlgebraicTopology.DoldKan

Definitions

Name	Category	Theorems
`HigherFacesVanish` 📖	MathDef	4 math math: `HigherFacesVanish.inclusionOfMooreComplexMap`, `HigherFacesVanish.on_Γ₀_summand_id`, `HigherFacesVanish.of_P`, `comp_P_eq_self_iff`

AlgebraicTopology.DoldKan.HigherFacesVanish

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_Hσ_eq` 📖	mathematical	`AlgebraicTopology.DoldKan.HigherFacesVanish`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `HomologicalComplex.Hom.f` `AlgebraicTopology.DoldKan.Hσ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.SimplicialObject.δ` `CategoryTheory.SimplicialObject.σ`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `AlgebraicTopology.DoldKan.Hσ.eq_1` `Homotopy.nullHomotopicMap'_f` `AlgebraicTopology.DoldKan.hσ'_eq` `AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq` `CategoryTheory.Category.comp_id` `CategoryTheory.Preadditive.sum_comp` `CategoryTheory.Preadditive.comp_sum` `CategoryTheory.Preadditive.comp_add` `Finset.sum_congr` `CategoryTheory.Preadditive.comp_zsmul` `CategoryTheory.Preadditive.zsmul_comp` `Fin.sum_congr'` `Fin.sum_trunc` `CategoryTheory.Limits.zero_comp` `smul_zero` `CategoryTheory.Category.assoc` `add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `lt_of_lt_of_le` `CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'` `comp_δ_eq_zero_assoc` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Nat.instZeroLEOneClass` `zsmul_zero` `Fin.sum_univ_castSucc` `add_assoc` `add_zero` `add_comm` `pow_add` `Odd.neg_one_pow` `neg_smul` `one_zsmul` `CategoryTheory.SimplicialObject.δ_comp_σ_self'` `CategoryTheory.SimplicialObject.δ_comp_σ_succ'` `pow_one` `mul_neg` `mul_one` `neg_mul` `add_neg_cancel` `Finset.sum_add_distrib` `Finset.sum_eq_zero` `Fin.le_iff_val_le_val` `CategoryTheory.SimplicialObject.δ_comp_σ_of_le` `add_eq_zero_iff_eq_neg` `neg_zsmul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.neg_mul`
`comp_Hσ_eq_zero` 📖	mathematical	`AlgebraicTopology.DoldKan.HigherFacesVanish`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `AlgebraicTopology.AlternatingFaceMapComplex.obj` `HomologicalComplex.Hom.f` `AlgebraicTopology.DoldKan.Hσ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `Homotopy.nullHomotopicMap'_f` `AlgebraicTopology.DoldKan.hσ'_eq_zero` `CategoryTheory.Limits.comp_zero` `zero_add` `CategoryTheory.Limits.zero_comp` `AlgebraicTopology.DoldKan.hσ'_eq` `pow_zero` `one_zsmul` `CategoryTheory.Category.comp_id` `AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq` `CategoryTheory.Preadditive.comp_sum` `Fin.sum_univ_succ` `Fintype.sum_eq_zero` `CategoryTheory.Preadditive.comp_zsmul` `add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `lt_of_lt_of_le` `CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'` `comp_δ_eq_zero_assoc` `zsmul_zero` `add_zero` `one_smul` `CategoryTheory.SimplicialObject.δ_comp_σ_self` `pow_one` `neg_smul` `CategoryTheory.Preadditive.comp_neg` `CategoryTheory.SimplicialObject.δ_comp_σ_succ` `add_neg_cancel`
`comp_δ_eq_zero` 📖	mathematical	`AlgebraicTopology.DoldKan.HigherFacesVanish`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `CategoryTheory.SimplicialObject.δ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	—
`comp_δ_eq_zero_assoc` 📖	mathematical	`AlgebraicTopology.DoldKan.HigherFacesVanish`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `CategoryTheory.SimplicialObject.δ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_δ_eq_zero`
`induction` 📖	mathematical	`AlgebraicTopology.DoldKan.HigherFacesVanish`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op` `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` `Quiver.Hom` `ChainComplex` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instCategory` `HomologicalComplex.instAddHom` `CategoryTheory.CategoryStruct.id` `AlgebraicTopology.DoldKan.Hσ`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Preadditive.comp_add` `CategoryTheory.Category.comp_id` `CategoryTheory.Preadditive.add_comp` `comp_Hσ_eq_zero` `CategoryTheory.Limits.zero_comp` `add_zero` `comp_Hσ_eq` `CategoryTheory.Preadditive.neg_comp` `add_neg_eq_zero` `CategoryTheory.Category.assoc` `Fin.eq_zero` `CategoryTheory.SimplicialObject.δ_comp_σ_succ` `Ne.le_iff_lt` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `add_lt_add_iff_right` `lt_of_lt_of_le` `CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'` `LE.le.lt_or_eq` `Fin.le_iff_val_le_val` `CategoryTheory.SimplicialObject.δ_comp_δ''_assoc` `CategoryTheory.SimplicialObject.δ_comp_δ_self'_assoc`
`of_comp` 📖	mathematical	`AlgebraicTopology.DoldKan.HigherFacesVanish`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Opposite.op`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Limits.comp_zero`
`of_succ` 📖	—	`AlgebraicTopology.DoldKan.HigherFacesVanish`	—	—	`le_add_right` `Nat.instCanonicallyOrderedAdd`

---

← Back to Index