English
If X is a scheme and f : X → Y is an open immersion, then the reducedness of Y implies reducedness of X.
Русский
Если X — схема и f: X → Y открытое вложение, то редуцированность Y влечёт редуцированность X.
LaTeX
$$$[\text{IsOpenImmersion } f] \Rightarrow (\text{IsReduced } Y) \Rightarrow (\text{IsReduced } X)$$$
Lean4
instance isReduced_stalk_of_isReduced [IsReduced X] (x : X) : _root_.IsReduced (X.presheaf.stalk x) :=
by
constructor
rintro g ⟨n, e⟩
obtain ⟨U, hxU, s, (rfl : (X.presheaf.germ U x hxU) s = g)⟩ := X.presheaf.germ_exist x g
rw [← map_pow, ← map_zero (X.presheaf.germ _ x hxU).hom] at e
obtain ⟨V, hxV, iU, iV, (e' : (X.presheaf.map iU.op) (s ^ n) = (X.presheaf.map iV.op) 0)⟩ :=
X.presheaf.germ_eq x hxU hxU _ 0 e
rw [map_pow, map_zero] at e'
replace e' := (IsNilpotent.mk _ _ e').eq_zero (R := Γ(X, V))
rw [← X.presheaf.germ_res iU x hxV, CommRingCat.comp_apply, e', map_zero]
