Theorems · Definition · algebraic topology
CategoryTheory.SimplicialObject.Split.s
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] → (self : CategoryTheory.SimplicialObject.Split C) → self.X.Splittinga splitting of the simplicial object
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.SimplicialObject.Splittingstatement · cited by 59
- CategoryTheory.SimplicialObject.Splitstatement and proof · cited by 37
- CategoryTheory.SimplicialObject.Split.Xstatement · cited by 30
Cited by36
Results whose statement or proof uses this declaration.
- CategoryTheory.SimplicialObject.Split.Hom.fstatement · cited by 15
- CategoryTheory.SimplicialObject.Split.nondegComplexFunctorproof · cited by 5
- CategoryTheory.SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁proof · cited by 3
- CategoryTheory.SimplicialObject.Split.evalNproof · cited by 3
- CategoryTheory.SimplicialObject.Split.Hom.extstatement and proof · cited by 2
- CategoryTheory.SimplicialObject.Split.Hom.mk.injstatement and proof · cited by 1
- CategoryTheory.SimplicialObject.Split.Hom.mk.injEqstatement and proof · cited by 1
- CategoryTheory.SimplicialObject.Split.Hom.mk.noConfusionstatement and proof · cited by 1
- CategoryTheory.SimplicialObject.Split.cofan_inj_naturality_symmstatement and proof · cited by 1
- CategoryTheory.SimplicialObject.Split.extstatement and proof · cited by 1
- CategoryTheory.SimplicialObject.Split.hom_extstatement · cited by 1
- CategoryTheory.SimplicialObject.Split.Hom.casesOnstatement and proof · cited by 1