Unramified primes in finite invariant extensions

In a finite flat invariant extension of domains, a maximal prime is unramified exactly when its inertia group has order one. This includes imperfect residue fields: the inertia group has order e * fᵢ, so its triviality forces both ramification index one and residue separability.

For the integral closure of a Dedekind domain in a finite Galois extension of its fraction field, the compatible Galois action gives IsGaloisGroup by IsGaloisGroup.of_isFractionRing. Assuming this integral closure is finite over the base, flatness follows from torsion-freeness; no residue-field hypothesis is needed.

The criterion for a prime of the base quantifies over all primes above it. It translates unramifiedness into an inertia condition without assuming finite or perfect residue fields, as needed when testing splitting in subextensions and composita over a general Dedekind base. Inertia conditions allow unramifiedness in subextensions to be studied through their fixing subgroups, relating the arithmetic of composita to intersections of subgroups.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §9.

theorem Ideal.card_inertia_eq_one_iff_isUnramifiedAt {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S] [Module.Flat R S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] (P : Ideal S) [P.IsMaximal] : Nat.card ↥(inertia G P) = 1 ↔ Algebra.IsUnramifiedAt R P

A maximal prime in a finite flat invariant extension is unramified exactly when its inertia group has order one, including when the residue fields are imperfect.

theorem Ideal.isUnramifiedAt_iff_inertia_eq_bot_of_isMaximal {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S] [Module.Flat R S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] (P : Ideal S) [P.IsMaximal] : Algebra.IsUnramifiedAt R P ↔ inertia G P = ⊥

A maximal prime in a finite flat invariant extension is unramified exactly when its inertia group is trivial. No residue-separability hypothesis is needed.

theorem Ideal.isUnramifiedIn_iff_forall_inertia_eq_bot {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S] [Module.Flat R S] [Group G] [MulSemiringAction G S] [IsGaloisGroup G R S] (p : Ideal R) [p.IsMaximal] : Algebra.IsUnramifiedIn S p ↔ ∀ P ∈ p.primesOver S, inertia G P = ⊥

A maximal prime of the base is unramified in a finite flat invariant extension exactly when every inertia group above it is trivial. No residue-separability hypothesis is needed.