Split simplicial objects #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 simplex_category. (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
simplicial_object.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.
Equations
- simplicial_object.splitting.index_set Δ = Σ (Δ' : simplex_categoryᵒᵖ), {α // category_theory.epi α}
Instances for simplicial_object.splitting.index_set
@[simp]
theorem
simplicial_object.splitting.index_set.mk_fst
{Δ Δ' : simplex_category}
(f : Δ ⟶ Δ')
[category_theory.epi f] :
def
simplicial_object.splitting.index_set.mk
{Δ Δ' : simplex_category}
(f : Δ ⟶ Δ')
[category_theory.epi f] :
The element in splitting.index_set Δ attached to an epimorphism f : Δ ⟶ Δ'.
Equations
- simplicial_object.splitting.index_set.mk f = ⟨opposite.op Δ', ⟨f, _⟩⟩
@[simp]
theorem
simplicial_object.splitting.index_set.mk_snd_coe
{Δ Δ' : simplex_category}
(f : Δ ⟶ Δ')
[category_theory.epi f] :
def
simplicial_object.splitting.index_set.e
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
The epimorphism in simplex_category associated to A : splitting.index_set Δ
Instances for simplicial_object.splitting.index_set.e
@[protected, instance]
theorem
simplicial_object.splitting.index_set.ext'
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
theorem
simplicial_object.splitting.index_set.ext
{Δ : simplex_categoryᵒᵖ}
(A₁ A₂ : simplicial_object.splitting.index_set Δ)
(h₁ : A₁.fst = A₂.fst)
(h₂ : A₁.e ≫ category_theory.eq_to_hom _ = A₂.e) :
A₁ = A₂
@[protected, instance]
Equations
- simplicial_object.splitting.index_set.fintype = fintype.of_injective (λ (A : simplicial_object.splitting.index_set Δ), ⟨⟨(opposite.unop A.fst).len, _⟩, ⇑(simplex_category.hom.to_order_hom A.e)⟩) simplicial_object.splitting.index_set.fintype._proof_2
The distinguished element in splitting.index_set Δ which corresponds to the
identity of Δ.
Equations
- simplicial_object.splitting.index_set.id Δ = ⟨Δ, ⟨𝟙 (opposite.unop Δ), _⟩⟩
@[protected, instance]
@[simp]
def
simplicial_object.splitting.index_set.eq_id
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
Prop
The condition that an element splitting.index_set Δ is the distinguished
element splitting.index_set.id Δ.
Equations
theorem
simplicial_object.splitting.index_set.eq_id_iff_len_eq
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
A.eq_id ↔ (opposite.unop A.fst).len = (opposite.unop Δ).len
theorem
simplicial_object.splitting.index_set.eq_id_iff_len_le
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
A.eq_id ↔ (opposite.unop Δ).len ≤ (opposite.unop A.fst).len
theorem
simplicial_object.splitting.index_set.eq_id_iff_mono
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
A.eq_id ↔ category_theory.mono A.e
def
simplicial_object.splitting.index_set.epi_comp
{Δ₁ Δ₂ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ₁)
(p : Δ₁ ⟶ Δ₂)
[category_theory.epi p.unop] :
Given A : index_set Δ₁, if p.unop : unop Δ₂ ⟶ unop Δ₁ is an epi, this
is the obvious element in A : index_set Δ₂ associated to the composition
of epimorphisms p.unop ≫ A.e.
@[simp]
theorem
simplicial_object.splitting.index_set.epi_comp_fst
{Δ₁ Δ₂ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ₁)
(p : Δ₁ ⟶ Δ₂)
[category_theory.epi p.unop] :
@[simp]
theorem
simplicial_object.splitting.index_set.epi_comp_snd_coe
{Δ₁ Δ₂ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ₁)
(p : Δ₁ ⟶ Δ₂)
[category_theory.epi p.unop] :
noncomputable
def
simplicial_object.splitting.index_set.pull
{Δ' Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
(θ : Δ ⟶ Δ') :
When A : index_set Δ and θ : Δ → Δ' is a morphism in simplex_categoryᵒᵖ,
an element in index_set Δ' can be defined by using the epi-mono factorisation
of θ.unop ≫ A.e.
Equations
theorem
simplicial_object.splitting.index_set.fac_pull
{Δ' Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
(θ : Δ ⟶ Δ') :
theorem
simplicial_object.splitting.index_set.fac_pull_assoc
{Δ' Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
(θ : Δ ⟶ Δ')
{X' : simplex_category}
(f' : opposite.unop A.fst ⟶ X') :
@[simp, nolint]
def
simplicial_object.splitting.summand
{C : Type u_1}
[category_theory.category C]
(N : ℕ → C)
(Δ : simplex_categoryᵒᵖ)
(A : simplicial_object.splitting.index_set Δ) :
C
Given a sequences of objects N : ℕ → C in a category C, this is
a family of objects indexed by the elements A : splitting.index_set Δ.
The Δ-simplices of a split simplicial objects shall identify to the
coproduct of objects in such a family.
Equations
- simplicial_object.splitting.summand N Δ A = N (opposite.unop A.fst).len
@[simp]
noncomputable
def
simplicial_object.splitting.coprod
{C : Type u_1}
[category_theory.category C]
(N : ℕ → C)
(Δ : simplex_categoryᵒᵖ)
[category_theory.limits.has_finite_coproducts C] :
C
The coproduct of the family summand N Δ
Equations
@[simp]
noncomputable
def
simplicial_object.splitting.ι_coprod
{C : Type u_1}
[category_theory.category C]
(N : ℕ → C)
{Δ : simplex_categoryᵒᵖ}
[category_theory.limits.has_finite_coproducts C]
(A : simplicial_object.splitting.index_set Δ) :
N (opposite.unop A.fst).len ⟶ simplicial_object.splitting.coprod N Δ
The inclusion of a summand in the coproduct.
Equations
- simplicial_object.splitting.ι_coprod N A = category_theory.limits.sigma.ι (λ (A : simplicial_object.splitting.index_set Δ), N (opposite.unop A.fst).len) A
@[simp]
noncomputable
def
simplicial_object.splitting.map
{C : Type u_1}
[category_theory.category C]
{N : ℕ → C}
(X : category_theory.simplicial_object C)
(φ : Π (n : ℕ), N n ⟶ X.obj (opposite.op (simplex_category.mk n)))
[category_theory.limits.has_finite_coproducts C]
(Δ : simplex_categoryᵒᵖ) :
simplicial_object.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].
Equations
- simplicial_object.splitting.map X φ Δ = category_theory.limits.sigma.desc (λ (A : simplicial_object.splitting.index_set Δ), φ (opposite.unop A.fst).len ≫ X.map A.e.op)
Instances for simplicial_object.splitting.map
@[nolint]
structure
simplicial_object.splitting
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
(X : category_theory.simplicial_object C) :
Type (max u_1 u_2)
- N : ℕ → C
- ι : Π (n : ℕ), self.N n ⟶ X.obj (opposite.op (simplex_category.mk n))
- map_is_iso' : ∀ (Δ : simplex_categoryᵒᵖ), category_theory.is_iso (simplicial_object.splitting.map X self.ι Δ)
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 Δ : simplex_categoryhᵒᵖ, the canonical map splitting.map X ι Δ
is an isomorphism.
Instances for simplicial_object.splitting
- simplicial_object.splitting.has_sizeof_inst
@[protected, instance]
def
simplicial_object.splitting.map_is_iso
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
(Δ : simplex_categoryᵒᵖ) :
@[simp]
theorem
simplicial_object.splitting.iso_inv
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
(Δ : simplex_categoryᵒᵖ) :
(s.iso Δ).inv = category_theory.inv (category_theory.limits.sigma.desc (λ (A : simplicial_object.splitting.index_set Δ), s.ι (opposite.unop A.fst).len ≫ X.map A.e.op))
@[simp]
theorem
simplicial_object.splitting.iso_hom
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
(Δ : simplex_categoryᵒᵖ) :
(s.iso Δ).hom = category_theory.limits.sigma.desc (λ (A : simplicial_object.splitting.index_set Δ), s.ι (opposite.unop A.fst).len ≫ X.map A.e.op)
noncomputable
def
simplicial_object.splitting.iso
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
(Δ : simplex_categoryᵒᵖ) :
simplicial_object.splitting.coprod s.N Δ ≅ X.obj Δ
The isomorphism on simplices given by the axiom splitting.map_is_iso'
Equations
- s.iso Δ = category_theory.as_iso (simplicial_object.splitting.map X s.ι Δ)
noncomputable
def
simplicial_object.splitting.ι_summand
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
Via the isomorphism s.iso Δ, this is the inclusion of a summand
in the direct sum decomposition given by the splitting s : splitting X.
theorem
simplicial_object.splitting.ι_summand_eq
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
theorem
simplicial_object.splitting.ι_summand_eq_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
{X' : C}
(f' : X.obj Δ ⟶ X') :
theorem
simplicial_object.splitting.ι_summand_id
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
(n : ℕ) :
@[simp]
def
simplicial_object.splitting.φ
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X Y : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
(f : X ⟶ Y)
(n : ℕ) :
s.N n ⟶ Y.obj (opposite.op (simplex_category.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 = s.ι n ≫ f.app (opposite.op (simplex_category.mk n))
@[simp]
theorem
simplicial_object.splitting.ι_summand_comp_app
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X Y : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
(f : X ⟶ Y)
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
@[simp]
theorem
simplicial_object.splitting.ι_summand_comp_app_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X Y : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
(f : X ⟶ Y)
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
{X' : C}
(f' : Y.obj Δ ⟶ X') :
theorem
simplicial_object.splitting.hom_ext'
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
{Z : C}
{Δ : simplex_categoryᵒᵖ}
(f g : X.obj Δ ⟶ Z)
(h : ∀ (A : simplicial_object.splitting.index_set Δ), s.ι_summand A ≫ f = s.ι_summand A ≫ g) :
f = g
theorem
simplicial_object.splitting.hom_ext
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X Y : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
(f g : X ⟶ Y)
(h : ∀ (n : ℕ), s.φ f n = s.φ g n) :
f = g
noncomputable
def
simplicial_object.splitting.desc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
{Z : C}
(Δ : simplex_categoryᵒᵖ)
(F : Π (A : simplicial_object.splitting.index_set Δ), s.N (opposite.unop A.fst).len ⟶ 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
@[simp]
theorem
simplicial_object.splitting.ι_desc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
{Z : C}
(Δ : simplex_categoryᵒᵖ)
(F : Π (A : simplicial_object.splitting.index_set Δ), s.N (opposite.unop A.fst).len ⟶ Z)
(A : simplicial_object.splitting.index_set Δ) :
@[simp]
theorem
simplicial_object.splitting.ι_desc_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
{Z : C}
(Δ : simplex_categoryᵒᵖ)
(F : Π (A : simplicial_object.splitting.index_set Δ), s.N (opposite.unop A.fst).len ⟶ Z)
(A : simplicial_object.splitting.index_set Δ)
{X' : C}
(f' : Z ⟶ X') :
def
simplicial_object.splitting.of_iso
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X Y : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
(e : X ≅ Y) :
A simplicial object that is isomorphic to a split simplicial object is split.
Equations
- s.of_iso e = {N := s.N, ι := λ (n : ℕ), s.ι n ≫ e.hom.app (opposite.op (simplex_category.mk n)), map_is_iso' := _}
@[simp]
theorem
simplicial_object.splitting.of_iso_N
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X Y : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
(e : X ≅ Y)
(ᾰ : ℕ) :
@[simp]
theorem
simplicial_object.splitting.of_iso_ι
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X Y : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
(e : X ≅ Y)
(n : ℕ) :
(s.of_iso e).ι n = s.ι n ≫ e.hom.app (opposite.op (simplex_category.mk n))
theorem
simplicial_object.splitting.ι_summand_epi_naturality
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
{Δ₁ Δ₂ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ₁)
(p : Δ₁ ⟶ Δ₂)
[category_theory.epi p.unop] :
theorem
simplicial_object.splitting.ι_summand_epi_naturality_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
{Δ₁ Δ₂ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ₁)
(p : Δ₁ ⟶ Δ₂)
[category_theory.epi p.unop]
{X' : C}
(f' : X.obj Δ₂ ⟶ X') :
theorem
simplicial_object.split.ext
{C : Type u_1}
{_inst_1 : category_theory.category C}
{_inst_2 : category_theory.limits.has_finite_coproducts C}
(x y : simplicial_object.split C)
(h : x.X = y.X)
(h_1 : x.s == y.s) :
x = y
theorem
simplicial_object.split.ext_iff
{C : Type u_1}
{_inst_1 : category_theory.category C}
{_inst_2 : category_theory.limits.has_finite_coproducts C}
(x y : simplicial_object.split C) :
@[nolint, ext]
structure
simplicial_object.split
(C : Type u_1)
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C] :
Type (max u_1 u_2)
- X : category_theory.simplicial_object C
- s : simplicial_object.splitting self.X
The category simplicial_object.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 simplicial_object.split
- simplicial_object.split.has_sizeof_inst
- simplicial_object.split.category_theory.category
@[simp]
theorem
simplicial_object.split.mk'_s
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X) :
(simplicial_object.split.mk' s).s = s
@[simp]
theorem
simplicial_object.split.mk'_X
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X) :
(simplicial_object.split.mk' s).X = X
def
simplicial_object.split.mk'
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X) :
The object in simplicial_object.split C attached to a splitting s : splitting X
of a simplicial object X.
Equations
- simplicial_object.split.mk' s = {X := X, s := s}
@[nolint]
structure
simplicial_object.split.hom
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
(S₁ S₂ : simplicial_object.split C) :
Type u_2
- F : S₁.X ⟶ S₂.X
- f : Π (n : ℕ), S₁.s.N n ⟶ S₂.s.N n
- comm' : ∀ (n : ℕ), S₁.s.ι n ≫ self.F.app (opposite.op (simplex_category.mk n)) = self.f n ≫ S₂.s.ι n
Morphisms in simplicial_object.split C are morphisms of simplicial objects that
are compatible with the splittings.
Instances for simplicial_object.split.hom
- simplicial_object.split.hom.has_sizeof_inst
@[ext]
theorem
simplicial_object.split.hom.ext
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{S₁ S₂ : simplicial_object.split C}
(Φ₁ Φ₂ : S₁.hom S₂)
(h : ∀ (n : ℕ), Φ₁.f n = Φ₂.f n) :
Φ₁ = Φ₂
@[simp]
theorem
simplicial_object.split.hom.comm
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{S₁ S₂ : simplicial_object.split C}
(self : S₁.hom S₂)
(n : ℕ) :
@[simp]
theorem
simplicial_object.split.hom.comm_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{S₁ S₂ : simplicial_object.split C}
(self : S₁.hom S₂)
(n : ℕ)
{X' : C}
(f' : S₂.X.obj (opposite.op (simplex_category.mk n)) ⟶ X') :
@[protected, instance]
def
simplicial_object.split.category_theory.category
(C : Type u_1)
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C] :
Equations
- simplicial_object.split.category_theory.category C = {to_category_struct := {to_quiver := {hom := simplicial_object.split.hom _inst_2}, id := λ (S : simplicial_object.split C), {F := 𝟙 S.X, f := λ (n : ℕ), 𝟙 (S.s.N n), comm' := _}, comp := λ (S₁ S₂ S₃ : simplicial_object.split C) (Φ₁₂ : S₁ ⟶ S₂) (Φ₂₃ : S₂ ⟶ S₃), {F := Φ₁₂.F ≫ Φ₂₃.F, f := λ (n : ℕ), Φ₁₂.f n ≫ Φ₂₃.f n, comm' := _}}, id_comp' := _, comp_id' := _, assoc' := _}
theorem
simplicial_object.split.congr_F
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{S₁ S₂ : simplicial_object.split C}
{Φ₁ Φ₂ : S₁ ⟶ S₂}
(h : Φ₁ = Φ₂) :
theorem
simplicial_object.split.congr_f
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{S₁ S₂ : simplicial_object.split C}
{Φ₁ Φ₂ : S₁ ⟶ S₂}
(h : Φ₁ = Φ₂)
(n : ℕ) :
@[simp]
theorem
simplicial_object.split.id_F
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
(S : simplicial_object.split C) :
@[simp]
theorem
simplicial_object.split.id_f
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
(S : simplicial_object.split C)
(n : ℕ) :
@[simp]
theorem
simplicial_object.split.comp_F
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{S₁ S₂ S₃ : simplicial_object.split C}
(Φ₁₂ : S₁ ⟶ S₂)
(Φ₂₃ : S₂ ⟶ S₃) :
@[simp]
theorem
simplicial_object.split.comp_f
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{S₁ S₂ S₃ : simplicial_object.split C}
(Φ₁₂ : S₁ ⟶ S₂)
(Φ₂₃ : S₂ ⟶ S₃)
(n : ℕ) :
@[simp]
theorem
simplicial_object.split.ι_summand_naturality_symm
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{S₁ S₂ : simplicial_object.split C}
(Φ : S₁ ⟶ S₂)
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
@[simp]
theorem
simplicial_object.split.ι_summand_naturality_symm_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{S₁ S₂ : simplicial_object.split C}
(Φ : S₁ ⟶ S₂)
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
{X' : C}
(f' : S₂.X.obj Δ ⟶ X') :
@[simp]
theorem
simplicial_object.split.forget_map
(C : Type u_1)
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
(S₁ S₂ : simplicial_object.split C)
(Φ : S₁ ⟶ S₂) :
(simplicial_object.split.forget C).map Φ = Φ.F
def
simplicial_object.split.forget
(C : Type u_1)
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C] :
The functor simplicial_object.split C ⥤ simplicial_object C which forgets
the splitting.
Equations
- simplicial_object.split.forget C = {obj := λ (S : simplicial_object.split C), S.X, map := λ (S₁ S₂ : simplicial_object.split C) (Φ : S₁ ⟶ S₂), Φ.F, map_id' := _, map_comp' := _}
@[simp]
theorem
simplicial_object.split.forget_obj
(C : Type u_1)
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
(S : simplicial_object.split C) :
(simplicial_object.split.forget C).obj S = S.X
@[simp]
theorem
simplicial_object.split.eval_N_obj
(C : Type u_1)
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
(n : ℕ)
(S : simplicial_object.split C) :
(simplicial_object.split.eval_N C n).obj S = S.s.N n
@[simp]
theorem
simplicial_object.split.eval_N_map
(C : Type u_1)
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
(n : ℕ)
(S₁ S₂ : simplicial_object.split C)
(Φ : S₁ ⟶ S₂) :
(simplicial_object.split.eval_N C n).map Φ = Φ.f n
def
simplicial_object.split.eval_N
(C : Type u_1)
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
(n : ℕ) :
The functor simplicial_object.split C ⥤ C which sends a simplicial object equipped
with a splitting to its nondegenerate n-simplices.
Equations
- simplicial_object.split.eval_N C n = {obj := λ (S : simplicial_object.split C), S.s.N n, map := λ (S₁ S₂ : simplicial_object.split C) (Φ : S₁ ⟶ S₂), Φ.f n, map_id' := _, map_comp' := _}
noncomputable
def
simplicial_object.split.nat_trans_ι_summand
(C : Type u_1)
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
The inclusion of each summand in the coproduct decomposition of simplices
in split simplicial objects is a natural transformation of functors
simplicial_object.split C ⥤ C
Equations
- simplicial_object.split.nat_trans_ι_summand C A = {app := λ (S : simplicial_object.split C), S.s.ι_summand A, naturality' := _}
@[simp]
theorem
simplicial_object.split.nat_trans_ι_summand_app
(C : Type u_1)
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
(S : simplicial_object.split C) :
(simplicial_object.split.nat_trans_ι_summand C A).app S = S.s.ι_summand A