FunctorGamma

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

Statistics

Metric	Count
Definitions Isδ₀, Γ₀, Γ₀', mapMono, map, obj₂, summand, map, obj, splitting, Γ₂	11
Theorems on_Γ₀_summand_id, eq_δ₀, iff, PInfty_on_Γ₀_splitting_summand_eq_self, PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Γ₀'_map_F, Γ₀'_map_f, Γ₀'_obj, mapMono_comp, mapMono_comp_assoc, mapMono_eq_zero, mapMono_id, mapMono_naturality, mapMono_naturality_assoc, mapMono_δ₀, mapMono_δ₀', mapMono_on_summand_id, mapMono_on_summand_id_assoc, map_epi_on_summand_id, map_epi_on_summand_id_assoc, map_on_summand, map_on_summand', map_on_summand'_assoc, map_on_summand_assoc, map_on_summand₀, map_on_summand₀', map_on_summand₀'_assoc, map_on_summand₀_assoc, map_app, obj_map, obj_obj, Γ₀_map_app, Γ₀_obj_map, Γ₀_obj_obj, Γ₂_map_f_app, Γ₂_obj_X_map, Γ₂_obj_X_obj, Γ₂_obj_p_app	38
Total	49

AlgebraicTopology.DoldKan

Definitions

Name	Category	Theorems
Isδ₀ 📖	MathDef	1 math math: Isδ₀.iff
Γ₀ 📖	CompOp	14 math math: N₂Γ₂ToKaroubiIso_inv_app, Γ₂_obj_p_app, Γ₀_obj_map, N₁Γ₀_hom_app_f_f, N₂Γ₂ToKaroubiIso_hom_app, N₂Γ₂_compatible_with_N₁Γ₀, whiskerLeft_toKaroubi_N₂Γ₂_hom, Γ₀_map_app, Γ₀_obj_obj, N₁Γ₀_hom_app, N₁Γ₀_inv_app, Γ₂_map_f_app, N₁Γ₀_inv_app_f_f, N₁Γ₀_app
Γ₀' 📖	CompOp	5 math math: Γ₀'_obj, Γ₀'_map_F, Γ₀_map_app, CategoryTheory.Idempotents.DoldKan.Γ_map_app, Γ₀'_map_f
Γ₂ 📖	CompOp	20 math math: N₂Γ₂ToKaroubiIso_inv_app, identity_N₂, instIsIsoFunctorSimplicialObjectKaroubiNatTrans, instIsIsoFunctorKaroubiSimplicialObjectNatTrans, Γ₂_obj_p_app, compatibility_Γ₂N₁_Γ₂N₂_natTrans, Γ₂N₂ToKaroubiIso_hom_app, Γ₂_obj_X_map, N₂Γ₂_inv_app_f_f, N₂Γ₂ToKaroubiIso_hom_app, N₂Γ₂_compatible_with_N₁Γ₀, whiskerLeft_toKaroubi_N₂Γ₂_hom, Γ₂N₂ToKaroubiIso_inv_app, Γ₂N₁.natTrans_app_f_app, Γ₂_obj_X_obj, Γ₂_map_f_app, Γ₂N₁_inv, identity_N₂_objectwise, Γ₂N₂_inv, Γ₂N₂.natTrans_app_f_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
PInfty_on_Γ₀_splitting_summand_eq_self 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.summand SimplicialObject.Splitting.N Γ₀.obj Γ₀.splitting Opposite.op SimplexCategory SimplicialObject.Splitting.IndexSet.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete SimplicialObject.Splitting.IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor SimplicialObject.Splitting.cofan 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 PInfty_f P_f_0_eq CategoryTheory.Category.comp_id HigherFacesVanish.comp_P_eq_self HigherFacesVanish.on_Γ₀_summand_id
PInfty_on_Γ₀_splitting_summand_eq_self_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.summand SimplicialObject.Splitting.N Γ₀.obj Γ₀.splitting Opposite.op SimplexCategory SimplicialObject.Splitting.IndexSet.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete SimplicialObject.Splitting.IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor SimplicialObject.Splitting.cofan 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_on_Γ₀_splitting_summand_eq_self
Γ₀'_map_F 📖	mathematical	—	SimplicialObject.Split.Hom.F SimplicialObject.Split.mk' Γ₀.obj Γ₀.splitting CategoryTheory.Functor.map ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd SimplicialObject.Split SimplicialObject.instCategorySplit Γ₀' Γ₀.map	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ₀'_map_f 📖	mathematical	—	SimplicialObject.Split.Hom.f SimplicialObject.Split.mk' Γ₀.obj Γ₀.splitting CategoryTheory.Functor.map ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd SimplicialObject.Split SimplicialObject.instCategorySplit Γ₀' HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ₀'_obj 📖	mathematical	—	CategoryTheory.Functor.obj ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd SimplicialObject.Split SimplicialObject.instCategorySplit Γ₀' SimplicialObject.Split.mk' Γ₀.obj Γ₀.splitting	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ₀_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj SimplicialObject.Split SimplicialObject.instCategorySplit CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject SimplicialObject.Split.forget ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup Γ₀' CategoryTheory.Functor.map AddRightCancelSemigroup.toIsRightCancelAdd Γ₀ SimplicialObject.Splitting.desc Γ₀.obj Γ₀.splitting Γ₀.Obj.obj₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.N SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi HomologicalComplex.X HomologicalComplex.Hom.f SimplicialObject.Splitting.IndexSet SimplicialObject.Splitting.summand SimplicialObject.Splitting.cofan	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ₀_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ₀ Γ₀.Obj.map	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ₀_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Γ₀ Γ₀.Obj.obj₂	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ₂_map_f_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Idempotents.Karoubi.X CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.obj ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight CategoryTheory.Idempotents.toKaroubi Γ₀ CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Functor.map CategoryTheory.Idempotents.Karoubi.p AddRightCancelSemigroup.toIsRightCancelAdd Γ₂ SimplicialObject.Splitting.desc Γ₀.obj Γ₀.splitting Γ₀.Obj.obj₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.N SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi HomologicalComplex.X HomologicalComplex.Hom.f SimplicialObject.Splitting.IndexSet SimplicialObject.Splitting.summand SimplicialObject.Splitting.cofan	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ₂_obj_X_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Idempotents.Karoubi.X CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.Karoubi.instCategory Γ₂ Γ₀.Obj.map	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ₂_obj_X_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Idempotents.Karoubi.X CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Idempotents.Karoubi.instCategory Γ₂ Γ₀.Obj.obj₂	—	AddRightCancelSemigroup.toIsRightCancelAdd
Γ₂_obj_p_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Idempotents.Karoubi.X CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.obj ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight CategoryTheory.Idempotents.toKaroubi Γ₀ CategoryTheory.Idempotents.Karoubi.p AddRightCancelSemigroup.toIsRightCancelAdd Γ₂ SimplicialObject.Splitting.desc Γ₀.obj Γ₀.splitting Γ₀.Obj.obj₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.N SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi HomologicalComplex.X HomologicalComplex.Hom.f SimplicialObject.Splitting.IndexSet SimplicialObject.Splitting.summand SimplicialObject.Splitting.cofan	—	AddRightCancelSemigroup.toIsRightCancelAdd

