feat(CategoryTheory): presentable objects and adjunctions

Mathlib.lean

@@ -2108,6 +2108,7 @@ import Mathlib.CategoryTheory.Adjunction.Parametrized
 import Mathlib.CategoryTheory.Adjunction.PartialAdjoint
 import Mathlib.CategoryTheory.Adjunction.Quadruple
 import Mathlib.CategoryTheory.Adjunction.Reflective
+import Mathlib.CategoryTheory.Adjunction.ReflectiveLimits
 import Mathlib.CategoryTheory.Adjunction.Restrict
 import Mathlib.CategoryTheory.Adjunction.Triple
 import Mathlib.CategoryTheory.Adjunction.Unique
@@ -2295,6 +2296,8 @@ import Mathlib.CategoryTheory.Functor.Functorial
 import Mathlib.CategoryTheory.Functor.Hom
 import Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
 import Mathlib.CategoryTheory.Functor.KanExtension.Basic
+import Mathlib.CategoryTheory.Functor.KanExtension.Dense
+import Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
 import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
 import Mathlib.CategoryTheory.Functor.KanExtension.Preserves
 import Mathlib.CategoryTheory.Functor.OfSequence
@@ -2320,6 +2323,7 @@ import Mathlib.CategoryTheory.Generator.Indization
 import Mathlib.CategoryTheory.Generator.Preadditive
 import Mathlib.CategoryTheory.Generator.Presheaf
 import Mathlib.CategoryTheory.Generator.Sheaf
+import Mathlib.CategoryTheory.Generator.StrongGenerator
 import Mathlib.CategoryTheory.GlueData
 import Mathlib.CategoryTheory.GradedObject
 import Mathlib.CategoryTheory.GradedObject.Associator
@@ -2680,6 +2684,7 @@ import Mathlib.CategoryTheory.Noetherian
 import Mathlib.CategoryTheory.ObjectProperty.Basic
 import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
 import Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
+import Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
 import Mathlib.CategoryTheory.ObjectProperty.ContainsZero
 import Mathlib.CategoryTheory.ObjectProperty.EpiMono
 import Mathlib.CategoryTheory.ObjectProperty.Extensions
@@ -2726,13 +2731,15 @@ import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
+import Mathlib.CategoryTheory.Presentable.Adjunction
 import Mathlib.CategoryTheory.Presentable.Basic
 import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
 import Mathlib.CategoryTheory.Presentable.ColimitPresentation
 import Mathlib.CategoryTheory.Presentable.Finite
 import Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
 import Mathlib.CategoryTheory.Presentable.Limits
 import Mathlib.CategoryTheory.Presentable.LocallyPresentable
+import Mathlib.CategoryTheory.Presentable.Retracts
 import Mathlib.CategoryTheory.Products.Associator
 import Mathlib.CategoryTheory.Products.Basic
 import Mathlib.CategoryTheory.Products.Bifunctor

Mathlib/Algebra/Category/ModuleCat/AB.lean

@@ -36,11 +36,11 @@ instance : AB4Star (ModuleCat.{u} R) where
 
 lemma ModuleCat.isSeparator [Small.{v} R] : IsSeparator (ModuleCat.of.{v} R (Shrink.{v} R)) :=
     fun X Y f g h ↦ by
