feat(CategoryTheory): the κ-accessible category of κ-directed posets

Mathlib.lean

@@ -2314,6 +2314,7 @@ 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
@@ -2340,6 +2341,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
@@ -2711,11 +2713,13 @@ 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
 import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
 import Mathlib.CategoryTheory.ObjectProperty.Ind
+import Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
 import Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
 import Mathlib.CategoryTheory.ObjectProperty.Local
 import Mathlib.CategoryTheory.ObjectProperty.Opposite
@@ -2759,8 +2763,10 @@ import Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
 import Mathlib.CategoryTheory.Presentable.Basic
+import Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
 import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
 import Mathlib.CategoryTheory.Presentable.ColimitPresentation
+import Mathlib.CategoryTheory.Presentable.Directed
 import Mathlib.CategoryTheory.Presentable.Finite
 import Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
 import Mathlib.CategoryTheory.Presentable.Limits
@@ -5113,6 +5119,7 @@ import Mathlib.Order.Category.LinOrd
 import Mathlib.Order.Category.NonemptyFinLinOrd
 import Mathlib.Order.Category.OmegaCompletePartialOrder
 import Mathlib.Order.Category.PartOrd
+import Mathlib.Order.Category.PartOrdEmb
 import Mathlib.Order.Category.Preord
 import Mathlib.Order.Category.Semilat
 import Mathlib.Order.Chain

Mathlib/CategoryTheory/Comma/Arrow.lean

@@ -72,6 +72,10 @@ theorem mk_eq (f : Arrow T) : Arrow.mk f.hom = f := by
   cases f
   rfl
 
+lemma mk_surjective (f : Arrow T) :
+    ∃ (X Y : T) (g : X ⟶ Y), f = Arrow.mk g :=
+  ⟨_, _, f.hom, rfl⟩
+
 theorem mk_injective (A B : T) :
     Function.Injective (Arrow.mk : (A ⟶ B) → Arrow T) := fun f g h => by
   cases h

Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean

@@ -17,14 +17,20 @@ 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.{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
@@ -45,6 +51,12 @@ namespace CostructuredArrow
 
 variable {S : C ⥤ D} {T : D}
 
+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

Mathlib/CategoryTheory/Filtered/Final.lean

@@ -436,24 +436,22 @@ end Pi
 
 section Prod
 
-open IsFiltered in
-instance final_fst [IsFilteredOrEmpty C] [IsFiltered D] : (Prod.fst C D).Final := by
-  apply Functor.final_of_exists_of_isFiltered
-  · exact fun c => ⟨(c, nonempty.some), ⟨𝟙 c⟩⟩
-  · intro c ⟨c', d'⟩ f g
-    exact ⟨(coeq f g, d'), (coeqHom f g, 𝟙 d'), coeq_condition _ _⟩
+instance final_fst [IsFiltered D] : (Prod.fst C D).Final := by
+  let F : D ⥤ Discrete PUnit.{1} := (Functor.const _).obj (Discrete.mk .unit)
+  have hF : F.Final := Functor.final_of_isFiltered_of_pUnit _
+  change (Functor.prod (𝟭 C) F ⋙ (prod.rightUnitorEquivalence.{0} C).functor).Final
+  infer_instance
 
-instance final_snd [IsFiltered C] [IsFilteredOrEmpty D] : (Prod.snd C D).Final :=
+instance final_snd [IsFiltered C] : (Prod.snd C D).Final :=
   inferInstanceAs ((Prod.braiding C D).functor ⋙ Prod.fst D C).Final
 
-open IsCofiltered in
-instance initial_fst [IsCofilteredOrEmpty C] [IsCofiltered D] : (Prod.fst C D).Initial := by
-  apply Functor.initial_of_exists_of_isCofiltered
-  · exact fun c => ⟨(c, nonempty.some), ⟨𝟙 c⟩⟩
-  · intro c ⟨c', d'⟩ f g
-    exact ⟨(eq f g, d'), (eqHom f g, 𝟙 d'), eq_condition _ _⟩
+instance initial_fst [IsCofiltered D] : (Prod.fst C D).Initial := by
+  let F : D ⥤ Discrete PUnit.{1} := (Functor.const _).obj (Discrete.mk .unit)
+  have hF : F.Initial := Functor.initial_of_isCofiltered_pUnit _
+  change (Functor.prod (𝟭 C) F ⋙ (prod.rightUnitorEquivalence.{0} C).functor).Initial
+  infer_instance
 
-instance initial_snd [IsCofiltered C] [IsCofilteredOrEmpty D] : (Prod.snd C D).Initial :=
+instance initial_snd [IsCofiltered C] : (Prod.snd C D).Initial :=
   inferInstanceAs ((Prod.braiding C D).functor ⋙ Prod.fst D C).Initial
 
 end Prod

Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean

@@ -0,0 +1,124 @@
+/-
+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.Functor.KanExtension.DenseAt
+import Mathlib.CategoryTheory.Limits.Presheaf
+import Mathlib.CategoryTheory.Generator.StrongGenerator
+
+/-!
+# Dense functors
+
+A functor `F : C ⥤ D` is dense (`F.IsDense`) if `𝟭 D` is a pointwise
+left Kan extension of `F` along itself, i.e. any `Y : D` is the
+colimit of all `F.obj X` for all morphisms `F.obj X ⟶ Y` (which
+is the condition `F.DenseAt Y`).
+When `F` is full, we show that this
+is equivalent to saying that the restricted Yoneda functor
+`D ⥤ Cᵒᵖ ⥤ Type _` is fully faithful (see the lemma
+`Functor.isDense_iff_fullyFaithful_restrictedULiftYoneda`).
+
+We also show that the range of a dense functor is a strong
+generator (see `Functor.isStrongGenerator_of_isDense`).
+
+## References
+
+* https://ncatlab.org/nlab/show/dense+subcategory
+
+-/
+
+universe w v₁ v₂ u₁ u₂
+
+namespace CategoryTheory
+
+open Limits Opposite Presheaf
+
+variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D]
+
+namespace Functor
+
+/-- A functor `F : C ⥤ D` is dense if any `Y : D` is a canonical colimit
+relatively to `F`. -/
+class IsDense (F : C ⥤ D) : Prop where
+  isDenseAt (F) (Y : D) : F.isDenseAt Y
+
+/-- This is a choice of structure `F.DenseAt Y` when `F : C ⥤ D`
+is dense, and `Y : D`. -/
+noncomputable def denseAt (F : C ⥤ D) [F.IsDense] (Y : D) : F.DenseAt Y :=
+  (IsDense.isDenseAt F Y).some
+
+lemma isDense_iff_nonempty_isPointwiseLeftKanExtension (F : C ⥤ D) :
+    F.IsDense ↔
+      Nonempty ((LeftExtension.mk _ (rightUnitor F).inv).IsPointwiseLeftKanExtension) :=
+  ⟨fun _ ↦ ⟨fun _ ↦ F.denseAt _⟩, fun ⟨h⟩ ↦ ⟨fun _ ↦ ⟨h _⟩⟩⟩
+
+variable (F : C ⥤ D)
+
+instance [F.IsDense] : (restrictedULiftYoneda.{w} F).Faithful where
+  map_injective h :=
+    (F.denseAt _).hom_ext' (fun X p ↦ by
+      simpa using ULift.up_injective (congr_fun (NatTrans.congr_app h (op X)) (ULift.up p)))
+
+instance [F.IsDense] : (restrictedULiftYoneda.{w} F).Full where
+  map_surjective {Y Z} f := by
+    let c : Cocone (CostructuredArrow.proj F Y ⋙ F) :=
+      { pt := Z
+        ι :=
+          { app g := ((f.app (op g.left)) (ULift.up g.hom)).down
+            naturality g₁ g₂ φ := by
+              simpa [uliftFunctor, uliftYoneda,
+                restrictedULiftYoneda, ← ULift.down_inj] using
+                (congr_fun (f.naturality φ.left.op) (ULift.up g₂.hom)).symm }}
+    refine ⟨(F.denseAt Y).desc c, ?_⟩
+    ext ⟨X⟩ ⟨x⟩
+    have := (F.denseAt Y).fac c (.mk x)
+    dsimp [c] at this
+    simpa using ULift.down_injective this
+
+variable {F} in
+lemma IsDense.of_fullyFaithful_restrictedULiftYoneda [F.Full]
+    (h : (restrictedULiftYoneda.{w} F).FullyFaithful) :
+    F.IsDense where
+  isDenseAt Y := by
+    let φ (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) :
+        (restrictedULiftYoneda.{w} F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
+      { app := fun ⟨X⟩ ⟨x⟩ ↦ ULift.up (s.ι.app (.mk x))
+        naturality := by
+          rintro ⟨X₁⟩ ⟨X₂⟩ ⟨f⟩
+          ext ⟨x⟩
+          let α : CostructuredArrow.mk (F.map f ≫ x) ⟶ CostructuredArrow.mk x :=
+            CostructuredArrow.homMk f
+          simp [uliftYoneda, ← s.w α, α] }
+    have hφ (s) (j) : (restrictedULiftYoneda F).map j.hom ≫ φ s =
+        (restrictedULiftYoneda F).map (s.ι.app j) := by
+      ext ⟨X⟩ ⟨x⟩
+      let α : .mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x)
+      have := s.w α
+      dsimp [uliftYoneda, φ, α] at this ⊢
+      rw [← this, map_preimage]
+    exact
+      ⟨{desc s := (h.preimage (φ s))
+        fac s j := h.map_injective (by simp [hφ])
+        uniq s m hm := h.map_injective (by
+          ext ⟨X⟩ ⟨x⟩
+          simp [uliftYoneda, φ, ← hm])}⟩
+
+lemma isDense_iff_fullyFaithful_restrictedULiftYoneda [F.Full] :
+    F.IsDense ↔ Nonempty (restrictedULiftYoneda.{w} F).FullyFaithful :=
+  ⟨fun _ ↦ ⟨FullyFaithful.ofFullyFaithful _⟩,
+    fun ⟨h⟩ ↦ IsDense.of_fullyFaithful_restrictedULiftYoneda h⟩
+
+open ObjectProperty in
+lemma isStrongGenerator_of_isDense [F.IsDense] :
+    IsStrongGenerator (.ofObj F.obj) :=
+  (IsStrongGenerator.mk_of_exists_colimitsOfShape.{max u₁ u₂ v₁ v₂} (fun Y ↦ ⟨_, _, ⟨{
+    ι := _
+    diag := _
+    isColimit := (IsColimit.whiskerEquivalence (F.denseAt Y)
+      ((ShrinkHoms.equivalence _).symm.trans ((Shrink.equivalence _)).symm))
+    prop_diag_obj := by simp }⟩⟩))
+
+end Functor
+
+end CategoryTheory