Split simplicial objects

In this file, we introduce the notion of split simplicial object. If C is a category that has finite coproducts, a splitting s : Splitting X of a simplicial object X in C consists of the datum of a sequence of objects s.N : ℕ → C (which we shall refer to as "nondegenerate simplices") and a sequence of morphisms s.ι n : s.N n → X _[n] that have the property that a certain canonical map identifies X _[n] with the coproduct of objects s.N i indexed by all possible epimorphisms [n] ⟶ [i] in SimplexCategory. (We do not assume that the morphisms s.ι n are monomorphisms: in the most common categories, this would be a consequence of the axioms.)

Simplicial objects equipped with a splitting form a category SimplicialObject.Split C.

References

• [Stacks: Splitting simplicial objects] https://stacks.math.columbia.edu/tag/017O

def SimplicialObject.Splitting.IndexSet (Δ : SimplexCategoryᵒᵖ) : Type

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

Equations

• SimplicialObject.Splitting.IndexSet Δ = ((Δ' : SimplexCategoryᵒᵖ) × { α : Δ.unop ⟶ Δ'.unop // CategoryTheory.Epi α })

@[simp]

theorem SimplicialObject.Splitting.IndexSet.mk_snd_coe {Δ : SimplexCategory} {Δ' : SimplexCategory} (f : Δ ⟶ Δ') [CategoryTheory.Epi f] : ↑(SimplicialObject.Splitting.IndexSet.mk f).snd = f

@[simp]

theorem SimplicialObject.Splitting.IndexSet.mk_fst {Δ : SimplexCategory} {Δ' : SimplexCategory} (f : Δ ⟶ Δ') [CategoryTheory.Epi f] : (SimplicialObject.Splitting.IndexSet.mk f).fst = Opposite.op Δ'

def SimplicialObject.Splitting.IndexSet.mk {Δ : SimplexCategory} {Δ' : SimplexCategory} (f : Δ ⟶ Δ') [CategoryTheory.Epi f] : SimplicialObject.Splitting.IndexSet (Opposite.op Δ)

The element in Splitting.IndexSet Δ attached to an epimorphism f : Δ ⟶ Δ'.

Equations

• SimplicialObject.Splitting.IndexSet.mk f = { fst := Opposite.op Δ', snd := { val := f, property := (_ : CategoryTheory.Epi f) } }

def SimplicialObject.Splitting.IndexSet.e {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : Δ.unop ⟶ A.fst.unop

The epimorphism in SimplexCategory associated to A : Splitting.IndexSet Δ

Equations

• SimplicialObject.Splitting.IndexSet.e A = ↑A.snd

instance SimplicialObject.Splitting.IndexSet.instEpiSimplexCategorySmallCategoryUnopFstOppositeSubtypeHomToQuiverToCategoryStructE {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : CategoryTheory.Epi (SimplicialObject.Splitting.IndexSet.e A)

Equations

• (_ : CategoryTheory.Epi (SimplicialObject.Splitting.IndexSet.e A)) = (_ : CategoryTheory.Epi ↑A.snd)

theorem SimplicialObject.Splitting.IndexSet.ext' {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : A = { fst := A.fst, snd := { val := SimplicialObject.Splitting.IndexSet.e A, property := (_ : CategoryTheory.Epi ↑A.snd) } }

theorem SimplicialObject.Splitting.IndexSet.ext {Δ : SimplexCategoryᵒᵖ} (A₁ : SimplicialObject.Splitting.IndexSet Δ) (A₂ : SimplicialObject.Splitting.IndexSet Δ) (h₁ : A₁.fst = A₂.fst) (h₂ : CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.IndexSet.e A₁) (CategoryTheory.eqToHom (_ : A₁.fst.unop = A₂.fst.unop)) = SimplicialObject.Splitting.IndexSet.e A₂) : A₁ = A₂

instance SimplicialObject.Splitting.IndexSet.instFintypeIndexSet {Δ : SimplexCategoryᵒᵖ} : Fintype (SimplicialObject.Splitting.IndexSet Δ)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SimplicialObject.Splitting.IndexSet.id_fst (Δ : SimplexCategoryᵒᵖ) : (SimplicialObject.Splitting.IndexSet.id Δ).fst = Δ

@[simp]

theorem SimplicialObject.Splitting.IndexSet.id_snd_coe (Δ : SimplexCategoryᵒᵖ) : ↑(SimplicialObject.Splitting.IndexSet.id Δ).snd = CategoryTheory.CategoryStruct.id Δ.unop

def SimplicialObject.Splitting.IndexSet.id (Δ : SimplexCategoryᵒᵖ) : SimplicialObject.Splitting.IndexSet Δ

The distinguished element in Splitting.IndexSet Δ which corresponds to the identity of Δ.

Equations

• One or more equations did not get rendered due to their size.

instance SimplicialObject.Splitting.IndexSet.instInhabitedIndexSet (Δ : SimplexCategoryᵒᵖ) : Inhabited (SimplicialObject.Splitting.IndexSet Δ)

Equations

• SimplicialObject.Splitting.IndexSet.instInhabitedIndexSet Δ = { default := SimplicialObject.Splitting.IndexSet.id Δ }

def SimplicialObject.Splitting.IndexSet.EqId {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : Prop

The condition that an element Splitting.IndexSet Δ is the distinguished element Splitting.IndexSet.Id Δ.

Equations

• SimplicialObject.Splitting.IndexSet.EqId A = (A = SimplicialObject.Splitting.IndexSet.id Δ)

theorem SimplicialObject.Splitting.IndexSet.eqId_iff_eq {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : SimplicialObject.Splitting.IndexSet.EqId A ↔ A.fst = Δ

theorem SimplicialObject.Splitting.IndexSet.eqId_iff_len_eq {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : SimplicialObject.Splitting.IndexSet.EqId A ↔ SimplexCategory.len A.fst.unop = SimplexCategory.len Δ.unop

theorem SimplicialObject.Splitting.IndexSet.eqId_iff_len_le {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : SimplicialObject.Splitting.IndexSet.EqId A ↔ SimplexCategory.len Δ.unop ≤ SimplexCategory.len A.fst.unop

theorem SimplicialObject.Splitting.IndexSet.eqId_iff_mono {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : SimplicialObject.Splitting.IndexSet.EqId A ↔ CategoryTheory.Mono (SimplicialObject.Splitting.IndexSet.e A)

@[simp]

theorem SimplicialObject.Splitting.IndexSet.epiComp_snd_coe {Δ₁ : SimplexCategoryᵒᵖ} {Δ₂ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂) [CategoryTheory.Epi p.unop] : ↑(SimplicialObject.Splitting.IndexSet.epiComp A p).snd = CategoryTheory.CategoryStruct.comp p.unop (SimplicialObject.Splitting.IndexSet.e A)

@[simp]

theorem SimplicialObject.Splitting.IndexSet.epiComp_fst {Δ₁ : SimplexCategoryᵒᵖ} {Δ₂ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂) [CategoryTheory.Epi p.unop] : (SimplicialObject.Splitting.IndexSet.epiComp A p).fst = A.fst

def SimplicialObject.Splitting.IndexSet.epiComp {Δ₁ : SimplexCategoryᵒᵖ} {Δ₂ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂) [CategoryTheory.Epi p.unop] : SimplicialObject.Splitting.IndexSet Δ₂

Given A : IndexSet Δ₁, if p.unop : unop Δ₂ ⟶ unop Δ₁ is an epi, this is the obvious element in A : IndexSet Δ₂ associated to the composition of epimorphisms p.unop ≫ A.e.

Equations

• One or more equations did not get rendered due to their size.

def SimplicialObject.Splitting.IndexSet.pull {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) {Δ' : SimplexCategoryᵒᵖ} (θ : Δ ⟶ Δ') : SimplicialObject.Splitting.IndexSet Δ'

When A : IndexSet Δ and θ : Δ → Δ' is a morphism in SimplexCategoryᵒᵖ, an element in IndexSet Δ' can be defined by using the epi-mono factorisation of θ.unop ≫ A.e.

Equations

• One or more equations did not get rendered due to their size.

theorem SimplicialObject.Splitting.IndexSet.fac_pull_assoc {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) {Δ' : SimplexCategoryᵒᵖ} (θ : Δ ⟶ Δ') {Z : SimplexCategory} (h : A.fst.unop ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.IndexSet.e (SimplicialObject.Splitting.IndexSet.pull A θ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop (SimplicialObject.Splitting.IndexSet.e A))) h) = CategoryTheory.CategoryStruct.comp θ.unop (CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.IndexSet.e A) h)

theorem SimplicialObject.Splitting.IndexSet.fac_pull {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) {Δ' : SimplexCategoryᵒᵖ} (θ : Δ ⟶ Δ') : CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.IndexSet.e (SimplicialObject.Splitting.IndexSet.pull A θ)) (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop (SimplicialObject.Splitting.IndexSet.e A))) = CategoryTheory.CategoryStruct.comp θ.unop (SimplicialObject.Splitting.IndexSet.e A)

def SimplicialObject.Splitting.summand {C : Type u_1} (N : ℕ → C) (Δ : SimplexCategoryᵒᵖ) (A : SimplicialObject.Splitting.IndexSet Δ) : C

Given a sequences of objects N : ℕ → C in a category C, this is a family of objects indexed by the elements A : Splitting.IndexSet Δ. The Δ-simplices of a split simplicial objects shall identify to the coproduct of objects in such a family.

Equations

• SimplicialObject.Splitting.summand N Δ A = N (SimplexCategory.len A.fst.unop)

def SimplicialObject.Splitting.cofan' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (N : ℕ → C) (X : CategoryTheory.SimplicialObject C) (φ : (n : ℕ) → N n ⟶ X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n))) (Δ : SimplexCategoryᵒᵖ) : CategoryTheory.Limits.Cofan (SimplicialObject.Splitting.summand N Δ)

The cofan for summand N Δ induced by morphisms N n ⟶ X_ [n] for all n : ℕ.

Equations

• One or more equations did not get rendered due to their size.

structure SimplicialObject.Splitting {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.SimplicialObject C) : Type (max u_1 u_2)

A splitting of a simplicial object X consists of the datum of a sequence of objects N, a sequence of morphisms ι : N n ⟶ X _[n] such that for all Δ : SimplexCategoryᵒᵖ, the canonical map Splitting.map X ι Δ is an isomorphism.

• N : ℕ → C

  The "nondegenerate simplices" N n for all n : ℕ.

• ι : (n : ℕ) → self.N n ⟶ X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n))

  The "inclusion" N n ⟶ X _[n] for all n : ℕ.

• isColimit' : (Δ : SimplexCategoryᵒᵖ) → CategoryTheory.Limits.IsColimit (SimplicialObject.Splitting.cofan' self.N X self.ι Δ)

  For each Δ, X.obj Δ identifies to the coproduct of the objects N A.1.unop.len for all A : IndexSet Δ.

def SimplicialObject.Splitting.cofan {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) (Δ : SimplexCategoryᵒᵖ) : CategoryTheory.Limits.Cofan (SimplicialObject.Splitting.summand s.N Δ)

The cofan for summand s.N Δ induced by a splitting of a simplicial object.

Equations

• One or more equations did not get rendered due to their size.

def SimplicialObject.Splitting.isColimit {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) (Δ : SimplexCategoryᵒᵖ) : CategoryTheory.Limits.IsColimit (SimplicialObject.Splitting.cofan s Δ)

The cofan s.cofan Δ is colimit.

Equations

• SimplicialObject.Splitting.isColimit s Δ = s.isColimit' Δ

theorem SimplicialObject.Splitting.cofan_inj_eq_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) {Z : C} (h : (SimplicialObject.Splitting.cofan s Δ).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A) h = CategoryTheory.CategoryStruct.comp (s.ι (SimplexCategory.len A.fst.unop)) (CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map (SimplicialObject.Splitting.IndexSet.e A).op) h)