-  simp only [Set.mem_singleton_iff, forall_eq, ModuleCat.hom_ext_iff, LinearMap.ext_iff] at h
+  simp only [ObjectProperty.singleton_iff, ModuleCat.hom_ext_iff, hom_comp,
+    LinearMap.ext_iff, LinearMap.coe_comp, Function.comp_apply, forall_eq'] at h
   ext x
-  simpa [Shrink.linearEquiv, Equiv.linearEquiv] using
-    h (ModuleCat.ofHom ((LinearMap.toSpanSingleton R X x).comp
-      (Shrink.linearEquiv R R : Shrink R →ₗ[R] R))) 1
+  simpa using h (ModuleCat.ofHom ((LinearMap.toSpanSingleton R X x).comp
+    (Shrink.linearEquiv R R : Shrink R →ₗ[R] R))) 1
 
 instance [Small.{v} R] : HasSeparator (ModuleCat.{v} R) where
   hasSeparator := ⟨ModuleCat.of R (Shrink.{v} R), ModuleCat.isSeparator R⟩

Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean

@@ -69,24 +69,23 @@ lemma freeYonedaEquiv_comp {M N : PresheafOfModules.{v} R} {X : C}
 variable (R) in
 /-- The set of `PresheafOfModules.{v} R` consisting of objects of the
 form `(free R).obj (yoneda.obj X)` for some `X`. -/
-def freeYoneda : Set (PresheafOfModules.{v} R) := Set.range (yoneda ⋙ free R).obj
+def freeYoneda : ObjectProperty (PresheafOfModules.{v} R) := .ofObj (yoneda ⋙ free R).obj
 
 namespace freeYoneda
 
-instance : Small.{u} (freeYoneda R) := by
-  let π : C → freeYoneda R := fun X ↦ ⟨_, ⟨X, rfl⟩⟩
-  have hπ : Function.Surjective π := by rintro ⟨_, ⟨X, rfl⟩⟩; exact ⟨X, rfl⟩
-  exact small_of_surjective hπ
+instance : ObjectProperty.Small.{u} (freeYoneda R) := by
+  dsimp [freeYoneda]
+  infer_instance
 
 variable (R)
 
-lemma isSeparating : IsSeparating (freeYoneda R) := by
+lemma isSeparating : ObjectProperty.IsSeparating (freeYoneda R) := by
   intro M N f₁ f₂ h
   ext ⟨X⟩ m
   obtain ⟨g, rfl⟩ := freeYonedaEquiv.surjective m
-  exact congr_arg freeYonedaEquiv (h _ ⟨X, rfl⟩ g)
+  exact congr_arg freeYonedaEquiv (h _ ⟨X⟩ g)
 
-lemma isDetecting : IsDetecting (freeYoneda R) :=
+lemma isDetecting : ObjectProperty.IsDetecting (freeYoneda R) :=
   (isSeparating R).isDetecting
 
 end freeYoneda

Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean

@@ -111,8 +111,8 @@ lemma exists_pushouts
     ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : (generatingMonomorphisms G).pushouts i)
       (_ : ¬ IsIso i) (_ : Mono p'), i ≫ p' = p := by
   rw [hG.isDetector.isIso_iff_of_mono] at hp
-  simp only [coyoneda_obj_obj, coyoneda_obj_map, Set.mem_singleton_iff, forall_eq,
-    Function.Surjective, not_forall, not_exists] at hp
+  simp only [ObjectProperty.singleton_iff, Function.Surjective, coyoneda_obj_obj,
+    coyoneda_obj_map, forall_eq', not_forall, not_exists] at hp
   -- `f : G ⟶ Y` is a monomorphism the image of which is not contained in `X`
   obtain ⟨f, hf⟩ := hp
   -- we use the subobject `X'` of `Y` that is generated by the images of `p : X ⟶ Y`

Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean

@@ -40,7 +40,7 @@ namespace CategoryTheory.IsGrothendieckAbelian
 variable {C : Type u} [Category.{v} C] [Abelian C] [IsGrothendieckAbelian.{v} C]
 
 instance {G : C} : (preadditiveCoyonedaObj G).IsRightAdjoint :=
-  isRightAdjoint_of_preservesLimits_of_isCoseparating (isCoseparator_coseparator _) _
+  isRightAdjoint_of_preservesLimits_of_isCoseparating.{v} (isCoseparator_coseparator _) _
 
 /-- The left adjoint of the functor `Hom(G, ·)`, which can be thought of as `· ⊗ G`. -/
 noncomputable def tensorObj (G : C) : ModuleCat (End G)ᵐᵒᵖ ⥤ C :=

Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean

@@ -101,20 +101,22 @@ variable {D : Type u'} [Category.{v} D]
 well-powered and has a small coseparating set, then `G` has a left adjoint.
 -/
 lemma isRightAdjoint_of_preservesLimits_of_isCoseparating [HasLimits D] [WellPowered.{v} D]
-    {𝒢 : Set D} [Small.{v} 𝒢] (h𝒢 : IsCoseparating 𝒢) (G : D ⥤ C) [PreservesLimits G] :
-    G.IsRightAdjoint :=
-  have : ∀ A, HasInitial (StructuredArrow A G) := fun A =>
-    hasInitial_of_isCoseparating (StructuredArrow.isCoseparating_proj_preimage A G h𝒢)
-  isRightAdjointOfStructuredArrowInitials _
+    {P : ObjectProperty D} [ObjectProperty.Small.{v} P]
+    (hP : P.IsCoseparating) (G : D ⥤ C) [PreservesLimits G] :
+    G.IsRightAdjoint := by
+  have : ∀ A, HasInitial (StructuredArrow A G) := fun A ↦
+    hasInitial_of_isCoseparating (StructuredArrow.isCoseparating_inverseImage_proj A G hP)
+  exact isRightAdjointOfStructuredArrowInitials _
 
 /-- 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.
 -/
 lemma isLeftAdjoint_of_preservesColimits_of_isSeparating [HasColimits C] [WellPowered.{v} Cᵒᵖ]
-    {𝒢 : Set C} [Small.{v} 𝒢] (h𝒢 : IsSeparating 𝒢) (F : C ⥤ D) [PreservesColimits F] :
+    {P : ObjectProperty C} [ObjectProperty.Small.{v} P]
+    (h𝒢 : P.IsSeparating) (F : C ⥤ D) [PreservesColimits F] :
     F.IsLeftAdjoint :=
   have : ∀ A, HasTerminal (CostructuredArrow F A) := fun A =>
-    hasTerminal_of_isSeparating (CostructuredArrow.isSeparating_proj_preimage F A h𝒢)
+    hasTerminal_of_isSeparating (CostructuredArrow.isSeparating_inverseImage_proj F A h𝒢)
   isLeftAdjoint_of_costructuredArrowTerminals _
 
 end SpecialAdjointFunctorTheorem
@@ -123,19 +125,19 @@ namespace Limits
 
 /-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
     has a small coseparating set, then it is cocomplete. -/
-theorem hasColimits_of_hasLimits_of_isCoseparating [HasLimits C] [WellPowered.{v} C] {𝒢 : Set C}
-    [Small.{v} 𝒢] (h𝒢 : IsCoseparating 𝒢) : HasColimits C :=
+theorem hasColimits_of_hasLimits_of_isCoseparating [HasLimits C] [WellPowered.{v} C]
+    {P : ObjectProperty C} [ObjectProperty.Small.{v} P] (hP : P.IsCoseparating) : HasColimits C :=
   { has_colimits_of_shape := fun _ _ =>
       hasColimitsOfShape_iff_isRightAdjoint_const.2
-        (isRightAdjoint_of_preservesLimits_of_isCoseparating h𝒢 _) }
+        (isRightAdjoint_of_preservesLimits_of_isCoseparating hP _) }
 
 /-- A consequence of the special adjoint functor theorem: if `C` is cocomplete, well-copowered and
     has a small separating set, then it is complete. -/
-theorem hasLimits_of_hasColimits_of_isSeparating [HasColimits C] [WellPowered.{v} Cᵒᵖ] {𝒢 : Set C}
-    [Small.{v} 𝒢] (h𝒢 : IsSeparating 𝒢) : HasLimits C :=
+theorem hasLimits_of_hasColimits_of_isSeparating [HasColimits C] [WellPowered.{v} Cᵒᵖ]
+    {P : ObjectProperty C} [ObjectProperty.Small.{v} P] (hP : P.IsSeparating) : HasLimits C :=
   { has_limits_of_shape := fun _ _ =>
       hasLimitsOfShape_iff_isLeftAdjoint_const.2
-        (isLeftAdjoint_of_preservesColimits_of_isSeparating h𝒢 _) }
+        (isLeftAdjoint_of_preservesColimits_of_isSeparating hP _) }
 
 /-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
     has a separator, then it is complete. -/

Mathlib/CategoryTheory/Adjunction/Basic.lean

@@ -78,7 +78,7 @@ namespace CategoryTheory
 open Category Functor
 
 -- declare the `v`'s first; see `CategoryTheory.Category` for an explanation
-universe v₁ v₂ v₃ u₁ u₂ u₃
+universe w v₁ v₂ v₃ u₁ u₂ u₃
 
 variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
 
@@ -498,6 +498,16 @@ def compCoyonedaIso {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Categor
     F.op ⋙ coyoneda ≅ coyoneda ⋙ (whiskeringLeft _ _ _).obj G :=
   NatIso.ofComponents fun X => NatIso.ofComponents fun Y => (adj.homEquiv X.unop Y).toIso
 
+/-- The isomorpism which an adjunction `F ⊣ G` induces on `F.op ⋙ uliftCoyoneda`.
+This states that `Adjunction.homEquiv` is natural in both arguments. -/
+@[simps!]
+def compUliftCoyonedaIso (adj : F ⊣ G) :
+    F.op ⋙ uliftCoyoneda.{max w v₁} ≅
+      uliftCoyoneda.{max w v₂} ⋙ (whiskeringLeft _ _ _).obj G :=
+  NatIso.ofComponents (fun X ↦ NatIso.ofComponents
+    (fun Y ↦ (Equiv.ulift.trans
+      ((adj.homEquiv X.unop Y).trans Equiv.ulift.symm)).toIso))
+
 section
 
 variable {E : Type u₃} [ℰ : Category.{v₃} E] {H : D ⥤ E} {I : E ⥤ D}

Mathlib/CategoryTheory/Adjunction/ReflectiveLimits.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Adjunction.FullyFaithful
+import Mathlib.CategoryTheory.Adjunction.Limits
+
+/-!
+# Existence of limits deduced from adjunctions
+
+Let `adj : F ⊣ G` be an adjunction.
+
+If `G : D ⥤ C` is fully faithful (i.e. `G` is reflective),
+then colimits of shape `J` exist in `D` if they exist in `C`.
+
+If `F : C ⥤ D` is fully faithful (i.e. `F` is coreflective),
+then limits of shape `J` exist in `C` if they exist in `D`.
+
+-/
+
+namespace CategoryTheory.Adjunction
+
+open Limits Functor
+
+variable {C D : Type*} [Category C] [Category D]
+  {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)
+
+include adj
+
+lemma hasColimitsOfShape [G.Full] [G.Faithful]
+    (J : Type*) [Category J] [HasColimitsOfShape J C] :
+    HasColimitsOfShape J D where
+  has_colimit K := by
+    have := adj.isLeftAdjoint
+    exact ⟨_, (IsColimit.precomposeInvEquiv
+      (associator _ _ _ ≪≫ isoWhiskerLeft _ (asIso adj.counit) ≪≫ rightUnitor _) _).2
+      (isColimitOfPreserves F (colimit.isColimit (K ⋙ G)))⟩
+
+lemma hasLimitsOfShape [F.Full] [F.Faithful]
+    (J : Type*) [Category J] [HasLimitsOfShape J D] :
+    HasLimitsOfShape J C where
+  has_limit K := by
+    have := adj.isRightAdjoint
+    exact ⟨_, (IsLimit.postcomposeHomEquiv
+      ((associator _ _ _ ≪≫ isoWhiskerLeft _ (asIso adj.unit).symm ≪≫ rightUnitor K)) _).2
+        (isLimitOfPreserves G (limit.isLimit (K ⋙ F)))⟩
+
+end CategoryTheory.Adjunction

Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean

@@ -5,7 +5,7 @@ Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
 import Mathlib.CategoryTheory.EssentiallySmall
-import Mathlib.Logic.Small.Set
+import Mathlib.CategoryTheory.ObjectProperty.Small
 
 /-!
 # Small sets in the category of structured arrows
@@ -17,34 +17,59 @@ be used in the proof of the Special Adjoint Functor Theorem.
 namespace CategoryTheory
 
 -- morphism levels before object levels. See note [category theory universes].
-universe v₁ v₂ u₁ u₂
+universe w v₁ v₂ u₁ u₂
 
 variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
 
 namespace StructuredArrow
 
 variable {S : D} {T : C ⥤ D}
 
-instance small_proj_preimage_of_locallySmall {𝒢 : Set C} [Small.{v₁} 𝒢] [LocallySmall.{v₁} D] :
-    Small.{v₁} ((proj S T).obj ⁻¹' 𝒢) := by
-  suffices (proj S T).obj ⁻¹' 𝒢 = Set.range fun f : Σ G : 𝒢, S ⟶ T.obj G => mk f.2 by
+instance [Small.{w} C] [LocallySmall.{w} D] : Small.{w} (StructuredArrow S T) :=
+  small_of_surjective (f := fun (f : Σ (X : C), S ⟶ T.obj X) ↦ StructuredArrow.mk f.2)
+    (fun f ↦ by
+      obtain ⟨X, f, rfl⟩ := f.mk_surjective
+      exact ⟨⟨X, f⟩, rfl⟩)
+
+instance small_inverseImage_proj_of_locallySmall
+    {P : ObjectProperty C} [ObjectProperty.Small.{v₁} P] [LocallySmall.{v₁} D] :
+    ObjectProperty.Small.{v₁} (P.inverseImage (proj S T)) := by
+  suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S ⟶ T.obj G => mk f.2 by
     rw [this]
     infer_instance
-  exact Set.ext fun X => ⟨fun h => ⟨⟨⟨_, h⟩, X.hom⟩, (eq_mk _).symm⟩, by cat_disch⟩
+  ext X
+  simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff,
+    Sigma.exists, Subtype.exists, exists_prop]
+  exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩
+
+@[deprecated (since := "2025-10-07")] alias small_proj_preimage_of_locallySmall :=
+  small_inverseImage_proj_of_locallySmall
 
 end StructuredArrow
 
 namespace CostructuredArrow
 
 variable {S : C ⥤ D} {T : D}
 
-instance small_proj_preimage_of_locallySmall {𝒢 : Set C} [Small.{v₁} 𝒢] [LocallySmall.{v₁} D] :
-    Small.{v₁} ((proj S T).obj ⁻¹' 𝒢) := by
-  suffices (proj S T).obj ⁻¹' 𝒢 = Set.range fun f : Σ G : 𝒢, S.obj G ⟶ T => mk f.2 by
+instance [Small.{w} C] [LocallySmall.{w} D] : Small.{w} (CostructuredArrow S T) :=
+  small_of_surjective (f := fun (f : Σ (X : C), S.obj X ⟶ T) ↦ CostructuredArrow.mk f.2)
+    (fun f ↦ by
+      obtain ⟨X, f, rfl⟩ := f.mk_surjective
+      exact ⟨⟨X, f⟩, rfl⟩)
+
+instance small_inverseImage_proj_of_locallySmall
+    {P : ObjectProperty C} [ObjectProperty.Small.{v₁} P] [LocallySmall.{v₁} D] :
+    ObjectProperty.Small.{v₁} (P.inverseImage (proj S T)) := by
+  suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S.obj G ⟶ T => mk f.2 by
     rw [this]
     infer_instance
-  exact Set.ext fun X => ⟨fun h => ⟨⟨⟨_, h⟩, X.hom⟩, (eq_mk _).symm⟩, by cat_disch⟩
+  ext X
+  simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff,
+    Sigma.exists, Subtype.exists, exists_prop]
+  exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩
 
+@[deprecated (since := "2025-10-07")] alias small_proj_preimage_of_locallySmall :=
+  small_inverseImage_proj_of_locallySmall
 end CostructuredArrow
 
 end CategoryTheory