feat(algebraic_geometry): Basic open set is empty iff section is zero in reduced schemes. (#11012)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: erdOne

src/algebraic_geometry/locally_ringed_space.lean

@@ -237,6 +237,18 @@ begin
     exact (is_unit_map_iff (PresheafedSpace.stalk_map f.1 _) _).mp hy }
 end
 
+-- This actually holds for all ringed spaces with nontrivial stalks.
+@[simp] lemma basic_open_zero (X : LocallyRingedSpace) (U : opens X.carrier) :
+  X.to_RingedSpace.basic_open (0 : X.presheaf.obj $ op U) = ∅ :=
+begin
+  ext,
+  simp only [set.mem_empty_eq, topological_space.opens.empty_eq, topological_space.opens.mem_coe,
+    opens.coe_bot, iff_false, RingedSpace.basic_open, is_unit_zero_iff, set.mem_set_of_eq,
+    map_zero],
+  rintro ⟨⟨y, _⟩, h, e⟩,
+  exact @zero_ne_one (X.presheaf.stalk y) _ _ h,
+end
+
 instance component_nontrivial (X : LocallyRingedSpace) (U : opens X.carrier)
   [hU : nonempty U] : nontrivial (X.presheaf.obj $ op U) :=
 (X.to_PresheafedSpace.presheaf.germ hU.some).domain_nontrivial

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -8,6 +8,7 @@ import ring_theory.ideal.prod
 import ring_theory.ideal.over
 import linear_algebra.finsupp
 import algebra.punit_instances
+import ring_theory.nilpotent
 import topology.sober
 
 /-!
