The category of monoids in a monoidal category.

We define monoids in a monoidal category C and show that the category of monoids is equivalent to the category of lax monoidal functors from the unit monoidal category to C. We also show that if C is braided, then the category of monoids is naturally monoidal.

class Mon_Class {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : Type v₁

A monoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called an "algebra object".

• one : 𝟙_ C ⟶ X

  The unit morphism of a monoid object.

• mul : CategoryTheory.MonoidalCategory.tensorObj X X ⟶ X

  The multiplication morphism of a monoid object.

• one_mul' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Mon_Class.one X) Mon_Class.mul = (CategoryTheory.MonoidalCategory.leftUnitor X).hom
• mul_one' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Mon_Class.one) Mon_Class.mul = (CategoryTheory.MonoidalCategory.rightUnitor X).hom
• mul_assoc' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Mon_Class.mul X) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Mon_Class.mul) Mon_Class.mul)

def Mon_Class.termμ : Lean.ParserDescr

The multiplication morphism of a monoid object.

Equations

• Mon_Class.termμ = Lean.ParserDescr.node `Mon_Class.termμ 1024 (Lean.ParserDescr.symbol "μ")

def Mon_Class.«termμ[_]» : Lean.ParserDescr

The multiplication morphism of a monoid object.

Equations

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

def Mon_Class.termη : Lean.ParserDescr

The unit morphism of a monoid object.

Equations

• Mon_Class.termη = Lean.ParserDescr.node `Mon_Class.termη 1024 (Lean.ParserDescr.symbol "η")

def Mon_Class.«termη[_]» : Lean.ParserDescr

The unit morphism of a monoid object.

Equations

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

theorem Mon_Class.one_mul'_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {X : C} [self : Mon_Class X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Mon_Class.one X) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom h

theorem Mon_Class.mul_one'_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {X : C} [self : Mon_Class X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Mon_Class.one) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom h

theorem Mon_Class.mul_assoc'_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {X : C} [self : Mon_Class X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Mon_Class.mul X) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Mon_Class.mul) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h))

@[simp]

theorem Mon_Class.one_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mon_Class X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Mon_Class.one X) Mon_Class.mul = (CategoryTheory.MonoidalCategory.leftUnitor X).hom

@[simp]

theorem Mon_Class.one_mul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mon_Class X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Mon_Class.one X) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom h

@[simp]

theorem Mon_Class.mul_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mon_Class X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Mon_Class.one) Mon_Class.mul = (CategoryTheory.MonoidalCategory.rightUnitor X).hom

@[simp]

theorem Mon_Class.mul_one_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mon_Class X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Mon_Class.one) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom h

@[simp]

theorem Mon_Class.mul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mon_Class X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Mon_Class.mul X) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Mon_Class.mul) Mon_Class.mul)

@[simp]

theorem Mon_Class.mul_assoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mon_Class X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Mon_Class.mul X) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Mon_Class.mul) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h))

class IsMon_Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : C} [Mon_Class M] [Mon_Class N] (f : M ⟶ N) : Prop

The property that a morphism between monoid objects is a monoid morphism.

• one_hom : CategoryTheory.CategoryStruct.comp Mon_Class.one f = Mon_Class.one
• mul_hom : CategoryTheory.CategoryStruct.comp Mon_Class.mul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f f) Mon_Class.mul

@[simp]

theorem IsMon_Hom.one_hom_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : C} {inst✝² : Mon_Class M} {inst✝³ : Mon_Class N} {f : M ⟶ N} [self : IsMon_Hom f] {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp Mon_Class.one (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp Mon_Class.one h

@[simp]

theorem IsMon_Hom.mul_hom_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : C} {inst✝² : Mon_Class M} {inst✝³ : Mon_Class N} {f : M ⟶ N} [self : IsMon_Hom f] {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp Mon_Class.mul (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f f) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h)

structure Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Type (max u₁ v₁)

A monoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called an "algebra object".

• X : C
• one : 𝟙_ C ⟶ self.X
• mul : CategoryTheory.MonoidalCategory.tensorObj self.X self.X ⟶ self.X
• one_mul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.one self.X) self.mul = (CategoryTheory.MonoidalCategory.leftUnitor self.X).hom
• mul_one : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft self.X self.one) self.mul = (CategoryTheory.MonoidalCategory.rightUnitor self.X).hom
• mul_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.mul self.X) self.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator self.X self.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft self.X self.mul) self.mul)