theorem SimplicialObject.Splitting.cofan_inj_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A = CategoryTheory.CategoryStruct.comp (s.ι (SimplexCategory.len A.fst.unop)) (X.toPrefunctor.map (SimplicialObject.Splitting.IndexSet.e A).op)

theorem SimplicialObject.Splitting.cofan_inj_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) (n : ℕ) : CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s (Opposite.op (SimplexCategory.mk n))) (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n))) = s.ι n

def SimplicialObject.Splitting.φ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) (f : X ⟶ Y) (n : ℕ) : s.N n ⟶ Y.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n))

As it is stated in Splitting.hom_ext, a morphism f : X ⟶ Y from a split simplicial object to any simplicial object is determined by its restrictions s.φ f n : s.N n ⟶ Y _[n] to the distinguished summands in each degree n.

Equations

• SimplicialObject.Splitting.φ s f n = CategoryTheory.CategoryStruct.comp (s.ι n) (f.app (Opposite.op (SimplexCategory.mk n)))

@[simp]

theorem SimplicialObject.Splitting.cofan_inj_comp_app_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) (f : X ⟶ Y) {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) {Z : C} (h : Y.toPrefunctor.obj Δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A) (CategoryTheory.CategoryStruct.comp (f.app Δ) h) = CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.φ s f (SimplexCategory.len A.fst.unop)) (CategoryTheory.CategoryStruct.comp (Y.toPrefunctor.map (SimplicialObject.Splitting.IndexSet.e A).op) h)

