Unramifiedness and separability at one prime

An essentially finite type algebra is unramified at a prime exactly when its ramification index is one and its residue field extension is separable. The separability condition concerns only the selected prime, rather than every prime above its contraction. This distinction matters over imperfect residue fields, where ramification index one alone does not imply unramifiedness. At a maximal prime over a maximal ideal the residue fields may be replaced by the quotient fields.

theorem Ideal.isUnramifiedAt_iff_ramificationIdx_eq_one_and_isSeparable_residueField {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (q : Ideal S) [q.IsPrime] [Algebra.EssFiniteType R S] : Algebra.IsUnramifiedAt R q ↔ q.ramificationIdx R = 1 ∧ let this := Localization.AtPrime.algebraOfLiesOver (under R q) q; Algebra.IsSeparable (under R q).ResidueField q.ResidueField

Unramifiedness at a prime is ramification index one together with separability of the selected residue extension. No separability assumption is imposed at other primes.

theorem Ideal.isUnramifiedAt_iff_ramificationIdx_eq_one_and_isSeparable_quotient {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsMaximal] (q : Ideal S) [q.IsMaximal] [q.LiesOver p] [Algebra.EssFiniteType R S] : Algebra.IsUnramifiedAt R q ↔ q.ramificationIdx R = 1 ∧ Algebra.IsSeparable (R ⧸ p) (S ⧸ q)

At a maximal prime q over a maximal ideal p, unramifiedness is ramification index one together with separability of the extension of quotient fields (S ⧸ q) / (R ⧸ p).