Documentation

Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Adjoint functor theorem #

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

We show that the converse holds, i.e. that if G has a left adjoint then it satisfies the solution set condition, see solutionSetCondition_of_isRightAdjoint (the file CategoryTheory/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:

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

source
def CategoryTheory.SolutionSetCondition {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] (G : CategoryTheory.Functor 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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.solutionSetCondition_of_isRightAdjoint {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] (G : CategoryTheory.Functor D C) [G.IsRightAdjoint] :
    CategoryTheory.SolutionSetCondition G

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

    source
    theorem CategoryTheory.isRightAdjoint_of_preservesLimits_of_solutionSetCondition {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] (G : CategoryTheory.Functor D C) [CategoryTheory.Limits.HasLimits D] [CategoryTheory.Limits.PreservesLimits G] (hG : CategoryTheory.SolutionSetCondition G) :
    G.IsRightAdjoint

    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.

    source
    theorem CategoryTheory.isRightAdjoint_of_preservesLimits_of_isCoseparating {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasLimits D] [CategoryTheory.WellPowered D] {𝒢 : Set D} [Small.{v, u'} ↑𝒢] (h𝒢 : CategoryTheory.IsCoseparating 𝒢) (G : CategoryTheory.Functor D C) [CategoryTheory.Limits.PreservesLimits G] :
    G.IsRightAdjoint

    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.

    source
    theorem CategoryTheory.isLeftAdjoint_of_preservesColimits_of_isSeparating {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.WellPowered Cᵒᵖ] {𝒢 : Set C} [Small.{v, u} ↑𝒢] (h𝒢 : CategoryTheory.IsSeparating 𝒢) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimits F] :
    F.IsLeftAdjoint

    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.

    source
    theorem CategoryTheory.Limits.hasColimits_of_hasLimits_of_isCoseparating {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.WellPowered C] {𝒢 : Set C} [Small.{v, u} ↑𝒢] (h𝒢 : CategoryTheory.IsCoseparating 𝒢) :
    CategoryTheory.Limits.HasColimits 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 CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparating {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.WellPowered Cᵒᵖ] {𝒢 : Set C} [Small.{v, u} ↑𝒢] (h𝒢 : CategoryTheory.IsSeparating 𝒢) :
    CategoryTheory.Limits.HasLimits 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.

    source
    theorem CategoryTheory.Limits.hasLimits_of_hasColimits_of_hasSeparator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.HasSeparator C] [CategoryTheory.WellPowered Cᵒᵖ] :
    CategoryTheory.Limits.HasLimits C

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

    source
    theorem CategoryTheory.Limits.hasColimits_of_hasLimits_of_hasCoseparator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.HasCoseparator C] [CategoryTheory.WellPowered C] :
    CategoryTheory.Limits.HasColimits C

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