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