instIsReducedSpecOfIsReducedCarrier

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

Похожие утверждения