# mathlibdocumentation

category_theory.monoidal.CommMon_

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

structure CommMon_ (C : Type u₁)  :
Type (max u₁ v₁)

A commutative monoid object internal to a monoidal category.

Instances for CommMon_
@[simp]
theorem CommMon_.mul_comm {C : Type u₁} (self : CommMon_ C) :
(β_ self.to_Mon_.X self.to_Mon_.X).hom self.to_Mon_.mul = self.to_Mon_.mul
@[simp]
theorem CommMon_.mul_comm_assoc {C : Type u₁} (self : CommMon_ C) {X' : C} (f' : self.to_Mon_.X X') :
(β_ self.to_Mon_.X self.to_Mon_.X).hom self.to_Mon_.mul f' = self.to_Mon_.mul f'
@[simp]
theorem CommMon_.trivial_to_Mon_ (C : Type u₁)  :
def CommMon_.trivial (C : Type u₁)  :

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

Equations
@[protected, instance]
def CommMon_.inhabited (C : Type u₁)  :
Equations
@[protected, instance]
Equations
@[simp]
theorem CommMon_.id_hom {C : Type u₁} (A : CommMon_ C) :
@[simp]
theorem CommMon_.comp_hom {C : Type u₁} {R S T : CommMon_ C} (f : R S) (g : S T) :
(f g).hom = f.hom g.hom
def CommMon_.forget₂_Mon_ (C : Type u₁)  :

The forgetful functor from commutative monoid objects to monoid objects.

Equations
Instances for CommMon_.forget₂_Mon_
@[protected, instance]
@[protected, instance]
@[simp]
theorem CommMon_.forget₂_Mon_obj_one (C : Type u₁) (A : CommMon_ C) :
@[simp]
theorem CommMon_.forget₂_Mon_obj_mul (C : Type u₁) (A : CommMon_ C) :
@[simp]
theorem CommMon_.forget₂_Mon_map_hom (C : Type u₁) {A B : CommMon_ C} (f : A B) :
.map f).hom = f.hom
@[protected, instance]
def CommMon_.unique_hom_from_trivial {C : Type u₁} (A : CommMon_ C) :
Equations
@[protected, instance]
def category_theory.lax_braided_functor.map_CommMon {C : Type u₁} {D : Type u₂}  :

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
@[simp]
theorem category_theory.lax_braided_functor.map_CommMon_map {C : Type u₁} {D : Type u₂} (A B : CommMon_ C) (f : A B) :
@[simp]
theorem category_theory.lax_braided_functor.map_CommMon_obj_to_Mon_ {C : Type u₁} {D : Type u₂} (A : CommMon_ C) :

map_CommMon is functorial in the lax braided functor.

Equations

Implementation of CommMon_.equiv_lax_braided_functor_punit.

Equations
@[simp]
@[simp]

Implementation of CommMon_.equiv_lax_braided_functor_punit.

Equations
@[simp]
@[simp]
@[simp]

Implementation of CommMon_.equiv_lax_braided_functor_punit.

Equations
@[simp]
@[simp]

Implementation of CommMon_.equiv_lax_braided_functor_punit.

Equations
@[simp]

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

Equations
@[simp]
@[simp]
@[simp]