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

Type (max u₁ v₁)

A commutative monoid object internal to a monoidal category.

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

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

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 := ⋯ }

source

@[simp]

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

(trivial C).one = CategoryTheory.CategoryStruct.id (𝟙_ C)

source

@[simp]

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

(trivial C).X = 𝟙_ C

source

@[simp]

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

(trivial C).mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (𝟙_ C)).hom

source

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 }

source

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_

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 S 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 B : CommMon_ C} (f 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₁ A₂ 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_

source

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

(forget₂Mon_ C).FullyFaithful

The forgetful functor from commutative monoid objects to monoid objects is fully faithful.

Equations

CommMon_.fullyFaithfulForget₂Mon_ C = CategoryTheory.fullyFaithfulInducedFunctor CommMon_.toMon_

source

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

(forget₂Mon_ C).Full

source

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

(forget₂Mon_ C).Faithful

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

((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) :

((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 B : CommMon_ C} (f : A ⟶ B) :

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

source

def CommMon_.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon_ C} (f : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by aesop_cat) :

M ≅ N

Constructor for isomorphisms in the category CommMon_ C.

Equations

CommMon_.mkIso f one_f mul_f = (CommMon_.fullyFaithfulForget₂Mon_ C).preimageIso (Mon_.mkIso f one_f mul_f)

source

@[simp]

theorem CommMon_.mkIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon_ C} (f : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by aesop_cat) :

(mkIso f one_f mul_f).hom.hom = f.hom

source

@[simp]

theorem CommMon_.mkIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon_ C} (f : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by aesop_cat) :

(mkIso f one_f mul_f).inv.hom = f.inv

source

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

Unique (trivial C ⟶ A)

Equations

A.uniqueHomFromTrivial = A.uniqueHomFromTrivial

source

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

CategoryTheory.Limits.HasInitial (CommMon_ C)

source

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

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.

source

@[simp]

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

(F.mapCommMon.obj A).mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map A.mul)

source

@[simp]

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

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

source

@[simp]

theorem CategoryTheory.Functor.mapCommMon_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] {X✝ Y✝ : CommMon_ C} (f : X✝ ⟶ Y✝) :

(F.mapCommMon.map f).hom = F.map f.hom

source

@[simp]

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

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

source

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

Functor (LaxBraidedFunctor C D) (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.

source

@[simp]

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

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

source

@[simp]

theorem CategoryTheory.Functor.mapCommMonFunctor_map_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {X✝ Y✝ : LaxBraidedFunctor C D} (α : X✝ ⟶ Y✝) (A : CommMon_ C) :

(((mapCommMonFunctor C D).map α).app A).hom = α.hom.app A.X

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.

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✝) :

(laxBraidedToCommMon C).map α = ((CategoryTheory.Functor.mapCommMonFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C).map α).app (trivial (CategoryTheory.Discrete PUnit.{u + 1}))

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

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

source

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

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

Implementation of CommMon_.equivLaxBraidedFunctorPUnit.

Equations

CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj A = (CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{?u.45 + 1})).obj A.X

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) (x✝ : CategoryTheory.Discrete PUnit.{u + 1}) :

(commMonToLaxBraidedObj A).obj x✝ = A.X

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_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✝) :

(commMonToLaxBraidedObj A).map x✝ = CategoryTheory.CategoryStruct.id A.X

source

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

(commMonToLaxBraidedObj A).LaxMonoidal

Equations

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

source

@[simp]

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

CategoryTheory.Functor.LaxMonoidal.ε (commMonToLaxBraidedObj A) = A.one

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) (X Y : CategoryTheory.Discrete PUnit.{u_1 + 1}) :

CategoryTheory.Functor.LaxMonoidal.μ (commMonToLaxBraidedObj A) X Y = A.mul

source

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

(commMonToLaxBraidedObj A).LaxBraided

Equations

CommMon_.EquivLaxBraidedFunctorPUnit.instLaxBraidedDiscretePUnitCommMonToLaxBraidedObj A = CategoryTheory.Functor.LaxBraided.mk ⋯

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.

source

@[simp]

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

(commMonToLaxBraided C).obj A = CategoryTheory.LaxBraidedFunctor.of (commMonToLaxBraidedObj A)

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_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}) :

((commMonToLaxBraided C).map f).hom.app x✝ = f.hom

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

Implementation of CommMon_.equivLaxBraidedFunctorPUnit.

Equations

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

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_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}) :

((unitIso C).inv.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj (𝟙_ (CategoryTheory.Discrete PUnit.{u + 1})))

source

@[simp]

theorem CommMon_.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_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}) :

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

source

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

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

Implementation of CommMon_.equivLaxBraidedFunctorPUnit.

Equations

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

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

((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) :

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

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.

source

@[simp]

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

(equivLaxBraidedFunctorPUnit C).counitIso = EquivLaxBraidedFunctorPUnit.counitIso C

source

@[simp]

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

(equivLaxBraidedFunctorPUnit C).inverse = EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C

source

@[simp]

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

(equivLaxBraidedFunctorPUnit C).unitIso = EquivLaxBraidedFunctorPUnit.unitIso C

source

@[simp]

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

(equivLaxBraidedFunctorPUnit C).functor = EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C

Documentation

Mathlib.CategoryTheory.Monoidal.CommMon_

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