# mathlibdocumentation

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

def adjunction.adjoint_of_op_adjoint_op {C : Type u₁} {D : Type u₂} (F : C D) (G : D C) :
(G.op F.op)(F G)

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

Equations
def adjunction.adjoint_unop_of_adjoint_op {C : Type u₁} {D : Type u₂} (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₁} {D : Type u₂} (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₁} {D : Type u₂} (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.op_adjoint_op_of_adjoint {C : Type u₁} {D : Type u₂} (F : C D) (G : D C) :
(G F)(F.op G.op)

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

Equations
def adjunction.adjoint_op_of_adjoint_unop {C : Type u₁} {D : Type u₂} (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₁} {D : Type u₂} (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₁} {D : Type u₂} (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₁} {D : Type u₂} {F F' : C D} {G : D C} :
(F G)(F' G)

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₁} {D : Type u₂} {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₁} {D : Type u₂} {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