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 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
The element in splitting.index_set Δ
attached to an epimorphism f : Δ ⟶ Δ'
.
Equations
- simplicial_object.splitting.index_set.mk f = ⟨opposite.op Δ', ⟨f, _⟩⟩
The epimorphism in simplex_category
associated to A : splitting.index_set Δ
Instances for simplicial_object.splitting.index_set.e
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 Δ), _⟩⟩
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
The coproduct of the family summand N Δ
Equations
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
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
- 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
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.ι Δ)
Via the isomorphism s.iso Δ
, this is the inclusion of a summand
in the direct sum decomposition given by the splitting s : splitting X
.
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))
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
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' := _}
- 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
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}
- 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
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' := _}
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' := _}
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' := _}
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' := _}