@[simp]

theorem SimplicialObject.Splitting.cofan_inj_comp_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) (f : X ⟶ Y) {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A) (f.app Δ) = CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.φ s f (SimplexCategory.len A.fst.unop)) (Y.toPrefunctor.map (SimplicialObject.Splitting.IndexSet.e A).op)

theorem SimplicialObject.Splitting.hom_ext' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) {Z : C} {Δ : SimplexCategoryᵒᵖ} (f : X.toPrefunctor.obj Δ ⟶ Z) (g : X.toPrefunctor.obj Δ ⟶ Z) (h : ∀ (A : SimplicialObject.Splitting.IndexSet Δ), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A) g) : f = g

theorem SimplicialObject.Splitting.hom_ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) (f : X ⟶ Y) (g : X ⟶ Y) (h : ∀ (n : ℕ), SimplicialObject.Splitting.φ s f n = SimplicialObject.Splitting.φ s g n) : f = g

def SimplicialObject.Splitting.desc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) {Z : C} (Δ : SimplexCategoryᵒᵖ) (F : (A : SimplicialObject.Splitting.IndexSet Δ) → s.N (SimplexCategory.len A.fst.unop) ⟶ Z) : X.toPrefunctor.obj Δ ⟶ Z

The map X.obj Δ ⟶ Z obtained by providing a family of morphisms on all the terms of decomposition given by a splitting s : Splitting X

