Documentation

Mathlib.AlgebraicTopology.SimplicialObject

Simplicial objects in a category. #

A simplicial object in a category C is a C-valued presheaf on SimplexCategory. (Similarly a cosimplicial object is functor SimplexCategory ⥤ C.)

Use the notation X _[n] in the Simplicial locale to obtain the n-th term of a (co)simplicial object X, where n is a natural number.

The category of simplicial objects valued in a category C. This is the category of contravariant functors from SimplexCategory to C.

Equations
Instances For

    X _[n] denotes the nth-term of the simplicial object X

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

      Pretty printer defined by notation3 command.

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

        Face maps for a simplicial object.

        Equations
        Instances For

          Degeneracy maps for a simplicial object.

          Equations
          Instances For

            Isomorphisms from identities in ℕ.

            Equations
            Instances For

              The skeleton functor from simplicial objects to truncated simplicial objects.

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.SimplicialObject.Augmented.toArrow_obj_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) :
                (CategoryTheory.SimplicialObject.Augmented.toArrow.obj X).hom = X.hom.app (Opposite.op (SimplexCategory.mk 0))
                @[simp]
                theorem CategoryTheory.SimplicialObject.Augmented.toArrow_map_right {C : Type u} [CategoryTheory.Category.{v, u} C] :
                ∀ {X Y : CategoryTheory.SimplicialObject.Augmented C} (η : X Y), (CategoryTheory.SimplicialObject.Augmented.toArrow.map η).right = CategoryTheory.SimplicialObject.Augmented.point.map η
                @[simp]
                theorem CategoryTheory.SimplicialObject.Augmented.toArrow_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) :
                (CategoryTheory.SimplicialObject.Augmented.toArrow.obj X).left = (CategoryTheory.SimplicialObject.Augmented.drop.obj X).obj (Opposite.op (SimplexCategory.mk 0))
                @[simp]
                theorem CategoryTheory.SimplicialObject.Augmented.toArrow_obj_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) :
                (CategoryTheory.SimplicialObject.Augmented.toArrow.obj X).right = CategoryTheory.SimplicialObject.Augmented.point.obj X
                @[simp]
                theorem CategoryTheory.SimplicialObject.Augmented.toArrow_map_left {C : Type u} [CategoryTheory.Category.{v, u} C] :
                ∀ {X Y : CategoryTheory.SimplicialObject.Augmented C} (η : X Y), (CategoryTheory.SimplicialObject.Augmented.toArrow.map η).left = (CategoryTheory.SimplicialObject.Augmented.drop.map η).app (Opposite.op (SimplexCategory.mk 0))

                The functor from augmented objects to arrows.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem CategoryTheory.SimplicialObject.Augmented.w₀ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.SimplicialObject.Augmented C} {Y : CategoryTheory.SimplicialObject.Augmented C} (f : X Y) :
                  CategoryTheory.CategoryStruct.comp ((CategoryTheory.SimplicialObject.Augmented.drop.map f).app (Opposite.op (SimplexCategory.mk 0))) (Y.hom.app (Opposite.op (SimplexCategory.mk 0))) = CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op (SimplexCategory.mk 0))) (CategoryTheory.SimplicialObject.Augmented.point.map f)

                  The compatibility of a morphism with the augmentation, on 0-simplices

                  Functor composition induces a functor on augmented simplicial objects.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem CategoryTheory.SimplicialObject.Augmented.whiskering_map_app_right (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u') [CategoryTheory.Category.{v', u'} D] :
                    ∀ {X Y : CategoryTheory.Functor C D} (η : X Y) (A : CategoryTheory.SimplicialObject.Augmented C), (((CategoryTheory.SimplicialObject.Augmented.whiskering C D).map η).app A).right = η.app (CategoryTheory.SimplicialObject.Augmented.point.obj A)

                    Functor composition induces a functor on augmented simplicial objects.

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

                      Augment a simplicial object with an object.

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

                        X _[n] denotes the nth-term of the cosimplicial object X

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

                          Coface maps for a cosimplicial object.

                          Equations
                          Instances For

                            Codegeneracy maps for a cosimplicial object.

                            Equations
                            Instances For

                              Isomorphisms from identities in ℕ.

                              Equations
                              Instances For

                                The skeleton functor from cosimplicial objects to truncated cosimplicial objects.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented C) :
                                  (CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).left = X.left
                                  @[simp]
                                  theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_map_left {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                  ∀ {X Y : CategoryTheory.CosimplicialObject.Augmented C} (η : X Y), (CategoryTheory.CosimplicialObject.Augmented.toArrow.map η).left = η.left
                                  @[simp]
                                  theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented C) :
                                  (CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).right = X.right.obj (SimplexCategory.mk 0)
                                  @[simp]
                                  theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented C) :
                                  (CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).hom = X.hom.app (SimplexCategory.mk 0)
                                  @[simp]
                                  theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_map_right {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                  ∀ {X Y : CategoryTheory.CosimplicialObject.Augmented C} (η : X Y), (CategoryTheory.CosimplicialObject.Augmented.toArrow.map η).right = η.right.app (SimplexCategory.mk 0)

                                  The functor from augmented objects to arrows.

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

                                    Functor composition induces a functor on augmented cosimplicial objects.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]

                                      Functor composition induces a functor on augmented cosimplicial objects.

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

                                        Augment a cosimplicial object with an object.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.cosimplicialSimplicialEquiv_inverse_map (C : Type u) [CategoryTheory.Category.{v, u} C] :
                                          ∀ {X Y : CategoryTheory.Functor SimplexCategoryᵒᵖ Cᵒᵖ} (α : X Y), (CategoryTheory.cosimplicialSimplicialEquiv C).inverse.map α = { app := fun (X_1 : SimplexCategory) => (α.app (Opposite.op X_1)).unop, naturality := }.op

                                          Construct an augmented cosimplicial object in the opposite category from an augmented simplicial object.

                                          Equations
                                          Instances For

                                            Construct an augmented simplicial object from an augmented cosimplicial object in the opposite category.

                                            Equations
                                            Instances For

                                              A functorial version of Cosimplicial_object.Augmented.leftOp.

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

                                                The contravariant categorical equivalence between augmented simplicial objects and augmented cosimplicial objects in the opposite category.

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