The dyadic ramification groups of ℚ(i) #
For K generated over ℚ by an algebraic integer θ with minpoly ℤ θ = X² + 1, let 𝔭 be
the prime of 𝓞 K above 2, and let G_i be its ramification groups in Gal(K/ℚ), the
elements acting trivially on 𝓞 K ⧸ 𝔭 ^ (i + 1). This file computes the whole filtration:
G_0 = G_1 = Gal(K/ℚ) ≅ ℤ/2, and G_i = 1 for i ≥ 2.
Every automorphism sends θ to a square root of −1, so to θ or −θ
(TauCeti.NumberField.smul_gen_eq_or_eq_neg), and 𝓞 K = ℤ[θ], so
by Serre's criterion (TauCeti.Ideal.mem_inertia_iff_of_adjoin_singleton_eq_top) an
automorphism σ lies in G_i exactly when σ θ − θ ∈ 𝔭 ^ (i + 1). For the conjugation
σ θ − θ = −2θ generates (2) = 𝔭², which lies in 𝔭² but not in 𝔭³.
The two nontrivial groups G_0 and G_1 contribute 1 each to Hilbert's formula
v_𝔭(𝔡) = Σ_{i ≥ 0} (#G_i − 1), which gives back the different exponent v_𝔭(𝔡) = 2
(TauCeti.NumberField.GaussianRationals.multiplicity_differentIdeal_eq_two). The jump of the
filtration is at 1, not 0: the prime is wildly ramified, so G_1, a 2-group, is not
trivial.
Main results #
TauCeti.NumberField.GaussianRationals.mem_ramificationGroup_iff:σ ∈ G_iexactly whenσ = 1ori ≤ 1.TauCeti.NumberField.GaussianRationals.ramificationGroup_eq_topandramificationGroup_eq_bot:G_i = Gal(K/ℚ)fori ≤ 1, andG_i = 1fori ≥ 2.TauCeti.NumberField.GaussianRationals.card_ramificationGroup_eq_two_of_le_one:#G_0 = #G_1 = 2.TauCeti.NumberField.GaussianRationals.finsum_card_ramificationGroup_sub_one_eq_two: the sumΣ_{i ≥ 0} (#G_i − 1)of Hilbert's formula equals2, the known different exponent.
References #
- J.-P. Serre, Corps Locaux, Chapter IV, §1.
The dyadic ramification filtration of ℚ(i). An automorphism σ lies in the i-th
ramification group of the prime above 2 exactly when σ = 1 or i ≤ 1.
Use simp [mem_ramificationGroup_iff hmin hgen 𝔭] to simplify membership. The generator θ
does not occur in the membership expression, so simp cannot infer it to apply this theorem
as a global rule, regardless of priority.
The ramification groups G_0 and G_1 of the prime above 2 are the whole Galois group
of ℚ(i).
The ramification groups G_i of the prime above 2 in ℚ(i) are trivial for
i ≥ 2.
G_0 = G_1 ≅ ℤ/2: the ramification groups G_0 and G_1 of the prime above 2 in
ℚ(i) have order 2.
Hilbert's different formula, checked in ℚ(i): the sum Σ_{i ≥ 0} (#G_i − 1) over the
ramification groups of the prime above 2 is the different exponent v_𝔭(𝔡) = 2, as the
general multiplicity_differentIdeal_eq_finsum_card_ramificationGroup_sub_one predicts.