feat(AlgebraicGeometry): zero locus of sections and characterisation of nilpotent elements (#14337)

Introduces the zero locus of a set of sections on a ringed space and characterizes nilpotent sections
over compact opens of a scheme in terms of basic opens and the zero locus.

Co-authored-by: Andrew Yang @erdOne

Author: chrisflav

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -273,11 +273,6 @@ theorem range_fromSpec :
   infer_instance
 #align algebraic_geometry.is_affine_open.from_Spec_range AlgebraicGeometry.IsAffineOpen.range_fromSpec
 
-@[simp]
-theorem fromSpec_image_top : hU.fromSpec ''ᵁ ⊤ = U :=
-  Opens.ext (Set.image_univ.trans (range_fromSpec hU))
-#align algebraic_geometry.is_affine_open.from_Spec_image_top AlgebraicGeometry.IsAffineOpen.fromSpec_image_top
-
 @[simp]
 theorem opensRange_fromSpec : Scheme.Hom.opensRange hU.fromSpec = U := Opens.ext (range_fromSpec hU)
 
@@ -669,6 +664,39 @@ theorem of_affine_open_cover {X : Scheme} {P : X.affineOpens → Prop}
   exact ⟨_, hf₁ ⟨x, hx⟩⟩
 #align algebraic_geometry.of_affine_open_cover AlgebraicGeometry.of_affine_open_cover
 
+section ZeroLocus
+
+/-- On a locally ringed space `X`, the preimage of the zero locus of the prime spectrum
+of `Γ(X, ⊤)` under `toΓSpecFun` agrees with the associated zero locus on `X`. -/
+lemma Scheme.toΓSpec_preimage_zeroLocus_eq {X : Scheme.{u}} (s : Set Γ(X, ⊤)) :
+    (ΓSpec.adjunction.unit.app X).val.base ⁻¹' PrimeSpectrum.zeroLocus s = X.zeroLocus s :=
+  LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq s
+
+open ConcreteCategory
+
+/-- If `X` is affine, the image of the zero locus of global sections of `X` under `toΓSpecFun`
+is the zero locus in terms of the prime spectrum of `Γ(X, ⊤)`. -/
+lemma Scheme.toΓSpec_image_zeroLocus_eq_of_isAffine {X : Scheme.{u}} [IsAffine X] (s : Set Γ(X, ⊤)) :
+    X.isoSpec.hom.val.base '' X.zeroLocus s = PrimeSpectrum.zeroLocus s := by
+  erw [← X.toΓSpec_preimage_zeroLocus_eq, Set.image_preimage_eq]
+  exact (bijective_of_isIso X.isoSpec.hom.val.base).surjective
+
+/-- If `X` is an affine scheme, every closed set of `X` is the zero locus
+of a set of global sections. -/
+lemma Scheme.eq_zeroLocus_of_isClosed_of_isAffine (X : Scheme.{u}) [IsAffine X] (s : Set X) :
+    IsClosed s ↔ ∃ I : Ideal (Γ(X, ⊤)), s = X.zeroLocus (I : Set Γ(X, ⊤)) := by
+  refine ⟨fun hs ↦ ?_, ?_⟩
+  · let Z : Set (Spec <| Γ(X, ⊤)) := X.toΓSpecFun '' s
+    have hZ : IsClosed Z := (X.isoSpec.hom.homeomorph).isClosedMap _ hs
+    obtain ⟨I, (hI : Z = _)⟩ := (PrimeSpectrum.isClosed_iff_zeroLocus_ideal _).mp hZ
+    use I
+    simp only [← Scheme.toΓSpec_preimage_zeroLocus_eq, ← hI, Z]
+    erw [Set.preimage_image_eq _ (bijective_of_isIso X.isoSpec.hom.val.base).injective]
+  · rintro ⟨I, rfl⟩
+    exact zeroLocus_isClosed X I.carrier
+
+end ZeroLocus
+
 @[deprecated (since := "2024-06-21"), nolint defLemma]
 alias isAffineAffineScheme := isAffine_affineScheme
 @[deprecated (since := "2024-06-21"), nolint defLemma]

Mathlib/AlgebraicGeometry/Cover/Open.lean

@@ -397,6 +397,44 @@ def OpenCover.fromAffineRefinement {X : Scheme.{u}} (𝓤 : X.OpenCover) :
   idx j := j.fst
   app j := (𝓤.obj j.fst).affineCover.map _
 
+/-- If two global sections agree after restriction to each member of a finite open cover, then
+they agree globally. -/
+lemma OpenCover.ext_elem {X : Scheme.{u}} {U : Opens X} (f g : Γ(X, U)) (𝒰 : X.OpenCover)
+    (h : ∀ i : 𝒰.J, (𝒰.map i).app U f = (𝒰.map i).app U g) : f = g := by
+  fapply TopCat.Sheaf.eq_of_locally_eq' X.sheaf
+    (fun i ↦ (𝒰.map (𝒰.f i)).opensRange ⊓ U) _ (fun _ ↦ homOfLE inf_le_right)
+  · intro x hx
+    simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_inf, Hom.opensRange_coe, Opens.coe_mk,
+      Set.mem_iUnion, Set.mem_inter_iff, Set.mem_range, SetLike.mem_coe, exists_and_right]
+    refine ⟨?_, hx⟩
+    simpa using ⟨_, 𝒰.covers x⟩
+  · intro x;
+    replace h := h (𝒰.f x)
+    rw [← IsOpenImmersion.map_ΓIso_inv] at h
+    exact (IsOpenImmersion.ΓIso (𝒰.map (𝒰.f x)) U).commRingCatIsoToRingEquiv.symm.injective h
+
+/-- If the restriction of a global section to each member of an open cover is zero, then it is
+globally zero. -/
+lemma zero_of_zero_cover {X : Scheme.{u}} {U : Opens X} (s : Γ(X, U)) (𝒰 : X.OpenCover)
+    (h : ∀ i : 𝒰.J, (𝒰.map i).app U s = 0) : s = 0 :=
+  𝒰.ext_elem s 0 (fun i ↦ by rw [map_zero]; exact h i)
+
+/-- If a global section is nilpotent on each member of a finite open cover, then `f` is
+nilpotent. -/
+lemma isNilpotent_of_isNilpotent_cover {X : Scheme.{u}} {U : Opens X} (s : Γ(X, U))
+    (𝒰 : X.OpenCover) [Finite 𝒰.J] (h : ∀ i : 𝒰.J, IsNilpotent ((𝒰.map i).app U s)) :
+    IsNilpotent s := by
+  choose fn hfn using h
+  have : Fintype 𝒰.J := Fintype.ofFinite 𝒰.J
+  /- the maximum of all `fn i` (exists, because `𝒰.J` is finite) -/
+  let N : ℕ := Finset.sup Finset.univ fn
+  have hfnleN (i : 𝒰.J) : fn i ≤ N := Finset.le_sup (Finset.mem_univ i)
+  use N
+  apply zero_of_zero_cover
+  intro i
+  simp only [map_pow]
+  exact pow_eq_zero_of_le (hfnleN i) (hfn i)
+
 section deprecated
 
 /-- The basic open sets form an affine open cover of `Spec R`. -/

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -81,17 +81,17 @@ theorem not_mem_prime_iff_unit_in_stalk (r : Γ.obj (op X)) (x : X) :
 
 /-- The preimage of a basic open in `Spec Γ(X)` under the unit is the basic
 open in `X` defined by the same element (they are equal as sets). -/