theorem Mon_.mul_one_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : Mon_ C) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft self.X self.one) (CategoryTheory.CategoryStruct.comp self.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor self.X).hom h

theorem Mon_.one_mul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : Mon_ C) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.one self.X) (CategoryTheory.CategoryStruct.comp self.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor self.X).hom h

@[simp]

theorem Mon_.mul_assoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : Mon_ C) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.mul self.X) (CategoryTheory.CategoryStruct.comp self.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator self.X self.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft self.X self.mul) (CategoryTheory.CategoryStruct.comp self.mul h))

def Mon_.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mon_Class X] : Mon_ C

Construct an object of Mon_ C from an object X : C and Mon_Class X instance.

Equations

• Mon_.mk' X = { X := X, one := Mon_Class.one, mul := Mon_Class.mul, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

@[simp]

theorem Mon_.mk'_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mon_Class X] : (Mon_.mk' X).one = Mon_Class.one

@[simp]

theorem Mon_.mk'_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mon_Class X] : (Mon_.mk' X).mul = Mon_Class.mul

@[simp]

theorem Mon_.mk'_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) [Mon_Class X] : (Mon_.mk' X).X = X

instance Mon_.instMon_ClassX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} : Mon_Class M.X

Equations

• Mon_.instMon_ClassX = { one := M.one, mul := M.mul, one_mul' := ⋯, mul_one' := ⋯, mul_assoc' := ⋯ }

def Mon_.trivial (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Mon_ C

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

Equations

• Mon_.trivial C = { X := 𝟙_ C, one := CategoryTheory.CategoryStruct.id (𝟙_ C), mul := (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

@[simp]

theorem Mon_.trivial_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Mon_.trivial C).mul = (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom

@[simp]

theorem Mon_.trivial_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Mon_.trivial C).one = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem Mon_.trivial_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Mon_.trivial C).X = 𝟙_ C

instance Mon_.instInhabited (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Inhabited (Mon_ C)

Equations

• Mon_.instInhabited C = { default := Mon_.trivial C }

@[simp]

theorem Mon_.one_mul_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} {Z : C} (f : Z ⟶ M.X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom M.one f) M.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor Z).hom f

@[simp]

theorem Mon_.mul_one_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} {Z : C} (f : Z ⟶ M.X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f M.one) M.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor Z).hom f

theorem Mon_.mul_assoc_flip {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X M.mul) M.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M.X M.X M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight M.mul M.X) M.mul)

structure Mon_.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M N : Mon_ C) : Type v₁

A morphism of monoid objects.

• hom : M.X ⟶ N.X
• one_hom : CategoryTheory.CategoryStruct.comp M.one self.hom = N.one
• mul_hom : CategoryTheory.CategoryStruct.comp M.mul self.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom self.hom self.hom) N.mul

theorem Mon_.Hom.ext {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M N : Mon_ C} {x y : M.Hom N} (hom : x.hom = y.hom) : x = y

@[simp]

theorem Mon_.Hom.one_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Mon_ C} (self : M.Hom N) {Z : C} (h : N.X ⟶ Z) : CategoryTheory.CategoryStruct.comp M.one (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp N.one h

@[simp]

theorem Mon_.Hom.mul_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Mon_ C} (self : M.Hom N) {Z : C} (h : N.X ⟶ Z) : CategoryTheory.CategoryStruct.comp M.mul (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom self.hom self.hom) (CategoryTheory.CategoryStruct.comp N.mul h)

def Mon_.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ C) : M.Hom M

The identity morphism on a monoid object.

Equations

• M.id = { hom := CategoryTheory.CategoryStruct.id M.X, one_hom := ⋯, mul_hom := ⋯ }

@[simp]

theorem Mon_.id_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ C) : M.id.hom = CategoryTheory.CategoryStruct.id M.X

instance Mon_.homInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ C) : Inhabited (M.Hom M)

Equations

• M.homInhabited = { default := M.id }

