Documentation Verification Report

AlternatingConst

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

Statistics

Metric	Count
Definitions `alternatingFaceMapComplexConst`, `alternatingConst`, `alternatingConstHomologyDataEvenNEZero`, `alternatingConstHomologyDataOdd`, `alternatingConstHomologyDataZero`, `alternatingConstHomologyZero`, `alternatingConstHomotopyEquiv`, `alternatingConst`, `alternatingConstHomologyIsoEven`, `alternatingConstHomologyIsoOdd`, `alternatingConstScIsoEven`, `alternatingConstScIsoOdd`	12
Theorems `alternatingConst_exactAt`, `alternatingConst_map_f`, `alternatingConst_obj`, `instHasHomologyNatObjAlternatingConst`, `down_nat_odd_add`, `up_nat_odd_add`, `alternatingConst_X`, `alternatingConst_d`, `alternatingConst_iCycles_even_comp`, `alternatingConst_iCycles_even_comp_apply`, `alternatingConst_iCycles_even_comp_assoc`, `alternatingConst_iCycles_odd_comp`, `alternatingConst_iCycles_odd_comp_apply`, `alternatingConst_iCycles_odd_comp_assoc`	14
Total	26

AlgebraicTopology

Definitions

Name	Category	Theorems
`alternatingFaceMapComplexConst` 📖	CompOp	—

ChainComplex

Definitions

Name	Category	Theorems
`alternatingConst` 📖	CompOp	4 math math: `instHasHomologyNatObjAlternatingConst`, `alternatingConst_exactAt`, `alternatingConst_map_f`, `alternatingConst_obj`
`alternatingConstHomologyDataEvenNEZero` 📖	CompOp	—
`alternatingConstHomologyDataOdd` 📖	CompOp	—
`alternatingConstHomologyDataZero` 📖	CompOp	—
`alternatingConstHomologyZero` 📖	CompOp	—
`alternatingConstHomotopyEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`alternatingConst_exactAt` 📖	mathematical	—	`HomologicalComplex.ExactAt` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `alternatingConst`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.even_or_odd` `CategoryTheory.Limits.isZero_zero`
`alternatingConst_map_f` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.alternatingConst` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `ComplexShape.instDecidableRelRelDown` `ComplexShape.down_nat_odd_add` `CategoryTheory.Functor.map` `ChainComplex` `HomologicalComplex.instCategory` `AddRightCancelSemigroup.toIsRightCancelAdd` `alternatingConst`	—	`ComplexShape.down_nat_odd_add` `AddRightCancelSemigroup.toIsRightCancelAdd`
`alternatingConst_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `ChainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `alternatingConst` `HomologicalComplex.alternatingConst` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `ComplexShape.instDecidableRelRelDown` `ComplexShape.down_nat_odd_add`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`instHasHomologyNatObjAlternatingConst` 📖	mathematical	—	`HomologicalComplex.HasHomology` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `alternatingConst`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.even_or_odd`

ComplexShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`down_nat_odd_add` 📖	mathematical	`Rel` `down` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne`	`Odd` `Nat.instSemiring`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`up_nat_odd_add` 📖	mathematical	`Rel` `up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne`	`Odd` `Nat.instSemiring`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

HomologicalComplex

Definitions

Name	Category	Theorems
`alternatingConst` 📖	CompOp	13 math math: `alternatingConst_iCycles_odd_comp_assoc`, `Rep.FiniteCyclicGroup.chainComplexFunctor_obj`, `alternatingConst_iCycles_even_comp_apply`, `Rep.FiniteCyclicGroup.chainComplexFunctor_map_f`, `alternatingConst_iCycles_odd_comp`, `alternatingConst_iCycles_even_comp`, `alternatingConst_d`, `alternatingConst_iCycles_odd_comp_apply`, `alternatingConst_X`, `alternatingConst_iCycles_even_comp_assoc`, `ChainComplex.alternatingConst_map_f`, `ChainComplex.alternatingConst_obj`, `Rep.FiniteCyclicGroup.resolution.π_f`
`alternatingConstHomologyIsoEven` 📖	CompOp	—
`alternatingConstHomologyIsoOdd` 📖	CompOp	—
`alternatingConstScIsoEven` 📖	CompOp	—
`alternatingConstScIsoOdd` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`alternatingConst_X` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `Odd` `Nat.instSemiring`	`X` `alternatingConst`	—	—
`alternatingConst_d` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `Odd` `Nat.instSemiring`	`d` `alternatingConst` `ComplexShape.Rel` `Even` `Nat.instDecidablePredEven`	—	—
`alternatingConst_iCycles_even_comp` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `Odd` `Nat.instSemiring` `ComplexShape.Rel` `ComplexShape.prev` `ComplexShape.next` `Even`	`cycles` `alternatingConst` `CategoryTheory.CategoryWithHomology.hasHomology` `sc` `X` `iCycles`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.ShortComplex.cyclesMap_i_assoc` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.comp_zero` `CategoryTheory.ShortComplex.iCycles_g`
`alternatingConst_iCycles_even_comp_apply` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `Odd` `Nat.instSemiring` `ComplexShape.Rel` `ComplexShape.prev` `ComplexShape.next` `Even`	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `cycles` `alternatingConst` `CategoryTheory.CategoryWithHomology.hasHomology` `sc` `iCycles`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.comp_apply` `Mathlib.Tactic.Elementwise.hom_elementwise` `alternatingConst_iCycles_even_comp`
`alternatingConst_iCycles_even_comp_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `Odd` `Nat.instSemiring` `ComplexShape.Rel` `ComplexShape.prev` `ComplexShape.next` `Even`	`cycles` `alternatingConst` `CategoryTheory.CategoryWithHomology.hasHomology` `sc` `X` `iCycles`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `alternatingConst_iCycles_even_comp`
`alternatingConst_iCycles_odd_comp` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `Odd` `Nat.instSemiring` `ComplexShape.Rel` `ComplexShape.prev` `ComplexShape.next`	`cycles` `alternatingConst` `CategoryTheory.CategoryWithHomology.hasHomology` `sc` `X` `iCycles`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.ShortComplex.cyclesMap_i_assoc` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.comp_zero` `CategoryTheory.ShortComplex.iCycles_g`
`alternatingConst_iCycles_odd_comp_apply` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `Odd` `Nat.instSemiring` `ComplexShape.Rel` `ComplexShape.prev` `ComplexShape.next`	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `cycles` `alternatingConst` `CategoryTheory.CategoryWithHomology.hasHomology` `sc` `iCycles`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.comp_apply` `Mathlib.Tactic.Elementwise.hom_elementwise` `alternatingConst_iCycles_odd_comp`
`alternatingConst_iCycles_odd_comp_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `Odd` `Nat.instSemiring` `ComplexShape.Rel` `ComplexShape.prev` `ComplexShape.next`	`cycles` `alternatingConst` `CategoryTheory.CategoryWithHomology.hasHomology` `sc` `X` `iCycles`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `alternatingConst_iCycles_odd_comp`

---

← Back to Index