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

Type (max u₁ v₁)

A commutative monoid object internal to a monoidal category.

X : C
The underlying object in the ambient monoidal category
mon : Mon_Class self.X
comm : IsCommMon self.X

Instances For

source

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

Mon_ C

A commutative monoid object is a monoid object.

Equations

A.toMon_ = { X := A.X, mon := A.mon }

Instances For

source

@[simp]

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

A.toMon_.X = A.X

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 = { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, mon := Mon_Class.instTensorUnit, comm := ⋯ }

Instances For

source

@[simp]

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

Mon_Class.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

source

@[simp]

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

(trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C

source

@[simp]

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

Mon_Class.mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit 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 = { 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

theorem CommMon_.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommMon_ C} {f g : A ⟶ B} :

f = g ↔ f.hom = g.hom

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_

Instances For

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_

Instances For

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

Mon_Class.one = Mon_Class.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) :

Mon_Class.mul = Mon_Class.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

@[deprecated CommMon_.forget₂Mon_obj_one (since := "2025-02-07")]

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

Mon_Class.one = Mon_Class.one

Alias of CommMon_.forget₂Mon_obj_one.

source

@[deprecated CommMon_.forget₂Mon_obj_mul (since := "2025-02-07")]

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

Mon_Class.mul = Mon_Class.mul

Alias of CommMon_.forget₂Mon_obj_mul.

source

@[deprecated CommMon_.forget₂Mon_map_hom (since := "2025-02-07")]

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

Alias of CommMon_.forget₂Mon_map_hom.

source

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

CategoryTheory.Functor (CommMon_ C) C

The forgetful functor from commutative monoid objects to the ambient category.

Equations

CommMon_.forget C = (CommMon_.forget₂Mon_ C).comp (Mon_.forget C)

Instances For

source

@[simp]

theorem CommMon_.forget_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : CommMon_ C} (f : X✝ ⟶ Y✝) :

(forget C).map f = f.hom

source

@[simp]

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

(forget C).obj X = ((forget₂Mon_ C).obj X).X

source

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

(forget C).Faithful

source

@[simp]

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

(forget₂Mon_ C).comp (Mon_.forget C) = forget C

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 Mon_Class.one f.hom = Mon_Class.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp Mon_Class.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) Mon_Class.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)

Instances For

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 Mon_Class.one f.hom = Mon_Class.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp Mon_Class.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) Mon_Class.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 Mon_Class.one f.hom = Mon_Class.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp Mon_Class.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) Mon_Class.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.toMon_.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.

Instances For

source

@[simp]

theorem CategoryTheory.Functor.mapCommMon_obj_mon_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) :

Mon_Class.one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map Mon_Class.one)

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

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

source

@[simp]

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

Mon_Class.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) Mon_Class.one

source

@[simp]

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

Mon_Class.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj A.X A.X)) Mon_Class.mul

source

@[simp]

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

Mon_Class.one = CategoryStruct.comp (LaxMonoidal.ε (F.comp G)) ((F.comp G).map Mon_Class.one)

source

@[simp]

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

Mon_Class.mul = CategoryStruct.comp (LaxMonoidal.μ (F.comp G) A.X A.X) ((F.comp G).map Mon_Class.mul)

source

noncomputable def CategoryTheory.Functor.mapCommMonIdIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :

(Functor.id C).mapCommMon ≅ Functor.id (CommMon_ C)

The identity functor is also the identity on commutative monoid objects.

Equations

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

Instances For

source

@[simp]

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

(mapCommMonIdIso.inv.app X).hom = CategoryStruct.id X.X

source

@[simp]

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

(mapCommMonIdIso.hom.app X).hom = CategoryStruct.id X.X

source

noncomputable def CategoryTheory.Functor.mapCommMonCompIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.LaxBraided] {G : Functor D E} [G.LaxBraided] :

(F.comp G).mapCommMon ≅ F.mapCommMon.comp G.mapCommMon

The composition functor is also the composition on commutative monoid objects.

Equations

CategoryTheory.Functor.mapCommMonCompIso = CategoryTheory.NatIso.ofComponents (fun (X : CommMon_ C) => CommMon_.mkIso (CategoryTheory.Iso.refl ((F.comp G).mapCommMon.obj X).X) ⋯ ⋯) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Functor.mapCommMonCompIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.LaxBraided] {G : Functor D E} [G.LaxBraided] (X : CommMon_ C) :

(mapCommMonCompIso.hom.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

source

@[simp]

theorem CategoryTheory.Functor.mapCommMonCompIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.LaxBraided] {G : Functor D E} [G.LaxBraided] (X : CommMon_ C) :