def Mon_.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N O : Mon_ C} (f : M.Hom N) (g : N.Hom O) : M.Hom O

Composition of morphisms of monoid objects.

Equations

• Mon_.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, one_hom := ⋯, mul_hom := ⋯ }

@[simp]

theorem Mon_.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N O : Mon_ C} (f : M.Hom N) (g : N.Hom O) : (Mon_.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

instance Mon_.instCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Category.{v₁, max u₁ v₁} (Mon_ C)

Equations

• Mon_.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

theorem Mon_.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X Y : Mon_ C} {f g : X ⟶ Y} (w : f.hom = g.hom) : f = g

@[simp]

theorem Mon_.id_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ C) : (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X

@[simp]

theorem Mon_.comp_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N K : Mon_ C} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

def Mon_.forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (Mon_ C) C

The forgetful functor from monoid objects to the ambient category.

Equations

• Mon_.forget C = { obj := fun (A : Mon_ C) => A.X, map := fun {X Y : Mon_ C} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Mon_.forget_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : (Mon_.forget C).obj A = A.X

@[simp]

theorem Mon_.forget_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : Mon_ C} (f : X✝ ⟶ Y✝) : (Mon_.forget C).map f = f.hom

instance Mon_.forget_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Mon_.forget C).Faithful

Equations

• ⋯ = ⋯

instance Mon_.instIsIsoHomOfMapForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : Mon_ C} (f : A ⟶ B) [e : CategoryTheory.IsIso ((Mon_.forget C).map f)] : CategoryTheory.IsIso f.hom

Equations

• ⋯ = e

instance Mon_.instReflectsIsomorphismsForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Mon_.forget C).ReflectsIsomorphisms

The forgetful functor from monoid objects to the ambient category reflects isomorphisms.

Equations

• ⋯ = ⋯

def Mon_.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Mon_ 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.MonoidalCategory.tensorHom f.hom f.hom) N.mul := by aesop_cat) : M ≅ N

Construct an isomorphism of monoids by giving an isomorphism between the underlying objects and checking compatibility with unit and multiplication only in the forward direction.

Equations

• Mon_.mkIso f one_f mul_f = { hom := { hom := f.hom, one_hom := ⋯, mul_hom := ⋯ }, inv := { hom := f.inv, one_hom := ⋯, mul_hom := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem Mon_.mkIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Mon_ 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.MonoidalCategory.tensorHom f.hom f.hom) N.mul := by aesop_cat) : (Mon_.mkIso f one_f mul_f).inv.hom = f.inv

@[simp]

theorem Mon_.mkIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : Mon_ 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.MonoidalCategory.tensorHom f.hom f.hom) N.mul := by aesop_cat) : (Mon_.mkIso f one_f mul_f).hom.hom = f.hom

instance Mon_.uniqueHomFromTrivial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : Unique (Mon_.trivial C ⟶ A)

Equations

• A.uniqueHomFromTrivial = { default := { hom := A.one, one_hom := ⋯, mul_hom := ⋯ }, uniq := ⋯ }

@[simp]

theorem Mon_.uniqueHomFromTrivial_default_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : default.hom = A.one

instance Mon_.instHasInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Limits.HasInitial (Mon_ C)

Equations

• ⋯ = ⋯

def CategoryTheory.Functor.mapMon {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] : CategoryTheory.Functor (Mon_ C) (Mon_ D)

A lax monoidal functor takes monoid objects to monoid objects.

That is, a lax monoidal functor F : C ⥤ D induces a functor Mon_ C ⥤ Mon_ D.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapMon_obj_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] (A : Mon_ C) : (F.mapMon.obj A).one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map A.one)

@[simp]

theorem CategoryTheory.Functor.mapMon_map_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] {X✝ Y✝ : Mon_ C} (f : X✝ ⟶ Y✝) : (F.mapMon.map f).hom = F.map f.hom

@[simp]

theorem CategoryTheory.Functor.mapMon_obj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] (A : Mon_ C) : (F.mapMon.obj A).X = F.obj A.X

@[simp]

theorem CategoryTheory.Functor.mapMon_obj_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] (A : Mon_ C) : (F.mapMon.obj A).mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A.X A.X) (F.map A.mul)

