Split

📁 Source: Mathlib/AlgebraicTopology/SimplicialObject/Split.lean

Statistics

Metric	Count
Definitions Split, F, f, X, evalN, forget, mk', natTransCofanInj, s, Splitting, IndexSet, EqId, e, epiComp, id, instFintype, instInhabited, mk, pull, N, cofan, cofan', desc, isColimit, isColimit', ofIso, summand, ι, φ, instCategorySplit	30
Theorems comm, comm_assoc, ext, ext_iff, cofan_inj_naturality_symm, cofan_inj_naturality_symm_assoc, comp_F, comp_f, congr_F, congr_f, evalN_map, evalN_obj, ext, ext_iff, forget_map, forget_obj, hom_ext, hom_ext_iff, id_F, id_f, mk'_X, mk'_s, natTransCofanInj_app, epiComp_fst, epiComp_snd_coe, eqId_iff_eq, eqId_iff_len_eq, eqId_iff_len_le, eqId_iff_mono, ext, ext', fac_pull, fac_pull_assoc, id_fst, id_snd_coe, instEpiSimplexCategoryE, mk_fst, mk_snd_coe, cofan_inj_comp_app, cofan_inj_comp_app_assoc, cofan_inj_epi_naturality, cofan_inj_epi_naturality_assoc, cofan_inj_eq, cofan_inj_eq_assoc, cofan_inj_id, hom_ext, hom_ext', ofIso_N, ofIso_isColimit', ofIso_ι, ι_desc, ι_desc_assoc	52
Total	82

SimplicialObject

Definitions

Name	Category	Theorems
Split 📖	CompData	18 math math: Split.evalN_obj, Split.comp_f, Split.forget_obj, Split.forget_map, Split.comp_F, AlgebraicTopology.DoldKan.Γ₀'_obj, Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, Split.nondegComplexFunctor_map_f, AlgebraicTopology.DoldKan.Γ₀'_map_F, AlgebraicTopology.DoldKan.Γ₀_map_app, Split.nondegComplexFunctor_obj, Split.id_f, Split.natTransCofanInj_app, Split.evalN_map, CategoryTheory.Idempotents.DoldKan.Γ_map_app, Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, Split.id_F, AlgebraicTopology.DoldKan.Γ₀'_map_f
Splitting 📖	CompData	1 math math: Split.ext_iff
instCategorySplit 📖	CompOp	18 math math: Split.evalN_obj, Split.comp_f, Split.forget_obj, Split.forget_map, Split.comp_F, AlgebraicTopology.DoldKan.Γ₀'_obj, Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, Split.nondegComplexFunctor_map_f, AlgebraicTopology.DoldKan.Γ₀'_map_F, AlgebraicTopology.DoldKan.Γ₀_map_app, Split.nondegComplexFunctor_obj, Split.id_f, Split.natTransCofanInj_app, Split.evalN_map, CategoryTheory.Idempotents.DoldKan.Γ_map_app, Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, Split.id_F, AlgebraicTopology.DoldKan.Γ₀'_map_f

SimplicialObject.Split

Definitions

