feat(CategoryTheory/Sites): characterization of conservative families of points

Mathlib.lean

@@ -2532,6 +2532,7 @@ public import Mathlib.CategoryTheory.Functor.KanExtension.Preserves
 public import Mathlib.CategoryTheory.Functor.OfSequence
 public import Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
 public import Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
+public import Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
 public import Mathlib.CategoryTheory.Functor.RegularEpi
 public import Mathlib.CategoryTheory.Functor.Trifunctor
 public import Mathlib.CategoryTheory.Functor.TwoSquare
@@ -3140,6 +3141,7 @@ public import Mathlib.CategoryTheory.Sites.Over
 public import Mathlib.CategoryTheory.Sites.Plus
 public import Mathlib.CategoryTheory.Sites.Point.Basic
 public import Mathlib.CategoryTheory.Sites.Point.Category
+public import Mathlib.CategoryTheory.Sites.Point.Conservative
 public import Mathlib.CategoryTheory.Sites.Precoverage
 public import Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
 public import Mathlib.CategoryTheory.Sites.Preserves
@@ -3226,6 +3228,7 @@ public import Mathlib.CategoryTheory.Triangulated.TriangleShift
 public import Mathlib.CategoryTheory.Triangulated.Triangulated
 public import Mathlib.CategoryTheory.Triangulated.Yoneda
 public import Mathlib.CategoryTheory.Types.Basic
+public import Mathlib.CategoryTheory.Types.Epimorphisms
 public import Mathlib.CategoryTheory.Types.Monomorphisms
 public import Mathlib.CategoryTheory.Types.Set
 public import Mathlib.CategoryTheory.UnivLE

Mathlib/CategoryTheory/Functor/ReflectsIso/Jointly.lean