def CategoryTheory.Functor.mapMonFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] : CategoryTheory.Functor (CategoryTheory.LaxMonoidalFunctor C D) (CategoryTheory.Functor (Mon_ C) (Mon_ D))

mapMon is functorial in the lax monoidal functor.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapMonFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) : (CategoryTheory.Functor.mapMonFunctor C D).obj F = F.mapMon

@[simp]

theorem CategoryTheory.Functor.mapMonFunctor_map_app_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {X✝ Y✝ : CategoryTheory.LaxMonoidalFunctor C D} (α : X✝ ⟶ Y✝) (A : Mon_ C) : (((CategoryTheory.Functor.mapMonFunctor C D).map α).app A).hom = α.hom.app A.X

def Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) (Mon_ C)

Implementation of Mon_.equivLaxMonoidalFunctorPUnit.

Equations

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

@[simp]

theorem Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) : (Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).obj F = F.mapMon.obj (Mon_.trivial (CategoryTheory.Discrete PUnit.{u + 1} ))

@[simp]

theorem Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C} (α : X✝ ⟶ Y✝) : (Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).map α = ((CategoryTheory.Functor.mapMonFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C).map α).app (Mon_.trivial (CategoryTheory.Discrete PUnit.{u + 1} ))

def Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u + 1} ) C

Implementation of Mon_.equivLaxMonoidalFunctorPUnit.

Equations

• Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A = (CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{?u.32 + 1} )).obj A.X

@[simp]

theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) {X✝ Y✝ : CategoryTheory.Discrete PUnit.{u + 1} } (x✝ : X✝ ⟶ Y✝) : (Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).map x✝ = CategoryTheory.CategoryStruct.id A.X

@[simp]

theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) (x✝ : CategoryTheory.Discrete PUnit.{u + 1} ) : (Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).obj x✝ = A.X

instance Mon_.EquivLaxMonoidalFunctorPUnit.instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : (Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A).LaxMonoidal

Equations

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

@[simp]

theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : CategoryTheory.Functor.LaxMonoidal.ε (Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) = A.one

@[simp]

theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) (X Y : CategoryTheory.Discrete PUnit.{u_1 + 1} ) : CategoryTheory.Functor.LaxMonoidal.μ (Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) X Y = A.mul

def Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor (Mon_ C) (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C)

Implementation of Mon_.equivLaxMonoidalFunctorPUnit.

Equations

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

@[simp]

theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : (Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).obj A = CategoryTheory.LaxMonoidalFunctor.of (Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A)

@[simp]

theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : Mon_ C} (f : X✝ ⟶ Y✝) (x✝ : CategoryTheory.Discrete PUnit.{u + 1} ) : ((Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).map f).hom.app x✝ = f.hom

def Mon_.EquivLaxMonoidalFunctorPUnit.unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Functor.id (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) ≅ (Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).comp (Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C)

Implementation of Mon_.equivLaxMonoidalFunctorPUnit.

Equations

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

@[simp]

theorem Mon_.EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) (X✝ : CategoryTheory.Discrete PUnit.{u + 1} ) : ((Mon_.EquivLaxMonoidalFunctorPUnit.unitIso C).inv.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj (𝟙_ (CategoryTheory.Discrete PUnit.{u + 1} )))

@[simp]

theorem Mon_.EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) (X✝ : CategoryTheory.Discrete PUnit.{u + 1} ) : ((Mon_.EquivLaxMonoidalFunctorPUnit.unitIso C).hom.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)

def Mon_.EquivLaxMonoidalFunctorPUnit.counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).comp (Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C) ≅ CategoryTheory.Functor.id (Mon_ C)

Implementation of Mon_.equivLaxMonoidalFunctorPUnit.

Equations

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

@[simp]

theorem Mon_.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Mon_ C) : ((Mon_.EquivLaxMonoidalFunctorPUnit.counitIso C).hom.app X).hom = CategoryTheory.CategoryStruct.id X.X

@[simp]

theorem Mon_.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Mon_ C) : ((Mon_.EquivLaxMonoidalFunctorPUnit.counitIso C).inv.app X).hom = CategoryTheory.CategoryStruct.id X.X

def Mon_.equivLaxMonoidalFunctorPUnit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C ≌ Mon_ C

