Documentation

TauCeti.CategoryTheory.Monoidal.Opposite

Opposites and monoidal opposites of monoidal functors #

A functor F : C ⥤ D induces a functor between the monoidal opposites by applying F to the underlying objects and morphisms. If F is lax, oplax, or strong monoidal, so is this induced functor: its tensor comparison is the monoidal opposite of the comparison of F, with the two inputs reversed.

The opposite functor F.op : Cᵒᵖ ⥤ Dᵒᵖ exchanges the two kinds of structure: since morphisms are reversed in Cᵒᵖ and Dᵒᵖ, the opposite of an oplax monoidal functor is lax monoidal and the opposite of a lax monoidal functor is oplax monoidal, with comparison morphisms the opposites of those of F. A strong monoidal functor has a strong monoidal opposite.

These constructions let a monoidal functor whose codomain is (Dᵒᵖ)ᴹᵒᵖ, such as the right dual functor of a rigid monoidal category, be applied twice: its opposite monoidal opposite lands in ((Dᵒᵖ)ᴹᵒᵖ)ᵒᵖᴹᵒᵖ, which is identified with D as a monoidal category by MonoidalOpposite.opMopOpMopEquivalence, since the two reversals of the tensor product cancel.

Main declarations #

source
def CategoryTheory.Functor.opMop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
Functor Cᴹᵒᵖ Dᴹᵒᵖ

A functor between monoidal categories, applied to the underlying objects and morphisms of their monoidal opposites.

