# mathlibdocumentation

category_theory.opposites

@[instance]
def category_theory.has_hom.opposite {C : Type u₁}  :

The hom types of the opposite of a category (or graph).

As with the objects, we'll make this irreducible below. Use f.op and f.unop to convert between morphisms of C and morphisms of Cᵒᵖ.

Equations
def category_theory.has_hom.hom.op {C : Type u₁} {X Y : C} (f : X Y) :

The opposite of a morphism in C.

Equations
def category_theory.has_hom.hom.unop {C : Type u₁} {X Y : Cᵒᵖ} (f : X Y) :

Given a morphism in Cᵒᵖ, we can take the "unopposite" back in C.

Equations
theorem category_theory.has_hom.hom.op_inj {C : Type u₁} {X Y : C} :
theorem category_theory.has_hom.hom.unop_inj {C : Type u₁} {X Y : Cᵒᵖ} :
@[simp]
theorem category_theory.has_hom.hom.unop_op {C : Type u₁} {X Y : C} {f : X Y} :
f.op.unop = f
@[simp]
theorem category_theory.has_hom.hom.op_unop {C : Type u₁} {X Y : Cᵒᵖ} {f : X Y} :
f.unop.op = f
@[instance]
def category_theory.category.opposite {C : Type u₁}  :

The opposite category.

Equations
@[simp]
theorem category_theory.op_comp {C : Type u₁} {X Y Z : C} {f : X Y} {g : Y Z} :
(f g).op = g.op f.op
@[simp]
theorem category_theory.op_id {C : Type u₁} {X : C} :
@[simp]
theorem category_theory.unop_comp {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Y} {g : Y Z} :
(f g).unop = g.unop f.unop
@[simp]
theorem category_theory.unop_id {C : Type u₁} {X : Cᵒᵖ} :
@[simp]
theorem category_theory.unop_id_op {C : Type u₁} {X : C} :
@[simp]
theorem category_theory.op_id_unop {C : Type u₁} {X : Cᵒᵖ} :
def category_theory.op_op (C : Type u₁)  :

The functor from the double-opposite of a category to the underlying category.

Equations
@[simp]
theorem category_theory.op_op_obj (C : Type u₁) (X : Cᵒᵖᵒᵖ) :
@[simp]
theorem category_theory.op_op_map (C : Type u₁) (X Y : Cᵒᵖᵒᵖ) (f : X Y) :
f = f.unop.unop
@[simp]
theorem category_theory.unop_unop_obj (C : Type u₁) (X : C) :
@[simp]
theorem category_theory.unop_unop_map (C : Type u₁) (X Y : C) (f : X Y) :
= f.op.op
def category_theory.unop_unop (C : Type u₁)  :

The functor from a category to its double-opposite.

Equations
@[simp]
@[simp]
theorem category_theory.op_op_equivalence_functor (C : Type u₁)  :

The double opposite category is equivalent to the original.

Equations
@[simp]
theorem category_theory.op_op_equivalence_inverse (C : Type u₁)  :
@[simp]
theorem category_theory.op_op_equivalence_unit_iso (C : Type u₁)  :
theorem category_theory.is_iso_of_op {C : Type u₁} {X Y : C} (f : X Y)  :

If f.op is an isomorphism f must be too. (This cannot be an instance as it would immediately loop!)

@[simp]
theorem category_theory.functor.op_map {C : Type u₁} {D : Type u₂} (F : C D) (X Y : Cᵒᵖ) (f : X Y) :
F.op.map f = (F.map f.unop).op
def category_theory.functor.op {C : Type u₁} {D : Type u₂} (F : C D) :

The opposite of a functor, i.e. considering a functor F : C ⥤ D as a functor Cᵒᵖ ⥤ Dᵒᵖ. In informal mathematics no distinction is made between these.

Equations
@[simp]
theorem category_theory.functor.op_obj {C : Type u₁} {D : Type u₂} (F : C D) (X : Cᵒᵖ) :
def category_theory.functor.unop {C : Type u₁} {D : Type u₂} (F : Cᵒᵖ Dᵒᵖ) :
C D