Equations

• SimplicialObject.Splitting.desc s Δ F = CategoryTheory.Limits.Cofan.IsColimit.desc (SimplicialObject.Splitting.isColimit s Δ) F

@[simp]

theorem SimplicialObject.Splitting.ι_desc_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) {Z : C} (Δ : SimplexCategoryᵒᵖ) (F : (A : SimplicialObject.Splitting.IndexSet Δ) → s.N (SimplexCategory.len A.fst.unop) ⟶ Z✝) (A : SimplicialObject.Splitting.IndexSet Δ) {Z : C} (h : Z✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A) (CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.desc s Δ F) h) = CategoryTheory.CategoryStruct.comp (F A) h

@[simp]

theorem SimplicialObject.Splitting.ι_desc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) {Z : C} (Δ : SimplexCategoryᵒᵖ) (F : (A : SimplicialObject.Splitting.IndexSet Δ) → s.N (SimplexCategory.len A.fst.unop) ⟶ Z) (A : SimplicialObject.Splitting.IndexSet Δ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ) A) (SimplicialObject.Splitting.desc s Δ F) = F A

@[simp]

theorem SimplicialObject.Splitting.ofIso_ι {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) (e : X ≅ Y) (n : ℕ) : (SimplicialObject.Splitting.ofIso s e).ι n = CategoryTheory.CategoryStruct.comp (s.ι n) (e.hom.app (Opposite.op (SimplexCategory.mk n)))

