Ramification and residue degrees below a fixed field #
Let H be a subgroup of Gal(L/K), let E = L ^ H, and let Q be a nonzero prime of 𝓞 L
over 𝓞 K. The product of the ramification index and residue degree of Q ∩ 𝓞 E over
𝓞 K is the relative index
[D(Q) : D(Q) ∩ H].
Equivalently, multiplying that product by the order of D(Q) ∩ H gives the corresponding
product for Q over 𝓞 K. The proof combines multiplicativity of ramification indices and
residue degrees in the tower K ⊆ E ⊆ L with the identification of the decomposition group over
E with D(Q) ∩ H. Applied to a translate σ • Q, this is the decomposition-group index formula
for the prime of E below that translate.
The ramification index alone is the relative index [I(Q) : I(Q) ∩ H] of inertia groups, by the
same argument with the inertia group of Q over E identified with I(Q) ∩ H. So the prime
below Q in E has e = 1 exactly when I(Q) ≤ H, and e = f = 1 exactly when D(Q) ≤ H.
If Q is unramified over K, all ramification indices in the tower are one. The general formula
then specializes to the residue-degree identity previously used in Frobenius arguments. Nothing
in either statement needs H cyclic: the Galois correspondence identifies
Gal(L/E) with H acting on ideals exactly as it does over K, so the decomposition group of Q
over E corresponds to H ⊓ D(Q) and in particular has as many elements, and multiplicativity of
the two local invariants does the rest.
A Frobenius φ at Q generates D(Q), so the count is Subgroup.relIndex — the index of
H ⊓ ⟨φ⟩ in ⟨φ⟩ — and the residue degree is one exactly when φ ∈ H. At H = ⟨φ⟩ membership
is automatic and the degree is one, which is the hypothesis of
NumberField.restrictScalars_eq_of_inertiaDeg_eq_one and so the step a fixed-field fibre count
runs through.
Main results #
Ideal.ramificationIdx_mul_inertiaDeg_under_fixedField_mul_card_inf: the local degree belowL ^ H, multiplied by the order ofD(Q) ∩ H, is the local degree ofQover the base.Ideal.ramificationIdx_mul_inertiaDeg_under_fixedField_eq_relIndex: the local degree belowL ^ His[D(Q) : D(Q) ∩ H].Ideal.inertiaDeg_under_fixedField_eq_one_of_stabilizer_le: ifD(Q) ≤ H, the residue degree belowL ^ His one.Ideal.ramificationIdx_under_fixedField_mul_card_inf: the ramification index belowL ^ H, multiplied by the order ofI(Q) ∩ H, is the ramification index ofQover the base.Ideal.ramificationIdx_under_fixedField_eq_relIndex: the ramification index belowL ^ His[I(Q) : I(Q) ∩ H].Ideal.ramificationIdx_under_fixedField_eq_one_iff: the ramification index belowL ^ His one exactly whenI(Q) ≤ H.Ideal.isUnramifiedAt_fixedField_iff_inertia_inf_eq_bot: unramifiedness overL ^ His equivalent to trivial intersection of inertia withH.Ideal.inertiaDeg_under_fixedField_mul_card_inf: the number of elements ofD(Q) ⊓ Htimes the residue degree belowL ^ His the residue degree ofQ.Ideal.inertiaDeg_under_fixedField_eq_relIndex: that residue degree isSubgroup.relIndex, the index ofH ⊓ ⟨φ⟩in⟨φ⟩.Ideal.isLeast_pow_mem_inertiaDeg_under_fixedField: equivalently, it is the leastn ≥ 1withφ ^ n ∈ H.Ideal.inertiaDeg_under_fixedField_eq_one_iff: it is one exactly when a Frobenius lies inH.Ideal.inertiaDeg_under_fixedField_eq_one_of_isArithFrobAt: atσ = φ, it is one.
References #
The decomposition-group index formula is Neukirch, Algebraic Number Theory, Chapter I, §9,
and Janusz, Algebraic Number Fields, Chapter I. The unramified Frobenius specialization also
appears in Sharifi, Algebraic Number Theory, Theorem 7.2.2. The corresponding step of the
Birkbeck--Brasca Chebotarev development,
CBirkbeck/chebotarev-density (Apache-2.0) at
commit 55a89985d47a3befcf6069aca1da250ff088b5c7, is the private declaration
inertiaDeg_under_E_eq_one_of_frobenius in CebotarevDensity/FixedFieldDensity.lean. There it is
one conjunct of a triple that also records the ramification index and the residue-field count, and
it carries orderOf σ = Nat.card Gal(L/E) as a hypothesis; that equality is a consequence of the
Galois correspondence and is derived here rather than assumed. Upstream states only the σ = φ
case; the general residue degree above is not there.
The local-degree product below a fixed field. For any subgroup H and E = L ^ H, the
ramification index times the residue degree of Q ∩ 𝓞 E over 𝓞 K, multiplied by the size of
D(Q) ∩ H, is the ramification index times the residue degree of Q over 𝓞 K.
This is the division-free form of
Ideal.ramificationIdx_mul_inertiaDeg_under_fixedField_eq_relIndex.
The decomposition-group index formula. For any subgroup H of Gal(L/K), the
ramification index times the residue degree of the prime below Q in L ^ H is the index of
D(Q) ∩ H in the decomposition group D(Q).
Instantiating this theorem at σ • Q gives the usual double-coset formula
e(𝔮_σ/𝔭) f(𝔮_σ/𝔭) = [σDσ⁻¹ : H ∩ σDσ⁻¹].
Above the decomposition group the residue degree is one. If H contains the
decomposition group D(Q), then the prime below Q in L ^ H has residue degree one over
𝓞 K.
The ramification index below a fixed field. For any subgroup H and E = L ^ H, the
ramification index of Q ∩ 𝓞 E over 𝓞 K, multiplied by the size of I(Q) ∩ H, is the
ramification index of Q over 𝓞 K.
This is the division-free form of Ideal.ramificationIdx_under_fixedField_eq_relIndex.
The inertia-group index formula. For any subgroup H of Gal(L/K), the ramification
index of the prime below Q in L ^ H is the index of I(Q) ∩ H in the inertia group I(Q).
In particular that prime is unramified over 𝓞 K exactly when I(Q) ≤ H, by
Subgroup.relIndex_eq_one.
Unramified below a fixed field. The prime below Q in L ^ H has ramification index
one over 𝓞 K exactly when H contains the inertia group I(Q).
A prime of L is unramified over L ^ H exactly when its inertia group over K
has trivial intersection with H.
The residue degree below a fixed field. For any subgroup H and E = L ^ H, the residue
degree of Q ∩ 𝓞 E over 𝓞 K times the size of the intersection of H with the decomposition
group is the residue degree of Q itself. Stated as a product, so no natural-number division is
truncated.
The residue degree is a relative index. For any subgroup H and φ a Frobenius at an
unramified Q, the residue degree below L ^ H is Subgroup.relIndex, Mathlib's name for the
index of H ⊓ ⟨φ⟩ in ⟨φ⟩.
The residue degree below the fixed field of a power of a Frobenius is its exponent's greatest common divisor with the Frobenius order.
The residue degree is the least exponent landing in H. For φ a Frobenius at an
unramified Q, the residue degree below L ^ H is the smallest n ≥ 1 with φ ^ n ∈ H.
This is the characterization the fixed-field fibre count uses: it turns the residue degree into a condition on powers of the Frobenius, with no index or relative index left to unfold.
Residue degree one is membership. The prime below Q in L ^ H has residue degree one
over 𝓞 K exactly when a Frobenius at Q lies in H.
The prime below Q in the fixed field of a Frobenius at Q has degree one. The case
H = ⟨σ⟩ with σ itself the Frobenius, where membership is automatic.