Documentation

Mathlib.CategoryTheory.Monoidal.Mon_

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.

Simp set for monoid object tautologies #

In this file, we also provide a simp set called mon_tauto whose goal is to prove all tautologies about morphisms from some (tensor) power of M to M, where M is a (commutative) monoid object in a (braided) monoidal category.

Please read the documentation in Mathlib/Tactic/Attr/Register.lean for full details.

TODO #

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 AddCommGrpCat ≌ RingCat. (We've already got Mon (ModuleCat R) ≌ AlgCat R, in Mathlib/CategoryTheory/Monoidal/Internal/Module.lean.)
Can you transport this monoidal structure to RingCat or AlgCat R? How does it compare to the "native" one?

class CategoryTheory.MonObj {C : Type u₁} [Category.{v₁, u₁} C] [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 : MonoidalCategoryStruct.tensorUnit C ⟶ X
The unit morphism of a monoid object.
mul : MonoidalCategoryStruct.tensorObj X X ⟶ X
The multiplication morphism of a monoid object.
one_mul : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight one X) mul = (MonoidalCategoryStruct.leftUnitor X).hom
mul_one : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X one) mul = (MonoidalCategoryStruct.rightUnitor X).hom
mul_assoc : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul X) mul = CategoryStruct.comp (MonoidalCategoryStruct.associator X X X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X mul) mul)

Instances

@[deprecated CategoryTheory.MonObj (since := "2025-09-09")]

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

Type v₁

Alias of CategoryTheory.MonObj.

A monoid object internal to a monoidal category.

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

Equations

Instances For

def CategoryTheory.MonObj.termμ :

Lean.ParserDescr

The multiplication morphism of a monoid object.

Equations

Instances For

def CategoryTheory.MonObj.«termμ[_]» :

Lean.ParserDescr

The multiplication morphism of a monoid object.

Equations

Instances For

def CategoryTheory.MonObj.termη :

Lean.ParserDescr

The unit morphism of a monoid object.

Equations

Instances For

def CategoryTheory.MonObj.«termη[_]» :

Lean.ParserDescr

The unit morphism of a monoid object.

Equations

Instances For

@[simp]

theorem CategoryTheory.MonObj.mul_one_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} (X : C) [self : MonObj X] {Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X one) (CategoryStruct.comp mul h) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).hom h

@[simp]

theorem CategoryTheory.MonObj.mul_assoc_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} (X : C) [self : MonObj X] {Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul X) (CategoryStruct.comp mul h) = CategoryStruct.comp (MonoidalCategoryStruct.associator X X X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X mul) (CategoryStruct.comp mul h))

@[simp]

theorem CategoryTheory.MonObj.one_mul_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} (X : C) [self : MonObj X] {Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight one X) (CategoryStruct.comp mul h) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).hom h

def CategoryTheory.MonObj.ofIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (e : M ≅ X) :

Transfer MonObj along an isomorphism.

Equations

Instances For

theorem CategoryTheory.MonObj.ofIso_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (e : M ≅ X) :

one = CategoryStruct.comp one e.hom

theorem CategoryTheory.MonObj.ofIso_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (e : M ≅ X) :

mul = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.inv e.inv) (CategoryStruct.comp mul e.hom)

instance CategoryTheory.MonObj.instTensorUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

MonObj (MonoidalCategoryStruct.tensorUnit C)

Equations

@[simp]

theorem CategoryTheory.MonObj.one_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

one = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.MonObj.mul_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

mul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom

theorem CategoryTheory.MonObj.ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} (h₁ h₂ : MonObj X) (H : mul = mul) :

h₁ = h₂

theorem CategoryTheory.MonObj.ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} {h₁ h₂ : MonObj X} :

h₁ = h₂ ↔ mul = mul

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom (MonoidalCategoryStruct.tensorHom f (MonoidalCategoryStruct.tensorHom g h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f g) h) (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) {Z : C} (h✝ : MonoidalCategoryStruct.tensorObj X₂ (MonoidalCategoryStruct.tensorObj Y₂ Z₂) ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (MonoidalCategoryStruct.tensorHom g h)) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f g) h) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom h✝)

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f g) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (MonoidalCategoryStruct.tensorHom g h)) (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) {Z : C} (h✝ : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X₂ Y₂) Z₂ ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f g) h) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (MonoidalCategoryStruct.tensorHom g h)) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv h✝)

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) (gh : MonoidalCategoryStruct.tensorObj Y₂ Z₂ ⟶ W) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom (MonoidalCategoryStruct.tensorHom f (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom g h) gh)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f g) h) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom (MonoidalCategoryStruct.tensorHom (CategoryStruct.id X₂) gh))

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) (gh : MonoidalCategoryStruct.tensorObj Y₂ Z₂ ⟶ W) {Z : C} (h✝ : MonoidalCategoryStruct.tensorObj X₂ W ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom g h) gh)) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f g) h) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id X₂) gh) h✝))

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) (fg : MonoidalCategoryStruct.tensorObj X₂ Y₂ ⟶ W) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) fg) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (MonoidalCategoryStruct.tensorHom g h)) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv (MonoidalCategoryStruct.tensorHom fg (CategoryStruct.id Z₂)))

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) (fg : MonoidalCategoryStruct.tensorObj X₂ Y₂ ⟶ W) {Z : C} (h✝ : MonoidalCategoryStruct.tensorObj W Z₂ ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) fg) h) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (MonoidalCategoryStruct.tensorHom g h)) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom fg (CategoryStruct.id Z₂)) h✝))

