Degeneracies

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

Statistics

Metric	Count
Definitions	0
Theorems comp_σ, degeneracy_comp_PInfty, degeneracy_comp_PInfty_assoc, σ_comp_PInfty, σ_comp_PInfty_assoc, σ_comp_P_eq_zero	6
Total	6

AlgebraicTopology.DoldKan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
degeneracy_comp_PInfty 📖	mathematical	CategoryTheory.Mono SimplexCategory SimplexCategory.smallCategory	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite 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 CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.Hom.f PInfty Quiver.Hom CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd Fintype.complete SimplexCategory.mono_iff_injective SimplexCategory.eq_σ_comp_of_not_injective CategoryTheory.op_comp CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc σ_comp_PInfty CategoryTheory.Limits.comp_zero
degeneracy_comp_PInfty_assoc 📖	mathematical	CategoryTheory.Mono SimplexCategory SimplexCategory.smallCategory	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver 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 PInfty Quiver.Hom CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' degeneracy_comp_PInfty
σ_comp_PInfty 📖	mathematical	—	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 CategoryTheory.SimplicialObject.σ HomologicalComplex.Hom.f PInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd PInfty_f σ_comp_P_eq_zero covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd
σ_comp_PInfty_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.SimplicialObject.σ 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 PInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' σ_comp_PInfty
σ_comp_P_eq_zero 📖	mathematical	—	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 CategoryTheory.SimplicialObject.σ HomologicalComplex.Hom.f P Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd P_succ HomologicalComplex.comp_f CategoryTheory.Category.assoc CategoryTheory.Limits.zero_comp Fintype.complete CategoryTheory.Preadditive.comp_add CategoryTheory.Category.comp_id Homotopy.nullHomotopicMap'_f AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq zero_add hσ'_eq' add_zero Fin.sum_univ_two Fin.sum_univ_succ pow_zero one_smul pow_one neg_smul CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.neg_comp CategoryTheory.Category.id_comp CategoryTheory.Preadditive.comp_neg pow_add mul_neg neg_mul one_mul neg_neg CategoryTheory.SimplicialObject.δ_comp_σ_self CategoryTheory.SimplicialObject.δ_comp_σ_self_assoc CategoryTheory.SimplicialObject.δ_comp_σ_succ CategoryTheory.SimplicialObject.δ_comp_σ_of_le le_refl CategoryTheory.SimplicialObject.δ_comp_σ_succ_assoc add_neg_cancel P_add_Q_f HigherFacesVanish.comp_σ HigherFacesVanish.of_P HigherFacesVanish.comp_P_eq_self HigherFacesVanish.comp_Hσ_eq decomposition_Q CategoryTheory.Preadditive.sum_comp Finset.sum_eq_zero add_comm CategoryTheory.SimplicialObject.σ_comp_σ_assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.comp_zero add_neg_eq_zero

AlgebraicTopology.DoldKan.HigherFacesVanish

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_σ 📖	mathematical	AlgebraicTopology.DoldKan.HigherFacesVanish	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.SimplicialObject.σ	—	CategoryTheory.Category.assoc lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_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.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing Mathlib.Tactic.Linarith.lt_of_lt_of_eq neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one neg_eq_zero sub_eq_zero_of_eq Nat.cast_add Nat.cast_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd 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 add_comm add_assoc zero_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.instCanonicallyOrderedAdd Unique.instSubsingleton CategoryTheory.Limits.zero_comp

---

← Back to Index