Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 23 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/AlgebraicGeometry/Sites/BigZariski.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
63 changes: 43 additions & 20 deletions Mathlib/CategoryTheory/Sites/Canonical.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions Mathlib/CategoryTheory/Sites/Coherent/CoherentSheaves.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
4 changes: 2 additions & 2 deletions Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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]

Expand Down
4 changes: 2 additions & 2 deletions Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
124 changes: 124 additions & 0 deletions Mathlib/CategoryTheory/Sites/Coherent/SequentialLimit.lean
Original file line number Diff line number Diff line change
@@ -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
Loading