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
- category_theory.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
.
If G.op
is adjoint to F
then F.unop
is adjoint to G
.
If G
is adjoint to F
then F.unop
is adjoint to G.unop
.
If G
is adjoint to F
then F.op
is adjoint to G.op
.
Equations
- category_theory.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
.
If G.unop
is adjoint to F
then F.op
is adjoint to G
.
If G.unop
is adjoint to F.unop
then F
is adjoint to 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
- adj1.left_adjoints_coyoneda_equiv 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.
Equations
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
- adj1.nat_iso_of_left_adjoint_nat_iso adj2 l = adj1.right_adjoint_uniq (adj2.of_nat_iso_left l.symm)
Given two adjunctions, if the right adjoints are naturally isomorphic, then so are the left adjoints.
Equations
- adj1.nat_iso_of_right_adjoint_nat_iso adj2 r = adj1.left_adjoint_uniq (adj2.of_nat_iso_right r.symm)