mathlib3 documentation

category_theory.opposites

Opposite categories #

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

We provide a category instance on Cᵒᵖ. The morphisms X ⟶ Y are defined to be the morphisms unop Y ⟶ unop X in C.

Here Cᵒᵖ is an irreducible typeclass synonym for C (it is the same one used in the algebra library).

We also provide various mechanisms for constructing opposite morphisms, functors, and natural transformations.

Unfortunately, because we do not have a definitional equality op (op X) = X, there are quite a few variations that are needed in practice.

theorem quiver.hom.op_inj {C : Type u₁} [quiver C] {X Y : C} :
@[simp]
theorem quiver.hom.unop_op {C : Type u₁} [quiver C] {X Y : C} (f : X Y) :
f.op.unop = f
@[simp]
theorem quiver.hom.op_unop {C : Type u₁} [quiver C] {X Y : Cᵒᵖ} (f : X Y) :
f.unop.op = f
@[simp]
theorem category_theory.op_comp {C : Type u₁} [category_theory.category C] {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₁} [category_theory.category C] {X : C} :
@[simp]
theorem category_theory.unop_comp {C : Type u₁} [category_theory.category C] {X Y Z : Cᵒᵖ} {f : X Y} {g : Y Z} :
(f g).unop = g.unop f.unop
@[simp]
@[simp]
@[simp]

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

Equations
@[simp]
@[simp]
theorem category_theory.unop_unop_map (C : Type u₁) [category_theory.category C] (X Y : C) (f : X Y) :

The functor from a category to its double-opposite.

Equations
@[protected, instance]

If f is an isomorphism, so is f.op

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

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

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
Instances for category_theory.functor.op
@[simp]
@[protected]

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ Dᵒᵖ) (X Y : C) (f : X Y) :
F.unop.map f = (F.map f.op).unop
@[simp]

The isomorphism between F.op.unop and F.

Equations
@[simp]

The isomorphism between F.unop.op and F.

Equations

Taking the opposite of a functor is functorial.

Equations
@[simp]
@[simp]

Take the "unopposite" of a functor is functorial.

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

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
Instances for category_theory.functor.left_op
@[protected]

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
Instances for category_theory.functor.right_op
@[simp]
theorem category_theory.functor.right_op_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ D) (X Y : C) (f : X Y) :
F.right_op.map f = (F.map f.op).op
@[protected, instance]

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

@[protected, instance]

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

Whenever possible, it is advisable to use the isomorphism right_op_left_op_iso instead of this equality of functors.

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

The opposite of a natural transformation.

Equations
@[protected]

The "unopposite" of a natural transformation.

Equations
@[simp]
@[protected]
def category_theory.nat_trans.remove_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {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]
@[protected]

Given a natural transformation α : F.unop ⟶ G.unop, we can take the opposite of each component obtaining a natural transformation G ⟶ F.

Equations
@[protected]

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
@[protected]

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]
@[protected]

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

Equations
@[protected]

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

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

The opposite isomorphism.

Equations
@[simp]
theorem category_theory.iso.op_inv {C : Type u₁} [category_theory.category C] {X Y : C} (α : X Y) :
α.op.inv = α.inv.op
@[simp]
theorem category_theory.iso.unop_inv {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (f : X Y) :
@[simp]
theorem category_theory.iso.unop_hom {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (f : X Y) :

The isomorphism obtained from an isomorphism in the opposite category.

Equations
@[simp]
theorem category_theory.iso.unop_op {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (f : X Y) :
f.unop.op = f
@[simp]
theorem category_theory.iso.op_unop {C : Type u₁} [category_theory.category C] {X Y : C} (f : X Y) :
f.op.unop = f
@[protected]
def category_theory.nat_iso.op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {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
@[protected]
def category_theory.nat_iso.remove_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {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
@[protected]

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

Equations

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

Equations

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

Equations

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]

The equivalence between isomorphisms of the form A ≅ B and B.unop ≅ A.unop.

Note this is definitionally the same as the other three variants:

Equations