@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou, Christian Merten
+-/
+module
+
+public import Mathlib.CategoryTheory.Limits.EpiMono
+public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
+public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
+public import Mathlib.CategoryTheory.MorphismProperty.Basic
+
+/-!
+# Families of functors which jointly reflect isomorphisms
+
+Let `Fᵢ : C ⥤ Dᵢ` be a family of functors. The family is said to jointly reflect
+isomorphisms (resp. monomorphisms, resp. epimorphisms) if every `f : X ⟶ Y`
+in `C` for which `Fᵢ.map f` is an isomorphism (resp. monomorphism, resp. epimorphism)
+for all `i` is an isomorphism.
+
+-/
+
+@[expose] public section
+
+namespace CategoryTheory
+
+open Category Limits
+
+variable {C : Type*} [Category C] {I : Type*} {D : I → Type*} [∀ i, Category (D i)]
+
+/-- A family of functors jointly reflects isomorphisms if for every morphism `f : X ⟶ Y`
+such that the image of `f` under all `F i` is an isomorphism, then `f` is an isomorphism. -/
+structure JointlyReflectIsomorphisms (F : ∀ i, C ⥤ D i) : Prop where
+  isIso {X Y : C} (f : X ⟶ Y) [∀ i, IsIso ((F i).map f)] : IsIso f
+
+/-- A family of functors jointly reflects monomorphisms if for every morphism `f : X ⟶ Y`
+such that the image of `f` under all `F i` is an monomorphism, then `f` is an monomorphism. -/
+structure JointlyReflectMonomorphisms (F : ∀ i, C ⥤ D i) : Prop where
+  mono {X Y : C} (f : X ⟶ Y) [∀ i, Mono ((F i).map f)] : Mono f
+
+/-- A family of functors jointly reflects epimorphisms if for every morphism `f : X ⟶ Y`
+such that the image of `f` under all `F i` is an epimorphism, then `f` is an epimorphism. -/
+structure JointlyReflectEpimorphisms (F : ∀ i, C ⥤ D i) : Prop where
+  epi {X Y : C} (f : X ⟶ Y) [∀ i, Epi ((F i).map f)] : Epi f
+
+/-- A family of functors is jointly faithful if whenever two morphisms `f : X ⟶ Y`
+and `g : X ⟶ Y` become equal after applying all functors `F i`, then `f = g`. -/
+structure JointlyFaithful (F : ∀ i, C ⥤ D i) : Prop where
+  map_injective {X Y : C} {f g : X ⟶ Y} (h : ∀ i, (F i).map f = (F i).map g) : f = g
+
+variable {F : ∀ i, C ⥤ D i}
+
+lemma JointlyFaithful.of_jointly_reflects_isIso_of_mono [HasEqualizers C]
+    [∀ i, PreservesLimitsOfShape WalkingParallelPair (F i)]
+    (hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [Mono f],
+      (∀ i, IsIso ((F i).map f)) → IsIso f) :
+    JointlyFaithful F where
+  map_injective {X Y} f g hfg := by
+    have :=
+      hF (equalizer.ι f g) (fun i ↦ by
+        let hc := isLimitForkMapOfIsLimit (F i) _ (equalizerIsEqualizer f g)
+        obtain ⟨l, hl⟩ := Fork.IsLimit.lift' hc (𝟙 _) (by simpa using hfg i)
+        exact ⟨l, Fork.IsLimit.hom_ext hc (by cat_disch), by cat_disch⟩)
+    exact eq_of_epi_equalizer
+
+namespace JointlyReflectIsomorphisms
+
+variable (h : JointlyReflectIsomorphisms F)
+
+include h
+
+lemma isIso_iff {X Y : C} (f : X ⟶ Y) :
+    IsIso f ↔ ∀ i, IsIso ((F i).map f) :=
+  ⟨fun _ _ ↦ inferInstance, fun _ ↦ h.isIso f⟩
+
+lemma mono {X Y : C} (f : X ⟶ Y) [hf : ∀ i, Mono ((F i).map f)]
+    [∀ i, PreservesLimit (cospan f f) (F i)] [HasPullback f f] :
+    Mono f := by
+  have hc := pullbackIsPullback f f
+  rw [mono_iff_isIso_fst hc, h.isIso_iff]
+  intro i
+  exact (mono_iff_isIso_fst ((isLimitMapConePullbackConeEquiv (F i) pullback.condition).1
+    (isLimitOfPreserves (F i) hc))).1 (hf i)
+
+lemma jointlyReflectMonomorphisms [∀ i, PreservesLimitsOfShape WalkingCospan (F i)]
+    [HasPullbacks C] :
+    JointlyReflectMonomorphisms F where
+  mono f _ := h.mono f
+
+lemma epi {X Y : C} (f : X ⟶ Y) [hf : ∀ i, Epi ((F i).map f)]
+    [∀ i, PreservesColimit (span f f) (F i)] [HasPushout f f] : Epi f := by
+  have hc := pushoutIsPushout f f
+  rw [epi_iff_isIso_inl hc, h.isIso_iff]
+  intro i
+  exact (epi_iff_isIso_inl ((isColimitMapCoconePushoutCoconeEquiv (F i) pushout.condition).1
+    (isColimitOfPreserves (F i) hc))).1 (hf i)
+
+lemma jointlyReflectEpimorphisms [∀ i, PreservesColimitsOfShape WalkingSpan (F i)]
+    [HasPushouts C] :
+    JointlyReflectEpimorphisms F where
+  epi f _ := h.epi f
+
+lemma jointlyFaithful [∀ i, PreservesLimitsOfShape WalkingParallelPair (F i)] [HasEqualizers C] :
+    JointlyFaithful F :=
+  .of_jointly_reflects_isIso_of_mono (fun _ _ _ _ _ ↦ h.isIso _)
+
+end JointlyReflectIsomorphisms
+
+lemma JointlyReflectMonomorphisms.mono_iff (h : JointlyReflectMonomorphisms F)
+    [∀ i, (F i).PreservesMonomorphisms] {X Y : C} (f : X ⟶ Y) :
+    Mono f ↔ ∀ i, Mono ((F i).map f) :=
+  ⟨fun _ _ ↦ inferInstance, fun _ ↦ h.mono f⟩
+
+lemma JointlyReflectEpimorphisms.epi_iff (h : JointlyReflectEpimorphisms F)
+    [∀ i, (F i).PreservesEpimorphisms] {X Y : C} (f : X ⟶ Y) :
+    Epi f ↔ ∀ i, Epi ((F i).map f) :=
+  ⟨fun _ _ ↦ inferInstance, fun _ ↦ h.epi f⟩
+
+namespace JointlyFaithful
+
+lemma jointlyReflectMonomorphisms (h : JointlyFaithful F) :
+    JointlyReflectMonomorphisms F where
+  mono {X Y} f _ := ⟨fun {Z} g₁ g₂ hg ↦ h.map_injective (fun i ↦ by
+    simp only [← cancel_mono ((F i).map f), ← Functor.map_comp, hg])⟩
+
+lemma jointlyReflectEpimorphisms (h : JointlyFaithful F) :
+    JointlyReflectEpimorphisms F where
+  epi {X Y} f _ := ⟨fun {Z} g₁ g₂ hg ↦ h.map_injective (fun i ↦ by
+    simp only [← cancel_epi ((F i).map f), ← Functor.map_comp, hg])⟩
+
+lemma jointlyReflectsIsomorphisms [Balanced C] (h : JointlyFaithful F) :
+    JointlyReflectIsomorphisms F where
+  isIso {X Y} f _ := by
+    have := h.jointlyReflectMonomorphisms.mono f
+    have := h.jointlyReflectEpimorphisms.epi f
+    exact Balanced.isIso_of_mono_of_epi f
+
+end JointlyFaithful
+
+end CategoryTheory

