feat(Condensed): a sequential limit of epimorphisms in light condensed modules is epimorphic

Mathlib.lean

@@ -1955,6 +1955,7 @@ import Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent
 import Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular
 import Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
 import Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
+import Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
 import Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
 import Mathlib.CategoryTheory.Sites.CompatiblePlus
 import Mathlib.CategoryTheory.Sites.CompatibleSheafification
@@ -1999,6 +2000,7 @@ import Mathlib.CategoryTheory.Sites.SheafOfTypes
 import Mathlib.CategoryTheory.Sites.Sheafification
 import Mathlib.CategoryTheory.Sites.Sieves
 import Mathlib.CategoryTheory.Sites.Spaces
+import Mathlib.CategoryTheory.Sites.Subcanonical
 import Mathlib.CategoryTheory.Sites.Subsheaf
 import Mathlib.CategoryTheory.Sites.Types
 import Mathlib.CategoryTheory.Sites.Whiskering

Mathlib/AlgebraicGeometry/Sites/BigZariski.lean

@@ -70,8 +70,8 @@ lemma zariskiTopology_openCover {Y : Scheme.{u}} (U : OpenCover.{v} Y) :
   rintro _ _ ⟨y⟩
   exact ⟨_, 𝟙 _, U.map (U.f y), ⟨_⟩, by simp⟩
 
-lemma subcanonical_zariskiTopology : Sheaf.Subcanonical zariskiTopology := by
-  apply Sheaf.Subcanonical.of_yoneda_isSheaf
+instance subcanonical_zariskiTopology : zariskiTopology.Subcanonical := by
+  apply GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
   intro X
   rw [Presieve.isSheaf_pretopology]
   rintro Y S ⟨𝓤,rfl⟩ x hx

Mathlib/CategoryTheory/Sites/Canonical.lean

@@ -205,60 +205,83 @@ theorem isSheaf_of_isRepresentable (P : Cᵒᵖ ⥤ Type v) [P.IsRepresentable]
     Presieve.IsSheaf (canonicalTopology C) P :=
   Presieve.isSheaf_iso (canonicalTopology C) P.reprW (isSheaf_yoneda_obj _)
 
+end Sheaf
+
+namespace GrothendieckTopology
+
+open Sheaf
+
 /-- A subcanonical topology is a topology which is smaller than the canonical topology.
 Equivalently, a topology is subcanonical iff every representable is a sheaf.
 -/
-def Subcanonical (J : GrothendieckTopology C) : Prop :=
-  J ≤ canonicalTopology C
+class Subcanonical (J : GrothendieckTopology C) : Prop where
+  le_canonical : J ≤ canonicalTopology C
+
+lemma le_canonical (J : GrothendieckTopology C) [Subcanonical J] : J ≤ canonicalTopology C :=
+  Subcanonical.le_canonical
+
+instance : (canonicalTopology C).Subcanonical where
+  le_canonical := le_rfl
 
 namespace Subcanonical
 
 /-- If every functor `yoneda.obj X` is a `J`-sheaf, then `J` is subcanonical. -/
-theorem of_yoneda_isSheaf (J : GrothendieckTopology C)
-    (h : ∀ X, Presieve.IsSheaf J (yoneda.obj X)) : Subcanonical J :=
-  le_finestTopology _ _
-    (by
-      rintro P ⟨X, rfl⟩
-      apply h)
+theorem of_isSheaf_yoneda_obj (J : GrothendieckTopology C)
+    (h : ∀ X, Presieve.IsSheaf J (yoneda.obj X)) : Subcanonical J where
+  le_canonical := le_finestTopology _ _ (by rintro P ⟨X, rfl⟩; apply h)
 
 /-- If `J` is subcanonical, then any representable is a `J`-sheaf. -/
-theorem isSheaf_of_isRepresentable {J : GrothendieckTopology C} (hJ : Subcanonical J)
+theorem isSheaf_of_isRepresentable {J : GrothendieckTopology C} [Subcanonical J]
     (P : Cᵒᵖ ⥤ Type v) [P.IsRepresentable] : Presieve.IsSheaf J P :=