(mapCommMonCompIso.inv.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

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.

Instances For

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

noncomputable def CategoryTheory.Functor.mapCommMonNatTrans {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (f : F ⟶ F') [NatTrans.IsMonoidal f] :

F.mapCommMon ⟶ F'.mapCommMon

Natural transformations between functors lift to monoid objects.

Equations

CategoryTheory.Functor.mapCommMonNatTrans f = { app := fun (X : CommMon_ C) => { hom := f.app X.toMon_.X, one_hom := ⋯, mul_hom := ⋯ }, naturality := ⋯ }

Instances For

source

@[simp]

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

((mapCommMonNatTrans f).app X).hom = f.app X.X

source

noncomputable def CategoryTheory.Functor.mapCommMonNatIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] :

F.mapCommMon ≅ F'.mapCommMon

Natural isomorphisms between functors lift to monoid objects.

Equations

CategoryTheory.Functor.mapCommMonNatIso e = CategoryTheory.NatIso.ofComponents (fun (X : CommMon_ C) => CommMon_.mkIso (e.app X.toMon_.X) ⋯ ⋯) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Functor.mapCommMonNatIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] (X : CommMon_ C) :

((mapCommMonNatIso e).inv.app X).hom = e.inv.app X.X

source

@[simp]

theorem CategoryTheory.Functor.mapCommMonNatIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] (X : CommMon_ C) :

((mapCommMonNatIso e).hom.app X).hom = e.hom.app X.X

source

noncomputable def CategoryTheory.Adjunction.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} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.LaxBraided] [a.IsMonoidal] :

F.mapCommMon ⊣ G.mapCommMon

An adjunction of braided functors lifts to an adjunction of their lifts to commutative monoid objects.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Adjunction.mapCommMon_unit {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} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.LaxBraided] [a.IsMonoidal] :

a.mapCommMon.unit = CategoryStruct.comp Functor.mapCommMonIdIso.inv (CategoryStruct.comp (Functor.mapCommMonNatTrans a.unit) Functor.mapCommMonCompIso.hom)

source

@[simp]

theorem CategoryTheory.Adjunction.mapCommMon_counit {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} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.LaxBraided] [a.IsMonoidal] :

a.mapCommMon.counit = CategoryStruct.comp Functor.mapCommMonCompIso.inv (CategoryStruct.comp (Functor.mapCommMonNatTrans a.counit) Functor.mapCommMonIdIso.hom)

source

noncomputable def CategoryTheory.Equivalence.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :

CommMon_ C ≌ CommMon_ D

An equivalence of categories lifts to an equivalence of their commutative monoid objects.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Equivalence.mapCommMon_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :

e.mapCommMon.functor = e.functor.mapCommMon

source

@[simp]

theorem CategoryTheory.Equivalence.mapCommMon_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :

e.mapCommMon.unitIso = Functor.mapCommMonIdIso.symm ≪≫ Functor.mapCommMonNatIso e.unitIso ≪≫ Functor.mapCommMonCompIso

source

@[simp]

theorem CategoryTheory.Equivalence.mapCommMon_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :

e.mapCommMon.inverse = e.inverse.mapCommMon

source

@[simp]

theorem CategoryTheory.Equivalence.mapCommMon_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :

e.mapCommMon.counitIso = Functor.mapCommMonCompIso.symm ≪≫ Functor.mapCommMonNatIso e.counitIso ≪≫ Functor.mapCommMonIdIso

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

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

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.32 + 1})).obj A.X

Instances For

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

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

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) = Mon_Class.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 = Mon_Class.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

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

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

Instances For

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

@[simp]

source

@[simp]

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

Mon_Class.one = CategoryTheory.CategoryStruct.comp Mon_Class.one (CategoryTheory.CategoryStruct.id A.X)

source

@[simp]

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

Mon_Class.mul = CategoryTheory.CategoryStruct.comp Mon_Class.mul (CategoryTheory.CategoryStruct.id A.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.

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

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

((counitIso C).inv.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.

Instances For

source

@[simp]

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

equivLaxBraidedFunctorPUnit.counitIso = EquivLaxBraidedFunctorPUnit.counitIso C

source

@[simp]

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

equivLaxBraidedFunctorPUnit.functor = EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C

source

@[simp]

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

equivLaxBraidedFunctorPUnit.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.unitIso = EquivLaxBraidedFunctorPUnit.unitIso C

Documentation

Mathlib.CategoryTheory.Monoidal.CommMon_

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