Ramification indices in finite flat towers

This file records consequences of the fundamental identity for ramification and inertia in a finite flat extension of domains. The number of primes above a prime and each prime's contribution are at most the rank of the extension. Ramification also cancels in a tower when the absolute ramification index at the top equals the absolute ramification index at the intermediate prime: multiplicativity then forces the relative ramification index to be one.

The cancellation result is the local step used in the finite-place half of the genus-field construction. At a rational prime dividing a prime discriminant, both the quadratic base and the prime-discriminant compositum have absolute ramification index two; cancellation then shows that the compositum is unramified over the quadratic base.

Main results

• TauCeti.RamificationInertia.ncard_primesOver_le_finrank: the number of primes above a prime is at most the rank of a finite flat extension.
• TauCeti.RamificationInertia.ramificationIdx_mul_inertiaDeg_le_finrank: the contribution of one prime to the fundamental identity is at most the rank of the extension.
• TauCeti.RamificationInertia.ramificationIdx_le_finrank: a ramification index is at most the rank of a finite flat extension.
• TauCeti.RamificationInertia.ramificationIdx_eq_one_of_eq_ramificationIdx: equal absolute ramification indices at two levels of a tower force relative ramification index one.
• TauCeti.RamificationInertia.isUnramifiedIn_of_forall_eq_ramificationIdx: if that equality holds at every prime above an intermediate prime, then the intermediate prime is unramified in the top ring.
• TauCeti.RamificationInertia.isUnramifiedIn_of_forall_ramificationIdx_le: it suffices to bound every absolute ramification index upstairs by the intermediate absolute ramification index.
• TauCeti.RamificationInertia.isUnramifiedIn_of_finrank_le_of_under_ramificationIdx_eq_one: a transverse unramified subextension of sufficiently small relative degree supplies that bound.
• TauCeti.RamificationInertia.isUnramifiedAt_of_isUnramifiedIn: unramifiedness over the base descends from an integral extension to the subring below it, for S integral and torsion-free over the Dedekind domain R, with R and S both essentially of finite type over the base A and A ≤ R ≤ S a scalar tower. The base ring and the ideal are arbitrary.

theorem TauCeti.RamificationInertia.ncard_primesOver_le_finrank {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] [Algebra R S] [Module.Finite R S] [Module.Flat R S] (p : Ideal R) [p.IsPrime] : (p.primesOver S).ncard ≤ Module.finrank R S

There are at most Module.finrank R S primes above a prime. Every ramification index and inertia degree in the fundamental identity is positive, so every prime above p contributes at least one to the rank.

theorem TauCeti.RamificationInertia.ramificationIdx_mul_inertiaDeg_le_finrank {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] [Algebra R S] [Module.Finite R S] [Module.Flat R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] : q.ramificationIdx R * q.inertiaDeg R ≤ Module.finrank R S

One prime's contribution to the fundamental identity is at most the extension rank. For a prime q of S above a prime p of R, the product of its ramification index and inertia degree is at most Module.finrank R S.

theorem TauCeti.RamificationInertia.ramificationIdx_le_finrank {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] [Algebra R S] [Module.Finite R S] [Module.Flat R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] : q.ramificationIdx R ≤ Module.finrank R S

A ramification index is at most the rank of a finite flat extension. For a prime q of S above a prime p of R, e(q / p) ≤ Module.finrank R S.

theorem TauCeti.RamificationInertia.ramificationIdx_eq_one_of_eq_ramificationIdx {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Module.Finite R S] [Module.Flat S T] (q : Ideal S) (r : Ideal T) [q.IsPrime] [r.LiesOver q] (h : r.ramificationIdx R = q.ramificationIdx R) : r.ramificationIdx S = 1

Ramification-index cancellation in a tower. Let r be a prime of T above a prime q of S. If their absolute ramification indices over R agree, then the relative ramification index e(r / q) is one. Indeed, multiplicativity gives e(r / R) = e(q / R) * e(r / S), and e(q / R) is positive in a finite extension.

