# mathlib3documentation

algebraic_topology.split_simplicial_object

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

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

Equations
Instances for simplicial_object.splitting.index_set
@[simp]

The element in splitting.index_set Δ attached to an epimorphism f : Δ ⟶ Δ'.

Equations
@[simp]

The epimorphism in simplex_category associated to A : splitting.index_set Δ

Equations
Instances for simplicial_object.splitting.index_set.e
@[protected, instance]
theorem simplicial_object.splitting.index_set.ext {Δ : simplex_categoryᵒᵖ} (A₁ A₂ : simplicial_object.splitting.index_set Δ) (h₁ : A₁.fst = A₂.fst) (h₂ : = A₂.e) :
A₁ = A₂
@[protected, instance]
Equations

The distinguished element in splitting.index_set Δ which corresponds to the identity of Δ.

Equations
@[protected, instance]
Equations
@[simp]

The condition that an element splitting.index_set Δ is the distinguished element splitting.index_set.id Δ.

Equations

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.

Equations
@[simp]
theorem simplicial_object.splitting.index_set.epi_comp_fst {Δ₁ Δ₂ : simplex_categoryᵒᵖ} (p : Δ₁ Δ₂)  :
(A.epi_comp p).fst = A.fst
@[simp]
theorem simplicial_object.splitting.index_set.epi_comp_snd_coe {Δ₁ Δ₂ : simplex_categoryᵒᵖ} (p : Δ₁ Δ₂)  :
((A.epi_comp p).snd) = p.unop A.e
noncomputable def simplicial_object.splitting.index_set.pull {Δ' Δ : simplex_categoryᵒᵖ} (θ : Δ Δ') :

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_assoc {Δ' Δ : simplex_categoryᵒᵖ} (θ : Δ Δ') {X' : simplex_category} (f' : X') :
(A.pull θ).e f' = θ.unop A.e f'
@[simp, nolint]

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
@[simp]
noncomputable def simplicial_object.splitting.coprod {C : Type u_1} (N : C) (Δ : simplex_categoryᵒᵖ)  :
C

The coproduct of the family summand N Δ

Equations
@[simp]
noncomputable def simplicial_object.splitting.ι_coprod {C : Type u_1} (N : C) {Δ : simplex_categoryᵒᵖ}  :

The inclusion of a summand in the coproduct.

Equations
@[simp]
noncomputable def simplicial_object.splitting.map {C : Type u_1} {N : C} (φ : Π (n : ), N n X.obj ) (Δ : simplex_categoryᵒᵖ) :

The canonical morphism coprod N Δ ⟶ X.obj Δ attached to a sequence of objects N and a sequence of morphisms N n ⟶ X _[n].

Equations
Instances for simplicial_object.splitting.map
@[nolint]
structure simplicial_object.splitting {C : Type u_1}  :
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 Δ : simplex_categoryhᵒᵖ, the canonical map splitting.map X ι Δ is an isomorphism.

Instances for simplicial_object.splitting
• simplicial_object.splitting.has_sizeof_inst
@[protected, instance]
noncomputable def simplicial_object.splitting.iso {C : Type u_1} (Δ : simplex_categoryᵒᵖ) :

The isomorphism on simplices given by the axiom splitting.map_is_iso'

Equations
noncomputable def simplicial_object.splitting.ι_summand {C : Type u_1} {Δ : simplex_categoryᵒᵖ}  :

Via the isomorphism s.iso Δ, this is the inclusion of a summand in the direct sum decomposition given by the splitting s : splitting X.

Equations
theorem simplicial_object.splitting.ι_summand_eq_assoc {C : Type u_1} {Δ : simplex_categoryᵒᵖ} {X' : C} (f' : X.obj Δ X') :
@[simp]
def simplicial_object.splitting.φ {C : Type u_1} (f : X Y) (n : ) :
s.N n Y.obj

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
@[simp]
@[simp]
theorem simplicial_object.splitting.ι_summand_comp_app_assoc {C : Type u_1} (f : X Y) {Δ : simplex_categoryᵒᵖ} {X' : C} (f' : Y.obj Δ X') :
s.ι_summand A f.app Δ f' = s.φ f (opposite.unop A.fst).len Y.map A.e.op f'
theorem simplicial_object.splitting.hom_ext' {C : Type u_1} {Z : C} {Δ : simplex_categoryᵒᵖ} (f g : X.obj Δ Z) (h : (A : , s.ι_summand A f = s.ι_summand A g) :
f = g
theorem simplicial_object.splitting.hom_ext {C : Type u_1} (f g : X Y) (h : (n : ), s.φ f n = s.φ g n) :
f = g
noncomputable def simplicial_object.splitting.desc {C : Type u_1} {Z : C} (Δ : simplex_categoryᵒᵖ) (F : Π (A : , 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
@[simp]
theorem simplicial_object.splitting.ι_desc {C : Type u_1} {Z : C} (Δ : simplex_categoryᵒᵖ) (F : Π (A : , s.N (opposite.unop A.fst).len Z)  :
s.ι_summand A s.desc Δ F = F A
@[simp]
theorem simplicial_object.splitting.ι_desc_assoc {C : Type u_1} {Z : C} (Δ : simplex_categoryᵒᵖ) (F : Π (A : , s.N (opposite.unop A.fst).len Z) {X' : C} (f' : Z X') :
s.ι_summand A s.desc Δ F f' = F A f'
def simplicial_object.splitting.of_iso {C : Type u_1} (e : X Y) :

A simplicial object that is isomorphic to a split simplicial object is split.

Equations
@[simp]
theorem simplicial_object.splitting.of_iso_N {C : Type u_1} (e : X Y) (ᾰ : ) :
(s.of_iso e).N = s.N
@[simp]
theorem simplicial_object.splitting.of_iso_ι {C : Type u_1} (e : X Y) (n : ) :
(s.of_iso e).ι n = s.ι n e.hom.app
theorem simplicial_object.splitting.ι_summand_epi_naturality {C : Type u_1} {Δ₁ Δ₂ : simplex_categoryᵒᵖ} (p : Δ₁ Δ₂)  :
theorem simplicial_object.splitting.ι_summand_epi_naturality_assoc {C : Type u_1} {Δ₁ Δ₂ : simplex_categoryᵒᵖ} (p : Δ₁ Δ₂) {X' : C} (f' : X.obj Δ₂ X') :
s.ι_summand A X.map p f' = s.ι_summand (A.epi_comp p) f'
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
@[nolint, ext]
structure simplicial_object.split (C : Type u_1)  :
Type (max u_1 u_2)
• X :
• s :

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
@[simp]
theorem simplicial_object.split.mk'_s {C : Type u_1}  :
@[simp]
theorem simplicial_object.split.mk'_X {C : Type u_1}  :

The object in simplicial_object.split C attached to a splitting s : splitting X of a simplicial object X.

Equations
• = {X := X, s := s}
@[nolint]
structure simplicial_object.split.hom {C : Type u_1} (S₁ S₂ : simplicial_object.split C) :
Type u_2

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} {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} {S₁ S₂ : simplicial_object.split C} (self : S₁.hom S₂) (n : ) :
S₁.s.ι n self.F.app = self.f n S₂.s.ι n
@[simp]
theorem simplicial_object.split.hom.comm_assoc {C : Type u_1} {S₁ S₂ : simplicial_object.split C} (self : S₁.hom S₂) (n : ) {X' : C} (f' : S₂.X.obj X') :
S₁.s.ι n self.F.app f' = self.f n S₂.s.ι n f'
@[protected, instance]
Equations
theorem simplicial_object.split.congr_F {C : Type u_1} {S₁ S₂ : simplicial_object.split C} {Φ₁ Φ₂ : S₁ S₂} (h : Φ₁ = Φ₂) :
Φ₁.F = Φ₂.F
theorem simplicial_object.split.congr_f {C : Type u_1} {S₁ S₂ : simplicial_object.split C} {Φ₁ Φ₂ : S₁ S₂} (h : Φ₁ = Φ₂) (n : ) :
Φ₁.f n = Φ₂.f n
@[simp]
theorem simplicial_object.split.id_F {C : Type u_1} (S : simplicial_object.split C) :
(𝟙 S).F = 𝟙 S.X
@[simp]
theorem simplicial_object.split.id_f {C : Type u_1} (S : simplicial_object.split C) (n : ) :
(𝟙 S).f n = 𝟙 (S.s.N n)
@[simp]
theorem simplicial_object.split.comp_F {C : Type u_1} {S₁ S₂ S₃ : simplicial_object.split C} (Φ₁₂ : S₁ S₂) (Φ₂₃ : S₂ S₃) :
(Φ₁₂ Φ₂₃).F = Φ₁₂.F Φ₂₃.F
@[simp]
theorem simplicial_object.split.comp_f {C : Type u_1} {S₁ S₂ S₃ : simplicial_object.split C} (Φ₁₂ : S₁ S₂) (Φ₂₃ : S₂ S₃) (n : ) :
(Φ₁₂ Φ₂₃).f n = Φ₁₂.f n Φ₂₃.f n
@[simp]
theorem simplicial_object.split.ι_summand_naturality_symm {C : Type u_1} {S₁ S₂ : simplicial_object.split C} (Φ : S₁ S₂) {Δ : simplex_categoryᵒᵖ}  :
S₁.s.ι_summand A Φ.F.app Δ = Φ.f (opposite.unop A.fst).len S₂.s.ι_summand A
@[simp]
theorem simplicial_object.split.ι_summand_naturality_symm_assoc {C : Type u_1} {S₁ S₂ : simplicial_object.split C} (Φ : S₁ S₂) {Δ : simplex_categoryᵒᵖ} {X' : C} (f' : S₂.X.obj Δ X') :
S₁.s.ι_summand A Φ.F.app Δ f' = Φ.f (opposite.unop A.fst).len S₂.s.ι_summand A f'
@[simp]
theorem simplicial_object.split.forget_map (C : Type u_1) (S₁ S₂ : simplicial_object.split C) (Φ : S₁ S₂) :
= Φ.F

The functor simplicial_object.split C ⥤ simplicial_object C which forgets the splitting.

Equations
@[simp]
@[simp]
theorem simplicial_object.split.eval_N_obj (C : Type u_1) (n : ) (S : simplicial_object.split C) :
= S.s.N n
@[simp]
theorem simplicial_object.split.eval_N_map (C : Type u_1) (n : ) (S₁ S₂ : simplicial_object.split C) (Φ : S₁ S₂) :
= Φ.f n
def simplicial_object.split.eval_N (C : Type u_1) (n : ) :

The functor simplicial_object.split C ⥤ C which sends a simplicial object equipped with a splitting to its nondegenerate n-simplices.

Equations

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