theorem CategoryTheory.Mathlib.Tactic.MonTauto.eq_one_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] :

(MonoidalCategoryStruct.leftUnitor M).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.one (CategoryStruct.id M)) MonObj.mul

theorem CategoryTheory.Mathlib.Tactic.MonTauto.eq_mul_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] :

(MonoidalCategoryStruct.rightUnitor M).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) MonObj.one) MonObj.mul

theorem CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X₁ : C} [MonObj M] (f : X₁ ⟶ M) :

CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.one f) MonObj.mul) = f

theorem CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X₁ : C} [MonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.one f) (CategoryStruct.comp MonObj.mul h)) = CategoryStruct.comp f h

theorem CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X₁ : C} [MonObj M] (f : X₁ ⟶ M) :

CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f MonObj.one) MonObj.mul) = f

theorem CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X₁ : C} [MonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f MonObj.one) (CategoryStruct.comp MonObj.mul h)) = CategoryStruct.comp f h

theorem CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (f : X ⟶ M) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X M M).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f MonObj.mul) MonObj.mul) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (CategoryStruct.id M)) MonObj.mul) (CategoryStruct.id M)) MonObj.mul

theorem CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (f : X ⟶ M) {Z : C} (h : M ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.associator X M M).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f MonObj.mul) (CategoryStruct.comp MonObj.mul h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (CategoryStruct.id M)) MonObj.mul) (CategoryStruct.id M)) (CategoryStruct.comp MonObj.mul h)

theorem CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (f : X ⟶ M) :

CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.mul f) MonObj.mul) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) f) MonObj.mul)) MonObj.mul

theorem CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (f : X ⟶ M) {Z : C} (h : M ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.mul f) (CategoryStruct.comp MonObj.mul h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) f) MonObj.mul)) (CategoryStruct.comp MonObj.mul h)

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

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

one_hom : CategoryStruct.comp MonObj.one f = MonObj.one
mul_hom : CategoryStruct.comp MonObj.mul f = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f f) MonObj.mul

Instances

@[deprecated CategoryTheory.IsMonHom (since := "2025-09-15")]

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

Alias of CategoryTheory.IsMonHom.

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

Equations

Instances For

@[simp]

theorem CategoryTheory.IsMonHom.one_hom_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M N : C} {inst✝² : MonObj M} {inst✝³ : MonObj N} (f : M ⟶ N) [self : IsMonHom f] {Z : C} (h : N ⟶ Z) :

CategoryStruct.comp MonObj.one (CategoryStruct.comp f h) = CategoryStruct.comp MonObj.one h

@[simp]

theorem CategoryTheory.IsMonHom.mul_hom_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M N : C} {inst✝² : MonObj M} {inst✝³ : MonObj N} (f : M ⟶ N) [self : IsMonHom f] {Z : C} (h : N ⟶ Z) :

CategoryStruct.comp MonObj.mul (CategoryStruct.comp f h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f f) (CategoryStruct.comp MonObj.mul h)

instance CategoryTheory.instIsMonHomId {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] :

IsMonHom (CategoryStruct.id M)

instance CategoryTheory.instIsMonHomComp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N O : C} [MonObj M] [MonObj N] [MonObj O] (f : M ⟶ N) (g : N ⟶ O) [IsMonHom f] [IsMonHom g] :

IsMonHom (CategoryStruct.comp f g)

instance CategoryTheory.isMonHom_ofIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (e : M ≅ X) :

instance CategoryTheory.instIsMonHomInvOfHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [MonObj M] [MonObj N] (f : M ≅ N) [IsMonHom f.hom] :

instance CategoryTheory.instIsMonHomHomAsIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [MonObj M] [MonObj N] {f : M ⟶ N} [IsIso f] [IsMonHom f] :

IsMonHom (asIso f).hom

structure CategoryTheory.Mon (C : Type u₁) [Category.{v₁, u₁} C] [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
The underlying object in the ambient monoidal category
mon : MonObj self.X

Instances For

@[deprecated CategoryTheory.Mon (since := "2025-09-15")]

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

Type (max u₁ v₁)

Alias of CategoryTheory.Mon.

A monoid object internal to a monoidal category.

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

Equations

Instances For

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

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

Equations

Instances For

@[simp]

theorem CategoryTheory.Mon.trivial_mon_one (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :

MonObj.one = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Mon.trivial_mon_mul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :

MonObj.mul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom

@[simp]

theorem CategoryTheory.Mon.trivial_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :

(trivial C).X = MonoidalCategoryStruct.tensorUnit C

instance CategoryTheory.Mon.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

Inhabited (Mon C)

Equations

@[simp]

theorem CategoryTheory.MonObj.one_mul_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] {Z : C} (f : Z ⟶ M) :

CategoryStruct.comp (MonoidalCategoryStruct.tensorHom one f) mul = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Z).hom f