Name	Category	Theorems
X 📖	CompOp	17 math math: evalN_obj, comp_f, forget_obj, comp_F, ext_iff, toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, nondegComplexFunctor_map_f, cofan_inj_naturality_symm_assoc, Hom.comm, nondegComplexFunctor_obj, mk'_X, id_f, Hom.comm_assoc, natTransCofanInj_app, toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, id_F, cofan_inj_naturality_symm
evalN 📖	CompOp	3 math math: evalN_obj, natTransCofanInj_app, evalN_map
forget 📖	CompOp	7 math math: forget_obj, forget_map, toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, AlgebraicTopology.DoldKan.Γ₀_map_app, natTransCofanInj_app, CategoryTheory.Idempotents.DoldKan.Γ_map_app, toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f
mk' 📖	CompOp	5 math math: mk'_s, AlgebraicTopology.DoldKan.Γ₀'_obj, AlgebraicTopology.DoldKan.Γ₀'_map_F, mk'_X, AlgebraicTopology.DoldKan.Γ₀'_map_f
natTransCofanInj 📖	CompOp	1 math math: natTransCofanInj_app
s 📖	CompOp	14 math math: evalN_obj, mk'_s, comp_f, ext_iff, toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, nondegComplexFunctor_map_f, cofan_inj_naturality_symm_assoc, Hom.comm, nondegComplexFunctor_obj, id_f, Hom.comm_assoc, natTransCofanInj_app, toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, cofan_inj_naturality_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cofan_inj_naturality_symm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.summand SimplicialObject.Splitting.N X s 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.NatTrans.app Hom.F SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi Hom.f	—	SimplicialObject.Splitting.cofan_inj_eq CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality Hom.comm_assoc
cofan_inj_naturality_symm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.summand SimplicialObject.Splitting.N X s 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.NatTrans.app Hom.F SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi Hom.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cofan_inj_naturality_symm
comp_F 📖	mathematical	—	Hom.F CategoryTheory.CategoryStruct.comp SimplicialObject.Split CategoryTheory.Category.toCategoryStruct SimplicialObject.instCategorySplit CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject X	—	—
comp_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.comp SimplicialObject.Split CategoryTheory.Category.toCategoryStruct SimplicialObject.instCategorySplit SimplicialObject.Splitting.N X s	—	—
congr_F 📖	mathematical	—	Hom.f	—	—
congr_f 📖	mathematical	—	Hom.f	—	—
evalN_map 📖	mathematical	—	CategoryTheory.Functor.map SimplicialObject.Split SimplicialObject.instCategorySplit evalN Hom.f	—	—
evalN_obj 📖	mathematical	—	CategoryTheory.Functor.obj SimplicialObject.Split SimplicialObject.instCategorySplit evalN SimplicialObject.Splitting.N X s	—	—
ext 📖	—	X SimplicialObject.Splitting s	—	—	—
ext_iff 📖	mathematical	—	X SimplicialObject.Splitting s	—	ext
forget_map 📖	mathematical	—	CategoryTheory.Functor.map SimplicialObject.Split SimplicialObject.instCategorySplit CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject forget Hom.F	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj SimplicialObject.Split SimplicialObject.instCategorySplit CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject forget X	—	—
hom_ext 📖	—	Hom.f	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.f	—	hom_ext
id_F 📖	mathematical	—	Hom.F CategoryTheory.CategoryStruct.id SimplicialObject.Split CategoryTheory.Category.toCategoryStruct SimplicialObject.instCategorySplit CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject X	—	—
id_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.id SimplicialObject.Split CategoryTheory.Category.toCategoryStruct SimplicialObject.instCategorySplit SimplicialObject.Splitting.N X s	—	—
mk'_X 📖	mathematical	—	X mk'	—	—
mk'_s 📖	mathematical	—	s mk'	—	—
natTransCofanInj_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplicialObject.Split SimplicialObject.instCategorySplit evalN SimplexCategory.len Opposite.unop SimplexCategory Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory CategoryTheory.Epi CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject forget CategoryTheory.Functor.obj CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.evaluation natTransCofanInj SimplicialObject.Splitting.IndexSet SimplicialObject.Splitting.summand SimplicialObject.Splitting.N X s SimplicialObject.Splitting.cofan	—	—

SimplicialObject.Split.Hom

Definitions

Name	Category	Theorems
F 📖	CompOp	8 math math: SimplicialObject.Split.forget_map, SimplicialObject.Split.comp_F, AlgebraicTopology.DoldKan.Γ₀'_map_F, SimplicialObject.Split.cofan_inj_naturality_symm_assoc, comm, comm_assoc, SimplicialObject.Split.id_F, SimplicialObject.Split.cofan_inj_naturality_symm
f 📖	CompOp	13 math math: ext_iff, SimplicialObject.Split.comp_f, SimplicialObject.Split.nondegComplexFunctor_map_f, SimplicialObject.Split.congr_F, SimplicialObject.Split.cofan_inj_naturality_symm_assoc, comm, SimplicialObject.Split.congr_f, SimplicialObject.Split.id_f, comm_assoc, SimplicialObject.Split.evalN_map, SimplicialObject.Split.hom_ext_iff, SimplicialObject.Split.cofan_inj_naturality_symm, AlgebraicTopology.DoldKan.Γ₀'_map_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.N SimplicialObject.Split.X SimplicialObject.Split.s CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op SimplicialObject.Splitting.ι CategoryTheory.NatTrans.app F f	—	—
comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.N SimplicialObject.Split.X SimplicialObject.Split.s CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op SimplicialObject.Splitting.ι CategoryTheory.NatTrans.app F f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
ext 📖	—	f	—	—	SimplicialObject.Splitting.hom_ext
ext_iff 📖	mathematical	—	f	—	ext