@[simp]

theorem SimplicialObject.Splitting.ofIso_N {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) (e : X ≅ Y) : ∀ (a : ℕ), (SimplicialObject.Splitting.ofIso s e).N a = s.N a

@[simp]

theorem SimplicialObject.Splitting.ofIso_isColimit' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) (e : X ≅ Y) (Δ : SimplexCategoryᵒᵖ) : (SimplicialObject.Splitting.ofIso s e).isColimit' Δ = CategoryTheory.Limits.IsColimit.ofIsoColimit (SimplicialObject.Splitting.isColimit s Δ) (CategoryTheory.Limits.Cofan.ext (e.app Δ))

def SimplicialObject.Splitting.ofIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) (e : X ≅ Y) : SimplicialObject.Splitting Y

A simplicial object that is isomorphic to a split simplicial object is split.

Equations

• One or more equations did not get rendered due to their size.

theorem SimplicialObject.Splitting.cofan_inj_epi_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) {Δ₁ : SimplexCategoryᵒᵖ} {Δ₂ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂) [CategoryTheory.Epi p.unop] {Z : C} (h : X.toPrefunctor.obj Δ₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ₁) A) (CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map p) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ₂) (SimplicialObject.Splitting.IndexSet.epiComp A p)) h

theorem SimplicialObject.Splitting.cofan_inj_epi_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) {Δ₁ : SimplexCategoryᵒᵖ} {Δ₂ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂) [CategoryTheory.Epi p.unop] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ₁) A) (X.toPrefunctor.map p) = CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan s Δ₂) (SimplicialObject.Splitting.IndexSet.epiComp A p)

theorem SimplicialObject.Split.ext {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} (x y : SimplicialObject.Split C), x.X = y.X → HEq x.s y.s → x = y

theorem SimplicialObject.Split.ext_iff {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} (x y : SimplicialObject.Split C), x = y ↔ x.X = y.X ∧ HEq x.s y.s

structure SimplicialObject.Split (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : Type (max u_1 u_2)

The category SimplicialObject.Split C is the category of simplicial objects in C equipped with a splitting, and morphisms are morphisms of simplicial objects which are compatible with the splittings.

• X : CategoryTheory.SimplicialObject C

  the underlying simplicial object

• s : SimplicialObject.Splitting self.X

  a splitting of the simplicial object

@[simp]

theorem SimplicialObject.Split.mk'_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) : (SimplicialObject.Split.mk' s).X = X

@[simp]

theorem SimplicialObject.Split.mk'_s {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) : (SimplicialObject.Split.mk' s).s = s

def SimplicialObject.Split.mk' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) : SimplicialObject.Split C

The object in SimplicialObject.Split C attached to a splitting s : Splitting X of a simplicial object X.

Equations

• SimplicialObject.Split.mk' s = { X := X, s := s }

structure SimplicialObject.Split.Hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (S₁ : SimplicialObject.Split C) (S₂ : SimplicialObject.Split C) : Type u_2