-theorem toΓSpec_preim_basicOpen_eq (r : Γ.obj (op X)) :
+theorem toΓSpec_preimage_basicOpen_eq (r : Γ.obj (op X)) :
     X.toΓSpecFun ⁻¹' (basicOpen r).1 = (X.toRingedSpace.basicOpen r).1 := by
       ext
       erw [X.toRingedSpace.mem_top_basicOpen]; apply not_mem_prime_iff_unit_in_stalk
-#align algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_preim_basic_open_eq AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preim_basicOpen_eq
+#align algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_preim_basic_open_eq AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq
 
 /-- `toΓSpecFun` is continuous. -/
 theorem toΓSpec_continuous : Continuous X.toΓSpecFun := by
   rw [isTopologicalBasis_basic_opens.continuous_iff]
   rintro _ ⟨r, rfl⟩
-  erw [X.toΓSpec_preim_basicOpen_eq r]
+  erw [X.toΓSpec_preimage_basicOpen_eq r]
   exact (X.toRingedSpace.basicOpen r).2
 #align algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_continuous AlgebraicGeometry.LocallyRingedSpace.toΓSpec_continuous
 
@@ -115,7 +115,7 @@ abbrev toΓSpecMapBasicOpen : Opens X :=
 
 /-- The preimage is the basic open in `X` defined by the same element `r`. -/
 theorem toΓSpecMapBasicOpen_eq : X.toΓSpecMapBasicOpen r = X.toRingedSpace.basicOpen r :=
