Augmented simplicial objects with an extra degeneracy #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In simplicial homotopy theory, in order to prove that the connected components
of a simplicial set X are contractible, it suffices to construct an extra
degeneracy as it is defined in Simplicial Homotopy Theory by Goerss-Jardine p. 190.
It consists of a series of maps π₀ X → X _[0] and X _[n] → X _[n+1] which
behave formally like an extra degeneracy σ (-1). It can be thought as a datum
associated to the augmented simplicial set X → π₀ X.
In this file, we adapt this definition to the case of augmented simplicial objects in any category.
Main definitions #
- the structure
extra_degeneracy Xfor anyX : simplicial_object.augmented C extra_degeneracy.map: extra degeneracies are preserved by the application of any functorC ⥤ DsSet.augmented.standard_simplex.extra_degeneracy: the standardn-simplex has an extra degeneracyarrow.augmented_cech_nerve.extra_degeneracy: the Čech nerve of a split epimorphism has an extra degeneracyextra_degeneracy.homotopy_equiv: in the case the categoryCis preadditive, if we have an extra degeneracy onX : simplicial_object.augmented C, then the augmentation on the alternating face map complex ofXis a homotopy equivalence.
References #
theorem
simplicial_object.augmented.extra_degeneracy.ext_iff
{C : Type u_1}
{_inst_1 : category_theory.category C}
{X : category_theory.simplicial_object.augmented C}
(x y : simplicial_object.augmented.extra_degeneracy X) :
@[ext]
structure
simplicial_object.augmented.extra_degeneracy
{C : Type u_1}
[category_theory.category C]
(X : category_theory.simplicial_object.augmented C) :
Type u_2
- s' : category_theory.simplicial_object.augmented.point.obj X ⟶ (category_theory.simplicial_object.augmented.drop.obj X).obj (opposite.op (simplex_category.mk 0))
- s : Π (n : ℕ), (category_theory.simplicial_object.augmented.drop.obj X).obj (opposite.op (simplex_category.mk n)) ⟶ (category_theory.simplicial_object.augmented.drop.obj X).obj (opposite.op (simplex_category.mk (n + 1)))
- s'_comp_ε' : self.s' ≫ X.hom.app (opposite.op (simplex_category.mk 0)) = 𝟙 (category_theory.simplicial_object.augmented.point.obj X)
- s₀_comp_δ₁' : self.s 0 ≫ (category_theory.simplicial_object.augmented.drop.obj X).δ 1 = X.hom.app (opposite.op (simplex_category.mk 0)) ≫ self.s'
- s_comp_δ₀' : ∀ (n : ℕ), self.s n ≫ (category_theory.simplicial_object.augmented.drop.obj X).δ 0 = 𝟙 ((category_theory.simplicial_object.augmented.drop.obj X).obj (opposite.op (simplex_category.mk n)))
- s_comp_δ' : ∀ (n : ℕ) (i : fin (n + 2)), self.s (n + 1) ≫ (category_theory.simplicial_object.augmented.drop.obj X).δ i.succ = (category_theory.simplicial_object.augmented.drop.obj X).δ i ≫ self.s n
- s_comp_σ' : ∀ (n : ℕ) (i : fin (n + 1)), self.s n ≫ (category_theory.simplicial_object.augmented.drop.obj X).σ i.succ = (category_theory.simplicial_object.augmented.drop.obj X).σ i ≫ self.s (n + 1)
The datum of an extra degeneracy is a technical condition on
augmented simplicial objects. The morphisms s' and s n of the
structure formally behave like extra degeneracies σ (-1).
Instances for simplicial_object.augmented.extra_degeneracy
- simplicial_object.augmented.extra_degeneracy.has_sizeof_inst
- sSet.augmented.standard_simplex.nonempty_extra_degeneracy_standard_simplex
theorem
simplicial_object.augmented.extra_degeneracy.ext
{C : Type u_1}
{_inst_1 : category_theory.category C}
{X : category_theory.simplicial_object.augmented C}
(x y : simplicial_object.augmented.extra_degeneracy X)
(h : x.s' = y.s')
(h_1 : x.s = y.s) :
x = y
@[simp]
theorem
simplicial_object.augmented.extra_degeneracy.s'_comp_ε
{C : Type u_1}
[category_theory.category C]
{X : category_theory.simplicial_object.augmented C}
(self : simplicial_object.augmented.extra_degeneracy X) :
self.s' ≫ X.hom.app (opposite.op (simplex_category.mk 0)) = 𝟙 X.right
theorem
simplicial_object.augmented.extra_degeneracy.s₀_comp_δ₁
{C : Type u_1}
[category_theory.category C]
{X : category_theory.simplicial_object.augmented C}
(self : simplicial_object.augmented.extra_degeneracy X) :
@[simp]
theorem
simplicial_object.augmented.extra_degeneracy.s_comp_δ₀
{C : Type u_1}
[category_theory.category C]
{X : category_theory.simplicial_object.augmented C}
(self : simplicial_object.augmented.extra_degeneracy X)
(n : ℕ) :
self.s n ≫ X.left.δ 0 = 𝟙 (X.left.obj (opposite.op (simplex_category.mk n)))
theorem
simplicial_object.augmented.extra_degeneracy.s_comp_δ
{C : Type u_1}
[category_theory.category C]
{X : category_theory.simplicial_object.augmented C}
(self : simplicial_object.augmented.extra_degeneracy X)
(n : ℕ)
(i : fin (n + 2)) :
theorem
simplicial_object.augmented.extra_degeneracy.s_comp_σ
{C : Type u_1}
[category_theory.category C]
{X : category_theory.simplicial_object.augmented C}
(self : simplicial_object.augmented.extra_degeneracy X)
(n : ℕ)
(i : fin (n + 1)) :
theorem
simplicial_object.augmented.extra_degeneracy.s_comp_δ₀_assoc
{C : Type u_1}
[category_theory.category C]
{X : category_theory.simplicial_object.augmented C}
(self : simplicial_object.augmented.extra_degeneracy X)
(n : ℕ)
{X' : C}
(f' : X.left.obj (opposite.op (simplex_category.mk n)) ⟶ X') :
theorem
simplicial_object.augmented.extra_degeneracy.s'_comp_ε_assoc
{C : Type u_1}
[category_theory.category C]
{X : category_theory.simplicial_object.augmented C}
(self : simplicial_object.augmented.extra_degeneracy X)
{X' : C}
(f' : X.right ⟶ X') :
self.s' ≫ X.hom.app (opposite.op (simplex_category.mk 0)) ≫ f' = f'
theorem
simplicial_object.augmented.extra_degeneracy.s₀_comp_δ₁_assoc
{C : Type u_1}
[category_theory.category C]
{X : category_theory.simplicial_object.augmented C}
(self : simplicial_object.augmented.extra_degeneracy X)
{X' : C}
(f' : X.left.obj (opposite.op (simplex_category.mk 0)) ⟶ X') :
theorem
simplicial_object.augmented.extra_degeneracy.s_comp_δ_assoc
{C : Type u_1}
[category_theory.category C]
{X : category_theory.simplicial_object.augmented C}
(self : simplicial_object.augmented.extra_degeneracy X)
(n : ℕ)
(i : fin (n + 2))
{X' : C}
(f' : X.left.obj (opposite.op (simplex_category.mk (n + 1))) ⟶ X') :
theorem
simplicial_object.augmented.extra_degeneracy.s_comp_σ_assoc
{C : Type u_1}
[category_theory.category C]
{X : category_theory.simplicial_object.augmented C}
(self : simplicial_object.augmented.extra_degeneracy X)
(n : ℕ)
(i : fin (n + 1))
{X' : C}
(f' : X.left.obj (opposite.op (simplex_category.mk (n + 1 + 1))) ⟶ X') :
def
simplicial_object.augmented.extra_degeneracy.map
{C : Type u_1}
[category_theory.category C]
{D : Type u_3}
[category_theory.category D]
{X : category_theory.simplicial_object.augmented C}
(ed : simplicial_object.augmented.extra_degeneracy X)
(F : C ⥤ D) :
If ed is an extra degeneracy for X : simplicial_object.augmented C and
F : C ⥤ D is a functor, then ed.map F is an extra degeneracy for the
augmented simplical object in D obtained by applying F to X.
Equations
- ed.map F = {s' := F.map ed.s', s := λ (n : ℕ), F.map (ed.s n), s'_comp_ε' := _, s₀_comp_δ₁' := _, s_comp_δ₀' := _, s_comp_δ' := _, s_comp_σ' := _}
def
simplicial_object.augmented.extra_degeneracy.of_iso
{C : Type u_1}
[category_theory.category C]
{X Y : category_theory.simplicial_object.augmented C}
(e : X ≅ Y)
(ed : simplicial_object.augmented.extra_degeneracy X) :
If X and Y are isomorphic augmented simplicial objects, then an extra
degeneracy for X gives also an extra degeneracy for Y
Equations
- simplicial_object.augmented.extra_degeneracy.of_iso e ed = {s' := (category_theory.simplicial_object.augmented.point.map_iso e).inv ≫ ed.s' ≫ (category_theory.simplicial_object.augmented.drop.map_iso e).hom.app (opposite.op (simplex_category.mk 0)), s := λ (n : ℕ), (category_theory.simplicial_object.augmented.drop.map_iso e).inv.app (opposite.op (simplex_category.mk n)) ≫ ed.s n ≫ (category_theory.simplicial_object.augmented.drop.map_iso e).hom.app (opposite.op (simplex_category.mk (n + 1))), s'_comp_ε' := _, s₀_comp_δ₁' := _, s_comp_δ₀' := _, s_comp_δ' := _, s_comp_σ' := _}
@[simp]
def
sSet.augmented.standard_simplex.shift
{n : ℕ}
{Δ : simplex_category}
(f : simplex_category.mk n ⟶ Δ) :
simplex_category.mk (n + 1) ⟶ Δ
The shift of a morphism f : [n] → Δ in simplex_category corresponds to
the monotone map which sends 0 to 0 and i.succ to f.to_order_hom i.
@[protected]
The obvious extra degeneracy on the standard simplex.
Equations
- sSet.augmented.standard_simplex.extra_degeneracy Δ = {s' := λ (x : category_theory.simplicial_object.augmented.point.obj (sSet.augmented.standard_simplex.obj Δ)), simplex_category.hom.mk (⇑(order_hom.const (fin ((opposite.unop (opposite.op (simplex_category.mk 0))).len + 1))) 0), s := λ (n : ℕ) (f : (category_theory.simplicial_object.augmented.drop.obj (sSet.augmented.standard_simplex.obj Δ)).obj (opposite.op (simplex_category.mk n))), sSet.augmented.standard_simplex.shift f, s'_comp_ε' := _, s₀_comp_δ₁' := _, s_comp_δ₀' := _, s_comp_δ' := _, s_comp_σ' := _}
@[protected, instance]
noncomputable
def
category_theory.arrow.augmented_cech_nerve.extra_degeneracy.s
{C : Type u_1}
[category_theory.category C]
(f : category_theory.arrow C)
[∀ (n : ℕ), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(S : category_theory.split_epi f.hom)
(n : ℕ) :
f.cech_nerve.obj (opposite.op (simplex_category.mk n)) ⟶ f.cech_nerve.obj (opposite.op (simplex_category.mk (n + 1)))
The extra degeneracy map on the Čech nerve of a split epi. It is
given on the 0-projection by the given section of the split epi,
and by shifting the indices on the other projections.
Equations
- category_theory.arrow.augmented_cech_nerve.extra_degeneracy.s f S n = category_theory.limits.wide_pullback.lift (category_theory.limits.wide_pullback.base (λ (i : fin ((opposite.unop (opposite.op (simplex_category.mk n))).len + 1)), f.hom)) (λ (i : fin ((opposite.unop (opposite.op (simplex_category.mk (n + 1)))).len + 1)), dite (i = 0) (λ (h : i = 0), category_theory.limits.wide_pullback.base (λ (i : fin ((opposite.unop (opposite.op (simplex_category.mk n))).len + 1)), f.hom) ≫ S.section_) (λ (h : ¬i = 0), category_theory.limits.wide_pullback.π (λ (i : fin ((opposite.unop (opposite.op (simplex_category.mk n))).len + 1)), f.hom) (i.pred h))) _
@[simp]
theorem
category_theory.arrow.augmented_cech_nerve.extra_degeneracy.s_comp_π_0
{C : Type u_1}
[category_theory.category C]
(f : category_theory.arrow C)
[∀ (n : ℕ), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(S : category_theory.split_epi f.hom)
(n : ℕ) :
category_theory.arrow.augmented_cech_nerve.extra_degeneracy.s f S n ≫ category_theory.limits.wide_pullback.π (λ (i : fin ((opposite.unop (opposite.op (simplex_category.mk (n + 1)))).len + 1)), f.hom) 0 = category_theory.limits.wide_pullback.base (λ (i : fin ((opposite.unop (opposite.op (simplex_category.mk n))).len + 1)), f.hom) ≫ S.section_
@[simp]
theorem
category_theory.arrow.augmented_cech_nerve.extra_degeneracy.s_comp_π_succ
{C : Type u_1}
[category_theory.category C]
(f : category_theory.arrow C)
[∀ (n : ℕ), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(S : category_theory.split_epi f.hom)
(n : ℕ)
(i : fin (n + 1)) :
category_theory.arrow.augmented_cech_nerve.extra_degeneracy.s f S n ≫ category_theory.limits.wide_pullback.π (λ (i : fin ((opposite.unop (opposite.op (simplex_category.mk (n + 1)))).len + 1)), f.hom) i.succ = category_theory.limits.wide_pullback.π (λ (i : fin ((opposite.unop (opposite.op (simplex_category.mk n))).len + 1)), f.hom) i
@[simp]
theorem
category_theory.arrow.augmented_cech_nerve.extra_degeneracy.s_comp_base
{C : Type u_1}
[category_theory.category C]
(f : category_theory.arrow C)
[∀ (n : ℕ), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(S : category_theory.split_epi f.hom)
(n : ℕ) :
category_theory.arrow.augmented_cech_nerve.extra_degeneracy.s f S n ≫ category_theory.limits.wide_pullback.base (λ (i : fin ((opposite.unop (opposite.op (simplex_category.mk (n + 1)))).len + 1)), f.hom) = category_theory.limits.wide_pullback.base (λ (i : fin ((opposite.unop (opposite.op (simplex_category.mk n))).len + 1)), f.hom)
noncomputable
def
category_theory.arrow.augmented_cech_nerve.extra_degeneracy
{C : Type u_1}
[category_theory.category C]
(f : category_theory.arrow C)
[∀ (n : ℕ), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(S : category_theory.split_epi f.hom) :
The augmented Čech nerve associated to a split epimorphism has an extra degeneracy.
Equations
- category_theory.arrow.augmented_cech_nerve.extra_degeneracy f S = {s' := S.section_ ≫ category_theory.limits.wide_pullback.lift f.hom (λ (i : fin ((opposite.unop (opposite.op (simplex_category.mk 0))).len + 1)), 𝟙 ((𝟭 C).obj f.left)) _, s := λ (n : ℕ), category_theory.arrow.augmented_cech_nerve.extra_degeneracy.s f S n, s'_comp_ε' := _, s₀_comp_δ₁' := _, s_comp_δ₀' := _, s_comp_δ' := _, s_comp_σ' := _}
noncomputable
def
simplicial_object.augmented.extra_degeneracy.homotopy_equiv
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
{X : category_theory.simplicial_object.augmented C}
(ed : simplicial_object.augmented.extra_degeneracy X) :
If C is a preadditive category and X is an augmented simplicial object
in C that has an extra degeneracy, then the augmentation on the alternating
face map complex of X is an homotopy equivalence.
Equations
- ed.homotopy_equiv = {hom := algebraic_topology.alternating_face_map_complex.ε.app X, inv := ((algebraic_topology.alternating_face_map_complex.obj (category_theory.simplicial_object.augmented.drop.obj X)).from_single₀_equiv (category_theory.simplicial_object.augmented.point.obj X)).inv_fun ed.s', homotopy_hom_inv_id := {hom := λ (i j : ℕ), dite (i + 1 = j) (λ (h : i + 1 = j), (-ed.s i) ≫ category_theory.eq_to_hom _) (λ (h : ¬i + 1 = j), 0), zero' := _, comm := _}, homotopy_inv_hom_id := homotopy.of_eq _}