-  Presieve.isSheaf_of_le _ hJ (Sheaf.isSheaf_of_isRepresentable P)
+  Presieve.isSheaf_of_le _ J.le_canonical (Sheaf.isSheaf_of_isRepresentable P)
 
-variable {J}
+variable {J : GrothendieckTopology C}
+
+end Subcanonical
+
+variable (J : GrothendieckTopology C)
 
 /--
 If `J` is subcanonical, we obtain a "Yoneda" functor from the defining site
 into the sheaf category.
 -/
 @[simps]
-def yoneda (hJ : Subcanonical J) : C ⥤ Sheaf J (Type v) where
+def yoneda [J.Subcanonical] : C ⥤ Sheaf J (Type v) where
   obj X := ⟨CategoryTheory.yoneda.obj X, by
     rw [isSheaf_iff_isSheaf_of_type]
-    apply hJ.isSheaf_of_isRepresentable⟩
+    apply Subcanonical.isSheaf_of_isRepresentable⟩
   map f := ⟨CategoryTheory.yoneda.map f⟩
 
-variable (hJ : Subcanonical J)
+variable [Subcanonical J]
 
 /--
 The yoneda embedding into the presheaf category factors through the one
 to the sheaf category.
 -/
 def yonedaCompSheafToPresheaf :
-    hJ.yoneda ⋙ sheafToPresheaf J (Type v) ≅ CategoryTheory.yoneda :=
+    J.yoneda ⋙ sheafToPresheaf J (Type v) ≅ CategoryTheory.yoneda :=
   Iso.refl _
 
 /-- The yoneda functor into the sheaf category is fully faithful -/
-def yonedaFullyFaithful : hJ.yoneda.FullyFaithful :=
+def yonedaFullyFaithful : (J.yoneda).FullyFaithful :=
   Functor.FullyFaithful.ofCompFaithful (G := sheafToPresheaf J (Type v)) Yoneda.fullyFaithful
 
-instance : hJ.yoneda.Full := hJ.yonedaFullyFaithful.full
+instance : (J.yoneda).Full := (J.yonedaFullyFaithful).full
 
-instance : hJ.yoneda.Faithful := hJ.yonedaFullyFaithful.faithful
+instance : (J.yoneda).Faithful := (J.yonedaFullyFaithful).faithful
 
-end Subcanonical
+end GrothendieckTopology
 
-end Sheaf
+@[deprecated (since := "2024-10-29")] alias Sheaf.Subcanonical := GrothendieckTopology.Subcanonical
+@[deprecated (since := "2024-10-29")] alias Sheaf.Subcanonical.of_isSheaf_yoneda_obj :=
+  GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
+@[deprecated (since := "2024-10-29")] alias Sheaf.Subcanonical.isSheaf_of_isRepresentable :=
+  GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable
+@[deprecated (since := "2024-10-29")] alias Sheaf.Subcanonical.yoneda :=
+  GrothendieckTopology.yoneda
+@[deprecated (since := "2024-10-29")] alias Sheaf.Subcanonical.yonedaCompSheafToPresheaf :=
+  GrothendieckTopology.yonedaCompSheafToPresheaf
+@[deprecated (since := "2024-10-29")] alias Sheaf.Subcanonical.yonedaFullyFaithful :=
+  GrothendieckTopology.yonedaFullyFaithful
 
 end CategoryTheory

Mathlib/CategoryTheory/Sites/Coherent/CoherentSheaves.lean

