English
The notion IsUnramifiedAt is defined as FormallyUnramified over the localized base.
Русский
Понятие IsUnramifiedAt определяется как FormallyUnramified после локализации по базе.
LaTeX
$$abbrev IsUnramifiedAt (q : Ideal A) [q.IsPrime] := FormallyUnramified R (Localization.AtPrime q)$$
Lean4
/-- We say that an `R`-algebra `A` is unramified at a prime `q` of `A`
if `A_q` is formally unramified over `R`.
If `A` is of finite type over `R` and `q` is lying over `p`, then this is equivalent to
`κ(q)/κ(p)` being separable and `pA_q = qA_q`.
See `Algebra.isUnramifiedAt_iff_map_eq` in `RingTheory.Unramified.LocalRing` -/
abbrev IsUnramifiedAt (q : Ideal A) [q.IsPrime] : Prop :=
FormallyUnramified R (Localization.AtPrime q)
