Documentation

Mathlib.CategoryTheory.Monoidal.Opposite

Monoidal opposites #

We write Cᵐᵒᵖ for the monoidal opposite of a monoidal category C.

structure CategoryTheory.MonoidalOpposite (C : Type u₁) :
Type u₁

The type of objects of the opposite (or "reverse") monoidal category. Use the notation Cᴹᵒᵖ.

Instances For

    The type of objects of the opposite (or "reverse") monoidal category. Use the notation Cᴹᵒᵖ.

    Equations
    Instances For
      theorem CategoryTheory.MonoidalOpposite.mop_injective {C : Type u₁} :
      Function.Injective CategoryTheory.MonoidalOpposite.mop
      theorem CategoryTheory.MonoidalOpposite.unmop_injective {C : Type u₁} :
      Function.Injective CategoryTheory.MonoidalOpposite.unmop
      theorem CategoryTheory.MonoidalOpposite.mop_inj_iff {C : Type u₁} (x : C) (y : C) :
      { unmop := x } = { unmop := y } x = y
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.unmop_inj_iff {C : Type u₁} (x : Cᴹᵒᵖ) (y : Cᴹᵒᵖ) :
      x.unmop = y.unmop x = y
      @[simp]
      theorem CategoryTheory.MonoidalOpposite.mop_unmop {C : Type u₁} (X : Cᴹᵒᵖ) :
      { unmop := X.unmop } = X
      theorem CategoryTheory.MonoidalOpposite.unmop_mop {C : Type u₁} (X : C) :
      { unmop := X }.unmop = X
      def Quiver.Hom.mop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) :
      { unmop := X } { unmop := Y }

      The monoidal opposite of a morphism f : X ⟶ Y is just f, thought of as mop X ⟶ mop Y.

      Equations
      • f.mop = { unmop := f }
      Instances For
        def Quiver.Hom.unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} (f : X Y) :
        X.unmop Y.unmop

        We can think of a morphism f : mop X ⟶ mop Y as a morphism X ⟶ Y.

        Equations
        • f.unmop = f.unmop
        Instances For
          theorem Quiver.Hom.mop_inj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} :
          Function.Injective Quiver.Hom.mop
          @[simp]
          theorem Quiver.Hom.unmop_mop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {f : X Y} :
          f.mop.unmop = f
          @[simp]
          theorem Quiver.Hom.mop_unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} {f : X Y} :
          f.unmop.mop = f
          @[simp]
          theorem CategoryTheory.mop_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} :
          @[simp]
          theorem CategoryTheory.mopFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (unmop : C) :
          (CategoryTheory.mopFunctor C).obj unmop = { unmop := unmop }
          @[simp]
          theorem CategoryTheory.mopFunctor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
          ∀ {X Y : C} (f : X Y), (CategoryTheory.mopFunctor C).map f = f.mop

          The identity functor on C, viewed as a functor from C to its monoidal opposite.

          Equations
          • CategoryTheory.mopFunctor C = { obj := CategoryTheory.MonoidalOpposite.mop, map := fun {X Y : C} => Quiver.Hom.mop, map_id := , map_comp := }
          Instances For
            @[simp]

            The identity functor on C, viewed as a functor from the monoidal opposite of C to C.

            Equations
            Instances For
              @[reducible, inline]
              abbrev CategoryTheory.Iso.mop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) :
              { unmop := X } { unmop := Y }

              An isomorphism in C gives an isomorphism in Cᴹᵒᵖ.

              Equations
              Instances For
                @[reducible, inline]
                abbrev CategoryTheory.Iso.unmop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᴹᵒᵖ} {Y : Cᴹᵒᵖ} (f : X Y) :
                X.unmop Y.unmop

                An isomorphism in Cᴹᵒᵖ gives an isomorphism in C.

                Equations
                Instances For
                  @[simp]
                  theorem CategoryTheory.op_tensorHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ Y₁) (g : X₂ Y₂) :
                  @[simp]
                  theorem CategoryTheory.mop_tensorHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : C} {Y₁ : C} {X₂ : C} {Y₂ : C} (f : X₁ Y₁) (g : X₂ Y₂) :
                  @[simp]
                  @[simp]
                  @[simp]

                  The (identity) equivalence between C and its monoidal opposite.

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