The category of monoids in a monoidal category. #
We define monoids in a monoidal category C and show that the category of monoids is equivalent to
the category of lax monoidal functors from the unit monoidal category to C. We also show that if
C is braided, then the category of monoids is naturally monoidal.
class
Mon_Class
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
:
Type v₁
A monoid object internal to a monoidal category.
When the monoidal category is preadditive, this is also sometimes called an "algebra object".
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
The multiplication morphism of a monoid object.
Equations
- Mon_Class.termμ = Lean.ParserDescr.node `Mon_Class.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
- Mon_Class.termη = Lean.ParserDescr.node `Mon_Class.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
theorem
Mon_Class.mul_one'_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
{X : C}
[self : Mon_Class X]
{Z : C}
(h : X ⟶ Z)
:
theorem
Mon_Class.mul_assoc'_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
{X : C}
[self : Mon_Class X]
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.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))
theorem
Mon_Class.one_mul'_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
{X : C}
[self : Mon_Class X]
{Z : C}
(h : X ⟶ Z)
:
@[simp]
@[simp]
theorem
Mon_Class.one_mul_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
[Mon_Class X]
{Z : C}
(h : X ⟶ Z)
:
@[simp]
@[simp]
theorem
Mon_Class.mul_one_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
[Mon_Class X]
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
Mon_Class.mul_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
[Mon_Class X]
:
@[simp]
theorem
Mon_Class.mul_assoc_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
[Mon_Class X]
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.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))
theorem
Mon_Class.ext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X : C}
(h₁ h₂ : Mon_Class X)
(H : mul = mul)
:
theorem
Mon_Class.ext_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X : C}
{h₁ h₂ : Mon_Class X}
:
class
IsMon_Hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : C}
[Mon_Class M]
[Mon_Class N]
(f : M ⟶ N)
:
The property that a morphism between monoid objects is a monoid morphism.
Instances
@[simp]
theorem
IsMon_Hom.mul_hom_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
{M N : C}
{inst✝² : Mon_Class M}
{inst✝³ : Mon_Class N}
(f : M ⟶ N)
[self : IsMon_Hom f]
{Z : C}
(h : N ⟶ Z)
:
@[simp]
theorem
IsMon_Hom.one_hom_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
{M N : C}
{inst✝² : Mon_Class M}
{inst✝³ : Mon_Class N}
(f : M ⟶ N)
[self : IsMon_Hom f]
{Z : C}
(h : N ⟶ Z)
:
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
The unit morphism of the monoid object
The multiplication morphism of a monoid object
- one_mul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.one self.X) self.mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor self.X).hom
- mul_one : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X self.one) self.mul = (CategoryTheory.MonoidalCategoryStruct.rightUnitor self.X).hom
- mul_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.mul self.X) self.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator self.X self.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X self.mul) self.mul)
Instances For
theorem
Mon_.one_mul_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(self : Mon_ C)
{Z : C}
(h : self.X ⟶ Z)
:
theorem
Mon_.mul_one_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(self : Mon_ C)
{Z : C}
(h : self.X ⟶ Z)
:
@[simp]
theorem
Mon_.mul_assoc_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(self : Mon_ C)
{Z : C}
(h : self.X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.mul self.X)
(CategoryTheory.CategoryStruct.comp self.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator self.X self.X self.X).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X self.mul)
(CategoryTheory.CategoryStruct.comp self.mul h))
def
Mon_.mk'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
[Mon_Class X]
:
Mon_ C
Construct an object of Mon_ C from an object X : C and Mon_Class X instance.
Equations
- Mon_.mk' X = { X := X, one := Mon_Class.one, mul := Mon_Class.mul, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
Instances For
@[simp]
theorem
Mon_.mk'_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
[Mon_Class X]
:
@[simp]
theorem
Mon_.mk'_X
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
[Mon_Class X]
:
@[simp]
theorem
Mon_.mk'_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
[Mon_Class X]
:
instance
Mon_.instMon_ClassX
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : Mon_ C}
:
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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Mon_.trivial_X
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
@[simp]
@[simp]
instance
Mon_.instInhabited
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
:
Equations
- Mon_.instInhabited C = { default := Mon_.trivial C }
@[simp]
theorem
Mon_.one_mul_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : Mon_ C}
{Z : C}
(f : Z ⟶ M.X)
:
@[simp]
theorem
Mon_.mul_one_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : Mon_ C}
{Z : C}
(f : Z ⟶ M.X)
:
theorem
Mon_.mul_assoc_flip
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : Mon_ C}
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X M.mul) M.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X M.X M.X).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.mul M.X) M.mul)
structure
Mon_.Hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M N : Mon_ C)
:
Type v₁
A morphism of monoid objects.
The underlying morphism
- mul_hom : CategoryTheory.CategoryStruct.comp M.mul self.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom self.hom self.hom) N.mul
Instances For
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}
:
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)
:
@[reducible, inline]
abbrev
Mon_.Hom.mk'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : C}
[Mon_Class M]
[Mon_Class N]
(f : M ⟶ N)
[IsMon_Hom f]
:
Construct a morphism M ⟶ N of Mon_ C from a map f : M ⟶ N and a IsMon_Hom f instance.
Equations
- Mon_.Hom.mk' f = { hom := f, one_hom := ⋯, mul_hom := ⋯ }
Instances For
@[simp]
theorem
Mon_.Hom.one_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon_ C}
(self : M.Hom N)
{Z : C}
(h : N.X ⟶ Z)
:
@[simp]
theorem
Mon_.Hom.mul_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon_ C}
(self : M.Hom N)
{Z : C}
(h : N.X ⟶ Z)
:
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_.instIsMon_HomHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon_ C}
(f : M ⟶ N)
:
theorem
Mon_.ext_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X Y : Mon_ C}
{f g : X ⟶ Y}
:
@[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_map
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X✝ Y✝ : Mon_ C}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
Mon_.forget_obj
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon_ C)
:
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.
def
Mon_.mkIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon_ C}
(f : M.X ≅ N.X)
(one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat)
(mul_f :
CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by
aesop_cat)
:
Construct an isomorphism of monoids by giving an isomorphism between the underlying objects and checking compatibility with unit and multiplication only in the forward direction.
Equations
Instances For
@[simp]
theorem
Mon_.mkIso_hom_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon_ C}
(f : M.X ≅ N.X)
(one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat)
(mul_f :
CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by
aesop_cat)
:
@[simp]
theorem
Mon_.mkIso_inv_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N : Mon_ C}
(f : M.X ≅ N.X)
(one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat)
(mul_f :
CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by
aesop_cat)
:
instance
Mon_.uniqueHomFromTrivial
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon_ C)
:
@[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.obj.instMon_Class
{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)
[Mon_Class 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
@[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)
[Mon_Class 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)
[Mon_Class 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)
[Mon_Class 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)
[Mon_Class X]
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp Mon_Class.mul h = CategoryStruct.comp (LaxMonoidal.μ F X X) (CategoryStruct.comp (F.map Mon_Class.mul) h)
instance
CategoryTheory.Functor.map.instIsMon_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 : C)
[Mon_Class X]
[Mon_Class Y]
(f : X ⟶ Y)
[IsMon_Hom 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_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.mapMon_obj_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_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)
:
noncomputable def
CategoryTheory.Functor.mapMonIdIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory 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_hom_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(X : Mon_ C)
:
@[simp]
theorem
CategoryTheory.Functor.mapMonIdIso_inv_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(X : Mon_ C)
:
noncomputable 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]
:
noncomputable 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
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)
:
noncomputable 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)
:
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.isMon_Hom_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}
[Mon_Class X]
[Mon_Class Y]
(f : F.obj X ⟶ F.obj Y)
[IsMon_Hom 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
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)
:
noncomputable 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_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]
:
@[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]
:
noncomputable 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_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]
:
@[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]
:
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.{u + 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_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon_ C)
(x✝ : CategoryTheory.Discrete PUnit.{u + 1})
:
@[simp]
theorem
Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon_ C)
{X✝ Y✝ : CategoryTheory.Discrete PUnit.{u + 1}}
(x✝ : X✝ ⟶ Y✝)
:
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]
theorem
Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon_ C)
:
@[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.{u + 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.counitIso
(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.counitIso_inv_app_hom
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : Mon_ C)
:
@[simp]
theorem
Mon_.EquivLaxMonoidalFunctorPUnit.counitIso_hom_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
@[simp]
In this section, we prove that the category of monoids in a braided monoidal category is monoidal.
Given two monoids M and N in a braided monoidal category C,
the multiplication on the tensor product M.X ⊗ N.X is defined in the obvious way:
it is the tensor product of the multiplications on M and N,
except that the tensor factors in the source come in the wrong order,
which we fix by pre-composing with a permutation isomorphism constructed from the braiding.
(There is a subtlety here: in fact there are two ways to do these, using either the positive or negative crossing.)
A more conceptual way of understanding this definition is the following:
The braiding on C gives rise to a monoidal structure on
the tensor product functor from C × C to C.
A pair of monoids in C gives rise to a monoid in C × C,
which the tensor product functor by being monoidal takes to a monoid in C.
The permutation isomorphism appearing in the definition of
the multiplication on the tensor product of two monoids is
an instance of a more general family of isomorphisms
which together form a strength that equips the tensor product functor with a monoidal structure,
and the monoid axioms for the tensor product follow from the monoid axioms for the tensor factors
plus the properties of the strength (i.e., monoidal functor axioms).
The strength tensorμ of the tensor product functor has been defined in
Mathlib.CategoryTheory.Monoidal.Braided.
Its properties, stated as independent lemmas in that module,
are used extensively in the proofs below.
Notice that we could have followed the above plan not only conceptually
but also as a possible implementation and
could have constructed the tensor product of monoids via mapMon,
but we chose to give a more explicit definition directly in terms of tensorμ.
To complete the definition of the monoidal category structure on the category of monoids,
we need to provide definitions of associator and unitors.
The obvious candidates are the associator and unitors from C,
but we need to prove that they are monoid morphisms, i.e., compatible with unit and multiplication.
These properties translate to the monoidality of the associator and unitors
(with respect to the monoidal structures on the functors they relate),
which have also been proved in Mathlib.CategoryTheory.Monoidal.Braided.
theorem
Mon_.one_associator
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M N P : Mon_ C}
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.one N.one))
P.one))
(CategoryTheory.MonoidalCategoryStruct.associator M.X N.X P.X).hom = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.one
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom N.one P.one)))
theorem
Mon_.one_leftUnitor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : Mon_ C}
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) M.one))
(CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).hom = M.one
theorem
Mon_.one_rightUnitor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{M : Mon_ C}
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.one
(CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))))
(CategoryTheory.MonoidalCategoryStruct.rightUnitor M.X).hom = M.one
theorem
Mon_.Mon_tensor_one_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(M N : Mon_ C)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.one N.one))
(CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X)
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.mul N.mul)) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X)).hom
theorem
Mon_.Mon_tensor_mul_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(M N : Mon_ C)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.one N.one)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X)
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.mul N.mul)) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X)).hom
theorem
Mon_.Mon_tensor_mul_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(M N : Mon_ C)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X)
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.mul N.mul))
(CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X)
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.mul N.mul)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X)
(CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X)
(CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X)).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X)
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.mul N.mul)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X)
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.mul N.mul)))
theorem
Mon_.mul_associator
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M N P : Mon_ C}
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) P.X
(CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X) P.X)
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X)
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.mul N.mul))
P.mul))
(CategoryTheory.MonoidalCategoryStruct.associator M.X N.X P.X).hom = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator M.X N.X P.X).hom
(CategoryTheory.MonoidalCategoryStruct.associator M.X N.X P.X).hom)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorμ M.X (CategoryTheory.MonoidalCategoryStruct.tensorObj N.X P.X) M.X
(CategoryTheory.MonoidalCategoryStruct.tensorObj N.X P.X))
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.mul
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ N.X P.X N.X P.X)
(CategoryTheory.MonoidalCategoryStruct.tensorHom N.mul P.mul))))
theorem
Mon_.mul_leftUnitor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M : Mon_ C}
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M.X
(CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M.X)
(CategoryTheory.MonoidalCategoryStruct.tensorHom
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
M.mul))
(CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).hom = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).hom
(CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).hom)
M.mul
theorem
Mon_.mul_rightUnitor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M : Mon_ C}
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorμ M.X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M.X
(CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
(CategoryTheory.MonoidalCategoryStruct.tensorHom M.mul
(CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom))
(CategoryTheory.MonoidalCategoryStruct.rightUnitor M.X).hom = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M.X).hom
(CategoryTheory.MonoidalCategoryStruct.rightUnitor M.X).hom)
M.mul
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_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]
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_.tensorUnit_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
:
@[simp]
theorem
Mon_.tensorUnit_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
:
@[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]
@[simp]
@[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_.instMon_ClassTensorObj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M N : C}
[Mon_Class M]
[Mon_Class N]
:
@[simp]
theorem
Mon_.instMon_ClassTensorObj_one
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M N : C}
[Mon_Class M]
[Mon_Class N]
:
@[simp]
theorem
Mon_.instMon_ClassTensorObj_mul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
{M N : C}
[Mon_Class M]
[Mon_Class N]
:
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)
:
theorem
Mon_.one_braiding
{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
Mon_.mul_braiding
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.SymmetricCategory C]
{X Y : Mon_ C}
:
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.
class
IsCommMon
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : C)
[Mon_Class X]
:
Predicate for a monoid object to be commutative.
Instances
@[simp]
theorem
IsCommMon.mul_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : C)
[Mon_Class X]
[IsCommMon X]
:
@[simp]
theorem
IsCommMon.mul_comm_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : C)
[Mon_Class X]
[IsCommMon X]
{Z : C}
(h : X ⟶ Z)
:
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.) - 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.