Documentation

Mathlib.AlgebraicTopology.SimplexCategory.Augmented

The Augmented simplex category #

This file defines the AugmentedSimplexCategory as the category obtained by adding an initial object to SimplexCategory (using CategoryTheory.WithInitial).

This definition provides a canonical full and faithful inclusion functor inclusion : SimplexCategory ⥤ AugmentedSimplexCategory.

We prove that functors out of AugmentedSimplexCategory are equivalent to augmented cosimplicial objects and that functors out of AugmentedSimplexCategoryᵒᵖ are equivalent to augmented simplicial objects, and we provide a translation of the main constrcutions on augmented (co)simplicial objects (i.e drop, point and toArrow) in terms of these equivalences.

TODOs #

source
def AugmentedSimplexCategory :
Type

The AugmentedSimplexCategory is the category obtained from SimplexCategory by adjoining an initial object.

Equations
    Instances For
      source
      instance instAugmentedSimplexCategorySmallCategory :
      CategoryTheory.SmallCategory AugmentedSimplexCategory
      Equations
        source
        def AugmentedSimplexCategory.inclusion :
        CategoryTheory.Functor SimplexCategory AugmentedSimplexCategory

        The canonical inclusion from SimplexCategory to AugmentedSimplexCategory.

        Equations
          Instances For
            source
            @[simp]
            theorem AugmentedSimplexCategory.inclusion_obj (a✝ : SimplexCategory) :
            inclusion.obj a✝ = CategoryTheory.WithInitial.of a✝
            source
            @[simp]
            theorem AugmentedSimplexCategory.inclusion_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) :
            inclusion.map f = f
            source
            instance AugmentedSimplexCategory.instFullSimplexCategoryInclusion :
            inclusion.Full
            source
            instance AugmentedSimplexCategory.instFaithfulSimplexCategoryInclusion :
            inclusion.Faithful
            source
            instance AugmentedSimplexCategory.instHasInitial :
            CategoryTheory.Limits.HasInitial AugmentedSimplexCategory
            source
            def AugmentedSimplexCategory.equivAugmentedCosimplicialObject {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
            CategoryTheory.Functor AugmentedSimplexCategory C ≌ CategoryTheory.CosimplicialObject.Augmented C

            The equivalence between functors out of AugmentedSimplexCategory and augmented cosimplicial objects.

            Equations
              Instances For
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory) (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C))) :
                (equivAugmentedCosimplicialObject.counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (F : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) (x : SimplexCategory) :
                (equivAugmentedCosimplicialObject.functor.obj F).hom.app x = F.map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of x))
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (c : CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory) (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C))) {X Y : CategoryTheory.WithInitial SimplexCategory} (f : X ⟶ Y) :
                (equivAugmentedCosimplicialObject.inverse.obj c).map f = match X, Y, f with | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => c.right.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => c.hom.app a | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id c.left
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) (X✝ : CategoryTheory.WithInitial SimplexCategory) :
                (equivAugmentedCosimplicialObject.unitIso.inv.app X).app X✝ = (match X✝ with | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).inv
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (F : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) :
                (equivAugmentedCosimplicialObject.functor.obj F).right.map f = F.map (CategoryTheory.WithInitial.incl.map f)
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (c : CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory) (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C))) (X : CategoryTheory.WithInitial SimplexCategory) :
                (equivAugmentedCosimplicialObject.inverse.obj c).obj X = match X with | CategoryTheory.WithInitial.of x => c.right.obj x | CategoryTheory.WithInitial.star => c.left
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_map_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory) (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C))} (φ : X✝ ⟶ Y✝) (x : CategoryTheory.WithInitial SimplexCategory) :
                (equivAugmentedCosimplicialObject.inverse.map φ).app x = match x with | CategoryTheory.WithInitial.of x => φ.right.app x | CategoryTheory.WithInitial.star => φ.left
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory) (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C))) :
                (equivAugmentedCosimplicialObject.counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (F : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) :
                (equivAugmentedCosimplicialObject.functor.obj F).left = F.obj CategoryTheory.WithInitial.star
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory) (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C))) (X✝ : SimplexCategory) :
                (equivAugmentedCosimplicialObject.counitIso.hom.app X).right.app X✝ = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithInitial.incl.obj X✝ with | CategoryTheory.WithInitial.of x => X.right.obj x | CategoryTheory.WithInitial.star => X.left)
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) (X✝ : CategoryTheory.WithInitial SimplexCategory) :
                (equivAugmentedCosimplicialObject.unitIso.hom.app X).app X✝ = (match X✝ with | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).hom
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C} (η : X✝ ⟶ Y✝) (X : SimplexCategory) :
                (equivAugmentedCosimplicialObject.functor.map η).right.app X = η.app (CategoryTheory.WithInitial.incl.obj X)
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C} (η : X✝ ⟶ Y✝) :
                (equivAugmentedCosimplicialObject.functor.map η).left = η.app CategoryTheory.WithInitial.star
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory) (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C))) (X✝ : SimplexCategory) :
                (equivAugmentedCosimplicialObject.counitIso.inv.app X).right.app X✝ = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithInitial.incl.obj X✝ with | CategoryTheory.WithInitial.of x => X.right.obj x | CategoryTheory.WithInitial.star => X.left)
                source
                @[simp]
                theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (F : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) (X : SimplexCategory) :
                (equivAugmentedCosimplicialObject.functor.obj F).right.obj X = F.obj (CategoryTheory.WithInitial.incl.obj X)
                source
                def AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
                equivAugmentedCosimplicialObject.functor.comp CategoryTheory.CosimplicialObject.Augmented.drop ≅ (CategoryTheory.Functor.whiskeringLeft SimplexCategory AugmentedSimplexCategory C).obj inclusion

                Through the equivalence (AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C, dropping the augmentation corresponds to precomposition with inclusion : SimplexCategory ⥤ AugmentedSimplexCategory.

                Equations
                  Instances For
                    source
                    @[simp]
                    theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C) (X✝ : SimplexCategory) :
                    (equivAugmentedCosimplicialObjectFunctorCompDropIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.WithInitial.incl.obj X✝))
                    source
                    @[simp]
                    theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C) (X✝ : SimplexCategory) :
                    (equivAugmentedCosimplicialObjectFunctorCompDropIso.inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.WithInitial.incl.obj X✝))
                    source
                    def AugmentedSimplexCategory.equivAugmentedCosimplicialObjecFunctorCompPointIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
                    equivAugmentedCosimplicialObject.functor.comp CategoryTheory.CosimplicialObject.Augmented.point ≅ (CategoryTheory.evaluation AugmentedSimplexCategory C).obj CategoryTheory.WithInitial.star

                    Through the equivalence (AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C, taking the point of the augmentation corresponds to evaluation at the initial object.

                    Equations
                      Instances For
                        source
                        @[simp]
                        theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjecFunctorCompPointIso_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C) :
                        equivAugmentedCosimplicialObjecFunctorCompPointIso.inv.app X = CategoryTheory.CategoryStruct.id (X.obj CategoryTheory.WithInitial.star)
                        source
                        @[simp]
                        theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjecFunctorCompPointIso_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C) :
                        equivAugmentedCosimplicialObjecFunctorCompPointIso.hom.app X = CategoryTheory.CategoryStruct.id (X.obj CategoryTheory.WithInitial.star)
                        source
                        def AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
                        equivAugmentedCosimplicialObject.functor.comp CategoryTheory.CosimplicialObject.Augmented.toArrow ≅ (CategoryTheory.Functor.mapArrowFunctor AugmentedSimplexCategory C).comp ((CategoryTheory.evaluation (CategoryTheory.Arrow AugmentedSimplexCategory) (CategoryTheory.Arrow C)).obj (CategoryTheory.Arrow.mk (CategoryTheory.WithInitial.homTo (SimplexCategory.mk 0))))

                        Through the equivalence (AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C, the arrow attached to the cosimplicial object is the one obtained by evaluation at the unique arrow star ⟶ of [0].

                        Equations
                          Instances For
                            source
                            @[simp]
                            theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C) :
                            (equivAugmentedCosimplicialObjectFunctorCompToArrowIso.hom.app X).right = CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.WithInitial.incl.obj (SimplexCategory.mk 0)))
                            source
                            @[simp]
                            theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C) :
                            (equivAugmentedCosimplicialObjectFunctorCompToArrowIso.inv.app X).left = CategoryTheory.CategoryStruct.id (X.obj CategoryTheory.WithInitial.star)
                            source
                            @[simp]
                            theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C) :
                            (equivAugmentedCosimplicialObjectFunctorCompToArrowIso.inv.app X).right = CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.WithInitial.incl.obj (SimplexCategory.mk 0)))
                            source
                            @[simp]
                            theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C) :
                            (equivAugmentedCosimplicialObjectFunctorCompToArrowIso.hom.app X).left = CategoryTheory.CategoryStruct.id (X.obj CategoryTheory.WithInitial.star)
                            source
                            def AugmentedSimplexCategory.equivAugmentedSimplicialObject {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
                            CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C ≌ CategoryTheory.SimplicialObject.Augmented C

                            The equivalence between functors out of AugmentedSimplexCategory and augmented simplicial objects.

                            Equations
                              Instances For
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C) (X✝ : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ) :
                                (equivAugmentedSimplicialObject.inverse.obj X).obj X✝ = match match Opposite.unop X✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x) | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star with | CategoryTheory.WithTerminal.of x => X.left.obj x | CategoryTheory.WithTerminal.star => X.right
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) (X✝ : SimplexCategoryᵒᵖ) :
                                (equivAugmentedSimplicialObject.functor.obj X).left.obj X✝ = X.obj (match CategoryTheory.WithTerminal.incl.obj X✝ with | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x)) | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star)
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C) (X✝ : SimplexCategoryᵒᵖ) :
                                (equivAugmentedSimplicialObject.counitIso.hom.app X).left.app X✝ = match match Opposite.unop (match CategoryTheory.WithTerminal.incl.obj X✝ with | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x)) | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star) with | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x) | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.incl.obj X✝, (match CategoryTheory.WithTerminal.incl.obj X✝ with | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of x) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).hom with | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => X.left.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => X.hom.app x | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id X.right
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) (X✝ : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ) :
                                (equivAugmentedSimplicialObject.unitIso.inv.app X).app X✝ = CategoryTheory.CategoryStruct.comp (match match Opposite.unop X✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x) | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star with | CategoryTheory.WithTerminal.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.incl.comp ((CategoryTheory.WithInitial.opEquiv SimplexCategory).inverse.comp X))).app x | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (X.obj (Opposite.op CategoryTheory.WithInitial.star))).inv (X.map (match Opposite.unop X✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithInitial.of x)) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithInitial.star)).inv)
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C) :
                                (equivAugmentedSimplicialObject.counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C} (f : X✝ ⟶ Y✝) (X : SimplexCategoryᵒᵖ) :
                                (equivAugmentedSimplicialObject.functor.map f).left.app X = f.app (match CategoryTheory.WithTerminal.incl.obj X with | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x)) | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star)
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) (X✝ : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ) :
                                (equivAugmentedSimplicialObject.unitIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.comp (X.map (match Opposite.unop X✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithInitial.of x)) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithInitial.star)).hom) (match match Opposite.unop X✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x) | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star with | CategoryTheory.WithTerminal.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.incl.comp ((CategoryTheory.WithInitial.opEquiv SimplexCategory).inverse.comp X))).app x | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (X.obj (Opposite.op CategoryTheory.WithInitial.star))).hom
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C} (f : X✝ ⟶ Y✝) :
                                (equivAugmentedSimplicialObject.functor.map f).right = f.app (Opposite.op CategoryTheory.WithInitial.star)
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) {X✝ Y✝ : SimplexCategoryᵒᵖ} (f : X✝ ⟶ Y✝) :
                                (equivAugmentedSimplicialObject.functor.obj X).left.map f = X.map (match CategoryTheory.WithTerminal.incl.obj X✝, CategoryTheory.WithTerminal.incl.obj Y✝, CategoryTheory.WithTerminal.incl.map f with | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f => CategoryTheory.WithInitial.down f | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x => Opposite.op (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of unop)) | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.WithInitial.star))
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C) :
                                (equivAugmentedSimplicialObject.counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C) (X✝ : SimplexCategoryᵒᵖ) :
                                (equivAugmentedSimplicialObject.counitIso.inv.app X).left.app X✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (match CategoryTheory.WithTerminal.incl.obj X✝ with | CategoryTheory.WithTerminal.of x => X.left.obj x | CategoryTheory.WithTerminal.star => X.right)) (match CategoryTheory.WithTerminal.incl.obj X✝, match Opposite.unop (match CategoryTheory.WithTerminal.incl.obj X✝ with | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x)) | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star) with | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x) | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star, (match CategoryTheory.WithTerminal.incl.obj X✝ with | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of x) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).inv with | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => X.left.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => X.hom.app x | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id X.right)
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X✝ Y✝ : CategoryTheory.SimplicialObject.Augmented C} (f : X✝ ⟶ Y✝) (X : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ) :
                                (equivAugmentedSimplicialObject.inverse.map f).app X = match match Opposite.unop X with | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x) | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star with | CategoryTheory.WithTerminal.of x => f.left.app x | CategoryTheory.WithTerminal.star => f.right
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) (x : SimplexCategoryᵒᵖ) :
                                (equivAugmentedSimplicialObject.functor.obj X).hom.app x = X.map (match CategoryTheory.WithTerminal.incl.obj x, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of x) with | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f => CategoryTheory.WithInitial.down f | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x => Opposite.op (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of unop)) | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.WithInitial.star))
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) :
                                (equivAugmentedSimplicialObject.functor.obj X).right = X.obj (Opposite.op CategoryTheory.WithInitial.star)
                                source
                                @[simp]
                                theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C) {X✝ Y✝ : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ} (f : X✝ ⟶ Y✝) :
                                (equivAugmentedSimplicialObject.inverse.obj X).map f = match match Opposite.unop X✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x) | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star, match Opposite.unop Y✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x) | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star, match X✝, Y✝, Opposite.unop f, f with | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_1 => (CategoryTheory.WithTerminal.down f).op | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_1 => CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of (Opposite.op a)) | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_1 => CategoryTheory.CategoryStruct.id CategoryTheory.WithTerminal.star with | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => X.left.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => X.hom.app x | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id X.right
                                source
                                def AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
                                equivAugmentedSimplicialObject.functor.comp CategoryTheory.SimplicialObject.Augmented.drop ≅ (CategoryTheory.Functor.whiskeringLeft SimplexCategoryᵒᵖ AugmentedSimplexCategoryᵒᵖ C).obj inclusion.op

                                Through the equivalence (AugmentedSimplexCategoryᵒᵖ ⥤ C) ≌ SimplicialObject.Augmented C, dropping the augmentation corresponds to precomposition with inclusionᵒᵖ : SimplexCategoryᵒᵖ ⥤ AugmentedSimplexCategoryᵒᵖ.

                                Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C) (X✝ : SimplexCategoryᵒᵖ) :
                                    (equivAugmentedSimplicialObjectFunctorCompDropIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj (match CategoryTheory.WithTerminal.incl.obj X✝ with | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x)) | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star))
                                    source
                                    @[simp]
                                    theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C) (X✝ : SimplexCategoryᵒᵖ) :
                                    (equivAugmentedSimplicialObjectFunctorCompDropIso.inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj (match CategoryTheory.WithTerminal.incl.obj X✝ with | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x)) | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star))
                                    source
                                    def AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
                                    equivAugmentedSimplicialObject.functor.comp CategoryTheory.SimplicialObject.Augmented.point ≅ (CategoryTheory.evaluation AugmentedSimplexCategoryᵒᵖ C).obj (Opposite.op CategoryTheory.WithInitial.star)

                                    Through the equivalence (AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C, taking the point of the augmentation corresponds to evaluation at the initial object.

                                    Equations
                                      Instances For
                                        source
                                        @[simp]
                                        theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C) :
                                        equivAugmentedSimplicialObjectFunctorCompPointIso.inv.app X = CategoryTheory.CategoryStruct.id (X.obj (Opposite.op CategoryTheory.WithInitial.star))
                                        source
                                        @[simp]
                                        theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C) :
                                        equivAugmentedSimplicialObjectFunctorCompPointIso.hom.app X = CategoryTheory.CategoryStruct.id (X.obj (Opposite.op CategoryTheory.WithInitial.star))
                                        source
                                        def AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
                                        equivAugmentedSimplicialObject.functor.comp CategoryTheory.SimplicialObject.Augmented.toArrow ≅ (CategoryTheory.Functor.mapArrowFunctor AugmentedSimplexCategoryᵒᵖ C).comp ((CategoryTheory.evaluation (CategoryTheory.Arrow AugmentedSimplexCategoryᵒᵖ) (CategoryTheory.Arrow C)).obj (CategoryTheory.Arrow.mk (CategoryTheory.WithInitial.homTo (SimplexCategory.mk 0)).op))

                                        Through the equivalence (AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C, the arrow attached to the cosimplicial object is the one obtained by evaluation at the unique arrow star ⟶ of [0].

                                        Equations
                                          Instances For
                                            source
                                            @[simp]
                                            theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C) :
                                            (equivAugmentedSimplicialObjectFunctorCompToArrowIso.hom.app X).left = CategoryTheory.CategoryStruct.id (X.obj (match CategoryTheory.WithTerminal.incl.obj (Opposite.op (SimplexCategory.mk 0)) with | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x)) | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star))
                                            source
                                            @[simp]
                                            theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C) :
                                            (equivAugmentedSimplicialObjectFunctorCompToArrowIso.hom.app X).right = CategoryTheory.CategoryStruct.id (X.obj (Opposite.op CategoryTheory.WithInitial.star))
                                            source
                                            @[simp]
                                            theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C) :
                                            (equivAugmentedSimplicialObjectFunctorCompToArrowIso.inv.app X).right = CategoryTheory.CategoryStruct.id (X.obj (Opposite.op CategoryTheory.WithInitial.star))
                                            source
                                            @[simp]
                                            theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C) :
                                            (equivAugmentedSimplicialObjectFunctorCompToArrowIso.inv.app X).left = CategoryTheory.CategoryStruct.id (X.obj (match CategoryTheory.WithTerminal.incl.obj (Opposite.op (SimplexCategory.mk 0)) with | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x)) | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star))