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.
class
MonObj
{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".
The unit morphism of a monoid object.
The multiplication morphism of a monoid object.
- mul_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight mul X) mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X mul) mul)
Instances
@[deprecated MonObj (since := "2025-09-09")]
def
Mon_Class
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
:
Type v₁
Alias of MonObj.
A monoid object internal to a monoidal category.
When the monoidal category is preadditive, this is also sometimes called an "algebra object".
Instances For
The multiplication morphism of a monoid object.
Equations
- MonObj.termμ = Lean.ParserDescr.node `MonObj.termμ 1024 (Lean.ParserDescr.symbol "μ")
Instances For
The multiplication morphism of a monoid object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unit morphism of a monoid object.
Equations
- MonObj.termη = Lean.ParserDescr.node `MonObj.termη 1024 (Lean.ParserDescr.symbol "η")
Instances For
The unit morphism of a monoid object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
MonObj.mul_assoc_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
(X : C)
[self : MonObj X]
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight mul X)
(CategoryTheory.CategoryStruct.comp mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X mul)
(CategoryTheory.CategoryStruct.comp mul h))
@[simp]
theorem
MonObj.mul_one_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
(X : C)
[self : MonObj X]
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
MonObj.one_mul_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
(X : C)
[self : MonObj X]
{Z : C}
(h : X ⟶ Z)
:
def
MonObj.ofIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M X : C}
[MonObj M]
(e : M ≅ X)
:
MonObj X
Transfer MonObj along an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MonObj.ofIso_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M X : C}
[MonObj M]
(e : M ≅ X)
:
theorem
MonObj.ofIso_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M X : C}
[MonObj M]
(e : M ≅ X)
:
instance
MonObj.instTensorUnit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
theorem
MonObj.ext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X : C}
(h₁ h₂ : MonObj X)
(H : mul = mul)
:
theorem
MonObj.ext_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X : C}
{h₁ h₂ : MonObj X}
:
theorem
Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
(h : Z₁ ⟶ Z₂)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom
(CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
(CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom
theorem
Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
(h : Z₁ ⟶ Z₂)
{Z : C}
(h✝ : CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Z₂) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h)) h✝) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom h✝)
theorem
Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
(h : Z₁ ⟶ Z₂)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
(CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv
theorem
Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
(h : Z₁ ⟶ Z₂)
{Z : C}
(h✝ : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) Z₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h) h✝) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv h✝)
theorem
Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
(h : Z₁ ⟶ Z₂)
(gh : CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Z₂ ⟶ W)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom
(CategoryTheory.MonoidalCategoryStruct.tensorHom f
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g h) gh)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X₂) gh))
theorem
Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_comp_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
(h : Z₁ ⟶ Z₂)
(gh : CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Z₂ ⟶ W)
{Z : C}
(h✝ : CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ W ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom f
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g h) gh))
h✝) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X₂) gh) h✝))
theorem
Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
(h : Z₁ ⟶ Z₂)
(fg : CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂ ⟶ W)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) fg) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom fg (CategoryTheory.CategoryStruct.id Z₂)))
theorem
Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_comp_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C}
(f : X₁ ⟶ X₂)
(g : Y₁ ⟶ Y₂)
(h : Z₁ ⟶ Z₂)
(fg : CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂ ⟶ W)
{Z : C}
(h✝ : CategoryTheory.MonoidalCategoryStruct.tensorObj W Z₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) fg) h)
h✝) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom fg (CategoryTheory.CategoryStruct.id Z₂)) h✝))
theorem
Mathlib.Tactic.MonTauto.eq_one_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : C}
[MonObj M]
:
theorem
Mathlib.Tactic.MonTauto.eq_mul_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : C}
[MonObj M]
:
theorem
Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M X₁ : C}
[MonObj M]
(f : X₁ ⟶ M)
:
theorem
Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M X₁ : C}
[MonObj M]
(f : X₁ ⟶ M)
{Z : C}
(h : M ⟶ Z)
:
theorem
Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M X₁ : C}
[MonObj M]
(f : X₁ ⟶ M)
:
theorem
Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M X₁ : C}
[MonObj M]
(f : X₁ ⟶ M)
{Z : C}
(h : M ⟶ Z)
:
theorem
Mathlib.Tactic.MonTauto.mul_assoc_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M X : C}
[MonObj M]
(f : X ⟶ M)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X M M).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f MonObj.mul) MonObj.mul) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id M)) MonObj.mul)
(CategoryTheory.CategoryStruct.id M))
MonObj.mul
theorem
Mathlib.Tactic.MonTauto.mul_assoc_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M X : C}
[MonObj M]
(f : X ⟶ M)
{Z : C}
(h : M ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X M M).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f MonObj.mul)
(CategoryTheory.CategoryStruct.comp MonObj.mul h)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id M)) MonObj.mul)
(CategoryTheory.CategoryStruct.id M))
(CategoryTheory.CategoryStruct.comp MonObj.mul h)
theorem
Mathlib.Tactic.MonTauto.mul_assoc_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M X : C}
[MonObj M]
(f : X ⟶ M)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom MonObj.mul f) MonObj.mul) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) f) MonObj.mul))
MonObj.mul
theorem
Mathlib.Tactic.MonTauto.mul_assoc_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M X : C}
[MonObj M]
(f : X ⟶ M)
{Z : C}
(h : M ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom MonObj.mul f)
(CategoryTheory.CategoryStruct.comp MonObj.mul h)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) f) MonObj.mul))
(CategoryTheory.CategoryStruct.comp MonObj.mul h)
class
IsMonHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : C}
[MonObj M]
[MonObj N]
(f : M ⟶ N)
:
The property that a morphism between monoid objects is a monoid morphism.
Instances
@[deprecated IsMonHom (since := "2025-09-15")]
def
IsMon_Hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : C}
[MonObj M]
[MonObj N]
(f : M ⟶ N)
:
Alias of IsMonHom.
The property that a morphism between monoid objects is a monoid morphism.
Instances For
@[simp]
theorem
IsMonHom.one_hom_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
{M N : C}
{inst✝² : MonObj M}
{inst✝³ : MonObj N}
(f : M ⟶ N)
[self : IsMonHom f]
{Z : C}
(h : N ⟶ Z)
:
@[simp]
theorem
IsMonHom.mul_hom_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
{M N : C}
{inst✝² : MonObj M}
{inst✝³ : MonObj N}
(f : M ⟶ N)
[self : IsMonHom f]
{Z : C}
(h : N ⟶ Z)
:
instance
instIsMonHomId
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : C}
[MonObj M]
:
instance
instIsMonHomComp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N O : C}
[MonObj M]
[MonObj N]
[MonObj O]
(f : M ⟶ N)
(g : N ⟶ O)
[IsMonHom f]
[IsMonHom g]
:
instance
isMonHom_ofIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M X : C}
[MonObj M]
(e : M ≅ X)
:
instance
instIsMonHomInvOfHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : C}
[MonObj M]
[MonObj N]
(f : M ≅ N)
[IsMonHom f.hom]
:
instance
instIsMonHomHomAsIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : C}
[MonObj M]
[MonObj N]
{f : M ⟶ N}
[CategoryTheory.IsIso f]
[IsMonHom f]
:
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
The underlying object in the ambient monoidal category
Instances For
@[deprecated Mon (since := "2025-09-15")]
def
Mon_
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
Type (max u₁ v₁)
Alias of Mon.
A monoid object internal to a monoidal category.
When the monoidal category is preadditive, this is also sometimes called an "algebra object".
Instances For
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 := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, mon := MonObj.instTensorUnit }
Instances For
@[simp]
theorem
Mon.trivial_X
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
instance
Mon.instInhabited
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
Equations
- Mon.instInhabited = { default := Mon.trivial C }
@[simp]
theorem
MonObj.one_mul_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : C}
[MonObj M]
{Z : C}
(f : Z ⟶ M)
:
@[simp]
theorem
MonObj.mul_one_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : C}
[MonObj M]
{Z : C}
(f : Z ⟶ M)
:
theorem
MonObj.mul_assoc_flip
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : C)
[MonObj M]
:
theorem
MonObj.mul_assoc_flip_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : C)
[MonObj M]
{Z : C}
(h : M ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M mul)
(CategoryTheory.CategoryStruct.comp mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M M).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight mul M)
(CategoryTheory.CategoryStruct.comp mul h))
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)
:
theorem
Mon.Hom.ext_iff
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
{M N : Mon C}
{x y : M.Hom N}
:
@[reducible, inline]
abbrev
Mon.Hom.mk'
{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 MonObj.one f = MonObj.one := by cat_disch)
(mul_f :
CategoryTheory.CategoryStruct.comp MonObj.mul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.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
- Mon.Hom.mk' f one_f mul_f = { hom := f, isMonHom_hom := ⋯ }
Instances For
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.
Instances For
@[simp]
theorem
Mon.id_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : Mon C)
:
instance
Mon.homInhabited
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : Mon C)
:
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
Instances For
@[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)
:
instance
Mon.instCategory
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
instance
Mon.instIsMonHomHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon C}
(f : M ⟶ N)
:
theorem
Mon.Hom.ext'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon C}
{f g : M ⟶ N}
(w : f.hom = g.hom)
:
theorem
Mon.Hom.ext'_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon C}
{f g : M ⟶ N}
:
theorem
Mon.hom_injective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon C}
:
@[simp]
theorem
Mon.id_hom'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : Mon C)
:
@[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)
:
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
Instances For
@[simp]
theorem
Mon.forget_obj
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon C)
:
@[simp]
theorem
Mon.forget_map
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X✝ Y✝ : Mon C}
(f : X✝ ⟶ Y✝)
:
instance
Mon.forget_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
instance
Mon.instIsIsoHomOfMapForget
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{A B : Mon C}
(f : A ⟶ B)
[e : CategoryTheory.IsIso ((forget C).map f)]
:
instance
Mon.instReflectsIsomorphismsForget
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
The forgetful functor from monoid objects to the ambient category reflects isomorphisms.
instance
Mon.instIsIsoHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon C}
{f : M ⟶ N}
[CategoryTheory.IsIso f]
:
def
Mon.mkIso'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : C}
[MonObj M]
[MonObj N]
(e : M ≅ N)
[IsMonHom e.hom]
:
Construct an isomorphism of monoid objects by giving a monoid isomorphism between the underlying objects.
Equations
Instances For
@[simp]
theorem
Mon.mkIso'_hom_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : C}
[MonObj M]
[MonObj N]
(e : M ≅ N)
[IsMonHom e.hom]
:
@[simp]
theorem
Mon.mkIso'_inv_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : C}
[MonObj M]
[MonObj N]
(e : M ≅ N)
[IsMonHom e.hom]
:
@[reducible, inline]
abbrev
Mon.mkIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon C}
(e : M.X ≅ N.X)
(one_f : CategoryTheory.CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch)
(mul_f :
CategoryTheory.CategoryStruct.comp MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by
cat_disch)
:
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
- Mon.mkIso e one_f mul_f = Mon.mkIso' e
Instances For
@[simp]
theorem
Mon.mkIso_hom_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon C}
(e : M.X ≅ N.X)
(one_f : CategoryTheory.CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch)
(mul_f :
CategoryTheory.CategoryStruct.comp MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by
cat_disch)
:
@[simp]
theorem
Mon.mkIso_inv_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon C}
(e : M.X ≅ N.X)
(one_f : CategoryTheory.CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch)
(mul_f :
CategoryTheory.CategoryStruct.comp MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by
cat_disch)
:
instance
Mon.uniqueHomFromTrivial
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon C)
:
Equations
- A.uniqueHomFromTrivial = { default := { hom := MonObj.one, isMonHom_hom := ⋯ }, uniq := ⋯ }
@[simp]
theorem
Mon.uniqueHomFromTrivial_default_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon C)
:
instance
Mon.instHasInitial
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
@[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]
:
The image of a monoid object under a lax monoidal functor is a monoid object.
Equations
- One or more equations did not get rendered due to their size.
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]
:
Alias of CategoryTheory.Functor.monObjObj.
The image of a monoid object under a lax monoidal functor is a monoid object.
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]
:
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)
:
@[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]
:
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]
:
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]
:
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.
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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✝)
:
@[simp]
theorem
CategoryTheory.Functor.id_mapMon_one
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(X : Mon C)
:
@[simp]
theorem
CategoryTheory.Functor.id_mapMon_mul
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(X : Mon C)
:
@[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)
:
@[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)
:
The identity functor is also the identity on monoid objects.
Equations
- CategoryTheory.Functor.mapMonIdIso = CategoryTheory.NatIso.ofComponents (fun (X : Mon C) => Mon.mkIso (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).mapMon.obj X).X) ⋯ ⋯) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapMonIdIso_inv_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(X : Mon C)
:
@[simp]
theorem
CategoryTheory.Functor.mapMonIdIso_hom_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(X : Mon C)
:
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]
:
The composition functor is also the composition on monoid objects.
Equations
- CategoryTheory.Functor.mapMonCompIso = CategoryTheory.NatIso.ofComponents (fun (X : Mon C) => Mon.mkIso (CategoryTheory.Iso.refl ((F.comp G).mapMon.obj X).X) ⋯ ⋯) ⋯
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)
:
@[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)
:
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]
:
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]
:
Natural transformations between functors lift to monoid objects.
Equations
- CategoryTheory.Functor.mapMonNatTrans f = { app := fun (X : Mon C) => Mon.Hom.mk' (f.app X.X) ⋯ ⋯, naturality := ⋯ }
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)
:
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]
:
Natural isomorphisms between functors lift to monoid objects.
Equations
- CategoryTheory.Functor.mapMonNatIso e = CategoryTheory.NatIso.ofComponents (fun (X : Mon C) => Mon.mkIso (e.app X.X) ⋯ ⋯) ⋯
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)
:
@[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)
:
@[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)]
:
MonObj X
Pullback a monoid object along a fully faithful oplax monoidal functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)]
:
@[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)]
:
@[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)]
:
MonObj 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]
:
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)
:
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)
:
@[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}
:
The essential image of a fully faithful functor between cartesian-monoidal categories is the same on monoid objects as on objects.
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
- One or more equations did not get rendered due to their size.
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)
:
@[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)
:
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]
:
An adjunction of monoidal functors lifts to an adjunction of their lifts to monoid objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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]
:
@[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]
:
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]
:
An equivalence of categories lifts to an equivalence of their monoid objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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]
:
@[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]
:
@[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]
:
@[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]
:
def
Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
Implementation of Mon.equivLaxMonoidalFunctorPUnit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X✝ Y✝ : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C}
(α : X✝ ⟶ Y✝)
:
@[simp]
def
Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon C)
:
Implementation of Mon.equivLaxMonoidalFunctorPUnit.
Equations
Instances For
@[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.{w + 1}}
(x✝ : X✝ ⟶ Y✝)
:
@[simp]
theorem
Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon C)
(x✝ : CategoryTheory.Discrete PUnit.{w + 1})
:
instance
Mon.EquivLaxMonoidalFunctorPUnit.instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon C)
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[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})
:
def
Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
Implementation of Mon.equivLaxMonoidalFunctorPUnit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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.{w + 1})
:
@[simp]
theorem
Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon C)
:
def
Mon.EquivLaxMonoidalFunctorPUnit.unitIso
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
Implementation of Mon.equivLaxMonoidalFunctorPUnit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
def
Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(F : Mon C)
:
(((monToLaxMonoidal C).comp (laxMonoidalToMon C)).obj F).X ≅ ((CategoryTheory.Functor.id (Mon C)).obj F).X
Auxiliary definition for counitIso.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(F : Mon C)
:
@[simp]
theorem
Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(F : Mon C)
:
theorem
Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(F : Mon C)
:
IsMonHom (counitIsoAux C F).hom
@[deprecated Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux (since := "2025-09-15")]
theorem
Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_IsMon_Hom
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(F : Mon C)
:
IsMonHom (counitIsoAux C F).hom
Alias of Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux.
def
Mon.EquivLaxMonoidalFunctorPUnit.counitIso
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
Implementation of Mon.equivLaxMonoidalFunctorPUnit.
Equations
- Mon.EquivLaxMonoidalFunctorPUnit.counitIso C = CategoryTheory.NatIso.ofComponents (fun (F : Mon C) => Mon.mkIso (Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F) ⋯ ⋯) ⋯
Instances For
@[simp]
theorem
Mon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : Mon C)
:
@[simp]
theorem
Mon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : Mon C)
:
def
Mon.equivLaxMonoidalFunctorPUnit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory 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.
Instances For
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.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.lean.
theorem
MonObj.one_associator
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N P : C}
[MonObj M]
[MonObj N]
[MonObj P]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom one one))
one))
(CategoryTheory.MonoidalCategoryStruct.associator M N P).hom = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom one
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom one one)))
theorem
MonObj.one_leftUnitor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : C}
[MonObj M]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) one))
(CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = one
theorem
MonObj.one_rightUnitor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : C}
[MonObj M]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom one
(CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))))
(CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom = one
theorem
MonObj.Mon_tensor_one_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(M N : C)
[MonObj M]
[MonObj N]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom one one))
(CategoryTheory.MonoidalCategoryStruct.tensorObj M N))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
(CategoryTheory.MonoidalCategoryStruct.tensorHom mul mul)) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom
theorem
MonObj.Mon_tensor_mul_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(M N : C)
[MonObj M]
[MonObj N]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom one one)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
(CategoryTheory.MonoidalCategoryStruct.tensorHom mul mul)) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom
theorem
MonObj.Mon_tensor_mul_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(M N : C)
[MonObj M]
[MonObj N]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
(CategoryTheory.MonoidalCategoryStruct.tensorHom mul mul))
(CategoryTheory.MonoidalCategoryStruct.tensorObj M N))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
(CategoryTheory.MonoidalCategoryStruct.tensorHom mul mul)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
(CategoryTheory.MonoidalCategoryStruct.tensorObj M N) (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
(CategoryTheory.MonoidalCategoryStruct.tensorHom mul mul)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
(CategoryTheory.MonoidalCategoryStruct.tensorHom mul mul)))
theorem
MonObj.mul_associator
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M N P : C}
[MonObj M]
[MonObj N]
[MonObj P]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) P
(CategoryTheory.MonoidalCategoryStruct.tensorObj M N) P)
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
(CategoryTheory.MonoidalCategoryStruct.tensorHom mul mul))
mul))
(CategoryTheory.MonoidalCategoryStruct.associator M N P).hom = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom
(CategoryTheory.MonoidalCategoryStruct.associator M N P).hom)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorμ M (CategoryTheory.MonoidalCategoryStruct.tensorObj N P) M
(CategoryTheory.MonoidalCategoryStruct.tensorObj N P))
(CategoryTheory.MonoidalCategoryStruct.tensorHom mul
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ N P N P)
(CategoryTheory.MonoidalCategoryStruct.tensorHom mul mul))))
theorem
MonObj.mul_leftUnitor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M : C}
[MonObj M]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M
(CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M)
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
mul))
(CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom
(CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom)
mul
theorem
MonObj.mul_rightUnitor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M : C}
[MonObj M]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorμ M (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M
(CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
(CategoryTheory.MonoidalCategoryStruct.tensorHom mul
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom))
(CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom
(CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom)
mul
instance
MonObj.tensorObj.instTensorObj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M N : C}
[MonObj M]
[MonObj N]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
MonObj.tensorObj.mul_def
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M N : C}
[MonObj M]
[MonObj N]
:
theorem
MonObj.tensorObj.one_def
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M N : C}
[MonObj M]
[MonObj N]
:
instance
MonObj.instIsMonHomTensorHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.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]
:
instance
MonObj.instIsMonHomId
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X : C}
[MonObj X]
:
instance
MonObj.instIsMonHomWhiskerLeft
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{X Y Z : C}
[MonObj X]
[MonObj Y]
[MonObj Z]
{f : Y ⟶ Z}
[IsMonHom f]
:
instance
MonObj.instIsMonHomWhiskerRight
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{X Y Z : C}
[MonObj X]
[MonObj Y]
[MonObj Z]
{f : X ⟶ Y}
[IsMonHom f]
:
instance
MonObj.instIsMonHomHomAssociator
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{X Y Z : C}
[MonObj X]
[MonObj Y]
[MonObj Z]
:
instance
MonObj.instIsMonHomHomLeftUnitor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{X : C}
[MonObj X]
:
instance
MonObj.instIsMonHomHomRightUnitor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{X : C}
[MonObj X]
:
theorem
MonObj.one_braiding
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X Y : C)
[MonObj X]
[MonObj Y]
:
instance
Mon.monMonoidalStruct
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory 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)
:
@[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₂✝)
:
@[simp]
@[simp]
theorem
Mon.tensorObj_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X Y : Mon C)
:
@[simp]
theorem
Mon.tensorObj_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X Y : Mon C)
:
@[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)
:
@[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)
:
@[simp]
theorem
Mon.leftUnitor_hom_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : Mon C)
:
@[simp]
theorem
Mon.leftUnitor_inv_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : Mon C)
:
@[simp]
theorem
Mon.rightUnitor_hom_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : Mon C)
:
@[simp]
theorem
Mon.rightUnitor_inv_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : Mon C)
:
@[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)
:
@[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)
:
@[simp]
theorem
Mon.tensor_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(M N : Mon C)
:
@[simp]
theorem
Mon.tensor_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(M N : Mon C)
:
instance
Mon.monMonoidal
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
:
Equations
- One or more equations did not get rendered due to their size.
instance
Mon.instMonObjTensorObj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M N : C}
[MonObj M]
[MonObj N]
:
Equations
- Mon.instMonObjTensorObj = inferInstanceAs (MonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj { X := M, mon := inst✝¹ } { X := N, mon := inst✝ }).X)
theorem
Mon.one_def
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M N : C}
[MonObj M]
[MonObj N]
:
theorem
Mon.mul_def
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M N : C}
[MonObj M]
[MonObj N]
:
instance
Mon.instMonoidalForget
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
:
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]
(X Y : Mon C)
:
@[simp]
theorem
Mon.forget_δ
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X Y : Mon C)
:
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
MonObj.mul_braiding
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.SymmetricCategory C]
(X Y : C)
[MonObj X]
[MonObj Y]
:
instance
MonObj.instIsMonHomHomBraiding
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.SymmetricCategory C]
{X Y : C}
[MonObj X]
[MonObj Y]
:
instance
Mon.instSymmetricCategory
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.SymmetricCategory C]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Mon.braiding_hom_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.SymmetricCategory C]
(M N : Mon C)
:
@[simp]
theorem
Mon.braiding_inv_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.SymmetricCategory C]
(M N : Mon C)
:
class
IsCommMonObj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : C)
[MonObj X]
:
Predicate for a monoid object to be commutative.
Instances
@[deprecated IsCommMonObj (since := "2025-09-14")]
def
IsCommMon
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : C)
[MonObj X]
:
Alias of IsCommMonObj.
Predicate for a monoid object to be commutative.
Equations
Instances For
@[simp]
theorem
IsCommMonObj.mul_comm_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
{inst✝² : CategoryTheory.BraidedCategory C}
(X : C)
{inst✝³ : MonObj X}
[self : IsCommMonObj X]
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
IsCommMonObj.mul_comm'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : C)
[MonObj M]
[CategoryTheory.BraidedCategory C]
[IsCommMonObj M]
:
@[simp]
theorem
IsCommMonObj.mul_comm'_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : C)
[MonObj M]
[CategoryTheory.BraidedCategory C]
[IsCommMonObj M]
{Z : C}
(h : M ⟶ Z)
:
@[simp]
theorem
MonObj.mul_mul_mul_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : C)
[MonObj M]
[CategoryTheory.BraidedCategory C]
[IsCommMonObj M]
:
@[simp]
theorem
MonObj.mul_mul_mul_comm_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : C)
[MonObj M]
[CategoryTheory.BraidedCategory C]
[IsCommMonObj M]
{Z : C}
(h : M ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom mul mul)
(CategoryTheory.CategoryStruct.comp mul h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom mul mul)
(CategoryTheory.CategoryStruct.comp mul h)
@[deprecated MonObj.mul_mul_mul_comm (since := "2025-09-09")]
theorem
Mon_Class.mul_mul_mul_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : C)
[MonObj M]
[CategoryTheory.BraidedCategory C]
[IsCommMonObj M]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul)
MonObj.mul) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul) MonObj.mul
Alias of MonObj.mul_mul_mul_comm.
@[simp]
theorem
MonObj.mul_mul_mul_comm'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : C)
[MonObj M]
[CategoryTheory.BraidedCategory C]
[IsCommMonObj M]
:
@[simp]
theorem
MonObj.mul_mul_mul_comm'_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : C)
[MonObj M]
[CategoryTheory.BraidedCategory C]
[IsCommMonObj M]
{Z : C}
(h : M ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ M M M M)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom mul mul)
(CategoryTheory.CategoryStruct.comp mul h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom mul mul)
(CategoryTheory.CategoryStruct.comp mul h)
@[deprecated MonObj.mul_mul_mul_comm' (since := "2025-09-09")]
theorem
Mon_Class.mul_mul_mul_comm'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M : C)
[MonObj M]
[CategoryTheory.BraidedCategory C]
[IsCommMonObj M]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ M M M M)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul)
MonObj.mul) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul) MonObj.mul
Alias of MonObj.mul_mul_mul_comm'.
instance
instIsCommMonObjTensorObj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.SymmetricCategory C]
{M N : C}
[MonObj M]
[MonObj N]
[IsCommMonObj M]
[IsCommMonObj N]
:
Projects:
- Check that
Mon MonCat ≌ CommMonCat, via the Eckmann-Hilton argument. (You'll have to hook up the Cartesian monoidal structure onMonCatfirst, available in https://github.com/leanprover-community/mathlib3/pull/3463) - More generally, check that
Mon (Mon C) ≌ CommMon CwhenCis braided. - Check that
Mon TopCat ≌ [bundled topological monoids]. - Check that
Mon AddCommGrp ≌ RingCat. (We've already gotMon (ModuleCat R) ≌ AlgCat R, inMathlib/CategoryTheory/Monoidal/Internal/Module.lean.) - Can you transport this monoidal structure to
RingCatorAlgCat R? How does it compare to the "native" one? - Show that when
Fis a lax braided functorC ⥤ D, the functormap_Mon F : Mon C ⥤ Mon Dis lax monoidal.