Ideals over a fixed field #
Let H be a subgroup of Gal(L/K) and E = L ^ H. The Galois correspondence identifies H with
Gal(L/E) without moving points, hence without moving ideals: an element of H and its image in
Gal(L/E) act alike on the ideals of 𝓞 L. The stabilizer of an ideal Q in Gal(L/E)
therefore corresponds to H ⊓ D(Q), with D(Q) the stabilizer of Q in Gal(L/K); in
particular the two have the same number of elements. The same holds for the inertia group
I(Q), because the two bundlings of an element of H act alike on 𝓞 L itself.
Let σ be an automorphism of L over K of finite order fixing an ideal Q of 𝓞 L. Then
every automorphism of L over the fixed field L ^ ⟨σ⟩ fixes Q, because Gal(L / L ^ ⟨σ⟩) is
generated by σ read over that field.
The stabilizer statement needs neither Q prime, nor σ an arithmetic Frobenius, nor L / K
Galois: its hypothesis is only that σ fixes Q. A Frobenius at an unramified prime supplies
that through IsArithFrobAt.mem_stabilizer, which is how a fixed-field fibre count uses this.
Transitivity of the Galois action then turns a full stabilizer into uniqueness of the prime above,
which is the second result. That one does ask for Q prime, but still not for L / K to be
Galois: L / L ^ ⟨σ⟩ is Galois on its own, being the fixed field of a finite group acting on L.
Uniqueness is not inertness — it excludes splitting, not ramification.
Main results #
AlgEquiv.toFixedFieldAlgEquiv_smul_ideal: the two bundlings ofσact alike on ideals.Subgroup.subgroupEquivAlgEquiv_smul_ideal: the Galois correspondenceH ≃* Gal(L / L ^ H)does not change how an element acts on ideals.Ideal.comap_stabilizer_fixedField_eq_subgroupOf: under that correspondence the stabilizer ofQinGal(L / L ^ H)corresponds toH ⊓ D(Q).Ideal.card_stabilizer_fixedField_eq_card_inf: so the two have the same number of elements.Ideal.comap_inertia_fixedField_eq_subgroupOf,Ideal.card_inertia_fixedField_eq_card_inf: the same two statements for the inertia group ofQin place of its stabilizer.NumberField.stabilizer_fixedField_zpowers_eq_top: overL ^ ⟨σ⟩, every automorphism fixesQ.NumberField.isGaloisGroup_ringOfIntegers_fixedField:His a Galois group of𝓞 Lover𝓞 (L ^ H).Ideal.eq_of_smul_eq_of_liesOver_under_fixedField:Qis the only prime of𝓞 Llying over its contraction to𝓞 (L ^ ⟨σ⟩).
References #
The corresponding step of the Birkbeck--Brasca Chebotarev development,
CBirkbeck/chebotarev-density (Apache-2.0) at
commit 55a89985d47a3befcf6069aca1da250ff088b5c7, is the private declaration
stabilizer_intermediate_eq_top_of_frobenius in CebotarevDensity/FixedFieldDensity.lean. There
it is stated for an arithmetic Frobenius at an unramified prime, with four instance arguments
threaded through the signature; neither the hypotheses nor the instances are needed. The
uniqueness statement is the private declaration eq_of_liesOver_under_E_of_frobenius in the same
file, likewise stated there for a Frobenius at an unramified prime; here it needs only that σ
fixes Q.
The rebundled automorphism acts as σ on ideals. AlgEquiv.toFixedFieldAlgEquiv σ is
σ with its base field changed, so it induces the same action on the ideals of 𝓞 L.
The Galois correspondence does not move points. For a subgroup H of Gal(L/K), the
automorphism of L over L ^ H attached to τ ∈ H is τ itself on elements.
The Galois correspondence does not move ideals. For a subgroup H of Gal(L/K), the
automorphism of L over L ^ H attached to τ ∈ H acts on the ideals of 𝓞 L exactly as τ
acts over K.
Over the fixed field, every automorphism fixes Q. If σ has finite order and fixes the
ideal Q, the stabilizer of Q in Gal(L / L ^ ⟨σ⟩) is the whole group.
This says the stabilizer is everything, not that L ^ ⟨σ⟩ is the largest such field.
A subgroup is the Galois group of the rings of integers over its fixed field. This is
Mathlib's ring-of-integers instance applied to IsGaloisGroup.fixedField. Instance search does
not find it unaided: the action of H on 𝓞 L restricted from Gal(L/K) and the one Mathlib's
instance builds from the action of H on L agree only after unfolding past instance
transparency.
A prime is the only one above its contraction to the fixed field. If σ fixes the prime
Q of 𝓞 L, then Q is the only prime of 𝓞 L lying over Q ∩ 𝓞 (L ^ ⟨σ⟩).
This excludes splitting, not ramification: it says the fibre is a single point, and asserts nothing
about the ramification index. A fixed-field fibre count is what needs it, and σ need not be a
Frobenius there either.
The decomposition group over a fixed field corresponds to the intersection. For a subgroup
H of Gal(L/K) and E = L ^ H, the Galois correspondence H ≃* Gal(L/E) pulls the stabilizer
of Q in Gal(L/E) back to the intersection of H with the stabilizer of Q in Gal(L/K),
read inside H.
The decomposition group over a fixed field has the size of the intersection. For a
subgroup H of Gal(L/K) and E = L ^ H, the stabilizer of Q in Gal(L/E) has as many
elements as the intersection of H with the stabilizer of Q in Gal(L/K).
The inertia group over a fixed field corresponds to the intersection. For a subgroup H
of Gal(L/K) and E = L ^ H, the Galois correspondence H ≃* Gal(L/E) pulls the inertia group
of Q in Gal(L/E) back to the intersection of H with the inertia group of Q in Gal(L/K),
read inside H.
The inertia group over a fixed field has the size of the intersection. For a subgroup
H of Gal(L/K) and E = L ^ H, the inertia group of Q in Gal(L/E) has as many elements as
the intersection of H with the inertia group of Q in Gal(L/K).