feat(Topology/Category): the standard Grothendieck topology on TopCat (leanprover-community#34979)

We define the Grothendieck topology generated by families of jointly surjective open embeddings on `TopCat` and show it is subcanonical. This will be used to show that for a topological space `T`, the presheaf `U ↦ C(U, T)` on `Scheme` is a Zariski-sheaf.

Co-authored by: Edward van de Meent <edwardvdmeent@gmail.com>

From Proetale.

Author: chrisflav

Mathlib.lean

@@ -7167,6 +7167,7 @@ public import Mathlib.Topology.Category.TopCat.Adjunctions
 public import Mathlib.Topology.Category.TopCat.Basic
 public import Mathlib.Topology.Category.TopCat.EffectiveEpi
 public import Mathlib.Topology.Category.TopCat.EpiMono
+public import Mathlib.Topology.Category.TopCat.GrothendieckTopology
 public import Mathlib.Topology.Category.TopCat.Limits.Basic
 public import Mathlib.Topology.Category.TopCat.Limits.Cofiltered
 public import Mathlib.Topology.Category.TopCat.Limits.Konig

Mathlib/CategoryTheory/MorphismProperty/Limits.lean

@@ -171,6 +171,14 @@ theorem IsStableUnderBaseChange.mk' [RespectsIso P]
     rw [← P.cancel_left_of_respectsIso e.inv, sq.flip.isoPullback_inv_fst]
     exact hP₂ _ _ _ f g hg
 
+lemma IsStableUnderBaseChange.of_forall_exists_isPullback {P : MorphismProperty C} [P.RespectsIso]
+    (H : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] (_ : P g),
+      ∃ (T : C) (fst : T ⟶ X) (snd : T ⟶ Y), IsPullback fst snd f g ∧ P fst) :
+    P.IsStableUnderBaseChange := by
+  refine .mk' fun X Y S f g _ hg ↦ ?_
+  obtain ⟨T, fst, snd, h, hfst⟩ := H f g hg
+  rwa [← h.isoPullback_inv_fst, P.cancel_left_of_respectsIso]
+
 variable (C)
 
 instance IsStableUnderBaseChange.isomorphisms :
@@ -295,6 +303,14 @@ theorem IsStableUnderCobaseChange.mk' [RespectsIso P]
     rw [← P.cancel_right_of_respectsIso _ e.hom, sq.flip.inr_isoPushout_hom]
     exact hP₂ _ _ _ f g hf
 
+lemma IsStableUnderCobaseChange.of_forall_exists_isPullback {P : MorphismProperty C} [P.RespectsIso]
+    (H : ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g] (_ : P f),
+      ∃ (T : C) (inl : X ⟶ T) (inr : Y ⟶ T), IsPushout f g inl inr ∧ P inr) :
+    P.IsStableUnderCobaseChange := by
+  refine .mk' fun X Y S f g _ hg ↦ ?_
+  obtain ⟨T, inl, inr, h, hinl⟩ := H f g hg
+  rwa [← h.inr_isoPushout_hom, P.cancel_right_of_respectsIso]
+
 instance IsStableUnderCobaseChange.isomorphisms :
     (isomorphisms C).IsStableUnderCobaseChange where
   of_isPushout {_ _ _ _ f g _ _} h (_ : IsIso f) :=

Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean

@@ -825,6 +825,21 @@ instance (J : Precoverage C) [Small.{w} J] {S : C} (E : ZeroHypercover.{w'} J S)
   use E'.I₀, ZeroHypercover.Small.restrictFun _ ∘ ZeroHypercover.Small.restrictFun _
   exact E'.mem₀
 
+instance {D : Type*} [Category* D] {F : C ⥤ D} (J : Precoverage D) [Small.{w} J] :
+    Small.{w} (J.comap F) where
+  zeroHypercoverSmall {X} E := by
+    refine ⟨(E.map F le_rfl).restrictIndexOfSmall.I₀, ZeroHypercover.Small.restrictFun _, ?_⟩
+    simpa using (E.map F le_rfl).restrictIndexOfSmall.mem₀
+
+lemma Small.inf {J K : Precoverage C} [Small.{w} J]
+    (of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve X⦄, R ≤ S → S ∈ K X → R ∈ K X) :
+    Small.{w} (J ⊓ K) where
+  zeroHypercoverSmall {S} E := by
+    refine ⟨(E.weaken (inf_le_left)).restrictIndexOfSmall.I₀,
+        ZeroHypercover.Small.restrictFun _, ⟨?_, ?_⟩⟩
+    · exact (E.weaken (inf_le_left)).restrictIndexOfSmall.mem₀
+    · exact of_le (by simp) E.mem₀.2
+
 instance [IsStableUnderBaseChange J] : RespectsIso J where
   of_iso {S E F} e h := by
     refine J.mem_coverings_of_isPullback (fun i ↦ E.f (e.inv.s₀ i)) ?_ (𝟙 S) _ (fun i ↦ ?_) ?_

Mathlib/CategoryTheory/Sites/JointlySurjective.lean

@@ -5,7 +5,7 @@ Authors: Christian Merten
 -/
 module
 
-public import Mathlib.CategoryTheory.Sites.Precoverage
+public import Mathlib.CategoryTheory.Sites.Hypercover.Zero
 public import Mathlib.CategoryTheory.Limits.Types.Pullbacks
 
 /-!
@@ -77,6 +77,14 @@ instance : jointlySurjectivePrecoverage.IsStableUnderSup where
     obtain ⟨Y, f, hf, hx⟩ := hR x
     use Y, f, .inl hf
 
+instance : Precoverage.Small.{u} jointlySurjectivePrecoverage.{u} where
+  zeroHypercoverSmall {X} E := by
+    choose i y hy using ofArrows_mem_jointlySurjectivePrecoverage_iff.mp E.mem₀
+    refine ⟨X, i, ?_⟩
+    rw [ofArrows_mem_jointlySurjectivePrecoverage_iff]
+    intro x
+    use x, y x, hy x
+
 end Types
 
 variable {C : Type*} [Category* C] (F : C ⥤ Type u)

Mathlib/Topology/Category/TopCat/GrothendieckTopology.lean

@@ -0,0 +1,120 @@
+/-
+Copyright (c) 2026 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Edward van de Meent, Christian Merten
+-/
+module
+
+public import Mathlib.CategoryTheory.Sites.Canonical
+public import Mathlib.CategoryTheory.Sites.JointlySurjective
+public import Mathlib.CategoryTheory.Sites.MorphismProperty
+public import Mathlib.Topology.Category.TopCat.Limits.Pullbacks
+
+/-!
+
+# The Grothendieck topology on `TopCat`
+
+In this file we define the standard Grothendieck topology on `TopCat`. This is the topology
+generated by families of jointly surjective open embeddings.
+
+## Main definitions and results
+
+- `TopCat.isOpenEmbedding`: The morphism property in `TopCat` given by open embeddings.
+- `TopCat.grothendieckTopology`: The Grothendieck topology generated by families of jointly
+  surjective open embeddings.
+- `TopCat.subcanonical_grothendieckTopology`: The Grothendieck topology on `TopCat` is subcanonical.
+
+## TODOs
+
+- Define the étale precoverage on `TopCat` (replace open embedding by local homeomorphism
+  in the definition of the Grothendieck topology) and show it induces the same Grothendieck
+  topology.
+
+-/
+
+@[expose] public section
+
+universe u
+
+open CategoryTheory Limits
+
+namespace TopCat
+
+/-- The morphism property on the category of topological spaces given by open embeddings. -/
+def isOpenEmbedding : MorphismProperty TopCat :=
+  fun _ _ f ↦ Topology.IsOpenEmbedding f
+
+@[simp]
+lemma isOpenEmbedding_iff {X Y : TopCat} (f : X ⟶ Y) :
+    isOpenEmbedding f ↔ Topology.IsOpenEmbedding f := .rfl
+
+instance : isOpenEmbedding.IsMultiplicative where
+  id_mem _ := .id
+  comp_mem _ _ hf hg := hg.comp hf
+
+instance : isOpenEmbedding.RespectsIso :=
+  MorphismProperty.respectsIso_of_isStableUnderComposition fun _ _ f (_ : IsIso f) ↦
+    (TopCat.homeoOfIso (asIso f)).isOpenEmbedding
+
+instance : isOpenEmbedding.IsStableUnderBaseChange :=
+  .mk' fun _ _ _ _ _ _ hg ↦ fst_isOpenEmbedding_of_right _ hg
+
+/-- The precoverage on `TopCat` given by jointly surjective families of open embeddings. -/
+def precoverage : Precoverage TopCat.{u} :=
+    Types.jointlySurjectivePrecoverage.comap (forget TopCat) ⊓ isOpenEmbedding.precoverage
+  deriving Precoverage.HasIsos, Precoverage.IsStableUnderBaseChange,
+    Precoverage.IsStableUnderComposition
+
+/-- The Grothendieck topology on the category of topological spaces is the topology given by
+jointly surjective open embeddings. -/
+abbrev grothendieckTopology : GrothendieckTopology TopCat.{u} :=
+  precoverage.toGrothendieck
+
+lemma exists_mem_zeroHypercover_range {X : TopCat} (E : precoverage.ZeroHypercover X) :
+    ∀ x, ∃ (i : E.I₀), x ∈ Set.range (E.f i) := by
+  simpa using E.mem₀.left
+
+lemma isOpenEmbedding_f_zeroHypercover {X : TopCat} (E : precoverage.ZeroHypercover X) :
+    ∀ i, Topology.IsOpenEmbedding (E.f i) := by
+  simpa using E.mem₀.right
+
+instance : Precoverage.Small.{u} precoverage.{u} :=
+  .inf fun _ _ _ hRS hS _ _ hf ↦ hS (hRS _ hf)
+
+/-- The Grothendieck topology on `TopCat` is subcanonical. -/
+instance subcanonical_grothendieckTopology : grothendieckTopology.Subcanonical := by
+  refine .of_isSheaf_yoneda_obj _ fun X ↦ ?_
+  rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small]
+  intro Y 𝒰
+  rw [Presieve.isSheafFor_arrows_iff]
+  have heq (i y) : 𝒰.f i y = (Subtype.val : Set.range (𝒰.f i) → Y) ⟨𝒰.f i y, by simp⟩ := rfl
+  refine fun x hx ↦ ⟨?_, fun i ↦ ?_, fun f hf ↦ ?_⟩
+  · refine ofHom <| ContinuousMap.liftCover (fun i ↦ Set.range (𝒰.f i)) ?_ ?_ ?_
+    · intro i
+      exact ⟨(x i).hom ∘ (isOpenEmbedding_f_zeroHypercover 𝒰 i).toHomeomorph.symm, by fun_prop⟩
+    · intro i j y
+      simp only [Set.mem_range, ContinuousMap.coe_mk, Function.comp_apply, forall_exists_index]
+      intro xi hi xj hj
+      conv_lhs => simp only [← hi]
+      conv_rhs => simp only [← hj]
+      have := hx i j _ (TopCat.pullbackCone (𝒰.f i) (𝒰.f j)).fst
+        (TopCat.pullbackCone (𝒰.f i) (𝒰.f j)).snd (TopCat.pullbackCone (𝒰.f i) (𝒰.f j)).condition
+      dsimp at this
+      simpa using congr($(this) ⟨(xi, xj), hi ▸ hj.symm⟩)
+    · intro x
+      obtain ⟨i, hi⟩ := exists_mem_zeroHypercover_range 𝒰 x
+      exact ⟨i, (isOpenEmbedding_f_zeroHypercover 𝒰 i).isOpen_range.mem_nhds hi⟩
+  · dsimp
+    ext
+    simp only [hom_comp, hom_ofHom, ContinuousMap.comp_apply]
+    rw [heq, ContinuousMap.liftCover_coe]
+    simp
+  · dsimp
+    ext x
+    obtain ⟨i, y, rfl⟩ := exists_mem_zeroHypercover_range 𝒰 x
+    have := congr($(hf i).hom y)
+    dsimp at this ⊢
+    rw [this, heq, ContinuousMap.liftCover_coe]
+    simp
+
+end TopCat

Mathlib/Topology/Homeomorph/Lemmas.lean

@@ -432,6 +432,11 @@ noncomputable def toHomeomorph {f : X → Y} (hf : IsEmbedding f) :
   Equiv.ofInjective f hf.injective |>.toHomeomorphOfIsInducing <|
     IsInducing.subtypeVal.of_comp_iff.mp hf.toIsInducing
 
+@[simp]
+lemma toHomeomorph_symm_apply {f : X → Y} (hf : IsEmbedding f) (x : X) :
+    hf.toHomeomorph.symm ⟨f x, by simp⟩ = x :=
+  hf.toHomeomorph.injective (by ext; simp)
+
 /-- A surjective embedding is a homeomorphism. -/
 @[simps! apply]
 noncomputable def toHomeomorphOfSurjective {f : X → Y}
@@ -454,6 +459,18 @@ theorem homeomorphOfSubsetRange_apply_coe {f : X → Y} (hf : IsEmbedding f)
 
 end Topology.IsEmbedding
 
+lemma Topology.IsEmbedding.uliftMap {f : X → Y} (hf : IsEmbedding f) :
+    IsEmbedding (ULift.map f) :=
+  .comp Homeomorph.ulift.symm.isEmbedding (.comp hf <| Homeomorph.ulift.isEmbedding)
+
+lemma Topology.IsOpenEmbedding.uliftMap {f : X → Y} (hf : IsOpenEmbedding f) :
+    IsOpenEmbedding (ULift.map f) :=
+  .comp Homeomorph.ulift.symm.isOpenEmbedding (.comp hf <| Homeomorph.ulift.isOpenEmbedding)
+
+lemma Topology.IsClosedEmbedding.uliftMap {f : X → Y} (hf : IsClosedEmbedding f) :
+    IsClosedEmbedding (ULift.map f) :=
+  .comp Homeomorph.ulift.symm.isClosedEmbedding (.comp hf <| Homeomorph.ulift.isClosedEmbedding)
+
 end
 
 namespace Continuous