SimplicialObject.Splitting

Definitions

Name	Category	Theorems
IndexSet 📖	CompOp	45 math math: cofan_inj_πSummand_eq_id_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id_assoc, cofan_inj_epi_naturality_assoc, ι_desc_assoc, cofan_inj_eq, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, cofan_inj_comp_PInfty_eq_zero, ιSummand_comp_d_comp_πSummand_eq_zero, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, ofIso_isColimit', πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, cofan_inj_πSummand_eq_id, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, SimplicialObject.Split.cofan_inj_naturality_symm_assoc, AlgebraicTopology.DoldKan.Γ₀_map_app, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, cofan_inj_πSummand_eq_zero, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, cofan_inj_comp_app, AlgebraicTopology.DoldKan.Γ₀.map_app, decomposition_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc, ι_desc, πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, SimplicialObject.Split.natTransCofanInj_app, cofan_inj_πSummand_eq_zero_assoc, CategoryTheory.Idempotents.DoldKan.Γ_map_app, cofan_inj_id, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, AlgebraicTopology.DoldKan.Γ₂_map_f_app, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id, toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', SimplicialObject.Split.cofan_inj_naturality_symm, cofan_inj_comp_app_assoc, cofan_inj_eq_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, cofan_inj_epi_naturality
N 📖	CompOp	57 math math: cofan_inj_πSummand_eq_id_assoc, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f, ofIso_N, AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id, SimplicialObject.Split.evalN_obj, PInfty_comp_πSummand_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id_assoc, cofan_inj_epi_naturality_assoc, SimplicialObject.Split.comp_f, ι_desc_assoc, cofan_inj_eq, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f, cofan_inj_comp_PInfty_eq_zero, ιSummand_comp_d_comp_πSummand_eq_zero, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, nondegComplex_X, ofIso_isColimit', πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, cofan_inj_πSummand_eq_id, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, SimplicialObject.Split.cofan_inj_naturality_symm_assoc, ofIso_ι, AlgebraicTopology.DoldKan.Γ₀_map_app, SimplicialObject.Split.Hom.comm, cofan_inj_πSummand_eq_zero, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, cofan_inj_comp_app, AlgebraicTopology.DoldKan.Γ₀.map_app, σ_comp_πSummand_id_eq_zero_assoc, PInfty_comp_πSummand_id_assoc, decomposition_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, SimplicialObject.Split.id_f, SimplicialObject.Split.Hom.comm_assoc, ι_desc, πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, SimplicialObject.Split.natTransCofanInj_app, cofan_inj_πSummand_eq_zero_assoc, comp_PInfty_eq_zero_iff, CategoryTheory.Idempotents.DoldKan.Γ_map_app, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, cofan_inj_id, σ_comp_πSummand_id_eq_zero, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, AlgebraicTopology.DoldKan.Γ₂_map_f_app, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id, toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', SimplicialObject.Split.cofan_inj_naturality_symm, cofan_inj_comp_app_assoc, cofan_inj_eq_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, cofan_inj_epi_naturality
cofan 📖	CompOp	41 math math: cofan_inj_πSummand_eq_id_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id_assoc, cofan_inj_epi_naturality_assoc, ι_desc_assoc, cofan_inj_eq, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, cofan_inj_comp_PInfty_eq_zero, ιSummand_comp_d_comp_πSummand_eq_zero, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, ofIso_isColimit', πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, cofan_inj_πSummand_eq_id, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, SimplicialObject.Split.cofan_inj_naturality_symm_assoc, AlgebraicTopology.DoldKan.Γ₀_map_app, cofan_inj_πSummand_eq_zero, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, cofan_inj_comp_app, AlgebraicTopology.DoldKan.Γ₀.map_app, decomposition_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, ι_desc, πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, SimplicialObject.Split.natTransCofanInj_app, cofan_inj_πSummand_eq_zero_assoc, CategoryTheory.Idempotents.DoldKan.Γ_map_app, cofan_inj_id, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, AlgebraicTopology.DoldKan.Γ₂_map_f_app, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id, toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', SimplicialObject.Split.cofan_inj_naturality_symm, cofan_inj_comp_app_assoc, cofan_inj_eq_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, cofan_inj_epi_naturality
cofan' 📖	CompOp	1 math math: ofIso_isColimit'
desc 📖	CompOp	8 math math: ι_desc_assoc, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, AlgebraicTopology.DoldKan.Γ₀_map_app, AlgebraicTopology.DoldKan.Γ₀.map_app, ι_desc, CategoryTheory.Idempotents.DoldKan.Γ_map_app, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, AlgebraicTopology.DoldKan.Γ₂_map_f_app
isColimit 📖	CompOp	1 math math: ofIso_isColimit'
isColimit' 📖	CompOp	1 math math: ofIso_isColimit'
ofIso 📖	CompOp	3 math math: ofIso_N, ofIso_isColimit', ofIso_ι
summand 📖	CompOp	41 math math: cofan_inj_πSummand_eq_id_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id_assoc, cofan_inj_epi_naturality_assoc, ι_desc_assoc, cofan_inj_eq, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, cofan_inj_comp_PInfty_eq_zero, ιSummand_comp_d_comp_πSummand_eq_zero, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, ofIso_isColimit', πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, cofan_inj_πSummand_eq_id, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, SimplicialObject.Split.cofan_inj_naturality_symm_assoc, AlgebraicTopology.DoldKan.Γ₀_map_app, cofan_inj_πSummand_eq_zero, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, cofan_inj_comp_app, AlgebraicTopology.DoldKan.Γ₀.map_app, decomposition_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, ι_desc, πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, SimplicialObject.Split.natTransCofanInj_app, cofan_inj_πSummand_eq_zero_assoc, CategoryTheory.Idempotents.DoldKan.Γ_map_app, cofan_inj_id, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, AlgebraicTopology.DoldKan.Γ₂_map_f_app, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id, toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', SimplicialObject.Split.cofan_inj_naturality_symm, cofan_inj_comp_app_assoc, cofan_inj_eq_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, cofan_inj_epi_naturality
ι 📖	CompOp	7 math math: cofan_inj_eq, ofIso_isColimit', ofIso_ι, SimplicialObject.Split.Hom.comm, SimplicialObject.Split.Hom.comm_assoc, cofan_inj_id, cofan_inj_eq_assoc
φ 📖	CompOp	2 math math: cofan_inj_comp_app, cofan_inj_comp_app_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cofan_inj_comp_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.NatTrans.app SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi Opposite.op φ CategoryTheory.Functor.map Quiver.Hom.op IndexSet.e	—	cofan_inj_eq_assoc CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality
cofan_inj_comp_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.NatTrans.app Opposite.op SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi φ CategoryTheory.Functor.map Quiver.Hom.op IndexSet.e	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cofan_inj_comp_app
cofan_inj_epi_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.map IndexSet.epiComp	—	CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp
cofan_inj_epi_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.map IndexSet.epiComp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cofan_inj_epi_naturality
cofan_inj_eq 📖	mathematical	—	IndexSet summand N cofan CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplexCategory.len Opposite.unop SimplexCategory Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SimplexCategory.smallCategory CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.Category.opposite Opposite.op ι CategoryTheory.Functor.map Quiver.Hom.op IndexSet.e	—	—
cofan_inj_eq_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi ι CategoryTheory.Functor.map Quiver.Hom.op IndexSet.e	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cofan_inj_eq
cofan_inj_id 📖	mathematical	—	IndexSet Opposite.op SimplexCategory summand N cofan IndexSet.id ι	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
hom_ext 📖	—	φ	—	—	CategoryTheory.SimplicialObject.hom_ext hom_ext' cofan_inj_comp_app
hom_ext' 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan	—	—	CategoryTheory.Limits.Cofan.IsColimit.hom_ext
ofIso_N 📖	mathematical	—	N ofIso	—	—
ofIso_isColimit' 📖	mathematical	—	isColimit' ofIso CategoryTheory.Limits.IsColimit.ofIsoColimit CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor summand N cofan cofan' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op ι CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject isColimit CategoryTheory.Limits.Cofan.ext CategoryTheory.Iso.app	—	—
ofIso_ι 📖	mathematical	—	ι ofIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct N CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject	—	—
ι_desc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan desc	—	CategoryTheory.Limits.Cofan.IsColimit.fac
ι_desc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_desc