Mathlib/CategoryTheory/ShrinkYoneda.lean

@@ -70,6 +70,23 @@ noncomputable def shrinkYonedaObjObjEquiv {X : C} {Y : Cᵒᵖ} :
     ((shrinkYoneda.{w}.obj X).obj Y) ≃ (Y.unop ⟶ X) :=
   (equivShrink _).symm
 
+lemma shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm
+    {X : C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : Y.unop ⟶ X) :
+    (shrinkYoneda.obj _).map g (shrinkYonedaObjObjEquiv.symm f) =
+      shrinkYonedaObjObjEquiv.symm (g.unop ≫ f) := by
+  simp [shrinkYoneda, shrinkYonedaObjObjEquiv]
+
+lemma shrinkYonedaObjObjEquiv_symm_comp {X Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ X) :
+    shrinkYonedaObjObjEquiv.symm (g ≫ f) =
+    (shrinkYoneda.obj _).map g.op (shrinkYonedaObjObjEquiv.symm f) :=
+  (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm g.op f).symm
+
+lemma shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm
+    {X X' : C} {Y : Cᵒᵖ} (f : Y.unop ⟶ X) (g : X ⟶ X') :
+    (shrinkYoneda.map g).app _ (shrinkYonedaObjObjEquiv.symm f) =
+      shrinkYonedaObjObjEquiv.symm (f ≫ g) := by
+  simp [shrinkYoneda, shrinkYonedaObjObjEquiv]
+
 /-- The type of natural transformations `shrinkYoneda.{w}.obj X ⟶ P`
 with `X : C` and `P : Cᵒᵖ ⥤ Type w` is equivalent to `P.obj (op X)`. -/
 noncomputable def shrinkYonedaEquiv {X : C} {P : Cᵒᵖ ⥤ Type w} :
@@ -114,6 +131,13 @@ lemma shrinkYonedaEquiv_symm_map {X Y : Cᵒᵖ} (f : X ⟶ Y) {P : Cᵒᵖ ⥤
     rw [← shrinkYonedaEquiv_naturality]
     simp)
 
+lemma shrinkYonedaEquiv_symm_app_shrinkYonedaObjObjEquiv_symm {X : C} {P : Cᵒᵖ ⥤ Type w}
+    (s : P.obj (op X)) {Y : C} (f : Y ⟶ X) :
+    (shrinkYonedaEquiv.symm s).app (op Y) (shrinkYonedaObjObjEquiv.symm f) =
+      P.map f.op s := by
+  obtain ⟨g, rfl⟩ := shrinkYonedaEquiv.surjective s
+  simp [map_shrinkYonedaEquiv]
+
 variable (C) in
 /-- The functor `shrinkYoneda : C ⥤ Cᵒᵖ ⥤ Type w` for a locally `w`-small category `C`
 is fully faithful. -/