@@ -59,8 +59,8 @@ theorem isSheaf_yoneda_obj (W : C) : Presieve.IsSheaf (coherentTopology C) (yone
 
 variable (C) in
 /-- The coherent topology on a precoherent category is subcanonical. -/
-theorem subcanonical : Sheaf.Subcanonical (coherentTopology C) :=
-  Sheaf.Subcanonical.of_yoneda_isSheaf _ isSheaf_yoneda_obj
+instance subcanonical : (coherentTopology C).Subcanonical :=
+  GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ isSheaf_yoneda_obj
 
 end coherentTopology
 

Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean

@@ -69,8 +69,8 @@ theorem extensiveTopology.isSheaf_yoneda_obj (W : C) : Presieve.IsSheaf (extensi
   exact isSheafFor_extensive_of_preservesFiniteProducts _ _
 
 /-- The extensive topology on a finitary pre-extensive category is subcanonical. -/
-theorem extensiveTopology.subcanonical : Sheaf.Subcanonical (extensiveTopology C) :=
-  Sheaf.Subcanonical.of_yoneda_isSheaf _ isSheaf_yoneda_obj
+instance extensiveTopology.subcanonical : (extensiveTopology C).Subcanonical :=
+  GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ isSheaf_yoneda_obj
 
 variable [FinitaryExtensive C]
 

Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean

@@ -257,8 +257,8 @@ lemma isSheaf_yoneda_obj [Preregular C] (W : C)  :
   · exact fun y hy ↦ t_uniq y <| Presieve.isAmalgamation_sieveExtend x y hy
 
 /-- The regular topology on any preregular category is subcanonical. -/
-theorem subcanonical [Preregular C] : Sheaf.Subcanonical (regularTopology C) :=
-  Sheaf.Subcanonical.of_yoneda_isSheaf _ isSheaf_yoneda_obj
+instance subcanonical [Preregular C] : (regularTopology C).Subcanonical :=
+  GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ isSheaf_yoneda_obj
 
 end regularTopology
 

Mathlib/CategoryTheory/Sites/Coherent/SequentialLimit.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2024 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
+import Mathlib.CategoryTheory.Functor.OfSequence
+import Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
+import Mathlib.CategoryTheory.Sites.EpiMono
+import Mathlib.CategoryTheory.Sites.Subcanonical
+/-!
+
+# Limits of epimorphisms in coherent topoi
+
+This file proves that a sequential limit of epimorphisms is epimorphic in the category of sheaves
+for the coherent topology on a preregular finitary extensive concrete category where the effective
+epimorphisms are precisely the surjective ones.
+
+In other words, given epimorphisms of sheaves
+
+`⋯ ⟶ Xₙ₊₁ ⟶ Xₙ ⟶ ⋯ ⟶ X₀`,
+
+the projection map `lim Xₙ ⟶ X₀` is an epimorphism (see `coherentTopology.epi_π_app_zero_of_epi`).
+
+This is deduced from the corresponding statement about locally surjective morphisms of sheaves
+(see `coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map`).
+-/
+
+universe w v u
+
+open CategoryTheory Limits Opposite
+
+attribute [local instance] ConcreteCategory.instFunLike
+
+namespace CategoryTheory.coherentTopology
+
+variable {C : Type u} [Category.{v} C] [Preregular C] [FinitaryExtensive C]
+    {F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)} {c : Cone F}
+    (hc : IsLimit c)
+    (hF : ∀ n, Sheaf.IsLocallySurjective (F.map (homOfLE (Nat.le_succ n)).op))
+
+private noncomputable def preimage (X : C) (y : (F.obj ⟨0⟩).val.obj ⟨X⟩) :
+    (n : ℕ) → ((Y : C) × (F.obj ⟨n⟩).val.obj ⟨Y⟩)
+  | 0 => ⟨X, y⟩
+  | (n+1) => by
+    have := hF n
+    rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff] at this
+    specialize this (preimage X y n).1 (preimage X y n).2
+    exact ⟨this.choose, this.choose_spec.choose_spec.choose_spec.choose⟩
+
+private noncomputable def preimageTransitionMap (X : C) (y : (F.obj ⟨0⟩).val.obj ⟨X⟩) (n : ℕ) :
+    (preimage hF X y (n + 1)).1 ⟶ (preimage hF X y n).1 := by
+  have := hF n
+  rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff] at this
+  specialize this (preimage hF X y n).1 (preimage hF X y n).2
+  exact this.choose_spec.choose
+
+private lemma preimageTransitionMap_effectiveEpi (X : C) (y : (F.obj ⟨0⟩).val.obj ⟨X⟩) (n : ℕ) :
+    EffectiveEpi (preimageTransitionMap hF X y n) := by
+  have := hF n
+  rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff] at this
+  specialize this (preimage hF X y n).1 (preimage hF X y n).2
+  exact this.choose_spec.choose_spec.choose
+
+private lemma preimage_w (X : C) (y : (F.obj ⟨0⟩).val.obj ⟨X⟩) (n : ℕ) :
+    (F.map (homOfLE (n.le_add_right 1)).op).val.app ⟨(preimage hF X y (n+1)).1⟩
+      (preimage hF X y (n+1)).2 = ((F.obj ⟨n⟩).val.map (preimageTransitionMap hF X y n).op)
+        (preimage hF X y n).2 := by
+  have := hF n
+  rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff] at this
+  specialize this (preimage hF X y n).1 (preimage hF X y n).2
+  exact this.choose_spec.choose_spec.choose_spec.choose_spec
+
+private noncomputable def preimageDiagram (X : C) (y : (F.obj ⟨0⟩).val.obj ⟨X⟩) : ℕᵒᵖ ⥤ C :=
+  Functor.ofOpSequence (X := fun n ↦ (preimage hF X y n).1)
+    fun n ↦ preimageTransitionMap hF X y n
+
+variable [HasLimitsOfShape ℕᵒᵖ C]
+
+private noncomputable def auxCone (X : C) (y : (F.obj ⟨0⟩).val.obj ⟨X⟩) : Cone F where
+  pt := ((coherentTopology C).yoneda).obj (limit (preimageDiagram hF X y))
+  π := NatTrans.ofOpSequence
+    (fun n ↦ (coherentTopology C).yoneda.map
+      (limit.π _ ⟨n⟩) ≫ ((coherentTopology C).yonedaEquiv).symm (preimage hF X y n).2) (by
+    intro n
+    simp only [Functor.const_obj_obj, homOfLE_leOfHom, Functor.const_obj_map, Category.id_comp,
+      Category.assoc, ← limit.w (preimageDiagram hF X y) (homOfLE (n.le_add_right 1)).op,
+      Nat.succ_eq_add_one, homOfLE_leOfHom, Functor.map_comp]
+    rw [GrothendieckTopology.yonedaEquiv_symm_naturality_left,
+      GrothendieckTopology.yonedaEquiv_symm_naturality_right]
+    erw [preimage_w hF X y n]
+    simp [preimageDiagram] )
+
+variable [ConcreteCategory C] (h : ∀ {X Y : C} (f : X ⟶ Y), EffectiveEpi f ↔ Function.Surjective f)
+
+variable [PreservesLimitsOfShape ℕᵒᵖ (forget C)]
+
+include hF h hc in
+lemma isLocallySurjective_π_app_zero_of_isLocallySurjective_map :
+    Sheaf.IsLocallySurjective (c.π.app ⟨0⟩) := by
+  rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff]
+  intro X y
+  have hh : EffectiveEpi (limit.π (preimageDiagram hF X y) ⟨0⟩) := by
+    rw [h]
+    refine Concrete.surjective_π_app_zero_of_surjective_map (limit.isLimit _) fun n ↦ ?_
+    simpa [preimageDiagram, ← h] using preimageTransitionMap_effectiveEpi hF X y n
+  refine ⟨limit (preimageDiagram hF X y), limit.π (preimageDiagram hF X y) ⟨0⟩, hh,
+    (coherentTopology C).yonedaEquiv (hc.lift (auxCone hF X y )),
+    (?_ : (c.π.app (op 0)).val.app _ _ = _)⟩
+  simp only [← (coherentTopology C).yonedaEquiv_comp, Functor.const_obj_obj, auxCone,
+    IsLimit.fac, NatTrans.ofOpSequence_app, (coherentTopology C).yonedaEquiv_comp,
+    (coherentTopology C).yonedaEquiv_yoneda_map]
+  rfl
+
+include h in
+lemma epi_π_app_zero_of_epi [HasSheafify (coherentTopology C) (Type v)]
+    [Balanced (Sheaf (coherentTopology C) (Type v))]
+    [(coherentTopology C).WEqualsLocallyBijective (Type v)]
+    {F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)}
+    {c : Cone F} (hc : IsLimit c)
+    (hF : ∀ n, Epi (F.map (homOfLE (Nat.le_succ n)).op)) : Epi (c.π.app ⟨0⟩) := by
+  simp_rw [← Sheaf.isLocallySurjective_iff_epi'] at hF ⊢
+  exact isLocallySurjective_π_app_zero_of_isLocallySurjective_map hc hF h
+
+end CategoryTheory.coherentTopology