feat(CategoryTheory/Presentable): accessible functors satisfy the solution set condition

Mathlib.lean

@@ -3275,19 +3275,25 @@ public import Mathlib.CategoryTheory.Presentable.Basic
 public import Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
 public import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
 public import Mathlib.CategoryTheory.Presentable.ColimitPresentation
+public import Mathlib.CategoryTheory.Presentable.Comma
 public import Mathlib.CategoryTheory.Presentable.Dense
 public import Mathlib.CategoryTheory.Presentable.Directed
 public import Mathlib.CategoryTheory.Presentable.EssentiallyLarge
 public import Mathlib.CategoryTheory.Presentable.Finite
 public import Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
+public import Mathlib.CategoryTheory.Presentable.IsDiscrete
 public import Mathlib.CategoryTheory.Presentable.Limits
 public import Mathlib.CategoryTheory.Presentable.LocallyPresentable
 public import Mathlib.CategoryTheory.Presentable.OrthogonalReflection
+public import Mathlib.CategoryTheory.Presentable.PreservesCardinalPresentable
 public import Mathlib.CategoryTheory.Presentable.Presheaf
 public import Mathlib.CategoryTheory.Presentable.Retracts
 public import Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
+public import Mathlib.CategoryTheory.Presentable.SharplyLT.Lemmas
+public import Mathlib.CategoryTheory.Presentable.SolutionSetCondition
 public import Mathlib.CategoryTheory.Presentable.StrongGenerator
 public import Mathlib.CategoryTheory.Presentable.Type
+public import Mathlib.CategoryTheory.Presentable.Uniformization
 public import Mathlib.CategoryTheory.Products.Associator
 public import Mathlib.CategoryTheory.Products.Basic
 public import Mathlib.CategoryTheory.Products.Bifunctor

Mathlib/CategoryTheory/Comma/CardinalArrow.lean

@@ -5,10 +5,8 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.CategoryTheory.Comma.Arrow
-public import Mathlib.CategoryTheory.FinCategory.Basic
 public import Mathlib.CategoryTheory.EssentiallySmall
-public import Mathlib.Data.Set.Finite.Basic
+public import Mathlib.CategoryTheory.FinCategory.Basic
 public import Mathlib.SetTheory.Cardinal.HasCardinalLT
 
 /-!
@@ -114,4 +112,13 @@ lemma hasCardinalLT_of_hasCardinalLT_arrow
     HasCardinalLT C κ :=
   h.of_injective (fun X ↦ Arrow.mk (𝟙 X)) (fun _ _ h ↦ congr_arg Comma.left h)
 
+lemma hasCardinalLT_arrow_iff_of_isThin (C : Type u) [Category.{v} C]
+    [Quiver.IsThin C] (κ : Cardinal.{w}) (hκ : Cardinal.aleph0 ≤ κ) :
+    HasCardinalLT (Arrow C) κ ↔ HasCardinalLT C κ :=
+  ⟨hasCardinalLT_of_hasCardinalLT_arrow, fun h ↦
+    (hasCardinalLT_prod hκ h h).of_injective (fun f ↦ (f.left, f.right))
+      (fun f g h ↦
+        Arrow.ext (congr_arg _root_.Prod.fst h) (congr_arg _root_.Prod.snd h)
+          (by subsingleton))⟩
+
 end CategoryTheory

Mathlib/CategoryTheory/EssentiallySmall.lean

@@ -25,7 +25,6 @@ the type `Skeleton C` is `w`-small, and `C` is `w`-locally small.
 
 @[expose] public section
 
-
 universe w w' v v' u u'
 
 open CategoryTheory

Mathlib/CategoryTheory/Limits/Comma.lean

@@ -71,25 +71,39 @@ noncomputable def coneOfPreserves [PreservesLimit (F ⋙ snd L R) R] (c₁ : Con
         · simp [← c₁.w t]
         · simp [← c₂.w t] }
 
