smoothLocus — Mathlib

English

For R and A, the smooth locus of A over R is the set of primes p in A for which the localization A_p is formally smooth over R.

Русский

Для пары колец R и A гладкостью локалуса по A называется множество таких простых идеалов p в A, для которых локализация A_p формально гладкая над R.

LaTeX

$$$\mathrm{smoothLocus}(R,A) = \{ p \in \mathrm{PrimeSpectrum}(A) \mid \mathrm{IsSmoothAt}(R,p.asIdeal) \}$$$

Lean4

/-- `Algebra.smoothLocus R A` is the set of primes `p` of `A`
such that `Aₚ` is formally smooth over `R`. -/
def smoothLocus : Set (PrimeSpectrum A) :=
  {p | IsSmoothAt R p.asIdeal}

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