feat(CategoryTheory): κ-continuous presheaves

Mathlib.lean

@@ -2885,6 +2885,7 @@ public import Mathlib.CategoryTheory.ObjectProperty.Equivalence
 public import Mathlib.CategoryTheory.ObjectProperty.Extensions
 public import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
 public import Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
+public import Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.Presheaf
 public import Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT
 public import Mathlib.CategoryTheory.ObjectProperty.Ind
 public import Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
@@ -2937,6 +2938,7 @@ public import Mathlib.CategoryTheory.Presentable.Adjunction
 public import Mathlib.CategoryTheory.Presentable.Basic
 public import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
 public import Mathlib.CategoryTheory.Presentable.ColimitPresentation
+public import Mathlib.CategoryTheory.Presentable.Continuous
 public import Mathlib.CategoryTheory.Presentable.Dense
 public import Mathlib.CategoryTheory.Presentable.Directed
 public import Mathlib.CategoryTheory.Presentable.EssentiallyLarge

Mathlib/CategoryTheory/Limits/Types/Limits.lean

@@ -35,6 +35,7 @@ def coneOfSection {s} (hs : s ∈ F.sections) : Cone F where
 
 /-- Given a cone over a functor F into `Type*` and an element in the cone point,
   construct a section of F. -/
+@[simps]
 def sectionOfCone (c : Cone F) (x : c.pt) : F.sections :=
   ⟨fun j ↦ c.π.app j x, fun f ↦ congr_fun (c.π.naturality f).symm x⟩
 

Mathlib/CategoryTheory/MorphismProperty/Basic.lean

@@ -214,6 +214,9 @@ lemma ofHoms_homFamily (P : MorphismProperty C) : ofHoms P.homFamily = P := by
   · intro hf
     exact ⟨(⟨f, hf⟩ : P.toSet)⟩
 
+/-- The class of morphisms containing a single morphism. -/
+abbrev single {X Y : C} (f : X ⟶ Y) : MorphismProperty C := .ofHoms (fun (_ : Unit) ↦ f)
+
 end
 
 section

Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean

@@ -60,6 +60,18 @@ lemma isSmall_iff_eq_ofHoms :
   · rintro ⟨_, _, _, _, rfl⟩
     infer_instance
 
+lemma iSup_ofHoms {α : Type*} {ι : α → Type t} {A B : ∀ a, ι a → C}
+    (f : ∀ a, ∀ i, A a i ⟶ B a i) :
+    ⨆ (a : α), ofHoms (f a) = ofHoms (fun (j : Σ (a : α), ι a) ↦ f j.1 j.2) := by
+  ext f
+  simp [ofHoms_iff]
+
+instance {ι : Type t} [Small.{w} ι] (W : ι → MorphismProperty C) [∀ i, IsSmall.{w} (W i)] :
+    IsSmall.{w} (⨆ i, W i) := by
+  choose α A B f hf using fun i ↦ (isSmall_iff_eq_ofHoms.{w} (W i)).1 inferInstance
+  simp only [hf, iSup_ofHoms]
+  infer_instance
+
 end MorphismProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/ObjectProperty/FunctorCategory/Presheaf.lean

