Monoid objects internal to monoidal opposites

In this file, we record the equivalence between Mon_ C and Mon Cᴹᵒᵖ.

instance Mon_Class.mopMon_Class {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : C) [Mon_Class M] : Mon_Class { unmop := M }

If M : C is a monoid object, then mop M : Cᴹᵒᵖ too.

Equations

• Mon_Class.mopMon_Class M = { one := Mon_Class.one.mop, mul := Mon_Class.mul.mop, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

@[simp]

theorem Mon_Class.mopMon_Class_one_unmop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : C) [Mon_Class M] : one.unmop = one

@[simp]

theorem Mon_Class.mopMon_Class_mul_unmop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : C) [Mon_Class M] : mul.unmop = mul

instance Mon_Class.mop_isMon_Hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {M : C} [Mon_Class M] {N : C} [Mon_Class N] (f : M ⟶ N) [IsMon_Hom f] : IsMon_Hom f.mop

If f is a morphism of monoid objects internal to C, then f.mop is a morphism of monoid objects internal to Cᴹᵒᵖ.

instance Mon_Class.unmopMon_Class {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Cᴹᵒᵖ) [Mon_Class M] : Mon_Class M.unmop

If M : Cᴹᵒᵖ is a monoid object, then unmop M : C too.

Equations

• Mon_Class.unmopMon_Class M = { one := Mon_Class.one.unmop, mul := Mon_Class.mul.unmop, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

theorem Mon_Class.unmopMon_Class_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Cᴹᵒᵖ) [Mon_Class M] : one = one.unmop

theorem Mon_Class.unmopMon_Class_mul {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Cᴹᵒᵖ) [Mon_Class M] : mul = mul.unmop

instance Mon_Class.unmop_isMon_Hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {M : Cᴹᵒᵖ} [Mon_Class M] {N : Cᴹᵒᵖ} [Mon_Class N] (f : M ⟶ N) [IsMon_Hom f] : IsMon_Hom f.unmop

If f is a morphism of monoid objects internal to Cᴹᵒᵖ, so is f.unmop.

def Mon_Class.mopEquiv (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : Mon_ C ≌ Mon_ Cᴹᵒᵖ

The equivalence of categories between monoids internal to C and monoids internal to the monoidal opposite of C.

Equations

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

@[simp]

theorem Mon_Class.mopEquiv_functor_obj_mon_one_unmop (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ C) : one.unmop = one

@[simp]

theorem Mon_Class.mopEquiv_unitIso_hom_app_hom (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : Mon_ C) : ((mopEquiv C).unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.X

@[simp]

theorem Mon_Class.mopEquiv_inverse_obj_X (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ Cᴹᵒᵖ) : ((mopEquiv C).inverse.obj M).X = M.X.unmop

@[simp]

theorem Mon_Class.mopEquiv_inverse_obj_mon_mul (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ Cᴹᵒᵖ) : mul = mul.unmop

@[simp]

theorem Mon_Class.mopEquiv_functor_obj_X_unmop (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ C) : ((mopEquiv C).functor.obj M).X.unmop = M.X

@[simp]

theorem Mon_Class.mopEquiv_counitIso_hom_app_hom_unmop (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : Mon_ Cᴹᵒᵖ) : ((mopEquiv C).counitIso.hom.app X).hom.unmop = CategoryTheory.CategoryStruct.id X.X.unmop

@[simp]

theorem Mon_Class.mopEquiv_inverse_obj_mon_one (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ Cᴹᵒᵖ) : one = one.unmop

@[simp]

theorem Mon_Class.mopEquiv_unitIso_inv_app_hom (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : Mon_ C) : ((mopEquiv C).unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.X

@[simp]

theorem Mon_Class.mopEquiv_inverse_map_hom (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : Mon_ Cᴹᵒᵖ} (f : X✝ ⟶ Y✝) : ((mopEquiv C).inverse.map f).hom = f.hom.unmop

@[simp]

theorem Mon_Class.mopEquiv_functor_obj_mon_mul_unmop (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ C) : mul.unmop = mul

@[simp]

theorem Mon_Class.mopEquiv_counitIso_inv_app_hom_unmop (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : Mon_ Cᴹᵒᵖ) : ((mopEquiv C).counitIso.inv.app X).hom.unmop = CategoryTheory.CategoryStruct.id X.X.unmop

@[simp]

theorem Mon_Class.mopEquiv_functor_map_hom_unmop (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X✝ Y✝ : Mon_ C} (f : X✝ ⟶ Y✝) : ((mopEquiv C).functor.map f).hom.unmop = f.hom

def Mon_Class.mopEquivCompForgetIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : (mopEquiv C).functor.comp (Mon_.forget Cᴹᵒᵖ) ≅ (Mon_.forget C).comp (CategoryTheory.MonoidalOpposite.mopEquiv C).functor

The equivalence of categories between monoids internal to C and monoids internal to the monoidal opposite of C lies over the equivalence C ≌ Cᴹᵒᵖ via the forgetful functors.

Equations

• Mon_Class.mopEquivCompForgetIso = CategoryTheory.Iso.refl ((Mon_Class.mopEquiv C).functor.comp (Mon_.forget Cᴹᵒᵖ))

@[simp]

theorem Mon_Class.mopEquivCompForgetIso_hom_app_unmop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : Mon_ C) : (mopEquivCompForgetIso.hom.app X).unmop = CategoryTheory.CategoryStruct.id X.X

@[simp]

theorem Mon_Class.mopEquivCompForgetIso_inv_app_unmop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : Mon_ C) : (mopEquivCompForgetIso.inv.app X).unmop = CategoryTheory.CategoryStruct.id X.X