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 CategoryTheory.SimplicialObject.Splitting.IndexSet (Δ : SimplexCategoryᵒᵖ) : Type

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

Equations

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

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

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

Equations

• CategoryTheory.SimplicialObject.Splitting.IndexSet.mk f = ⟨Opposite.op Δ', ⟨f, ⋯⟩⟩

@[simp]

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

@[simp]

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

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

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

Equations

• A.e = ↑A.snd

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

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

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

@[implicit_reducible]

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

Equations

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

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

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

Equations

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

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

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

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

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

def CategoryTheory.SimplicialObject.Splitting.IndexSet.epiComp {Δ₁ Δ₂ : SimplexCategoryᵒᵖ} (A : IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂) [Epi p.unop] : 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 CategoryTheory.SimplicialObject.Splitting.IndexSet.epiComp_snd_coe {Δ₁ Δ₂ : SimplexCategoryᵒᵖ} (A : IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂) [Epi p.unop] : ↑(A.epiComp p).snd = CategoryStruct.comp p.unop A.e

@[simp]

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

noncomputable def CategoryTheory.SimplicialObject.Splitting.IndexSet.pull {Δ : SimplexCategoryᵒᵖ} (A : IndexSet Δ) {Δ' : SimplexCategoryᵒᵖ} (θ : Δ ⟶ Δ') : 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 θ = CategoryTheory.SimplicialObject.Splitting.IndexSet.mk (CategoryTheory.Limits.factorThruImage (CategoryTheory.CategoryStruct.comp θ.unop A.e))

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

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

def CategoryTheory.SimplicialObject.Splitting.summand {C : Type u_1} (N : ℕ → C) (Δ : SimplexCategoryᵒᵖ) (A : 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

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

@[reducible, inline]

abbrev CategoryTheory.SimplicialObject.Splitting.cofan' {C : Type u_1} [Category.{v_1, u_1} C] (N : ℕ → C) (X : SimplicialObject C) (φ : (n : ℕ) → N n ⟶ X.obj (Opposite.op { len := n })) (Δ : SimplexCategoryᵒᵖ) : Limits.Cofan (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 CategoryTheory.SimplicialObject.Splitting {C : Type u_1} [Category.{v_1, u_1} C] (X : SimplicialObject C) : Type (max u_1 v_1)

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 { len := n })

  The "inclusion" N n ⟶ X _⦋n⦌ for all n : ℕ.

• isColimit' (Δ : SimplexCategoryᵒᵖ) : Limits.IsColimit (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 CategoryTheory.SimplicialObject.Splitting.cofan {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) (Δ : SimplexCategoryᵒᵖ) : Limits.Cofan (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 CategoryTheory.SimplicialObject.Splitting.isColimit {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) (Δ : SimplexCategoryᵒᵖ) : Limits.IsColimit (s.cofan Δ)

The cofan s.cofan Δ is colimit.

Equations

• s.isColimit Δ = s.isColimit' Δ

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

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

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

def CategoryTheory.SimplicialObject.Splitting.φ {C : Type u_1} [Category.{v_1, u_1} C] {X Y : SimplicialObject C} (s : X.Splitting) (f : X ⟶ Y) (n : ℕ) : s.N n ⟶ Y.obj (Opposite.op { len := 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 { len := n }))

@[simp]

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

@[simp]

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

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

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

def CategoryTheory.SimplicialObject.Splitting.desc {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) {Z : C} (Δ : SimplexCategoryᵒᵖ) (F : (A : 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 CategoryTheory.SimplicialObject.Splitting.ι_desc {C : Type u_1} [Category.{v_1, u_1} C] {X : SimplicialObject C} (s : X.Splitting) {Z : C} (Δ : SimplexCategoryᵒᵖ) (F : (A : IndexSet Δ) → s.N (Opposite.unop A.fst).len ⟶ Z) (A : IndexSet Δ) : CategoryStruct.comp ((s.cofan Δ).inj A) (s.desc Δ F) = F A

@[simp]

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

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

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 CategoryTheory.SimplicialObject.Splitting.ofIso_N {C : Type u_1} [Category.{v_1, u_1} C] {X Y : SimplicialObject C} (s : X.Splitting) (e : X ≅ Y) (a✝ : ℕ) : (s.ofIso e).N a✝ = s.N a✝

@[simp]

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

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

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

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

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 : SimplicialObject C

  the underlying simplicial object

• s : self.X.Splitting

  a splitting of the simplicial object

theorem CategoryTheory.SimplicialObject.Split.ext_iff {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {x y : Split C} : x = y ↔ x.X = y.X ∧ x.s ≍ y.s

theorem CategoryTheory.SimplicialObject.Split.ext {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {x y : Split C} (X : x.X = y.X) (s : x.s ≍ y.s) : x = y

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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 : ℕ) : CategoryStruct.comp (S₁.s.ι n) (self.F.app (Opposite.op { len := n })) = CategoryStruct.comp (self.f n) (S₂.s.ι n)

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

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

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

@[implicit_reducible]

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

Equations

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

def CategoryTheory.SimplicialObject.Split.evalN (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) : Functor (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 CategoryTheory.SimplicialObject.Split.evalN_map (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) {X✝ Y✝ : Split C} (Φ : X✝ ⟶ Y✝) : (evalN C n).map Φ = Φ.f n

@[simp]

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

def CategoryTheory.SimplicialObject.Split.natTransCofanInj (C : Type u_1) [Category.{v_1, u_1} C] {Δ : SimplexCategoryᵒᵖ} (A : Splitting.IndexSet Δ) : evalN C (Opposite.unop A.fst).len ⟶ (forget C).comp ((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

• CategoryTheory.SimplicialObject.Split.natTransCofanInj C A = { app := fun (S : CategoryTheory.SimplicialObject.Split C) => (S.s.cofan Δ).inj A, naturality := ⋯ }

@[simp]

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