isIntegral_of_isAffine_of_isDomain

English

For X affine, if the global sections form a domain, then X is integral.

Русский

Для X аффинной схемы, если глобальные секции образуют область, то X интегральна.

LaTeX

$$$\text{IsAffine}(X) \wedge [\text{Nonempty } X] \wedge \text{IsDomain}(\Gamma(X, \mathcal{O}_X)) \Rightarrow \text{IsIntegral}(X)$$$

Lean4

theorem isIntegral_of_isAffine_of_isDomain [IsAffine X] [Nonempty X] [IsDomain Γ(X, ⊤)] : IsIntegral X :=
  isIntegral_of_isOpenImmersion X.isoSpec.hom

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