-  Opens.ext (X.toΓSpec_preim_basicOpen_eq r)
+  Opens.ext (X.toΓSpec_preimage_basicOpen_eq r)
 #align algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_map_basic_open_eq AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq
 
 /-- The map from the global sections `Γ(X)` to the sections on the (preimage of) a basic open. -/
@@ -255,6 +255,23 @@ def toΓSpec : X ⟶ Spec.locallyRingedSpaceObj (Γ.obj (op X)) where
     exact ht.mul <| this.map _
 #align algebraic_geometry.LocallyRingedSpace.to_Γ_Spec AlgebraicGeometry.LocallyRingedSpace.toΓSpec
 
+/-- On a locally ringed space `X`, the preimage of the zero locus of the prime spectrum
+of `Γ(X, ⊤)` under `toΓSpec` agrees with the associated zero locus on `X`. -/
+lemma toΓSpec_preimage_zeroLocus_eq {X : LocallyRingedSpace.{u}}
+    (s : Set (X.presheaf.obj (op ⊤))) :
+    X.toΓSpec.val.base ⁻¹' PrimeSpectrum.zeroLocus s = X.toRingedSpace.zeroLocus s := by
+  simp only [RingedSpace.zeroLocus]
+  have (i : LocallyRingedSpace.Γ.obj (op X)) (_ : i ∈ s) :
+      ((X.toRingedSpace.basicOpen i).carrier)ᶜ =
+        X.toΓSpec.val.base ⁻¹' (PrimeSpectrum.basicOpen i).carrierᶜ := by
+    symm
+    erw [Set.preimage_compl, X.toΓSpec_preimage_basicOpen_eq i]
+  erw [Set.iInter₂_congr this]
+  simp_rw [← Set.preimage_iInter₂, Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
+    compl_compl]
+  rw [← PrimeSpectrum.zeroLocus_iUnion₂]
+  simp
+
 theorem comp_ring_hom_ext {X : LocallyRingedSpace.{u}} {R : CommRingCat.{u}} {f : R ⟶ Γ.obj (op X)}
     {β : X ⟶ Spec.locallyRingedSpaceObj R}
     (w : X.toΓSpec.1.base ≫ (Spec.locallyRingedSpaceMap f).1.base = β.1.base)
@@ -596,4 +613,8 @@ instance Spec.reflective : Reflective Scheme.Spec where
   adj := ΓSpec.adjunction
 #align algebraic_geometry.Spec.reflective AlgebraicGeometry.Spec.reflective
 
+@[deprecated (since := "2024-07-02")]
+alias LocallyRingedSpace.toΓSpec_preim_basicOpen_eq :=
+  LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq
+
 end AlgebraicGeometry

Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