@[simp]

theorem CategoryTheory.MonObj.mul_one_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] {Z : C} (f : Z ⟶ M) :

CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f one) mul = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Z).hom f

theorem CategoryTheory.MonObj.mul_assoc_flip {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M mul) mul = CategoryStruct.comp (MonoidalCategoryStruct.associator M M M).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul M) mul)

theorem CategoryTheory.MonObj.mul_assoc_flip_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] {Z : C} (h : M ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M mul) (CategoryStruct.comp mul h) = CategoryStruct.comp (MonoidalCategoryStruct.associator M M M).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul M) (CategoryStruct.comp mul h))

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/Basic.lean. 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/Basic.lean.

theorem CategoryTheory.MonObj.one_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N P : C} [MonObj M] [MonObj N] [MonObj P] :

theorem CategoryTheory.MonObj.Mon_tensor_mul_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : C) [MonObj M] [MonObj N] :

theorem CategoryTheory.MonObj.mul_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N P : C} [MonObj M] [MonObj N] [MonObj P] :

instance CategoryTheory.MonObj.tensorObj.instTensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [MonObj M] [MonObj N] :

MonObj (MonoidalCategoryStruct.tensorObj M N)

Equations

theorem CategoryTheory.MonObj.tensorObj.mul_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [MonObj M] [MonObj N] :

mul = CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom mul mul)

theorem CategoryTheory.MonObj.tensorObj.one_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [MonObj M] [MonObj N] :

one = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom one one)

instance CategoryTheory.MonObj.instIsMonHomTensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y Z W : C} [MonObj X] [MonObj Y] [MonObj Z] [MonObj W] {f : X ⟶ Y} {g : Z ⟶ W} [IsMonHom f] [IsMonHom g] :

IsMonHom (MonoidalCategoryStruct.tensorHom f g)

instance CategoryTheory.MonObj.instIsMonHomId {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} [MonObj X] :

IsMonHom (CategoryStruct.id X)

instance CategoryTheory.MonObj.instIsMonHomWhiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y Z : C} [MonObj X] [MonObj Y] [MonObj Z] {f : Y ⟶ Z} [IsMonHom f] :

IsMonHom (MonoidalCategoryStruct.whiskerLeft X f)

instance CategoryTheory.MonObj.instIsMonHomWhiskerRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y Z : C} [MonObj X] [MonObj Y] [MonObj Z] {f : X ⟶ Y} [IsMonHom f] :

IsMonHom (MonoidalCategoryStruct.whiskerRight f Z)

instance CategoryTheory.MonObj.instIsMonHomHomAssociator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y Z : C} [MonObj X] [MonObj Y] [MonObj Z] :

IsMonHom (MonoidalCategoryStruct.associator X Y Z).hom

instance CategoryTheory.MonObj.instIsMonHomHomLeftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X : C} [MonObj X] :

IsMonHom (MonoidalCategoryStruct.leftUnitor X).hom

instance CategoryTheory.MonObj.instIsMonHomHomRightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X : C} [MonObj X] :

IsMonHom (MonoidalCategoryStruct.rightUnitor X).hom

theorem CategoryTheory.MonObj.one_braiding {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : C) [MonObj X] [MonObj Y] :

CategoryStruct.comp one (β_ X Y).hom = one

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

Type v₁

A morphism of monoid objects.

hom : M.X ⟶ N.X
The underlying morphism
isMonHom_hom : IsMonHom self.hom

Instances For

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

x = y

theorem CategoryTheory.Mon.Hom.ext_iff {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M N : Mon C} {x y : M.Hom N} :

x = y ↔ x.hom = y.hom

@[reducible, inline]

abbrev CategoryTheory.Mon.Hom.mk' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} (f : M.X ⟶ N.X) (one_f : CategoryStruct.comp MonObj.one f = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul f = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f f) MonObj.mul := by cat_disch) :

M.Hom N

Construct a morphism M ⟶ N of Mon C from a map f : M ⟶ N and a IsMonHom f instance.

Equations

Instances For

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

M.Hom M

The identity morphism on a monoid object.

Equations

Instances For

@[simp]

theorem CategoryTheory.Mon.id_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Mon C) :

M.id.hom = CategoryStruct.id M.X

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

Inhabited (M.Hom M)

Equations

def CategoryTheory.Mon.comp {C : Type u₁} [Category.{v₁, u₁} C] [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

Instances For

@[simp]

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

(comp f g).hom = CategoryStruct.comp f.hom g.hom

instance CategoryTheory.Mon.instCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

Category.{v₁, max u₁ v₁} (Mon C)

Equations

instance CategoryTheory.Mon.instIsMonHomHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} (f : M ⟶ N) :

