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.

@[reducible, inline]

abbrev AugmentedSimplexCategory : Type

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

def AugmentedSimplexCategory.inclusion : CategoryTheory.Functor SimplexCategory AugmentedSimplexCategory

The canonical inclusion from SimplexCategory to AugmentedSimplexCategory.

@[simp]

theorem AugmentedSimplexCategory.inclusion_obj (a✝ : SimplexCategory) : inclusion.obj a✝ = CategoryTheory.WithInitial.of a✝

@[simp]

theorem AugmentedSimplexCategory.inclusion_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) : inclusion.map f = f

instance AugmentedSimplexCategory.instFullSimplexCategoryInclusion : inclusion.Full

instance AugmentedSimplexCategory.instFaithfulSimplexCategoryInclusion : inclusion.Faithful

instance AugmentedSimplexCategory.instHasInitial : CategoryTheory.Limits.HasInitial AugmentedSimplexCategory

def AugmentedSimplexCategory.equivAugmentedCosimplicialObject {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] : CategoryTheory.Functor AugmentedSimplexCategory C ≌ CategoryTheory.CosimplicialObject.Augmented C

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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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))

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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)

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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)

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_left {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) : (equivAugmentedCosimplicialObject.functor.obj F).left = F.obj CategoryTheory.WithInitial.star

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_map_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_left {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C} (η : X✝ ⟶ Y✝) : (equivAugmentedCosimplicialObject.functor.map η).left = η.app CategoryTheory.WithInitial.star

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left {C : Type u_1} [CategoryTheory.Category.{v_1, 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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left {C : Type u_1} [CategoryTheory.Category.{v_1, 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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_obj {C : Type u_1} [CategoryTheory.Category.{v_1, 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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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)

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_map {C : Type u_1} [CategoryTheory.Category.{v_1, 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)

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_map {C : Type u_1} [CategoryTheory.Category.{v_1, 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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_obj {C : Type u_1} [CategoryTheory.Category.{v_1, 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)

def AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso {C : Type u_1} [CategoryTheory.Category.{v_1, 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.

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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✝))

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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✝))

def AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso {C : Type u_1} [CategoryTheory.Category.{v_1, 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.

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C) : equivAugmentedCosimplicialObjectFunctorCompPointIso.hom.app X = CategoryTheory.CategoryStruct.id (X.obj CategoryTheory.WithInitial.star)

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C) : equivAugmentedCosimplicialObjectFunctorCompPointIso.inv.app X = CategoryTheory.CategoryStruct.id (X.obj CategoryTheory.WithInitial.star)

@[deprecated AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso (since := "2025-08-22")]

def AugmentedSimplexCategory.equivAugmentedCosimplicialObjecFunctorCompPointIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] : equivAugmentedCosimplicialObject.functor.comp CategoryTheory.CosimplicialObject.Augmented.point ≅ (CategoryTheory.evaluation AugmentedSimplexCategory C).obj CategoryTheory.WithInitial.star

Alias of AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso.

---

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

def AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso {C : Type u_1} [CategoryTheory.Category.{v_1, 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].

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C) : (equivAugmentedCosimplicialObjectFunctorCompToArrowIso.hom.app X).left = CategoryTheory.CategoryStruct.id (X.obj CategoryTheory.WithInitial.star)

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right {C : Type u_1} [CategoryTheory.Category.{v_1, 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)))

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right {C : Type u_1} [CategoryTheory.Category.{v_1, 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)))

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C) : (equivAugmentedCosimplicialObjectFunctorCompToArrowIso.inv.app X).left = CategoryTheory.CategoryStruct.id (X.obj CategoryTheory.WithInitial.star)

def AugmentedSimplexCategory.equivAugmentedSimplicialObject {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C ≌ CategoryTheory.SimplicialObject.Augmented C

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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map {C : Type u_1} [CategoryTheory.Category.{v_1, 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))

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C) : (equivAugmentedSimplicialObject.counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C) : (equivAugmentedSimplicialObject.counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_obj {C : Type u_1} [CategoryTheory.Category.{v_1, 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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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))

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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)

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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)

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right {C : Type u_1} [CategoryTheory.Category.{v_1, 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)

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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)

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj {C : Type u_1} [CategoryTheory.Category.{v_1, 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)

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_right {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) : (equivAugmentedSimplicialObject.functor.obj X).right = X.obj (Opposite.op CategoryTheory.WithInitial.star)

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map {C : Type u_1} [CategoryTheory.Category.{v_1, 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

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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

def AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso {C : Type u_1} [CategoryTheory.Category.{v_1, 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ᵒᵖ.

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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))

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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))

def AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso {C : Type u_1} [CategoryTheory.Category.{v_1, 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.

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C) : equivAugmentedSimplicialObjectFunctorCompPointIso.inv.app X = CategoryTheory.CategoryStruct.id (X.obj (Opposite.op CategoryTheory.WithInitial.star))

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C) : equivAugmentedSimplicialObjectFunctorCompPointIso.hom.app X = CategoryTheory.CategoryStruct.id (X.obj (Opposite.op CategoryTheory.WithInitial.star))

def AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso {C : Type u_1} [CategoryTheory.Category.{v_1, 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].

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left {C : Type u_1} [CategoryTheory.Category.{v_1, 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))

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C) : (equivAugmentedSimplicialObjectFunctorCompToArrowIso.inv.app X).right = CategoryTheory.CategoryStruct.id (X.obj (Opposite.op CategoryTheory.WithInitial.star))

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left {C : Type u_1} [CategoryTheory.Category.{v_1, 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))

@[simp]

theorem AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C) : (equivAugmentedSimplicialObjectFunctorCompToArrowIso.hom.app X).right = CategoryTheory.CategoryStruct.id (X.obj (Opposite.op CategoryTheory.WithInitial.star))