-set_option backward.isDefEq.respectTransparency false in
+set_option backward.defeqAttrib.useBackward true in
+/-- Let `F : J ⥤ Comma L R`. If `R` preserves the limit of
+`F ⋙ snd _ _`, then `Comma.fst L R` and `Comma.snd L R` jointly
+reflect the limit of `F`, i.e. if `c` is a cone for `F` which
+becomes a limit after applying `Comma.fst L R` and `Comma.snd L R`,
+then `c` is a limit. -/
+def fstSndJointlyReflectLimit {F : J ⥤ Comma L R} {c : Cone F}
+    [PreservesLimit (F ⋙ snd _ _) R]
+    (h₁ : IsLimit ((fst _ _).mapCone c))
+    (h₂ : IsLimit ((snd _ _).mapCone c)) :
+    IsLimit c where
+  lift s :=
+    { left := h₁.lift ((fst _ _).mapCone s)
+      right := h₂.lift ((snd _ _).mapCone s)
+      w := (isLimitOfPreserves R h₂).hom_ext (fun j ↦ by
+        simp [← Functor.map_comp, ← Functor.map_comp_assoc, ← CommaMorphism.w,
+          dsimp% h₂.fac ((snd _ _).mapCone s) j,
+          dsimp% h₁.fac ((fst _ _).mapCone s) j]) }
+  fac s j := by
+    ext
+    · exact h₁.fac ((fst _ _).mapCone s) j
+    · exact h₂.fac ((snd _ _).mapCone s) j
+  uniq s _ hm := by
+    ext
+    · exact h₁.uniq ((fst _ _).mapCone s) _ (by simp [← hm])
+    · exact h₂.uniq ((snd _ _).mapCone s) _ (by simp [← hm])
+
 /-- Provided that `R` preserves the appropriate limit, then the cone in `coneOfPreserves` is a
 limit. -/
 noncomputable def coneOfPreservesIsLimit [PreservesLimit (F ⋙ snd L R) R] {c₁ : Cone (F ⋙ fst L R)}
     (t₁ : IsLimit c₁) {c₂ : Cone (F ⋙ snd L R)} (t₂ : IsLimit c₂) :
-    IsLimit (coneOfPreserves F c₁ t₂) where
-  lift s :=
-    { left := t₁.lift ((fst L R).mapCone s)
-      right := t₂.lift ((snd L R).mapCone s)
-      w :=
-        (isLimitOfPreserves R t₂).hom_ext fun j => by
-          rw [coneOfPreserves_pt_hom, assoc, assoc, (isLimitOfPreserves R t₂).fac,
-            limitAuxiliaryCone_π_app, ← L.map_comp_assoc, t₁.fac, R.mapCone_π_app,
-            ← R.map_comp, t₂.fac]
-          exact (s.π.app j).w }
-  uniq s m w := by
-    apply CommaMorphism.ext
-    · exact t₁.uniq ((fst L R).mapCone s) _ (fun j => by simp [← w])
-    · exact t₂.uniq ((snd L R).mapCone s) _ (fun j => by simp [← w])
+    IsLimit (coneOfPreserves F c₁ t₂) :=
+  fstSndJointlyReflectLimit t₁ t₂
 
 /-- (Implementation). An auxiliary cocone which is useful in order to construct colimits
 in the comma category. -/
@@ -120,26 +134,40 @@ noncomputable def coconeOfPreserves [PreservesColimit (F ⋙ fst L R) L] {c₁ :
         · simp [← c₁.w t]
         · simp [← c₂.w t] }
 
