# Monoidal categories #

A monoidal category is a category equipped with a tensor product, unitors, and an associator. In the definition, we provide the tensor product as a pair of functions

- `tensorObj : C → C → C`
- `tensorHom : (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → ((X₁ ⊗ X₂) ⟶ (Y₁ ⊗ Y₂))` and allow use of the overloaded notation `⊗` for both. The unitors and associator are provided componentwise.

The tensor product can be expressed as a functor via `tensor : C × C ⥤ C`. The unitors and associator are gathered together as natural isomorphisms in `leftUnitor_nat_iso`, `rightUnitor_nat_iso` and `associator_nat_iso`.

Some consequences of the definition are proved in other files after proving the coherence theorem, e.g. `(λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom` in `CategoryTheory.Monoidal.CoherenceLemmas`.

## Implementation notes #

In the definition of monoidal categories, we also provide the whiskering operators:

- `whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : X ⊗ Y₁ ⟶ X ⊗ Y₂`, denoted by `X ◁ f`,
- `whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : X₁ ⊗ Y ⟶ X₂ ⊗ Y`, denoted by `f ▷ Y`. These are products of an object and a morphism (the terminology "whiskering" is borrowed from 2-category theory). The tensor product of morphisms `tensorHom` can be defined in terms of the whiskerings. There are two possible such definitions, which are related by the exchange property of the whiskerings. These two definitions are accessed by `tensorHom_def` and `tensorHom_def'`. By default, `tensorHom` is defined so that `tensorHom_def` holds definitionally.

If you want to provide `tensorHom` and define `whiskerLeft` and `whiskerRight` in terms of it, you can use the alternative constructor `CategoryTheory.MonoidalCategory.ofTensorHom`.

The whiskerings are useful when considering simp-normal forms of morphisms in monoidal categories.

### Simp-normal form for morphisms #

Rewriting involving associators and unitors could be very complicated. We try to ease this complexity by putting carefully chosen simp lemmas that rewrite any morphisms into the simp-normal form defined below. Rewriting into simp-normal form is especially useful in preprocessing performed by the `coherence` tactic.

The simp-normal form of morphisms is defined to be an expression that has the minimal number of parentheses. More precisely,

1. it is a composition of morphisms like `f₁ ≫ f₂ ≫ f₃ ≫ f₄ ≫ f₅` such that each `fᵢ` is either a structural morphism (morphisms made up only of identities, associators, unitors) or a non-structural morphism, and
2. each non-structural morphism in the composition is of the form `X₁ ◁ X₂ ◁ X₃ ◁ f ▷ X₄ ▷ X₅`, where each `Xᵢ` is an object that is not the identity or a tensor and `f` is a non-structural morphism that is not the identity or a composite.

Note that `X₁ ◁ X₂ ◁ X₃ ◁ f ▷ X₄ ▷ X₅` is actually `X₁ ◁ (X₂ ◁ (X₃ ◁ ((f ▷ X₄) ▷ X₅)))`.

Currently, the simp lemmas don't rewrite `𝟙 X ⊗ₘ f` and `f ⊗ₘ 𝟙 Y` into `X ◁ f` and `f ▷ Y`, respectively, since it requires a huge refactoring. We hope to add these simp lemmas soon.

## References #

- Tensor categories, Etingof, Gelaki, Nikshych, Ostrik, http://www-math.mit.edu/~etingof/egnobookfinal.pdf
- https://stacks.math.columbia.edu/tag/0FFK.

source
class CategoryTheory.MonoidalCategoryStruct (C : Type u) [𝒞 : Category.{v, u} C] :
Type (max u v)

Auxiliary structure to carry only the data fields of (and provide notation for) `MonoidalCategory`.

- tensorObj : C → C → C

  curried tensor product of objects

- whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : tensorObj X Y₁ ⟶ tensorObj X Y₂

  left whiskering for morphisms

- whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y

  right whiskering for morphisms

- tensorHom {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂

  Tensor product of identity maps is the identity: `𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)`

- tensorUnit : C

  The tensor unity in the monoidal structure `𝟙_ C`

- associator (X Y Z : C) : tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)

  The associator isomorphism `(X ⊗ Y) ⊗ Z ≃ X ⊗ (Y ⊗ Z)`

- leftUnitor (X : C) : tensorObj (tensorUnit C) X ≅ X

  The left unitor: `𝟙_ C ⊗ X ≃ X`

- rightUnitor (X : C) : tensorObj X (tensorUnit C) ≅ X

  The right unitor: `X ⊗ 𝟙_ C ≃ X`

Instances

source
def CategoryTheory.MonoidalCategory.«term_⊗_» :
Lean.TrailingParserDescr

Notation for `tensorObj`, the tensor product of objects in a monoidal category

Equations

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

Instances For

source
def CategoryTheory.MonoidalCategory.«term_◁_» :
Lean.TrailingParserDescr

Notation for the `whiskerLeft` operator of monoidal categories

Equations

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

Instances For

source
def CategoryTheory.MonoidalCategory.«term_▷_» :
Lean.TrailingParserDescr

Notation for the `whiskerRight` operator of monoidal categories

Equations

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

Instances For

source
def CategoryTheory.MonoidalCategory.«term_⊗ₘ_» :
Lean.TrailingParserDescr

Notation for `tensorHom`, the tensor product of morphisms in a monoidal category

Equations

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

Instances For

source
def CategoryTheory.MonoidalCategory.«term𝟙__» :
Lean.ParserDescr

Notation for `tensorUnit`, the two-sided identity of `⊗`

Equations

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

Instances For

source
def CategoryTheory.MonoidalCategory.termα_ :
Lean.ParserDescr

Notation for the monoidal `associator`: `(X ⊗ Y) ⊗ Z ≃ X ⊗ (Y ⊗ Z)`

Equations

- CategoryTheory.MonoidalCategory.termα_ = Lean.ParserDescr.node `CategoryTheory.MonoidalCategory.termα_ 1024 (Lean.ParserDescr.symbol "α_")

Instances For

source
def CategoryTheory.MonoidalCategory.«termλ_» :
Lean.ParserDescr

Notation for the `leftUnitor`: `𝟙_C ⊗ X ≃ X`

Equations

- CategoryTheory.MonoidalCategory.«termλ_» = Lean.ParserDescr.node `CategoryTheory.MonoidalCategory.«termλ_» 1024 (Lean.ParserDescr.symbol "λ_")

Instances For

source
def CategoryTheory.MonoidalCategory.termρ_ :
Lean.ParserDescr

Notation for the `rightUnitor`: `X ⊗ 𝟙_C ≃ X`

Equations

