mathlib3 documentation


Augmented simplicial objects with an extra degeneracy #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Instances for simplicial_object.augmented.extra_degeneracy

If ed is an extra degeneracy for X : simplicial_object.augmented C and F : C ⥤ D is a functor, then F is an extra degeneracy for the augmented simplical object in D obtained by applying F to X.

def sSet.augmented.standard_simplex.shift_fun {n : } {X : Type u_1} [has_zero X] (f : fin n X) (i : fin (n + 1)) :

When [has_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.


The shift of a morphism f : [n] → Δ in simplex_category corresponds to the monotone map which sends 0 to 0 and i.succ to f.to_order_hom i.


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.