Adjoint functor theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves the (general) adjoint functor theorem, in the form:

If G : D ⥤ C preserves limits and D has limits, and satisfies the solution set condition, then it has a left adjoint: is_right_adjoint_of_preserves_limits_of_solution_set_condition.

We show that the converse holds, i.e. that if G has a left adjoint then it satisfies the solution set condition, see solution_set_condition_of_is_right_adjoint (the file category_theory/adjunction/limits already shows it preserves limits).

We define the solution set condition for the functor G : D ⥤ C to mean, for every object A : C, there is a set-indexed family ${f_i : A ⟶ G (B_i)}$ such that any morphism A ⟶ G X factors through one of the f_i.

This file also proves the special adjoint functor theorem, in the form:

If G : D ⥤ C preserves limits and D is complete, well-powered and has a small coseparating set, then G has a left adjoint: is_right_adjoint_of_preserves_limits_of_is_coseparating

Finally, we prove the following corollary of the special adjoint functor theorem:

If C is complete, well-powered and has a small coseparating set, then it is cocomplete: has_colimits_of_has_limits_of_is_coseparating

source

def category_theory.solution_set_condition {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] (G : D ⥤ C) :

Prop

The functor G : D ⥤ C satisfies the solution set condition if for every A : C, there is a family of morphisms {f_i : A ⟶ G (B_i) // i ∈ ι} such that given any morphism h : A ⟶ G X, there is some i ∈ ι such that h factors through f_i.

The key part of this definition is that the indexing set ι lives in Type v, where v is the universe of morphisms of the category: this is the "smallness" condition which allows the general adjoint functor theorem to go through.

Equations

category_theory.solution_set_condition G = ∀ (A : C), ∃ (ι : Type v) (B : ι → D) (f : Π (i : ι), A ⟶ G.obj (B i)), ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h

source

theorem category_theory.solution_set_condition_of_is_right_adjoint {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] (G : D ⥤ C) [category_theory.is_right_adjoint G] :

category_theory.solution_set_condition G

If G : D ⥤ C is a right adjoint it satisfies the solution set condition.

source

noncomputable def category_theory.is_right_adjoint_of_preserves_limits_of_solution_set_condition {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] (G : D ⥤ C) [category_theory.limits.has_limits D] [category_theory.limits.preserves_limits G] (hG : category_theory.solution_set_condition G) :

category_theory.is_right_adjoint G

The general adjoint functor theorem says that if G : D ⥤ C preserves limits and D has them, if G satisfies the solution set condition then G is a right adjoint.

Equations

category_theory.is_right_adjoint_of_preserves_limits_of_solution_set_condition G hG = category_theory.is_right_adjoint_of_structured_arrow_initials G

source

noncomputable def category_theory.is_right_adjoint_of_preserves_limits_of_is_coseparating {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_limits D] [category_theory.well_powered D] {𝒢 : set D} [small ↥𝒢] (h𝒢 : category_theory.is_coseparating 𝒢) (G : D ⥤ C) [category_theory.limits.preserves_limits G] :

category_theory.is_right_adjoint G

The special adjoint functor theorem: if G : D ⥤ C preserves limits and D is complete, well-powered and has a small coseparating set, then G has a left adjoint.

Equations

category_theory.is_right_adjoint_of_preserves_limits_of_is_coseparating h𝒢 G = have this : ∀ (A : C), category_theory.limits.has_initial (category_theory.structured_arrow A G), from _, category_theory.is_right_adjoint_of_structured_arrow_initials G _

source

noncomputable def category_theory.is_left_adjoint_of_preserves_colimits_of_is_separatig {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_colimits C] [category_theory.well_powered Cᵒᵖ] {𝒢 : set C} [small ↥𝒢] (h𝒢 : category_theory.is_separating 𝒢) (F : C ⥤ D) [category_theory.limits.preserves_colimits F] :

category_theory.is_left_adjoint F

The special adjoint functor theorem: if F : C ⥤ D preserves colimits and C is cocomplete, well-copowered and has a small separating set, then F has a right adjoint.

Equations

category_theory.is_left_adjoint_of_preserves_colimits_of_is_separatig h𝒢 F = have this : ∀ (A : D), category_theory.limits.has_terminal (category_theory.costructured_arrow F A), from _, category_theory.is_left_adjoint_of_costructured_arrow_terminals F _

source

theorem category_theory.limits.has_colimits_of_has_limits_of_is_coseparating {C : Type u} [category_theory.category C] [category_theory.limits.has_limits C] [category_theory.well_powered C] {𝒢 : set C} [small ↥𝒢] (h𝒢 : category_theory.is_coseparating 𝒢) :

category_theory.limits.has_colimits C

A consequence of the special adjoint functor theorem: if C is complete, well-powered and has a small coseparating set, then it is cocomplete.

source

theorem category_theory.limits.has_limits_of_has_colimits_of_is_separating {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] [category_theory.well_powered Cᵒᵖ] {𝒢 : set C} [small ↥𝒢] (h𝒢 : category_theory.is_separating 𝒢) :

category_theory.limits.has_limits C

A consequence of the special adjoint functor theorem: if C is cocomplete, well-copowered and has a small separating set, then it is complete.