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 _ 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 Xfor 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
Cis preadditive, if we have an extra degeneracy on
X : SimplicialObject.Augmented C, then the augmentation on the alternating face map complex of
Xis a homotopy equivalence.
- [Paul G. Goerss, John F. Jardine, Simplical Homotopy Theory][goerss-jardine-2009]
- s_comp_δ : ∀ (n : ℕ) (i : Fin (n + 2)), CategoryTheory.CategoryStruct.comp (SimplicialObject.Augmented.ExtraDegeneracy.s s (n + 1)) (CategoryTheory.SimplicialObject.δ X.left (Fin.succ i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X.left i) (SimplicialObject.Augmented.ExtraDegeneracy.s s n)
- s_comp_σ : ∀ (n : ℕ) (i : Fin (n + 1)), CategoryTheory.CategoryStruct.comp (SimplicialObject.Augmented.ExtraDegeneracy.s s n) (CategoryTheory.SimplicialObject.σ X.left (Fin.succ i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X.left i) (SimplicialObject.Augmented.ExtraDegeneracy.s s (n + 1))
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 simplical object in
D obtained by applying
Y are isomorphic augmented simplicial objects, then an extra
X gives also an extra degeneracy for
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.
The augmented Čech nerve associated to a split epimorphism has an extra degeneracy.
C is a preadditive category and
X is an augmented simplicial object
C that has an extra degeneracy, then the augmentation on the alternating
face map complex of
X is a homotopy equivalence.