feat(CategoryTheory): presheaves of types which preserve a limit

Mathlib.lean

@@ -3117,6 +3117,7 @@ public import Mathlib.CategoryTheory.ObjectProperty.Extensions
 public import Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
 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

Mathlib/CategoryTheory/MorphismProperty/Basic.lean

@@ -214,6 +214,15 @@ 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)
+
+lemma iSup_ofHoms {α : Type*} {ι : α → Type*} {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]
+
 end
 
 section

Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean

@@ -72,6 +72,12 @@ instance isSmall_iSup {α : Type*} (W : α → MorphismProperty C)
     obtain ⟨i, hf⟩ := hf
     exact ⟨⟨i, ⟨_, hf⟩⟩, rfl⟩
 
+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,152 @@
+/-
+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)
+
+set_option backward.isDefEq.respectTransparency false in
+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))
+
+set_option backward.isDefEq.respectTransparency false in
+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
+
+set_option backward.isDefEq.respectTransparency false in
+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 abbrev preservesLimitHomFamilySrc :=
+  colimit (F.leftOp ⋙ shrinkYoneda)
+
+/-- Auxiliary definition for `Presheaf.preservesLimitHomFamily`. -/
+noncomputable abbrev 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 abbrev 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

@@ -102,6 +102,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