Monoid objects in C are "just" lax monoidal functors from the trivial monoidal category to C.

Equations

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

@[simp]

theorem Mon_.equivLaxMonoidalFunctorPUnit_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Mon_.equivLaxMonoidalFunctorPUnit C).functor = Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C

@[simp]

theorem Mon_.equivLaxMonoidalFunctorPUnit_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Mon_.equivLaxMonoidalFunctorPUnit C).unitIso = Mon_.EquivLaxMonoidalFunctorPUnit.unitIso C

@[simp]

theorem Mon_.equivLaxMonoidalFunctorPUnit_inverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Mon_.equivLaxMonoidalFunctorPUnit C).inverse = Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C

@[simp]

theorem Mon_.equivLaxMonoidalFunctorPUnit_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (Mon_.equivLaxMonoidalFunctorPUnit C).counitIso = Mon_.EquivLaxMonoidalFunctorPUnit.counitIso C

In this section, we prove that the category of monoids in a braided monoidal category is monoidal.

Given two monoids M and N in a braided monoidal category C, the multiplication on the tensor product M.X ⊗ N.X is defined in the obvious way: it is the tensor product of the multiplications on M and N, except that the tensor factors in the source come in the wrong order, which we fix by pre-composing with a permutation isomorphism constructed from the braiding.

(There is a subtlety here: in fact there are two ways to do these, using either the positive or negative crossing.)

A more conceptual way of understanding this definition is the following: The braiding on C gives rise to a monoidal structure on the tensor product functor from C × C to C. A pair of monoids in C gives rise to a monoid in C × C, which the tensor product functor by being monoidal takes to a monoid in C. The permutation isomorphism appearing in the definition of the multiplication on the tensor product of two monoids is an instance of a more general family of isomorphisms which together form a strength that equips the tensor product functor with a monoidal structure, and the monoid axioms for the tensor product follow from the monoid axioms for the tensor factors plus the properties of the strength (i.e., monoidal functor axioms). The strength tensorμ of the tensor product functor has been defined in Mathlib.CategoryTheory.Monoidal.Braided. Its properties, stated as independent lemmas in that module, are used extensively in the proofs below. Notice that we could have followed the above plan not only conceptually but also as a possible implementation and could have constructed the tensor product of monoids via mapMon, but we chose to give a more explicit definition directly in terms of tensorμ.

To complete the definition of the monoidal category structure on the category of monoids, we need to provide definitions of associator and unitors. The obvious candidates are the associator and unitors from C, but we need to prove that they are monoid morphisms, i.e., compatible with unit and multiplication. These properties translate to the monoidality of the associator and unitors (with respect to the monoidal structures on the functors they relate), which have also been proved in Mathlib.CategoryTheory.Monoidal.Braided.

theorem Mon_.one_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N P : Mon_ C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom M.one N.one)) P.one)) (CategoryTheory.MonoidalCategory.associator M.X N.X P.X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom M.one (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom N.one P.one)))

theorem Mon_.one_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (𝟙_ C)) M.one)) (CategoryTheory.MonoidalCategory.leftUnitor M.X).hom = M.one

theorem Mon_.one_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom M.one (CategoryTheory.CategoryStruct.id (𝟙_ C)))) (CategoryTheory.MonoidalCategory.rightUnitor M.X).hom = M.one

theorem Mon_.Mon_tensor_one_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : Mon_ C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom M.one N.one)) (CategoryTheory.MonoidalCategory.tensorObj M.X N.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)) = (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj M.X N.X)).hom

theorem Mon_.Mon_tensor_mul_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : Mon_ C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj M.X N.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom M.one N.one))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)) = (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj M.X N.X)).hom

theorem Mon_.Mon_tensor_mul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : Mon_ C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)) (CategoryTheory.MonoidalCategory.tensorObj M.X N.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj M.X N.X) (CategoryTheory.MonoidalCategory.tensorObj M.X N.X) (CategoryTheory.MonoidalCategory.tensorObj M.X N.X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj M.X N.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)))

