# mathlibdocumentation

category_theory.monoidal.free.basic

# The free monoidal category over a type #

Given a type C, the free monoidal category over C has as objects formal expressions built from (formal) tensor products of terms of C and a formal unit. Its morphisms are compositions and tensor products of identities, unitors and associators.

In this file, we construct the free monoidal category and prove that it is a monoidal category. If D is a monoidal category, we construct the functor free_monoidal_category C ⥤ D associated to a function C → D.

The free monoidal category has two important properties: it is a groupoid and it is thin. The former is obvious from the construction, and the latter is what is commonly known as the monoidal coherence theorem. Both of these properties are proved in the file coherence.lean.

inductive category_theory.free_monoidal_category (C : Type u) :
Type u
• of : Π (C : Type u),
• unit : Π (C : Type u),
• tensor :

Given a type C, the free monoidal category over C has as objects formal expressions built from (formal) tensor products of terms of C and a formal unit. Its morphisms are compositions and tensor products of identities, unitors and associators.

@[instance]
@[nolint]
inductive category_theory.free_monoidal_category.hom {C : Type u} :
• id : Π {C : Type u} (X : , X.hom X
• α_hom : Π {C : Type u} (X Y Z : , ((X.tensor Y).tensor Z).hom (X.tensor (Y.tensor Z))
• α_inv : Π {C : Type u} (X Y Z : , (X.tensor (Y.tensor Z)).hom ((X.tensor Y).tensor Z)
• l_hom : Π {C : Type u} (X : ,
• l_inv : Π {C : Type u} (X : ,
• ρ_hom : Π {C : Type u} (X : ,
• ρ_inv : Π {C : Type u} (X : ,
• comp : Π {C : Type u} {X Y Z : , X.hom YY.hom ZX.hom Z
• tensor : Π {C : Type u} {W X Y Z : , W.hom YX.hom Z(W.tensor X).hom (Y.tensor Z)

Formal compositions and tensor products of identities, unitors and associators. The morphisms of the free monoidal category are obtained as a quotient of these formal morphisms by the relations defining a monoidal category.

inductive category_theory.free_monoidal_category.hom_equiv {C : Type u}  :
X.hom YX.hom Y → Prop
• refl : ∀ {C : Type u} {X Y : (f : X.hom Y),
• symm : ∀ {C : Type u} {X Y : (f g : X.hom Y),
• trans : ∀ {C : Type u} {X Y : {f g h : X.hom Y},
• comp : ∀ {C : Type u} {X Y Z : {f f' : X.hom Y} {g g' : Y.hom Z},
• tensor : ∀ {C : Type u} {W X Y Z : {f f' : W.hom X} {g g' : Y.hom Z},
• comp_id : ∀ {C : Type u} {X Y : (f : X.hom Y),
• id_comp : ∀ {C : Type u} {X Y : (f : X.hom Y),
• assoc : ∀ {C : Type u} {X Y U V : (f : X.hom U) (g : U.hom V) (h : V.hom Y), (f.comp (g.comp h))
• tensor_id :
• tensor_comp : ∀ {C : Type u} {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : (f₁ : X₁.hom Y₁) (f₂ : X₂.hom Y₂) (g₁ : Y₁.hom Z₁) (g₂ : Y₂.hom Z₂), category_theory.free_monoidal_category.hom_equiv ((f₁.comp g₁).tensor (f₂.comp g₂)) ((f₁.tensor f₂).comp (g₁.tensor g₂))
• α_hom_inv : ∀ {C : Type u} {X Y Z : ,
• α_inv_hom : ∀ {C : Type u} {X Y Z : ,
• associator_naturality : ∀ {C : Type u} {X₁ X₂ X₃ Y₁ Y₂ Y₃ : (f₁ : X₁.hom Y₁) (f₂ : X₂.hom Y₂) (f₃ : X₃.hom Y₃), category_theory.free_monoidal_category.hom_equiv (((f₁.tensor f₂).tensor f₃).comp .comp (f₁.tensor (f₂.tensor f₃)))
• ρ_hom_inv :
• ρ_inv_hom :
• ρ_naturality :
• l_hom_inv :
• l_inv_hom :
• l_naturality :
• pentagon :
• triangle :

The morphisms of the free monoidal category satisfy 21 relations ensuring that the resulting category is in fact a category and that it is monoidal.

@[instance]

We say that two formal morphisms in the free monoidal category are equivalent if they become equal if we apply the relations that are true in a monoidal category. Note that we will prove that there is only one equivalence class -- this is the monoidal coherence theorem.

Equations
@[instance]
Equations
@[simp]
theorem category_theory.free_monoidal_category.mk_tensor {C : Type u} {X₁ Y₁ X₂ Y₂ : category_theory.free_monoidal_category C} (f : X₁.hom Y₁) (g : X₂.hom Y₂) :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
def category_theory.free_monoidal_category.project_obj {C : Type u} {D : Type u'} (f : C → D) :

Auxiliary definition for free_monoidal_category.project.

Equations
@[simp]
def category_theory.free_monoidal_category.project_map_aux {C : Type u} {D : Type u'} (f : C → D)  :

Auxiliary definition for free_monoidal_category.project.

Equations
def category_theory.free_monoidal_category.project_map {C : Type u} {D : Type u'} (f : C → D)  :

Auxiliary definition for free_monoidal_category.project.

Equations
def category_theory.free_monoidal_category.project {C : Type u} {D : Type u'} (f : C → D) :

If D is a monoidal category and we have a function C → D, then we have a functor from the free monoidal category over C to the category D.

Equations