theorem CategoryTheory.Mon.Hom.ext' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} {f g : M ⟶ N} (w : f.hom = g.hom) :

f = g

theorem CategoryTheory.Mon.Hom.ext'_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} {f g : M ⟶ N} :

f = g ↔ f.hom = g.hom

theorem CategoryTheory.Mon.hom_injective {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} :

Function.Injective Hom.hom

@[simp]

theorem CategoryTheory.Mon.id_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Mon C) :

(CategoryStruct.id M).hom = CategoryStruct.id M.X

@[simp]

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

(CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

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

Functor (Mon C) C

The forgetful functor from monoid objects to the ambient category.

Equations

Instances For

@[simp]

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

(forget C).map f = f.hom

@[simp]

theorem CategoryTheory.Mon.forget_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) :

(forget C).obj A = A.X

instance CategoryTheory.Mon.forget_faithful {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

(forget C).Faithful

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

instance CategoryTheory.Mon.instReflectsIsomorphismsForget {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

(forget C).ReflectsIsomorphisms

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

instance CategoryTheory.Mon.instIsIsoHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} {f : M ⟶ N} [IsIso f] :

def CategoryTheory.Mon.mkIso' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [MonObj M] [MonObj N] (e : M ≅ N) [IsMonHom e.hom] :

{ X := M, mon := inst✝ } ≅ { X := N, mon := inst✝¹ }

Construct an isomorphism of monoid objects by giving a monoid isomorphism between the underlying objects.

Equations

Instances For

@[simp]

theorem CategoryTheory.Mon.mkIso'_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [MonObj M] [MonObj N] (e : M ≅ N) [IsMonHom e.hom] :

(mkIso' e).hom.hom = e.hom

@[simp]

theorem CategoryTheory.Mon.mkIso'_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [MonObj M] [MonObj N] (e : M ≅ N) [IsMonHom e.hom] :

(mkIso' e).inv.hom = e.inv

@[reducible, inline]

abbrev CategoryTheory.Mon.mkIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} (e : M.X ≅ N.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :

M ≅ N

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

Equations

Instances For

@[simp]

theorem CategoryTheory.Mon.mkIso_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} (e : M.X ≅ N.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :

(mkIso e one_f mul_f).inv.hom = e.inv

@[simp]

theorem CategoryTheory.Mon.mkIso_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} (e : M.X ≅ N.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :

(mkIso e one_f mul_f).hom.hom = e.hom

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

Unique (trivial C ⟶ A)

Equations

@[simp]

theorem CategoryTheory.Mon.uniqueHomFromTrivial_default_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) :

default.hom = MonObj.one

instance CategoryTheory.Mon.instHasInitial {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

Limits.HasInitial (Mon C)

instance CategoryTheory.Mon.monMonoidalStruct {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :

MonoidalCategoryStruct (Mon C)

Equations

@[simp]

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

(MonoidalCategoryStruct.tensorHom f g).hom = MonoidalCategoryStruct.tensorHom f.hom g.hom

@[simp]

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

(MonoidalCategoryStruct.tensorObj M N).X = MonoidalCategoryStruct.tensorObj M.X N.X

@[simp]

theorem CategoryTheory.Mon.tensorUnit_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :

(MonoidalCategoryStruct.tensorUnit (Mon C)).X = MonoidalCategoryStruct.tensorUnit C

@[simp]

theorem CategoryTheory.Mon.tensorUnit_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :

MonObj.one = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Mon.tensorUnit_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :

MonObj.mul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom

@[simp]

theorem CategoryTheory.Mon.tensorObj_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : Mon C) :

MonObj.one = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom MonObj.one MonObj.one)

@[simp]

theorem CategoryTheory.Mon.tensorObj_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : Mon C) :

MonObj.mul = CategoryStruct.comp (MonoidalCategory.tensorμ X.X Y.X X.X Y.X) (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul)

@[simp]

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

(MonoidalCategoryStruct.whiskerRight f Z).hom = MonoidalCategoryStruct.whiskerRight f.hom Z.X

@[simp]

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

(MonoidalCategoryStruct.whiskerLeft X f).hom = MonoidalCategoryStruct.whiskerLeft X.X f.hom

@[simp]

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

(MonoidalCategoryStruct.leftUnitor X).hom.hom = (MonoidalCategoryStruct.leftUnitor X.X).hom

@[simp]

theorem CategoryTheory.Mon.leftUnitor_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : Mon C) :

(MonoidalCategoryStruct.leftUnitor X).inv.hom = (MonoidalCategoryStruct.leftUnitor X.X).inv

@[simp]

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

(MonoidalCategoryStruct.rightUnitor X).hom.hom = (MonoidalCategoryStruct.rightUnitor X.X).hom

@[simp]

theorem CategoryTheory.Mon.rightUnitor_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : Mon C) :

