Documentation

Mathlib.CategoryTheory.Monoidal.CommMon_

The category of commutative monoids in a braided monoidal category. #

The trivial commutative monoid object. We later show this is initial in CommMon_ C.

Equations
Instances For

    The forgetful functor from commutative monoid objects to monoid objects is fully faithful.

    Equations
    Instances For

      Constructor for isomorphisms in the category CommMon_ C.

      Equations
      Instances For
        @[simp]
        theorem CommMon_.mkIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon_ C} (f : M.X N.X) (one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by aesop_cat) :
        (mkIso f one_f mul_f).hom.hom = f.hom
        @[simp]
        theorem CommMon_.mkIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon_ C} (f : M.X N.X) (one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by aesop_cat) :
        (mkIso f one_f mul_f).inv.hom = f.inv
        Equations
        • A.uniqueHomFromTrivial = A.uniqueHomFromTrivial

        A lax braided functor takes commutative monoid objects to commutative monoid objects.

        That is, a lax braided functor F : C ⥤ D induces a functor CommMon_ C ⥤ CommMon_ D.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.Functor.mapCommMon_obj_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] (A : CommMon_ C) :
          (F.mapCommMon.obj A).mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map A.mul)
          @[simp]
          theorem CategoryTheory.Functor.mapCommMon_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] (A : CommMon_ C) :
          (F.mapCommMon.obj A).X = F.obj A.X
          @[simp]
          theorem CategoryTheory.Functor.mapCommMon_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] {X✝ Y✝ : CommMon_ C} (f : X✝ Y✝) :
          (F.mapCommMon.map f).hom = F.map f.hom
          @[simp]
          theorem CategoryTheory.Functor.mapCommMon_obj_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] (A : CommMon_ C) :
          (F.mapCommMon.obj A).one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map A.one)

          mapCommMon is functorial in the lax braided functor.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.Functor.mapCommMonFunctor_map_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {X✝ Y✝ : LaxBraidedFunctor C D} (α : X✝ Y✝) (A : CommMon_ C) :
            (((mapCommMonFunctor C D).map α).app A).hom = α.hom.app A.X

            Commutative monoid objects in C are "just" braided lax monoidal functors from the trivial braided monoidal category to C.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For