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_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) :
      inclusion.map f = f
      source
      @[simp]
      theorem AugmentedSimplexCategory.inclusion_obj (a✝ : SimplexCategory) :
      inclusion.obj a✝ = CategoryTheory.WithInitial.of a✝
      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_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_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_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_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_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_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_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_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_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_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_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_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_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_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.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
        • One or more equations did not get rendered due to their size.
        Instances For
          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
          @[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
          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
          • One or more equations did not get rendered due to their size.
          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
            • One or more equations did not get rendered due to their size.
            Instances For
              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_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
              @[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_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
              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_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_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_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_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_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_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_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_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_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_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_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
                @[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_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
                def AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
                equivAugmentedSimplicialObject.functor.comp CategoryTheory.SimplicialObject.Augmented.drop ≅ (CategoryTheory.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
                • One or more equations did not get rendered due to their size.
                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
                  • One or more equations did not get rendered due to their size.
                  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
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      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))
                      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))