English
Let R be a commutative ring, A a commutative R-algebra, and p a prime ideal of A. Then A is smooth at p precisely when the localization A_p is formally smooth over R.
Русский
Пусть R — коммутативное кольцо, A — коммутативная R-алгебра, и p — прайм-идеал A. Тогда A гладко в точке p тогда и только тогда, когда локализация A_p формально гладкая над R.
LaTeX
$$$\mathrm{IsSmoothAt}(R,A,p) \;\Longleftrightarrow\; A_{p} \text{ is formally smooth over } R$$$
Lean4
/-- An `R`-algebra `A` is smooth at a prime `p` of `A` if `Aₚ` is formally smooth over `R`.
This does not imply `Aₚ` is smooth over `R` under the mathlib definition
even if `A` is finitely presented,
but it can be shown that this is equivalent to the stacks project definition that `A` is smooth
at `p` if and only if there exists `f ∉ p` such that `A_f` is smooth over `R`.
See `Algebra.basicOpen_subset_smoothLocus_iff_smooth` and `Algebra.isOpen_smoothLocus`.
-/
@[stacks 00TB]
abbrev IsSmoothAt (p : Ideal A) [p.IsPrime] : Prop :=
Algebra.FormallySmooth R (Localization.AtPrime p)
