Monoidal structure on the augmented simplex category

This file defines a monoidal structure on AugmentedSimplexCategory. The tensor product of objects is characterized by the fact that the initial object star is also the unit, and the fact that ⦋m⦌ ⊗ ⦋n⦌ = ⦋m + n + 1⦌ for n m : ℕ.

Through the (not in mathlib) equivalence between AugmentedSimplexCategory and the category of finite ordinals, the tensor products corresponds to ordinal sum.

As the unit of this structure is an initial object, for every x y : AugmentedSimplexCategory, there are maps AugmentedSimplexCategory.inl x y : x ⟶ x ⊗ y and AugmentedSimplexCategory.inr x y : y ⟶ x ⊗ y. The main API for working with the tensor product of maps is given by AugmentedSimplexCategory.tensorObj_hom_ext, which characterizes maps x ⊗ y ⟶ z in terms of their composition with these two maps. We also characterize the behaviour of the associator isomorphism with respect to these maps.

@[simp]

theorem AugmentedSimplexCategory.eqToHom_toOrderHom {x y : SimplexCategory} (h : CategoryTheory.WithInitial.of x = CategoryTheory.WithInitial.of y) : SimplexCategory.Hom.toOrderHom (CategoryTheory.WithInitial.down (CategoryTheory.eqToHom h)) = (Fin.castOrderIso ⋯).toOrderEmbedding.toOrderHom

@[reducible, inline]

abbrev AugmentedSimplexCategory.tensorObjOf (m n : SimplexCategory) : SimplexCategory

An auxiliary definition for the tensor product of two objects in AugmentedSimplexCategory.

def AugmentedSimplexCategory.tensorObj (m n : AugmentedSimplexCategory) : AugmentedSimplexCategory

The tensor product of two objects of AugmentedSimplexCategory.

def AugmentedSimplexCategory.tensorHomOf {x₁ y₁ x₂ y₂ : SimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂) : tensorObjOf x₁ x₂ ⟶ tensorObjOf y₁ y₂

The action of the tensor product on maps coming from SimplexCategory.

def AugmentedSimplexCategory.tensorHom {x₁ y₁ x₂ y₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂) : x₁.tensorObj x₂ ⟶ y₁.tensorObj y₂

The action of the tensor product on maps of AugmentedSimplexCategory.

@[reducible, inline]

abbrev AugmentedSimplexCategory.tensorUnit : AugmentedSimplexCategory

The unit for the monoidal structure on AugmentedSimplexCategory is the initial object.

def AugmentedSimplexCategory.associator (x y z : AugmentedSimplexCategory) : (x.tensorObj y).tensorObj z ≅ x.tensorObj (y.tensorObj z)

The associator isomorphism for the monoidal structure on AugmentedSimplexCategory

def AugmentedSimplexCategory.leftUnitor (x : AugmentedSimplexCategory) : tensorUnit.tensorObj x ≅ x

The left unitor isomorphism for the monoidal structure in AugmentedSimplexCategory

def AugmentedSimplexCategory.rightUnitor (x : AugmentedSimplexCategory) : x.tensorObj tensorUnit ≅ x

The right unitor isomorphism for the monoidal structure in AugmentedSimplexCategory

instance AugmentedSimplexCategory.instMonoidalCategoryStruct : CategoryTheory.MonoidalCategoryStruct AugmentedSimplexCategory

theorem AugmentedSimplexCategory.id_tensorHom (x : AugmentedSimplexCategory) {y₁ y₂ : AugmentedSimplexCategory} (f : y₁ ⟶ y₂) : CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id x) f = CategoryTheory.MonoidalCategoryStruct.whiskerLeft x f

theorem AugmentedSimplexCategory.tensorHom_id {x₁ x₂ : AugmentedSimplexCategory} (y : AugmentedSimplexCategory) (f : x₁ ⟶ x₂) : CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id y) = CategoryTheory.MonoidalCategoryStruct.whiskerRight f y

theorem AugmentedSimplexCategory.whiskerLeft_id_star {x : AugmentedSimplexCategory} : CategoryTheory.MonoidalCategoryStruct.whiskerLeft x (CategoryTheory.CategoryStruct.id CategoryTheory.WithInitial.star) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj x CategoryTheory.WithInitial.star)

theorem AugmentedSimplexCategory.id_star_whiskerRight {x : AugmentedSimplexCategory} : CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id CategoryTheory.WithInitial.star) x = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.WithInitial.star x)

def AugmentedSimplexCategory.inl (x y : AugmentedSimplexCategory) : x ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj x y

Thanks to tensorUnit being initial in AugmentedSimplexCategory, we get a morphism Δ ⟶ Δ ⊗ Δ' for every pair of objects Δ, Δ'.

def AugmentedSimplexCategory.inr (x y : AugmentedSimplexCategory) : y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj x y

Thanks to tensorUnit being initial in AugmentedSimplexCategory, we get a morphism Δ' ⟶ Δ ⊗ Δ' for every pair of objects Δ, Δ'.

@[reducible, inline]

abbrev AugmentedSimplexCategory.inl' (x y : SimplexCategory) : x ⟶ tensorObjOf x y

To ease type checking, we also provide a version of inl that lives in SimplexCategory.

@[reducible, inline]

abbrev AugmentedSimplexCategory.inr' (x y : SimplexCategory) : y ⟶ tensorObjOf x y

