Documentation

Mathlib.CategoryTheory.Monoidal.Opposite.Mon_

Monoid objects internal to monoidal opposites #

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

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

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

Equations
source
@[simp]
theorem MonObj.mopMonObj_one_unmop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : C) [MonObj M] :
one.unmop = one
source
@[simp]
theorem MonObj.mopMonObj_mul_unmop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : C) [MonObj M] :
mul.unmop = mul
source
instance MonObj.mop_isMon_Hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {M : C} [MonObj M] {N : C} [MonObj 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ᴹᵒᵖ.

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

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

Equations
source
theorem MonObj.unmopMonObj_mul {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Cᴹᵒᵖ) [MonObj M] :
mul = mul.unmop
source
theorem MonObj.unmopMonObj_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (M : Cᴹᵒᵖ) [MonObj M] :
one = one.unmop
source
instance MonObj.unmop_isMon_Hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {M : Cᴹᵒᵖ} [MonObj M] {N : Cᴹᵒᵖ} [MonObj 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.

source
def MonObj.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.
Instances For
    source
    @[simp]
    theorem MonObj.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
    source
    @[simp]
    theorem MonObj.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
    source
    @[simp]
    theorem MonObj.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
    source
    @[simp]
    theorem MonObj.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
    source
    @[simp]
    theorem MonObj.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
    source
    @[simp]
    theorem MonObj.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
    source
    @[simp]
    theorem MonObj.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
    source
    @[simp]
    theorem MonObj.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
    source
    @[simp]
    theorem MonObj.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
    source
    @[simp]
    theorem MonObj.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
    source
    @[simp]
    theorem MonObj.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
    source
    @[simp]
    theorem MonObj.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
    source
    def MonObj.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
    Instances For
      source
      @[simp]
      theorem MonObj.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
      source
      @[simp]
      theorem MonObj.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