The category of commutative monoids in a braided monoidal category.

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

A commutative monoid object internal to a monoidal category.

• X : C
• one : 𝟙_ C ⟶ self.X
• mul : CategoryTheory.MonoidalCategory.tensorObj self.X self.X ⟶ self.X
• one_mul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.one self.X) self.mul = (CategoryTheory.MonoidalCategory.leftUnitor self.X).hom
• mul_one : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft self.X self.one) self.mul = (CategoryTheory.MonoidalCategory.rightUnitor self.X).hom
• mul_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.mul self.X) self.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator self.X self.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft self.X self.mul) self.mul)
• mul_comm : CategoryTheory.CategoryStruct.comp (β_ self.X self.X).hom self.mul = self.mul

@[simp]

theorem CommMon_.mul_comm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (self : CommMon_ C) : CategoryTheory.CategoryStruct.comp (β_ self.X self.X).hom self.mul = self.mul

@[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

@[simp]

theorem CommMon_.trivial_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CommMon_.trivial C).one = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem CommMon_.trivial_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CommMon_.trivial C).mul = (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom

@[simp]

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

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.

Equations

• CommMon_.trivial C = { toMon_ := Mon_.trivial C, mul_comm := ⋯ }

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

Equations

• CommMon_.instInhabited C = { default := CommMon_.trivial C }

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

Equations

• CommMon_.instCategory = CategoryTheory.InducedCategory.category CommMon_.toMon_

@[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

@[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

theorem CommMon_.hom_ext_iff {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} : f = g ↔ f.hom = g.hom

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

@[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_

@[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

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.

Equations

• CommMon_.forget₂Mon_ C = CategoryTheory.inducedFunctor CommMon_.toMon_

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[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

@[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

@[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

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)

Equations

• A.uniqueHomFromTrivial = A.uniqueHomFromTrivial

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

Equations

• ⋯ = ⋯

@[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) : (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₁} [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) : (F.mapCommMon.obj A).X = F.obj A.X

@[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) : (F.mapCommMon.obj A).one = CategoryTheory.CategoryStruct.comp F.ε (F.map A.one)

@[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), (F.mapCommMon.map f).hom = F.map f.hom

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.

Equations

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

@[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 = F.mapCommMon

@[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

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.

Equations

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

@[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 = F.mapCommMon.obj (CommMon_.trivial (CategoryTheory.Discrete PUnit.{u + 1} ))

@[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} ))

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.

Equations

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

@[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

@[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

@[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

@[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} ), ((CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C).obj A).μ x x_1 = A.mul

@[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 : CategoryTheory.Discrete PUnit.{u + 1} ) => A.X) X)

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.

Equations

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

@[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.Discrete PUnit.{u + 1} )))

@[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)

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) ≅ (CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C).comp (CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C)

Implementation of CommMon_.equivLaxBraidedFunctorPUnit.

Equations

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

@[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

@[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

def CommMon_.EquivLaxBraidedFunctorPUnit.counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C).comp (CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C) ≅ CategoryTheory.Functor.id (CommMon_ C)

Implementation of CommMon_.equivLaxBraidedFunctorPUnit.

Equations

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

@[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

@[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

@[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

@[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

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.

Equations

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