affine_isIntegral_iff — Mathlib

English

For an affine scheme Spec R, IsIntegral iff IsDomain R.

Русский

Для аффинной схемы Spec R интегральность эквивалентна тому, что R — область.

LaTeX

$$$\text{IsIntegral}(\operatorname{Spec} R) \iff \text{IsDomain}(R)$$$

Lean4

theorem affine_isIntegral_iff (R : CommRingCat) : IsIntegral (Spec R) ↔ IsDomain R :=
  ⟨fun _ => MulEquiv.isDomain Γ(Spec R, ⊤) (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv.toMulEquiv, fun _ =>
    inferInstance⟩

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