AlgebraicTopology.DoldKan.HigherFacesVanish

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
on_Γ₀_summand_id 📖	mathematical	—	AlgebraicTopology.DoldKan.HigherFacesVanish AlgebraicTopology.DoldKan.Γ₀.obj SimplicialObject.Splitting.summand SimplicialObject.Splitting.N AlgebraicTopology.DoldKan.Γ₀.splitting Opposite.op SimplexCategory SimplicialObject.Splitting.IndexSet.id SimplicialObject.Splitting.IndexSet SimplicialObject.Splitting.cofan	—	AddRightCancelSemigroup.toIsRightCancelAdd SimplexCategory.instMonoδ AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id CategoryTheory.Limits.zero_comp AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero

AlgebraicTopology.DoldKan.Isδ₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_δ₀ 📖	mathematical	AlgebraicTopology.DoldKan.Isδ₀	SimplexCategory.δ	—	SimplexCategory.eq_δ_of_mono SimplexCategory.instMonoδ iff
iff 📖	mathematical	—	AlgebraicTopology.DoldKan.Isδ₀ SimplexCategory.δ SimplexCategory.instMonoδ	—	SimplexCategory.instMonoδ Fin.succAbove_ne_zero_zero

AlgebraicTopology.DoldKan.Γ₀

Definitions

