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

source

structure CommMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] extends Mon_ :

Type (max u₁ v₁)

X : C
one : CategoryTheory.MonoidalCategory.tensorUnit C ⟶ s.X
mul : CategoryTheory.MonoidalCategory.tensorObj s.X s.X ⟶ s.X
one_mul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.one (CategoryTheory.CategoryStruct.id s.X)) s.mul = (CategoryTheory.MonoidalCategory.leftUnitor s.X).hom
mul_one : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id s.X) s.one) s.mul = (CategoryTheory.MonoidalCategory.rightUnitor s.X).hom
mul_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.mul (CategoryTheory.CategoryStruct.id s.X)) s.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator s.X s.X s.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id s.X) s.mul) s.mul)
mul_comm : CategoryTheory.CategoryStruct.comp (β_ s.X s.X).hom s.mul = s.mul

A commutative monoid object internal to a monoidal category.

Instances For

source

@[simp]

theorem CommMon_.mul_comm_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (self : CommMon_ C) {Z : C} (h : self.X ⟶ Z) :

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

source

@[simp]

theorem CommMon_.trivial_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(CommMon_.trivial C).toMon_.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)

source

@[simp]

theorem CommMon_.trivial_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(CommMon_.trivial C).toMon_.mul = (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).hom

source

@[simp]

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

(CommMon_.trivial C).toMon_.X = CategoryTheory.MonoidalCategory.tensorUnit C

source

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

CommMon_ C

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

Instances For

source

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

Inhabited (CommMon_ C)

source

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

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

source

@[simp]

theorem CommMon_.id_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :

(CategoryTheory.CategoryStruct.id A).hom = CategoryTheory.CategoryStruct.id A.X

source

@[simp]

theorem CommMon_.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {R : CommMon_ C} {S : CommMon_ C} {T : CommMon_ C} (f : R ⟶ S) (g : S ⟶ T) :

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

source

theorem CommMon_.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A : CommMon_ C} {B : CommMon_ C} (f : A ⟶ B) (g : A ⟶ B) (h : f.hom = g.hom) :

f = g

source

@[simp]

theorem CommMon_.id' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :

CategoryTheory.CategoryStruct.id A = CategoryTheory.CategoryStruct.id A.toMon_

source

@[simp]

theorem CommMon_.comp' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A₁ : CommMon_ C} {A₂ : CommMon_ C} {A₃ : CommMon_ C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) :

CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f g

source

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

CategoryTheory.Functor (CommMon_ C) (Mon_ C)

The forgetful functor from commutative monoid objects to monoid objects.

Instances For

source

instance CommMon_.instFullCommMon_InstCategoryCommMon_Mon_InstCategoryMon_Forget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.Full (CommMon_.forget₂Mon_ C)

source

instance CommMon_.instFaithfulCommMon_InstCategoryCommMon_Mon_InstCategoryMon_Forget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.Faithful (CommMon_.forget₂Mon_ C)

source

@[simp]

theorem CommMon_.forget₂_Mon_obj_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :

((CommMon_.forget₂Mon_ C).obj A).one = A.one

source

@[simp]

theorem CommMon_.forget₂_Mon_obj_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :

((CommMon_.forget₂Mon_ C).obj A).mul = A.mul

source

@[simp]

theorem CommMon_.forget₂_Mon_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A : CommMon_ C} {B : CommMon_ C} (f : A ⟶ B) :

((CommMon_.forget₂Mon_ C).map f).hom = f.hom

source

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

Unique (CommMon_.trivial C ⟶ A)

source

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

CategoryTheory.Limits.HasInitial (CommMon_ C)

source

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.mapCommMon_map_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.LaxBraidedFunctor C D) :

∀ {X Y : CommMon_ C} (f : X ⟶ Y), ((CategoryTheory.LaxBraidedFunctor.mapCommMon F).map f).hom = F.map f.hom

source

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.mapCommMon_obj_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.LaxBraidedFunctor C D) (A : CommMon_ C) :

((CategoryTheory.LaxBraidedFunctor.mapCommMon F).obj A).one = CategoryTheory.CategoryStruct.comp F.ε (F.map A.one)

source

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.mapCommMon_obj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.LaxBraidedFunctor C D) (A : CommMon_ C) :

((CategoryTheory.LaxBraidedFunctor.mapCommMon F).obj A).X = F.obj A.X

source

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.mapCommMon_obj_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.LaxBraidedFunctor C D) (A : CommMon_ C) :

((CategoryTheory.LaxBraidedFunctor.mapCommMon F).obj A).mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor A.X A.X) (F.map A.mul)

source

def CategoryTheory.LaxBraidedFunctor.mapCommMon {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.LaxBraidedFunctor C D) :

CategoryTheory.Functor (CommMon_ C) (CommMon_ D)

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.

Instances For

source

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.mapCommMonFunctor_map_app_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] :

∀ {X Y : CategoryTheory.LaxBraidedFunctor C D} (α : X ⟶ Y) (A : CommMon_ C), (((CategoryTheory.LaxBraidedFunctor.mapCommMonFunctor C D).map α).app A).hom = α.app A.X