-set_option backward.isDefEq.respectTransparency false in
+set_option backward.defeqAttrib.useBackward true in
+/-- Let `F : J ⥤ Comma L R`. If `L` preserves the colimit of
+`F ⋙ fst _ _`, then `Comma.fst L R` and `Comma.snd L R` jointly
+reflect the colimit of `F`, i.e. if `c` is a cocone for `F` which
+becomes a colimit after applying `Comma.fst L R` and `Comma.snd L R`,
+then `c` is a colimit. -/
+def fstSndJointlyReflectColimit {F : J ⥤ Comma L R} {c : Cocone F}
+    [PreservesColimit (F ⋙ fst _ _) L]
+    (h₁ : IsColimit ((fst _ _).mapCocone c))
+    (h₂ : IsColimit ((snd _ _).mapCocone c)) :
+    IsColimit c where
+  desc s :=
+    { left := h₁.desc ((fst _ _).mapCocone s)
+      right := h₂.desc ((snd _ _).mapCocone s)
+      w := (isColimitOfPreserves L h₁).hom_ext (fun j ↦ by
+        simp [← Functor.map_comp_assoc, ← Functor.map_comp,
+          dsimp% h₁.fac ((fst _ _).mapCocone s) j,
+          dsimp% h₂.fac ((snd _ _).mapCocone s) j]) }
+  fac s j := by
+    ext
+    · exact h₁.fac ((fst _ _).mapCocone s) j
+    · exact h₂.fac ((snd _ _).mapCocone s) j
+  uniq s _ hm := by
+    ext
+    · exact h₁.uniq ((fst _ _).mapCocone s) _ (by simp [← hm])
+    · exact h₂.uniq ((snd _ _).mapCocone s) _ (by simp [← hm])
+
 /-- Provided that `L` preserves the appropriate colimit, then the cocone in `coconeOfPreserves` is
 a colimit. -/
 noncomputable def coconeOfPreservesIsColimit [PreservesColimit (F ⋙ fst L R) L]
     {c₁ : Cocone (F ⋙ fst L R)}
     (t₁ : IsColimit c₁) {c₂ : Cocone (F ⋙ snd L R)} (t₂ : IsColimit c₂) :
-    IsColimit (coconeOfPreserves F t₁ c₂) where
-  desc s :=
-    { left := t₁.desc ((fst L R).mapCocone s)
-      right := t₂.desc ((snd L R).mapCocone s)
-      w :=
-        (isColimitOfPreserves L t₁).hom_ext fun j => by
-          rw [coconeOfPreserves_pt_hom, (isColimitOfPreserves L t₁).fac_assoc,
-            colimitAuxiliaryCocone_ι_app, assoc, ← R.map_comp, t₂.fac, L.mapCocone_ι_app, ←
-            L.map_comp_assoc, t₁.fac]
-          exact (s.ι.app j).w }
-  uniq s m w := by
-    apply CommaMorphism.ext
-    · exact t₁.uniq ((fst L R).mapCocone s) _ (fun j => by simp [← w])
-    · exact t₂.uniq ((snd L R).mapCocone s) _ (fun j => by simp [← w])
+    IsColimit (coconeOfPreserves F t₁ c₂) :=
+  fstSndJointlyReflectColimit t₁ t₂
 
 instance hasLimit (F : J ⥤ Comma L R) [HasLimit (F ⋙ fst L R)] [HasLimit (F ⋙ snd L R)]
     [PreservesLimit (F ⋙ snd L R) R] : HasLimit F :=

Mathlib/CategoryTheory/ObjectProperty/Small.lean

@@ -41,6 +41,17 @@ lemma Small.of_le {P Q : ObjectProperty C} [ObjectProperty.Small.{w} Q] (h : P 
     ObjectProperty.Small.{w} P :=
   small_of_injective (Subtype.map_injective h Function.injective_id)
 
+lemma Small.exists_eq_ofObj (P : ObjectProperty C) [ObjectProperty.Small.{w} P] :
+    ∃ (ι : Type w) (X : ι → C), P = .ofObj X :=
+  ⟨Shrink.{w} (Subtype P), fun i ↦ ((equivShrink _).symm i).val,
+    le_antisymm (fun X hX ↦ by
+      rw [ofObj_iff]
+      exact ⟨equivShrink _ ⟨X, hX⟩, by simp⟩) (by
+      rw [ofObj_le_iff]
+      intro i
+      obtain ⟨X, rfl⟩ := (equivShrink _).surjective i
+      simpa using X.prop)⟩
+
 instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] :
     ObjectProperty.Small.{w} P.op :=
   small_of_injective P.subtypeOpEquiv.injective
