Adjunctions between functors #
F ⊣ G
represents the data of an adjunction between two functors
F : C ⥤ D
and G : D ⥤ C
. F
is the left adjoint and G
is the right adjoint.
We provide various useful constructors:
mk_of_hom_equiv
mk_of_unit_counit
left_adjoint_of_equiv
/right_adjoint_of equiv
construct a left/right adjoint of a given functor given the action on objects and the relevant equivalence of morphism spaces.adjunction_of_equiv_left
/adjunction_of_equiv_right
witness that these constructions give adjunctions.
There are also typeclasses is_left_adjoint
/ is_right_adjoint
, carrying data witnessing
that a given functor is a left or right adjoint.
Given [is_left_adjoint F]
, a right adjoint of F
can be constructed as right_adjoint F
.
adjunction.comp
composes adjunctions.
to_equivalence
upgrades an adjunction to an equivalence,
given witnesses that the unit and counit are pointwise isomorphisms.
Conversely equivalence.to_adjunction
recovers the underlying adjunction from an equivalence.
- hom_equiv : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
- unit : 𝟭 C ⟶ F ⋙ G
- counit : G ⋙ F ⟶ 𝟭 D
- hom_equiv_unit' : (∀ {X : C} {Y : D} {f : F.obj X ⟶ Y}, ⇑(self.hom_equiv X Y) f = self.unit.app X ≫ G.map f) . "obviously"
- hom_equiv_counit' : (∀ {X : C} {Y : D} {g : X ⟶ G.obj Y}, ⇑((self.hom_equiv X Y).symm) g = F.map g ≫ self.counit.app Y) . "obviously"
F ⊣ G
represents the data of an adjunction between two functors
F : C ⥤ D
and G : D ⥤ C
. F
is the left adjoint and G
is the right adjoint.
To construct an adjunction
between two functors, it's often easier to instead use the
constructors mk_of_hom_equiv
or mk_of_unit_counit
. To construct a left adjoint,
there are also constructors left_adjoint_of_equiv
and adjunction_of_equiv_left
(as
well as their duals) which can be simpler in practice.
Uniqueness of adjoints is shown in category_theory.adjunction.opposites
.
See https://stacks.math.columbia.edu/tag/0037.
Instances for category_theory.adjunction
- category_theory.adjunction.has_sizeof_inst
- category_theory.adjunction.inhabited
- right : D ⥤ C
- adj : left ⊣ category_theory.is_left_adjoint.right left
A class giving a chosen right adjoint to the functor left
.
Instances of this typeclass
- category_theory.functor.left_adjoint_of_equivalence
- category_theory.comonadic_left_adjoint.to_is_left_adjoint
- category_theory.adjunction.left_adjoint_of_comp
- Top.category_theory.forget.category_theory.is_left_adjoint
- category_theory.evaluation_is_left_adjoint
- category_theory.comonad.forget.category_theory.is_left_adjoint
- category_theory.over.forget.is_left_adjoint
- category_theory.obj.is_left_adjoint
Instances of other typeclasses for category_theory.is_left_adjoint
- category_theory.is_left_adjoint.has_sizeof_inst
- left : C ⥤ D
- adj : category_theory.is_right_adjoint.left right ⊣ right
A class giving a chosen left adjoint to the functor right
.
Instances of this typeclass
- category_theory.functor.right_adjoint_of_equivalence
- category_theory.reflective.to_is_right_adjoint
- category_theory.monadic_right_adjoint.to_is_right_adjoint
- category_theory.adjunction.right_adjoint_of_comp
- Algebra.category_theory.forget.category_theory.is_right_adjoint
- category_theory.over.pullback_is_right_adjoint
- category_theory.mono_over.forget.category_theory.is_right_adjoint
- AddCommGroup.category_theory.forget.category_theory.is_right_adjoint
- Group.category_theory.forget.category_theory.is_right_adjoint
- Mon.units.category_theory.is_right_adjoint
- CommMon.units.category_theory.is_right_adjoint
- Module.category_theory.forget.category_theory.is_right_adjoint
- category_theory.forget.category_theory.is_right_adjoint
- CommRing.category_theory.forget.category_theory.is_right_adjoint
- Top.category_theory.forget.category_theory.is_right_adjoint
- category_theory.Sheaf_to_presheaf_is_right_adjoint
- algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.is_right_adjoint
- algebraic_geometry.Scheme.Spec.category_theory.is_right_adjoint
- category_theory.evaluation_is_right_adjoint
- category_theory.monad.forget.category_theory.is_right_adjoint
- category_theory.Sheaf.category_theory.Sheaf_compose.category_theory.is_right_adjoint
- category_theory.Sheaf.category_theory.Sheaf_forget.category_theory.is_right_adjoint
- UniformSpace.category_theory.forget₂.category_theory.is_right_adjoint
Instances of other typeclasses for category_theory.is_right_adjoint
- category_theory.is_right_adjoint.has_sizeof_inst
Extract the left adjoint from the instance giving the chosen adjoint.
Extract the right adjoint from the instance giving the chosen adjoint.
The adjunction associated to a functor known to be a left adjoint.
The adjunction associated to a functor known to be a right adjoint.
- hom_equiv : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
- hom_equiv_naturality_left_symm' : (∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y), ⇑((self.hom_equiv X' Y).symm) (f ≫ g) = F.map f ≫ ⇑((self.hom_equiv X Y).symm) g) . "obviously"
- hom_equiv_naturality_right' : (∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), ⇑(self.hom_equiv X Y') (f ≫ g) = ⇑(self.hom_equiv X Y) f ≫ G.map g) . "obviously"
This is an auxiliary data structure useful for constructing adjunctions.
See adjunction.mk_of_hom_equiv
.
This structure won't typically be used anywhere else.
Instances for category_theory.adjunction.core_hom_equiv
- category_theory.adjunction.core_hom_equiv.has_sizeof_inst
- unit : 𝟭 C ⟶ F ⋙ G
- counit : G ⋙ F ⟶ 𝟭 D
- left_triangle' : category_theory.whisker_right self.unit F ≫ (F.associator G F).hom ≫ category_theory.whisker_left F self.counit = category_theory.nat_trans.id (𝟭 C ⋙ F) . "obviously"
- right_triangle' : category_theory.whisker_left G self.unit ≫ (G.associator F G).inv ≫ category_theory.whisker_right self.counit G = category_theory.nat_trans.id (G ⋙ 𝟭 C) . "obviously"
This is an auxiliary data structure useful for constructing adjunctions.
See adjunction.mk_of_unit_counit
.
This structure won't typically be used anywhere else.
Instances for category_theory.adjunction.core_unit_counit
- category_theory.adjunction.core_unit_counit.has_sizeof_inst
Construct an adjunction between F
and G
out of a natural bijection between each
F.obj X ⟶ Y
and X ⟶ G.obj Y
.
Equations
- category_theory.adjunction.mk_of_hom_equiv adj = {hom_equiv := adj.hom_equiv, unit := {app := λ (X : C), ⇑(adj.hom_equiv X (F.obj X)) (𝟙 (F.obj X)), naturality' := _}, counit := {app := λ (Y : D), (adj.hom_equiv (G.obj Y) ((𝟭 D).obj Y)).inv_fun (𝟙 (G.obj Y)), naturality' := _}, hom_equiv_unit' := _, hom_equiv_counit' := _}
Construct an adjunction between functors F
and G
given a unit and counit for the adjunction
satisfying the triangle identities.
Equations
- category_theory.adjunction.mk_of_unit_counit adj = {hom_equiv := λ (X : C) (Y : D), {to_fun := λ (f : F.obj X ⟶ Y), adj.unit.app X ≫ G.map f, inv_fun := λ (g : X ⟶ G.obj Y), F.map g ≫ adj.counit.app Y, left_inv := _, right_inv := _}, unit := adj.unit, counit := adj.counit, hom_equiv_unit' := _, hom_equiv_counit' := _}
The adjunction between the identity functor on a category and itself.
Equations
- category_theory.adjunction.id = {hom_equiv := λ (X Y : C), equiv.refl ((𝟭 C).obj X ⟶ Y), unit := 𝟙 (𝟭 C), counit := 𝟙 (𝟭 C ⋙ 𝟭 C), hom_equiv_unit' := _, hom_equiv_counit' := _}
Equations
If F and G are naturally isomorphic functors, establish an equivalence of hom-sets.
If G and H are naturally isomorphic functors, establish an equivalence of hom-sets.
Transport an adjunction along an natural isomorphism on the left.
Equations
- adj.of_nat_iso_left iso = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : C) (Y : D), (category_theory.adjunction.equiv_homset_left_of_nat_iso iso.symm).trans (adj.hom_equiv X Y), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
Transport an adjunction along an natural isomorphism on the right.
Equations
- adj.of_nat_iso_right iso = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : C) (Y : D), (adj.hom_equiv X Y).trans (category_theory.adjunction.equiv_homset_right_of_nat_iso iso), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
Transport being a right adjoint along a natural isomorphism.
Transport being a left adjoint along a natural isomorphism.
Composition of adjunctions.
See https://stacks.math.columbia.edu/tag/0DV0.
Equations
- adj₁.comp adj₂ = {hom_equiv := λ (X : C) (Z : E), (adj₂.hom_equiv (F.obj X) Z).trans (adj₁.hom_equiv X (I.obj Z)), unit := adj₁.unit ≫ category_theory.whisker_left F (category_theory.whisker_right adj₂.unit G) ≫ (F.associator (H ⋙ I) G).inv, counit := (I.associator G (F ⋙ H)).hom ≫ category_theory.whisker_left I (category_theory.whisker_right adj₁.counit H) ≫ adj₂.counit, hom_equiv_unit' := _, hom_equiv_counit' := _}
If F
and G
are left adjoints then F ⋙ G
is a left adjoint too.
If F
and G
are right adjoints then F ⋙ G
is a right adjoint too.
Construct a left adjoint functor to G
, given the functor's value on objects F_obj
and
a bijection e
between F_obj X ⟶ Y
and X ⟶ G.obj Y
satisfying a naturality law
he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g
.
Dual to right_adjoint_of_equiv
.
Show that the functor given by left_adjoint_of_equiv
is indeed left adjoint to G
. Dual
to adjunction_of_equiv_right
.
Construct a right adjoint functor to F
, given the functor's value on objects G_obj
and
a bijection e
between F.obj X ⟶ Y
and X ⟶ G_obj Y
satisfying a naturality law
he : ∀ X Y Y' g h, e X' Y (F.map f ≫ g) = f ≫ e X Y g
.
Dual to left_adjoint_of_equiv
.
Show that the functor given by right_adjoint_of_equiv
is indeed right adjoint to F
. Dual
to adjunction_of_equiv_left
.
If the unit and counit of a given adjunction are (pointwise) isomorphisms, then we can upgrade the adjunction to an equivalence.
Equations
- adj.to_equivalence = {functor := F, inverse := G, unit_iso := category_theory.nat_iso.of_components (λ (X : C), category_theory.as_iso (adj.unit.app X)) _, counit_iso := category_theory.nat_iso.of_components (λ (Y : D), category_theory.as_iso (adj.counit.app Y)) _, functor_unit_iso_comp' := _}
If the unit and counit for the adjunction corresponding to a right adjoint functor are (pointwise) isomorphisms, then the functor is an equivalence of categories.
The adjunction given by an equivalence of categories. (To obtain the opposite adjunction,
simply use e.symm.to_adjunction
.
Equations
- e.to_adjunction = category_theory.adjunction.mk_of_unit_counit {unit := e.unit, counit := e.counit, left_triangle' := _, right_triangle' := _}
An equivalence E
is left adjoint to its inverse.
Equations
If F
is an equivalence, it's a left adjoint.
Equations
- category_theory.functor.left_adjoint_of_equivalence = {right := F.inv _inst_3, adj := F.adjunction _inst_3}
If F
is an equivalence, it's a right adjoint.
Equations
- category_theory.functor.right_adjoint_of_equivalence = {left := F.inv _inst_3, adj := F.inv.adjunction F.is_equivalence_inv}