theorem Mon_.mul_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N P : Mon_ C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategory.tensorObj M.X N.X) P.X (CategoryTheory.MonoidalCategory.tensorObj M.X N.X) P.X) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)) P.mul)) (CategoryTheory.MonoidalCategory.associator M.X N.X P.X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator M.X N.X P.X).hom (CategoryTheory.MonoidalCategory.associator M.X N.X P.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X (CategoryTheory.MonoidalCategory.tensorObj N.X P.X) M.X (CategoryTheory.MonoidalCategory.tensorObj N.X P.X)) (CategoryTheory.MonoidalCategory.tensorHom M.mul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ N.X P.X N.X P.X) (CategoryTheory.MonoidalCategory.tensorHom N.mul P.mul))))

theorem Mon_.mul_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : Mon_ C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (𝟙_ C) M.X (𝟙_ C) M.X) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom M.mul)) (CategoryTheory.MonoidalCategory.leftUnitor M.X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor M.X).hom (CategoryTheory.MonoidalCategory.leftUnitor M.X).hom) M.mul

theorem Mon_.mul_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : Mon_ C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X (𝟙_ C) M.X (𝟙_ C)) (CategoryTheory.MonoidalCategory.tensorHom M.mul (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom)) (CategoryTheory.MonoidalCategory.rightUnitor M.X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor M.X).hom (CategoryTheory.MonoidalCategory.rightUnitor M.X).hom) M.mul

instance Mon_.monMonoidalStruct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonoidalCategoryStruct (Mon_ C)

Equations

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

@[simp]

theorem Mon_.monMonoidalStruct_tensorObj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : Mon_ C) : (CategoryTheory.MonoidalCategory.tensorObj M N).X = CategoryTheory.MonoidalCategory.tensorObj M.X N.X

@[simp]

theorem Mon_.monMonoidalStruct_tensorHom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : Mon_ C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (CategoryTheory.MonoidalCategory.tensorHom f g).hom = CategoryTheory.MonoidalCategory.tensorHom f.hom g.hom

@[simp]

theorem Mon_.tensorUnit_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (𝟙_ (Mon_ C)).X = 𝟙_ C

@[simp]

theorem Mon_.tensorUnit_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (𝟙_ (Mon_ C)).one = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem Mon_.tensorUnit_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (𝟙_ (Mon_ C)).mul = (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom

@[simp]

theorem Mon_.tensorObj_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Mon_ C) : (CategoryTheory.MonoidalCategory.tensorObj X Y).one = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom X.one Y.one)

@[simp]

theorem Mon_.tensorObj_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Mon_ C) : (CategoryTheory.MonoidalCategory.tensorObj X Y).mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X.X Y.X X.X Y.X) (CategoryTheory.MonoidalCategory.tensorHom X.mul Y.mul)

@[simp]

theorem Mon_.whiskerLeft_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X Y : Mon_ C} (f : X ⟶ Y) (Z : Mon_ C) : (CategoryTheory.MonoidalCategory.whiskerRight f Z).hom = CategoryTheory.MonoidalCategory.whiskerRight f.hom Z.X

@[simp]

theorem Mon_.whiskerRight_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : Mon_ C) {Y Z : Mon_ C} (f : Y ⟶ Z) : (CategoryTheory.MonoidalCategory.whiskerLeft X f).hom = CategoryTheory.MonoidalCategory.whiskerLeft X.X f.hom

@[simp]

theorem Mon_.leftUnitor_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : Mon_ C) : (CategoryTheory.MonoidalCategory.leftUnitor X).hom.hom = (CategoryTheory.MonoidalCategory.leftUnitor X.X).hom

@[simp]

theorem Mon_.leftUnitor_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : Mon_ C) : (CategoryTheory.MonoidalCategory.leftUnitor X).inv.hom = (CategoryTheory.MonoidalCategory.leftUnitor X.X).inv

@[simp]

theorem Mon_.rightUnitor_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : Mon_ C) : (CategoryTheory.MonoidalCategory.rightUnitor X).hom.hom = (CategoryTheory.MonoidalCategory.rightUnitor X.X).hom

@[simp]

theorem Mon_.rightUnitor_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : Mon_ C) : (CategoryTheory.MonoidalCategory.rightUnitor X).inv.hom = (CategoryTheory.MonoidalCategory.rightUnitor X.X).inv

@[simp]