To ease type checking, we also provide a version of inr that lives in SimplexCategory.

theorem AugmentedSimplexCategory.inl'_eval (x y : SimplexCategory) (i : Fin (x.len + 1)) : (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)

theorem AugmentedSimplexCategory.inr'_eval (x y : SimplexCategory) (i : Fin (y.len + 1)) : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)

theorem AugmentedSimplexCategory.tensorObj_hom_ext {x y z : AugmentedSimplexCategory} (f g : CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟶ z) (h₁ : CategoryTheory.CategoryStruct.comp (x.inl y) f = CategoryTheory.CategoryStruct.comp (x.inl y) g) (h₂ : CategoryTheory.CategoryStruct.comp (x.inr y) f = CategoryTheory.CategoryStruct.comp (x.inr y) g) : f = g

We can characterize morphisms out of a tensor product via their precomposition with inl and inr.

theorem AugmentedSimplexCategory.tensorObj_hom_ext_iff {x y z : AugmentedSimplexCategory} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟶ z} : f = g ↔ CategoryTheory.CategoryStruct.comp (x.inl y) f = CategoryTheory.CategoryStruct.comp (x.inl y) g ∧ CategoryTheory.CategoryStruct.comp (x.inr y) f = CategoryTheory.CategoryStruct.comp (x.inr y) g

@[simp]

theorem AugmentedSimplexCategory.inl_comp_tensorHom {x₁ y₁ x₂ y₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂) : CategoryTheory.CategoryStruct.comp (x₁.inl x₂) (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) = CategoryTheory.CategoryStruct.comp f₁ (y₁.inl y₂)

@[simp]

theorem AugmentedSimplexCategory.inl_comp_tensorHom_assoc {x₁ y₁ x₂ y₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂) {Z : AugmentedSimplexCategory} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj y₁ y₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (x₁.inl x₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) h) = CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.CategoryStruct.comp (y₁.inl y₂) h)

@[simp]

theorem AugmentedSimplexCategory.inr_comp_tensorHom {x₁ y₁ x₂ y₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂) : CategoryTheory.CategoryStruct.comp (x₁.inr x₂) (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) = CategoryTheory.CategoryStruct.comp f₂ (y₁.inr y₂)

@[simp]

theorem AugmentedSimplexCategory.inr_comp_tensorHom_assoc {x₁ y₁ x₂ y₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂) {Z : AugmentedSimplexCategory} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj y₁ y₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (x₁.inr x₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) h) = CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.CategoryStruct.comp (y₁.inr y₂) h)

@[simp]

theorem AugmentedSimplexCategory.inr_comp_associator (x y z : AugmentedSimplexCategory) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inr z) (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom = CategoryTheory.CategoryStruct.comp (y.inr z) (x.inr (CategoryTheory.MonoidalCategoryStruct.tensorObj y z))

@[simp]

theorem AugmentedSimplexCategory.inr_comp_associator_assoc (x y z : AugmentedSimplexCategory) {Z : AugmentedSimplexCategory} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj x (CategoryTheory.MonoidalCategoryStruct.tensorObj y z) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inr z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom h) = CategoryTheory.CategoryStruct.comp (y.inr z) (CategoryTheory.CategoryStruct.comp (x.inr (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)) h)

@[simp]

theorem AugmentedSimplexCategory.inl_comp_inl_comp_associator (x y z : AugmentedSimplexCategory) : CategoryTheory.CategoryStruct.comp (x.inl y) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inl z) (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom) = x.inl (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)

@[simp]

theorem AugmentedSimplexCategory.inl_comp_inl_comp_associator_assoc (x y z : AugmentedSimplexCategory) {Z : AugmentedSimplexCategory} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj x (CategoryTheory.MonoidalCategoryStruct.tensorObj y z) ⟶ Z) : CategoryTheory.CategoryStruct.comp (x.inl y) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inl z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom h)) = CategoryTheory.CategoryStruct.comp (x.inl (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)) h

@[simp]

theorem AugmentedSimplexCategory.inr_comp_inl_comp_associator (x y z : AugmentedSimplexCategory) : CategoryTheory.CategoryStruct.comp (x.inr y) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inl z) (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom) = CategoryTheory.CategoryStruct.comp (y.inl z) (x.inr (CategoryTheory.MonoidalCategoryStruct.tensorObj y z))

@[simp]

theorem AugmentedSimplexCategory.inr_comp_inl_comp_associator_assoc (x y z : AugmentedSimplexCategory) {Z : AugmentedSimplexCategory} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj x (CategoryTheory.MonoidalCategoryStruct.tensorObj y z) ⟶ Z) : CategoryTheory.CategoryStruct.comp (x.inr y) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inl z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom h)) = CategoryTheory.CategoryStruct.comp (y.inl z) (CategoryTheory.CategoryStruct.comp (x.inr (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)) h)

theorem AugmentedSimplexCategory.tensorHom_comp_tensorHom {x₁ y₁ z₁ x₂ y₂ z₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂) (g₁ : y₁ ⟶ z₁) (g₂ : y₂ ⟶ z₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂) = CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂)

theorem AugmentedSimplexCategory.tensor_id (x y : AugmentedSimplexCategory) : CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id x) (CategoryTheory.CategoryStruct.id y) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)

instance AugmentedSimplexCategory.instMonoidalCategory : CategoryTheory.MonoidalCategory AugmentedSimplexCategory