Name	Category	Theorems
map 📖	CompOp	2 math math: AlgebraicTopology.DoldKan.Γ₀'_map_F, map_app
obj 📖	CompOp	30 math math: AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f, AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id, Obj.map_epi_on_summand_id_assoc, Obj.map_on_summand_assoc, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, AlgebraicTopology.DoldKan.Γ₀'_obj, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, AlgebraicTopology.DoldKan.Γ₀'_map_F, Obj.mapMono_on_summand_id, AlgebraicTopology.DoldKan.Γ₀_map_app, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, map_app, Obj.map_on_summand, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, obj_map, CategoryTheory.Idempotents.DoldKan.Γ_map_app, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, Obj.mapMono_on_summand_id_assoc, AlgebraicTopology.DoldKan.Γ₂_map_f_app, obj_obj, Obj.map_epi_on_summand_id, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, Obj.map_on_summand', AlgebraicTopology.DoldKan.N₁Γ₀_app, Obj.map_on_summand'_assoc, AlgebraicTopology.DoldKan.Γ₀'_map_f
splitting 📖	CompOp	28 math math: AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f, AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id, Obj.map_epi_on_summand_id_assoc, Obj.map_on_summand_assoc, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, AlgebraicTopology.DoldKan.Γ₀'_obj, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, AlgebraicTopology.DoldKan.Γ₀'_map_F, Obj.mapMono_on_summand_id, AlgebraicTopology.DoldKan.Γ₀_map_app, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, map_app, Obj.map_on_summand, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, CategoryTheory.Idempotents.DoldKan.Γ_map_app, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, Obj.mapMono_on_summand_id_assoc, AlgebraicTopology.DoldKan.Γ₂_map_f_app, Obj.map_epi_on_summand_id, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, Obj.map_on_summand', AlgebraicTopology.DoldKan.N₁Γ₀_app, Obj.map_on_summand'_assoc, AlgebraicTopology.DoldKan.Γ₀'_map_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory obj map SimplicialObject.Splitting.desc splitting CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.N SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.Hom.f SimplicialObject.Splitting.IndexSet SimplicialObject.Splitting.summand SimplicialObject.Splitting.cofan	—	AddRightCancelSemigroup.toIsRightCancelAdd
obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory obj Obj.map	—	—
obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory obj Obj.obj₂	—	—

AlgebraicTopology.DoldKan.Γ₀.Obj

Definitions

