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

Instances For

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

          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
              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 : ) :
              f.cechNerve.obj (Opposite.op (SimplexCategory.mk n)) f.cechNerve.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.
              Instances For
                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) :

                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

                  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