isReduced_of_isAffine_isReduced — Mathlib

English

If X is an affine scheme and the ring of global sections Γ(X, ⊤) is reduced, then X is a reduced scheme.

Русский

Если X — аффинный базис схемы и кольцо глобальных секций Γ(X, ⊤) редуцировано, то X — редуцированная схема.

LaTeX

$$$[IsAffine X] \land \text{IsReduced}(\Gamma(X, \top)) \Rightarrow \text{IsReduced}(X)$$

Lean4

theorem isReduced_of_isAffine_isReduced [IsAffine X] [_root_.IsReduced Γ(X, ⊤)] : IsReduced X :=
  isReduced_of_isOpenImmersion X.isoSpec.hom

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