(MonoidalCategoryStruct.rightUnitor X).inv.hom = (MonoidalCategoryStruct.rightUnitor X.X).inv

@[simp]

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

(MonoidalCategoryStruct.associator X Y Z).hom.hom = (MonoidalCategoryStruct.associator X.X Y.X Z.X).hom

@[simp]

theorem CategoryTheory.Mon.associator_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y Z : Mon C) :

(MonoidalCategoryStruct.associator X Y Z).inv.hom = (MonoidalCategoryStruct.associator X.X Y.X Z.X).inv

@[simp]

theorem CategoryTheory.Mon.tensor_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : Mon C) :

MonObj.one = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom MonObj.one MonObj.one)

@[simp]

theorem CategoryTheory.Mon.tensor_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : Mon C) :

MonObj.mul = CategoryStruct.comp (MonoidalCategory.tensorμ M.X N.X M.X N.X) (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul)

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

MonoidalCategory (Mon C)

Equations

instance CategoryTheory.Mon.instMonObjTensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [MonObj M] [MonObj N] :

MonObj (MonoidalCategoryStruct.tensorObj M N)

Equations

theorem CategoryTheory.Mon.mul_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [MonObj M] [MonObj N] :

MonObj.mul = CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul)

theorem CategoryTheory.Mon.one_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [MonObj M] [MonObj N] :

MonObj.one = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom MonObj.one MonObj.one)

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

(forget C).Monoidal

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

Equations

@[simp]

theorem CategoryTheory.Mon.forget_ε (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :

Functor.LaxMonoidal.ε (forget C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Mon.forget_η (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :

Functor.OplaxMonoidal.η (forget C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Mon.forget_μ (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : Mon C) :

Functor.LaxMonoidal.μ (forget C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.X Y.X)

@[simp]

theorem CategoryTheory.Mon.forget_δ (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : Mon C) :

Functor.OplaxMonoidal.δ (forget C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.X Y.X)

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 CategoryTheory.MonObj.mul_braiding {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] (X Y : C) [MonObj X] [MonObj Y] :

CategoryStruct.comp mul (β_ X Y).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (β_ X Y).hom (β_ X Y).hom) mul

instance CategoryTheory.MonObj.instIsMonHomHomBraiding {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] {X Y : C} [MonObj X] [MonObj Y] :

IsMonHom (β_ X Y).hom

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

SymmetricCategory (Mon C)

Equations

@[simp]

theorem CategoryTheory.Mon.braiding_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] (M N : Mon C) :

(β_ M N).hom.hom = (β_ M.X N.X).hom

@[simp]

theorem CategoryTheory.Mon.braiding_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] (M N : Mon C) :

(β_ M N).inv.hom = (β_ M.X N.X).inv

@[reducible, inline]

abbrev CategoryTheory.Functor.monObjObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [MonObj X] :

MonObj (F.obj X)

The image of a monoid object under a lax monoidal functor is a monoid object.

Equations

Instances For

@[deprecated CategoryTheory.Functor.monObjObj (since := "2025-09-09")]

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

MonObj (F.obj X)

Alias of CategoryTheory.Functor.monObjObj.

The image of a monoid object under a lax monoidal functor is a monoid object.

Equations

Instances For

@[simp]

theorem CategoryTheory.Functor.obj.η_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [MonObj X] :

MonObj.one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map MonObj.one)

theorem CategoryTheory.Functor.obj.η_def_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [MonObj X] {Z : D} (h : F.obj X ⟶ Z) :

CategoryStruct.comp MonObj.one h = CategoryStruct.comp (LaxMonoidal.ε F) (CategoryStruct.comp (F.map MonObj.one) h)

@[simp]

theorem CategoryTheory.Functor.obj.μ_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [MonObj X] :

MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ F X X) (F.map MonObj.mul)

theorem CategoryTheory.Functor.obj.μ_def_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [MonObj X] {Z : D} (h : F.obj X ⟶ Z) :

CategoryStruct.comp MonObj.mul h = CategoryStruct.comp (LaxMonoidal.μ F X X) (CategoryStruct.comp (F.map MonObj.mul) h)

instance CategoryTheory.Functor.map.instIsMonHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X Y : C) [MonObj X] [MonObj Y] (f : X ⟶ Y) [IsMonHom f] :

IsMonHom (F.map f)

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

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

Instances For

@[simp]

theorem CategoryTheory.Functor.mapMon_obj_mon_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (A : Mon C) :

MonObj.one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map MonObj.one)

@[simp]

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

(F.mapMon.obj A).X = F.obj A.X

@[simp]

theorem CategoryTheory.Functor.mapMon_obj_mon_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (A : Mon C) :

MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map MonObj.mul)

@[simp]

theorem CategoryTheory.Functor.mapMon_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : 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.id_mapMon_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) :

MonObj.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) MonObj.one

@[simp]

theorem CategoryTheory.Functor.id_mapMon_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) :

MonObj.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.X X.X)) MonObj.mul

@[simp]

