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.

Equations

• AugmentedSimplexCategory.tensorObjOf m n = SimplexCategory.mk (m.len + n.len + 1)

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

The tensor product of two objects of AugmentedSimplexCategory.

Equations

• AugmentedSimplexCategory.tensorObj (CategoryTheory.WithInitial.of m_2) (CategoryTheory.WithInitial.of n_2) = CategoryTheory.WithInitial.of (AugmentedSimplexCategory.tensorObjOf m_2 n_2)
• AugmentedSimplexCategory.tensorObj CategoryTheory.WithInitial.star n = n
• m.tensorObj CategoryTheory.WithInitial.star = m

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.

Equations

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

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.

Equations

• One or more equations did not get rendered due to their size.
• AugmentedSimplexCategory.tensorHom f₁_2 f₂_2 = AugmentedSimplexCategory.tensorHomOf f₁_2 f₂_2
• AugmentedSimplexCategory.tensorHom x f₂_2 = f₂_2
• AugmentedSimplexCategory.tensorHom f₁_2 x = f₁_2
• AugmentedSimplexCategory.tensorHom f₁ f₂ = CategoryTheory.WithInitial.starInitial.to (y₁.tensorObj y₂)

@[reducible, inline]

abbrev AugmentedSimplexCategory.tensorUnit : AugmentedSimplexCategory

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

Equations

• AugmentedSimplexCategory.tensorUnit = CategoryTheory.WithInitial.star

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

Equations

• One or more equations did not get rendered due to their size.
• AugmentedSimplexCategory.associator (CategoryTheory.WithInitial.of x_2) (CategoryTheory.WithInitial.of y_2) (CategoryTheory.WithInitial.of z_2) = CategoryTheory.eqToIso ⋯

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

The left unitor isomorphism for the monoidal structure in AugmentedSimplexCategory

Equations

• AugmentedSimplexCategory.leftUnitor (CategoryTheory.WithInitial.of a) = CategoryTheory.Iso.refl (AugmentedSimplexCategory.tensorUnit.tensorObj (CategoryTheory.WithInitial.of a))
• AugmentedSimplexCategory.leftUnitor CategoryTheory.WithInitial.star = CategoryTheory.Iso.refl (AugmentedSimplexCategory.tensorUnit.tensorObj CategoryTheory.WithInitial.star)

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

The right unitor isomorphism for the monoidal structure in AugmentedSimplexCategory

Equations

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

instance AugmentedSimplexCategory.instMonoidalCategoryStruct : CategoryTheory.MonoidalCategoryStruct AugmentedSimplexCategory

Equations

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

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 Δ, Δ'.

Equations

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

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 Δ, Δ'.

Equations

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

@[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.

Equations

• AugmentedSimplexCategory.inl' x y = CategoryTheory.WithInitial.down (AugmentedSimplexCategory.inl (CategoryTheory.WithInitial.of x) (CategoryTheory.WithInitial.of y))

@[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.

Equations

• AugmentedSimplexCategory.inr' x y = CategoryTheory.WithInitial.down (AugmentedSimplexCategory.inr (CategoryTheory.WithInitial.of x) (CategoryTheory.WithInitial.of y))

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

Equations

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