@@ -604,7 +605,7 @@ set.ext $ λ x, by simpa only [set.mem_compl_eq, mem_zero_locus, set.singleton_s
 topological_space.opens.ext $ by {simp, refl}
 
 @[simp] lemma basic_open_zero : basic_open (0 : R) = ⊥ :=
-topological_space.opens.ext $ by {simp, refl}
+topological_space.opens.ext $ by simp
 
 lemma basic_open_le_basic_open_iff (f g : R) :
   basic_open f ≤ basic_open g ↔ f ∈ (ideal.span ({g} : set R)).radical :=
@@ -669,6 +670,17 @@ begin
   exact ⟨n, hs⟩
 end
 
+@[simp]
+lemma basic_open_eq_bot_iff (f : R) :
+  basic_open f = ⊥ ↔ is_nilpotent f :=
+begin
+  rw [← subtype.coe_injective.eq_iff, basic_open_eq_zero_locus_compl],
+  simp only [set.eq_univ_iff_forall, topological_space.opens.empty_eq, set.singleton_subset_iff,
+    topological_space.opens.coe_bot, nilpotent_iff_mem_prime, set.compl_empty_iff, mem_zero_locus,
+    set_like.mem_coe],
+  exact subtype.forall,
+end
+
 lemma localization_away_comap_range (S : Type v) [comm_ring S] [algebra R S] (r : R)
   [is_localization.away r S] : set.range (comap (algebra_map R S)) = basic_open r :=
 begin

src/algebraic_geometry/properties.lean

@@ -96,6 +96,115 @@ begin
   rw [comp_apply, e', map_zero]
 end
 
+lemma is_reduced_of_open_immersion {X Y : Scheme} (f : X ⟶ Y) [H : is_open_immersion f]
+  [is_reduced Y] : is_reduced X :=
+begin
+  constructor,
+  intro U,
+  have : U = (opens.map f.1.base).obj (H.base_open.is_open_map.functor.obj U),
+  { ext1, exact (set.preimage_image_eq _ H.base_open.inj).symm },
+  rw this,
+  exact is_reduced_of_injective (inv $ f.1.c.app (op $ H.base_open.is_open_map.functor.obj U))
+    (as_iso $ f.1.c.app (op $ H.base_open.is_open_map.functor.obj U) : Y.presheaf.obj _ ≅ _).symm
+      .CommRing_iso_to_ring_equiv.injective
+end
+
+local attribute [elementwise] category_theory.is_iso.hom_inv_id
+
+lemma basic_open_eq_of_affine {R : CommRing} (f : R) :
+  RingedSpace.basic_open (Spec.to_SheafedSpace.obj (op R)) ((Spec_Γ_identity.app R).inv f) =
+    prime_spectrum.basic_open f :=
+begin
+  ext,
+  change ↑(⟨x, trivial⟩ : (⊤ : opens _)) ∈
+    RingedSpace.basic_open (Spec.to_SheafedSpace.obj (op R)) _ ↔ _,
+  rw RingedSpace.mem_basic_open,
+  suffices : is_unit (structure_sheaf.to_stalk R x f) ↔ f ∉ prime_spectrum.as_ideal x,
+  { exact this },
+  erw [← is_unit_map_iff (structure_sheaf.stalk_to_fiber_ring_hom R x),
+    structure_sheaf.stalk_to_fiber_ring_hom_to_stalk],
+  exact (is_localization.at_prime.is_unit_to_map_iff
+    (localization.at_prime (prime_spectrum.as_ideal x)) (prime_spectrum.as_ideal x) f : _)
+end
+
+lemma basic_open_eq_of_affine' {R : CommRing}
+  (f : (Spec.to_SheafedSpace.obj (op R)).presheaf.obj (op ⊤)) :
+  RingedSpace.basic_open (Spec.to_SheafedSpace.obj (op R)) f =
+    prime_spectrum.basic_open ((Spec_Γ_identity.app R).hom f) :=
+begin
+  convert basic_open_eq_of_affine ((Spec_Γ_identity.app R).hom f),
+  exact (coe_hom_inv_id _ _).symm
+end
+
+lemma reduce_to_affine_global (P : ∀ (X : Scheme) (U : opens X.carrier), Prop)
+  (h₁ : ∀ (X : Scheme) (U : opens X.carrier),
+    (∀ (x : U), ∃ {V} (h : x.1 ∈ V) (i : V ⟶ U), P X V) → P X U)
+  (h₂ : ∀ {X Y} (f : X ⟶ Y) [hf : is_open_immersion f], ∃ {U : set X.carrier} {V : set Y.carrier}
+    (hU : U = ⊤) (hV : V = set.range f.1.base), P X ⟨U, hU.symm ▸ is_open_univ⟩ →
+      P Y ⟨V, hV.symm ▸ hf.base_open.open_range⟩)
+  (h₃ : ∀ (R : CommRing), P (Scheme.Spec.obj $ op R) ⊤) :
+  ∀ (X : Scheme) (U : opens X.carrier), P X U :=
+begin
+  intros X U,
+  apply h₁,
+  intro x,
+  obtain ⟨_,⟨j,rfl⟩,hx,i⟩ := X.affine_basis_cover_is_basis.exists_subset_of_mem_open x.prop U.2,
+  let U' : opens _ := ⟨_, (X.affine_basis_cover.is_open j).base_open.open_range⟩,
+  let i' : U' ⟶ U :=
+    hom_of_le i,
+  refine ⟨U', hx, i', _⟩,
+  obtain ⟨_,_,rfl,rfl,h₂'⟩ := h₂ (X.affine_basis_cover.map j),
+  apply h₂',
+  apply h₃
+end
+
+lemma eq_zero_of_basic_open_empty {X : Scheme} [hX : is_reduced X] {U : opens X.carrier}
+  (s : X.presheaf.obj (op U)) (hs : X.to_LocallyRingedSpace.to_RingedSpace.basic_open s = ∅) :
+  s = 0 :=
+begin
+  apply Top.presheaf.section_ext X.sheaf U,
+  simp_rw ring_hom.map_zero,
+  tactic.unfreeze_local_instances,
+  revert X U hX s,
+  refine reduce_to_affine_global _ _ _ _,
+  { intros X U hx hX s hs x,
+    obtain ⟨V, hx, i, H⟩ := hx x,
+    specialize H (X.presheaf.map i.op s),
+    erw RingedSpace.basic_open_res at H,
+    rw [hs, ← subtype.coe_injective.eq_iff, opens.empty_eq, opens.inter_eq, inf_bot_eq] at H,
+    specialize H rfl ⟨x, hx⟩,
+    erw Top.presheaf.germ_res_apply at H,
+    exact H },
+  { rintros X Y f hf,
+    have e : (f.val.base) ⁻¹' set.range ⇑(f.val.base) = ⊤,
+    { rw [← set.image_univ, set.preimage_image_eq _ hf.base_open.inj, set.top_eq_univ] },
+    refine ⟨_, _, e, rfl, _⟩,
+    rintros H hX s hs ⟨_, x, rfl⟩,
+    haveI := is_reduced_of_open_immersion f,
+    specialize H (f.1.c.app _ s) _ ⟨x, by { change x ∈ (f.val.base) ⁻¹' _, rw e, trivial }⟩,
+    { rw [← LocallyRingedSpace.preimage_basic_open, hs], ext1, simp [opens.map] },
+    { erw ← PresheafedSpace.stalk_map_germ_apply f.1 ⟨_,_⟩ ⟨x,_⟩ at H,
+      apply_fun (inv $ PresheafedSpace.stalk_map f.val x) at H,
+      erw [category_theory.is_iso.hom_inv_id_apply, map_zero] at H,
+      exact H } },
+  { intros R hX s hs x,
+    erw [basic_open_eq_of_affine', prime_spectrum.basic_open_eq_bot_iff] at hs,
+    replace hs := (hs.map (Spec_Γ_identity.app R).inv).eq_zero,
+    rw coe_hom_inv_id at hs,
+    rw [hs, map_zero],
+    exact @@is_reduced.component_reduced hX ⊤ }
+end
+
+@[simp]
+lemma basic_open_eq_bot_iff {X : Scheme} [is_reduced X] {U : opens X.carrier}
+  (s : X.presheaf.obj $ op U) :
+  X.to_LocallyRingedSpace.to_RingedSpace.basic_open s = ⊥ ↔ s = 0 :=
+begin
+  refine ⟨eq_zero_of_basic_open_empty s, _⟩,
+  rintro rfl,
+  simp,
+end
+
 @[priority 900]
 instance is_reduced_of_is_integral [is_integral X] : is_reduced X :=
 begin

src/algebraic_geometry/structure_sheaf.lean

@@ -527,6 +527,12 @@ corresponding to a prime ideal in `R` and the localization of `R` at `p`. -/
     by { ext f, simp only [ring_hom.comp_apply, ring_hom.id_apply, localization_to_stalk_of,
                            stalk_to_fiber_ring_hom_to_stalk] } }
 
+instance (x : prime_spectrum R) : is_iso (stalk_to_fiber_ring_hom R x) :=
+is_iso.of_iso (stalk_iso R x)
+
+instance (x : prime_spectrum R) : is_iso (localization_to_stalk R x) :=
+is_iso.of_iso (stalk_iso R x).symm
+
 /-- The canonical ring homomorphism interpreting `s ∈ R_f` as a section of the structure sheaf
 on the basic open defined by `f ∈ R`. -/
 def to_basic_open (f : R) : localization.away f →+*

src/ring_theory/nilpotent.lean

@@ -72,6 +72,17 @@ is_reduced.eq_zero x h
   is_nilpotent x ↔ x = 0 :=
 ⟨λ h, h.eq_zero, λ h, h.symm ▸ is_nilpotent.zero⟩
 
+lemma is_reduced_of_injective [monoid_with_zero R] [monoid_with_zero S]
+  {F : Type*} [monoid_with_zero_hom_class F R S] (f : F)
+  (hf : function.injective f) [_root_.is_reduced S] : _root_.is_reduced R :=
+begin
+  constructor,
+  intros x hx,
+  apply hf,
+  rw map_zero,
+  exact (hx.map f).eq_zero,
+end
+
 namespace commute
 
 section semiring

src/topology/opens.lean

@@ -95,6 +95,7 @@ by refl
   (⟨U, hU⟩ ⊓ ⟨V, hV⟩ : opens α) = ⟨U ⊓ V, is_open.inter hU hV⟩ := rfl
 @[simp,norm_cast] lemma coe_inf {U V : opens α} :
   ((U ⊓ V : opens α) : set α) = (U : set α) ⊓ (V : set α) := rfl
+@[simp] lemma coe_bot : ((⊥ : opens α) : set α) = ∅ := rfl
 
 instance : has_inter (opens α) := ⟨λ U V, U ⊓ V⟩
 instance : has_union (opens α) := ⟨λ U V, U ⊔ V⟩