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₁)

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

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).one = CategoryTheory.CategoryStruct.id (𝟙_ C)

source

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

source

@[simp]

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

(CommMon_.trivial C).X = 𝟙_ 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.

Equations

CommMon_.trivial C = let __src := Mon_.trivial C; { toMon_ := __src, mul_comm := ⋯ }

Instances For

source

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

Inhabited (CommMon_ C)

Equations

CommMon_.instInhabitedCommMon_ C = { default := CommMon_.trivial 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)

Equations

CommMon_.instCategoryCommMon_ = CategoryTheory.InducedCategory.category CommMon_.toMon_

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.

Equations

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

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.Functor.Full (CommMon_.forget₂Mon_ C)

Equations

⋯ = ⋯

source

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

CategoryTheory.Functor.Faithful (CommMon_.forget₂Mon_ C)

Equations

⋯ = ⋯

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)

Equations

CommMon_.uniqueHomFromTrivial A = Mon_.uniqueHomFromTrivial A.toMon_

source

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

CategoryTheory.Limits.HasInitial (CommMon_ C)

Equations

⋯ = ⋯

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_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_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 (F.μ 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.

Equations

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

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.

Equations

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

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.

Equations

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

Instances For

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_μ (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

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

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

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.

Instances For

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

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

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.

Equations

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

Instances For

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

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

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.

Equations

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

Instances For

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_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_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_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.

Equations

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

Instances For

Documentation

Mathlib.CategoryTheory.Monoidal.CommMon_

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