theorem CategoryTheory.Functor.comp_mapMon_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : Mon C) :

MonObj.one = CategoryStruct.comp (LaxMonoidal.ε (F.comp G)) ((F.comp G).map MonObj.one)

@[simp]

theorem CategoryTheory.Functor.comp_mapMon_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : Mon C) :

MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ (F.comp G) X.X X.X) ((F.comp G).map MonObj.mul)

def CategoryTheory.Functor.mapMonIdIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

(Functor.id C).mapMon ≅ Functor.id (Mon C)

The identity functor is also the identity on monoid objects.

Equations

Instances For

@[simp]

theorem CategoryTheory.Functor.mapMonIdIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) :

(mapMonIdIso.hom.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.Functor.mapMonIdIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) :

(mapMonIdIso.inv.app X).hom = CategoryStruct.id X.X

def CategoryTheory.Functor.mapMonCompIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] :

(F.comp G).mapMon ≅ F.mapMon.comp G.mapMon

The composition functor is also the composition on monoid objects.

Equations

Instances For

@[simp]

theorem CategoryTheory.Functor.mapMonCompIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : Mon C) :

(mapMonCompIso.hom.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

@[simp]

theorem CategoryTheory.Functor.mapMonCompIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : Mon C) :

(mapMonCompIso.inv.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

instance CategoryTheory.Functor.Faithful.mapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] [F.Faithful] :

F.mapMon.Faithful

def CategoryTheory.Functor.mapMonNatTrans {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (f : F ⟶ F') [NatTrans.IsMonoidal f] :

F.mapMon ⟶ F'.mapMon

Natural transformations between functors lift to monoid objects.

Equations

Instances For

@[simp]

theorem CategoryTheory.Functor.mapMonNatTrans_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (f : F ⟶ F') [NatTrans.IsMonoidal f] (X : Mon C) :

((mapMonNatTrans f).app X).hom = f.app X.X

def CategoryTheory.Functor.mapMonNatIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] :

F.mapMon ≅ F'.mapMon

Natural isomorphisms between functors lift to monoid objects.

Equations

Instances For

@[simp]

theorem CategoryTheory.Functor.mapMonNatIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] (X : Mon C) :

((mapMonNatIso e).inv.app X).hom = e.inv.app X.X

@[simp]

theorem CategoryTheory.Functor.mapMonNatIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] (X : Mon C) :

((mapMonNatIso e).hom.app X).hom = e.hom.app X.X

instance CategoryTheory.Functor.instIsMonHomε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] :

IsMonHom (LaxMonoidal.ε F)

@[reducible, inline]

abbrev CategoryTheory.Functor.FullyFaithful.monObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [MonObj (F.obj X)] :

Pullback a monoid object along a fully faithful oplax monoidal functor.

Equations

Instances For

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.monObj_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [MonObj (F.obj X)] :

MonObj.mul = hF.preimage (CategoryStruct.comp (OplaxMonoidal.δ F X X) MonObj.mul)

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.monObj_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [MonObj (F.obj X)] :

MonObj.one = hF.preimage (CategoryStruct.comp (OplaxMonoidal.η F) MonObj.one)

@[deprecated CategoryTheory.Functor.FullyFaithful.monObj (since := "2025-09-09")]

def CategoryTheory.Functor.FullyFaithful.mon_Class {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [MonObj (F.obj X)] :

Alias of CategoryTheory.Functor.FullyFaithful.monObj.

Pullback a monoid object along a fully faithful oplax monoidal functor.

Equations

Instances For

instance CategoryTheory.Functor.Full.mapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] [F.Full] [F.Faithful] :

instance CategoryTheory.Functor.FullyFaithful.isMonHom_preimage {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] (hF : F.FullyFaithful) {X Y : C} [MonObj X] [MonObj Y] (f : F.obj X ⟶ F.obj Y) [IsMonHom f] :

IsMonHom (hF.preimage f)

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

F.mapMon.FullyFaithful

If F : C ⥤ D is a fully faithful monoidal functor, then Mon(F) : Mon C ⥤ Mon D is fully faithful too.

Equations

Instances For

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.mapMon_preimage_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] (hF : F.FullyFaithful) {X Y : Mon C} (f : F.mapMon.obj X ⟶ F.mapMon.obj Y) :

(hF.mapMon.preimage f).hom = hF.preimage f.hom

@[simp]

theorem CategoryTheory.Functor.essImage_mapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] [F.Full] [F.Faithful] {M : Mon D} :

F.mapMon.essImage M ↔ F.essImage M.X

The essential image of a fully faithful functor between cartesian-monoidal categories is the same on monoid objects as on objects.

instance CategoryTheory.Functor.instIsMonHomμ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [BraidedCategory C] [BraidedCategory D] [F.LaxBraided] (M N : C) [MonObj M] [MonObj N] :

IsMonHom (LaxMonoidal.μ F M N)

instance CategoryTheory.Functor.instLaxMonoidalMonMapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [BraidedCategory C] [BraidedCategory D] [F.LaxBraided] :