Given a functor F : Cᵒᵖ ⥤ Dᵒᵖ we can take the "unopposite" functor F : C ⥤ D. In informal mathematics no distinction is made between these.

Equations
@[simp]
theorem category_theory.functor.unop_map {C : Type u₁} {D : Type u₂} (F : Cᵒᵖ Dᵒᵖ) (X Y : C) (f : X Y) :
F.unop.map f = (F.map f.op).unop
@[simp]
theorem category_theory.functor.unop_obj {C : Type u₁} {D : Type u₂} (F : Cᵒᵖ Dᵒᵖ) (X : C) :
def category_theory.functor.op_unop_iso {C : Type u₁} {D : Type u₂} (F : C D) :
F.op.unop F

The isomorphism between F.op.unop and F.

Equations
def category_theory.functor.unop_op_iso {C : Type u₁} {D : Type u₂} (F : Cᵒᵖ Dᵒᵖ) :
F.unop.op F

The isomorphism between F.unop.op and F.

Equations
def category_theory.functor.op_hom (C : Type u₁) (D : Type u₂)  :

Taking the opposite of a functor is functorial.

Equations
@[simp]
theorem category_theory.functor.op_hom_map_app (C : Type u₁) (D : Type u₂) (F G : (C D)ᵒᵖ) (α : F G) (X : Cᵒᵖ) :
α).app X = (α.unop.app (opposite.unop X)).op
@[simp]
theorem category_theory.functor.op_hom_obj (C : Type u₁) (D : Type u₂) (F : (C D)ᵒᵖ) :
= .op
@[simp]
theorem category_theory.functor.op_inv_map (C : Type u₁) (D : Type u₂) (F G : Cᵒᵖ Dᵒᵖ) (α : F G) :
@[simp]
theorem category_theory.functor.op_inv_obj (C : Type u₁) (D : Type u₂) (F : Cᵒᵖ Dᵒᵖ) :
def category_theory.functor.op_inv (C : Type u₁) (D : Type u₂)  :

Take the "unopposite" of a functor is functorial.

Equations
@[simp]
theorem category_theory.functor.left_op_map {C : Type u₁} {D : Type u₂} (F : C Dᵒᵖ) (X Y : Cᵒᵖ) (f : X Y) :
F.left_op.map f = (F.map f.unop).unop
def category_theory.functor.left_op {C : Type u₁} {D : Type u₂} (F : C Dᵒᵖ) :

Another variant of the opposite of functor, turning a functor C ⥤ Dᵒᵖ into a functor Cᵒᵖ ⥤ D. In informal mathematics no distinction is made.

Equations
@[simp]
theorem category_theory.functor.left_op_obj {C : Type u₁} {D : Type u₂} (F : C Dᵒᵖ) (X : Cᵒᵖ) :
def category_theory.functor.right_op {C : Type u₁} {D : Type u₂} (F : Cᵒᵖ D) :

Another variant of the opposite of functor, turning a functor Cᵒᵖ ⥤ D into a functor C ⥤ Dᵒᵖ. In informal mathematics no distinction is made.

Equations
@[simp]
theorem category_theory.functor.right_op_map {C : Type u₁} {D : Type u₂} (F : Cᵒᵖ D) (X Y : C) (f : X Y) :
F.right_op.map f = (F.map f.op).op
@[simp]
theorem category_theory.functor.right_op_obj {C : Type u₁} {D : Type u₂} (F : Cᵒᵖ D) (X : C) :
@[instance]
def category_theory.functor.op.category_theory.full {C : Type u₁} {D : Type u₂} {F : C D}  :
Equations
@[instance]
def category_theory.functor.op.category_theory.faithful {C : Type u₁} {D : Type u₂} {F : C D}  :
@[instance]
def category_theory.functor.right_op_faithful {C : Type u₁} {D : Type u₂} {F : Cᵒᵖ D}  :

If F is faithful then the right_op of F is also faithful.

@[instance]
def category_theory.functor.left_op_faithful {C : Type u₁} {D : Type u₂} {F : C Dᵒᵖ}  :

If F is faithful then the left_op of F is also faithful.

