mathlib documentation

category_theory.adjunction.opposites

Opposite adjunctions

This file contains constructions to relate adjunctions of functors to adjunctions of their opposites. These constructions are used to show uniqueness of adjoints (up to natural isomorphism).

Tags

adjunction, opposite, uniqueness

def adjunction.adjoint_unop_of_adjoint_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) (G : Dᵒᵖ Cᵒᵖ) :
(G F.op)(F G.unop)

If G is adjoint to F.op then F is adjoint to G.unop.

Equations
def adjunction.unop_adjoint_of_op_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ Dᵒᵖ) (G : D C) :
(G.op F)(F.unop G)

If G.op is adjoint to F then F.unop is adjoint to G.

Equations
def adjunction.unop_adjoint_unop_of_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ Dᵒᵖ) (G : Dᵒᵖ Cᵒᵖ) :
(G F)(F.unop G.unop)

If G is adjoint to F then F.unop is adjoint to G.unop.

Equations
def adjunction.adjoint_op_of_adjoint_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ Dᵒᵖ) (G : D C) :
(G F.unop)(F G.op)

If G is adjoint to F.unop then F is adjoint to G.op.

Equations
def adjunction.op_adjoint_of_unop_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) (G : Dᵒᵖ Cᵒᵖ) :
(G.unop F)(F.op G)

If G.unop is adjoint to F then F.op is adjoint to G.

Equations
def adjunction.adjoint_of_unop_adjoint_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ Dᵒᵖ) (G : Dᵒᵖ Cᵒᵖ) :
(G.unop F.unop)(F G)

If G.unop is adjoint to F.unop then F is adjoint to G.

Equations
def adjunction.left_adjoints_coyoneda_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : D C} :

If F and F' are both adjoint to G, there is a natural isomorphism F.op ⋙ coyoneda ≅ F'.op ⋙ coyoneda. We use this in combination with fully_faithful_cancel_right to show left adjoints are unique.

Equations
def adjunction.left_adjoint_uniq {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : D C} :
(F G)(F' G)(F F')

If F and F' are both left adjoint to G, then they are naturally isomorphic.

Equations
def adjunction.right_adjoint_uniq {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' : D C} :
(F G)(F G')(G G')

If G and G' are both right adjoint to F, then they are naturally isomorphic.

Equations