The Frobenius, the inertia subgroup, and the decomposition group #
Let L / K be a finite Galois extension of number fields with Galois group G = Gal(L/K), and
let Q be a nonzero prime of 𝓞 L lying over 𝔭 = Q ∩ 𝓞 K. Mathlib's IsArithFrobAt
expresses that an element σ ∈ G satisfies σ x ≡ x ^ #(𝓞 K ⧸ 𝔭) (mod Q). Tau Ceti's
NumberField.exists_isArithFrobAt supplies such an element, and
NumberField.isArithFrobAt_eq_of_isUnramifiedAt proves it unique when L / K is unramified at
Q. This file identifies what that element is. In general, a Frobenius at Q together with the
inertia subgroup of Q generates the decomposition group of Q; at an unramified prime the
inertia subgroup is trivial, and the Frobenius alone generates the decomposition group, mapping
to the Frobenius automorphism of the residue extension.
The link is Mathlib's Ideal.Quotient.stabilizerHom, the action of the decomposition group
MulAction.stabilizer G Q on the residue extension (𝓞 L ⧸ Q) / (𝓞 K ⧸ 𝔭). Its kernel is the
inertia subgroup, which is trivial exactly when Q is unramified, because the cardinality of the
inertia subgroup is the ramification index (Ideal.card_inertia_eq_ramificationIdx). So at an
unramified prime the decomposition group embeds in the residue Galois group, and a Frobenius
element is precisely a preimage of the residue Frobenius x ↦ x ^ #(𝓞 K ⧸ 𝔭). Counting through
that embedding turns the classical facts about finite fields into facts about G:
- the order of a Frobenius element is the inertia degree
f(Q/𝔭); - the decomposition group has cardinality
f(Q/𝔭)as well, so the embedding is an isomorphism; - consequently the decomposition group is
⟨σ⟩, and it is cyclic.
The last section transports these statements along the action of G on the primes above 𝔭.
Unramifiedness is invariant under that action, and the Frobenius at τ • Q is the conjugate
τ σ τ⁻¹: Mathlib's IsArithFrobAt.conj gives one inclusion and uniqueness at the unramified
prime τ • Q gives the other.
Main results #
Ideal.isUnramifiedAt_iff_inertia_eq_bot: unramifiedness atQis triviality of the inertia subgroup ofQinGal(L/K).Ideal.ramificationGroup_zero_eq_bot_iff_isUnramifiedAtandIdeal.ramificationGroup_eq_bot_of_isUnramifiedAt: equivalently, the ramification groupG_0ofQis trivial, and then so is everyG_i.Ideal.stabilizerHom_eq_frobeniusAlgEquivOfAlgebraic: a Frobenius element atQacts on the residue field𝓞 L ⧸ Qas the residue Frobenius.Ideal.orderOf_eq_inertiaDeg_of_isArithFrobAt: a Frobenius element at an unramifiedQhas order the inertia degree ofQover𝓞 K.Ideal.zpowers_eq_stabilizer_of_isArithFrobAt: a Frobenius element at an unramifiedQgenerates the decomposition group ofQ.Ideal.card_stabilizer_eq_inertiaDeg_of_isUnramifiedAt: the decomposition group of an unramifiedQhas order the inertia degree ofQover𝓞 K.Ideal.stabilizerEquivResidueAut: the decomposition group of an unramified prime is isomorphic to the automorphism group of the residue extension.Ideal.isCyclic_stabilizer_of_isUnramifiedAt: the decomposition group of an unramified prime is cyclic.Ideal.zpowers_sup_inertia_eq_stabilizer_of_isArithFrobAt: at any nonzero primeQ, a Frobenius element together with the inertia subgroup generates the decomposition group.Ideal.inertiaDeg_dvd_orderOf_of_isArithFrobAtandIdeal.inertiaDeg_eq_one_iff_mem_inertia_of_isArithFrobAt: at any primeQ, the inertia degree divides the order of a Frobenius element, and it is1exactly when that element lies in the inertia subgroup.Ideal.orbit_stabilizer_eq_orbit_zpowers_of_isArithFrobAt: on a set where the inertia subgroup acts trivially, the orbits of the decomposition group are those of any Frobenius.Ideal.isArithFrobAt_pointwise_smul_iff_eq_conj: the Frobenius elements atτ • Qare exactly the conjugatesτ σ τ⁻¹of the Frobenius elementsσat an unramifiedQ.
Implementation notes #
FiniteField.frobeniusAlgEquivOfAlgebraic is stated for a Fintype base field, so the residue
identification supplies that instance internally through Fintype.ofFinite. Residue rings are
made into fields by the local instance Ideal.Quotient.field, following Mathlib's own
ramification files.
References #
- [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter I, §9.
Unramifiedness and the inertia subgroup #
Unramified means trivial inertia. For a finite Galois extension L / K of number fields,
L / K is unramified at a prime Q of 𝓞 L exactly when the inertia subgroup of Q in
Gal(L/K) is trivial.
This is the group-theoretic reading of Ideal.card_inertia_eq_ramificationIdx: the inertia
subgroup has as many elements as the ramification index of Q over 𝓞 K.
Unramified means trivial G_0. For a finite Galois extension L / K of number fields,
the ramification group G_0 of a prime Q of 𝓞 L is trivial exactly when L / K is unramified
at Q.
The ramification filtration of an unramified prime is trivial. For a finite Galois
extension L / K of number fields unramified at a prime Q of 𝓞 L, every ramification group
G_i of Q is trivial.
The decomposition group at an unramified prime #
The decomposition group of an unramified prime embeds in the residue Galois group.
Mathlib's Ideal.Quotient.stabilizerHom has the inertia subgroup as its kernel, and that
subgroup is trivial at an unramified prime.
The decomposition group of an unramified prime is the residue Galois group. Mathlib's
Ideal.Quotient.stabilizerHom is always surjective for an invariant extension, and at an
unramified prime it is also injective, so it is an isomorphism from the decomposition group of
Q onto the automorphism group of the residue extension (𝓞 L ⧸ Q) / (𝓞 K ⧸ 𝔭).
This is the unramified case of Mathlib's Ideal.Quotient.stabilizerQuotientInertiaEquiv, where
the inertia subgroup one quotients by is trivial; the point of stating it separately is that the
source is the decomposition group itself, so an element of Gal(L/K) can be compared with a
residue automorphism without passing through a quotient. Under it, an arithmetic Frobenius at Q
corresponds to the residue Frobenius, by
Ideal.stabilizerHom_eq_frobeniusAlgEquivOfAlgebraic.
Equations
- Q.stabilizerEquivResidueAut = MulEquiv.ofBijective (Ideal.Quotient.stabilizerHom Q (Ideal.under (NumberField.RingOfIntegers K) Q) Gal(L/K)) ⋯
Instances For
Applying the residue action to the inverse image of a residue automorphism recovers that automorphism.
A Frobenius element induces the residue Frobenius. The action of an arithmetic Frobenius
σ at Q on the residue field 𝓞 L ⧸ Q is the #(𝓞 K ⧸ 𝔭)-power map, that is
FiniteField.frobeniusAlgEquivOfAlgebraic of the residue extension.
This is the defining congruence σ x ≡ x ^ #(𝓞 K ⧸ 𝔭) (mod Q) read as an equality of
automorphisms of 𝓞 L ⧸ Q; no unramifiedness is needed.
The residue degree is the order of the residue Frobenius. For an arithmetic Frobenius σ
at a prime Q, possibly ramified, the automorphism of the residue field 𝓞 L ⧸ Q induced by σ
has order the inertia degree f(Q / 𝔭): it is the residue Frobenius, whose order is the degree
of the residue extension.
The order of a Frobenius element is the inertia degree. For Q unramified over 𝓞 K, an
arithmetic Frobenius σ at Q has orderOf σ = f(Q / 𝔭).
The decomposition group injects into the residue Galois group, where the image of σ is the
residue Frobenius; that automorphism has order the degree of the residue extension, which is the
inertia degree.
The decomposition group of an unramified prime has order the inertia degree.
A Frobenius element generates the decomposition group. At an unramified prime Q the
cyclic subgroup generated by an arithmetic Frobenius at Q is the whole decomposition group,
both having f(Q / 𝔭) elements.
The decomposition group of an unramified prime is cyclic. A Frobenius element exists at
every nonzero prime of 𝓞 L, and at an unramified prime it generates the decomposition group.
The decomposition group at a possibly ramified prime #
A Frobenius and the inertia subgroup generate the decomposition group. Inside the
decomposition group of a prime Q, the subgroup generated by an arithmetic Frobenius σ at Q
together with the inertia subgroup is everything. No unramifiedness is needed; at an unramified
prime this recovers Ideal.zpowers_eq_stabilizer_of_isArithFrobAt.
The decomposition group is generated by a Frobenius and the inertia subgroup. For a
prime Q and an arithmetic Frobenius σ at Q, the decomposition group of Q in
Gal(L/K) is ⟨σ⟩ ⊔ I(Q). At an unramified prime the inertia subgroup is trivial and this is
Ideal.zpowers_eq_stabilizer_of_isArithFrobAt.
The orbit of a point fixed by inertia under the decomposition group is its orbit under a
Frobenius. Let Gal(L/K) act on a set, and let x be a point fixed by the inertia subgroup of
a prime Q. Then the orbit of x under the decomposition group of Q is its orbit under the
cyclic group generated by any arithmetic Frobenius at Q. This is how a Frobenius at a possibly
ramified prime of a Galois closure still determines the splitting in an unramified subfield.
The residue degree divides the order of a Frobenius. At any prime Q, ramified or not,
the inertia degree f(Q / 𝔭) divides the order of an arithmetic Frobenius σ at Q. At an
unramified prime the two are equal (Ideal.orderOf_eq_inertiaDeg_of_isArithFrobAt); at a
ramified prime σ is only determined up to the inertia subgroup, and its order can be larger.
Residue degree one means a Frobenius lies in the inertia subgroup. At any prime Q,
ramified or not, the inertia degree f(Q / 𝔭) is 1 exactly when an arithmetic Frobenius at Q
belongs to the inertia subgroup of Q, that is, acts trivially on the residue field.
Conjugation along the fibre #
Frobenius elements are conjugated by the automorphism action on primes. At an unramified
prime Q with arithmetic Frobenius σ, an element of Gal(L/K) is an arithmetic Frobenius at the
translated prime τ • Q exactly when it is the conjugate τ σ τ⁻¹.
The extension need not be normal.