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][goerss-jardine-2009]

structure CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy {C : Type u_1} [Category.{u_2, u_1} C] (X : Augmented C) : Type u_2

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' : point.obj X ⟶ (drop.obj X).obj (Opposite.op (SimplexCategory.mk 0))

  a section of the augmentation in dimension 0

• s (n : ℕ) : (drop.obj X).obj (Opposite.op (SimplexCategory.mk n)) ⟶ (drop.obj X).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 (point.obj X)
• 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 ((drop.obj X).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 {C : Type u_1} {inst✝ : Category.{u_2, 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.{u_2, 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.{u_2, 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)

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁_assoc {C : Type u_1} [Category.{u_2, 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.{u_2, 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)

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀_assoc {C : Type u_1} [Category.{u_2, 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.{u_2, u_1} C] {X : Augmented C} (self : X.ExtraDegeneracy) {Z : C} (h : ((SimplicialObject.const C).obj X.right).obj (Opposite.op (SimplexCategory.mk 0)) ⟶ 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.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, 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.{u_2, 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 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

@[deprecated SSet.Augmented.StandardSimplex.shiftFun_zero (since := "2025-04-19")]

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

Alias of SSet.Augmented.StandardSimplex.shiftFun_zero.

@[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.{u_2, 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.

theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0 {C : Type u_1} [Category.{u_2, 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 ((Opposite.unop (Opposite.op (SimplexCategory.mk (n + 1)))).len + 1)) => f.hom) 0) = CategoryStruct.comp (Limits.WidePullback.base fun (x : Fin (n + 1)) => f.hom) S.section_

theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ {C : Type u_1} [Category.{u_2, 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 ((Opposite.unop (Opposite.op (SimplexCategory.mk (n + 1)))).len + 1)) => f.hom) i.succ) = Limits.WidePullback.π (fun (x : Fin (n + 1)) => f.hom) i

theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base {C : Type u_1} [Category.{u_2, 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 ((Opposite.unop (Opposite.op (SimplexCategory.mk (n + 1)))).len + 1)) => f.hom) = Limits.WidePullback.base fun (x : Fin ((Opposite.unop (Opposite.op (SimplexCategory.mk n))).len + 1)) => f.hom

noncomputable def CategoryTheory.Arrow.AugmentedCechNerve.extraDegeneracy {C : Type u_1} [Category.{u_2, 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.{u_2, 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.{u_2, u_1} C] (X : C) (x✝ : ℕ) : (const X).s x✝ = CategoryStruct.id ((drop.obj (Augmented.const.obj X)).obj (Opposite.op (SimplexCategory.mk x✝)))

@[simp]

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

noncomputable def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv {C : Type u_1} [Category.{u_2, 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.