@@ -0,0 +1,150 @@
+/-
+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
+-/
+module
+
+public import Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
+public import Mathlib.CategoryTheory.ObjectProperty.Local
+public import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
+public import Mathlib.CategoryTheory.Limits.Types.Colimits
+public import Mathlib.CategoryTheory.Limits.Types.Limits
+public import Mathlib.CategoryTheory.ShrinkYoneda
+
+/-!
+# Presheaves of types which preserves a limit
+
+Let `F : J ⥤ Cᵒᵖ` be a functor. We show that a presheaf `P : Cᵒᵖ ⥤ Type w`
+preserves the limit of `F` iff `P` is a local object with respect to a suitable
+family of morphisms in `Cᵒᵖ ⥤ Type w` (this family contains `1` or `0` morphism
+depending on whether the limit of `F` exists or not).
+
+-/
+
+@[expose] public section
+
+universe w w' v v' u u'
+
+namespace CategoryTheory
+
+open Limits Opposite
+
+namespace Presheaf
+
+section
+
+variable {C : Type u} [Category.{v} C]
+  {J : Type u'} [Category.{v'} J] [LocallySmall.{w} C]
+  {F : J ⥤ Cᵒᵖ} (c : Cone F) {c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w})}
+  (hc : IsLimit c) (hc' : IsColimit c') (P : Cᵒᵖ ⥤ Type w)
+
+variable {P} in
+/-- Let `F : J ⥤ Cᵒᵖ` be a functor, `c'` a colimit cocone for `F.leftOp ⋙ shrinkYoneda.{w}`.
+For any `P : Cᵒᵖ ⥤ Type w`, this is the bijection between `c'.pt ⟶ P` and the type
+of sections of `F ⋙ P`. -/
+@[simps -isSimp symm_apply apply_coe]
+noncomputable def coconeCompShrinkYonedaHomEquiv :
+    (c'.pt ⟶ P) ≃ (F ⋙ P).sections where
+  toFun f :=
+    { val j := shrinkYonedaEquiv (c'.ι.app (op j) ≫ f)
+      property {X X'} g := by
+        have h₁ := c'.w g.op
+        dsimp at h₁ ⊢
+        rw [← h₁, Category.assoc]
+        conv_rhs => rw [shrinkYonedaEquiv_comp]
+        rw [shrinkYonedaEquiv_shrinkYoneda_map]
+        apply map_shrinkYonedaEquiv }
+  invFun s := hc'.desc (Cocone.mk _
+    { app j := shrinkYonedaEquiv.symm (s.val j.unop)
+      naturality j₁ j₂ f := by
+        rw [← s.property f.unop]
+        dsimp
+        rw [shrinkYonedaEquiv_symm_map, Category.comp_id] })
+  left_inv f := hc'.hom_ext (by simp)
+  right_inv u := by ext; simp
+
+
+/-- Let `F : J ⥤ Cᵒᵖ` be a functor, `c'` a colimit cocone for `F.leftOp ⋙ shrinkYoneda.{w}`.
+For any cone `c` for `F`, this is the canonical natural transformation
+`c'.pt ⟶ shrinkYoneda.{w}.obj c.pt.unop`. -/
+noncomputable def coconePtToShrinkYoneda :
+    c'.pt ⟶ shrinkYoneda.{w}.obj c.pt.unop :=
+  hc'.desc (shrinkYoneda.{w}.mapCocone (coconeLeftOpOfCone c))
+
+variable {P} in
+@[reassoc]
+lemma coconePtToShrinkYoneda_comp (x : P.obj c.pt) :
+    coconePtToShrinkYoneda c hc' ≫ shrinkYonedaEquiv.symm x =
+      (coconeCompShrinkYonedaHomEquiv hc').symm
+        (Types.sectionOfCone (P.mapCone c) x) := by
+  refine hc'.hom_ext (fun j ↦ ?_)
+  dsimp [coconePtToShrinkYoneda, coconeCompShrinkYonedaHomEquiv_symm_apply]
+  rw [hc'.fac_assoc, hc'.fac]
+  exact (shrinkYonedaEquiv_symm_map _ _).symm
+
+lemma nonempty_isLimit_mapCone_iff :
+    Nonempty (IsLimit (P.mapCone c)) ↔
+      (MorphismProperty.single (coconePtToShrinkYoneda c hc')).isLocal P := by
+  rw [Types.isLimit_iff_bijective_sectionOfCone,
+    MorphismProperty.isLocal_single_iff_bijective,
+    ← Function.Bijective.of_comp_iff' (coconeCompShrinkYonedaHomEquiv hc').symm.bijective,
+    ← Function.Bijective.of_comp_iff _ shrinkYonedaEquiv.bijective]
+  convert Iff.rfl using 2
+  ext : 1
+  simp [← coconePtToShrinkYoneda_comp]
+
+variable {c}
+
+include hc in
+lemma preservesLimit_eq_isLocal_single :
+    ObjectProperty.preservesLimit F =
+      (MorphismProperty.single (coconePtToShrinkYoneda c hc')).isLocal := by
+  ext P
+  rw [← nonempty_isLimit_mapCone_iff c hc' P]
+  exact ⟨fun _ ↦ ⟨isLimitOfPreserves P hc⟩,
+    fun ⟨h⟩ ↦ preservesLimit_of_preserves_limit_cone hc h⟩
+
+variable (F) [Small.{w} J]
+
+/-- Auxiliary definition for `Presheaf.preservesLimitHomFamily`. -/
+noncomputable def preservesLimitHomFamilySrc :=
+  colimit (F.leftOp ⋙ shrinkYoneda)
+
+/-- Auxiliary definition for `Presheaf.preservesLimitHomFamily`. -/
+noncomputable def preservesLimitHomFamilyTgt (h : PLift (HasLimit F)) :=
+  letI := h.down
+  shrinkYoneda.obj (limit F).unop
+
+/-- Let `F : J ⥤ Cᵒᵖ` be a functor. This is the family of morphisms
+which consists of the single morphism
+`colimit (F.leftOp ⋙ shrinkYoneda) ⟶ shrinkYoneda.obj (limit F).unop`
+if `F` has a limit, or is the empty family otherwise. -/
+noncomputable def preservesLimitHomFamily (h : PLift (HasLimit F)) :
+    preservesLimitHomFamilySrc F ⟶ preservesLimitHomFamilyTgt F h :=
+  letI := h.down
+  coconePtToShrinkYoneda (limit.cone F) (colimit.isColimit _)
+
+lemma preservesLimit_eq_isLocal :
+    ObjectProperty.preservesLimit F =
+      (MorphismProperty.ofHoms (preservesLimitHomFamily F)).isLocal := by
+  ext G
+  by_cases hF : HasLimit F
+  · rw [preservesLimit_eq_isLocal_single (limit.isLimit F) (colimit.isColimit _)]
+    convert Iff.rfl
+    ext _ _ f
+    exact ⟨fun ⟨_⟩ ↦ ⟨⟨⟩⟩, fun ⟨_⟩ ↦ ⟨⟨hF⟩⟩⟩
+  · exact ⟨fun _ _ _ _ ⟨h⟩ ↦ (hF h.down).elim,
+      fun _ ↦ ⟨fun hc ↦ (hF ⟨_, hc⟩).elim⟩⟩
+
+lemma preservesLimitsOfShape_eq_isLocal :
+    ObjectProperty.preservesLimitsOfShape J =
+      (⨆ (F : J ⥤ Cᵒᵖ), MorphismProperty.ofHoms (preservesLimitHomFamily F)).isLocal := by
+  simp only [ObjectProperty.preservesLimitsOfShape_eq_iSup,
+    MorphismProperty.isLocal_iSup, preservesLimit_eq_isLocal]
+
+end
+
+end Presheaf
+
+end CategoryTheory

Mathlib/CategoryTheory/ObjectProperty/Local.lean

@@ -100,6 +100,28 @@ instance (J : Type u') [Category.{v'} J] :
           (by simp [h]) }),
       p.isColimit.hom_ext (fun j ↦ by simp [p.isColimit.fac_assoc, h])⟩
 
+attribute [local simp] isLocal_iff in
+@[simp]
+lemma isLocal_iSup {ι : Sort*} (W : ι → MorphismProperty C) :
+    (⨆ (i : ι), W i).isLocal = ⨅ (i : ι), (W i).isLocal := by
+  aesop
+
+attribute [local simp] isColocal_iff in
+@[simp]
+lemma isColocal_iSup {ι : Sort*} (W : ι → MorphismProperty C) :
+    (⨆ (i : ι), W i).isColocal = ⨅ (i : ι), (W i).isColocal := by
+  aesop
+
+lemma isLocal_single_iff_bijective {X Y : C} (f : X ⟶ Y) (Z : C) :
+    (MorphismProperty.single f).isLocal Z ↔
+      (Function.Bijective (fun (g : _ ⟶ Z) ↦ f ≫ g)) :=
+  ⟨fun h ↦ h _ ⟨⟨⟩⟩, fun h ↦ by rintro _ _ _ ⟨_⟩; exact h⟩
+
+lemma isColocal_single_iff_bijective {X Y : C} (f : X ⟶ Y) (Z : C) :
+    (MorphismProperty.single f).isColocal Z ↔
+      (Function.Bijective (fun (g : Z ⟶ _) ↦ g ≫ f)) :=
+  ⟨fun h ↦ h _ ⟨⟨⟩⟩, fun h ↦ by rintro _ _ _ ⟨_⟩; exact h⟩
+
 end MorphismProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/Presentable/Continuous.lean

@@ -0,0 +1,102 @@
+/-
+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
+-/
+module
+
+public import Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.Presheaf
+public import Mathlib.CategoryTheory.MorphismProperty.IsSmall
+public import Mathlib.CategoryTheory.SmallRepresentatives
+public import Mathlib.SetTheory.Cardinal.HasCardinalLT
+
+/-!
+# `κ`-continuous functors
+
+Given categories `C`, `D` and a regular cardinal `κ : Cardinal.{w}`, we define
+`isCardinalContinuous C D κ : ObjectProperty (C ⥤ D)` as the property
+of functors which preserves limits indexed by categories `J`
+such that `HasCardinalLT (Arrow J) κ`.
+
+When `C : Type w` is a small category, we show that `κ`-continuous
+functors `Cᵒᵖ ⥤ Type w` are exactly the objects that are local with
+respect to a suitable `w`-small family of morphisms.
+
+## TODO (@joelriou)
+* Show that `(isCardinalContinuous Cᵒᵖ (Type w) κ).FullSubcategory` is
+locally `κ`-presentable, and that any locally `κ`-presentable category
+is equivalent to a category of `κ`-continuous presheaves.
+
+-/
+
+@[expose] public section
+
+universe w v v' u u'
+
+namespace CategoryTheory
+
+open Limits
+
+namespace Functor
+
+section
+
+variable {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D]
+  (κ : Cardinal.{w}) [Fact κ.IsRegular]
+
+variable (C D) in
+def isCardinalContinuous : ObjectProperty (C ⥤ D) :=
+  ⨅ (J : Type w) (_ : Category.{w} J) (_ : HasCardinalLT (Arrow J) κ),
+    ObjectProperty.preservesLimitsOfShape J
+
+lemma isCardinalContinuous_iff (F : C ⥤ D) (κ : Cardinal.{w}) [Fact κ.IsRegular] :
+    isCardinalContinuous C D κ F ↔
+      ∀ (J : Type w) [SmallCategory J] (_ : HasCardinalLT (Arrow J) κ),
+        PreservesLimitsOfShape J F := by
+  simp [isCardinalContinuous]
+
+variable {κ} in
+lemma isCardinalContinuous.preservesColimitsOfShape {F : C ⥤ D}
+    (hF : isCardinalContinuous C D κ F)
+    (J : Type w) [SmallCategory.{w} J] (hκ : HasCardinalLT (Arrow J) κ) :
+    PreservesLimitsOfShape J F :=
+  (isCardinalContinuous_iff F κ).1 hF J hκ
+
+end
+
+end Functor
+
+namespace Presheaf
+
+open Functor
+
+variable (C : Type w) [SmallCategory C] (κ : Cardinal.{w}) [Fact κ.IsRegular]
+
+abbrev isCardinalContinuousMorphismProperty : MorphismProperty (Cᵒᵖ ⥤ Type w) :=
+  ⨆ (J) (F : SmallCategoryCardinalLT.categoryFamily κ J ⥤ Cᵒᵖ),
+    MorphismProperty.ofHoms (Presheaf.preservesLimitHomFamily F)
+
+example : MorphismProperty.IsSmall.{w}
+    (isCardinalContinuousMorphismProperty C κ) := by
+  infer_instance
+
+lemma isCardinalContinuous_eq_isLocal :
+    isCardinalContinuous Cᵒᵖ (Type w) κ =
+      (isCardinalContinuousMorphismProperty.{w} C κ).isLocal := by
+  trans ⨅ (J : SmallCategoryCardinalLT κ),
+    ObjectProperty.preservesLimitsOfShape (SmallCategoryCardinalLT.categoryFamily κ J)
+  · refine le_antisymm ?_ ?_
+    · simp only [le_iInf_iff]
+      intro J P hP
+      simpa using hP.preservesColimitsOfShape _ (SmallCategoryCardinalLT.hasCardinalLT κ J)
+    · dsimp [isCardinalContinuous]
+      simp only [le_iInf_iff]
+      intro J _ hJ
+      obtain ⟨J', ⟨e⟩⟩ := SmallCategoryCardinalLT.exists_equivalence κ J hJ
+      rw [← ObjectProperty.congr_preservesLimitsOfShape _ _ e]
+      apply iInf_le
+  · simp [preservesLimitsOfShape_eq_isLocal]
+
+end Presheaf
+
+end CategoryTheory