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
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' := _}
If G
is adjoint to F.op
then F
is adjoint to G.unop
.
Equations
If G.op
is adjoint to F
then F.unop
is adjoint to G
.
Equations
If G
is adjoint to F
then F.unop
is adjoint to G.unop
.
Equations
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' := _}
If G
is adjoint to F.unop
then F
is adjoint to G.op
.
Equations
If G.unop
is adjoint to F
then F.op
is adjoint to G
.
Equations
If G.unop
is adjoint to F.unop
then F
is adjoint to G
.
Equations
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
- adjunction.left_adjoints_coyoneda_equiv adj1 adj2 = category_theory.nat_iso.of_components (λ (X : Cᵒᵖ), category_theory.nat_iso.of_components (λ (Y : D), ((adj1.hom_equiv (opposite.unop X) Y).trans (adj2.hom_equiv (opposite.unop X) Y).symm).to_iso) _) _
If F
and F'
are both left adjoint to G
, then they are naturally isomorphic.
If G
and G'
are both right adjoint to F
, then they are naturally isomorphic.
Equations
Given two adjunctions, if the left adjoints are naturally isomorphic, then so are the right adjoints.
Equations
- adjunction.nat_iso_of_left_adjoint_nat_iso adj1 adj2 l = adjunction.right_adjoint_uniq adj1 (adj2.of_nat_iso_left l.symm)
Given two adjunctions, if the right adjoints are naturally isomorphic, then so are the left adjoints.
Equations
- adjunction.nat_iso_of_right_adjoint_nat_iso adj1 adj2 r = adjunction.left_adjoint_uniq adj1 (adj2.of_nat_iso_right r.symm)