@@ -341,4 +341,30 @@ theorem exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact (X : Scheme
   apply Finset.le_sup (Finset.mem_univ i)
 #align algebraic_geometry.exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_compact AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact
 
+/-- A section over a compact open of a scheme is nilpotent if and only if its associated
+basic open is empty. -/
+lemma Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact {X : Scheme.{u}}
+    {U : Opens X} (hU : IsCompact U.carrier) (f : Γ(X, U)) :
+    IsNilpotent f ↔ X.basicOpen f = ⊥ := by
+  refine ⟨X.basicOpen_eq_bot_of_isNilpotent U f, fun hf ↦ ?_⟩
+  have h : (1 : Γ(X, U)) |_ X.basicOpen f = (0 : Γ(X, X.basicOpen f)) := by
+    have e : X.basicOpen f ≤ ⊥ := by rw [hf]
+    rw [← X.presheaf.restrict_restrict e bot_le]
+    have : Subsingleton Γ(X, ⊥) :=
+      CommRingCat.subsingleton_of_isTerminal X.sheaf.isTerminalOfEmpty
+    rw [Subsingleton.eq_zero (1 |_ ⊥)]
+    show X.presheaf.map _ 0 = 0
+    rw [map_zero]
+  obtain ⟨n, hn⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact X hU 1 f h
+  rw [mul_one] at hn
+  use n
+
+/-- The zero locus of a set of sections over a compact open of a scheme is `X` if and only if
+`s` is contained in the nilradical of `Γ(X, U)`. -/
+lemma Scheme.zeroLocus_eq_top_iff_subset_nilradical_of_isCompact {X : Scheme.{u}} {U : Opens X}
+    (hU : IsCompact U.carrier) (s : Set Γ(X, U)) :
+    X.zeroLocus s = ⊤ ↔ s ⊆ (nilradical Γ(X, U)).carrier := by
+  simp [Scheme.zeroLocus_def, ← Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact hU,
+    ← mem_nilradical, Set.subset_def]
+
 end AlgebraicGeometry

Mathlib/AlgebraicGeometry/OpenImmersion.lean

@@ -94,6 +94,29 @@ abbrev opensFunctor : Opens X ⥤ Opens Y :=
 /-- `f ''ᵁ U` is notation for the image (as an open set) of `U` under an open immersion `f`. -/
 scoped[AlgebraicGeometry] notation3:90 f:91 " ''ᵁ " U:90 => (Scheme.Hom.opensFunctor f).obj U
 
+lemma image_le_image_of_le {U V : Opens X} (e : U ≤ V) : f ''ᵁ U ≤ f ''ᵁ V := by
+  rintro a ⟨u, hu, rfl⟩
+  exact Set.mem_image_of_mem (⇑f.val.base) (e hu)
+
+@[simp]
+lemma opensFunctor_map_homOfLE {U V : Opens X} (e : U ≤ V) :
+    (Scheme.Hom.opensFunctor f).map (homOfLE e) = homOfLE (f.image_le_image_of_le e) :=
+  rfl
+
+@[simp]
+lemma image_top_eq_opensRange : f ''ᵁ ⊤ = f.opensRange := by
+  apply Opens.ext
+  simp
+
+@[simp]
+lemma preimage_image_eq (U : Opens X) : f ⁻¹ᵁ f ''ᵁ U = U := by
+  apply Opens.ext
+  simp [Set.preimage_image_eq _ f.openEmbedding.inj]
+
+lemma image_preimage_eq_opensRange_inter (U : Opens Y) : f ''ᵁ f ⁻¹ᵁ U = f.opensRange ⊓ U := by
+  apply Opens.ext
+  simp [Set.image_preimage_eq_range_inter]
+
 /-- The isomorphism `Γ(X, U) ⟶ Γ(Y, f(U))` induced by an open immersion `f : X ⟶ Y`. -/
 def invApp (U) : Γ(X, U) ⟶ Γ(Y, f ''ᵁ U) :=
   LocallyRingedSpace.IsOpenImmersion.invApp f U
@@ -131,6 +154,17 @@ theorem invApp_app (U) :
       (eqToHom (Opens.ext <| by exact Set.preimage_image_eq U.1 H.base_open.inj)).op :=
   (PresheafedSpace.IsOpenImmersion.invApp_app _ _).trans (by rw [eqToHom_op])
 
+@[reassoc (attr := simp), elementwise]
+lemma appLE_invApp {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] {U : Opens Y}
+    {V : Opens X} (e : V ≤ f ⁻¹ᵁ U) :
+    Scheme.Hom.appLE f U V e ≫ Scheme.Hom.invApp f V =
+        Y.presheaf.map (homOfLE <| (f.image_le_image_of_le e).trans
+          (f.image_preimage_eq_opensRange_inter U ▸ inf_le_right)).op := by
+  simp only [Scheme.Hom.appLE, Category.assoc, Scheme.Hom.invApp_naturality, Functor.op_obj,
+    Functor.op_map, Quiver.Hom.unop_op, Scheme.Hom.opensFunctor_map_homOfLE,
+    Scheme.Hom.app_invApp_assoc, Opens.carrier_eq_coe]
+  erw [← Functor.map_comp, ← op_comp, homOfLE_comp]
+
 end Scheme.Hom
 
 /-- The open sets of an open subscheme corresponds to the open sets containing in the image. -/
@@ -547,6 +581,33 @@ theorem lift_app {X Y U : Scheme.{u}} (f : U ⟶ Y) (g : X ⟶ Y) [IsOpenImmersi
   IsOpenImmersion.app_eq_invApp_app_of_comp_eq _ _ _ (lift_fac _ _ _).symm _
 #align algebraic_geometry.IsOpenImmersion.lift_app AlgebraicGeometry.IsOpenImmersion.lift_app
 
+/-- If `f` is an open immersion `X ⟶ Y`, the global sections of `X`
+are naturally isomorphic to the sections of `Y` over the image of `f`. -/
+noncomputable
+def ΓIso {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : Opens Y) :
+    Γ(X, f⁻¹ᵁ U) ≅ Γ(Y, f.opensRange ⊓ U) :=
+  asIso (Scheme.Hom.invApp f <| f⁻¹ᵁ U) ≪≫
+    Y.presheaf.mapIso (eqToIso <| (f.image_preimage_eq_opensRange_inter U).symm).op
+
+@[simp]
+lemma ΓIso_inv {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : Opens Y) :
+    (ΓIso f U).inv = f.appLE (f.opensRange ⊓ U) (f⁻¹ᵁ U)
+      (by rw [← f.image_preimage_eq_opensRange_inter, f.preimage_image_eq]) := by
+  simp only [ΓIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, eqToIso.inv, eqToHom_op,
+    asIso_inv, IsIso.comp_inv_eq, Scheme.Hom.appLE_invApp]
+  rfl
+
+@[reassoc, elementwise]
+lemma map_ΓIso_inv {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : Opens Y) :
+    Y.presheaf.map (homOfLE inf_le_right).op ≫ (ΓIso f U).inv = f.app U := by
+  simp [Scheme.Hom.appLE_eq_app]
+
+@[reassoc, elementwise]
+lemma ΓIso_hom_map {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : Opens Y) :
+    f.app U ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE inf_le_right).op := by
+  rw [← map_ΓIso_inv]
+  simp [-ΓIso_inv]
+
 end IsOpenImmersion
 
 namespace Scheme

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -320,6 +320,19 @@ theorem vanishingIdeal_eq_top_iff {s : Set (PrimeSpectrum R)} : vanishingIdeal s
     Set.subset_empty_iff]
 #align prime_spectrum.vanishing_ideal_eq_top_iff PrimeSpectrum.vanishingIdeal_eq_top_iff
 
