affine_isReduced_iff — Mathlib

English

For any commutative ring R, IsReduced(Spec R) holds if and only if IsReduced R holds.

Русский

Для любой кольцевой структуры R верно: IsReduced(Spec R) эквивалично IsReduced R.

LaTeX

$$$\text{IsReduced}(\operatorname{Spec} R) \iff \text{IsReduced}(R)$$$

Lean4

theorem affine_isReduced_iff (R : CommRingCat) : IsReduced (Spec R) ↔ _root_.IsReduced R :=
  by
  refine ⟨?_, fun h => inferInstance⟩
  intro h
  exact isReduced_of_injective (Scheme.ΓSpecIso R).inv.hom (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv.injective

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