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ᵒᵖ) × { α : Opposite.unop Δ ⟶ Opposite.unop Δ' // CategoryTheory.Epi α })

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 = ⟨Opposite.op Δ', ⟨f, ⋯⟩⟩

@[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.e {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : Opposite.unop Δ ⟶ Opposite.unop A.fst

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

Equations

• A.e = ↑A.snd

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

Equations

• ⋯ = ⋯

theorem SimplicialObject.Splitting.IndexSet.ext' {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : A = ⟨A.fst, ⟨A.e, ⋯⟩⟩

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

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

Equations

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

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

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

Equations

• SimplicialObject.Splitting.IndexSet.id Δ = ⟨Δ, ⟨CategoryTheory.CategoryStruct.id (Opposite.unop Δ), ⋯⟩⟩

@[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 (Opposite.unop Δ)

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

Equations

• SimplicialObject.Splitting.IndexSet.instInhabited Δ = { 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

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

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

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

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

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

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

• A.epiComp p = ⟨A.fst, ⟨CategoryTheory.CategoryStruct.comp p.unop A.e, ⋯⟩⟩

@[simp]

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

@[simp]

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

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

• A.pull θ = SimplicialObject.Splitting.IndexSet.mk (CategoryTheory.Limits.factorThruImage (CategoryTheory.CategoryStruct.comp θ.unop A.e))

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

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

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 (Opposite.unop A.fst).len

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

• s.cofan Δ = CategoryTheory.Limits.Cofan.mk (X.obj Δ) fun (A : SimplicialObject.Splitting.IndexSet Δ) => CategoryTheory.CategoryStruct.comp (s.ι (Opposite.unop A.fst).len) (X.map A.e.op)

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 (s.cofan Δ)

The cofan s.cofan Δ is colimit.

Equations

• s.isColimit Δ = s.isColimit' Δ

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 Δ) : (s.cofan Δ).inj A = CategoryTheory.CategoryStruct.comp (s.ι (Opposite.unop A.fst).len) (X.map A.e.op)

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 : (s.cofan Δ).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) h = CategoryTheory.CategoryStruct.comp (s.ι (Opposite.unop A.fst).len) (CategoryTheory.CategoryStruct.comp (X.map A.e.op) h)

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 : ℕ) : (s.cofan (Opposite.op (SimplexCategory.mk n))).inj (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.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

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

@[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 ((s.cofan Δ).inj A) (f.app Δ) = CategoryTheory.CategoryStruct.comp (s.φ f (Opposite.unop A.fst).len) (Y.map A.e.op)

@[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.obj Δ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp (f.app Δ) h) = CategoryTheory.CategoryStruct.comp (s.φ f (Opposite.unop A.fst).len) (CategoryTheory.CategoryStruct.comp (Y.map A.e.op) h)

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.obj Δ ⟶ Z) (g : X.obj Δ ⟶ Z) (h : ∀ (A : SimplicialObject.Splitting.IndexSet Δ), 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} [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 : ℕ), s.φ f n = 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 (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

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

@[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 (Opposite.unop A.fst).len ⟶ Z) (A : SimplicialObject.Splitting.IndexSet Δ) : CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (s.desc Δ F) = F A

@[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 (Opposite.unop A.fst).len ⟶ Z✝) (A : SimplicialObject.Splitting.IndexSet Δ) {Z : C} (h : Z✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp (s.desc Δ F) h) = CategoryTheory.CategoryStruct.comp (F A) h

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.

@[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 : ℕ), (s.ofIso e).N a = s.N 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 : ℕ) : (s.ofIso e).ι n = CategoryTheory.CategoryStruct.comp (s.ι n) (e.hom.app (Opposite.op (SimplexCategory.mk n)))

@[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ᵒᵖ) : (s.ofIso e).isColimit' Δ = (s.isColimit Δ).ofIsoColimit (CategoryTheory.Limits.Cofan.ext (e.app Δ) ⋯)

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 ((s.cofan Δ₁).inj A) (X.map p) = (s.cofan Δ₂).inj (A.epiComp p)

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

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

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

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 }

@[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

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)

@[simp]

theorem SimplicialObject.Split.Hom.comm {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {S₁ : SimplicialObject.Split C} {S₂ : SimplicialObject.Split C} (self : S₁.Hom S₂) (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} (Φ₁ : S₁.Hom S₂) (Φ₂ : S₁.Hom 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 : S₁.Hom S₂) (n : ℕ) {Z : C} (h : S₂.X.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 {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 ((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.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.obj Δ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((S₁.s.cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp (Φ.F.app Δ) h) = CategoryTheory.CategoryStruct.comp (Φ.f (Opposite.unop A.fst).len) (CategoryTheory.CategoryStruct.comp ((S₂.s.cofan Δ).inj A) h)

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 = { obj := fun (S : SimplicialObject.Split C) => S.X, map := fun {X Y : SimplicialObject.Split C} (Φ : X ⟶ Y) => Φ.F, map_id := ⋯, map_comp := ⋯ }

@[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).map Φ = Φ.F

@[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).obj S = S.X

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

• SimplicialObject.Split.evalN C n = { obj := fun (S : SimplicialObject.Split C) => S.s.N n, map := fun {X Y : SimplicialObject.Split C} (Φ : X ⟶ Y) => Φ.f n, map_id := ⋯, map_comp := ⋯ }

@[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).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).obj S = S.s.N n

def SimplicialObject.Split.natTransCofanInj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) : SimplicialObject.Split.evalN C (Opposite.unop A.fst).len ⟶ (SimplicialObject.Split.forget C).comp ((CategoryTheory.evaluation SimplexCategoryᵒᵖ C).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 = { app := fun (S : SimplicialObject.Split C) => (S.s.cofan Δ).inj A, naturality := ⋯ }

@[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 = (S.s.cofan Δ).inj A