Augmented simplicial objects with an extra degeneracy

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 ExtraDegeneracy X for any X : SimplicialObject.Augmented C
• ExtraDegeneracy.map: extra degeneracies are preserved by the application of any functor C ⥤ D
• SSet.Augmented.StandardSimplex.extraDegeneracy: the standard n-simplex has an extra degeneracy
• Arrow.AugmentedCechNerve.extraDegeneracy: the Čech nerve of a split epimorphism has an extra degeneracy
• ExtraDegeneracy.homotopyEquiv: in the case the category C is preadditive, if we have an extra degeneracy on X : SimplicialObject.Augmented C, then the augmentation on the alternating face map complex of X is a homotopy equivalence.

References

• Paul G. Goerss, John F. Jardine, Simplicial Homotopy Theory

structure CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy {C : Type u_1} [Category.{v_1, u_1} C] (X : Augmented C) : Type v_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).

• s' : X.right ⟶ X.left.obj (Opposite.op (SimplexCategory.mk 0))

  a section of the augmentation in dimension 0

• s (n : ℕ) : X.left.obj (Opposite.op (SimplexCategory.mk n)) ⟶ X.left.obj (Opposite.op (SimplexCategory.mk (n + 1)))

  the extra degeneracy

• s'_comp_ε : CategoryStruct.comp self.s' (X.hom.app (Opposite.op (SimplexCategory.mk 0))) = CategoryStruct.id X.right
• s₀_comp_δ₁ : CategoryStruct.comp (self.s 0) (X.left.δ 1) = CategoryStruct.comp (X.hom.app (Opposite.op (SimplexCategory.mk 0))) self.s'
• s_comp_δ₀ (n : ℕ) : CategoryStruct.comp (self.s n) (X.left.δ 0) = CategoryStruct.id (X.left.obj (Opposite.op (SimplexCategory.mk n)))
• s_comp_δ (n : ℕ) (i : Fin (n + 2)) : CategoryStruct.comp (self.s (n + 1)) (X.left.δ i.succ) = CategoryStruct.comp (X.left.δ i) (self.s n)
• s_comp_σ (n : ℕ) (i : Fin (n + 1)) : CategoryStruct.comp (self.s n) (X.left.σ i.succ) = CategoryStruct.comp (X.left.σ i) (self.s (n + 1))

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.ext_iff {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {X : Augmented C} {x y : X.ExtraDegeneracy} : x = y ↔ x.s' = y.s' ∧ x.s = y.s

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.ext {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {X : Augmented C} {x y : X.ExtraDegeneracy} (s' : x.s' = y.s') (s : x.s = y.s) : x = y

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (self : X.ExtraDegeneracy) (n : ℕ) (i : Fin (n + 1)) {Z : C} (h : X.left.obj (Opposite.op (SimplexCategory.mk (n + 1 + 1))) ⟶ Z) : CategoryStruct.comp (self.s n) (CategoryStruct.comp (X.left.σ i.succ) h) = CategoryStruct.comp (X.left.σ i) (CategoryStruct.comp (self.s (n + 1)) h)

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (self : X.ExtraDegeneracy) {Z : C} (h : X.left.obj (Opposite.op (SimplexCategory.mk 0)) ⟶ Z) : CategoryStruct.comp (self.s 0) (CategoryStruct.comp (X.left.δ 1) h) = CategoryStruct.comp (X.hom.app (Opposite.op (SimplexCategory.mk 0))) (CategoryStruct.comp self.s' h)

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (self : X.ExtraDegeneracy) (n : ℕ) (i : Fin (n + 2)) {Z : C} (h : X.left.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ Z) : CategoryStruct.comp (self.s (n + 1)) (CategoryStruct.comp (X.left.δ i.succ) h) = CategoryStruct.comp (X.left.δ i) (CategoryStruct.comp (self.s n) h)

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (self : X.ExtraDegeneracy) (n : ℕ) {Z : C} (h : X.left.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryStruct.comp (self.s n) (CategoryStruct.comp (X.left.δ 0) h) = h

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (self : X.ExtraDegeneracy) {Z : C} (h : X.right ⟶ Z) : CategoryStruct.comp self.s' (CategoryStruct.comp (X.hom.app (Opposite.op (SimplexCategory.mk 0))) h) = h

def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {X : Augmented C} (ed : X.ExtraDegeneracy) (F : Functor C D) : (((whiskering C D).obj F).obj X).ExtraDegeneracy

If ed is an extra degeneracy for X : SimplicialObject.Augmented C and F : C ⥤ D is a functor, then ed.map F is an extra degeneracy for the augmented simplicial object in D obtained by applying F to X.

Equations

• ed.map F = { s' := F.map ed.s', s := fun (n : ℕ) => F.map (ed.s n), s'_comp_ε := ⋯, s₀_comp_δ₁ := ⋯, s_comp_δ₀ := ⋯, s_comp_δ := ⋯, s_comp_σ := ⋯ }

def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.ofIso {C : Type u_1} [Category.{v_1, u_1} C] {X Y : Augmented C} (e : X ≅ Y) (ed : X.ExtraDegeneracy) : Y.ExtraDegeneracy

If X and Y are isomorphic augmented simplicial objects, then an extra degeneracy for X gives also an extra degeneracy for Y

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_ {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) : (SimplicialObject.const C).obj X.right ⟶ X.left

The section of the augmentation that is induced by the extradegeneracy.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_app_op_mk_zero {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) : ed.section_.app (Opposite.op (SimplexCategory.mk 0)) = ed.s'

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_app_comp_hom_app {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) (n : SimplexCategoryᵒᵖ) : CategoryStruct.comp (ed.section_.app n) (X.hom.app n) = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_app_comp_hom_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) (n : SimplexCategoryᵒᵖ) {Z : C} (h : X.right ⟶ Z) : CategoryStruct.comp (ed.section_.app n) (CategoryStruct.comp (X.hom.app n) h) = h

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_comp_hom {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) : CategoryStruct.comp ed.section_ X.hom = CategoryStruct.id ((SimplicialObject.const C).obj X.right)

def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.splitEpi {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) : SplitEpi X.hom

If an augmented simplicial object has an extradegeneracy, then then augmentation is a split epimorphism.

Equations

• ed.splitEpi = { section_ := ed.section_, id := ⋯ }

def SSet.Augmented.StandardSimplex.shiftFun {n : ℕ} {X : Type u_1} [Zero X] (f : Fin n → X) (i : Fin (n + 1)) : X

When [Zero X], the shift of a map f : Fin n → X is a map Fin (n + 1) → X which sends 0 to 0 and i.succ to f i.

Equations

• SSet.Augmented.StandardSimplex.shiftFun f i = Matrix.vecCons 0 f i

@[simp]

theorem SSet.Augmented.StandardSimplex.shiftFun_zero {n : ℕ} {X : Type u_1} [Zero X] (f : Fin n → X) : shiftFun f 0 = 0

@[simp]

theorem SSet.Augmented.StandardSimplex.shiftFun_succ {n : ℕ} {X : Type u_1} [Zero X] (f : Fin n → X) (i : Fin n) : shiftFun f i.succ = f i

def SSet.Augmented.StandardSimplex.shift {n : ℕ} {Δ : SimplexCategory} (f : SimplexCategory.mk n ⟶ Δ) : SimplexCategory.mk (n + 1) ⟶ Δ

The shift of a morphism f : ⦋n⦌ → Δ in SimplexCategory corresponds to the monotone map which sends 0 to 0 and i.succ to f.toOrderHom i.

Equations

• SSet.Augmented.StandardSimplex.shift f = SimplexCategory.Hom.mk { toFun := SSet.Augmented.StandardSimplex.shiftFun ⇑(SimplexCategory.Hom.toOrderHom f), monotone' := ⋯ }

noncomputable def SSet.Augmented.StandardSimplex.extraDegeneracy (Δ : SimplexCategory) : CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy (stdSimplex.obj Δ)

The obvious extra degeneracy on the standard simplex.

Equations

• One or more equations did not get rendered due to their size.

instance SSet.Augmented.StandardSimplex.nonempty_extraDegeneracy_stdSimplex (Δ : SimplexCategory) : Nonempty (CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy (stdSimplex.obj Δ))

noncomputable def CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s {C : Type u_1} [Category.{v_1, u_1} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : SplitEpi f.hom) (n : ℕ) : f.cechNerve.obj (Opposite.op (SimplexCategory.mk n)) ⟶ f.cechNerve.obj (Opposite.op (SimplexCategory.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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0 {C : Type u_1} [Category.{v_1, u_1} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : SplitEpi f.hom) (n : ℕ) : CategoryStruct.comp (s f S n) (Limits.WidePullback.π (fun (x : Fin (n + 1 + 1)) => f.hom) 0) = CategoryStruct.comp (Limits.WidePullback.base fun (x : Fin (n + 1)) => f.hom) S.section_

@[simp]

theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0_assoc {C : Type u_1} [Category.{v_1, u_1} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : SplitEpi f.hom) (n : ℕ) {Z : C} (h : f.left ⟶ Z) : CategoryStruct.comp (s f S n) (CategoryStruct.comp (Limits.WidePullback.π (fun (x : Fin (n + 1 + 1)) => f.hom) 0) h) = CategoryStruct.comp (Limits.WidePullback.base fun (x : Fin (n + 1)) => f.hom) (CategoryStruct.comp S.section_ h)

@[simp]

theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ {C : Type u_1} [Category.{v_1, u_1} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : SplitEpi f.hom) (n : ℕ) (i : Fin (n + 1)) : CategoryStruct.comp (s f S n) (Limits.WidePullback.π (fun (x : Fin (n + 1 + 1)) => f.hom) i.succ) = Limits.WidePullback.π (fun (x : Fin (n + 1)) => f.hom) i

@[simp]

theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ_assoc {C : Type u_1} [Category.{v_1, u_1} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : SplitEpi f.hom) (n : ℕ) (i : Fin (n + 1)) {Z : C} (h : f.left ⟶ Z) : CategoryStruct.comp (s f S n) (CategoryStruct.comp (Limits.WidePullback.π (fun (x : Fin (n + 1 + 1)) => f.hom) i.succ) h) = CategoryStruct.comp (Limits.WidePullback.π (fun (x : Fin (n + 1)) => f.hom) i) h

@[simp]

theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base {C : Type u_1} [Category.{v_1, u_1} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : SplitEpi f.hom) (n : ℕ) : CategoryStruct.comp (s f S n) (Limits.WidePullback.base fun (x : Fin (n + 1 + 1)) => f.hom) = Limits.WidePullback.base fun (x : Fin (n + 1)) => f.hom

@[simp]

theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base_assoc {C : Type u_1} [Category.{v_1, u_1} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : SplitEpi f.hom) (n : ℕ) {Z : C} (h : f.right ⟶ Z) : CategoryStruct.comp (s f S n) (CategoryStruct.comp (Limits.WidePullback.base fun (x : Fin (n + 1 + 1)) => f.hom) h) = CategoryStruct.comp (Limits.WidePullback.base fun (x : Fin (n + 1)) => f.hom) h

noncomputable def CategoryTheory.Arrow.AugmentedCechNerve.extraDegeneracy {C : Type u_1} [Category.{v_1, u_1} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : SplitEpi f.hom) : f.augmentedCechNerve.ExtraDegeneracy

The augmented Čech nerve associated to a split epimorphism has an extra degeneracy.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const {C : Type u_1} [Category.{v_1, u_1} C] (X : C) : (Augmented.const.obj X).ExtraDegeneracy

The constant augmented simplicial object has an extra degeneracy.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const_s' {C : Type u_1} [Category.{v_1, u_1} C] (X : C) : (const X).s' = CategoryStruct.id (Augmented.const.obj X).right

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const_s {C : Type u_1} [Category.{v_1, u_1} C] (X : C) (x✝ : ℕ) : (const X).s x✝ = CategoryStruct.id ((Augmented.const.obj X).left.obj (Opposite.op (SimplexCategory.mk x✝)))

noncomputable def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasZeroObject C] {X : Augmented C} (ed : X.ExtraDegeneracy) : HomotopyEquiv (AlgebraicTopology.AlternatingFaceMapComplex.obj (drop.obj X)) ((ChainComplex.single₀ C).obj (point.obj 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 a homotopy equivalence.

Equations

• One or more equations did not get rendered due to their size.