Monoid objects internal to monoidal opposites

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

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

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

Equations

• MonObj.mopMonObj M = { one := CategoryTheory.MonObj.one.mop, mul := CategoryTheory.MonObj.mul.mop, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

@[simp]

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

@[simp]

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

instance MonObj.mop_isMonHom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.MonObj M] {N : C} [CategoryTheory.MonObj N] (f : M ⟶ N) [CategoryTheory.IsMonHom f] : CategoryTheory.IsMonHom 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 MonObj.unmopMonObj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Cᴹᵒᵖ) [CategoryTheory.MonObj M] : CategoryTheory.MonObj M.unmop

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

Equations

• MonObj.unmopMonObj M = { one := CategoryTheory.MonObj.one.unmop, mul := CategoryTheory.MonObj.mul.unmop, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

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

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

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

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

def MonObj.mopEquiv (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Mon C ≌ CategoryTheory.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 MonObj.mopEquiv_functor_obj_X_unmop (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : CategoryTheory.Mon C) : ((mopEquiv C).functor.obj M).X.unmop = M.X

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def MonObj.mopEquivCompForgetIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : (mopEquiv C).functor.comp (CategoryTheory.Mon.forget Cᴹᵒᵖ) ≅ (CategoryTheory.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

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

@[simp]

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

@[simp]

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