# 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 #

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

Equations
• = ((Δ' : ) × { α : // })
Instances For

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

Equations
• = ⟨, f,
Instances For

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

Equations
• A.e = A.snd
Instances For
Equations
• =
theorem SimplicialObject.Splitting.IndexSet.ext' {Δ : } :
A = A.fst, A.e,
theorem SimplicialObject.Splitting.IndexSet.ext {Δ : } (h₁ : A₁.fst = A₂.fst) (h₂ : ) :
A₁ = A₂
Equations
• One or more equations did not get rendered due to their size.
@[simp]

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

Equations
Instances For
Equations

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

Equations
• A.EqId =
Instances For
@[simp]
theorem SimplicialObject.Splitting.IndexSet.epiComp_fst {Δ₁ : } {Δ₂ : } (p : Δ₁ Δ₂) [CategoryTheory.Epi p.unop] :
(A.epiComp p).fst = A.fst
@[simp]
theorem SimplicialObject.Splitting.IndexSet.epiComp_snd_coe {Δ₁ : } {Δ₂ : } (p : Δ₁ Δ₂) [CategoryTheory.Epi p.unop] :
(A.epiComp p).snd = CategoryTheory.CategoryStruct.comp p.unop A.e
def SimplicialObject.Splitting.IndexSet.epiComp {Δ₁ : } {Δ₂ : } (p : Δ₁ Δ₂) [CategoryTheory.Epi p.unop] :

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
Instances For
def SimplicialObject.Splitting.IndexSet.pull {Δ : } {Δ' : } (θ : Δ Δ') :

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
• A.pull θ =
Instances For
def SimplicialObject.Splitting.summand {C : Type u_1} (N : C) (Δ : ) :
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
Instances For
def SimplicialObject.Splitting.cofan' {C : Type u_1} [] (N : C) (φ : (n : ) → N n X.obj ) (Δ : ) :

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.
Instances For
structure SimplicialObject.Splitting {C : Type u_1} [] :
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.obj

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

• isColimit' : (Δ : ) → 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 Δ.

Instances For
def SimplicialObject.Splitting.cofan {C : Type u_1} [] (s : ) (Δ : ) :

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

Equations
Instances For
def SimplicialObject.Splitting.isColimit {C : Type u_1} [] (s : ) (Δ : ) :

The cofan s.cofan Δ is colimit.

Equations
• s.isColimit Δ = s.isColimit' Δ
Instances For
theorem SimplicialObject.Splitting.cofan_inj_eq_assoc {C : Type u_1} [] (s : ) {Δ : } {Z : C} (h : (s.cofan Δ).pt Z) :
theorem SimplicialObject.Splitting.cofan_inj_eq {C : Type u_1} [] (s : ) {Δ : } :
(s.cofan Δ).inj A = CategoryTheory.CategoryStruct.comp (s (Opposite.unop A.fst).len) (X.map A.e.op)
theorem SimplicialObject.Splitting.cofan_inj_id {C : Type u_1} [] (s : ) (n : ) :
(s.cofan ).inj = s n
def SimplicialObject.Splitting.φ {C : Type u_1} [] (s : ) (f : X Y) (n : ) :
s.N n Y.obj

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
Instances For
@[simp]
theorem SimplicialObject.Splitting.cofan_inj_comp_app_assoc {C : Type u_1} [] (s : ) (f : X Y) {Δ : } {Z : C} (h : Y.obj Δ Z) :
@[simp]
theorem SimplicialObject.Splitting.cofan_inj_comp_app {C : Type u_1} [] (s : ) (f : X Y) {Δ : } :
CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (f.app Δ) = CategoryTheory.CategoryStruct.comp (s f (Opposite.unop A.fst).len) (Y.map A.e.op)
theorem SimplicialObject.Splitting.hom_ext' {C : Type u_1} [] (s : ) {Z : C} {Δ : } (f : X.obj Δ Z) (g : X.obj Δ Z) (h : ∀ (A : ), CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) f = CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) g) :
f = g
theorem SimplicialObject.Splitting.hom_ext {C : Type u_1} [] (s : ) (f : X Y) (g : X Y) (h : ∀ (n : ), s f n = s g n) :
f = g
def SimplicialObject.Splitting.desc {C : Type u_1} [] (s : ) {Z : C} (Δ : ) (F : (A : ) → s.N (Opposite.unop A.fst).len Z) :
X.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
Instances For
@[simp]
theorem SimplicialObject.Splitting.ι_desc_assoc {C : Type u_1} [] (s : ) {Z : C} (Δ : ) (F : (A : ) → s.N (Opposite.unop A.fst).len Z✝) {Z : C} (h : Z✝ Z) :
@[simp]
theorem SimplicialObject.Splitting.ι_desc {C : Type u_1} [] (s : ) {Z : C} (Δ : ) (F : (A : ) → s.N (Opposite.unop A.fst).len Z) :
CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (s.desc Δ F) = F A
@[simp]
theorem SimplicialObject.Splitting.ofIso_N {C : Type u_1} [] (s : ) (e : X Y) :
∀ (a : ), (s.ofIso e).N a = s.N a
@[simp]
theorem SimplicialObject.Splitting.ofIso_ι {C : Type u_1} [] (s : ) (e : X Y) (n : ) :
(s.ofIso e) n = CategoryTheory.CategoryStruct.comp (s n) (e.hom.app )
@[simp]
theorem SimplicialObject.Splitting.ofIso_isColimit' {C : Type u_1} [] (s : ) (e : X Y) (Δ : ) :
(s.ofIso e).isColimit' Δ = (s.isColimit Δ).ofIsoColimit (CategoryTheory.Limits.Cofan.ext (e.app Δ) )
def SimplicialObject.Splitting.ofIso {C : Type u_1} [] (s : ) (e : X 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.
Instances For
theorem SimplicialObject.Splitting.cofan_inj_epi_naturality_assoc {C : Type u_1} [] (s : ) {Δ₁ : } {Δ₂ : } (p : Δ₁ Δ₂) [CategoryTheory.Epi p.unop] {Z : C} (h : X.obj Δ₂ Z) :
CategoryTheory.CategoryStruct.comp ((s.cofan Δ₁).inj A) (CategoryTheory.CategoryStruct.comp (X.map p) h) = CategoryTheory.CategoryStruct.comp ((s.cofan Δ₂).inj (A.epiComp p)) h
theorem SimplicialObject.Splitting.cofan_inj_epi_naturality {C : Type u_1} [] (s : ) {Δ₁ : } {Δ₂ : } (p : Δ₁ Δ₂) [CategoryTheory.Epi p.unop] :
CategoryTheory.CategoryStruct.comp ((s.cofan Δ₁).inj A) (X.map p) = (s.cofan Δ₂).inj (A.epiComp p)
theorem SimplicialObject.Split.ext_iff {C : Type u_1} :
∀ {inst : } {x y : }, x = y x.X = y.X HEq x.s y.s
theorem SimplicialObject.Split.ext {C : Type u_1} :
∀ {inst : } {x y : }, x.X = y.XHEq x.s y.sx = y
structure SimplicialObject.Split (C : Type u_1) [] :
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.

• the underlying simplicial object

• s :

a splitting of the simplicial object

Instances For
@[simp]
theorem SimplicialObject.Split.mk'_X {C : Type u_1} [] (s : ) :
= X
@[simp]
theorem SimplicialObject.Split.mk'_s {C : Type u_1} [] (s : ) :
= s
def SimplicialObject.Split.mk' {C : Type u_1} [] (s : ) :

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

Equations
• = { X := X, s := s }
Instances For
structure SimplicialObject.Split.Hom {C : Type u_1} [] (S₁ : ) (S₂ : ) :
Type u_2

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

Instances For
@[simp]
theorem SimplicialObject.Split.Hom.comm {C : Type u_1} [] {S₁ : } {S₂ : } (self : S₁.Hom S₂) (n : ) :
CategoryTheory.CategoryStruct.comp (S₁.s n) (self.F.app ) = CategoryTheory.CategoryStruct.comp (self.f n) (S₂.s n)
theorem SimplicialObject.Split.Hom.ext_iff {C : Type u_1} [] {S₁ : } {S₂ : } {Φ₁ : S₁.Hom S₂} {Φ₂ : S₁.Hom S₂} :
Φ₁ = Φ₂ ∀ (n : ), Φ₁.f n = Φ₂.f n
theorem SimplicialObject.Split.Hom.ext {C : Type u_1} [] {S₁ : } {S₂ : } (Φ₁ : S₁.Hom S₂) (Φ₂ : S₁.Hom S₂) (h : ∀ (n : ), Φ₁.f n = Φ₂.f n) :
Φ₁ = Φ₂
theorem SimplicialObject.Split.Hom.comm_assoc {C : Type u_1} [] {S₁ : } {S₂ : } (self : S₁.Hom S₂) (n : ) {Z : C} (h : S₂.X.obj Z) :
Equations
theorem SimplicialObject.Split.hom_ext_iff {C : Type u_1} [] {S₁ : } {S₂ : } {Φ₁ : S₁ S₂} {Φ₂ : S₁ S₂} :
Φ₁ = Φ₂ ∀ (n : ), Φ₁.f n = Φ₂.f n
theorem SimplicialObject.Split.hom_ext {C : Type u_1} [] {S₁ : } {S₂ : } (Φ₁ : S₁ S₂) (Φ₂ : S₁ S₂) (h : ∀ (n : ), Φ₁.f n = Φ₂.f n) :
Φ₁ = Φ₂
theorem SimplicialObject.Split.congr_F {C : Type u_1} [] {S₁ : } {S₂ : } {Φ₁ : S₁ S₂} {Φ₂ : S₁ S₂} (h : Φ₁ = Φ₂) :
Φ₁.f = Φ₂.f
theorem SimplicialObject.Split.congr_f {C : Type u_1} [] {S₁ : } {S₂ : } {Φ₁ : S₁ S₂} {Φ₂ : S₁ S₂} (h : Φ₁ = Φ₂) (n : ) :
Φ₁.f n = Φ₂.f n
@[simp]
theorem SimplicialObject.Split.id_F {C : Type u_1} [] (S : ) :
@[simp]
theorem SimplicialObject.Split.id_f {C : Type u_1} [] (S : ) (n : ) :
@[simp]
theorem SimplicialObject.Split.comp_F {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (Φ₁₂ : S₁ S₂) (Φ₂₃ : S₂ S₃) :
.F = CategoryTheory.CategoryStruct.comp Φ₁₂.F Φ₂₃.F
@[simp]
theorem SimplicialObject.Split.comp_f {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (Φ₁₂ : S₁ S₂) (Φ₂₃ : S₂ S₃) (n : ) :
.f n = CategoryTheory.CategoryStruct.comp (Φ₁₂.f n) (Φ₂₃.f n)
@[simp]
theorem SimplicialObject.Split.cofan_inj_naturality_symm_assoc {C : Type u_1} [] {S₁ : } {S₂ : } (Φ : S₁ S₂) {Δ : } {Z : C} (h : S₂.X.obj Δ Z) :
@[simp]
theorem SimplicialObject.Split.cofan_inj_naturality_symm {C : Type u_1} [] {S₁ : } {S₂ : } (Φ : S₁ S₂) {Δ : } :
CategoryTheory.CategoryStruct.comp ((S₁.s.cofan Δ).inj A) (Φ.F.app Δ) = CategoryTheory.CategoryStruct.comp (Φ.f (Opposite.unop A.fst).len) ((S₂.s.cofan Δ).inj A)
@[simp]
theorem SimplicialObject.Split.forget_map (C : Type u_1) [] :
∀ {X Y : } (Φ : X Y), .map Φ = Φ.F
@[simp]
theorem SimplicialObject.Split.forget_obj (C : Type u_1) [] (S : ) :
.obj S = S.X

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

Equations
• = { obj := fun (S : ) => S.X, map := fun {X Y : } (Φ : X Y) => Φ.F, map_id := , map_comp := }
Instances For
@[simp]
theorem SimplicialObject.Split.evalN_map (C : Type u_1) [] (n : ) :
∀ {X Y : } (Φ : X Y), .map Φ = Φ.f n
@[simp]
theorem SimplicialObject.Split.evalN_obj (C : Type u_1) [] (n : ) (S : ) :
.obj S = S.s.N n
def SimplicialObject.Split.evalN (C : Type u_1) [] (n : ) :

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

Equations
• = { obj := fun (S : ) => S.s.N n, map := fun {X Y : } (Φ : X Y) => Φ.f n, map_id := , map_comp := }
Instances For
@[simp]
theorem SimplicialObject.Split.natTransCofanInj_app (C : Type u_1) [] {Δ : } (S : ) :
.app S = (S.s.cofan Δ).inj A

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
• = { app := fun (S : ) => (S.s.cofan Δ).inj A, naturality := }
Instances For