mathlib3 documentation

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

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

Equations

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

Equations
Instances for simplicial_object.splitting.index_set.e
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₂

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

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

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
@[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]

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]

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

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
@[simp]

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

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

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

Equations
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]

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

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

Equations
@[nolint]

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 : ) :
S₁.s.ι n self.F.app (opposite.op (simplex_category.mk n)) = self.f n S₂.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') :
S₁.s.ι n self.F.app (opposite.op (simplex_category.mk n)) f' = self.f n S₂.s.ι n f'
@[protected, instance]
Equations
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 : Φ₁ = Φ₂) :
Φ₁.F = Φ₂.F
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 : ) :
Φ₁.f n = Φ₂.f 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₃) :
(Φ₁₂ Φ₂₃).F = Φ₁₂.F Φ₂₃.F
@[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 : ) :
(Φ₁₂ Φ₂₃).f n = Φ₁₂.f n Φ₂₃.f n

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

Equations

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

Equations