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 byX ◁ f
,whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : X₁ ⊗ Y ⟶ X₂ ⊗ Y
, denoted byf ▷ Y
. These are products of an object and a morphism (the terminology "whiskering" is borrowed from 2-category theory). The tensor product of morphismstensorHom
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 bytensorHom_def
andtensorHom_def'
. By default,tensorHom
is defined so thattensorHom_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,
- it is a composition of morphisms like
f₁ ≫ f₂ ≫ f₃ ≫ f₄ ≫ f₅
such that eachfᵢ
is either a structural morphisms (morphisms made up only of identities, associators, unitors) or non-structural morphisms, and - each non-structural morphism in the composition is of the form
X₁ ◁ X₂ ◁ X₃ ◁ f ▷ X₄ ▷ X₅
, where eachXᵢ
is a object that is not the identity or a tensor andf
is a non-structural morphisms 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.
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} → (Y₁ ⟶ Y₂) → (CategoryTheory.MonoidalCategory.tensorObj X Y₁ ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y₂)
left whiskering for morphisms
- whiskerRight : {X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → CategoryTheory.MonoidalCategory.tensorObj X₁ Y ⟶ CategoryTheory.MonoidalCategory.tensorObj X₂ Y
right whiskering for morphisms
- tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂ ⟶ CategoryTheory.MonoidalCategory.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) → CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z ≅ CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z)
The associator isomorphism
(X ⊗ Y) ⊗ Z ≃ X ⊗ (Y ⊗ Z)
- leftUnitor : (X : C) → CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) X ≅ X
The left unitor:
𝟙_ C ⊗ X ≃ X
- rightUnitor : (X : C) → CategoryTheory.MonoidalCategory.tensorObj X (𝟙_ C) ≅ X
The right unitor:
X ⊗ 𝟙_ C ≃ X
Instances
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
Notation for the whiskerLeft
operator of monoidal categories
Equations
- One or more equations did not get rendered due to their size.
Instances For
Notation for the whiskerRight
operator of monoidal categories
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Notation for tensorUnit
, the two-sided identity of ⊗
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used to ensure that 𝟙_
notation is used, as the ascription makes this not automatic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Notation for the leftUnitor
: 𝟙_C ⊗ X ≃ X
Equations
- CategoryTheory.MonoidalCategory.«termλ_» = Lean.ParserDescr.node `CategoryTheory.MonoidalCategory.«termλ_» 1024 (Lean.ParserDescr.symbol "λ_")
Instances For
Notation for the rightUnitor
: X ⊗ 𝟙_C ≃ X
Equations
- CategoryTheory.MonoidalCategory.termρ_ = Lean.ParserDescr.node `CategoryTheory.MonoidalCategory.termρ_ 1024 (Lean.ParserDescr.symbol "ρ_")
Instances For
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.
See https://stacks.math.columbia.edu/tag/0FFK.
- tensorObj : C → C → C
- whiskerLeft : (X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (CategoryTheory.MonoidalCategory.tensorObj X Y₁ ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y₂)
- whiskerRight : {X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → CategoryTheory.MonoidalCategory.tensorObj X₁ Y ⟶ CategoryTheory.MonoidalCategory.tensorObj X₂ Y
- tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂ ⟶ CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂)
- tensorUnit : C
- leftUnitor : (X : C) → CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) X ≅ X
- rightUnitor : (X : C) → CategoryTheory.MonoidalCategory.tensorObj X (𝟙_ C) ≅ X
- tensorHom_def : ∀ {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f X₂) (CategoryTheory.MonoidalCategory.whiskerLeft Y₁ g)
- tensor_id : ∀ (X₁ X₂ : C), CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)
Tensor product of identity maps is the identity:
(𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)
- tensor_comp : ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂), CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) (CategoryTheory.MonoidalCategory.tensorHom g₁ g₂)
Composition of tensor products is tensor product of compositions:
(f₁ ⊗ g₁) ∘ (f₂ ⊗ g₂) = (f₁ ∘ f₂) ⊗ (g₁ ⊗ g₂)
- whiskerLeft_id : ∀ (X Y : C), CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)
- id_whiskerRight : ∀ (X Y : C), CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.id X) Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)
- associator_naturality : ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) f₃) (CategoryTheory.MonoidalCategory.associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X₁ X₂ X₃).hom (CategoryTheory.MonoidalCategory.tensorHom f₁ (CategoryTheory.MonoidalCategory.tensorHom f₂ f₃))
Naturality of the associator isomorphism:
(f₁ ⊗ f₂) ⊗ f₃ ≃ f₁ ⊗ (f₂ ⊗ f₃)
- leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) f) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.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), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f (𝟙_ C)) (CategoryTheory.MonoidalCategory.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom f
Naturality of the right unitor: commutativity of
X ⊗ 𝟙_ C ⟶ Y ⊗ 𝟙_ C ⟶ Y
andX ⊗ 𝟙_ C ⟶ X ⟶ Y
- pentagon : ∀ (W X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator W X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft W (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).hom (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom
The pentagon identity relating the isomorphism between
X ⊗ (Y ⊗ (Z ⊗ W))
and((X ⊗ Y) ⊗ Z) ⊗ W
- triangle : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X (𝟙_ C) Y).hom (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.leftUnitor Y).hom) = CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.rightUnitor X).hom Y
The identity relating the isomorphisms between
X ⊗ (𝟙_ C ⊗ Y)
,(X ⊗ 𝟙_ C) ⊗ Y
andX ⊗ Y
Instances
Tensor product of identity maps is the identity: (𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)
Composition of tensor products is tensor product of compositions:
(f₁ ⊗ g₁) ∘ (f₂ ⊗ g₂) = (f₁ ∘ f₂) ⊗ (g₁ ⊗ g₂)
Naturality of the associator isomorphism: (f₁ ⊗ f₂) ⊗ f₃ ≃ f₁ ⊗ (f₂ ⊗ f₃)
Naturality of the left unitor, commutativity of 𝟙_ C ⊗ X ⟶ 𝟙_ C ⊗ Y ⟶ Y
and 𝟙_ C ⊗ X ⟶ X ⟶ Y
Naturality of the right unitor: commutativity of X ⊗ 𝟙_ C ⟶ Y ⊗ 𝟙_ C ⟶ Y
and X ⊗ 𝟙_ C ⟶ X ⟶ Y
The pentagon identity relating the isomorphism between X ⊗ (Y ⊗ (Z ⊗ W))
and ((X ⊗ Y) ⊗ Z) ⊗ W
The identity relating the isomorphisms between X ⊗ (𝟙_ C ⊗ Y)
, (X ⊗ 𝟙_ C) ⊗ Y
and X ⊗ Y
The left whiskering of an isomorphism is an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
The right whiskering of an isomorphism is an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
The tensor product of two isomorphisms is an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Notation for tensorIso
, the tensor product of isomorphisms
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
The lemmas in the next section are true by coherence, but we prove them directly as they are used in proving the coherence theorem.
We state it as a simp lemma, which is regarded as an involved version of
id_whiskerRight X Y : 𝟙 X ▷ Y = 𝟙 (X ⊗ Y)
.
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
The tensor product expressed as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The left-associated triple tensor product as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The right-associated triple tensor product as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Tensoring on the left with a fixed object, as a functor.
Equations
Instances For
Tensoring on the right with a fixed object, as a functor.
Equations
Instances For
The functor fun X ↦ 𝟙_ C ⊗ X
.
Equations
Instances For
The functor fun X ↦ X ⊗ 𝟙_ C
.
Equations
Instances For
The associator as a natural isomorphism.
Equations
- CategoryTheory.MonoidalCategory.associatorNatIso C = CategoryTheory.NatIso.ofComponents (fun (x : C × C × C) => CategoryTheory.MonoidalCategory.associator x.1 x.2.1 x.2.2) ⋯
Instances For
The left unitor as a natural isomorphism.
Equations
- CategoryTheory.MonoidalCategory.leftUnitorNatIso C = CategoryTheory.NatIso.ofComponents CategoryTheory.MonoidalCategory.leftUnitor ⋯
Instances For
The right unitor as a natural isomorphism.
Equations
- CategoryTheory.MonoidalCategory.rightUnitorNatIso C = CategoryTheory.NatIso.ofComponents CategoryTheory.MonoidalCategory.rightUnitor ⋯
Instances For
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
Tensoring on the left with X ⊗ Y
is naturally isomorphic to
tensoring on the left with Y
, and then again with X
.
Equations
Instances For
Tensoring on the left, as a functor from C
into endofunctors of C
.
TODO: show this is an op-monoidal functor.
Equations
Instances For
Equations
- ⋯ = ⋯
Tensoring on the right, as a functor from C
into endofunctors of C
.
We later show this is a monoidal functor.
Equations
Instances For
Equations
- ⋯ = ⋯
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.MonoidalCategory.associator Z X Y).symm) ⋯
Instances For
Equations
- CategoryTheory.MonoidalCategory.prodMonoidal C₁ C₂ = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