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 : CategoryTheory.Category.{u_2, u_1} C} {X : CategoryTheory.SimplicialObject.Augmented C} (x y : SimplicialObject.Augmented.ExtraDegeneracy X), x = y ↔ x.s' = y.s' ∧ x.s = y.s

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

structure SimplicialObject.Augmented.ExtraDegeneracy {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.SimplicialObject.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' : CategoryTheory.SimplicialObject.Augmented.point.toPrefunctor.obj X ⟶ (CategoryTheory.SimplicialObject.Augmented.drop.toPrefunctor.obj X).toPrefunctor.obj (Opposite.op (SimplexCategory.mk 0))
• s : (n : ℕ) → (CategoryTheory.SimplicialObject.Augmented.drop.toPrefunctor.obj X).toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ (CategoryTheory.SimplicialObject.Augmented.drop.toPrefunctor.obj X).toPrefunctor.obj (Opposite.op (SimplexCategory.mk (n + 1)))
• s'_comp_ε : CategoryTheory.CategoryStruct.comp self.s' (X.hom.app (Opposite.op (SimplexCategory.mk 0))) = CategoryTheory.CategoryStruct.id (CategoryTheory.SimplicialObject.Augmented.point.toPrefunctor.obj X)
• s₀_comp_δ₁ : CategoryTheory.CategoryStruct.comp (self.s 0) (CategoryTheory.SimplicialObject.δ X.left 1) = CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op (SimplexCategory.mk 0))) self.s'
• s_comp_δ₀ : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (self.s n) (CategoryTheory.SimplicialObject.δ X.left 0) = CategoryTheory.CategoryStruct.id ((CategoryTheory.SimplicialObject.Augmented.drop.toPrefunctor.obj X).toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)))
• s_comp_δ : ∀ (n : ℕ) (i : Fin (n + 2)), CategoryTheory.CategoryStruct.comp (self.s (n + 1)) (CategoryTheory.SimplicialObject.δ X.left (Fin.succ i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X.left i) (self.s n)
• s_comp_σ : ∀ (n : ℕ) (i : Fin (n + 1)), CategoryTheory.CategoryStruct.comp (self.s n) (CategoryTheory.SimplicialObject.σ X.left (Fin.succ i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X.left i) (self.s (n + 1))

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

• SSet.Augmented.StandardSimplex.shiftFun f i = if x : i = 0 then 0 else f (Fin.pred i x)

@[simp]

theorem SSet.Augmented.StandardSimplex.shiftFun_0 {n : ℕ} {X : Type u_1} [Zero X] (f : Fin n → X) : SSet.Augmented.StandardSimplex.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) : SSet.Augmented.StandardSimplex.shiftFun f (Fin.succ i) = 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

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

noncomputable def SSet.Augmented.StandardSimplex.extraDegeneracy (Δ : SimplexCategory) : SimplicialObject.Augmented.ExtraDegeneracy (SSet.Augmented.standardSimplex.toPrefunctor.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_standardSimplex (Δ : SimplexCategory) : Nonempty (SimplicialObject.Augmented.ExtraDegeneracy (SSet.Augmented.standardSimplex.toPrefunctor.obj Δ))

Equations

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

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

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

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

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

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.

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