source

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.mapCommMonFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.LaxBraidedFunctor C D) :

(CategoryTheory.LaxBraidedFunctor.mapCommMonFunctor C D).obj F = CategoryTheory.LaxBraidedFunctor.mapCommMon F

source

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

CategoryTheory.Functor (CategoryTheory.LaxBraidedFunctor C D) (CategoryTheory.Functor (CommMon_ C) (CommMon_ D))

mapCommMon is functorial in the lax braided functor.

Instances For

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPunit.laxBraidedToCommMon_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (F : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) :

(CommMon_.EquivLaxBraidedFunctorPunit.laxBraidedToCommMon C).obj F = (CategoryTheory.LaxBraidedFunctor.mapCommMon F).obj (CommMon_.trivial (CategoryTheory.Discrete PUnit.{u + 1} ))

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPunit.laxBraidedToCommMon_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

∀ {X Y : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C} (α : X ⟶ Y), (CommMon_.EquivLaxBraidedFunctorPunit.laxBraidedToCommMon C).map α = ((CategoryTheory.LaxBraidedFunctor.mapCommMonFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C).map α).app (CommMon_.trivial (CategoryTheory.Discrete PUnit.{u + 1} ))

source

def CommMon_.EquivLaxBraidedFunctorPunit.laxBraidedToCommMon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.Functor (CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) (CommMon_ C)

Implementation of CommMon_.equivLaxBraidedFunctorPunit.

Instances For

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided_map_toNatTrans_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

∀ {X Y : CommMon_ C} (f : X ⟶ Y) (x : CategoryTheory.Discrete PUnit.{u + 1} ), ((CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided C).map f).app x = f.hom

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided_obj_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :

∀ (x x_1 : CategoryTheory.Discrete PUnit.{u + 1} ), CategoryTheory.LaxMonoidalFunctor.μ ((CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided C).obj A).toLaxMonoidalFunctor x x_1 = A.mul

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :

∀ (x : CategoryTheory.Discrete PUnit.{u + 1} ), ((CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided C).obj A).obj x = A.X

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided_obj_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :

((CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided C).obj A).ε = A.one

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided_obj_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :

∀ {X Y : CategoryTheory.Discrete PUnit.{u + 1} } (x : X ⟶ Y), ((CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided C).obj A).map x = CategoryTheory.CategoryStruct.id ((fun x => A.X) X)

source

def CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.Functor (CommMon_ C) (CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C)

Implementation of CommMon_.equivLaxBraidedFunctorPunit.

Instances For

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPunit.unitIso_hom_app_toNatTrans_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) (X : CategoryTheory.Discrete PUnit.{u + 1} ) :

((CommMon_.EquivLaxBraidedFunctorPunit.unitIso C).hom.app X).app X = CategoryTheory.CategoryStruct.id (X.obj X)

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPunit.unitIso_inv_app_toNatTrans_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) (X : CategoryTheory.Discrete PUnit.{u + 1} ) :

((CommMon_.EquivLaxBraidedFunctorPunit.unitIso C).inv.app X).app X = CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete PUnit.{u + 1} )))

source

def CommMon_.EquivLaxBraidedFunctorPunit.unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.Functor.id (CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) ≅ CategoryTheory.Functor.comp (CommMon_.EquivLaxBraidedFunctorPunit.laxBraidedToCommMon C) (CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided C)

Implementation of CommMon_.equivLaxBraidedFunctorPunit.

Instances For

source

@[simp]

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

((CommMon_.EquivLaxBraidedFunctorPunit.counitIso C).hom.app X).hom = CategoryTheory.CategoryStruct.id X.X

source

@[simp]

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

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

source

def CommMon_.EquivLaxBraidedFunctorPunit.counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.Functor.comp (CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided C) (CommMon_.EquivLaxBraidedFunctorPunit.laxBraidedToCommMon C) ≅ CategoryTheory.Functor.id (CommMon_ C)

Implementation of CommMon_.equivLaxBraidedFunctorPunit.

Instances For

source

@[simp]

theorem CommMon_.equivLaxBraidedFunctorPunit_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(CommMon_.equivLaxBraidedFunctorPunit C).counitIso = CommMon_.EquivLaxBraidedFunctorPunit.counitIso C

source

@[simp]

theorem CommMon_.equivLaxBraidedFunctorPunit_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(CommMon_.equivLaxBraidedFunctorPunit C).functor = CommMon_.EquivLaxBraidedFunctorPunit.laxBraidedToCommMon C

source

@[simp]

theorem CommMon_.equivLaxBraidedFunctorPunit_inverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(CommMon_.equivLaxBraidedFunctorPunit C).inverse = CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided C

source

@[simp]

theorem CommMon_.equivLaxBraidedFunctorPunit_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(CommMon_.equivLaxBraidedFunctorPunit C).unitIso = CommMon_.EquivLaxBraidedFunctorPunit.unitIso C

source

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

CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C ≌ CommMon_ C

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

Instances For