mathlib3documentation

category_theory.monoidal.opposite

Monoidal opposites #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[nolint, irreducible]

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

Equations
Instances for category_theory.monoidal_opposite

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

Equations

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

Equations
@[simp]
theorem category_theory.monoidal_opposite.op_inj_iff {C : Type u₁} (x y : C) :
@[simp]
@[simp]
@[simp]
theorem category_theory.monoidal_opposite.unmop_mop {C : Type u₁} (X : C) :
@[protected, instance]
Equations
def quiver.hom.mop {C : Type u₁} {X Y : C} (f : X Y) :

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

Equations
def quiver.hom.unmop {C : Type u₁} {X Y : Cᴹᵒᵖ} (f : X Y) :

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

Equations
theorem category_theory.mop_inj {C : Type u₁} {X Y : C} :
theorem category_theory.unmop_inj {C : Type u₁} {X Y : Cᴹᵒᵖ} :
@[simp]
theorem category_theory.unmop_mop {C : Type u₁} {X Y : C} {f : X Y} :
f.mop.unmop = f
@[simp]
theorem category_theory.mop_unmop {C : Type u₁} {X Y : Cᴹᵒᵖ} {f : X Y} :
f.unmop.mop = f
@[simp]
theorem category_theory.mop_comp {C : Type u₁} {X Y Z : C} {f : X Y} {g : Y Z} :
(f g).mop = f.mop g.mop
@[simp]
theorem category_theory.mop_id {C : Type u₁} {X : C} :
@[simp]
theorem category_theory.unmop_comp {C : Type u₁} {X Y Z : Cᴹᵒᵖ} {f : X Y} {g : Y Z} :
(f g).unmop = f.unmop g.unmop
@[simp]
theorem category_theory.unmop_id {C : Type u₁} {X : Cᴹᵒᵖ} :
@[simp]
theorem category_theory.unmop_id_mop {C : Type u₁} {X : C} :
@[simp]
theorem category_theory.mop_id_unmop {C : Type u₁} {X : Cᴹᵒᵖ} :
def category_theory.iso.mop {C : Type u₁} {X Y : C} (f : X Y) :

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

Equations
@[simp]
theorem category_theory.iso.mop_inv {C : Type u₁} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.iso.mop_hom {C : Type u₁} {X Y : C} (f : X Y) :
@[protected, instance]
Equations
theorem category_theory.op_tensor_obj {C : Type u₁} (X Y : Cᵒᵖ) :
X Y =
@[protected, instance]
Equations