PInfty

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

Statistics

Metric	Count
Definitions PInfty, QInfty, natTransPInfty, natTransPInfty_f	4
Theorems PInfty_add_QInfty, PInfty_comp_QInfty, PInfty_comp_QInfty_assoc, PInfty_f, PInfty_f_0, PInfty_f_add_QInfty_f, PInfty_f_comp_QInfty_f, PInfty_f_comp_QInfty_f_assoc, PInfty_f_idem, PInfty_f_idem_assoc, PInfty_f_naturality, PInfty_f_naturality_assoc, PInfty_idem, PInfty_idem_assoc, P_is_eventually_constant, QInfty_comp_PInfty, QInfty_comp_PInfty_assoc, QInfty_f, QInfty_f_0, QInfty_f_comp_PInfty_f, QInfty_f_comp_PInfty_f_assoc, QInfty_f_idem, QInfty_f_idem_assoc, QInfty_f_naturality, QInfty_f_naturality_assoc, QInfty_idem, QInfty_idem_assoc, Q_is_eventually_constant, karoubi_PInfty_f, map_PInfty_f, natTransPInfty_app, natTransPInfty_f_app	32
Total	36

AlgebraicTopology.DoldKan

Definitions

Name	Category	Theorems
PInfty 📖	CompOp	61 math math: natTransPInfty_app, PInfty_comp_PInftyToNormalizedMooreComplex, PInfty_f_add_QInfty_f, σ_comp_PInfty_assoc, N₁_map_f, N₂Γ₂ToKaroubiIso_inv_app, PInfty_comp_QInfty, SimplicialObject.Splitting.PInfty_comp_πSummand_id, PInfty_idem, homotopyPInftyToId_hom, PInftyToNormalizedMooreComplex_f, PInfty_f_naturality_assoc, N₁_obj_p, PInfty_f_comp_QInfty_f_assoc, PInfty_on_Γ₀_splitting_summand_eq_self_assoc, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, QInfty_f_comp_PInfty_f, inclusionOfMooreComplexMap_comp_PInfty_assoc, PInfty_comp_map_mono_eq_zero, SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero, PInfty_idem_assoc, inclusionOfMooreComplexMap_comp_PInfty, N₂Γ₂ToKaroubiIso_hom_app, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, map_PInfty_f, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, QInfty_comp_PInfty, PInfty_f, toKaroubiCompN₂IsoN₁_hom_app, PInfty_on_Γ₀_splitting_summand_eq_self, degeneracy_comp_PInfty_assoc, toKaroubiCompN₂IsoN₁_inv_app, PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc, natTransPInfty_f_app, MorphComponents.id_a, PInfty_f_0, PInfty_f_naturality, PInfty_f_idem_assoc, homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, PInfty_f_idem, N₂_obj_p_f, σ_comp_PInfty, CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f, PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, karoubi_PInfty_f, SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, Γ₂N₁.natTrans_app_f_app, degeneracy_comp_PInfty, PInfty_f_comp_QInfty_f, QInfty_comp_PInfty_assoc, QInfty_f_comp_PInfty_f_assoc, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, PInfty_comp_PInftyToNormalizedMooreComplex_assoc, PInfty_comp_QInfty_assoc, Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, N₂_map_f_f, factors_normalizedMooreComplex_PInfty, Γ₀_obj_termwise_mapMono_comp_PInfty, PInfty_add_QInfty
QInfty 📖	CompOp	18 math math: PInfty_f_add_QInfty_f, PInfty_comp_QInfty, QInfty_idem, QInfty_idem_assoc, QInfty_f, PInfty_f_comp_QInfty_f_assoc, QInfty_f_0, QInfty_f_comp_PInfty_f, QInfty_f_naturality_assoc, QInfty_comp_PInfty, QInfty_f_naturality, QInfty_f_idem_assoc, QInfty_f_idem, PInfty_f_comp_QInfty_f, QInfty_comp_PInfty_assoc, QInfty_f_comp_PInfty_f_assoc, PInfty_comp_QInfty_assoc, PInfty_add_QInfty
natTransPInfty 📖	CompOp	1 math math: natTransPInfty_app
natTransPInfty_f 📖	CompOp	1 math math: natTransPInfty_f_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
PInfty_add_QInfty 📖	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 PInfty QInfty CategoryTheory.CategoryStruct.id	—	AddRightCancelSemigroup.toIsRightCancelAdd add_sub_cancel
PInfty_comp_QInfty 📖	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 PInfty QInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd PInfty_f_comp_QInfty_f
PInfty_comp_QInfty_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 PInfty QInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' PInfty_comp_QInfty
PInfty_f 📖	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 PInfty P	—	AddRightCancelSemigroup.toIsRightCancelAdd
PInfty_f_0 📖	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 PInfty CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct HomologicalComplex.X	—	AddRightCancelSemigroup.toIsRightCancelAdd
PInfty_f_add_QInfty_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 AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup HomologicalComplex.Hom.f PInfty QInfty CategoryTheory.CategoryStruct.id	—	HomologicalComplex.congr_hom AddRightCancelSemigroup.toIsRightCancelAdd PInfty_add_QInfty
PInfty_f_comp_QInfty_f 📖	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 PInfty QInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Preadditive.comp_sub CategoryTheory.Category.comp_id PInfty_f_idem sub_self
PInfty_f_comp_QInfty_f_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 PInfty QInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' PInfty_f_comp_QInfty_f
PInfty_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 PInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd P_f_idem
PInfty_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 PInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' PInfty_f_idem
PInfty_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 PInfty	—	P_f_naturality
PInfty_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 PInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' PInfty_f_naturality
PInfty_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 PInfty	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd PInfty_f_idem
PInfty_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 PInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' PInfty_idem
P_is_eventually_constant 📖	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	—	AddRightCancelSemigroup.toIsRightCancelAdd P_f_0_eq CategoryTheory.Preadditive.comp_add CategoryTheory.Category.comp_id AddLeftCancelSemigroup.toIsLeftCancelAdd HigherFacesVanish.comp_Hσ_eq_zero HigherFacesVanish.of_P
QInfty_comp_PInfty 📖	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 QInfty PInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd QInfty_f_comp_PInfty_f
QInfty_comp_PInfty_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 QInfty PInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' QInfty_comp_PInfty
QInfty_f 📖	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 QInfty Q	—	AddRightCancelSemigroup.toIsRightCancelAdd
QInfty_f_0 📖	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 QInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd sub_self
QInfty_f_comp_PInfty_f 📖	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 QInfty PInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Preadditive.sub_comp CategoryTheory.Category.id_comp PInfty_f_idem sub_self
QInfty_f_comp_PInfty_f_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 QInfty PInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' QInfty_f_comp_PInfty_f
QInfty_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 QInfty	—	Q_f_idem
QInfty_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 QInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' QInfty_f_idem
QInfty_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 QInfty	—	Q_f_naturality
QInfty_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 QInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' QInfty_f_naturality
QInfty_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 QInfty	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd QInfty_f_idem
QInfty_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 QInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' QInfty_idem
Q_is_eventually_constant 📖	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	—	AddRightCancelSemigroup.toIsRightCancelAdd P_is_eventually_constant
karoubi_PInfty_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f HomologicalComplex.X CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Idempotents.instPreadditiveKaroubi ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj CategoryTheory.Functor.obj CategoryTheory.Functor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.category CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding HomologicalComplex.Hom.f PInfty CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Idempotents.Karoubi.X CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Idempotents.Karoubi.p	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.Karoubi.hom_ext_iff map_PInfty_f CategoryTheory.Idempotents.instAdditiveKaroubiToKaroubi CategoryTheory.Functor.congr_obj CategoryTheory.Idempotents.toKaroubi_comp_karoubiFunctorCategoryEmbedding CategoryTheory.Idempotents.natTrans_eq CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp PInfty_f_naturality CategoryTheory.Idempotents.app_idem_assoc
map_PInfty_f 📖	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 CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.SimplicialObject.whiskering PInfty CategoryTheory.Functor.map HomologicalComplex.X	—	AddRightCancelSemigroup.toIsRightCancelAdd map_P
natTransPInfty_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 natTransPInfty PInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd
natTransPInfty_f_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.comp 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 HomologicalComplex.eval natTransPInfty_f HomologicalComplex.Hom.f CategoryTheory.Functor.obj PInfty	—	CategoryTheory.Category.id_comp

---

← Back to Index