+theorem zeroLocus_eq_top_iff (s : Set R) :
+    zeroLocus s = ⊤ ↔ s ⊆ nilradical R := by
+  constructor
+  · intro h x hx
+    refine nilpotent_iff_mem_prime.mpr (fun J hJ ↦ ?_)
+    have hJz : ⟨J, hJ⟩ ∈ zeroLocus s := by
+      rw [h]
+      trivial
+    exact (mem_zeroLocus _ _).mpr hJz hx
+  · rw [eq_top_iff]
+    intro h p _
+    apply Set.Subset.trans h (nilradical_le_prime p.asIdeal)
+
 theorem zeroLocus_sup (I J : Ideal R) :
     zeroLocus ((I ⊔ J : Ideal R) : Set R) = zeroLocus I ∩ zeroLocus J :=
   (gc R).l_sup
@@ -344,6 +357,10 @@ theorem zeroLocus_iUnion {ι : Sort*} (s : ι → Set R) :
   (gc_set R).l_iSup
 #align prime_spectrum.zero_locus_Union PrimeSpectrum.zeroLocus_iUnion
 
+theorem zeroLocus_iUnion₂ {ι : Sort*} {κ : (i : ι) → Sort*} (s : ∀ i, κ i → Set R) :
+    zeroLocus (⋃ (i) (j), s i j) = ⋂ (i) (j), zeroLocus (s i j) :=
+  (gc_set R).l_iSup₂
+
 theorem zeroLocus_bUnion (s : Set (Set R)) :
     zeroLocus (⋃ s' ∈ s, s' : Set R) = ⋂ s' ∈ s, zeroLocus s' := by simp only [zeroLocus_iUnion]
 #align prime_spectrum.zero_locus_bUnion PrimeSpectrum.zeroLocus_bUnion

