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 simplical 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
The index set which appears in the definition of split simplicial objects.
Instances For
@[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]
:
The element in Splitting.IndexSet Δ attached to an epimorphism f : Δ ⟶ Δ'.
Instances For
def
SimplicialObject.Splitting.IndexSet.e
{Δ : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ)
:
Δ.unop ⟶ A.fst.unop
The epimorphism in SimplexCategory associated to A : Splitting.IndexSet Δ
Instances For
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₂
@[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
The distinguished element in Splitting.IndexSet Δ which corresponds to the
identity of Δ.
Instances For
def
SimplicialObject.Splitting.IndexSet.EqId
{Δ : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ)
:
The condition that an element Splitting.IndexSet Δ is the distinguished
element Splitting.IndexSet.Id Δ.
Instances For
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
@[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
@[simp]
theorem
SimplicialObject.Splitting.IndexSet.epiComp_snd_coe
{Δ₁ : SimplexCategoryᵒᵖ}
{Δ₂ : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ₁)
(p : Δ₁ ⟶ Δ₂)
[CategoryTheory.Epi p.unop]
:
def
SimplicialObject.Splitting.IndexSet.epiComp
{Δ₁ : SimplexCategoryᵒᵖ}
{Δ₂ : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ₁)
(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.
Instances For
def
SimplicialObject.Splitting.IndexSet.pull
{Δ : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ)
{Δ' : SimplexCategoryᵒᵖ}
(θ : Δ ⟶ Δ')
:
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.
Instances For
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.
Instances For
@[inline, reducible]
abbrev
SimplicialObject.Splitting.coprod
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(N : ℕ → C)
(Δ : SimplexCategoryᵒᵖ)
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
C
The coproduct of the family summand N Δ
Instances For
def
SimplicialObject.Splitting.ιCoprod
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(N : ℕ → C)
{Δ : SimplexCategoryᵒᵖ}
[CategoryTheory.Limits.HasFiniteCoproducts C]
(A : SimplicialObject.Splitting.IndexSet Δ)
:
N (SimplexCategory.len A.fst.unop) ⟶ SimplicialObject.Splitting.coprod N Δ
The inclusion of a summand in the coproduct.
Instances For
def
SimplicialObject.Splitting.map
{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)))
[CategoryTheory.Limits.HasFiniteCoproducts C]
(Δ : SimplexCategoryᵒᵖ)
:
SimplicialObject.Splitting.coprod N Δ ⟶ X.obj Δ
The canonical morphism coprod N Δ ⟶ X.obj Δ attached to a sequence
of objects N and a sequence of morphisms N n ⟶ X _[n].
Instances For
structure
SimplicialObject.Splitting
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(X : CategoryTheory.SimplicialObject C)
:
Type (max u_1 u_2)
- N : ℕ → C
- ι : (n : ℕ) → SimplicialObject.Splitting.N s n ⟶ X.obj (Opposite.op (SimplexCategory.mk n))
- map_isIso : ∀ (Δ : SimplexCategoryᵒᵖ), CategoryTheory.IsIso (SimplicialObject.Splitting.map X s.ι Δ)
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.
Instances For
def
SimplicialObject.Splitting.iso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
(Δ : SimplexCategoryᵒᵖ)
:
SimplicialObject.Splitting.coprod s.N Δ ≅ X.obj Δ
The isomorphism on simplices given by the axiom Splitting.map_isIso
Instances For
@[simp]
theorem
SimplicialObject.Splitting.iso_hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
(Δ : SimplexCategoryᵒᵖ)
:
(SimplicialObject.Splitting.iso s Δ).hom = SimplicialObject.Splitting.map X s.ι Δ
@[simp]
theorem
SimplicialObject.Splitting.iso_inv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
(Δ : SimplexCategoryᵒᵖ)
:
(SimplicialObject.Splitting.iso s Δ).inv = CategoryTheory.inv (SimplicialObject.Splitting.map X s.ι Δ)
def
SimplicialObject.Splitting.ιSummand
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
{Δ : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ)
:
SimplicialObject.Splitting.N s (SimplexCategory.len A.fst.unop) ⟶ X.obj Δ
Via the isomorphism s.iso Δ, this is the inclusion of a summand
in the direct sum decomposition given by the splitting s : Splitting X.
Instances For
theorem
SimplicialObject.Splitting.ιSummand_eq_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
{Δ : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ)
{Z : C}
(h : X.obj Δ ⟶ Z)
:
theorem
SimplicialObject.Splitting.ιSummand_eq
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
{Δ : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ)
:
SimplicialObject.Splitting.ιSummand s A = CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.ι s (SimplexCategory.len A.fst.unop))
(X.map (SimplicialObject.Splitting.IndexSet.e A).op)
theorem
SimplicialObject.Splitting.ιSummand_id
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
(n : ℕ)
:
def
SimplicialObject.Splitting.φ
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
{Y : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
(f : X ⟶ Y)
(n : ℕ)
:
SimplicialObject.Splitting.N s 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.
Instances For
@[simp]
theorem
SimplicialObject.Splitting.ιSummand_comp_app_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts 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 (SimplicialObject.Splitting.ιSummand s A)
(CategoryTheory.CategoryStruct.comp (f.app Δ) h) = CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.φ s f (SimplexCategory.len A.fst.unop))
(CategoryTheory.CategoryStruct.comp (Y.map (SimplicialObject.Splitting.IndexSet.e A).op) h)
@[simp]
theorem
SimplicialObject.Splitting.ιSummand_comp_app
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
{Y : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
(f : X ⟶ Y)
{Δ : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ)
:
CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.ιSummand s A) (f.app Δ) = CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.φ s f (SimplexCategory.len A.fst.unop))
(Y.map (SimplicialObject.Splitting.IndexSet.e A).op)
theorem
SimplicialObject.Splitting.hom_ext'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts 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 (SimplicialObject.Splitting.ιSummand s A) f = CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.ιSummand s A) g)
:
f = g
theorem
SimplicialObject.Splitting.hom_ext
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts 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]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
{Z : C}
(Δ : SimplexCategoryᵒᵖ)
(F : (A : SimplicialObject.Splitting.IndexSet Δ) → SimplicialObject.Splitting.N s (SimplexCategory.len A.fst.unop) ⟶ 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
Instances For
@[simp]
theorem
SimplicialObject.Splitting.ι_desc_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
{Z : C}
(Δ : SimplexCategoryᵒᵖ)
(F : (A : SimplicialObject.Splitting.IndexSet Δ) → SimplicialObject.Splitting.N s (SimplexCategory.len A.fst.unop) ⟶ Z)
(A : SimplicialObject.Splitting.IndexSet Δ)
{Z : C}
(h : Z ⟶ Z)
:
@[simp]
theorem
SimplicialObject.Splitting.ι_desc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
{Z : C}
(Δ : SimplexCategoryᵒᵖ)
(F : (A : SimplicialObject.Splitting.IndexSet Δ) → SimplicialObject.Splitting.N s (SimplexCategory.len A.fst.unop) ⟶ Z)
(A : SimplicialObject.Splitting.IndexSet Δ)
:
@[simp]
theorem
SimplicialObject.Splitting.ofIso_ι
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
{Y : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
(e : X ≅ Y)
(n : ℕ)
:
SimplicialObject.Splitting.ι (SimplicialObject.Splitting.ofIso s e) n = CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.ι 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]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
{Y : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
(e : X ≅ Y)
:
∀ (a : ℕ), SimplicialObject.Splitting.N (SimplicialObject.Splitting.ofIso s e) a = SimplicialObject.Splitting.N s a
def
SimplicialObject.Splitting.ofIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
{Y : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
(e : X ≅ Y)
:
A simplicial object that is isomorphic to a split simplicial object is split.
Instances For
theorem
SimplicialObject.Splitting.ιSummand_epi_naturality_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts 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)
:
theorem
SimplicialObject.Splitting.ιSummand_epi_naturality
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
{Δ₁ : SimplexCategoryᵒᵖ}
{Δ₂ : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ₁)
(p : Δ₁ ⟶ Δ₂)
[CategoryTheory.Epi p.unop]
:
theorem
SimplicialObject.Split.ext
{C : Type u_1}
:
∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Limits.HasFiniteCoproducts 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} {inst_1 : CategoryTheory.Limits.HasFiniteCoproducts 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]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
Type (max u_1 u_2)
- s : SimplicialObject.Splitting s.X
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.
Instances For
@[simp]
theorem
SimplicialObject.Split.mk'_s
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
:
(SimplicialObject.Split.mk' s).s = s
@[simp]
theorem
SimplicialObject.Split.mk'_X
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
:
(SimplicialObject.Split.mk' s).X = X
def
SimplicialObject.Split.mk'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{X : CategoryTheory.SimplicialObject C}
(s : SimplicialObject.Splitting X)
:
The object in SimplicialObject.Split C attached to a splitting s : Splitting X
of a simplicial object X.
Instances For
structure
SimplicialObject.Split.Hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(S₁ : SimplicialObject.Split C)
(S₂ : SimplicialObject.Split C)
:
Type u_2
- F : S₁.X ⟶ S₂.X
- f : (n : ℕ) → SimplicialObject.Splitting.N S₁.s n ⟶ SimplicialObject.Splitting.N S₂.s n
- comm : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.ι S₁.s n) (s.F.app (Opposite.op (SimplexCategory.mk n))) = CategoryTheory.CategoryStruct.comp (SimplicialObject.Split.Hom.f s n) (SimplicialObject.Splitting.ι S₂.s n)
Morphisms in SimplicialObject.Split C are morphisms of simplicial objects that
are compatible with the splittings.
Instances For
theorem
SimplicialObject.Split.Hom.ext
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{S₁ : SimplicialObject.Split C}
{S₂ : SimplicialObject.Split C}
(Φ₁ : SimplicialObject.Split.Hom S₁ S₂)
(Φ₂ : SimplicialObject.Split.Hom S₁ S₂)
(h : ∀ (n : ℕ), SimplicialObject.Split.Hom.f Φ₁ n = SimplicialObject.Split.Hom.f Φ₂ n)
:
Φ₁ = Φ₂
theorem
SimplicialObject.Split.Hom.comm_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{S₁ : SimplicialObject.Split C}
{S₂ : SimplicialObject.Split C}
(self : SimplicialObject.Split.Hom S₁ S₂)
(n : ℕ)
{Z : C}
(h : S₂.X.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.ι S₁.s n)
(CategoryTheory.CategoryStruct.comp (self.F.app (Opposite.op (SimplexCategory.mk n))) h) = CategoryTheory.CategoryStruct.comp (SimplicialObject.Split.Hom.f self n)
(CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.ι S₂.s n) h)
theorem
SimplicialObject.Split.hom_ext
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{S₁ : SimplicialObject.Split C}
{S₂ : SimplicialObject.Split C}
(Φ₁ : S₁ ⟶ S₂)
(Φ₂ : S₁ ⟶ S₂)
(h : ∀ (n : ℕ), SimplicialObject.Split.Hom.f Φ₁ n = SimplicialObject.Split.Hom.f Φ₂ n)
:
Φ₁ = Φ₂
theorem
SimplicialObject.Split.congr_F
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts 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]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{S₁ : SimplicialObject.Split C}
{S₂ : SimplicialObject.Split C}
{Φ₁ : S₁ ⟶ S₂}
{Φ₂ : S₁ ⟶ S₂}
(h : Φ₁ = Φ₂)
(n : ℕ)
:
@[simp]
theorem
SimplicialObject.Split.id_F
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(S : SimplicialObject.Split C)
:
@[simp]
theorem
SimplicialObject.Split.id_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(S : SimplicialObject.Split C)
(n : ℕ)
:
@[simp]
theorem
SimplicialObject.Split.comp_F
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts 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]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{S₁ : SimplicialObject.Split C}
{S₂ : SimplicialObject.Split C}
{S₃ : SimplicialObject.Split C}
(Φ₁₂ : S₁ ⟶ S₂)
(Φ₂₃ : S₂ ⟶ S₃)
(n : ℕ)
:
@[simp]
theorem
SimplicialObject.Split.ιSummand_naturality_symm_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts 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 (SimplicialObject.Splitting.ιSummand S₁.s A)
(CategoryTheory.CategoryStruct.comp (Φ.F.app Δ) h) = CategoryTheory.CategoryStruct.comp (SimplicialObject.Split.Hom.f Φ (SimplexCategory.len A.fst.unop))
(CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.ιSummand S₂.s A) h)
@[simp]
theorem
SimplicialObject.Split.ιSummand_naturality_symm
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{S₁ : SimplicialObject.Split C}
{S₂ : SimplicialObject.Split C}
(Φ : S₁ ⟶ S₂)
{Δ : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ)
:
CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.ιSummand S₁.s A) (Φ.F.app Δ) = CategoryTheory.CategoryStruct.comp (SimplicialObject.Split.Hom.f Φ (SimplexCategory.len A.fst.unop))
(SimplicialObject.Splitting.ιSummand S₂.s A)
@[simp]
theorem
SimplicialObject.Split.forget_obj
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(S : SimplicialObject.Split C)
:
(SimplicialObject.Split.forget C).obj S = S.X
@[simp]
theorem
SimplicialObject.Split.forget_map
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
∀ {X Y : SimplicialObject.Split C} (Φ : X ⟶ Y), (SimplicialObject.Split.forget C).map Φ = Φ.F
def
SimplicialObject.Split.forget
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
The functor SimplicialObject.Split C ⥤ SimplicialObject C which forgets
the splitting.
Instances For
@[simp]
theorem
SimplicialObject.Split.evalN_map
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(n : ℕ)
:
∀ {X Y : SimplicialObject.Split C} (Φ : X ⟶ Y),
(SimplicialObject.Split.evalN C n).map Φ = SimplicialObject.Split.Hom.f Φ n
@[simp]
theorem
SimplicialObject.Split.evalN_obj
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(n : ℕ)
(S : SimplicialObject.Split C)
:
(SimplicialObject.Split.evalN C n).obj S = SimplicialObject.Splitting.N S.s n
def
SimplicialObject.Split.evalN
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(n : ℕ)
:
The functor SimplicialObject.Split C ⥤ C which sends a simplicial object equipped
with a splitting to its nondegenerate n-simplices.
Instances For
@[simp]
theorem
SimplicialObject.Split.natTransιSummand_app
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
{Δ : SimplexCategoryᵒᵖ}
(A : SimplicialObject.Splitting.IndexSet Δ)
(S : SimplicialObject.Split C)
:
(SimplicialObject.Split.natTransιSummand C A).app S = SimplicialObject.Splitting.ιSummand S.s A
def
SimplicialObject.Split.natTransιSummand
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts 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).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