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

structure CommMon_ (C : Type u₁) [] extends :
Type (max u₁ v₁)

A commutative monoid object internal to a monoidal category.

Instances For
@[simp]
theorem CommMon_.mul_comm {C : Type u₁} [] (self : ) :
CategoryTheory.CategoryStruct.comp (β_ self.X self.X).hom self.mul = self.mul
@[simp]
theorem CommMon_.mul_comm_assoc {C : Type u₁} [] (self : ) {Z : C} (h : self.X Z) :
@[simp]
theorem CommMon_.trivial_mul (C : Type u₁) [] :
().mul = .hom
@[simp]
theorem CommMon_.trivial_one (C : Type u₁) [] :
().one =
@[simp]
theorem CommMon_.trivial_X (C : Type u₁) [] :
().X = 𝟙_ C
def CommMon_.trivial (C : Type u₁) [] :

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

Equations
• = let __src := ; { toMon_ := __src, mul_comm := }
Instances For
instance CommMon_.instInhabited (C : Type u₁) [] :
Equations
• = { default := }
instance CommMon_.instCategory {C : Type u₁} [] :
Equations
@[simp]
theorem CommMon_.id_hom {C : Type u₁} [] (A : ) :
@[simp]
theorem CommMon_.comp_hom {C : Type u₁} [] {R : } {S : } {T : } (f : R S) (g : S T) :
theorem CommMon_.hom_ext {C : Type u₁} [] {A : } {B : } (f : A B) (g : A B) (h : f.hom = g.hom) :
f = g
@[simp]
theorem CommMon_.id' {C : Type u₁} [] (A : ) :
@[simp]
theorem CommMon_.comp' {C : Type u₁} [] {A₁ : } {A₂ : } {A₃ : } (f : A₁ A₂) (g : A₂ A₃) :
def CommMon_.forget₂Mon_ (C : Type u₁) [] :

The forgetful functor from commutative monoid objects to monoid objects.

Equations
Instances For
instance CommMon_.instFullMon_Forget₂Mon_ (C : Type u₁) [] :
.Full
Equations
• =
instance CommMon_.instFaithfulMon_Forget₂Mon_ (C : Type u₁) [] :
.Faithful
Equations
• =
@[simp]
theorem CommMon_.forget₂_Mon_obj_one (C : Type u₁) [] (A : ) :
(.obj A).one = A.one
@[simp]
theorem CommMon_.forget₂_Mon_obj_mul (C : Type u₁) [] (A : ) :
(.obj A).mul = A.mul
@[simp]
theorem CommMon_.forget₂_Mon_map_hom (C : Type u₁) [] {A : } {B : } (f : A B) :
(.map f).hom = f.hom
instance CommMon_.uniqueHomFromTrivial {C : Type u₁} [] (A : ) :
Equations
• A.uniqueHomFromTrivial = A.uniqueHomFromTrivial
Equations
• =
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.mapCommMon_map_hom {C : Type u₁} [] {D : Type u₂} [] (F : ) :
∀ {X Y : } (f : X Y), (F.mapCommMon.map f).hom = F.map f.hom
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.mapCommMon_obj_mul {C : Type u₁} [] {D : Type u₂} [] (F : ) (A : ) :
(F.mapCommMon.obj A).mul = CategoryTheory.CategoryStruct.comp (F A.X A.X) (F.map A.mul)
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.mapCommMon_obj_X {C : Type u₁} [] {D : Type u₂} [] (F : ) (A : ) :
(F.mapCommMon.obj A).X = F.obj A.X
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.mapCommMon_obj_one {C : Type u₁} [] {D : Type u₂} [] (F : ) (A : ) :
(F.mapCommMon.obj A).one = CategoryTheory.CategoryStruct.comp F (F.map A.one)

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.mapCommMonFunctor_obj (C : Type u₁) [] (D : Type u₂) [] (F : ) :
= F.mapCommMon
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.mapCommMonFunctor_map_app_hom (C : Type u₁) [] (D : Type u₂) [] :
∀ {X Y : } (α : X Y) (A : ), (().app A).hom = α.app A.X

mapCommMon is functorial in the lax braided functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_map (C : Type u₁) [] :
∀ {X Y : } (α : X Y), = .app
@[simp]
theorem CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_obj (C : Type u₁) [] :
= F.mapCommMon.obj

Implementation of CommMon_.equivLaxBraidedFunctorPUnit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_obj_μ (C : Type u₁) [] (A : ) :
∀ (x x_1 : ), x x_1 = A.mul
@[simp]
theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_toNatTrans_app (C : Type u₁) [] :
∀ {X Y : } (f : X Y) (x : ), .app x = f.hom
@[simp]
@[simp]
theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_obj_map (C : Type u₁) [] (A : ) :
∀ {X Y : } (x : X Y), .map x = CategoryTheory.CategoryStruct.id ((fun (x : ) => A.X) X)
@[simp]
theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_obj_obj (C : Type u₁) [] (A : ) :
∀ (x : ), .obj x = A.X

Implementation of CommMon_.equivLaxBraidedFunctorPunit.

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

Implementation of CommMon_.equivLaxBraidedFunctorPUnit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CommMon_.EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom (C : Type u₁) [] (X : ) :
(.app X).hom =
@[simp]
theorem CommMon_.EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom (C : Type u₁) [] (X : ) :
(.app X).hom =

Implementation of CommMon_.equivLaxBraidedFunctorPUnit.

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

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

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