The free monoidal category over a type #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
- of : Π {C : Type u}, C → category_theory.free_monoidal_category C
- unit : Π {C : Type u}, category_theory.free_monoidal_category C
- tensor : Π {C : Type u}, category_theory.free_monoidal_category C → category_theory.free_monoidal_category C → category_theory.free_monoidal_category C
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.
Instances for category_theory.free_monoidal_category
- category_theory.free_monoidal_category.has_sizeof_inst
- category_theory.free_monoidal_category.inhabited
- category_theory.free_monoidal_category.category_free_monoidal_category
- category_theory.free_monoidal_category.category_theory.monoidal_category
- category_theory.free_monoidal_category.category_theory.groupoid
@[protected, instance]
@[nolint]
- id : Π {C : Type u} (X : category_theory.free_monoidal_category C), X.hom X
- α_hom : Π {C : Type u} (X Y Z : category_theory.free_monoidal_category C), ((X.tensor Y).tensor Z).hom (X.tensor (Y.tensor Z))
- α_inv : Π {C : Type u} (X Y Z : category_theory.free_monoidal_category C), (X.tensor (Y.tensor Z)).hom ((X.tensor Y).tensor Z)
- l_hom : Π {C : Type u} (X : category_theory.free_monoidal_category C), (category_theory.free_monoidal_category.unit.tensor X).hom X
- l_inv : Π {C : Type u} (X : category_theory.free_monoidal_category C), X.hom (category_theory.free_monoidal_category.unit.tensor X)
- ρ_hom : Π {C : Type u} (X : category_theory.free_monoidal_category C), (X.tensor category_theory.free_monoidal_category.unit).hom X
- ρ_inv : Π {C : Type u} (X : category_theory.free_monoidal_category C), X.hom (X.tensor category_theory.free_monoidal_category.unit)
- comp : Π {C : Type u} {X Y Z : category_theory.free_monoidal_category C}, X.hom Y → Y.hom Z → X.hom Z
- tensor : Π {C : Type u} {W X Y Z : category_theory.free_monoidal_category C}, W.hom Y → X.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.
Instances for category_theory.free_monoidal_category.hom
- category_theory.free_monoidal_category.hom.has_sizeof_inst
- category_theory.free_monoidal_category.setoid_hom
inductive
category_theory.free_monoidal_category.hom_equiv
{C : Type u}
{X Y : category_theory.free_monoidal_category C} :
- refl : ∀ {C : Type u} {X Y : category_theory.free_monoidal_category C} (f : X.hom Y), category_theory.free_monoidal_category.hom_equiv f f
- symm : ∀ {C : Type u} {X Y : category_theory.free_monoidal_category C} (f g : X.hom Y), category_theory.free_monoidal_category.hom_equiv f g → category_theory.free_monoidal_category.hom_equiv g f
- trans : ∀ {C : Type u} {X Y : category_theory.free_monoidal_category C} {f g h : X.hom Y}, category_theory.free_monoidal_category.hom_equiv f g → category_theory.free_monoidal_category.hom_equiv g h → category_theory.free_monoidal_category.hom_equiv f h
- comp : ∀ {C : Type u} {X Y Z : category_theory.free_monoidal_category C} {f f' : X.hom Y} {g g' : Y.hom Z}, category_theory.free_monoidal_category.hom_equiv f f' → category_theory.free_monoidal_category.hom_equiv g g' → category_theory.free_monoidal_category.hom_equiv (f.comp g) (f'.comp g')
- tensor : ∀ {C : Type u} {W X Y Z : category_theory.free_monoidal_category C} {f f' : W.hom X} {g g' : Y.hom Z}, category_theory.free_monoidal_category.hom_equiv f f' → category_theory.free_monoidal_category.hom_equiv g g' → category_theory.free_monoidal_category.hom_equiv (f.tensor g) (f'.tensor g')
- comp_id : ∀ {C : Type u} {X Y : category_theory.free_monoidal_category C} (f : X.hom Y), category_theory.free_monoidal_category.hom_equiv (f.comp (category_theory.free_monoidal_category.hom.id Y)) f
- id_comp : ∀ {C : Type u} {X Y : category_theory.free_monoidal_category C} (f : X.hom Y), category_theory.free_monoidal_category.hom_equiv ((category_theory.free_monoidal_category.hom.id X).comp f) f
- assoc : ∀ {C : Type u} {X Y U V : category_theory.free_monoidal_category C} (f : X.hom U) (g : U.hom V) (h : V.hom Y), category_theory.free_monoidal_category.hom_equiv ((f.comp g).comp h) (f.comp (g.comp h))
- tensor_id : ∀ {C : Type u} {X Y : category_theory.free_monoidal_category C}, category_theory.free_monoidal_category.hom_equiv ((category_theory.free_monoidal_category.hom.id X).tensor (category_theory.free_monoidal_category.hom.id Y)) (category_theory.free_monoidal_category.hom.id (X.tensor Y))
- tensor_comp : ∀ {C : Type u} {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : category_theory.free_monoidal_category C} (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 : category_theory.free_monoidal_category C}, category_theory.free_monoidal_category.hom_equiv ((category_theory.free_monoidal_category.hom.α_hom X Y Z).comp (category_theory.free_monoidal_category.hom.α_inv X Y Z)) (category_theory.free_monoidal_category.hom.id ((X.tensor Y).tensor Z))
- α_inv_hom : ∀ {C : Type u} {X Y Z : category_theory.free_monoidal_category C}, category_theory.free_monoidal_category.hom_equiv ((category_theory.free_monoidal_category.hom.α_inv X Y Z).comp (category_theory.free_monoidal_category.hom.α_hom X Y Z)) (category_theory.free_monoidal_category.hom.id (X.tensor (Y.tensor Z)))
- associator_naturality : ∀ {C : Type u} {X₁ X₂ X₃ Y₁ Y₂ Y₃ : category_theory.free_monoidal_category C} (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 (category_theory.free_monoidal_category.hom.α_hom Y₁ Y₂ Y₃)) ((category_theory.free_monoidal_category.hom.α_hom X₁ X₂ X₃).comp (f₁.tensor (f₂.tensor f₃)))
- ρ_hom_inv : ∀ {C : Type u} {X : category_theory.free_monoidal_category C}, category_theory.free_monoidal_category.hom_equiv ((category_theory.free_monoidal_category.hom.ρ_hom X).comp (category_theory.free_monoidal_category.hom.ρ_inv X)) (category_theory.free_monoidal_category.hom.id (X.tensor category_theory.free_monoidal_category.unit))
- ρ_inv_hom : ∀ {C : Type u} {X : category_theory.free_monoidal_category C}, category_theory.free_monoidal_category.hom_equiv ((category_theory.free_monoidal_category.hom.ρ_inv X).comp (category_theory.free_monoidal_category.hom.ρ_hom X)) (category_theory.free_monoidal_category.hom.id X)
- ρ_naturality : ∀ {C : Type u} {X Y : category_theory.free_monoidal_category C} (f : X.hom Y), category_theory.free_monoidal_category.hom_equiv ((f.tensor (category_theory.free_monoidal_category.hom.id category_theory.free_monoidal_category.unit)).comp (category_theory.free_monoidal_category.hom.ρ_hom Y)) ((category_theory.free_monoidal_category.hom.ρ_hom X).comp f)
- l_hom_inv : ∀ {C : Type u} {X : category_theory.free_monoidal_category C}, category_theory.free_monoidal_category.hom_equiv ((category_theory.free_monoidal_category.hom.l_hom X).comp (category_theory.free_monoidal_category.hom.l_inv X)) (category_theory.free_monoidal_category.hom.id (category_theory.free_monoidal_category.unit.tensor X))
- l_inv_hom : ∀ {C : Type u} {X : category_theory.free_monoidal_category C}, category_theory.free_monoidal_category.hom_equiv ((category_theory.free_monoidal_category.hom.l_inv X).comp (category_theory.free_monoidal_category.hom.l_hom X)) (category_theory.free_monoidal_category.hom.id X)
- l_naturality : ∀ {C : Type u} {X Y : category_theory.free_monoidal_category C} (f : X.hom Y), category_theory.free_monoidal_category.hom_equiv (((category_theory.free_monoidal_category.hom.id category_theory.free_monoidal_category.unit).tensor f).comp (category_theory.free_monoidal_category.hom.l_hom Y)) ((category_theory.free_monoidal_category.hom.l_hom X).comp f)
- pentagon : ∀ {C : Type u} {W X Y Z : category_theory.free_monoidal_category C}, category_theory.free_monoidal_category.hom_equiv (((category_theory.free_monoidal_category.hom.α_hom W X Y).tensor (category_theory.free_monoidal_category.hom.id Z)).comp ((category_theory.free_monoidal_category.hom.α_hom W (X.tensor Y) Z).comp ((category_theory.free_monoidal_category.hom.id W).tensor (category_theory.free_monoidal_category.hom.α_hom X Y Z)))) ((category_theory.free_monoidal_category.hom.α_hom (W.tensor X) Y Z).comp (category_theory.free_monoidal_category.hom.α_hom W X (Y.tensor Z)))
- triangle : ∀ {C : Type u} {X Y : category_theory.free_monoidal_category C}, category_theory.free_monoidal_category.hom_equiv ((category_theory.free_monoidal_category.hom.α_hom X category_theory.free_monoidal_category.unit Y).comp ((category_theory.free_monoidal_category.hom.id X).tensor (category_theory.free_monoidal_category.hom.l_hom Y))) ((category_theory.free_monoidal_category.hom.ρ_hom X).tensor (category_theory.free_monoidal_category.hom.id Y))
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]
def
category_theory.free_monoidal_category.setoid_hom
{C : Type u}
(X Y : category_theory.free_monoidal_category C) :
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
- X.setoid_hom Y = {r := category_theory.free_monoidal_category.hom_equiv Y, iseqv := _}
@[protected, instance]
Equations
- category_theory.free_monoidal_category.category_free_monoidal_category = {to_category_struct := {to_quiver := {hom := λ (X Y : category_theory.free_monoidal_category C), quotient (X.setoid_hom Y)}, id := λ (X : category_theory.free_monoidal_category C), ⟦category_theory.free_monoidal_category.hom.id X⟧, comp := λ (X Y Z : category_theory.free_monoidal_category C) (f : X ⟶ Y) (g : Y ⟶ Z), quotient.map₂ category_theory.free_monoidal_category.hom.comp _ f g}, id_comp' := _, comp_id' := _, assoc' := _}
@[protected, instance]
Equations
- category_theory.free_monoidal_category.category_theory.monoidal_category = {tensor_obj := λ (X Y : category_theory.free_monoidal_category C), X.tensor Y, tensor_hom := λ (X₁ Y₁ X₂ Y₂ : category_theory.free_monoidal_category C), quotient.map₂ category_theory.free_monoidal_category.hom.tensor _, tensor_id' := _, tensor_comp' := _, tensor_unit := category_theory.free_monoidal_category.unit C, associator := λ (X Y Z : category_theory.free_monoidal_category C), {hom := ⟦category_theory.free_monoidal_category.hom.α_hom X Y Z⟧, inv := ⟦category_theory.free_monoidal_category.hom.α_inv X Y Z⟧, hom_inv_id' := _, inv_hom_id' := _}, associator_naturality' := _, left_unitor := λ (X : category_theory.free_monoidal_category C), {hom := ⟦category_theory.free_monoidal_category.hom.l_hom X⟧, inv := ⟦category_theory.free_monoidal_category.hom.l_inv X⟧, hom_inv_id' := _, inv_hom_id' := _}, left_unitor_naturality' := _, right_unitor := λ (X : category_theory.free_monoidal_category C), {hom := ⟦category_theory.free_monoidal_category.hom.ρ_hom X⟧, inv := ⟦category_theory.free_monoidal_category.hom.ρ_inv X⟧, hom_inv_id' := _, inv_hom_id' := _}, right_unitor_naturality' := _, pentagon' := _, triangle' := _}
@[simp]
theorem
category_theory.free_monoidal_category.mk_id
{C : Type u}
{X : category_theory.free_monoidal_category C} :
@[simp]
theorem
category_theory.free_monoidal_category.mk_α_hom
{C : Type u}
{X Y Z : category_theory.free_monoidal_category C} :
@[simp]
theorem
category_theory.free_monoidal_category.mk_α_inv
{C : Type u}
{X Y Z : category_theory.free_monoidal_category C} :
@[simp]
theorem
category_theory.free_monoidal_category.mk_ρ_hom
{C : Type u}
{X : category_theory.free_monoidal_category C} :
@[simp]
theorem
category_theory.free_monoidal_category.mk_ρ_inv
{C : Type u}
{X : category_theory.free_monoidal_category C} :
@[simp]
theorem
category_theory.free_monoidal_category.mk_l_hom
{C : Type u}
{X : category_theory.free_monoidal_category C} :
@[simp]
theorem
category_theory.free_monoidal_category.mk_l_inv
{C : Type u}
{X : category_theory.free_monoidal_category C} :
@[simp]
theorem
category_theory.free_monoidal_category.tensor_eq_tensor
{C : Type u}
{X Y : category_theory.free_monoidal_category C} :
def
category_theory.free_monoidal_category.project_obj
{C : Type u}
{D : Type u'}
[category_theory.category D]
[category_theory.monoidal_category D]
(f : C → D) :
Auxiliary definition for free_monoidal_category.project.
Equations
- category_theory.free_monoidal_category.project_obj f (X.tensor Y) = category_theory.free_monoidal_category.project_obj f X ⊗ category_theory.free_monoidal_category.project_obj f Y
- category_theory.free_monoidal_category.project_obj f category_theory.free_monoidal_category.unit = 𝟙_ D
- category_theory.free_monoidal_category.project_obj f (category_theory.free_monoidal_category.of X) = f X
@[simp]
def
category_theory.free_monoidal_category.project_map_aux
{C : Type u}
{D : Type u'}
[category_theory.category D]
[category_theory.monoidal_category D]
(f : C → D)
{X Y : category_theory.free_monoidal_category C} :
Auxiliary definition for free_monoidal_category.project.
Equations
- category_theory.free_monoidal_category.project_map_aux f (f_1.tensor g) = category_theory.free_monoidal_category.project_map_aux f f_1 ⊗ category_theory.free_monoidal_category.project_map_aux f g
- category_theory.free_monoidal_category.project_map_aux f (f_1.comp g) = category_theory.free_monoidal_category.project_map_aux f f_1 ≫ category_theory.free_monoidal_category.project_map_aux f g
- category_theory.free_monoidal_category.project_map_aux f (category_theory.free_monoidal_category.hom.ρ_inv _x) = (ρ_ (category_theory.free_monoidal_category.project_obj f _x)).inv
- category_theory.free_monoidal_category.project_map_aux f (category_theory.free_monoidal_category.hom.ρ_hom _x) = (ρ_ (category_theory.free_monoidal_category.project_obj f _x)).hom
- category_theory.free_monoidal_category.project_map_aux f (category_theory.free_monoidal_category.hom.l_inv _x) = (λ_ (category_theory.free_monoidal_category.project_obj f _x)).inv
- category_theory.free_monoidal_category.project_map_aux f (category_theory.free_monoidal_category.hom.l_hom _x) = (λ_ (category_theory.free_monoidal_category.project_obj f _x)).hom
- category_theory.free_monoidal_category.project_map_aux f (category_theory.free_monoidal_category.hom.α_inv _x _x_1 _x_2) = (α_ (category_theory.free_monoidal_category.project_obj f _x) (category_theory.free_monoidal_category.project_obj f _x_1) (category_theory.free_monoidal_category.project_obj f _x_2)).inv
- category_theory.free_monoidal_category.project_map_aux f (category_theory.free_monoidal_category.hom.α_hom _x _x_1 _x_2) = (α_ (category_theory.free_monoidal_category.project_obj f _x) (category_theory.free_monoidal_category.project_obj f _x_1) (category_theory.free_monoidal_category.project_obj f _x_2)).hom
- category_theory.free_monoidal_category.project_map_aux f (category_theory.free_monoidal_category.hom.id _x) = 𝟙 (category_theory.free_monoidal_category.project_obj f _x)
def
category_theory.free_monoidal_category.project_map
{C : Type u}
{D : Type u'}
[category_theory.category D]
[category_theory.monoidal_category D]
(f : C → D)
(X Y : category_theory.free_monoidal_category C) :
Auxiliary definition for free_monoidal_category.project.
def
category_theory.free_monoidal_category.project
{C : Type u}
{D : Type u'}
[category_theory.category D]
[category_theory.monoidal_category D]
(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
- category_theory.free_monoidal_category.project f = {to_lax_monoidal_functor := {to_functor := {obj := category_theory.free_monoidal_category.project_obj f, map := category_theory.free_monoidal_category.project_map f, map_id' := _, map_comp' := _}, ε := 𝟙 (𝟙_ D), μ := λ (X Y : category_theory.free_monoidal_category C), 𝟙 ({obj := category_theory.free_monoidal_category.project_obj f, map := category_theory.free_monoidal_category.project_map f, map_id' := _, map_comp' := _}.obj X ⊗ {obj := category_theory.free_monoidal_category.project_obj f, map := category_theory.free_monoidal_category.project_map f, map_id' := _, map_comp' := _}.obj Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}