English
For any f in A, the basic open D(f) inside Spec(A) sits inside the unramified locus over R exactly when the localization A_f is formally unramified over R.
Русский
Пусть f ∈ A. Тогда базовое открытое множество D(f) внутри Spec(A) целиком лежит в неразветвленной локусации над R тогда, когда локализация A_f является формально неразветвленной над R.
LaTeX
$$$\\uparrow\\mathrm{PrimeSpectrum.basicOpen}\\, f \\subseteq \\mathrm{unramifiedLocus}(R,A) \\;\\Longleftrightarrow\\; \\mathrm{Algebra.FormallyUnramified}\\; R\\; (\\mathrm{Localization.Away}\\; f).$$$
Lean4
theorem basicOpen_subset_unramifiedLocus_iff {f : A} :
↑(PrimeSpectrum.basicOpen f) ⊆ unramifiedLocus R A ↔ Algebra.FormallyUnramified R (Localization.Away f) :=
by
rw [unramifiedLocus_eq_compl_support, Set.subset_compl_comm, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl,
← LocalizedModule.subsingleton_iff_support_subset, Algebra.formallyUnramified_iff]
exact (IsLocalizedModule.iso (.powers f) (KaehlerDifferential.map R R A (Localization.Away f))).subsingleton_congr