theorem Mon_.associator_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : Mon_ C) : (CategoryTheory.MonoidalCategory.associator X Y Z).hom.hom = (CategoryTheory.MonoidalCategory.associator X.X Y.X Z.X).hom

@[simp]

theorem Mon_.associator_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : Mon_ C) : (CategoryTheory.MonoidalCategory.associator X Y Z).inv.hom = (CategoryTheory.MonoidalCategory.associator X.X Y.X Z.X).inv

@[simp]

theorem Mon_.tensor_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : Mon_ C) : (CategoryTheory.MonoidalCategory.tensorObj M N).one = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom M.one N.one)

@[simp]

theorem Mon_.tensor_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : Mon_ C) : (CategoryTheory.MonoidalCategory.tensorObj M N).mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)

instance Mon_.monMonoidal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonoidalCategory (Mon_ C)

Equations

• Mon_.monMonoidal = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Mon_.instMon_ClassTensorObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} [Mon_Class M] [Mon_Class N] : Mon_Class (CategoryTheory.MonoidalCategory.tensorObj M N)

Equations

• Mon_.instMon_ClassTensorObj = inferInstanceAs (Mon_Class (CategoryTheory.MonoidalCategory.tensorObj (Mon_.mk' M) (Mon_.mk' N)).X)

@[simp]

theorem Mon_.instMon_ClassTensorObj_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} [Mon_Class M] [Mon_Class N] : Mon_Class.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom Mon_Class.one Mon_Class.one)

@[simp]

theorem Mon_.instMon_ClassTensorObj_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} [Mon_Class M] [Mon_Class N] : Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategory.tensorHom Mon_Class.mul Mon_Class.mul)

instance Mon_.instMonoidalForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (Mon_.forget C).Monoidal

The forgetful functor from Mon_ C to C is monoidal when C is monoidal.

Equations

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

@[simp]

theorem Mon_.forget_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor.LaxMonoidal.ε (Mon_.forget C) = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem Mon_.forget_η (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor.OplaxMonoidal.η (Mon_.forget C) = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem Mon_.forget_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Mon_ C) : CategoryTheory.Functor.LaxMonoidal.μ (Mon_.forget C) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.X Y.X)

@[simp]

theorem Mon_.forget_δ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Mon_ C) : CategoryTheory.Functor.OplaxMonoidal.δ (Mon_.forget C) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.X Y.X)

theorem Mon_.one_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X Y : Mon_ C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorObj X Y).one (β_ X.X Y.X).hom = (CategoryTheory.MonoidalCategory.tensorObj Y X).one

We next show that if C is symmetric, then Mon_ C is braided, and indeed symmetric.

Note that Mon_ C is not braided in general when C is only braided.

The more interesting construction is the 2-category of monoids in C, bimodules between the monoids, and intertwiners between the bimodules.

When C is braided, that is a monoidal 2-category.

theorem Mon_.mul_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] {X Y : Mon_ C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorObj X Y).mul (β_ X.X Y.X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (β_ X.X Y.X).hom (β_ X.X Y.X).hom) (CategoryTheory.MonoidalCategory.tensorObj Y X).mul

instance Mon_.instSymmetricCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] : CategoryTheory.SymmetricCategory (Mon_ C)

Equations

• Mon_.instSymmetricCategory = CategoryTheory.SymmetricCategory.mk ⋯

Projects:

• Check that Mon_ MonCat ≌ CommMonCat, via the Eckmann-Hilton argument. (You'll have to hook up the cartesian monoidal structure on MonCat first, available in https://github.com/leanprover-community/mathlib3/pull/3463)
• More generally, check that Mon_ (Mon_ C) ≌ CommMon_ C when C is braided.
• Check that Mon_ TopCat ≌ [bundled topological monoids].
• Check that Mon_ AddCommGrp ≌ RingCat. (We've already got Mon_ (ModuleCat R) ≌ AlgebraCat R, in Mathlib.CategoryTheory.Monoidal.Internal.Module.)
• Can you transport this monoidal structure to RingCat or AlgebraCat R? How does it compare to the "native" one?
• Show that when F is a lax braided functor C ⥤ D, the functor map_Mon F : Mon_ C ⥤ Mon_ D is lax monoidal.