- CategoryTheory.MonoidalCategory.termρ_ = Lean.ParserDescr.node `CategoryTheory.MonoidalCategory.termρ_ 1024 (Lean.ParserDescr.symbol "ρ_")

Instances For

source
def CategoryTheory.MonoidalCategory.Pentagon {C : Type u} [Category.{v, u} C] [MonoidalCategoryStruct C] (Y₁ Y₂ Y₃ Y₄ : C) :
Prop

The property that the pentagon relation is satisfied by four objects in a category equipped with a `MonoidalCategoryStruct`.

Equations

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

Instances For

source
class CategoryTheory.MonoidalCategory (C : Type u) [𝒞 : Category.{v, u} C] extends CategoryTheory.MonoidalCategoryStruct C :
Type (max u v)

In a monoidal category, we can take the tensor product of objects, `X ⊗ Y` and of morphisms `f ⊗ₘ g`. Tensor product does not need to be strictly associative on objects, but there is a specified associator, `α_ X Y Z : (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z)`. There is a tensor unit `𝟙_ C`, with specified left and right unitor isomorphisms `λ_ X : 𝟙_ C ⊗ X ≅ X` and `ρ_ X : X ⊗ 𝟙_ C ≅ X`. These associators and unitors satisfy the pentagon and triangle equations.

- tensorObj : C → C → C
- whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : tensorObj X Y₁ ⟶ tensorObj X Y₂
- whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y
- tensorHom {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂
- tensorUnit : C
- associator (X Y Z : C) : tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
- leftUnitor (X : C) : tensorObj (tensorUnit C) X ≅ X
- rightUnitor (X : C) : tensorObj X (tensorUnit C) ≅ X
- tensorHom_def {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorHom f g = CategoryStruct.comp (whiskerRight f X₂) (whiskerLeft Y₁ g)
- id_tensorHom_id (X₁ X₂ : C) : tensorHom (CategoryStruct.id X₁) (CategoryStruct.id X₂) = CategoryStruct.id (tensorObj X₁ X₂)

  Tensor product of identity maps is the identity: `𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)`

- tensorHom_comp_tensorHom {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂) = tensorHom (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ g₂)

  Composition of tensor products is tensor product of compositions: `(f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = (f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂)`

- whiskerLeft_id (X Y : C) : whiskerLeft X (CategoryStruct.id Y) = CategoryStruct.id (tensorObj X Y)
- id_whiskerRight (X Y : C) : whiskerRight (CategoryStruct.id X) Y = CategoryStruct.id (tensorObj X Y)
- associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (associator X₁ X₂ X₃).hom (tensorHom f₁ (tensorHom f₂ f₃))

  Naturality of the associator isomorphism: `(f₁ ⊗ₘ f₂) ⊗ₘ f₃ ≃ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)`

- leftUnitor_naturality {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (whiskerLeft (tensorUnit C) f) (leftUnitor Y).hom = CategoryStruct.comp (leftUnitor X).hom f

  Naturality of the left unitor, commutativity of `𝟙_ C ⊗ X ⟶ 𝟙_ C ⊗ Y ⟶ Y` and `𝟙_ C ⊗ X ⟶ X ⟶ Y`

- rightUnitor_naturality {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (whiskerRight f (tensorUnit C)) (rightUnitor Y).hom = CategoryStruct.comp (rightUnitor X).hom f

  Naturality of the right unitor: commutativity of `X ⊗ 𝟙_ C ⟶ Y ⊗ 𝟙_ C ⟶ Y` and `X ⊗ 𝟙_ C ⟶ X ⟶ Y`

- pentagon (W X Y Z : C) : CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) (CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (whiskerLeft W (associator X Y Z).hom)) = CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (associator W X (tensorObj Y Z)).hom

  The pentagon identity relating the isomorphism between `X ⊗ (Y ⊗ (Z ⊗ W))` and `((X ⊗ Y) ⊗ Z) ⊗ W`

- triangle (X Y : C) : CategoryStruct.comp (associator X (tensorUnit C) Y).hom (whiskerLeft X (leftUnitor Y).hom) = whiskerRight (rightUnitor X).hom Y

  The identity relating the isomorphisms between `X ⊗ (𝟙_ C ⊗ Y)`, `(X ⊗ 𝟙_ C) ⊗ Y` and `X ⊗ Y`

Instances

source
theorem CategoryTheory.MonoidalCategory.tensorHom_def_assoc {C : Type u} {𝒞 : Category.{v, u} C} [self : MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) {Z : C} (h : tensorObj Y₁ Y₂ ⟶ Z) :
CategoryStruct.comp (tensorHom f g) h = CategoryStruct.comp (whiskerRight f X₂) (CategoryStruct.comp (whiskerLeft Y₁ g) h)
source
theorem CategoryTheory.MonoidalCategory.whiskerLeft_id_assoc {C : Type u} {𝒞 : Category.{v, u} C} [self : MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X Y ⟶ Z) :
CategoryStruct.comp (whiskerLeft X (CategoryStruct.id Y)) h = h
source
theorem CategoryTheory.MonoidalCategory.id_whiskerRight_assoc {C : Type u} {𝒞 : Category.{v, u} C} [self : MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X Y ⟶ Z) :
CategoryStruct.comp (whiskerRight (CategoryStruct.id X) Y) h = h
source
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc {C : Type u} {𝒞 : Category.{v, u} C} [self : MonoidalCategory C] {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) {Z : C} (h : tensorObj Z₁ Z₂ ⟶ Z) :
CategoryStruct.comp (tensorHom f₁ f₂) (CategoryStruct.comp (tensorHom g₁ g₂) h) = CategoryStruct.comp (tensorHom (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ g₂)) h
source
theorem CategoryTheory.MonoidalCategory.associator_naturality_assoc {C : Type u} {𝒞 : Category.{v, u} C} [self : MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) {Z : C} (h : tensorObj Y₁ (tensorObj Y₂ Y₃) ⟶ Z) :
CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (CategoryStruct.comp (associator Y₁ Y₂ Y₃).hom h) = CategoryStruct.comp (associator X₁ X₂ X₃).hom (CategoryStruct.comp (tensorHom f₁ (tensorHom f₂ f₃)) h)
source
theorem CategoryTheory.MonoidalCategory.leftUnitor_naturality_assoc {C : Type u} {𝒞 : Category.{v, u} C} [self : MonoidalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) :
CategoryStruct.comp (whiskerLeft (tensorUnit C) f) (CategoryStruct.comp (leftUnitor Y).hom h) = CategoryStruct.comp (leftUnitor X).hom (CategoryStruct.comp f h)
source
theorem CategoryTheory.MonoidalCategory.rightUnitor_naturality_assoc {C : Type u} {𝒞 : Category.{v, u} C} [self : MonoidalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) :
CategoryStruct.comp (whiskerRight f (tensorUnit C)) (CategoryStruct.comp (rightUnitor Y).hom h) = CategoryStruct.comp (rightUnitor X).hom (CategoryStruct.comp f h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_assoc {C : Type u} {𝒞 : Category.{v, u} C} [self : MonoidalCategory C] (W X Y Z : C) {Z✝ : C} (h : tensorObj W (tensorObj X (tensorObj Y Z)) ⟶ Z✝) :
CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) (CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (CategoryStruct.comp (whiskerLeft W (associator X Y Z).hom) h)) = CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (CategoryStruct.comp (associator W X (tensorObj Y Z)).hom h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.triangle_assoc {C : Type u} {𝒞 : Category.{v, u} C} [self : MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X Y ⟶ Z) :
CategoryStruct.comp (associator X (tensorUnit C) Y).hom (CategoryStruct.comp (whiskerLeft X (leftUnitor Y).hom) h) = CategoryStruct.comp (whiskerRight (rightUnitor X).hom Y) h
source
@[simp]
theorem CategoryTheory.MonoidalCategory.id_tensorHom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) :
tensorHom (CategoryStruct.id X) f = whiskerLeft X f
source
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorHom_id {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
tensorHom f (CategoryStruct.id Y) = whiskerRight f Y
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_comp {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (W : C) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
whiskerLeft W (CategoryStruct.comp f g) = CategoryStruct.comp (whiskerLeft W f) (whiskerLeft W g)
source
theorem CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (W : C) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : tensorObj W Z ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft W (CategoryStruct.comp f g)) h = CategoryStruct.comp (whiskerLeft W f) (CategoryStruct.comp (whiskerLeft W g) h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.id_whiskerLeft {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) :
whiskerLeft (tensorUnit C) f = CategoryStruct.comp (leftUnitor X).hom (CategoryStruct.comp f (leftUnitor Y).inv)
source
theorem CategoryTheory.MonoidalCategory.id_whiskerLeft_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : tensorObj (tensorUnit C) Y ⟶ Z) :
CategoryStruct.comp (whiskerLeft (tensorUnit C) f) h = CategoryStruct.comp (leftUnitor X).hom (CategoryStruct.comp f (CategoryStruct.comp (leftUnitor Y).inv h))
source
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_whiskerLeft {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
whiskerLeft (tensorObj X Y) f = CategoryStruct.comp (associator X Y Z).hom (CategoryStruct.comp (whiskerLeft X (whiskerLeft Y f)) (associator X Y Z').inv)
source
theorem CategoryTheory.MonoidalCategory.tensor_whiskerLeft_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z Z' : C} (f : Z ⟶ Z') {Z✝ : C} (h : tensorObj (tensorObj X Y) Z' ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft (tensorObj X Y) f) h = CategoryStruct.comp (associator X Y Z).hom (CategoryStruct.comp (whiskerLeft X (whiskerLeft Y f)) (CategoryStruct.comp (associator X Y Z').inv h))
source
@[simp]
theorem CategoryTheory.MonoidalCategory.comp_whiskerRight {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y : C} (f : W ⟶ X) (g : X ⟶ Y) (Z : C) :
whiskerRight (CategoryStruct.comp f g) Z = CategoryStruct.comp (whiskerRight f Z) (whiskerRight g Z)
source
theorem CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y : C} (f : W ⟶ X) (g : X ⟶ Y) (Z : C) {Z✝ : C} (h : tensorObj Y Z ⟶ Z✝) :
CategoryStruct.comp (whiskerRight (CategoryStruct.comp f g) Z) h = CategoryStruct.comp (whiskerRight f Z) (CategoryStruct.comp (whiskerRight g Z) h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRight_id {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) :
whiskerRight f (tensorUnit C) = CategoryStruct.comp (rightUnitor X).hom (CategoryStruct.comp f (rightUnitor Y).inv)
source
theorem CategoryTheory.MonoidalCategory.whiskerRight_id_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : tensorObj Y (tensorUnit C) ⟶ Z) :
CategoryStruct.comp (whiskerRight f (tensorUnit C)) h = CategoryStruct.comp (rightUnitor X).hom (CategoryStruct.comp f (CategoryStruct.comp (rightUnitor Y).inv h))
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRight_tensor {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' : C} (f : X ⟶ X') (Y Z : C) :
whiskerRight f (tensorObj Y Z) = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (whiskerRight (whiskerRight f Y) Z) (associator X' Y Z).hom)
source
theorem CategoryTheory.MonoidalCategory.whiskerRight_tensor_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' : C} (f : X ⟶ X') (Y Z : C) {Z✝ : C} (h : tensorObj X' (tensorObj Y Z) ⟶ Z✝) :
CategoryStruct.comp (whiskerRight f (tensorObj Y Z)) h = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (whiskerRight (whiskerRight f Y) Z) (CategoryStruct.comp (associator X' Y Z).hom h))
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whisker_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
whiskerRight (whiskerLeft X f) Z = CategoryStruct.comp (associator X Y Z).hom (CategoryStruct.comp (whiskerLeft X (whiskerRight f Z)) (associator X Y' Z).inv)
source
theorem CategoryTheory.MonoidalCategory.whisker_assoc_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) {Z✝ : C} (h : tensorObj (tensorObj X Y') Z ⟶ Z✝) :
CategoryStruct.comp (whiskerRight (whiskerLeft X f) Z) h = CategoryStruct.comp (associator X Y Z).hom (CategoryStruct.comp (whiskerLeft X (whiskerRight f Z)) (CategoryStruct.comp (associator X Y' Z).inv h))
source
theorem CategoryTheory.MonoidalCategory.whisker_exchange {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) :
CategoryStruct.comp (whiskerLeft W g) (whiskerRight f Z) = CategoryStruct.comp (whiskerRight f Y) (whiskerLeft X g)
source
theorem CategoryTheory.MonoidalCategory.whisker_exchange_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) {Z✝ : C} (h : tensorObj X Z ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft W g) (CategoryStruct.comp (whiskerRight f Z) h) = CategoryStruct.comp (whiskerRight f Y) (CategoryStruct.comp (whiskerLeft X g) h)
source
theorem CategoryTheory.MonoidalCategory.tensorHom_def' {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
tensorHom f g = CategoryStruct.comp (whiskerLeft X₁ g) (whiskerRight f Y₂)
source
theorem CategoryTheory.MonoidalCategory.tensorHom_def'_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) {Z : C} (h : tensorObj Y₁ Y₂ ⟶ Z) :
CategoryStruct.comp (tensorHom f g) h = CategoryStruct.comp (whiskerLeft X₁ g) (CategoryStruct.comp (whiskerRight f Y₂) h)
source
theorem CategoryTheory.MonoidalCategory.whiskerLeft_comp_tensorHom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
CategoryStruct.comp (whiskerLeft V g) (tensorHom f h) = tensorHom f (CategoryStruct.comp g h)
source
theorem CategoryTheory.MonoidalCategory.whiskerLeft_comp_tensorHom_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z✝ : C} (h✝ : tensorObj W Z ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft V g) (CategoryStruct.comp (tensorHom f h) h✝) = CategoryStruct.comp (tensorHom f (CategoryStruct.comp g h)) h✝
source
theorem CategoryTheory.MonoidalCategory.whiskerRight_comp_tensorHom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : V ⟶ W) :
CategoryStruct.comp (whiskerRight f V) (tensorHom g h) = tensorHom (CategoryStruct.comp f g) h
source
theorem CategoryTheory.MonoidalCategory.whiskerRight_comp_tensorHom_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : V ⟶ W) {Z✝ : C} (h✝ : tensorObj Z W ⟶ Z✝) :
CategoryStruct.comp (whiskerRight f V) (CategoryStruct.comp (tensorHom g h) h✝) = CategoryStruct.comp (tensorHom (CategoryStruct.comp f g) h) h✝
source
theorem CategoryTheory.MonoidalCategory.tensorHom_comp_whiskerLeft {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
CategoryStruct.comp (tensorHom f g) (whiskerLeft W h) = tensorHom f (CategoryStruct.comp g h)
source
theorem CategoryTheory.MonoidalCategory.tensorHom_comp_whiskerLeft_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z✝ : C} (h✝ : tensorObj W Z ⟶ Z✝) :
CategoryStruct.comp (tensorHom f g) (CategoryStruct.comp (whiskerLeft W h) h✝) = CategoryStruct.comp (tensorHom f (CategoryStruct.comp g h)) h✝
source
theorem CategoryTheory.MonoidalCategory.tensorHom_comp_whiskerRight {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : V ⟶ W) :
CategoryStruct.comp (tensorHom f h) (whiskerRight g W) = tensorHom (CategoryStruct.comp f g) h
source
theorem CategoryTheory.MonoidalCategory.tensorHom_comp_whiskerRight_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : V ⟶ W) {Z✝ : C} (h✝ : tensorObj Z W ⟶ Z✝) :
CategoryStruct.comp (tensorHom f h) (CategoryStruct.comp (whiskerRight g W) h✝) = CategoryStruct.comp (tensorHom (CategoryStruct.comp f g) h) h✝
source
theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_comp_tensorHom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y Z : C} (f : tensorUnit C ⟶ Y) (g : X ⟶ Z) :
CategoryStruct.comp (leftUnitor X).inv (tensorHom f g) = CategoryStruct.comp g (CategoryStruct.comp (leftUnitor Z).inv (whiskerRight f Z))
source
theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_comp_tensorHom_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y Z : C} (f : tensorUnit C ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : tensorObj Y Z ⟶ Z✝) :
CategoryStruct.comp (leftUnitor X).inv (CategoryStruct.comp (tensorHom f g) h) = CategoryStruct.comp g (CategoryStruct.comp (leftUnitor Z).inv (CategoryStruct.comp (whiskerRight f Z) h))
source
theorem CategoryTheory.MonoidalCategory.rightUnitor_inv_comp_tensorHom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y Z : C} (f : X ⟶ Y) (g : tensorUnit C ⟶ Z) :
CategoryStruct.comp (rightUnitor X).inv (tensorHom f g) = CategoryStruct.comp f (CategoryStruct.comp (rightUnitor Y).inv (whiskerLeft Y g))
source
theorem CategoryTheory.MonoidalCategory.rightUnitor_inv_comp_tensorHom_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y Z : C} (f : X ⟶ Y) (g : tensorUnit C ⟶ Z) {Z✝ : C} (h : tensorObj Y Z ⟶ Z✝) :
CategoryStruct.comp (rightUnitor X).inv (CategoryStruct.comp (tensorHom f g) h) = CategoryStruct.comp f (CategoryStruct.comp (rightUnitor Y).inv (CategoryStruct.comp (whiskerLeft Y g) h))
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ≅ Z) :
CategoryStruct.comp (whiskerLeft X f.hom) (whiskerLeft X f.inv) = CategoryStruct.id (tensorObj X Y)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ≅ Z) {Z✝ : C} (h : tensorObj X Y ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft X f.hom) (CategoryStruct.comp (whiskerLeft X f.inv) h) = h
source
@[simp]
theorem CategoryTheory.MonoidalCategory.hom_inv_whiskerRight {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ≅ Y) (Z : C) :
CategoryStruct.comp (whiskerRight f.hom Z) (whiskerRight f.inv Z) = CategoryStruct.id (tensorObj X Z)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.hom_inv_whiskerRight_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ≅ Y) (Z : C) {Z✝ : C} (h : tensorObj X Z ⟶ Z✝) :
CategoryStruct.comp (whiskerRight f.hom Z) (CategoryStruct.comp (whiskerRight f.inv Z) h) = h
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ≅ Z) :
CategoryStruct.comp (whiskerLeft X f.inv) (whiskerLeft X f.hom) = CategoryStruct.id (tensorObj X Z)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ≅ Z) {Z✝ : C} (h : tensorObj X Z ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft X f.inv) (CategoryStruct.comp (whiskerLeft X f.hom) h) = h
source
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_hom_whiskerRight {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ≅ Y) (Z : C) :
CategoryStruct.comp (whiskerRight f.inv Z) (whiskerRight f.hom Z) = CategoryStruct.id (tensorObj Y Z)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_hom_whiskerRight_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ≅ Y) (Z : C) {Z✝ : C} (h : tensorObj Y Z ⟶ Z✝) :
CategoryStruct.comp (whiskerRight f.inv Z) (CategoryStruct.comp (whiskerRight f.hom Z) h) = h
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv' {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
CategoryStruct.comp (whiskerLeft X f) (whiskerLeft X (inv f)) = CategoryStruct.id (tensorObj X Y)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv'_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] {Z✝ : C} (h : tensorObj X Y ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft X f) (CategoryStruct.comp (whiskerLeft X (inv f)) h) = h
source
@[simp]
theorem CategoryTheory.MonoidalCategory.hom_inv_whiskerRight' {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) [IsIso f] (Z : C) :
CategoryStruct.comp (whiskerRight f Z) (whiskerRight (inv f) Z) = CategoryStruct.id (tensorObj X Z)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.hom_inv_whiskerRight'_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) [IsIso f] (Z : C) {Z✝ : C} (h : tensorObj X Z ⟶ Z✝) :
CategoryStruct.comp (whiskerRight f Z) (CategoryStruct.comp (whiskerRight (inv f) Z) h) = h
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom' {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
CategoryStruct.comp (whiskerLeft X (inv f)) (whiskerLeft X f) = CategoryStruct.id (tensorObj X Z)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom'_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] {Z✝ : C} (h : tensorObj X Z ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft X (inv f)) (CategoryStruct.comp (whiskerLeft X f) h) = h
source
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_hom_whiskerRight' {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) [IsIso f] (Z : C) :
CategoryStruct.comp (whiskerRight (inv f) Z) (whiskerRight f Z) = CategoryStruct.id (tensorObj Y Z)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_hom_whiskerRight'_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) [IsIso f] (Z : C) {Z✝ : C} (h : tensorObj Y Z ⟶ Z✝) :
CategoryStruct.comp (whiskerRight (inv f) Z) (CategoryStruct.comp (whiskerRight f Z) h) = h
source
def CategoryTheory.MonoidalCategory.whiskerLeftIso {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ≅ Z) :
tensorObj X Y ≅ tensorObj X Z

The left whiskering of an isomorphism is an isomorphism.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ≅ Z) :
(whiskerLeftIso X f).inv = whiskerLeft X f.inv
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_hom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ≅ Z) :
(whiskerLeftIso X f).hom = whiskerLeft X f.hom
source
instance CategoryTheory.MonoidalCategory.whiskerLeft_isIso {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
IsIso (whiskerLeft X f)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_whiskerLeft {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
inv (whiskerLeft X f) = whiskerLeft X (inv f)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_refl {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (W X : C) :
whiskerLeftIso W (Iso.refl X) = Iso.refl (tensorObj W X)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_trans {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (W : C) {X Y Z : C} (f : X ≅ Y) (g : Y ≅ Z) :
whiskerLeftIso W (f ≪≫ g) = whiskerLeftIso W f ≪≫ whiskerLeftIso W g
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_symm {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (W : C) {X Y : C} (f : X ≅ Y) :
(whiskerLeftIso W f).symm = whiskerLeftIso W f.symm
source
def CategoryTheory.MonoidalCategory.whiskerRightIso {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ≅ Y) (Z : C) :
tensorObj X Z ≅ tensorObj Y Z

The right whiskering of an isomorphism is an isomorphism.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRightIso_hom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ≅ Y) (Z : C) :
(whiskerRightIso f Z).hom = whiskerRight f.hom Z
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRightIso_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ≅ Y) (Z : C) :
(whiskerRightIso f Z).inv = whiskerRight f.inv Z
source
instance CategoryTheory.MonoidalCategory.whiskerRight_isIso {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) [IsIso f] :
IsIso (whiskerRight f Z)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_whiskerRight {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) [IsIso f] :
inv (whiskerRight f Z) = whiskerRight (inv f) Z
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRightIso_refl {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X W : C) :
whiskerRightIso (Iso.refl X) W = Iso.refl (tensorObj X W)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRightIso_trans {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y Z : C} (f : X ≅ Y) (g : Y ≅ Z) (W : C) :
whiskerRightIso (f ≪≫ g) W = whiskerRightIso f W ≪≫ whiskerRightIso g W
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerRightIso_symm {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ≅ Y) (W : C) :
(whiskerRightIso f W).symm = whiskerRightIso f.symm W
source
def CategoryTheory.MonoidalCategory.tensorIso {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y X' Y' : C} (f : X ≅ Y) (g : X' ≅ Y') :
tensorObj X X' ≅ tensorObj Y Y'

The tensor product of two isomorphisms is an isomorphism.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorIso_hom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y X' Y' : C} (f : X ≅ Y) (g : X' ≅ Y') :
(tensorIso f g).hom = tensorHom f.hom g.hom
source
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorIso_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y X' Y' : C} (f : X ≅ Y) (g : X' ≅ Y') :
(tensorIso f g).inv = tensorHom f.inv g.inv
source
def CategoryTheory.MonoidalCategory.«term_⊗ᵢ_» :
Lean.TrailingParserDescr

Notation for `tensorIso`, the tensor product of isomorphisms

Equations

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

Instances For

source
theorem CategoryTheory.MonoidalCategory.tensorIso_def {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y X' Y' : C} (f : X ≅ Y) (g : X' ≅ Y') :
tensorIso f g = whiskerRightIso f X' ≪≫ whiskerLeftIso Y g
source
theorem CategoryTheory.MonoidalCategory.tensorIso_def' {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y X' Y' : C} (f : X ≅ Y) (g : X' ≅ Y') :
tensorIso f g = whiskerLeftIso X g ≪≫ whiskerRightIso f Y'
source
instance CategoryTheory.MonoidalCategory.tensor_isIso {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) [IsIso f] (g : Y ⟶ Z) [IsIso g] :
IsIso (tensorHom f g)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.inv_tensor {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) [IsIso f] (g : Y ⟶ Z) [IsIso g] :
inv (tensorHom f g) = tensorHom (inv f) (inv g)
source
theorem CategoryTheory.MonoidalCategory.whiskerLeft_dite {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {P : Prop} [Decidable P] (X : C) {Y Z : C} (f : P → (Y ⟶ Z)) (f' : ¬P → (Y ⟶ Z)) :
whiskerLeft X (if h : P then f h else f' h) = if h : P then whiskerLeft X (f h) else whiskerLeft X (f' h)
source
theorem CategoryTheory.MonoidalCategory.dite_whiskerRight {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {P : Prop} [Decidable P] {X Y : C} (f : P → (X ⟶ Y)) (f' : ¬P → (X ⟶ Y)) (Z : C) :
whiskerRight (if h : P then f h else f' h) Z = if h : P then whiskerRight (f h) Z else whiskerRight (f' h) Z
source
theorem CategoryTheory.MonoidalCategory.tensor_dite {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {P : Prop} [Decidable P] {W X Y Z : C} (f : W ⟶ X) (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)) :
tensorHom f (if h : P then g h else g' h) = if h : P then tensorHom f (g h) else tensorHom f (g' h)
source
theorem CategoryTheory.MonoidalCategory.dite_tensor {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {P : Prop} [Decidable P] {W X Y Z : C} (f : W ⟶ X) (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)) :
tensorHom (if h : P then g h else g' h) f = if h : P then tensorHom (g h) f else tensorHom (g' h) f
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_eqToHom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Z : C} (f : Y = Z) :
whiskerLeft X (eqToHom f) = eqToHom ⋯
source
@[simp]
theorem CategoryTheory.MonoidalCategory.eqToHom_whiskerRight {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X = Y) (Z : C) :
whiskerRight (eqToHom f) Z = eqToHom ⋯
source
theorem CategoryTheory.MonoidalCategory.associator_naturality_left {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' : C} (f : X ⟶ X') (Y Z : C) :
CategoryStruct.comp (whiskerRight (whiskerRight f Y) Z) (associator X' Y Z).hom = CategoryStruct.comp (associator X Y Z).hom (whiskerRight f (tensorObj Y Z))
source
theorem CategoryTheory.MonoidalCategory.associator_naturality_left_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' : C} (f : X ⟶ X') (Y Z : C) {Z✝ : C} (h : tensorObj X' (tensorObj Y Z) ⟶ Z✝) :
CategoryStruct.comp (whiskerRight (whiskerRight f Y) Z) (CategoryStruct.comp (associator X' Y Z).hom h) = CategoryStruct.comp (associator X Y Z).hom (CategoryStruct.comp (whiskerRight f (tensorObj Y Z)) h)
source
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_left {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' : C} (f : X ⟶ X') (Y Z : C) :
CategoryStruct.comp (whiskerRight f (tensorObj Y Z)) (associator X' Y Z).inv = CategoryStruct.comp (associator X Y Z).inv (whiskerRight (whiskerRight f Y) Z)
source
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_left_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' : C} (f : X ⟶ X') (Y Z : C) {Z✝ : C} (h : tensorObj (tensorObj X' Y) Z ⟶ Z✝) :
CategoryStruct.comp (whiskerRight f (tensorObj Y Z)) (CategoryStruct.comp (associator X' Y Z).inv h) = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (whiskerRight (whiskerRight f Y) Z) h)
source
theorem CategoryTheory.MonoidalCategory.whiskerRight_tensor_symm {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' : C} (f : X ⟶ X') (Y Z : C) :
whiskerRight (whiskerRight f Y) Z = CategoryStruct.comp (associator X Y Z).hom (CategoryStruct.comp (whiskerRight f (tensorObj Y Z)) (associator X' Y Z).inv)
source
theorem CategoryTheory.MonoidalCategory.whiskerRight_tensor_symm_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' : C} (f : X ⟶ X') (Y Z : C) {Z✝ : C} (h : tensorObj (tensorObj X' Y) Z ⟶ Z✝) :
CategoryStruct.comp (whiskerRight (whiskerRight f Y) Z) h = CategoryStruct.comp (associator X Y Z).hom (CategoryStruct.comp (whiskerRight f (tensorObj Y Z)) (CategoryStruct.comp (associator X' Y Z).inv h))
source
theorem CategoryTheory.MonoidalCategory.associator_naturality_middle {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
CategoryStruct.comp (whiskerRight (whiskerLeft X f) Z) (associator X Y' Z).hom = CategoryStruct.comp (associator X Y Z).hom (whiskerLeft X (whiskerRight f Z))
source
theorem CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) {Z✝ : C} (h : tensorObj X (tensorObj Y' Z) ⟶ Z✝) :
CategoryStruct.comp (whiskerRight (whiskerLeft X f) Z) (CategoryStruct.comp (associator X Y' Z).hom h) = CategoryStruct.comp (associator X Y Z).hom (CategoryStruct.comp (whiskerLeft X (whiskerRight f Z)) h)
source
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_middle {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
CategoryStruct.comp (whiskerLeft X (whiskerRight f Z)) (associator X Y' Z).inv = CategoryStruct.comp (associator X Y Z).inv (whiskerRight (whiskerLeft X f) Z)
source
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) {Z✝ : C} (h : tensorObj (tensorObj X Y') Z ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft X (whiskerRight f Z)) (CategoryStruct.comp (associator X Y' Z).inv h) = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (whiskerRight (whiskerLeft X f) Z) h)
source
theorem CategoryTheory.MonoidalCategory.whisker_assoc_symm {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
whiskerLeft X (whiskerRight f Z) = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (whiskerRight (whiskerLeft X f) Z) (associator X Y' Z).hom)
source
theorem CategoryTheory.MonoidalCategory.whisker_assoc_symm_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) {Z✝ : C} (h : tensorObj X (tensorObj Y' Z) ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft X (whiskerRight f Z)) h = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (whiskerRight (whiskerLeft X f) Z) (CategoryStruct.comp (associator X Y' Z).hom h))
source
theorem CategoryTheory.MonoidalCategory.associator_naturality_right {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
CategoryStruct.comp (whiskerLeft (tensorObj X Y) f) (associator X Y Z').hom = CategoryStruct.comp (associator X Y Z).hom (whiskerLeft X (whiskerLeft Y f))
source
theorem CategoryTheory.MonoidalCategory.associator_naturality_right_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z Z' : C} (f : Z ⟶ Z') {Z✝ : C} (h : tensorObj X (tensorObj Y Z') ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft (tensorObj X Y) f) (CategoryStruct.comp (associator X Y Z').hom h) = CategoryStruct.comp (associator X Y Z).hom (CategoryStruct.comp (whiskerLeft X (whiskerLeft Y f)) h)
source
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_right {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
CategoryStruct.comp (whiskerLeft X (whiskerLeft Y f)) (associator X Y Z').inv = CategoryStruct.comp (associator X Y Z).inv (whiskerLeft (tensorObj X Y) f)
source
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z Z' : C} (f : Z ⟶ Z') {Z✝ : C} (h : tensorObj (tensorObj X Y) Z' ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft X (whiskerLeft Y f)) (CategoryStruct.comp (associator X Y Z').inv h) = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (whiskerLeft (tensorObj X Y) f) h)
source
theorem CategoryTheory.MonoidalCategory.tensor_whiskerLeft_symm {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
whiskerLeft X (whiskerLeft Y f) = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (whiskerLeft (tensorObj X Y) f) (associator X Y Z').hom)
source
theorem CategoryTheory.MonoidalCategory.tensor_whiskerLeft_symm_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z Z' : C} (f : Z ⟶ Z') {Z✝ : C} (h : tensorObj X (tensorObj Y Z') ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft X (whiskerLeft Y f)) h = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (whiskerLeft (tensorObj X Y) f) (CategoryStruct.comp (associator X Y Z').hom h))
source
theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) :
CategoryStruct.comp f (leftUnitor Y).inv = CategoryStruct.comp (leftUnitor X).inv (whiskerLeft (tensorUnit C) f)
source
theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : tensorObj (tensorUnit C) Y ⟶ Z) :
CategoryStruct.comp f (CategoryStruct.comp (leftUnitor Y).inv h) = CategoryStruct.comp (leftUnitor X).inv (CategoryStruct.comp (whiskerLeft (tensorUnit C) f) h)
source
theorem CategoryTheory.MonoidalCategory.id_whiskerLeft_symm {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' : C} (f : X ⟶ X') :
f = CategoryStruct.comp (leftUnitor X).inv (CategoryStruct.comp (whiskerLeft (tensorUnit C) f) (leftUnitor X').hom)
source
theorem CategoryTheory.MonoidalCategory.id_whiskerLeft_symm_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' : C} (f : X ⟶ X') {Z : C} (h : X' ⟶ Z) :
CategoryStruct.comp f h = CategoryStruct.comp (leftUnitor X).inv (CategoryStruct.comp (whiskerLeft (tensorUnit C) f) (CategoryStruct.comp (leftUnitor X').hom h))
source
theorem CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' : C} (f : X ⟶ X') :
CategoryStruct.comp f (rightUnitor X').inv = CategoryStruct.comp (rightUnitor X).inv (whiskerRight f (tensorUnit C))
source
theorem CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' : C} (f : X ⟶ X') {Z : C} (h : tensorObj X' (tensorUnit C) ⟶ Z) :
CategoryStruct.comp f (CategoryStruct.comp (rightUnitor X').inv h) = CategoryStruct.comp (rightUnitor X).inv (CategoryStruct.comp (whiskerRight f (tensorUnit C)) h)
source
theorem CategoryTheory.MonoidalCategory.whiskerRight_id_symm {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) :
f = CategoryStruct.comp (rightUnitor X).inv (CategoryStruct.comp (whiskerRight f (tensorUnit C)) (rightUnitor Y).hom)
source
theorem CategoryTheory.MonoidalCategory.whiskerRight_id_symm_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) :
CategoryStruct.comp f h = CategoryStruct.comp (rightUnitor X).inv (CategoryStruct.comp (whiskerRight f (tensorUnit C)) (CategoryStruct.comp (rightUnitor Y).hom h))
source
theorem CategoryTheory.MonoidalCategory.whiskerLeft_iff {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f g : X ⟶ Y) :
whiskerLeft (tensorUnit C) f = whiskerLeft (tensorUnit C) g ↔ f = g
source
theorem CategoryTheory.MonoidalCategory.whiskerRight_iff {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f g : X ⟶ Y) :
whiskerRight f (tensorUnit C) = whiskerRight g (tensorUnit C) ↔ f = g

The lemmas in the next section are true by coherence, but we prove them directly as they are used in proving the coherence theorem.

source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} :
CategoryStruct.comp (whiskerLeft W (associator X Y Z).inv) (CategoryStruct.comp (associator W (tensorObj X Y) Z).inv (whiskerRight (associator W X Y).inv Z)) = CategoryStruct.comp (associator W X (tensorObj Y Z)).inv (associator (tensorObj W X) Y Z).inv
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z Z✝ : C} (h : tensorObj (tensorObj (tensorObj W X) Y) Z ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft W (associator X Y Z).inv) (CategoryStruct.comp (associator W (tensorObj X Y) Z).inv (CategoryStruct.comp (whiskerRight (associator W X Y).inv Z) h)) = CategoryStruct.comp (associator W X (tensorObj Y Z)).inv (CategoryStruct.comp (associator (tensorObj W X) Y Z).inv h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_hom_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} :
CategoryStruct.comp (associator W (tensorObj X Y) Z).inv (CategoryStruct.comp (whiskerRight (associator W X Y).inv Z) (associator (tensorObj W X) Y Z).hom) = CategoryStruct.comp (whiskerLeft W (associator X Y Z).hom) (associator W X (tensorObj Y Z)).inv
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_hom_inv_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z Z✝ : C} (h : tensorObj (tensorObj W X) (tensorObj Y Z) ⟶ Z✝) :
CategoryStruct.comp (associator W (tensorObj X Y) Z).inv (CategoryStruct.comp (whiskerRight (associator W X Y).inv Z) (CategoryStruct.comp (associator (tensorObj W X) Y Z).hom h)) = CategoryStruct.comp (whiskerLeft W (associator X Y Z).hom) (CategoryStruct.comp (associator W X (tensorObj Y Z)).inv h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} :
CategoryStruct.comp (associator (tensorObj W X) Y Z).inv (CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) (associator W (tensorObj X Y) Z).hom) = CategoryStruct.comp (associator W X (tensorObj Y Z)).hom (whiskerLeft W (associator X Y Z).inv)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_inv_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z Z✝ : C} (h : tensorObj W (tensorObj (tensorObj X Y) Z) ⟶ Z✝) :
CategoryStruct.comp (associator (tensorObj W X) Y Z).inv (CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) (CategoryStruct.comp (associator W (tensorObj X Y) Z).hom h)) = CategoryStruct.comp (associator W X (tensorObj Y Z)).hom (CategoryStruct.comp (whiskerLeft W (associator X Y Z).inv) h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} :
CategoryStruct.comp (whiskerLeft W (associator X Y Z).hom) (CategoryStruct.comp (associator W X (tensorObj Y Z)).inv (associator (tensorObj W X) Y Z).inv) = CategoryStruct.comp (associator W (tensorObj X Y) Z).inv (whiskerRight (associator W X Y).inv Z)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_inv_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z Z✝ : C} (h : tensorObj (tensorObj (tensorObj W X) Y) Z ⟶ Z✝) :
CategoryStruct.comp (whiskerLeft W (associator X Y Z).hom) (CategoryStruct.comp (associator W X (tensorObj Y Z)).inv (CategoryStruct.comp (associator (tensorObj W X) Y Z).inv h)) = CategoryStruct.comp (associator W (tensorObj X Y) Z).inv (CategoryStruct.comp (whiskerRight (associator W X Y).inv Z) h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_hom_inv_hom_hom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} :
CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (CategoryStruct.comp (associator W X (tensorObj Y Z)).hom (whiskerLeft W (associator X Y Z).inv)) = CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) (associator W (tensorObj X Y) Z).hom
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_hom_inv_hom_hom_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z Z✝ : C} (h : tensorObj W (tensorObj (tensorObj X Y) Z) ⟶ Z✝) :
CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (CategoryStruct.comp (associator W X (tensorObj Y Z)).hom (CategoryStruct.comp (whiskerLeft W (associator X Y Z).inv) h)) = CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) (CategoryStruct.comp (associator W (tensorObj X Y) Z).hom h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_hom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} :
CategoryStruct.comp (associator W X (tensorObj Y Z)).hom (CategoryStruct.comp (whiskerLeft W (associator X Y Z).inv) (associator W (tensorObj X Y) Z).inv) = CategoryStruct.comp (associator (tensorObj W X) Y Z).inv (whiskerRight (associator W X Y).hom Z)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_hom_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z Z✝ : C} (h : tensorObj (tensorObj W (tensorObj X Y)) Z ⟶ Z✝) :
CategoryStruct.comp (associator W X (tensorObj Y Z)).hom (CategoryStruct.comp (whiskerLeft W (associator X Y Z).inv) (CategoryStruct.comp (associator W (tensorObj X Y) Z).inv h)) = CategoryStruct.comp (associator (tensorObj W X) Y Z).inv (CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_hom_inv_inv_hom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} :
CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (CategoryStruct.comp (whiskerLeft W (associator X Y Z).hom) (associator W X (tensorObj Y Z)).inv) = CategoryStruct.comp (whiskerRight (associator W X Y).inv Z) (associator (tensorObj W X) Y Z).hom
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_hom_inv_inv_hom_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z Z✝ : C} (h : tensorObj (tensorObj W X) (tensorObj Y Z) ⟶ Z✝) :
CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (CategoryStruct.comp (whiskerLeft W (associator X Y Z).hom) (CategoryStruct.comp (associator W X (tensorObj Y Z)).inv h)) = CategoryStruct.comp (whiskerRight (associator W X Y).inv Z) (CategoryStruct.comp (associator (tensorObj W X) Y Z).hom h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_hom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} :
CategoryStruct.comp (whiskerRight (associator W X Y).inv Z) (CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (associator W X (tensorObj Y Z)).hom) = CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (whiskerLeft W (associator X Y Z).hom)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_hom_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z Z✝ : C} (h : tensorObj W (tensorObj X (tensorObj Y Z)) ⟶ Z✝) :
CategoryStruct.comp (whiskerRight (associator W X Y).inv Z) (CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (CategoryStruct.comp (associator W X (tensorObj Y Z)).hom h)) = CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (CategoryStruct.comp (whiskerLeft W (associator X Y Z).hom) h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_inv_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} :
CategoryStruct.comp (associator W X (tensorObj Y Z)).inv (CategoryStruct.comp (associator (tensorObj W X) Y Z).inv (whiskerRight (associator W X Y).hom Z)) = CategoryStruct.comp (whiskerLeft W (associator X Y Z).inv) (associator W (tensorObj X Y) Z).inv
source
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_inv_inv_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z Z✝ : C} (h : tensorObj (tensorObj W (tensorObj X Y)) Z ⟶ Z✝) :
CategoryStruct.comp (associator W X (tensorObj Y Z)).inv (CategoryStruct.comp (associator (tensorObj W X) Y Z).inv (CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) h)) = CategoryStruct.comp (whiskerLeft W (associator X Y Z).inv) (CategoryStruct.comp (associator W (tensorObj X Y) Z).inv h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
CategoryStruct.comp (associator X (tensorUnit C) Y).inv (whiskerRight (rightUnitor X).hom Y) = whiskerLeft X (leftUnitor Y).hom
source
@[simp]
theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X Y ⟶ Z) :
CategoryStruct.comp (associator X (tensorUnit C) Y).inv (CategoryStruct.comp (whiskerRight (rightUnitor X).hom Y) h) = CategoryStruct.comp (whiskerLeft X (leftUnitor Y).hom) h
source
@[simp]
theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
CategoryStruct.comp (whiskerRight (rightUnitor X).inv Y) (associator X (tensorUnit C) Y).hom = whiskerLeft X (leftUnitor Y).inv
source
@[simp]
theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X (tensorObj (tensorUnit C) Y) ⟶ Z) :
CategoryStruct.comp (whiskerRight (rightUnitor X).inv Y) (CategoryStruct.comp (associator X (tensorUnit C) Y).hom h) = CategoryStruct.comp (whiskerLeft X (leftUnitor Y).inv) h
source
@[simp]
theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
CategoryStruct.comp (whiskerLeft X (leftUnitor Y).inv) (associator X (tensorUnit C) Y).inv = whiskerRight (rightUnitor X).inv Y
source
@[simp]
theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj (tensorObj X (tensorUnit C)) Y ⟶ Z) :
CategoryStruct.comp (whiskerLeft X (leftUnitor Y).inv) (CategoryStruct.comp (associator X (tensorUnit C) Y).inv h) = CategoryStruct.comp (whiskerRight (rightUnitor X).inv Y) h
source
@[simp]
theorem CategoryTheory.MonoidalCategory.leftUnitor_whiskerRight {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
whiskerRight (leftUnitor X).hom Y = CategoryStruct.comp (associator (tensorUnit C) X Y).hom (leftUnitor (tensorObj X Y)).hom

We state it as a simp lemma, which is regarded as an involved version of `id_whiskerRight X Y : 𝟙 X ▷ Y = 𝟙 (X ⊗ Y)`.

source
theorem CategoryTheory.MonoidalCategory.leftUnitor_whiskerRight_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X Y ⟶ Z) :
CategoryStruct.comp (whiskerRight (leftUnitor X).hom Y) h = CategoryStruct.comp (associator (tensorUnit C) X Y).hom (CategoryStruct.comp (leftUnitor (tensorObj X Y)).hom h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_whiskerRight {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
whiskerRight (leftUnitor X).inv Y = CategoryStruct.comp (leftUnitor (tensorObj X Y)).inv (associator (tensorUnit C) X Y).inv
source
theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_whiskerRight_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj (tensorObj (tensorUnit C) X) Y ⟶ Z) :
CategoryStruct.comp (whiskerRight (leftUnitor X).inv Y) h = CategoryStruct.comp (leftUnitor (tensorObj X Y)).inv (CategoryStruct.comp (associator (tensorUnit C) X Y).inv h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
whiskerLeft X (rightUnitor Y).hom = CategoryStruct.comp (associator X Y (tensorUnit C)).inv (rightUnitor (tensorObj X Y)).hom
source
theorem CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X Y ⟶ Z) :
CategoryStruct.comp (whiskerLeft X (rightUnitor Y).hom) h = CategoryStruct.comp (associator X Y (tensorUnit C)).inv (CategoryStruct.comp (rightUnitor (tensorObj X Y)).hom h)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
whiskerLeft X (rightUnitor Y).inv = CategoryStruct.comp (rightUnitor (tensorObj X Y)).inv (associator X Y (tensorUnit C)).hom
source
theorem CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_inv_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X (tensorObj Y (tensorUnit C)) ⟶ Z) :
CategoryStruct.comp (whiskerLeft X (rightUnitor Y).inv) h = CategoryStruct.comp (rightUnitor (tensorObj X Y)).inv (CategoryStruct.comp (associator X Y (tensorUnit C)).hom h)
source
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
(leftUnitor (tensorObj X Y)).hom = CategoryStruct.comp (associator (tensorUnit C) X Y).inv (whiskerRight (leftUnitor X).hom Y)
source
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X Y ⟶ Z) :
CategoryStruct.comp (leftUnitor (tensorObj X Y)).hom h = CategoryStruct.comp (associator (tensorUnit C) X Y).inv (CategoryStruct.comp (whiskerRight (leftUnitor X).hom Y) h)
source
@[deprecated CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom (since := "2025-06-24")]
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
(leftUnitor (tensorObj X Y)).hom = CategoryStruct.comp (associator (tensorUnit C) X Y).inv (whiskerRight (leftUnitor X).hom Y)

Alias of `CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom`.

source
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
(leftUnitor (tensorObj X Y)).inv = CategoryStruct.comp (whiskerRight (leftUnitor X).inv Y) (associator (tensorUnit C) X Y).hom
source
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj (tensorUnit C) (tensorObj X Y) ⟶ Z) :
CategoryStruct.comp (leftUnitor (tensorObj X Y)).inv h = CategoryStruct.comp (whiskerRight (leftUnitor X).inv Y) (CategoryStruct.comp (associator (tensorUnit C) X Y).hom h)
source
theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor_hom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
(rightUnitor (tensorObj X Y)).hom = CategoryStruct.comp (associator X Y (tensorUnit C)).hom (whiskerLeft X (rightUnitor Y).hom)
source
theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor_hom_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X Y ⟶ Z) :
CategoryStruct.comp (rightUnitor (tensorObj X Y)).hom h = CategoryStruct.comp (associator X Y (tensorUnit C)).hom (CategoryStruct.comp (whiskerLeft X (rightUnitor Y).hom) h)
source
@[deprecated CategoryTheory.MonoidalCategory.rightUnitor_tensor_hom (since := "2025-06-24")]
theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
(rightUnitor (tensorObj X Y)).hom = CategoryStruct.comp (associator X Y (tensorUnit C)).hom (whiskerLeft X (rightUnitor Y).hom)

Alias of `CategoryTheory.MonoidalCategory.rightUnitor_tensor_hom`.

source
theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
(rightUnitor (tensorObj X Y)).inv = CategoryStruct.comp (whiskerLeft X (rightUnitor Y).inv) (associator X Y (tensorUnit C)).inv
source
theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj (tensorObj X Y) (tensorUnit C) ⟶ Z) :
CategoryStruct.comp (rightUnitor (tensorObj X Y)).inv h = CategoryStruct.comp (whiskerLeft X (rightUnitor Y).inv) (CategoryStruct.comp (associator X Y (tensorUnit C)).inv h)
source
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y Z X' Y' Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
CategoryStruct.comp (tensorHom f (tensorHom g h)) (associator X' Y' Z').inv = CategoryStruct.comp (associator X Y Z).inv (tensorHom (tensorHom f g) h)
source
theorem CategoryTheory.MonoidalCategory.associator_inv_naturality_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y Z X' Y' Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') {Z✝ : C} (h✝ : tensorObj (tensorObj X' Y') Z' ⟶ Z✝) :
CategoryStruct.comp (tensorHom f (tensorHom g h)) (CategoryStruct.comp (associator X' Y' Z').inv h✝) = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (tensorHom (tensorHom f g) h) h✝)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.associator_conjugation {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
tensorHom (tensorHom f g) h = CategoryStruct.comp (associator X Y Z).hom (CategoryStruct.comp (tensorHom f (tensorHom g h)) (associator X' Y' Z').inv)
source
theorem CategoryTheory.MonoidalCategory.associator_conjugation_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') {Z✝ : C} (h✝ : tensorObj (tensorObj X' Y') Z' ⟶ Z✝) :
CategoryStruct.comp (tensorHom (tensorHom f g) h) h✝ = CategoryStruct.comp (associator X Y Z).hom (CategoryStruct.comp (tensorHom f (tensorHom g h)) (CategoryStruct.comp (associator X' Y' Z').inv h✝))
source
theorem CategoryTheory.MonoidalCategory.associator_inv_conjugation {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
tensorHom f (tensorHom g h) = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (tensorHom (tensorHom f g) h) (associator X' Y' Z').hom)
source
theorem CategoryTheory.MonoidalCategory.associator_inv_conjugation_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') {Z✝ : C} (h✝ : tensorObj X' (tensorObj Y' Z') ⟶ Z✝) :
CategoryStruct.comp (tensorHom f (tensorHom g h)) h✝ = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (tensorHom (tensorHom f g) h) (CategoryStruct.comp (associator X' Y' Z').hom h✝))
source
theorem CategoryTheory.MonoidalCategory.id_tensor_associator_naturality {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y Z Z' : C} (h : Z ⟶ Z') :
CategoryStruct.comp (tensorHom (CategoryStruct.id (tensorObj X Y)) h) (associator X Y Z').hom = CategoryStruct.comp (associator X Y Z).hom (tensorHom (CategoryStruct.id X) (tensorHom (CategoryStruct.id Y) h))
source
theorem CategoryTheory.MonoidalCategory.id_tensor_associator_naturality_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y Z Z' : C} (h : Z ⟶ Z') {Z✝ : C} (h✝ : tensorObj X (tensorObj Y Z') ⟶ Z✝) :
CategoryStruct.comp (tensorHom (CategoryStruct.id (tensorObj X Y)) h) (CategoryStruct.comp (associator X Y Z').hom h✝) = CategoryStruct.comp (associator X Y Z).hom (CategoryStruct.comp (tensorHom (CategoryStruct.id X) (tensorHom (CategoryStruct.id Y) h)) h✝)
source
theorem CategoryTheory.MonoidalCategory.id_tensor_associator_inv_naturality {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y Z X' : C} (f : X ⟶ X') :
CategoryStruct.comp (tensorHom f (CategoryStruct.id (tensorObj Y Z))) (associator X' Y Z).inv = CategoryStruct.comp (associator X Y Z).inv (tensorHom (tensorHom f (CategoryStruct.id Y)) (CategoryStruct.id Z))
source
theorem CategoryTheory.MonoidalCategory.id_tensor_associator_inv_naturality_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y Z X' : C} (f : X ⟶ X') {Z✝ : C} (h : tensorObj (tensorObj X' Y) Z ⟶ Z✝) :
CategoryStruct.comp (tensorHom f (CategoryStruct.id (tensorObj Y Z))) (CategoryStruct.comp (associator X' Y Z).inv h) = CategoryStruct.comp (associator X Y Z).inv (CategoryStruct.comp (tensorHom (tensorHom f (CategoryStruct.id Y)) (CategoryStruct.id Z)) h)
source
theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
CategoryStruct.comp (tensorHom f.hom g) (tensorHom f.inv h) = CategoryStruct.comp (tensorHom (CategoryStruct.id V) g) (tensorHom (CategoryStruct.id V) h)
source
theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z✝ : C} (h✝ : tensorObj V Z ⟶ Z✝) :
CategoryStruct.comp (tensorHom f.hom g) (CategoryStruct.comp (tensorHom f.inv h) h✝) = CategoryStruct.comp (tensorHom (CategoryStruct.id V) g) (CategoryStruct.comp (tensorHom (CategoryStruct.id V) h) h✝)
source
theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
CategoryStruct.comp (tensorHom f.inv g) (tensorHom f.hom h) = CategoryStruct.comp (tensorHom (CategoryStruct.id W) g) (tensorHom (CategoryStruct.id W) h)
source
theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z✝ : C} (h✝ : tensorObj W Z ⟶ Z✝) :
CategoryStruct.comp (tensorHom f.inv g) (CategoryStruct.comp (tensorHom f.hom h) h✝) = CategoryStruct.comp (tensorHom (CategoryStruct.id W) g) (CategoryStruct.comp (tensorHom (CategoryStruct.id W) h) h✝)
source
theorem CategoryTheory.MonoidalCategory.tensor_hom_inv_id {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
CategoryStruct.comp (tensorHom g f.hom) (tensorHom h f.inv) = CategoryStruct.comp (tensorHom g (CategoryStruct.id V)) (tensorHom h (CategoryStruct.id V))
source
theorem CategoryTheory.MonoidalCategory.tensor_hom_inv_id_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z✝ : C} (h✝ : tensorObj Z V ⟶ Z✝) :
CategoryStruct.comp (tensorHom g f.hom) (CategoryStruct.comp (tensorHom h f.inv) h✝) = CategoryStruct.comp (tensorHom g (CategoryStruct.id V)) (CategoryStruct.comp (tensorHom h (CategoryStruct.id V)) h✝)
source
theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
CategoryStruct.comp (tensorHom g f.inv) (tensorHom h f.hom) = CategoryStruct.comp (tensorHom g (CategoryStruct.id W)) (tensorHom h (CategoryStruct.id W))
source
theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z✝ : C} (h✝ : tensorObj Z W ⟶ Z✝) :
CategoryStruct.comp (tensorHom g f.inv) (CategoryStruct.comp (tensorHom h f.hom) h✝) = CategoryStruct.comp (tensorHom g (CategoryStruct.id W)) (CategoryStruct.comp (tensorHom h (CategoryStruct.id W)) h✝)
source
theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor' {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
CategoryStruct.comp (tensorHom f g) (tensorHom (inv f) h) = CategoryStruct.comp (tensorHom (CategoryStruct.id V) g) (tensorHom (CategoryStruct.id V) h)
source
theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor'_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) {Z✝ : C} (h✝ : tensorObj V Z ⟶ Z✝) :
CategoryStruct.comp (tensorHom f g) (CategoryStruct.comp (tensorHom (inv f) h) h✝) = CategoryStruct.comp (tensorHom (CategoryStruct.id V) g) (CategoryStruct.comp (tensorHom (CategoryStruct.id V) h) h✝)
source
theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor' {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
CategoryStruct.comp (tensorHom (inv f) g) (tensorHom f h) = CategoryStruct.comp (tensorHom (CategoryStruct.id W) g) (tensorHom (CategoryStruct.id W) h)
source
theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor'_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) {Z✝ : C} (h✝ : tensorObj W Z ⟶ Z✝) :
CategoryStruct.comp (tensorHom (inv f) g) (CategoryStruct.comp (tensorHom f h) h✝) = CategoryStruct.comp (tensorHom (CategoryStruct.id W) g) (CategoryStruct.comp (tensorHom (CategoryStruct.id W) h) h✝)
source
theorem CategoryTheory.MonoidalCategory.tensor_hom_inv_id' {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
CategoryStruct.comp (tensorHom g f) (tensorHom h (inv f)) = CategoryStruct.comp (tensorHom g (CategoryStruct.id V)) (tensorHom h (CategoryStruct.id V))
source
theorem CategoryTheory.MonoidalCategory.tensor_hom_inv_id'_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) {Z✝ : C} (h✝ : tensorObj Z V ⟶ Z✝) :
CategoryStruct.comp (tensorHom g f) (CategoryStruct.comp (tensorHom h (inv f)) h✝) = CategoryStruct.comp (tensorHom g (CategoryStruct.id V)) (CategoryStruct.comp (tensorHom h (CategoryStruct.id V)) h✝)
source
theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id' {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
CategoryStruct.comp (tensorHom g (inv f)) (tensorHom h f) = CategoryStruct.comp (tensorHom g (CategoryStruct.id W)) (tensorHom h (CategoryStruct.id W))
source
theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id'_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) {Z✝ : C} (h✝ : tensorObj Z W ⟶ Z✝) :
CategoryStruct.comp (tensorHom g (inv f)) (CategoryStruct.comp (tensorHom h f) h✝) = CategoryStruct.comp (tensorHom g (CategoryStruct.id W)) (CategoryStruct.comp (tensorHom h (CategoryStruct.id W)) h✝)
source
@[reducible, inline]
abbrev CategoryTheory.MonoidalCategory.ofTensorHom {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategoryStruct C] (id_tensorHom_id : ∀ (X₁ X₂ : C), tensorHom (CategoryStruct.id X₁) (CategoryStruct.id X₂) = CategoryStruct.id (tensorObj X₁ X₂) := by cat_disch) (id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (CategoryStruct.id X) f = whiskerLeft X f := by cat_disch) (tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (CategoryStruct.id Y) = whiskerRight f Y := by cat_disch) (tensorHom_comp_tensorHom : ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂), CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂) = tensorHom (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ g₂) := by cat_disch) (associator_naturality : ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃), CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (associator X₁ X₂ X₃).hom (tensorHom f₁ (tensorHom f₂ f₃)) := by cat_disch) (leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryStruct.comp (tensorHom (CategoryStruct.id (tensorUnit C)) f) (leftUnitor Y).hom = CategoryStruct.comp (leftUnitor X).hom f := by cat_disch) (rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryStruct.comp (tensorHom f (CategoryStruct.id (tensorUnit C))) (rightUnitor Y).hom = CategoryStruct.comp (rightUnitor X).hom f := by cat_disch) (pentagon : ∀ (W X Y Z : C), CategoryStruct.comp (tensorHom (associator W X Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (tensorHom (CategoryStruct.id W) (associator X Y Z).hom)) = CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (associator W X (tensorObj Y Z)).hom := by cat_disch) (triangle : ∀ (X Y : C), CategoryStruct.comp (associator X (tensorUnit C) Y).hom (tensorHom (CategoryStruct.id X) (leftUnitor Y).hom) = tensorHom (rightUnitor X).hom (CategoryStruct.id Y) := by cat_disch) :
MonoidalCategory C

A constructor for monoidal categories that requires `tensorHom` instead of `whiskerLeft` and `whiskerRight`.

Equations

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

Instances For

source
theorem CategoryTheory.MonoidalCategory.comp_tensor_id {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) :
tensorHom (CategoryStruct.comp f g) (CategoryStruct.id Z) = CategoryStruct.comp (tensorHom f (CategoryStruct.id Z)) (tensorHom g (CategoryStruct.id Z))
source
theorem CategoryTheory.MonoidalCategory.comp_tensor_id_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) {Z✝ : C} (h : tensorObj Y Z ⟶ Z✝) :
CategoryStruct.comp (tensorHom (CategoryStruct.comp f g) (CategoryStruct.id Z)) h = CategoryStruct.comp (tensorHom f (CategoryStruct.id Z)) (CategoryStruct.comp (tensorHom g (CategoryStruct.id Z)) h)
source
theorem CategoryTheory.MonoidalCategory.id_tensor_comp {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) :
tensorHom (CategoryStruct.id Z) (CategoryStruct.comp f g) = CategoryStruct.comp (tensorHom (CategoryStruct.id Z) f) (tensorHom (CategoryStruct.id Z) g)
source
theorem CategoryTheory.MonoidalCategory.id_tensor_comp_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) {Z✝ : C} (h : tensorObj Z Y ⟶ Z✝) :
CategoryStruct.comp (tensorHom (CategoryStruct.id Z) (CategoryStruct.comp f g)) h = CategoryStruct.comp (tensorHom (CategoryStruct.id Z) f) (CategoryStruct.comp (tensorHom (CategoryStruct.id Z) g) h)
source
theorem CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) :
CategoryStruct.comp (tensorHom (CategoryStruct.id Y) f) (tensorHom g (CategoryStruct.id X)) = tensorHom g f
source
theorem CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) {Z✝ : C} (h : tensorObj Z X ⟶ Z✝) :
CategoryStruct.comp (tensorHom (CategoryStruct.id Y) f) (CategoryStruct.comp (tensorHom g (CategoryStruct.id X)) h) = CategoryStruct.comp (tensorHom g f) h
source
theorem CategoryTheory.MonoidalCategory.tensor_id_comp_id_tensor {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) :
CategoryStruct.comp (tensorHom g (CategoryStruct.id W)) (tensorHom (CategoryStruct.id Z) f) = tensorHom g f
source
theorem CategoryTheory.MonoidalCategory.tensor_id_comp_id_tensor_assoc {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) {Z✝ : C} (h : tensorObj Z X ⟶ Z✝) :
CategoryStruct.comp (tensorHom g (CategoryStruct.id W)) (CategoryStruct.comp (tensorHom (CategoryStruct.id Z) f) h) = CategoryStruct.comp (tensorHom g f) h
source
theorem CategoryTheory.MonoidalCategory.tensor_left_iff {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f g : X ⟶ Y) :
tensorHom (CategoryStruct.id (tensorUnit C)) f = tensorHom (CategoryStruct.id (tensorUnit C)) g ↔ f = g
source
theorem CategoryTheory.MonoidalCategory.tensor_right_iff {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C} (f g : X ⟶ Y) :
tensorHom f (CategoryStruct.id (tensorUnit C)) = tensorHom g (CategoryStruct.id (tensorUnit C)) ↔ f = g
source
def CategoryTheory.MonoidalCategory.tensor (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
Functor (C × C) C

The tensor product expressed as a functor.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_map (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C × C} (f : X ⟶ Y) :
(tensor C).map f = tensorHom f.1 f.2
source
@[simp]
theorem CategoryTheory.MonoidalCategory.tensor_obj (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C × C) :
(tensor C).obj X = tensorObj X.1 X.2
source
def CategoryTheory.MonoidalCategory.leftAssocTensor (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
Functor (C × C × C) C

The left-associated triple tensor product as a functor.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.leftAssocTensor_obj (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C × C × C) :
(leftAssocTensor C).obj X = tensorObj (tensorObj X.1 X.2.1) X.2.2
source
@[simp]
theorem CategoryTheory.MonoidalCategory.leftAssocTensor_map (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C × C × C} (f : X ⟶ Y) :
(leftAssocTensor C).map f = tensorHom (tensorHom f.1 f.2.1) f.2.2
source
def CategoryTheory.MonoidalCategory.rightAssocTensor (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
Functor (C × C × C) C

The right-associated triple tensor product as a functor.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.rightAssocTensor_obj (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C × C × C) :
(rightAssocTensor C).obj X = tensorObj X.1 (tensorObj X.2.1 X.2.2)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.rightAssocTensor_map (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X Y : C × C × C} (f : X ⟶ Y) :
(rightAssocTensor C).map f = tensorHom f.1 (tensorHom f.2.1 f.2.2)
source
def CategoryTheory.MonoidalCategory.curriedTensor (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
Functor C (Functor C C)

The tensor product bifunctor `C ⥤ C ⥤ C` of a monoidal category.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.curriedTensor_obj_obj (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
((curriedTensor C).obj X).obj Y = tensorObj X Y
source
@[simp]
theorem CategoryTheory.MonoidalCategory.curriedTensor_map_app (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : C) :
((curriedTensor C).map f).app Y = whiskerRight f Y
source
@[simp]
theorem CategoryTheory.MonoidalCategory.curriedTensor_obj_map (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) {X✝ Y✝ : C} (g : X✝ ⟶ Y✝) :
((curriedTensor C).obj X).map g = whiskerLeft X g
source
@[reducible, inline]
abbrev CategoryTheory.MonoidalCategory.tensorLeft {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) :
Functor C C

Tensoring on the left with a fixed object, as a functor.

Equations

- CategoryTheory.MonoidalCategory.tensorLeft X = (CategoryTheory.MonoidalCategory.curriedTensor C).obj X

Instances For

source
@[reducible, inline]
abbrev CategoryTheory.MonoidalCategory.tensorRight {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) :
Functor C C

Tensoring on the right with a fixed object, as a functor.

Equations

- CategoryTheory.MonoidalCategory.tensorRight X = (CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X

Instances For

source
@[reducible, inline]
abbrev CategoryTheory.MonoidalCategory.tensorUnitLeft (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
Functor C C

The functor `fun X ↦ 𝟙_ C ⊗ X`.

Equations

- CategoryTheory.MonoidalCategory.tensorUnitLeft C = CategoryTheory.MonoidalCategory.tensorLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

Instances For

source
@[reducible, inline]
abbrev CategoryTheory.MonoidalCategory.tensorUnitRight (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
Functor C C

The functor `fun X ↦ X ⊗ 𝟙_ C`.

Equations

- CategoryTheory.MonoidalCategory.tensorUnitRight C = CategoryTheory.MonoidalCategory.tensorRight (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

Instances For

source
def CategoryTheory.MonoidalCategory.associatorNatIso (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
leftAssocTensor C ≅ rightAssocTensor C

The associator as a natural isomorphism.

Equations

- CategoryTheory.MonoidalCategory.associatorNatIso C = CategoryTheory.NatIso.ofComponents (fun (x : C × C × C) => CategoryTheory.MonoidalCategoryStruct.associator x.1 x.2.1 x.2.2) ⋯

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.associatorNatIso_inv_app (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C × C × C) :
(associatorNatIso C).inv.app X = (associator X.1 X.2.1 X.2.2).inv
source
@[simp]
theorem CategoryTheory.MonoidalCategory.associatorNatIso_hom_app (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C × C × C) :
(associatorNatIso C).hom.app X = (associator X.1 X.2.1 X.2.2).hom
source
def CategoryTheory.MonoidalCategory.leftUnitorNatIso (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
tensorUnitLeft C ≅ Functor.id C

The left unitor as a natural isomorphism.

Equations

- CategoryTheory.MonoidalCategory.leftUnitorNatIso C = CategoryTheory.NatIso.ofComponents CategoryTheory.MonoidalCategoryStruct.leftUnitor ⋯

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.leftUnitorNatIso_hom_app (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) :
(leftUnitorNatIso C).hom.app X = (leftUnitor X).hom
source
@[simp]
theorem CategoryTheory.MonoidalCategory.leftUnitorNatIso_inv_app (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) :
(leftUnitorNatIso C).inv.app X = (leftUnitor X).inv
source
def CategoryTheory.MonoidalCategory.rightUnitorNatIso (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
tensorUnitRight C ≅ Functor.id C

The right unitor as a natural isomorphism.

Equations

- CategoryTheory.MonoidalCategory.rightUnitorNatIso C = CategoryTheory.NatIso.ofComponents CategoryTheory.MonoidalCategoryStruct.rightUnitor ⋯

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.rightUnitorNatIso_hom_app (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) :
(rightUnitorNatIso C).hom.app X = (rightUnitor X).hom
source
@[simp]
theorem CategoryTheory.MonoidalCategory.rightUnitorNatIso_inv_app (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X : C) :
(rightUnitorNatIso C).inv.app X = (rightUnitor X).inv
source
def CategoryTheory.MonoidalCategory.curriedAssociatorNatIso (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
bifunctorComp₁₂ (curriedTensor C) (curriedTensor C) ≅ bifunctorComp₂₃ (curriedTensor C) (curriedTensor C)

The associator as a natural isomorphism between trifunctors `C ⥤ C ⥤ C ⥤ C`.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.curriedAssociatorNatIso_hom_app_app_app (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X X✝ X✝¹ : C) :
(((curriedAssociatorNatIso C).hom.app X).app X✝).app X✝¹ = (associator X X✝ X✝¹).hom
source
@[simp]
theorem CategoryTheory.MonoidalCategory.curriedAssociatorNatIso_inv_app_app_app (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X X✝ X✝¹ : C) :
(((curriedAssociatorNatIso C).inv.app X).app X✝).app X✝¹ = (associator X X✝ X✝¹).inv
source
def CategoryTheory.MonoidalCategory.tensorLeftTensor {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
tensorLeft (tensorObj X Y) ≅ (tensorLeft Y).comp (tensorLeft X)

Tensoring on the left with `X ⊗ Y` is naturally isomorphic to tensoring on the left with `Y`, and then again with `X`.

Equations

- CategoryTheory.MonoidalCategory.tensorLeftTensor X Y = CategoryTheory.NatIso.ofComponents (CategoryTheory.MonoidalCategoryStruct.associator X Y) ⋯

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorLeftTensor_hom_app {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y Z : C) :
(tensorLeftTensor X Y).hom.app Z = (associator X Y Z).hom
source
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorLeftTensor_inv_app {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y Z : C) :
(tensorLeftTensor X Y).inv.app Z = (associator X Y Z).inv
source
@[reducible, inline]
abbrev CategoryTheory.MonoidalCategory.tensoringLeft (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
Functor C (Functor C C)

Tensoring on the left, as a functor from `C` into endofunctors of `C`.

TODO: show this is an op-monoidal functor.

Equations

- CategoryTheory.MonoidalCategory.tensoringLeft C = CategoryTheory.MonoidalCategory.curriedTensor C

Instances For

source
instance CategoryTheory.MonoidalCategory.instFaithfulFunctorTensoringLeft (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
(tensoringLeft C).Faithful
source
@[reducible, inline]
abbrev CategoryTheory.MonoidalCategory.tensoringRight (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
Functor C (Functor C C)

Tensoring on the right, as a functor from `C` into endofunctors of `C`.

We later show this is a monoidal functor.

Equations

- CategoryTheory.MonoidalCategory.tensoringRight C = (CategoryTheory.MonoidalCategory.curriedTensor C).flip

Instances For

source
instance CategoryTheory.MonoidalCategory.instFaithfulFunctorTensoringRight (C : Type u) [𝒞 : Category.{v, u} C] [MonoidalCategory C] :
(tensoringRight C).Faithful
source
def CategoryTheory.MonoidalCategory.tensorRightTensor {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y : C) :
tensorRight (tensorObj X Y) ≅ (tensorRight X).comp (tensorRight Y)

Tensoring on the right with `X ⊗ Y` is naturally isomorphic to tensoring on the right with `X`, and then again with `Y`.

Equations

- CategoryTheory.MonoidalCategory.tensorRightTensor X Y = CategoryTheory.NatIso.ofComponents (fun (Z : C) => (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).symm) ⋯

Instances For

source
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorRightTensor_hom_app {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y Z : C) :
(tensorRightTensor X Y).hom.app Z = (associator Z X Y).inv
source
@[simp]
theorem CategoryTheory.MonoidalCategory.tensorRightTensor_inv_app {C : Type u} [𝒞 : Category.{v, u} C] [MonoidalCategory C] (X Y Z : C) :
(tensorRightTensor X Y).inv.app Z = (associator Z X Y).hom
source
instance CategoryTheory.MonoidalCategory.prodMonoidal (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] :
MonoidalCategory (C₁ × C₂)
Equations

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

source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_associator (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] (X Y Z : C₁ × C₂) :
associator X Y Z = (associator X.1 Y.1 Z.1).prod (associator X.2 Y.2 Z.2)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_whiskerLeft (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] (X x✝ x✝¹ : C₁ × C₂) (f : x✝ ⟶ x✝¹) :
whiskerLeft X f = (whiskerLeft X.1 f.1, whiskerLeft X.2 f.2)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_tensorUnit (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] :
tensorUnit (C₁ × C₂) = (tensorUnit C₁, tensorUnit C₂)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_tensorHom (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] {X₁✝ Y₁✝ X₂✝ Y₂✝ : C₁ × C₂} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) :
tensorHom f g = (tensorHom f.1 g.1, tensorHom f.2 g.2)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_tensorObj (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] (X Y : C₁ × C₂) :
tensorObj X Y = (tensorObj X.1 Y.1, tensorObj X.2 Y.2)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_whiskerRight (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] {X₁✝ X₂✝ : C₁ × C₂} (f : X₁✝ ⟶ X₂✝) (X : C₁ × C₂) :
whiskerRight f X = (whiskerRight f.1 X.1, whiskerRight f.2 X.2)
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor_hom_fst (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] (X : C₁ × C₂) :
(leftUnitor X).hom.1 = (leftUnitor X.1).hom
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor_hom_snd (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] (X : C₁ × C₂) :
(leftUnitor X).hom.2 = (leftUnitor X.2).hom
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor_inv_fst (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] (X : C₁ × C₂) :
(leftUnitor X).inv.1 = (leftUnitor X.1).inv
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor_inv_snd (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] (X : C₁ × C₂) :
(leftUnitor X).inv.2 = (leftUnitor X.2).inv
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor_hom_fst (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] (X : C₁ × C₂) :
(rightUnitor X).hom.1 = (rightUnitor X.1).hom
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor_hom_snd (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] (X : C₁ × C₂) :
(rightUnitor X).hom.2 = (rightUnitor X.2).hom
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor_inv_fst (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] (X : C₁ × C₂) :
(rightUnitor X).inv.1 = (rightUnitor X.1).inv
source
@[simp]
theorem CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor_inv_snd (C₁ : Type u₁) [Category.{v₁, u₁} C₁] [MonoidalCategory C₁] (C₂ : Type u₂) [Category.{v₂, u₂} C₂] [MonoidalCategory C₂] (X : C₁ × C₂) :
(rightUnitor X).inv.2 = (rightUnitor X.2).inv
source
theorem CategoryTheory.NatTrans.tensor_naturality {J : Type u_1} [Category.{u_3, u_1} J] {C : Type u_2} [Category.{u_4, u_2} C] [MonoidalCategory C] {F G F' G' : Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X Y X' Y' : J} (f : X ⟶ Y) (g : X' ⟶ Y') :
CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (G.map g)) (MonoidalCategoryStruct.tensorHom (α.app Y) (β.app Y')) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (α.app X) (β.app X')) (MonoidalCategoryStruct.tensorHom (F'.map f) (G'.map g))
source
theorem CategoryTheory.NatTrans.tensor_naturality_assoc {J : Type u_1} [Category.{u_3, u_1} J] {C : Type u_2} [Category.{u_4, u_2} C] [MonoidalCategory C] {F G F' G' : Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X Y X' Y' : J} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : C} (h : MonoidalCategoryStruct.tensorObj (F'.obj Y) (G'.obj Y') ⟶ Z) :
CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (G.map g)) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (α.app Y) (β.app Y')) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (α.app X) (β.app X')) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F'.map f) (G'.map g)) h)
source
theorem CategoryTheory.NatTrans.whiskerRight_app_tensor_app {J : Type u_1} [Category.{u_3, u_1} J] {C : Type u_2} [Category.{u_4, u_2} C] [MonoidalCategory C] {F G F' G' : Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X Y : J} (f : X ⟶ Y) (X' : J) :
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (G.obj X')) (MonoidalCategoryStruct.tensorHom (α.app Y) (β.app X')) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (α.app X) (β.app X')) (MonoidalCategoryStruct.whiskerRight (F'.map f) (G'.obj X'))
source
theorem CategoryTheory.NatTrans.whiskerRight_app_tensor_app_assoc {J : Type u_1} [Category.{u_3, u_1} J] {C : Type u_2} [Category.{u_4, u_2} C] [MonoidalCategory C] {F G F' G' : Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X Y : J} (f : X ⟶ Y) (X' : J) {Z : C} (h : MonoidalCategoryStruct.tensorObj (F'.obj Y) (G'.obj X') ⟶ Z) :
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (G.obj X')) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (α.app Y) (β.app X')) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (α.app X) (β.app X')) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F'.map f) (G'.obj X')) h)
source
theorem CategoryTheory.NatTrans.whiskerLeft_app_tensor_app {J : Type u_1} [Category.{u_3, u_1} J] {C : Type u_2} [Category.{u_4, u_2} C] [MonoidalCategory C] {F G F' G' : Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X' Y' : J} (f : X' ⟶ Y') (X : J) :
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (G.map f)) (MonoidalCategoryStruct.tensorHom (α.app X) (β.app Y')) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (α.app X) (β.app X')) (MonoidalCategoryStruct.whiskerLeft (F'.obj X) (G'.map f))
source
theorem CategoryTheory.NatTrans.whiskerLeft_app_tensor_app_assoc {J : Type u_1} [Category.{u_3, u_1} J] {C : Type u_2} [Category.{u_4, u_2} C] [MonoidalCategory C] {F G F' G' : Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X' Y' : J} (f : X' ⟶ Y') (X : J) {Z : C} (h : MonoidalCategoryStruct.tensorObj (F'.obj X) (G'.obj Y') ⟶ Z) :
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (G.map f)) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (α.app X) (β.app Y')) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (α.app X) (β.app X')) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F'.obj X) (G'.map f)) h)
source
@[reducible, inline]
abbrev CategoryTheory.MonoidalCategory.fullSubcategory {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (P : ObjectProperty C) (tensorUnit : P (tensorUnit C)) (tensorObj : ∀ (X Y : C), P X → P Y → P (tensorObj X Y)) :
MonoidalCategory P.FullSubcategory

The restriction of a monoidal category along an object property that's closed under the monoidal structure.

Equations

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

Instances For