# 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]
theorem SimplicialObject.Augmented.ExtraDegeneracy.ext_iff {C : Type u_1} :
∀ {inst : } {X : } (x y : ), x = y x.s' = y.s' x.s = y.s
theorem SimplicialObject.Augmented.ExtraDegeneracy.ext {C : Type u_1} :
∀ {inst : } {X : } (x y : ), x.s' = y.s'x.s = y.sx = y

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
@[simp]
theorem SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε {C : Type u_1} [] :
CategoryTheory.CategoryStruct.comp self.s' (X.hom.app { unop := }) = CategoryTheory.CategoryStruct.id (CategoryTheory.SimplicialObject.Augmented.point.obj X)
@[simp]
theorem SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀ {C : Type u_1} [] (n : ) :
CategoryTheory.CategoryStruct.comp (self.s n) (X.left 0) = CategoryTheory.CategoryStruct.id ((CategoryTheory.SimplicialObject.Augmented.drop.obj X).obj { unop := })
theorem SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ {C : Type u_1} [] (n : ) (i : Fin (n + 2)) :
CategoryTheory.CategoryStruct.comp (self.s (n + 1)) (X.left i.succ) = CategoryTheory.CategoryStruct.comp (X.left i) (self.s n)
theorem SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ {C : Type u_1} [] (n : ) (i : Fin (n + 1)) :
CategoryTheory.CategoryStruct.comp (self.s n) (X.left i.succ) = CategoryTheory.CategoryStruct.comp (X.left i) (self.s (n + 1))
theorem SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁_assoc {C : Type u_1} [] {Z : C} (h : X.left.obj { unop := } Z) :
theorem SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ_assoc {C : Type u_1} [] (n : ) (i : Fin (n + 1)) {Z : C} (h : X.left.obj { unop := SimplexCategory.mk (n + 1 + 1) } Z) :
theorem SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ_assoc {C : Type u_1} [] (n : ) (i : Fin (n + 2)) {Z : C} (h : X.left.obj { unop := SimplexCategory.mk (n + 1) } Z) :
@[simp]
theorem SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀_assoc {C : Type u_1} [] (n : ) {Z : C} (h : X.left.obj { unop := } Z) :
@[simp]
theorem SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε_assoc {C : Type u_1} [] {Z : C} (h : ( X.right).obj { unop := } Z) :
def SimplicialObject.Augmented.ExtraDegeneracy.map {C : Type u_1} [] {D : Type u_2} [] (F : ) :

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_σ := }
Instances For

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.
Instances For
def SSet.Augmented.StandardSimplex.shiftFun {n : } {X : Type u_1} [Zero X] (f : Fin nX) (i : Fin (n + 1)) :
X

When [HasZero 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
• = if x : i = 0 then 0 else f (i.pred x)
Instances For
@[simp]
theorem SSet.Augmented.StandardSimplex.shiftFun_0 {n : } {X : Type u_1} [Zero X] (f : Fin nX) :
@[simp]
theorem SSet.Augmented.StandardSimplex.shiftFun_succ {n : } {X : Type u_1} [Zero X] (f : Fin nX) (i : Fin n) :
= f i

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
Instances For

The obvious extra degeneracy on the standard simplex.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
noncomputable def CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s {C : Type u_1} [] (f : ) [∀ (n : ), CategoryTheory.Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : ) (n : ) :
f.cechNerve.obj { unop := } f.cechNerve.obj { unop := 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.
Instances For
theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0 {C : Type u_1} [] (f : ) [∀ (n : ), CategoryTheory.Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : ) (n : ) :
theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ {C : Type u_1} [] (f : ) [∀ (n : ), CategoryTheory.Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : ) (n : ) (i : Fin (n + 1)) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun (x : Fin ({ unop := SimplexCategory.mk (n + 1) }.unop.len + 1)) => f.hom) i.succ) = CategoryTheory.Limits.WidePullback.π (fun (x : Fin (n + 1)) => f.hom) i
theorem CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base {C : Type u_1} [] (f : ) [∀ (n : ), CategoryTheory.Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : ) (n : ) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun (x : Fin ({ unop := SimplexCategory.mk (n + 1) }.unop.len + 1)) => f.hom) = CategoryTheory.Limits.WidePullback.base fun (x : Fin ({ unop := }.unop.len + 1)) => f.hom
noncomputable def CategoryTheory.Arrow.AugmentedCechNerve.extraDegeneracy {C : Type u_1} [] (f : ) [∀ (n : ), CategoryTheory.Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (S : ) :

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.
Instances For
noncomputable def SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv {C : Type u_1} [] :
HomotopyEquiv (AlgebraicTopology.AlternatingFaceMapComplex.obj (CategoryTheory.SimplicialObject.Augmented.drop.obj X)) (.obj (CategoryTheory.SimplicialObject.Augmented.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.
Instances For