F.mapMon.LaxMonoidal

Equations

instance CategoryTheory.Functor.instMonoidalMonMapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [BraidedCategory C] [BraidedCategory D] [F.Braided] :

F.mapMon.Monoidal

Equations

instance CategoryTheory.Functor.instLaxBraidedMonMapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [SymmetricCategory C] [SymmetricCategory D] [F.LaxBraided] :

F.mapMon.LaxBraided

Equations

instance CategoryTheory.Functor.instBraidedMonMapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [SymmetricCategory C] [SymmetricCategory D] [F.Braided] :

F.mapMon.Braided

Equations

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

Functor (LaxMonoidalFunctor C D) (Functor (Mon C) (Mon D))

mapMon is functorial in the lax monoidal functor.

Equations

Instances For

@[simp]

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

(mapMonFunctor C D).obj F = F.mapMon

@[simp]

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

(((mapMonFunctor C D).map α).app A).hom = α.hom.app A.X

def CategoryTheory.Adjunction.mapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] :

F.mapMon ⊣ G.mapMon

An adjunction of monoidal functors lifts to an adjunction of their lifts to monoid objects.

Equations

Instances For

@[simp]

theorem CategoryTheory.Adjunction.mapMon_unit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] :

a.mapMon.unit = CategoryStruct.comp Functor.mapMonIdIso.inv (CategoryStruct.comp (Functor.mapMonNatTrans a.unit) Functor.mapMonCompIso.hom)

@[simp]

theorem CategoryTheory.Adjunction.mapMon_counit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] :

a.mapMon.counit = CategoryStruct.comp Functor.mapMonCompIso.inv (CategoryStruct.comp (Functor.mapMonNatTrans a.counit) Functor.mapMonIdIso.hom)

def CategoryTheory.Equivalence.mapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] :

Mon C ≌ Mon D

An equivalence of categories lifts to an equivalence of their monoid objects.

Equations

Instances For

@[simp]

theorem CategoryTheory.Equivalence.mapMon_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] :

e.mapMon.functor = e.functor.mapMon

@[simp]

theorem CategoryTheory.Equivalence.mapMon_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] :

e.mapMon.counitIso = Functor.mapMonCompIso.symm ≪≫ Functor.mapMonNatIso e.counitIso ≪≫ Functor.mapMonIdIso

@[simp]

theorem CategoryTheory.Equivalence.mapMon_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] :

e.mapMon.inverse = e.inverse.mapMon

@[simp]

theorem CategoryTheory.Equivalence.mapMon_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] :

e.mapMon.unitIso = Functor.mapMonIdIso.symm ≪≫ Functor.mapMonNatIso e.unitIso ≪≫ Functor.mapMonCompIso

def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :

Functor (LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (Mon C)

Implementation of Mon.equivLaxMonoidalFunctorPUnit.

Equations

Instances For

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) :

(laxMonoidalToMon C).obj F = F.mapMon.obj (trivial (Discrete PUnit.{w + 1}))

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C} (α : X✝ ⟶ Y✝) :

(laxMonoidalToMon C).map α = ((Functor.mapMonFunctor (Discrete PUnit.{w + 1}) C).map α).app (trivial (Discrete PUnit.{w + 1}))

def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) :

Functor (Discrete PUnit.{w + 1}) C

Implementation of Mon.equivLaxMonoidalFunctorPUnit.

Equations

Instances For

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_map {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) {X✝ Y✝ : Discrete PUnit.{w + 1}} (x✝ : X✝ ⟶ Y✝) :

(monToLaxMonoidalObj A).map x✝ = CategoryStruct.id A.X

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_obj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) (x✝ : Discrete PUnit.{w + 1}) :

(monToLaxMonoidalObj A).obj x✝ = A.X

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

(monToLaxMonoidalObj A).LaxMonoidal

Equations

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) :

Functor.LaxMonoidal.ε (monToLaxMonoidalObj A) = MonObj.one

@[simp]

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

Functor.LaxMonoidal.μ (monToLaxMonoidalObj A) X Y = MonObj.mul

def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :

Functor (Mon C) (LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C)

Implementation of Mon.equivLaxMonoidalFunctorPUnit.

Equations

Instances For

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) :

(monToLaxMonoidal C).obj A = LaxMonoidalFunctor.of (monToLaxMonoidalObj A)

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : Mon C} (f : X✝ ⟶ Y✝) (x✝ : Discrete PUnit.{w + 1}) :

((monToLaxMonoidal C).map f).hom.app x✝ = f.hom

def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :

Functor.id (LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) ≅ (laxMonoidalToMon C).comp (monToLaxMonoidal C)

Implementation of Mon.equivLaxMonoidalFunctorPUnit.

Equations

Instances For

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (X✝ : Discrete PUnit.{w + 1}) :

((unitIso C).inv.app X).hom.app X✝ = CategoryStruct.id (X.obj (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1})))

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (X✝ : Discrete PUnit.{w + 1}) :

