smoothLocus_eq_univ_iff — Mathlib

English

For a finitely presented R-algebra A, smoothness holds for A if and only if the basic open subset corresponding to 1 equals the whole spectrum.

Русский

Для конечной презентации R-алгебра A гладкость эквивалентна тому, что базовый открытый набор, соответствующий единице, совпадает со всем спектром.

LaTeX

$$$\mathrm{smoothLocus}(R,A) = \mathrm{Spec}(A) \iff \mathrm{FormallySmooth}(R,A)$$$

Lean4

theorem smoothLocus_eq_univ_iff [FinitePresentation R A] : smoothLocus R A = Set.univ ↔ Algebra.FormallySmooth R A :=
  by
  have := IsLocalization.atUnits A (.powers 1) (S := Localization.Away (1 : A)) (by simp)
  rw [Algebra.FormallySmooth.iff_of_equiv (this.restrictScalars R), ← basicOpen_subset_smoothLocus_iff]
  simp

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