SimplicialObject.Splitting.IndexSet

Definitions

Name	Category	Theorems
EqId 📖	MathDef	4 math math: eqId_iff_len_eq, eqId_iff_mono, eqId_iff_eq, eqId_iff_len_le
e 📖	CompOp	15 math math: fac_pull_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', SimplicialObject.Splitting.cofan_inj_eq, ext', eqId_iff_mono, fac_pull, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, instEpiSimplexCategoryE, SimplicialObject.Splitting.cofan_inj_comp_app, epiComp_snd_coe, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', SimplicialObject.Splitting.cofan_inj_comp_app_assoc, SimplicialObject.Splitting.cofan_inj_eq_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc
epiComp 📖	CompOp	4 math math: epiComp_fst, SimplicialObject.Splitting.cofan_inj_epi_naturality_assoc, epiComp_snd_coe, SimplicialObject.Splitting.cofan_inj_epi_naturality
id 📖	CompOp	23 math math: id_fst, AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id, SimplicialObject.Splitting.PInfty_comp_πSummand_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id_assoc, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, id_snd_coe, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero_assoc, SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, SimplicialObject.Splitting.cofan_inj_id, SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f
instFintype 📖	CompOp	5 math math: AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, SimplicialObject.Splitting.decomposition_id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc
instInhabited 📖	CompOp	—
mk 📖	CompOp	—
pull 📖	CompOp	6 math math: fac_pull_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', fac_pull, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epiComp_fst 📖	mathematical	—	Opposite SimplexCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop CategoryTheory.Epi epiComp	—	—
epiComp_snd_coe 📖	mathematical	—	Quiver.Hom SimplexCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop Opposite CategoryTheory.Epi epiComp CategoryTheory.CategoryStruct.comp Quiver.Hom.unop e	—	—
eqId_iff_eq 📖	mathematical	—	EqId Opposite SimplexCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop CategoryTheory.Epi	—	ext CategoryTheory.Category.comp_id SimplexCategory.eq_id_of_epi
eqId_iff_len_eq 📖	mathematical	—	EqId SimplexCategory.len Opposite.unop SimplexCategory Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory CategoryTheory.Epi	—	eqId_iff_eq Opposite.unop_inj_iff SimplexCategory.ext
eqId_iff_len_le 📖	mathematical	—	EqId SimplexCategory.len Opposite.unop SimplexCategory Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory CategoryTheory.Epi	—	eqId_iff_len_eq le_refl le_antisymm SimplexCategory.len_le_of_epi instEpiSimplexCategoryE
eqId_iff_mono 📖	mathematical	—	EqId CategoryTheory.Mono SimplexCategory SimplexCategory.smallCategory Opposite.unop Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Epi e	—	CategoryTheory.instMonoId eqId_iff_len_le SimplexCategory.len_le_of_mono
ext 📖	—	Opposite SimplexCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop CategoryTheory.Epi CategoryTheory.CategoryStruct.comp e CategoryTheory.eqToHom	—	—	CategoryTheory.Category.comp_id
ext' 📖	mathematical	—	Opposite SimplexCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop CategoryTheory.Epi e	—	—
fac_pull 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategory CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi pull e CategoryTheory.Limits.image.ι Quiver.Hom.unop CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations	—	CategoryTheory.Limits.image.fac
fac_pull_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SimplexCategory CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi pull e CategoryTheory.Limits.image.ι Quiver.Hom.unop CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations SimplexCategory.instHasStrongEpiMonoFactorisations CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac_pull
id_fst 📖	mathematical	—	Opposite SimplexCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop CategoryTheory.Epi id	—	—
id_snd_coe 📖	mathematical	—	Quiver.Hom SimplexCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop CategoryTheory.Epi Opposite id CategoryTheory.CategoryStruct.id	—	—
instEpiSimplexCategoryE 📖	mathematical	—	CategoryTheory.Epi SimplexCategory SimplexCategory.smallCategory Opposite.unop Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct e	—	—
mk_fst 📖	mathematical	—	Opposite SimplexCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop Opposite.op CategoryTheory.Epi	—	—
mk_snd_coe 📖	mathematical	—	Quiver.Hom SimplexCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.smallCategory Opposite.unop Opposite.op CategoryTheory.Epi Opposite	—	—

---

← Back to Index