theorem TauCeti.RamificationInertia.isUnramifiedIn_of_forall_eq_ramificationIdx {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Module.Finite R S] [Module.Flat S T] [IsDomain S] [Module.Finite ℤ S] [CharZero S] [Module.Finite S T] (q : Ideal S) [q.IsPrime] (h : ∀ (r : Ideal T) [r.IsPrime], r.LiesOver q → r.ramificationIdx R = q.ramificationIdx R) : Algebra.IsUnramifiedIn T q

Absolute ramification-index equality implies relative unramifiedness. Let q be a prime of S. If every prime r of T above q has the same absolute ramification index over R as q, then q is unramified in T. This is the all-primes form of ramificationIdx_eq_one_of_eq_ramificationIdx.

theorem TauCeti.RamificationInertia.isUnramifiedIn_of_forall_ramificationIdx_le {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Module.Finite R S] [Module.Flat S T] [IsDomain S] [Module.Finite ℤ S] [CharZero S] [Module.Finite S T] (q : Ideal S) [q.IsPrime] (h : ∀ (r : Ideal T) [r.IsPrime], r.LiesOver q → r.ramificationIdx R ≤ q.ramificationIdx R) : Algebra.IsUnramifiedIn T q

No increase in absolute ramification implies relative unramifiedness. Let q be a prime of S. If every prime r of T above q has absolute ramification index at most that of q, then q is unramified in T. The reverse inequality is automatic from multiplicativity in the tower, so the absolute indices are equal and isUnramifiedIn_of_forall_eq_ramificationIdx applies.

theorem TauCeti.RamificationInertia.isUnramifiedIn_of_finrank_le_of_under_ramificationIdx_eq_one {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Module.Finite R S] [Module.Flat S T] [IsDomain S] [Module.Finite ℤ S] [CharZero S] [Module.Finite S T] {U : Type u_4} [CommRing U] [IsDomain U] [Algebra R U] [Algebra U T] [IsScalarTower R U T] [Module.Finite U T] [Module.Flat U T] (q : Ideal S) [q.IsPrime] (hrank : Module.finrank U T ≤ q.ramificationIdx R) (hunr : ∀ (r : Ideal T) [r.IsPrime], r.LiesOver q → (Ideal.under U r).ramificationIdx R = 1) : Algebra.IsUnramifiedIn T q

A transverse unramified subextension cancels the base ramification. Suppose T is also an extension of a domain U over R. Let q be a prime of S, assume Module.finrank U T ≤ e(q / R), and assume that for every prime r above q, its contraction to U has absolute ramification index one. Then q is unramified in T.

Indeed, the tower through U identifies e(r / R) with e(r / U), which is at most Module.finrank U T; hence e(r / R) ≤ e(q / R), and isUnramifiedIn_of_forall_ramificationIdx_le applies. For a biquadratic compositum at a shared ramified prime, S / R has ramification index two while T / U has degree two.

theorem TauCeti.RamificationInertia.isUnramifiedAt_of_isUnramifiedIn {A : Type u_1} {R : Type u_2} {S : Type u_3} [CommRing A] [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDomain S] [Algebra A R] [Algebra A S] [Algebra R S] [IsScalarTower A R S] [Algebra.IsIntegral R S] [Module.IsTorsionFree R S] [Algebra.EssFiniteType A R] [Algebra.EssFiniteType A S] {I : Ideal A} (hur : Algebra.IsUnramifiedIn S I) (𝔮 : Ideal R) [𝔮.IsPrime] [𝔮.LiesOver I] : Algebra.IsUnramifiedAt A 𝔮

Unramifiedness descends to a subring. If an ideal I of the base A is unramified in S, then every prime of an intermediate ring R lying over I is unramified over A. The direction is descent, not ascent: the hypothesis is upstairs and the conclusion downstairs.

A and I are arbitrary; the hypotheses that carry the argument are the ambient ones on R and S. Its number-field instance is NumberField.isUnramifiedAway_of_intermediateField, which quantifies it over the places outside a finite set.