Projections

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

Statistics

Metric	Count
Definitions P, Q, natTransP, natTransQ	4
Theorems comp_P_eq_self, comp_P_eq_self_assoc, of_P, P_add_Q, P_add_Q_f, P_f_0_eq, P_f_idem, P_f_idem_assoc, P_f_naturality, P_f_naturality_assoc, P_idem, P_idem_assoc, P_succ, P_zero, Q_f_0_eq, Q_f_idem, Q_f_idem_assoc, Q_f_naturality, Q_f_naturality_assoc, Q_idem, Q_idem_assoc, Q_succ, Q_zero, comp_P_eq_self_iff, map_P, map_Q, natTransP_app, natTransQ_app	28
Total	32

AlgebraicTopology.DoldKan

Definitions

Name	Category	Theorems
P 📖	CompOp	24 math math: P_f_0_eq, HigherFacesVanish.of_P, homotopyPInftyToId_hom, comp_P_eq_self_iff, P_f_idem_assoc, P_f_idem, P_succ, PInfty_f, P_f_naturality_assoc, map_P, P_idem, natTransP_app, HigherFacesVanish.comp_P_eq_self_assoc, HigherFacesVanish.comp_P_eq_self, Q_succ, P_add_Q, P_is_eventually_constant, P_zero, homotopyPToId_eventually_constant, decomposition_Q, σ_comp_P_eq_zero, P_idem_assoc, P_f_naturality, P_add_Q_f
Q 📖	CompOp	16 math math: QInfty_f, Q_idem, Q_idem_assoc, Q_f_0_eq, Q_is_eventually_constant, Q_f_naturality_assoc, Q_succ, P_add_Q, map_Q, decomposition_Q, Q_f_idem_assoc, Q_f_naturality, Q_zero, P_add_Q_f, natTransQ_app, Q_f_idem
natTransP 📖	CompOp	1 math math: natTransP_app
natTransQ 📖	CompOp	1 math math: natTransQ_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
P_add_Q 📖	mathematical	—	Quiver.Hom ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AlgebraicTopology.AlternatingFaceMapComplex.obj HomologicalComplex.instAddHom P Q CategoryTheory.CategoryStruct.id	—	AddRightCancelSemigroup.toIsRightCancelAdd Q.eq_1 Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg zero_add Mathlib.Tactic.Abel.zero_termg
P_add_Q_f 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct 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.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup HomologicalComplex.Hom.f P Q CategoryTheory.CategoryStruct.id	—	HomologicalComplex.congr_hom AddRightCancelSemigroup.toIsRightCancelAdd P_add_Q
P_f_0_eq 📖	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 P CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct HomologicalComplex.X	—	AddRightCancelSemigroup.toIsRightCancelAdd Hσ_eq_zero add_zero CategoryTheory.Category.id_comp
P_f_idem 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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 P	—	AddRightCancelSemigroup.toIsRightCancelAdd P_f_0_eq CategoryTheory.Category.comp_id HigherFacesVanish.comp_P_eq_self HigherFacesVanish.of_P
P_f_idem_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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 P	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' P_f_idem
P_f_naturality 📖	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.NatTrans.app HomologicalComplex.Hom.f P	—	HomologicalComplex.congr_hom AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.NatTrans.naturality
P_f_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.NatTrans.app 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 P	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' P_f_naturality
P_idem 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AlgebraicTopology.AlternatingFaceMapComplex.obj P	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd P_f_idem
P_idem_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AlgebraicTopology.AlternatingFaceMapComplex.obj P	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' P_idem
P_succ 📖	mathematical	—	P CategoryTheory.CategoryStruct.comp ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AlgebraicTopology.AlternatingFaceMapComplex.obj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instAddHom CategoryTheory.CategoryStruct.id Hσ	—	AddRightCancelSemigroup.toIsRightCancelAdd
P_zero 📖	mathematical	—	P CategoryTheory.CategoryStruct.id ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AlgebraicTopology.AlternatingFaceMapComplex.obj	—	AddRightCancelSemigroup.toIsRightCancelAdd
Q_f_0_eq 📖	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 Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd P_f_0_eq sub_self
Q_f_idem 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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 Q	—	CategoryTheory.Idempotents.idem_of_id_sub_idem AddRightCancelSemigroup.toIsRightCancelAdd P_f_idem
Q_f_idem_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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 Q	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' Q_f_idem
Q_f_naturality 📖	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.NatTrans.app HomologicalComplex.Hom.f Q	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Preadditive.comp_sub P_f_naturality CategoryTheory.Preadditive.sub_comp CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
Q_f_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.NatTrans.app 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 Q	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' Q_f_naturality
Q_idem 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AlgebraicTopology.AlternatingFaceMapComplex.obj Q	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd Q_f_idem
Q_idem_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AlgebraicTopology.AlternatingFaceMapComplex.obj Q	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' Q_idem
Q_succ 📖	mathematical	—	Q Quiver.Hom ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AlgebraicTopology.AlternatingFaceMapComplex.obj HomologicalComplex.instSubHom CategoryTheory.CategoryStruct.comp P Hσ	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Preadditive.comp_add CategoryTheory.Category.comp_id Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.term_neg neg_zero
Q_zero 📖	mathematical	—	Q Quiver.Hom ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AlgebraicTopology.AlternatingFaceMapComplex.obj HomologicalComplex.instZeroHom_1	—	sub_self AddRightCancelSemigroup.toIsRightCancelAdd
comp_P_eq_self_iff 📖	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 HomologicalComplex.Hom.f P HigherFacesVanish	—	AddRightCancelSemigroup.toIsRightCancelAdd HigherFacesVanish.of_comp HigherFacesVanish.of_P HigherFacesVanish.comp_P_eq_self
map_P 📖	mathematical	—	CategoryTheory.Functor.map 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 P CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.SimplicialObject.whiskering	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.map_id CategoryTheory.Preadditive.comp_add CategoryTheory.Category.comp_id CategoryTheory.Functor.map_add CategoryTheory.Functor.map_comp map_Hσ
map_Q 📖	mathematical	—	CategoryTheory.Functor.map 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 Q CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.SimplicialObject.whiskering	—	AddRightCancelSemigroup.toIsRightCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd CategoryTheory.Functor.map_add map_P P_add_Q_f CategoryTheory.Functor.map_id
natTransP_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AlgebraicTopology.alternatingFaceMapComplex natTransP P	—	AddRightCancelSemigroup.toIsRightCancelAdd
natTransQ_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AlgebraicTopology.alternatingFaceMapComplex natTransQ Q	—	AddRightCancelSemigroup.toIsRightCancelAdd

AlgebraicTopology.DoldKan.HigherFacesVanish

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_P_eq_self 📖	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.P	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.comp_id CategoryTheory.Preadditive.comp_add of_succ AddLeftCancelSemigroup.toIsLeftCancelAdd comp_Hσ_eq_zero comp_Hσ_eq add_assoc le_refl CategoryTheory.Limits.zero_comp
comp_P_eq_self_assoc 📖	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.P	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_P_eq_self
of_P 📖	mathematical	—	AlgebraicTopology.DoldKan.HigherFacesVanish 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.P	—	AddRightCancelSemigroup.toIsRightCancelAdd induction

---

← Back to Index