Mathlib/AlgebraicGeometry/Restrict.lean

@@ -44,6 +44,16 @@ notation3:60 X:60 " ∣_ᵤ " U:61 => Scheme.restrict X (U : Opens X).openEmbedd
 /-- The restriction of a scheme to an open subset. -/
 abbrev Scheme.ιOpens {X : Scheme.{u}} (U : Opens X) : X ∣_ᵤ U ⟶ X := X.ofRestrict _
 
+lemma Scheme.ιOpens_image_top {X : Scheme.{u}} (U : Opens X) : (Scheme.ιOpens U) ''ᵁ ⊤ = U :=
+  U.openEmbedding_obj_top
+
+instance Scheme.ιOpens_appLE_isIso {X : Scheme.{u}} (U : Opens X) :
+    IsIso ((Scheme.ιOpens U).appLE U ⊤ (by simp)) := by
+  simp only [restrict_presheaf_obj, ofRestrict_appLE]
+  have : IsIso (homOfLE <| le_of_eq (ιOpens_image_top U)) :=
+    homOfLE_isIso_of_eq _ <| ιOpens_image_top U
+  infer_instance
+
 lemma Scheme.ofRestrict_app_self {X : Scheme.{u}} (U : Opens X) :
     (ιOpens U).app U = X.presheaf.map (eqToHom (by simp)).op := rfl
 
@@ -86,7 +96,6 @@ lemma Scheme.map_basicOpen_map (X : Scheme.{u}) (U : Opens X) (r : Γ(X, U)) :
       X.presheaf.map (eqToHom U.openEmbedding_obj_top).op r) = X.basicOpen r := by
   rw [Scheme.map_basicOpen', Scheme.basicOpen_res_eq, Scheme.basicOpen_res_eq]
 
-
 -- Porting note: `simps` can't synthesize `obj_left, obj_hom, mapLeft`
 /-- The functor taking open subsets of `X` to open subschemes of `X`. -/
 -- @[simps obj_left obj_hom mapLeft]