of_isLocalization_Away — Mathlib

English

Localization away from an element yields smoothness: if A is localized away from r, then A is smooth over R.

Русский

Локализация away от элемента r даёт гладкость: если A локализуется away от r, то A гладко над R.

LaTeX

$$$\operatorname{Smooth}(R,A) \text{ for } A = \operatorname{Away}_r(R)$$$

Lean4

/-- Localization at an element is smooth. -/
theorem of_isLocalization_Away (r : R) [IsLocalization.Away r A] : Smooth R A
    where
  formallySmooth := Algebra.FormallySmooth.of_isLocalization (Submonoid.powers r)
  finitePresentation := IsLocalization.Away.finitePresentation r

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