Documentation

Mathlib.AlgebraicTopology.ExtraDegeneracy

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 #

References #

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).

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

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

The obvious extra degeneracy on the standard simplex.

Equations
  • One or more equations did not get rendered due to their size.
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 : ) :

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_π_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

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.

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.