@[simp]
theorem category_theory.nat_trans.op_app {C : Type u₁} {D : Type u₂} {F G : C D} (α : F G) (X : Cᵒᵖ) :
= (α.app (opposite.unop X)).op
def category_theory.nat_trans.op {C : Type u₁} {D : Type u₂} {F G : C D} (α : F G) :
G.op F.op

The opposite of a natural transformation.

Equations
@[simp]
theorem category_theory.nat_trans.op_id {C : Type u₁} {D : Type u₂} (F : C D) :
def category_theory.nat_trans.unop {C : Type u₁} {D : Type u₂} {F G : Cᵒᵖ Dᵒᵖ} (α : F G) :

The "unopposite" of a natural transformation.

Equations
@[simp]
theorem category_theory.nat_trans.unop_app {C : Type u₁} {D : Type u₂} {F G : Cᵒᵖ Dᵒᵖ} (α : F G) (X : C) :
= (α.app (opposite.op X)).unop
@[simp]
theorem category_theory.nat_trans.unop_id {C : Type u₁} {D : Type u₂} (F : Cᵒᵖ Dᵒᵖ) :
def category_theory.nat_trans.remove_op {C : Type u₁} {D : Type u₂} {F G : C D} (α : F.op G.op) :
G F

Given a natural transformation α : F.op ⟶ G.op, we can take the "unopposite" of each component obtaining a natural transformation G ⟶ F.

Equations
@[simp]
theorem category_theory.nat_trans.remove_op_app {C : Type u₁} {D : Type u₂} {F G : C D} (α : F.op G.op) (X : C) :
= (α.app (opposite.op X)).unop
@[simp]
theorem category_theory.nat_trans.remove_op_id {C : Type u₁} {D : Type u₂} (F : C D) :
@[simp]
theorem category_theory.nat_trans.left_op_app {C : Type u₁} {D : Type u₂} {F G : C Dᵒᵖ} (α : F G) (X : Cᵒᵖ) :
def category_theory.nat_trans.left_op {C : Type u₁} {D : Type u₂} {F G : C Dᵒᵖ} (α : F G) :

Given a natural transformation α : F ⟶ G, for F G : C ⥤ Dᵒᵖ, taking unop of each component gives a natural transformation G.left_op ⟶ F.left_op.

Equations
@[simp]
theorem category_theory.nat_trans.remove_left_op_app {C : Type u₁} {D : Type u₂} {F G : C Dᵒᵖ} (α : F.left_op G.left_op) (X : C) :
= (α.app (opposite.op X)).op
def category_theory.nat_trans.remove_left_op {C : Type u₁} {D : Type u₂} {F G : C Dᵒᵖ} (α : F.left_op G.left_op) :
G F

Given a natural transformation α : F.left_op ⟶ G.left_op, for F G : C ⥤ Dᵒᵖ, taking op of each component gives a natural transformation G ⟶ F.

Equations
@[simp]
theorem category_theory.iso.op_hom {C : Type u₁} {X Y : C} (α : X Y) :
α.op.hom = α.hom.op
def category_theory.iso.op {C : Type u₁} {X Y : C} (α : X Y) :

The opposite isomorphism.

Equations
@[simp]
theorem category_theory.iso.op_inv {C : Type u₁} {X Y : C} (α : X Y) :
α.op.inv = α.inv.op
@[simp]
theorem category_theory.nat_iso.op_inv {C : Type u₁} {D : Type u₂} {F G : C D} (α : F G) :
def category_theory.nat_iso.op {C : Type u₁} {D : Type u₂} {F G : C D} (α : F G) :
G.op F.op

The natural isomorphism between opposite functors G.op ≅ F.op induced by a natural isomorphism between the original functors F ≅ G.

Equations
@[simp]
theorem category_theory.nat_iso.op_hom {C : Type u₁} {D : Type u₂} {F G : C D} (α : F G) :
@[simp]
theorem category_theory.nat_iso.remove_op_inv {C : Type u₁} {D : Type u₂} {F G : C D} (α : F.op G.op) :
@[simp]
theorem category_theory.nat_iso.remove_op_hom {C : Type u₁} {D : Type u₂} {F G : C D} (α : F.op G.op) :
def category_theory.nat_iso.remove_op {C : Type u₁} {D : Type u₂} {F G : C D} (α : F.op G.op) :
G F

