feat(algebraic_geometry): A scheme is reduced iff its stalks are redu…

…ced. (#10879)

src/algebraic_geometry/properties.lean

@@ -58,6 +58,31 @@ class is_reduced : Prop :=
 
 attribute [instance] is_reduced.component_reduced
 
+lemma is_reduced_of_stalk_is_reduced [∀ x : X.carrier, _root_.is_reduced (X.presheaf.stalk x)] :
+  is_reduced X :=
+begin
+  refine ⟨λ U, ⟨λ s hs, _⟩⟩,
+  apply presheaf.section_ext X.sheaf U s 0,
+  intro x,
+  rw ring_hom.map_zero,
+  change X.presheaf.germ x s = 0,
+  exact (hs.map _).eq_zero
+end
+
+instance stalk_is_reduced_of_reduced [is_reduced X] (x : X.carrier) :
+  _root_.is_reduced (X.presheaf.stalk x) :=
+begin
+  constructor,
+  rintros g ⟨n, e⟩,
+  obtain ⟨U, hxU, s, rfl⟩ := X.presheaf.germ_exist x g,
+  rw [← map_pow, ← map_zero (X.presheaf.germ ⟨x, hxU⟩)] at e,
+  obtain ⟨V, hxV, iU, iV, e'⟩ := X.presheaf.germ_eq x hxU hxU _ 0 e,
+  rw [map_pow, map_zero] at e',
+  replace e' := (is_nilpotent.mk _ _ e').eq_zero,
+  erw ← concrete_category.congr_hom (X.presheaf.germ_res iU ⟨x, hxV⟩) s,
+  rw [comp_apply, e', map_zero]
+end
+
 @[priority 900]
 instance is_reduced_of_is_integral [is_integral X] : is_reduced X :=
 begin

src/ring_theory/nilpotent.lean

@@ -32,6 +32,9 @@ Note that we require only the bare minimum assumptions for the definition to mak
 power-associative. -/
 def is_nilpotent [has_zero R] [has_pow R ℕ] (x : R) : Prop := ∃ (n : ℕ), x^n = 0
 
+lemma is_nilpotent.mk [has_zero R] [has_pow R ℕ] (x : R) (n : ℕ)
+  (e : x ^ n = 0) : is_nilpotent x := ⟨n, e⟩
+
 lemma is_nilpotent.zero [monoid_with_zero R] : is_nilpotent (0 : R) := ⟨1, pow_one 0⟩
 
 lemma is_nilpotent.neg [ring R] (h : is_nilpotent x) : is_nilpotent (-x) :=