Documentation

Mathlib.CategoryTheory.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 FreeMonoidalCategory 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.

source
inductive CategoryTheory.FreeMonoidalCategory (C : Type u) :
Type u

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
    source
    instance CategoryTheory.instInhabitedFreeMonoidalCategory :
    {a : Type u_1} → Inhabited (CategoryTheory.FreeMonoidalCategory a)
    Equations
    • CategoryTheory.instInhabitedFreeMonoidalCategory = { default := CategoryTheory.FreeMonoidalCategory.Unit }
    source
    inductive CategoryTheory.FreeMonoidalCategory.Hom {C : Type u} :
    CategoryTheory.FreeMonoidalCategory C → CategoryTheory.FreeMonoidalCategory C → Type u

    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
      source
      inductive CategoryTheory.FreeMonoidalCategory.HomEquiv {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C} {Y : CategoryTheory.FreeMonoidalCategory C} :
      CategoryTheory.FreeMonoidalCategory.Hom X Y → CategoryTheory.FreeMonoidalCategory.Hom X Y → Prop

      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.

      Instances For
        source
        instance CategoryTheory.FreeMonoidalCategory.setoidHom {C : Type u} (X : CategoryTheory.FreeMonoidalCategory C) (Y : CategoryTheory.FreeMonoidalCategory C) :
        Setoid (CategoryTheory.FreeMonoidalCategory.Hom X Y)

        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
        source
        instance CategoryTheory.FreeMonoidalCategory.categoryFreeMonoidalCategory {C : Type u} :
        CategoryTheory.Category.{u, u} (CategoryTheory.FreeMonoidalCategory C)
        Equations
        • CategoryTheory.FreeMonoidalCategory.categoryFreeMonoidalCategory = CategoryTheory.Category.mk
        source
        instance CategoryTheory.FreeMonoidalCategory.instMonoidalCategoryFreeMonoidalCategoryCategoryFreeMonoidalCategory {C : Type u} :
        CategoryTheory.MonoidalCategory (CategoryTheory.FreeMonoidalCategory C)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem CategoryTheory.FreeMonoidalCategory.mk_comp {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C} {Y : CategoryTheory.FreeMonoidalCategory C} {Z : CategoryTheory.FreeMonoidalCategory C} (f : CategoryTheory.FreeMonoidalCategory.Hom X Y) (g : CategoryTheory.FreeMonoidalCategory.Hom Y Z) :
        Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom X Z) (CategoryTheory.FreeMonoidalCategory.Hom.comp f g) = CategoryTheory.CategoryStruct.comp (Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom X Y) f) (Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom Y Z) g)
        source
        @[simp]
        theorem CategoryTheory.FreeMonoidalCategory.mk_tensor {C : Type u} {X₁ : CategoryTheory.FreeMonoidalCategory C} {Y₁ : CategoryTheory.FreeMonoidalCategory C} {X₂ : CategoryTheory.FreeMonoidalCategory C} {Y₂ : CategoryTheory.FreeMonoidalCategory C} (f : CategoryTheory.FreeMonoidalCategory.Hom X₁ Y₁) (g : CategoryTheory.FreeMonoidalCategory.Hom X₂ Y₂) :
        Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂)) (CategoryTheory.FreeMonoidalCategory.Hom.tensor f g) = CategoryTheory.MonoidalCategory.tensorHom (Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom X₁ Y₁) f) (Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom X₂ Y₂) g)
        source
        @[simp]
        theorem CategoryTheory.FreeMonoidalCategory.mk_id {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C} :
        Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom X X) (CategoryTheory.FreeMonoidalCategory.Hom.id X) = CategoryTheory.CategoryStruct.id X
        source
        @[simp]
        theorem CategoryTheory.FreeMonoidalCategory.mk_α_hom {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C} {Y : CategoryTheory.FreeMonoidalCategory C} {Z : CategoryTheory.FreeMonoidalCategory C} :
        Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z))) (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z) = (CategoryTheory.MonoidalCategory.associator X Y Z).hom
        source
        @[simp]
        theorem CategoryTheory.FreeMonoidalCategory.mk_α_inv {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C} {Y : CategoryTheory.FreeMonoidalCategory C} {Z : CategoryTheory.FreeMonoidalCategory C} :
        Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z)) (CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z) = (CategoryTheory.MonoidalCategory.associator X Y Z).inv
        source
        @[simp]
        theorem CategoryTheory.FreeMonoidalCategory.mk_ρ_hom {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C} :
        Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom (CategoryTheory.MonoidalCategory.tensorObj X CategoryTheory.MonoidalCategory.tensorUnit') X) (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom X) = (CategoryTheory.MonoidalCategory.rightUnitor X).hom
        source
        @[simp]
        theorem CategoryTheory.FreeMonoidalCategory.mk_ρ_inv {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C} :
        Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom X (CategoryTheory.MonoidalCategory.tensorObj X CategoryTheory.MonoidalCategory.tensorUnit')) (CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv X) = (CategoryTheory.MonoidalCategory.rightUnitor X).inv
        source
        @[simp]
        theorem CategoryTheory.FreeMonoidalCategory.mk_l_hom {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C} :
        Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom (CategoryTheory.MonoidalCategory.tensorObj CategoryTheory.MonoidalCategory.tensorUnit' X) X) (CategoryTheory.FreeMonoidalCategory.Hom.l_hom X) = (CategoryTheory.MonoidalCategory.leftUnitor X).hom
        source
        @[simp]
        theorem CategoryTheory.FreeMonoidalCategory.mk_l_inv {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C} :
        Quotient.mk (CategoryTheory.FreeMonoidalCategory.setoidHom X (CategoryTheory.MonoidalCategory.tensorObj CategoryTheory.MonoidalCategory.tensorUnit' X)) (CategoryTheory.FreeMonoidalCategory.Hom.l_inv X) = (CategoryTheory.MonoidalCategory.leftUnitor X).inv
        source
        @[simp]
        theorem CategoryTheory.FreeMonoidalCategory.tensor_eq_tensor {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C} {Y : CategoryTheory.FreeMonoidalCategory C} :
        CategoryTheory.FreeMonoidalCategory.tensor X Y = CategoryTheory.MonoidalCategory.tensorObj X Y
        source
        @[simp]
        theorem CategoryTheory.FreeMonoidalCategory.unit_eq_unit {C : Type u} :
        CategoryTheory.FreeMonoidalCategory.Unit = CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.FreeMonoidalCategory C)
        source
        def CategoryTheory.FreeMonoidalCategory.projectObj {C : Type u} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (f : C → D) :
        CategoryTheory.FreeMonoidalCategory C → D

        Auxiliary definition for free_monoidal_category.project.

        Equations
        Instances For
          source
          def CategoryTheory.FreeMonoidalCategory.projectMapAux {C : Type u} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (f : C → D) {X : CategoryTheory.FreeMonoidalCategory C} {Y : CategoryTheory.FreeMonoidalCategory C} :
          CategoryTheory.FreeMonoidalCategory.Hom X Y → (CategoryTheory.FreeMonoidalCategory.projectObj f X ⟶ CategoryTheory.FreeMonoidalCategory.projectObj f Y)

          Auxiliary definition for FreeMonoidalCategory.project.

          Equations
          Instances For
            source
            def CategoryTheory.FreeMonoidalCategory.projectMap {C : Type u} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (f : C → D) (X : CategoryTheory.FreeMonoidalCategory C) (Y : CategoryTheory.FreeMonoidalCategory C) :
            (X ⟶ Y) → (CategoryTheory.FreeMonoidalCategory.projectObj f X ⟶ CategoryTheory.FreeMonoidalCategory.projectObj f Y)

            Auxiliary definition for FreeMonoidalCategory.project.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def CategoryTheory.FreeMonoidalCategory.project {C : Type u} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.MonoidalCategory D] (f : C → D) :
              CategoryTheory.MonoidalFunctor (CategoryTheory.FreeMonoidalCategory 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
              • One or more equations did not get rendered due to their size.
              Instances For