English
Let R be a reduced commutative ring. Then the spectrum of R, denoted Spec R, is a reduced scheme.
Русский
Пусть R — редуцированное коммутативное кольцо. Тогда спектр Spec R редуцирован как схемa.
LaTeX
$$$\text{IsReduced}(R) \rightarrow \text{IsReduced}(\operatorname{Spec} R)$$$
Lean4
instance {R : CommRingCat.{u}} [H : _root_.IsReduced R] : IsReduced (Spec R) :=
by
apply (config := { allowSynthFailures := true }) isReduced_of_isReduced_stalk
intro x; dsimp
have : _root_.IsReduced (CommRingCat.of <| Localization.AtPrime (PrimeSpectrum.asIdeal x)) := by dsimp; infer_instance
exact
isReduced_of_injective (StructureSheaf.stalkIso R x).hom.hom
(StructureSheaf.stalkIso R x).commRingCatIsoToRingEquiv.injective