Morphisms in SimplicialObject.Split C are morphisms of simplicial objects that are compatible with the splittings.

• F : S₁.X ⟶ S₂.X

  the morphism between the underlying simplicial objects

• f : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n

  the morphism between the "nondegenerate" n-simplices for all n : ℕ

• comm : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (self.F.app (Opposite.op (SimplexCategory.mk n))) = CategoryTheory.CategoryStruct.comp (self.f n) (S₂.s.ι n)

theorem SimplicialObject.Split.Hom.ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {S₁ : SimplicialObject.Split C} {S₂ : SimplicialObject.Split C} (Φ₁ : SimplicialObject.Split.Hom S₁ S₂) (Φ₂ : SimplicialObject.Split.Hom S₁ S₂) (h : ∀ (n : ℕ), Φ₁.f n = Φ₂.f n) : Φ₁ = Φ₂

theorem SimplicialObject.Split.Hom.comm_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {S₁ : SimplicialObject.Split C} {S₂ : SimplicialObject.Split C} (self : SimplicialObject.Split.Hom S₁ S₂) (n : ℕ) {Z : C} (h : S₂.X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (CategoryTheory.CategoryStruct.comp (self.F.app (Opposite.op (SimplexCategory.mk n))) h) = CategoryTheory.CategoryStruct.comp (self.f n) (CategoryTheory.CategoryStruct.comp (S₂.s.ι n) h)

instance SimplicialObject.instCategorySplit (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.Category.{u_2, max u_2 u_1} (SimplicialObject.Split C)

Equations

• SimplicialObject.instCategorySplit C = CategoryTheory.Category.mk

theorem SimplicialObject.Split.hom_ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {S₁ : SimplicialObject.Split C} {S₂ : SimplicialObject.Split C} (Φ₁ : S₁ ⟶ S₂) (Φ₂ : S₁ ⟶ S₂) (h : ∀ (n : ℕ), Φ₁.f n = Φ₂.f n) : Φ₁ = Φ₂

theorem SimplicialObject.Split.congr_F {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {S₁ : SimplicialObject.Split C} {S₂ : SimplicialObject.Split C} {Φ₁ : S₁ ⟶ S₂} {Φ₂ : S₁ ⟶ S₂} (h : Φ₁ = Φ₂) : Φ₁.f = Φ₂.f

theorem SimplicialObject.Split.congr_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {S₁ : SimplicialObject.Split C} {S₂ : SimplicialObject.Split C} {Φ₁ : S₁ ⟶ S₂} {Φ₂ : S₁ ⟶ S₂} (h : Φ₁ = Φ₂) (n : ℕ) : Φ₁.f n = Φ₂.f n

@[simp]

theorem SimplicialObject.Split.id_F {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (S : SimplicialObject.Split C) : (CategoryTheory.CategoryStruct.id S).F = CategoryTheory.CategoryStruct.id S.X

@[simp]

theorem SimplicialObject.Split.id_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (S : SimplicialObject.Split C) (n : ℕ) : (CategoryTheory.CategoryStruct.id S).f n = CategoryTheory.CategoryStruct.id (S.s.N n)

@[simp]

theorem SimplicialObject.Split.comp_F {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {S₁ : SimplicialObject.Split C} {S₂ : SimplicialObject.Split C} {S₃ : SimplicialObject.Split C} (Φ₁₂ : S₁ ⟶ S₂) (Φ₂₃ : S₂ ⟶ S₃) : (CategoryTheory.CategoryStruct.comp Φ₁₂ Φ₂₃).F = CategoryTheory.CategoryStruct.comp Φ₁₂.F Φ₂₃.F

@[simp]

theorem SimplicialObject.Split.comp_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {S₁ : SimplicialObject.Split C} {S₂ : SimplicialObject.Split C} {S₃ : SimplicialObject.Split C} (Φ₁₂ : S₁ ⟶ S₂) (Φ₂₃ : S₂ ⟶ S₃) (n : ℕ) : (CategoryTheory.CategoryStruct.comp Φ₁₂ Φ₂₃).f n = CategoryTheory.CategoryStruct.comp (Φ₁₂.f n) (Φ₂₃.f n)

@[simp]

theorem SimplicialObject.Split.cofan_inj_naturality_symm_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {S₁ : SimplicialObject.Split C} {S₂ : SimplicialObject.Split C} (Φ : S₁ ⟶ S₂) {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) {Z : C} (h : S₂.X.toPrefunctor.obj Δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan S₁.s Δ) A) (CategoryTheory.CategoryStruct.comp (Φ.F.app Δ) h) = CategoryTheory.CategoryStruct.comp (Φ.f (SimplexCategory.len A.fst.unop)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan S₂.s Δ) A) h)

@[simp]

theorem SimplicialObject.Split.cofan_inj_naturality_symm {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {S₁ : SimplicialObject.Split C} {S₂ : SimplicialObject.Split C} (Φ : S₁ ⟶ S₂) {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan S₁.s Δ) A) (Φ.F.app Δ) = CategoryTheory.CategoryStruct.comp (Φ.f (SimplexCategory.len A.fst.unop)) (CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan S₂.s Δ) A)

@[simp]

theorem SimplicialObject.Split.forget_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (S : SimplicialObject.Split C) : (SimplicialObject.Split.forget C).toPrefunctor.obj S = S.X

@[simp]

theorem SimplicialObject.Split.forget_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : ∀ {X Y : SimplicialObject.Split C} (Φ : X ⟶ Y), (SimplicialObject.Split.forget C).toPrefunctor.map Φ = Φ.F

def SimplicialObject.Split.forget (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.Functor (SimplicialObject.Split C) (CategoryTheory.SimplicialObject C)

The functor SimplicialObject.Split C ⥤ SimplicialObject C which forgets the splitting.

Equations

• SimplicialObject.Split.forget C = CategoryTheory.Functor.mk { obj := fun (S : SimplicialObject.Split C) => S.X, map := fun {X Y : SimplicialObject.Split C} (Φ : X ⟶ Y) => Φ.F }

@[simp]

theorem SimplicialObject.Split.evalN_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (n : ℕ) : ∀ {X Y : SimplicialObject.Split C} (Φ : X ⟶ Y), (SimplicialObject.Split.evalN C n).toPrefunctor.map Φ = Φ.f n

@[simp]

theorem SimplicialObject.Split.evalN_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (n : ℕ) (S : SimplicialObject.Split C) : (SimplicialObject.Split.evalN C n).toPrefunctor.obj S = S.s.N n

def SimplicialObject.Split.evalN (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (n : ℕ) : CategoryTheory.Functor (SimplicialObject.Split C) C

The functor SimplicialObject.Split C ⥤ C which sends a simplicial object equipped with a splitting to its nondegenerate n-simplices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SimplicialObject.Split.natTransCofanInj_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) (S : SimplicialObject.Split C) : (SimplicialObject.Split.natTransCofanInj C A).app S = CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan S.s Δ) A

def SimplicialObject.Split.natTransCofanInj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : SimplicialObject.Split.evalN C (SimplexCategory.len A.fst.unop) ⟶ CategoryTheory.Functor.comp (SimplicialObject.Split.forget C) ((CategoryTheory.evaluation SimplexCategoryᵒᵖ C).toPrefunctor.obj Δ)

The inclusion of each summand in the coproduct decomposition of simplices in split simplicial objects is a natural transformation of functors SimplicialObject.Split C ⥤ C

Equations

• SimplicialObject.Split.natTransCofanInj C A = CategoryTheory.NatTrans.mk fun (S : SimplicialObject.Split C) => CategoryTheory.Limits.Cofan.inj (SimplicialObject.Splitting.cofan S.s Δ) A