Mathlib/CategoryTheory/Sites/LocallySurjective.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.CategoryTheory.Sites.Subsheaf
 public import Mathlib.CategoryTheory.Sites.CompatibleSheafification
 public import Mathlib.CategoryTheory.Sites.LocallyInjective
+public import Mathlib.CategoryTheory.ShrinkYoneda
 /-!
 
 # Locally surjective morphisms
@@ -31,7 +32,7 @@ public import Mathlib.CategoryTheory.Sites.LocallyInjective
 
 universe v u w v' u' w'
 
-open Opposite CategoryTheory CategoryTheory.GrothendieckTopology CategoryTheory.Functor
+open Opposite CategoryTheory CategoryTheory.GrothendieckTopology CategoryTheory.Functor Limits
 
 namespace CategoryTheory
 
@@ -52,6 +53,13 @@ def imageSieve {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C} (s : ToType (G.obj (o
     refine ⟨F.map j.op t, ?_⟩
     rw [op_comp, G.map_comp, ConcreteCategory.comp_apply, ← ht, NatTrans.naturality_apply f]
 
+lemma pullback_imageSieve
+    {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C} (s : ToType (G.obj (op U)))
+    {V : C} (g : V ⟶ U) :
+    (imageSieve f s).pullback g = imageSieve f (G.map g.op s) := by
+  ext W g
+  simp [imageSieve]
+
 theorem imageSieve_eq_sieveOfSection {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C}
     (s : ToType (G.obj (op U))) :
     imageSieve f s = (Subfunctor.range (whiskerRight f (forget A))).sieveOfSection s :=
@@ -395,4 +403,42 @@ lemma isAmalgamation_map_localPreimage :
 
 end Presieve.FamilyOfElements
 
+namespace GrothendieckTopology
+
+variable [LocallySmall.{w} C]
+
+lemma ofArrows_mem_iff_isLocallySurjective
+    {S : C} {ι : Type*} [Small.{w} ι] {X : ι → C}
+    (f : ∀ i, X i ⟶ S) :
+    Sieve.ofArrows _ f ∈ J S ↔
+      Presheaf.IsLocallySurjective J (Sigma.desc (fun i ↦ shrinkYoneda.{w}.map (f i))) := by
+  refine ⟨fun hf ↦ ⟨fun {U u} ↦ ?_⟩, fun _ ↦ ?_⟩
+  · obtain ⟨u : U ⟶ S, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective u
+    refine J.superset_covering (fun V g ↦ ?_) (J.pullback_stable u hf)
+    rintro ⟨_, v, _, ⟨i⟩, fac⟩
+    refine ⟨(Sigma.ι (fun i ↦ shrinkYoneda.{w}.obj (X i)) i).app _
+      (shrinkYonedaObjObjEquiv.symm v),
+      (congr_fun (NatTrans.congr_app
+      (Sigma.ι_desc (fun i ↦ shrinkYoneda.{w}.map (f i)) i) _) _).trans ?_⟩
+    rw [shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm, fac,
+      shrinkYonedaObjObjEquiv_symm_comp]
+    rfl
+  · refine J.superset_covering ?_
+      (Presheaf.imageSieve_mem J (Sigma.desc (fun i ↦ shrinkYoneda.{w}.map (f i)))
+        (shrinkYonedaObjObjEquiv.symm (𝟙 S)))
+    rintro Z g ⟨a, ha⟩
+    obtain ⟨⟨i⟩, a, rfl⟩ := Types.jointly_surjective_of_isColimit
+      (isColimitOfPreserves ((evaluation _ _).obj (op Z))
+      (coproductIsCoproduct (fun i ↦ shrinkYoneda.{w}.obj (X i)))) a
+    obtain ⟨a, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective a
+    refine ⟨_, a, _, ⟨i⟩, shrinkYonedaObjObjEquiv.symm.injective ?_⟩
+    convert ha
+    · rw [← shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm]
+      exact congr_fun (NatTrans.congr_app
+        (Sigma.ι_desc (fun i ↦ shrinkYoneda.{w}.map (f i)) i) (op Z)).symm
+        (shrinkYonedaObjObjEquiv.symm a)
+    · simpa using (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm g.op (𝟙 _)).symm
+
+end GrothendieckTopology
+
 end CategoryTheory