Adjoint functor theorems for locally presentable categories

Stream: Is there code for X?

[Dagur Asgeirsson]

Has anyone worked on proving the adjoint functor theorems in the setting of locally presentable categories? Something like the following

import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
import Mathlib.CategoryTheory.Presentable.LocallyPresentable

universe v u

open CategoryTheory Limits Functor

namespace CategoryTheory.Adjunction

variable {C D : Type u} [Category.{v} C] [Category.{v} D] [IsLocallyPresentable.{v} C]
    [IsLocallyPresentable.{v} D]

lemma presentableAdjointFunctorTheorem₁ (L : C ⥤ D) [PreservesColimits L] [HasColimits C] :
    L.IsLeftAdjoint := by
  sorry

lemma presentableAdjointFunctorTheorem₂ (R : C ⥤ D) [IsAccessible.{v} R] [PreservesLimits R]
    [HasLimits C] : R.IsRightAdjoint := by
  sorry

end CategoryTheory.Adjunction

See nLab and Adamek Rosicky theorem 1.66. I see presentability/accessibility is actively being worked on, so I just want to make sure I don't duplicate efforts. (@Joël Riou, @Christian Merten , @Andrew Yang)

[Christian Merten]

I am not working on anything related. If someone has done something on this, then most likely Joël.

[Joël Riou]

I am not working specifically on this theorem. I have been doing a few pull requests #29565, #29556, #29543, #29519, #29518 as I intend to show theorem 1.20 of Adámek-Rosicky that a category is locally κ-presentable iff it is cocomplete and has a strong generator formed by κ-presentable objects. (In particular, if it is so, it is also locally κ'-presentable for any larger κ', which seems to be the first step of the proof of theorem 1.66.)
(My plan is to understand a little bit of how locally presentable categories behave with respect to the change of the regular cardinal. My real goal in this matter is to formalize Theorem 2.43 about the accessibility of comma categories (for which I have done some preliminary work in #20267), but for this, I would need to understand how accessible categories respect behave regarding to the change of the regular cardinal, which is quite intricate...)

[Joël Riou]

I have just finished formalising a few theorems about locally presentable categories:

• the characterization of locally presentable categories mentioned above https://github.com/joelriou/mathlib4/blob/ea3a7bb9fb083d629e20759d2e85205cbfb10c1b/Mathlib/CategoryTheory/Presentable/StrongGenerator.lean#L164
• the orthogonal reflection theorem (Theorem 1.39 (only (i) → (ii), as the opposite implication is wrong...) and Corollary 1.40 from Adámek-Rosicky), see also https://ncatlab.org/nlab/show/orthogonal+subcategory+problem https://github.com/joelriou/mathlib4/blob/ea3a7bb9fb083d629e20759d2e85205cbfb10c1b/Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean#L451
• Cᵒᵖ ⥤ A is locally presentable when C is small and A is locally presentable https://github.com/joelriou/mathlib4/blob/ea3a7bb9fb083d629e20759d2e85205cbfb10c1b/Mathlib/CategoryTheory/Presentable/Representation.lean#L180
• if C is an (essentially) w-small category and κ : Cardinal.{w} is a regular cardinal, then the full subcategory of Cᵒᵖ ⥤ Type w consisting of κ-continuous functors is locally κ-presentable (a functor is κ-continuous if it preserves limits indexed by categories J such that the cardinality of Arrow J is < κ https://github.com/joelriou/mathlib4/blob/ea3a7bb9fb083d629e20759d2e85205cbfb10c1b/Mathlib/CategoryTheory/Presentable/Continuous.lean#L211
• the representation theorem 1.46 ((i) ↔ (ii) ↔ (iii) ↔ (iv)), the most important part of which states that if C is locally κ-presentable, then C is equivalent to the category of κ-presheaves of types on the full subcategory of κ-presentable objects of C https://github.com/joelriou/mathlib4/blob/ea3a7bb9fb083d629e20759d2e85205cbfb10c1b/Mathlib/CategoryTheory/Presentable/Representation.lean#L165
• locally presentable categories have limits https://github.com/joelriou/mathlib4/blob/ea3a7bb9fb083d629e20759d2e85205cbfb10c1b/Mathlib/CategoryTheory/Presentable/Representation.lean#L189

The last PR #30847 is very much a draft, but the code standards are better in the other PRs in the series.
The adjoint functor theorem 1.66 regarding locally presentable categories should be made easier using part of these results.

[Dagur Asgeirsson]

Very nice! Thank you for all this work. Maybe we can use this thread to keep track of which PRs in this series are ready for review/reviewed, etc?

[Joël Riou]

The PR that are currently ready for review are:

[Joël Riou]

• #30269 refactor(CategoryTheory/Generator): use ObjectProperty instead of Set

[Joël Riou]

• #29881: refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape

[Joël Riou]

• #30509: feat(CategoryTheory): LeftBousfield.W is stable under transfinite compositions

[Joël Riou]

• #30492: feat(CategoryTheory): the orthogonal-reflection construction

[Robin Carlier]

I have #30269 assigned and will have some free time either sunday or monday, I can review a few of the others as well if you assign me.

[Dagur Asgeirsson]

I finally got back to this today and proving the forward direction of theorem 1.66 wasn't too bad: #33110 (not ready for review)