Opposite adjunctions
This file contains constructions to relate adjunctions of functors to adjunctions of their opposites.
Tags
adjunction, opposite
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) :
If G.op is adjoint to F.op then F is adjoint to G.
Equations
- adjunction.adjoint_of_op_adjoint_op F G h = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : C) (Y : D), ((h.hom_equiv (opposite.op Y) (opposite.op X)).trans (category_theory.op_equiv (opposite.op Y) (F.op.obj (opposite.op X)))).symm.trans (category_theory.op_equiv (G.op.obj (opposite.op Y)) (opposite.op X)), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
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ᵒᵖ) :
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) :
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ᵒᵖ) :
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₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(G : D ⥤ C) :
If G is adjoint to F then F.op is adjoint to G.op.
Equations
- adjunction.op_adjoint_op_of_adjoint F G h = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Cᵒᵖ) (Y : Dᵒᵖ), (category_theory.op_equiv (F.op.obj X) Y).trans ((h.hom_equiv (opposite.unop Y) (opposite.unop X)).symm.trans (category_theory.op_equiv X (opposite.op (G.obj (opposite.unop Y)))).symm), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
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) :
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ᵒᵖ) :
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ᵒᵖ) :
If G.unop is adjoint to F.unop then F is adjoint to G.