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.
• ExtraDegeneracy.homotopy: if we have an extra degeneracy ed on X : SimplicialObject.Augmented C (for any category C), then the morphism X.hom ≫ ed.section_ is homotopic to 𝟙 X.left.

References

• Paul G. Goerss, John F. Jardine, Simplicial Homotopy Theory
• M. Barr, J. Kennison, J. and R. Robert, Contractible simplicial objects

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 { len := 0 })

  a section of the augmentation in dimension 0

• s (n : ℕ) : X.left.obj (Opposite.op { len := n }) ⟶ X.left.obj (Opposite.op { len := n + 1 })

  the extra degeneracy

• s'_comp_ε : CategoryStruct.comp self.s' (X.hom.app (Opposite.op { len := 0 })) = CategoryStruct.id X.right
• s₀_comp_δ₁ : CategoryStruct.comp (self.s 0) (X.left.δ 1) = CategoryStruct.comp (X.hom.app (Opposite.op { len := 0 })) self.s'
• s_comp_δ₀ (n : ℕ) : CategoryStruct.comp (self.s n) (X.left.δ 0) = CategoryStruct.id (X.left.obj (Opposite.op { len := 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 {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.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.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 { len := 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)

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 { len := 0 }) ⟶ Z) : CategoryStruct.comp (self.s 0) (CategoryStruct.comp (X.left.δ 1) h) = CategoryStruct.comp (X.hom.app (Opposite.op { len := 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 + 1)) {Z : C} (h : X.left.obj (Opposite.op { len := 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)

@[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 { len := 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 { len := 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 { len := 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 := ⋯ }

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_σ₀Iter {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) (n : ℕ) : CategoryStruct.comp ed.s' (X.left.σ₀Iter n ⋯) = ed.section_.app (Opposite.op { len := n })

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_σ₀Iter_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) (n : ℕ) {Z : C} (h : X.left.obj (Opposite.op { len := n }) ⟶ Z) : CategoryStruct.comp ed.s' (CategoryStruct.comp (X.left.σ₀Iter n ⋯) h) = CategoryStruct.comp (ed.section_.app (Opposite.op { len := n })) h

def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) {n : ℕ} (i : Fin (n + 1)) : X.left.obj (Opposite.op { len := n }) ⟶ X.left.obj (Opposite.op { len := n + 1 })

Auxiliary definition for ExtraDegeneracy.homotopy.

Equations

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

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) {n : ℕ} (i : Fin (n + 1)) (j : ℕ) (hj : j = ↑i.rev := by grind) : h ed i = CategoryStruct.comp (X.left.δ₀Iter ↑i ⋯) (CategoryStruct.comp (ed.s j) (X.left.σ₀Iter ↑i ⋯))

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) {n : ℕ} (i : Fin (n + 1)) (j : ℕ) (hj : j = ↑i.rev := by grind) {Z : C} (h : X.left.obj (Opposite.op { len := n + 1 }) ⟶ Z) : CategoryStruct.comp (homotopy.h ed i) h = CategoryStruct.comp (X.left.δ₀Iter ↑i ⋯) (CategoryStruct.comp (ed.s j) (CategoryStruct.comp (X.left.σ₀Iter ↑i ⋯) h))

def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) : Homotopy (CategoryStruct.comp X.hom ed.section_) (CategoryStruct.id X.left)

If ed is an extradegeneracy for an augmented simplicial object X, then this is a homotopy from X.hom ≫ ed.section_ to 𝟙 X.left.

Equations

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

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy_h {C : Type u_1} [Category.{v_1, u_1} C] {X : Augmented C} (ed : X.ExtraDegeneracy) {n✝ : ℕ} (i : Fin (n✝ + 1)) : ed.homotopy.h i = homotopy.h ed i

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 : { len := n } ⟶ Δ) : { len := 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 { len := n }) ⟶ f.cechNerve.obj (Opposite.op { len := 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) (x✝ : ℕ) : (const X).s x✝ = CategoryStruct.id ((Augmented.const.obj X).left.obj (Opposite.op { len := x✝ }))

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

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.