Mathlib Map

Theorems · Definition · algebraic topology

CategoryTheory.SimplicialObject.Splitting.IndexSet

SimplexCategoryᵒᵖ → Type

The index set which appears in the definition of split simplicial objects.

Defined in
Mathlib.AlgebraicTopology.SimplicialObject.Split
Cited by
65 results in Mathlib
Foundations
Depth 30 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.SimplicialObject.Splitting.summand · cited by 48Splitting.summandCategoryTheory.SimplicialObject.Splitting.cofan · cited by 46Splitting.cofanCategoryTheory.SimplicialObject.Splitting.IndexSet.e · cited by 28IndexSet.eCategoryTheory.SimplicialObject.Splitting.IndexSet.id · cited by 28IndexSet.idAlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ · cited by 21Obj.obj₂CategoryTheory.SimplicialObject.Splitting.πSummand · cited by 17Splitting.πSummandCategoryTheory.SimplicialObject.Splitting.desc · cited by 12Splitting.descAlgebraicTopology.DoldKan.Γ₀.Obj.map · cited by 9Obj.mapCategoryTheory.SimplicialObject.Splitting.IndexSet.mk · cited by 8IndexSet.mkCategoryTheory.SimplicialObject.Splitting.IndexSet.EqId · cited by 7IndexSet.EqIdCategoryTheory.SimplicialObject.Splitting.IndexSet.pull · cited by 7IndexSet.pullCategoryTheory.SimplicialObject.Splitting.IndexSet.epiComp · cited by 5IndexSet.epiCompCategoryTheory.SimplicialObject.Splitting.hom_ext' · cited by 5Splitting.hom_ext'CategoryTheory.SimplicialObject.Splitting.map · cited by 5Splitting.mapCategoryTheory.SimplicialObject.Splitting.ι_desc · cited by 5Splitting.ι_descQuiver.Hom · cited by 32603Quiver.HomOpposite · cited by 8081OppositeOpposite.unop · cited by 2231Opposite.unopSimplexCategory · cited by 2204SimplexCategoryCategoryTheory.Epi · cited by 688CategoryTheory.EpiSplitting.IndexSetCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by89

Results whose statement or proof uses this declaration.