Name	Category	Theorems
map 📖	CompOp	8 math math: map_on_summand₀', AlgebraicTopology.DoldKan.Γ₀_obj_map, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, map_on_summand₀, map_on_summand₀'_assoc, CategoryTheory.Idempotents.DoldKan.Γ_obj_map, map_on_summand₀_assoc, AlgebraicTopology.DoldKan.Γ₀.obj_map
obj₂ 📖	CompOp	12 math math: map_on_summand₀', AlgebraicTopology.DoldKan.Γ₂_obj_p_app, map_on_summand₀, AlgebraicTopology.DoldKan.Γ₀_map_app, map_on_summand₀'_assoc, AlgebraicTopology.DoldKan.Γ₀_obj_obj, CategoryTheory.Idempotents.DoldKan.Γ_obj_obj, map_on_summand₀_assoc, CategoryTheory.Idempotents.DoldKan.Γ_map_app, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, AlgebraicTopology.DoldKan.Γ₂_map_f_app, AlgebraicTopology.DoldKan.Γ₀.obj_obj
summand 📖	CompOp	4 math math: map_on_summand₀', map_on_summand₀, map_on_summand₀'_assoc, map_on_summand₀_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMono_on_summand_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.summand SimplicialObject.Splitting.N AlgebraicTopology.DoldKan.Γ₀.obj AlgebraicTopology.DoldKan.Γ₀.splitting Opposite.op SimplexCategory SimplicialObject.Splitting.IndexSet.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete SimplicialObject.Splitting.IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor SimplicialObject.Splitting.cofan CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory 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 SimplexCategory.len Termwise.mapMono	—	map_on_summand CategoryTheory.instEpiId
mapMono_on_summand_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.summand SimplicialObject.Splitting.N AlgebraicTopology.DoldKan.Γ₀.obj AlgebraicTopology.DoldKan.Γ₀.splitting Opposite.op SimplexCategory SimplicialObject.Splitting.IndexSet.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete SimplicialObject.Splitting.IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor SimplicialObject.Splitting.cofan CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory 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 SimplexCategory.len Termwise.mapMono	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapMono_on_summand_id
map_epi_on_summand_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.summand SimplicialObject.Splitting.N AlgebraicTopology.DoldKan.Γ₀.obj AlgebraicTopology.DoldKan.Γ₀.splitting Opposite.op SimplexCategory SimplicialObject.Splitting.IndexSet.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete SimplicialObject.Splitting.IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor SimplicialObject.Splitting.cofan CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.instMonoId map_on_summand Termwise.mapMono_id CategoryTheory.Category.id_comp
map_epi_on_summand_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.summand SimplicialObject.Splitting.N AlgebraicTopology.DoldKan.Γ₀.obj AlgebraicTopology.DoldKan.Γ₀.splitting Opposite.op SimplexCategory SimplicialObject.Splitting.IndexSet.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete SimplicialObject.Splitting.IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor SimplicialObject.Splitting.cofan CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_epi_on_summand_id
map_on_summand 📖	mathematical	CategoryTheory.CategoryStruct.comp SimplexCategory CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi Quiver.Hom.unop SimplicialObject.Splitting.IndexSet.e	SimplicialObject.Splitting.summand SimplicialObject.Splitting.N AlgebraicTopology.DoldKan.Γ₀.obj AlgebraicTopology.DoldKan.Γ₀.splitting CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete SimplicialObject.Splitting.IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor SimplicialObject.Splitting.cofan CategoryTheory.Functor.obj CategoryTheory.Category.opposite 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 SimplexCategory.len Termwise.mapMono	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete Finite.of_fintype map_on_summand₀ CategoryTheory.Category.comp_id CategoryTheory.instMonoId Termwise.mapMono_id CategoryTheory.Category.id_comp
map_on_summand' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.summand SimplicialObject.Splitting.N AlgebraicTopology.DoldKan.Γ₀.obj AlgebraicTopology.DoldKan.Γ₀.splitting CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete SimplicialObject.Splitting.IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor SimplicialObject.Splitting.cofan CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory 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 SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi CategoryTheory.Limits.image Quiver.Hom.unop SimplicialObject.Splitting.IndexSet.e CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations Termwise.mapMono CategoryTheory.Limits.image.ι CategoryTheory.Limits.instMonoι SimplicialObject.Splitting.IndexSet.pull	—	map_on_summand CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.instMonoι CategoryTheory.Limits.image.fac
map_on_summand'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.summand SimplicialObject.Splitting.N AlgebraicTopology.DoldKan.Γ₀.obj AlgebraicTopology.DoldKan.Γ₀.splitting CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete SimplicialObject.Splitting.IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor SimplicialObject.Splitting.cofan CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory 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 SimplexCategory.len CategoryTheory.Limits.image Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi Quiver.Hom.unop SimplicialObject.Splitting.IndexSet.e CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations Termwise.mapMono CategoryTheory.Limits.image.ι CategoryTheory.Limits.instMonoι SimplicialObject.Splitting.IndexSet.pull	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.instMonoι CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_on_summand'
map_on_summand_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SimplexCategory CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi Quiver.Hom.unop SimplicialObject.Splitting.IndexSet.e	SimplicialObject.Splitting.summand SimplicialObject.Splitting.N AlgebraicTopology.DoldKan.Γ₀.obj AlgebraicTopology.DoldKan.Γ₀.splitting CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete SimplicialObject.Splitting.IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor SimplicialObject.Splitting.cofan CategoryTheory.Functor.obj CategoryTheory.Category.opposite 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 SimplexCategory.len Termwise.mapMono	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_on_summand
map_on_summand₀ 📖	mathematical	CategoryTheory.CategoryStruct.comp SimplexCategory CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi Quiver.Hom.unop SimplicialObject.Splitting.IndexSet.e	summand CategoryTheory.Limits.sigmaObj SimplicialObject.Splitting.IndexSet CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete Finite.of_fintype SimplicialObject.Splitting.IndexSet.instFintype CategoryTheory.Discrete.functor obj₂ CategoryTheory.Limits.Sigma.ι map HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne SimplexCategory.len Termwise.mapMono	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete Finite.of_fintype AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations SimplexCategory.image_eq SimplexCategory.image_ι_eq SimplexCategory.factorThruImage_eq
map_on_summand₀' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand CategoryTheory.Limits.sigmaObj SimplicialObject.Splitting.IndexSet CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete Finite.of_fintype SimplicialObject.Splitting.IndexSet.instFintype CategoryTheory.Discrete.functor obj₂ CategoryTheory.Limits.Sigma.ι map HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne SimplexCategory.len Opposite.unop SimplexCategory Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SimplexCategory.smallCategory CategoryTheory.Epi CategoryTheory.Limits.image Quiver.Hom.unop SimplicialObject.Splitting.IndexSet.e CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations Termwise.mapMono CategoryTheory.Limits.image.ι CategoryTheory.Limits.instMonoι SimplicialObject.Splitting.IndexSet.pull	—	map_on_summand₀ CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.instMonoι SimplicialObject.Splitting.IndexSet.fac_pull
map_on_summand₀'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand CategoryTheory.Limits.sigmaObj SimplicialObject.Splitting.IndexSet CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete Finite.of_fintype SimplicialObject.Splitting.IndexSet.instFintype CategoryTheory.Discrete.functor CategoryTheory.Limits.Sigma.ι obj₂ map HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne SimplexCategory.len CategoryTheory.Limits.image SimplexCategory SimplexCategory.smallCategory Opposite.unop Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi Quiver.Hom.unop SimplicialObject.Splitting.IndexSet.e CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations Termwise.mapMono CategoryTheory.Limits.image.ι CategoryTheory.Limits.instMonoι SimplicialObject.Splitting.IndexSet.pull	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete Finite.of_fintype AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations CategoryTheory.Limits.instMonoι CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_on_summand₀'
map_on_summand₀_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp SimplexCategory CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi Quiver.Hom.unop SimplicialObject.Splitting.IndexSet.e	summand CategoryTheory.Limits.sigmaObj SimplicialObject.Splitting.IndexSet CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete Finite.of_fintype SimplicialObject.Splitting.IndexSet.instFintype CategoryTheory.Discrete.functor CategoryTheory.Limits.Sigma.ι obj₂ map HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne SimplexCategory.len Termwise.mapMono	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete Finite.of_fintype AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_on_summand₀

AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise

Definitions

Name	Category	Theorems
mapMono 📖	CompOp	20 math math: mapMono_comp_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, mapMono_δ₀', mapMono_comp, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, mapMono_eq_zero, mapMono_naturality, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, mapMono_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, mapMono_naturality_assoc, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, mapMono_δ₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMono_comp 📖	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 SimplexCategory.len mapMono SimplexCategory SimplexCategory.smallCategory CategoryTheory.mono_comp	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.mono_comp SimplexCategory.eq_id_of_mono CategoryTheory.Category.comp_id mapMono.congr_simp mapMono_id CategoryTheory.Category.id_comp SimplexCategory.len_lt_of_mono mapMono_eq_zero AddLeftCancelSemigroup.toIsLeftCancelAdd Unique.instSubsingleton mapMono_δ₀' HomologicalComplex.d_comp_d CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp
mapMono_comp_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 SimplexCategory.len mapMono SimplexCategory SimplexCategory.smallCategory CategoryTheory.mono_comp	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.mono_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapMono_comp
mapMono_eq_zero 📖	mathematical	AlgebraicTopology.DoldKan.Isδ₀	mapMono 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 SimplexCategory.len CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd
mapMono_id 📖	mathematical	—	mapMono CategoryTheory.CategoryStruct.id SimplexCategory CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory CategoryTheory.instMonoId HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne SimplexCategory.len	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.instMonoId
mapMono_naturality 📖	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 SimplexCategory.len mapMono HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id HomologicalComplex.Hom.comm CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero
mapMono_naturality_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 SimplexCategory.len mapMono HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapMono_naturality
mapMono_δ₀ 📖	mathematical	—	mapMono SimplexCategory.δ SimplexCategory.instMonoδ HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	mapMono_δ₀' SimplexCategory.instMonoδ AlgebraicTopology.DoldKan.Isδ₀.iff
mapMono_δ₀' 📖	mathematical	AlgebraicTopology.DoldKan.Isδ₀	mapMono HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne SimplexCategory.len	—	AddRightCancelSemigroup.toIsRightCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd

---

← Back to Index