@@ -141,6 +152,14 @@ lemma EssentiallySmall.exists_small (P : ObjectProperty C) [P.IsClosedUnderIsomo
   obtain ⟨Q, _, hQ₁, hQ₂⟩ := exists_small_le P
   exact ⟨Q, inferInstance, le_antisymm hQ₂ (by rwa [isoClosure_le_iff])⟩
 
+lemma EssentiallySmall.exists_eq_isoClosure_ofObj
+    (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms]
+    [ObjectProperty.EssentiallySmall.{w} P] :
+    ∃ (ι : Type w) (X : ι → C), P = (ObjectProperty.ofObj X).isoClosure := by
+  obtain ⟨P₀, _, h⟩ := exists_small.{w} P
+  obtain ⟨ι, X, rfl⟩ := Small.exists_eq_ofObj.{w} P₀
+  exact ⟨ι, X, h⟩
+
 lemma EssentiallySmall.of_le {P Q : ObjectProperty C}
     [ObjectProperty.EssentiallySmall.{w} Q] (h : P ≤ Q) :
     ObjectProperty.EssentiallySmall.{w} P where

Mathlib/CategoryTheory/Presentable/Basic.lean

@@ -5,12 +5,8 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.CategoryTheory.Adjunction.Limits
 public import Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
-public import Mathlib.CategoryTheory.Limits.Preserves.Ulift
-public import Mathlib.CategoryTheory.Limits.Types.Filtered
 public import Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
-public import Mathlib.SetTheory.Cardinal.HasCardinalLT
 
 /-! # Presentable objects
 
@@ -22,7 +18,7 @@ a regular cardinal `κ` such that `Functor.IsCardinalAccessible`.
 
 An object `X` of a category is `κ`-presentable (`IsCardinalPresentable`)
 if the functor `Hom(X, _)` (i.e. `coyoneda.obj (op X)`) is `κ`-accessible.
-Similarly as for accessible functors, we define a type class `IsAccessible`.
+Similarly as for accessible functors, we define a type class `IsPresentable`.
 
 ## References
 * [Adámek, J. and Rosický, J., *Locally presentable and accessible categories*][Adamek_Rosicky_1994]
@@ -110,18 +106,21 @@ end
 
 section
 
-variable (F : C ⥤ D)
-
 /-- A functor is accessible relative to a universe `w` if
 it is `κ`-accessible for some regular `κ : Cardinal.{w}`. -/
 @[pp_with_univ]
-class IsAccessible : Prop where
-  exists_cardinal : ∃ (κ : Cardinal.{w}) (_ : Fact κ.IsRegular), IsCardinalAccessible F κ
+class IsAccessible (F : C ⥤ D) : Prop where
+  exists_cardinal (F) : ∃ (κ : Cardinal.{w}) (_ : Fact κ.IsRegular), IsCardinalAccessible F κ
+
+variable (F : C ⥤ D)
 
 lemma isAccessible_of_isCardinalAccessible (κ : Cardinal.{w}) [Fact κ.IsRegular]
     [IsCardinalAccessible F κ] : IsAccessible.{w} F where
   exists_cardinal := ⟨κ, inferInstance, inferInstance⟩
 
+instance : IsAccessible.{w} (𝟭 C) :=
+  ⟨.aleph0, Cardinal.fact_isRegular_aleph0, inferInstance⟩
+
 instance {E : Type u₃} [Category.{v₃} E] (F : C ⥤ D) (G : D ⥤ E) [IsAccessible.{w} F]
     [IsAccessible.{w} G] : IsAccessible.{w} (F ⋙ G) := by
   obtain ⟨κF, _, _⟩ := IsAccessible.exists_cardinal (F := F)
@@ -150,7 +149,7 @@ abbrev IsCardinalPresentable : Prop := (coyoneda.obj (op X)).IsCardinalAccessibl
 
 variable (C) in
 /-- The property of objects that are `κ`-presentable. -/
-def isCardinalPresentable : ObjectProperty C := fun X ↦ IsCardinalPresentable X κ
+abbrev isCardinalPresentable : ObjectProperty C := fun X ↦ IsCardinalPresentable X κ
 
 instance (X : (isCardinalPresentable C κ).FullSubcategory) :
     IsCardinalPresentable X.obj κ :=
@@ -237,6 +236,33 @@ lemma isCardinalPresentable_iff_of_isEquivalence
   · intro
     infer_instance
 
+variable {X κ} in
+set_option backward.isDefEq.respectTransparency false in
+set_option backward.defeqAttrib.useBackward true in
+open IsFiltered in
+lemma IsCardinalPresentable.mk
+    (hX : ∀ (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ]
+      (F : J ⥤ C) (c : Cocone F) (_ : IsColimit c),
+      (∀ (g : X ⟶ c.pt), ∃ (j : J) (f : X ⟶ F.obj j), f ≫ c.ι.app j = g) ∧
+      (∀ (j : J) (f₁ f₂ : X ⟶ F.obj j) (_ : f₁ ≫ c.ι.app j = f₂ ≫ c.ι.app j),
+        ∃ (j' : J) (a : j ⟶ j'), f₁ ≫ F.map a = f₂ ≫ F.map a)) :
+    IsCardinalPresentable X κ where
+  preservesColimitOfShape J _ _ :=
+    ⟨fun {F} ↦ ⟨fun {c} hc ↦ by
+      have := isFiltered_of_isCardinalFiltered J κ
+      rw [Types.isColimit_iff_coconeTypesIsColimit]
+      refine ⟨fun f₁ f₂ hf ↦ ?_, fun g ↦ ?_⟩
+      · obtain ⟨j₁, f₁, rfl⟩ := Functor.ιColimitType_jointly_surjective _ f₁
+        obtain ⟨j₂, f₂, rfl⟩ := Functor.ιColimitType_jointly_surjective _ f₂
+        dsimp at f₁ f₂ hf
+        obtain ⟨j', a, ha⟩ := (hX J F c hc).2 _ (f₁ ≫ F.map (leftToMax j₁ j₂))
+          (f₂ ≫ F.map (rightToMax j₁ j₂)) (by simpa)
+        simp only [Category.assoc] at ha
+        exact Functor.ιColimitType_eq_of_map_eq_map _ _ _
+          (leftToMax j₁ j₂ ≫ a) (rightToMax j₁ j₂ ≫ a) (by simpa)
+      · obtain ⟨j, f, rfl⟩ := (hX J F c hc).1 g
+        exact ⟨Functor.ιColimitType _ j f, rfl⟩⟩⟩
+
 section
 
 variable {J : Type*} [Category* J] {D : J ⥤ C}
@@ -344,18 +370,27 @@ end
 
 section
 
-variable (C) (κ : Cardinal.{w}) [Fact κ.IsRegular]
-
 /-- A category has `κ`-filtered colimits if it has colimits of shape `J`
 for any `κ`-filtered category `J`. -/
-class HasCardinalFilteredColimits : Prop where
-  hasColimitsOfShape (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] :
+class HasCardinalFilteredColimits
+    (C : Type u₁) [Category.{v₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : Prop where
+  hasColimitsOfShape (C) (κ) (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] :
     HasColimitsOfShape J C := by intros; infer_instance
 
 attribute [instance] HasCardinalFilteredColimits.hasColimitsOfShape
 
+variable (C) (κ : Cardinal.{w}) [Fact κ.IsRegular]
+
 instance [HasColimitsOfSize.{w, w} C] : HasCardinalFilteredColimits.{w} C κ where
 
+variable {κ} in
+lemma HasCardinalFilteredColimits.of_le
+    [HasCardinalFilteredColimits C κ] {κ' : Cardinal.{w}} [Fact κ'.IsRegular] (h : κ ≤ κ') :
+    HasCardinalFilteredColimits C κ' where
+  hasColimitsOfShape J _ _ := by
+    have := IsCardinalFiltered.of_le J h
+    exact HasCardinalFilteredColimits.hasColimitsOfShape C κ J
+
 end
 
 end CategoryTheory

Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean

@@ -5,10 +5,9 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.CategoryTheory.ObjectProperty.Small
+public import Mathlib.CategoryTheory.Generator.StrongGenerator
 public import Mathlib.CategoryTheory.Presentable.Limits
 public import Mathlib.CategoryTheory.Presentable.Retracts
-public import Mathlib.CategoryTheory.Generator.StrongGenerator
 
 /-!
 # Presentable generators
@@ -33,14 +32,18 @@ such that `P.IsCardinalFilteredGenerator κ` holds.
 
 public section
 
-universe w v u
+universe w₁ w₂ w v u
 
 namespace CategoryTheory
 
 variable {C : Type u} [Category.{v} C]
 
 namespace Limits.ColimitPresentation
 
+/-- If an object `X` admits a presentation `p` as a colimit of
+a functor `p.diag : J ⥤ C` with values in `κ`-presentable objects,
+then `X` is `κ'`-presentable if `κ ≤ κ'` and the cardinality
+of `Arrow J` is `< κ'`. -/
 lemma isCardinalPresentable {X : C} {J : Type w} [SmallCategory J]
     (p : ColimitPresentation J X) (κ : Cardinal.{w}) [Fact κ.IsRegular]
     (h : ∀ (j : J), IsCardinalPresentable (p.diag.obj j) κ) [LocallySmall.{w} C]
@@ -58,6 +61,11 @@ namespace ObjectProperty
 
 variable {P : ObjectProperty C}
 
+/-- If an object `X` admits a presentation `p : P.ColimitsOfShape J X`
+as a colimit of a functor `p.diag : J ⥤ C` with values in objects
+satisfying a property `P` such that `P ≤ isCardinalPresentable C κ`,
+then `X` is `κ'`-presentable if `κ ≤ κ'` and the cardinality
+of `Arrow J` is `< κ'`. -/
 lemma ColimitOfShape.isCardinalPresentable {X : C} {J : Type w} [SmallCategory J]
     (p : P.ColimitOfShape J X) {κ : Cardinal.{w}} [Fact κ.IsRegular]
     (hP : P ≤ isCardinalPresentable C κ) [LocallySmall.{w} C]
@@ -83,6 +91,17 @@ structure IsCardinalFilteredGenerator : Prop where
 
 namespace IsCardinalFilteredGenerator
 
+lemma mk' (h₁ : P ≤ isCardinalPresentable C κ)
+    (h₂ : ∀ (X : C), ∃ (J : Type w₁) (_ : Category.{w₂} J)
+      (_ : EssentiallySmall.{w} J) (_ : IsCardinalFiltered J κ), P.colimitsOfShape J X) :
+    P.IsCardinalFilteredGenerator κ where
+  le_isCardinalPresentable := h₁
+  exists_colimitsOfShape X := by
+    obtain ⟨J, _, _, _, p⟩ := h₂ X
+    exact ⟨SmallModel.{w} J, inferInstance,
+      IsCardinalFiltered.of_equivalence κ (equivSmallModel.{w} J),
+      by rwa [← P.colimitsOfShape_congr (equivSmallModel.{w} J)]⟩
+
 variable (h : P.IsCardinalFilteredGenerator κ) (X : C)
 
 include h in