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

source
def adjunction.adjoint_of_op_adjoint_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (G : D ⥤ C) (h : G.op ⊣ F.op) :
F ⊣ G

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

Equations
source
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ᵒᵖ) (h : G ⊣ F.op) :
F ⊣ G.unop

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

Equations
source
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) (h : G.op ⊣ F) :
F.unop ⊣ G

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

Equations
source
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ᵒᵖ) (h : G ⊣ F) :
F.unop ⊣ G.unop

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

Equations
source
def adjunction.op_adjoint_op_of_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (G : D ⥤ C) (h : G ⊣ F) :
F.op ⊣ G.op

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

Equations
source
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) (h : G ⊣ F.unop) :
F ⊣ G.op

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

Equations
source
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ᵒᵖ) (h : G.unop ⊣ F) :
F.op ⊣ G

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

Equations
source
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ᵒᵖ) (h : G.unop ⊣ F.unop) :
F ⊣ G

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

Equations
source
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} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
F.op ⋙ category_theory.coyoneda ≅ F'.op ⋙ category_theory.coyoneda

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
source
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} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
F ≅ F'

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

Equations
source
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} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
G ≅ G'

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

Equations
source
def adjunction.nat_iso_of_left_adjoint_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (l : F ≅ F') :
G ≅ G'

Given two adjunctions, if the left adjoints are naturally isomorphic, then so are the right adjoints.

Equations
source
def adjunction.nat_iso_of_right_adjoint_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (r : G ≅ G') :
F ≅ F'

Given two adjunctions, if the right adjoints are naturally isomorphic, then so are the left adjoints.

Equations