Documentation

Mathlib.CategoryTheory.Monoidal.Opposite

Monoidal opposites #

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

A type synonym for the monoidal opposite. Use the notation Cᴹᵒᵖ.

Instances For

    Think of an object of C as an object of Cᴹᵒᵖ.

    Instances For

      Think of an object of Cᴹᵒᵖ as an object of C.

      Instances For
        theorem CategoryTheory.MonoidalOpposite.op_injective {C : Type u₁} :
        Function.Injective CategoryTheory.MonoidalOpposite.mop
        theorem CategoryTheory.MonoidalOpposite.unop_injective {C : Type u₁} :
        Function.Injective CategoryTheory.MonoidalOpposite.unmop

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

        Instances For

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

          Instances For
            theorem CategoryTheory.mop_inj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} :
            Function.Injective Quiver.Hom.mop
            @[simp]
            @[simp]
            @[simp]

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

            Instances For