((unitIso C).hom.app X).hom.app X✝ = CategoryStruct.id (X.obj X✝)

def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) :

(((monToLaxMonoidal C).comp (laxMonoidalToMon C)).obj F).X ≅ ((Functor.id (Mon C)).obj F).X

Auxiliary definition for counitIso.

Equations

Instances For

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) :

(counitIsoAux C F).inv = CategoryStruct.id F.X

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) :

(counitIsoAux C F).hom = CategoryStruct.id F.X

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) :

MonObj.one = CategoryStruct.comp MonObj.one (CategoryStruct.id F.X)

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) :

MonObj.mul = CategoryStruct.comp MonObj.mul (CategoryStruct.id F.X)

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) :

IsMonHom (counitIsoAux C F).hom

@[deprecated CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux (since := "2025-09-15")]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_IsMon_Hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) :

IsMonHom (counitIsoAux C F).hom

Alias of CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux.

def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] :

(monToLaxMonoidal C).comp (laxMonoidalToMon C) ≅ Functor.id (Mon C)

Implementation of Mon.equivLaxMonoidalFunctorPUnit.

Equations

Instances For

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) :

((counitIso C).inv.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) :

((counitIso C).hom.app X).hom = CategoryStruct.id X.X

def CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C ≌ Mon C

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

Equations

Instances For

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

equivLaxMonoidalFunctorPUnit.functor = EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

equivLaxMonoidalFunctorPUnit.unitIso = EquivLaxMonoidalFunctorPUnit.unitIso C

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

equivLaxMonoidalFunctorPUnit.counitIso = EquivLaxMonoidalFunctorPUnit.counitIso C

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

equivLaxMonoidalFunctorPUnit.inverse = EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C

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

Predicate for a monoid object to be commutative.

mul_comm : CategoryStruct.comp (β_ X X).hom MonObj.mul = MonObj.mul

Instances

@[deprecated CategoryTheory.IsCommMonObj (since := "2025-09-14")]

def CategoryTheory.IsCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : C) [MonObj X] :

Alias of CategoryTheory.IsCommMonObj.

Predicate for a monoid object to be commutative.

Equations

Instances For

@[simp]

theorem CategoryTheory.IsCommMonObj.mul_comm_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {inst✝² : BraidedCategory C} (X : C) {inst✝³ : MonObj X} [self : IsCommMonObj X] {Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (β_ X X).hom (CategoryStruct.comp MonObj.mul h) = CategoryStruct.comp MonObj.mul h

@[simp]

theorem CategoryTheory.IsCommMonObj.mul_comm' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] :

CategoryStruct.comp (β_ M M).inv MonObj.mul = MonObj.mul

@[simp]

theorem CategoryTheory.IsCommMonObj.mul_comm'_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] {Z : C} (h : M ⟶ Z) :

CategoryStruct.comp (β_ M M).inv (CategoryStruct.comp MonObj.mul h) = CategoryStruct.comp MonObj.mul h

instance CategoryTheory.IsCommMonObj.instTensorUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :

IsCommMonObj (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.MonObj.mul_mul_mul_comm {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] :

CategoryStruct.comp (MonoidalCategory.tensorμ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) mul) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) mul

@[simp]

theorem CategoryTheory.MonObj.mul_mul_mul_comm_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] {Z : C} (h : M ⟶ Z) :

CategoryStruct.comp (MonoidalCategory.tensorμ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) (CategoryStruct.comp mul h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) (CategoryStruct.comp mul h)

@[deprecated CategoryTheory.MonObj.mul_mul_mul_comm (since := "2025-09-09")]

theorem CategoryTheory.Mon_Class.mul_mul_mul_comm {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] :

CategoryStruct.comp (MonoidalCategory.tensorμ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul) MonObj.mul) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul) MonObj.mul

Alias of CategoryTheory.MonObj.mul_mul_mul_comm.

@[simp]

theorem CategoryTheory.MonObj.mul_mul_mul_comm' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] :

CategoryStruct.comp (MonoidalCategory.tensorδ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) mul) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) mul

@[simp]

theorem CategoryTheory.MonObj.mul_mul_mul_comm'_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] {Z : C} (h : M ⟶ Z) :

CategoryStruct.comp (MonoidalCategory.tensorδ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) (CategoryStruct.comp mul h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) (CategoryStruct.comp mul h)

@[deprecated CategoryTheory.MonObj.mul_mul_mul_comm' (since := "2025-09-09")]

theorem CategoryTheory.Mon_Class.mul_mul_mul_comm' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] :

CategoryStruct.comp (MonoidalCategory.tensorδ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul) MonObj.mul) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul) MonObj.mul

Alias of CategoryTheory.MonObj.mul_mul_mul_comm'.

instance CategoryTheory.instIsCommMonObjTensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] {M N : C} [MonObj M] [MonObj N] [IsCommMonObj M] [IsCommMonObj N] :

IsCommMonObj (MonoidalCategoryStruct.tensorObj M N)