The natural isomorphism between functors G ≅ F induced by a natural isomorphism between the opposite functors F.op ≅ G.op.

Equations
@[simp]
theorem category_theory.nat_iso.unop_hom {C : Type u₁} {D : Type u₂} {F G : Cᵒᵖ Dᵒᵖ} (α : F G) :
@[simp]
theorem category_theory.nat_iso.unop_inv {C : Type u₁} {D : Type u₂} {F G : Cᵒᵖ Dᵒᵖ} (α : F G) :
def category_theory.nat_iso.unop {C : Type u₁} {D : Type u₂} {F G : Cᵒᵖ Dᵒᵖ} (α : F G) :

The natural isomorphism between functors G.unop ≅ F.unop induced by a natural isomorphism between the original functors F ≅ G.

Equations
@[simp]
theorem category_theory.equivalence.op_counit_iso {C : Type u₁} {D : Type u₂} (e : C D) :
@[simp]
theorem category_theory.equivalence.op_inverse {C : Type u₁} {D : Type u₂} (e : C D) :
@[simp]
theorem category_theory.equivalence.op_functor {C : Type u₁} {D : Type u₂} (e : C D) :
@[simp]
theorem category_theory.equivalence.op_unit_iso {C : Type u₁} {D : Type u₂} (e : C D) :
def category_theory.equivalence.op {C : Type u₁} {D : Type u₂} (e : C D) :

An equivalence between categories gives an equivalence between the opposite categories.

Equations
@[simp]
theorem category_theory.equivalence.unop_inverse {C : Type u₁} {D : Type u₂} (e : Cᵒᵖ Dᵒᵖ) :
@[simp]
theorem category_theory.equivalence.unop_functor {C : Type u₁} {D : Type u₂} (e : Cᵒᵖ Dᵒᵖ) :
def category_theory.equivalence.unop {C : Type u₁} {D : Type u₂} (e : Cᵒᵖ Dᵒᵖ) :
C D

An equivalence between opposite categories gives an equivalence between the original categories.

Equations
@[simp]
theorem category_theory.equivalence.unop_counit_iso {C : Type u₁} {D : Type u₂} (e : Cᵒᵖ Dᵒᵖ) :
@[simp]
theorem category_theory.equivalence.unop_unit_iso {C : Type u₁} {D : Type u₂} (e : Cᵒᵖ Dᵒᵖ) :
def category_theory.op_equiv {C : Type u₁} (A B : Cᵒᵖ) :
(A B)

The equivalence between arrows of the form A ⟶ B and B.unop ⟶ A.unop. Useful for building adjunctions. Note that this (definitionally) gives variants

def op_equiv' (A : C) (B : Cᵒᵖ) : (opposite.op A ⟶ B) ≃ (B.unop ⟶ A) :=
op_equiv _ _

def op_equiv'' (A : Cᵒᵖ) (B : C) : (A ⟶ opposite.op B) ≃ (B ⟶ A.unop) :=
op_equiv _ _

def op_equiv''' (A B : C) : (opposite.op A ⟶ opposite.op B) ≃ (B ⟶ A) :=
op_equiv _ _

`
Equations
@[simp]
theorem category_theory.op_equiv_symm_apply {C : Type u₁} (A B : Cᵒᵖ) (g : ) :
B).symm) g = g.op
@[simp]
theorem category_theory.op_equiv_apply {C : Type u₁} (A B : Cᵒᵖ) (f : A B) :
f = f.unop
@[instance]
def category_theory.subsingleton_of_unop {C : Type u₁} (A B : Cᵒᵖ) [subsingleton ] :
@[instance]
def category_theory.decidable_eq_of_unop {C : Type u₁} (A B : Cᵒᵖ) [decidable_eq ] :
Equations
def category_theory.op_hom_of_le {α : Type v} [preorder α] {U V : αᵒᵖ} (h : ) :
U V

Construct a morphism in the opposite of a preorder category from an inequality.

Equations
theorem category_theory.le_of_op_hom {α : Type v} [preorder α] {U V : αᵒᵖ} (h : U V) :