Instances For
    source
    @[simp]
    theorem CategoryTheory.Functor.opMop_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : Cᴹᵒᵖ) :
    F.opMop.obj X = { unmop := F.obj X.unmop }

    The monoidal opposite of a functor applies the original functor to the underlying object.

    source
    @[simp]
    theorem CategoryTheory.Functor.opMop_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : Cᴹᵒᵖ} (f : X ⟶ Y) :
    F.opMop.map f = (F.map f.unmop).mop

    The monoidal opposite of a functor applies the original functor to the underlying morphism.

    source
    @[instance_reducible]
    instance CategoryTheory.Functor.opMopLaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] :
    F.opMop.LaxMonoidal

    Taking monoidal opposites preserves lax monoidal functors.

    source
    @[instance_reducible]
    instance CategoryTheory.Functor.opMopOplaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] :
    F.opMop.OplaxMonoidal

    Taking monoidal opposites preserves oplax monoidal functors.

    source
    @[instance_reducible]
    instance CategoryTheory.Functor.opMopMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] :
    F.opMop.Monoidal

    Taking monoidal opposites preserves strong monoidal functors.

    source
    instance CategoryTheory.Functor.isEquivalence_opMop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.IsEquivalence] :
    F.opMop.IsEquivalence

    The monoidal opposite of an equivalence of categories is an equivalence of categories.

    source
    @[simp]
    theorem CategoryTheory.Functor.opMop_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] :
    LaxMonoidal.ε F.opMop = (LaxMonoidal.ε F).mop

    The unit comparison of the monoidal opposite of a lax monoidal functor.

    source
    @[simp]
    theorem CategoryTheory.Functor.opMop_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y : Cᴹᵒᵖ) :
    LaxMonoidal.μ F.opMop X Y = (LaxMonoidal.μ F Y.unmop X.unmop).mop

    The tensor comparison of the monoidal opposite of a lax monoidal functor.

    source
    @[simp]
    theorem CategoryTheory.Functor.opMop_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] :
    OplaxMonoidal.η F.opMop = (OplaxMonoidal.η F).mop

    The counit comparison of the monoidal opposite of an oplax monoidal functor.

    source
    @[simp]
    theorem CategoryTheory.Functor.opMop_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y : Cᴹᵒᵖ) :
    OplaxMonoidal.δ F.opMop X Y = (OplaxMonoidal.δ F Y.unmop X.unmop).mop

    The cotensor comparison of the monoidal opposite of an oplax monoidal functor.

    source
    @[instance_reducible]
    instance CategoryTheory.Functor.opLaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] :
    F.op.LaxMonoidal

    The opposite of an oplax monoidal functor is lax monoidal.

    source
    @[instance_reducible]
    instance CategoryTheory.Functor.opOplaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] :
    F.op.OplaxMonoidal

    The opposite of a lax monoidal functor is oplax monoidal.

    source
    @[instance_reducible]
    instance CategoryTheory.Functor.opMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] :
    F.op.Monoidal

    The opposite of a strong monoidal functor is strong monoidal.

    source
    @[simp]
    theorem CategoryTheory.Functor.op_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] :
    LaxMonoidal.ε F.op = (OplaxMonoidal.η F).op

    The unit comparison of the opposite of an oplax monoidal functor.

    source
    @[simp]
    theorem CategoryTheory.Functor.op_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y : Cᵒᵖ) :
    LaxMonoidal.μ F.op X Y = (OplaxMonoidal.δ F (Opposite.unop X) (Opposite.unop Y)).op

    The tensor comparison of the opposite of an oplax monoidal functor.

    source
    @[simp]
    theorem CategoryTheory.Functor.op_η {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] :
    OplaxMonoidal.η F.op = (LaxMonoidal.ε F).op

    The counit comparison of the opposite of a lax monoidal functor.

    source
    @[simp]
    theorem CategoryTheory.Functor.op_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (X Y : Cᵒᵖ) :
    OplaxMonoidal.δ F.op X Y = (LaxMonoidal.μ F (Opposite.unop X) (Opposite.unop Y)).op

    The cotensor comparison of the opposite of a lax monoidal functor.

    source
    def CategoryTheory.MonoidalOpposite.opMopOpMopEquivalence (C : Type u) [Category.{v, u} C] :
    Cᵒᵖᴹᵒᵖᵒᵖᴹᵒᵖ ≌ C

    The equivalence between ((Cᵒᵖ)ᴹᵒᵖ)ᵒᵖᴹᵒᵖ and C, removing the four wrappers.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.opMopOpMopEquivalence_functor_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : Cᵒᵖᴹᵒᵖᵒᵖᴹᵒᵖ} (f : X✝ ⟶ Y✝) :
      (opMopOpMopEquivalence C).functor.map f = f.unmop.unop.unmop.unop
      source
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.opMopOpMopEquivalence_unitIso (C : Type u) [Category.{v, u} C] :
      (opMopOpMopEquivalence C).unitIso = Iso.refl (Functor.id Cᵒᵖᴹᵒᵖᵒᵖᴹᵒᵖ)
      source
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.opMopOpMopEquivalence_functor_obj (C : Type u) [Category.{v, u} C] (X : Cᵒᵖᴹᵒᵖᵒᵖᴹᵒᵖ) :
      (opMopOpMopEquivalence C).functor.obj X = Opposite.unop (Opposite.unop X.unmop).unmop
      source
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.opMopOpMopEquivalence_inverse_obj_unmop (C : Type u) [Category.{v, u} C] (X : C) :
      ((opMopOpMopEquivalence C).inverse.obj X).unmop = Opposite.op { unmop := Opposite.op X }
      source
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.opMopOpMopEquivalence_inverse_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
      (opMopOpMopEquivalence C).inverse.map f = f.op.mop.op.mop
      source
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.opMopOpMopEquivalence_counitIso (C : Type u) [Category.{v, u} C] :
      (opMopOpMopEquivalence C).counitIso = Iso.refl ({ obj := fun (X : C) => { unmop := Opposite.op { unmop := Opposite.op X } }, map := fun {X Y : C} (f : X ⟶ Y) => f.op.mop.op.mop, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (X : Cᵒᵖᴹᵒᵖᵒᵖᴹᵒᵖ) => Opposite.unop (Opposite.unop X.unmop).unmop, map := fun {X Y : Cᵒᵖᴹᵒᵖᵒᵖᴹᵒᵖ} (f : X ⟶ Y) => f.unmop.unop.unmop.unop, map_id := ⋯, map_comp := ⋯ })
      source
      @[instance_reducible]
      instance CategoryTheory.MonoidalOpposite.opMopOpMopEquivalenceFunctorMonoidal (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :
      (opMopOpMopEquivalence C).functor.Monoidal

      Removing the four wrappers from ((Cᵒᵖ)ᴹᵒᵖ)ᵒᵖᴹᵒᵖ is strong monoidal with identity comparison morphisms: the tensor product is reversed twice.

      source
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.opMopOpMopEquivalence_functor_ε (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :
      Functor.LaxMonoidal.ε (opMopOpMopEquivalence C).functor = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

      The unit comparison of the removal of the four wrappers is the identity.

      source
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.opMopOpMopEquivalence_functor_μ (C : Type u) [Category.{v, u} C] [MonoidalCategory C] (X Y : Cᵒᵖᴹᵒᵖᵒᵖᴹᵒᵖ) :
      Functor.LaxMonoidal.μ (opMopOpMopEquivalence C).functor X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((opMopOpMopEquivalence C).functor.obj X) ((opMopOpMopEquivalence C).functor.obj Y))

      The tensor comparison of the removal of the four wrappers is the identity.

      source
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.opMopOpMopEquivalence_functor_η (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :
      Functor.OplaxMonoidal.η (opMopOpMopEquivalence C).functor = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

      The counit comparison of the removal of the four wrappers is the identity.

      source
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.opMopOpMopEquivalence_functor_δ (C : Type u) [Category.{v, u} C] [MonoidalCategory C] (X Y : Cᵒᵖᴹᵒᵖᵒᵖᴹᵒᵖ) :
      Functor.OplaxMonoidal.δ (opMopOpMopEquivalence C).functor X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((opMopOpMopEquivalence C).functor.obj X) ((opMopOpMopEquivalence C).functor.obj Y))

      The cotensor comparison of the removal of the four wrappers is the identity.