The degree of a Kummer extension #
Let K be a field containing the n-th roots of unity, that is, with n distinct n-th roots of
unity (HasEnoughRootsOfUnity K n), and let Δ be a subgroup of Kˣ. Inside an extension E of
K, the Kummer field K(Δ^{1/n}) is the subfield generated over K by every n-th root of
every element of Δ (TauCeti.kummerField). This file proves the main theorem of Kummer theory
for it:
K(Δ^{1/n})/Kis an abelian Galois extension (TauCeti.isAbelianGalois_kummerField), and it is finite whenΔhas finite image in the power classesKˣ ⧸ (Kˣ)ⁿ(TauCeti.finiteDimensional_kummerField);- if every element of
Δhas ann-th root inE, its degree is the index ofΔ ∩ (Kˣ)ⁿinΔ, that is, the order of the image ofΔinKˣ ⧸ (Kˣ)ⁿ(TauCeti.finrank_kummerField).
For instance, over a number field containing the n-th roots of unity, the n-th roots of the
S-units, for a finite set S of places, generate such an extension; extensions of this kind are
used in the proof of the second inequality of global class field theory.
The degree is computed with the Kummer pairing ⟨σ, a⟩ = σ α / α, for σ an automorphism of
K(Δ^{1/n}) and α an n-th root of a ∈ Δ. Two roots of a differ by an n-th root of unity,
which lies in K (TauCeti.exists_eq_algebraMap_mul_of_pow_eq), so the pairing does not depend on
the choice of α, and it is bimultiplicative. It embeds the Galois group in the characters of
Δ modulo n-th powers, and Δ modulo n-th powers in the characters of the Galois group.
Dedekind's bound on the number of characters of a finite group (TauCeti.natCard_monoidHom_le)
turns these two embeddings into the equality of orders.
The Kummer character MonoidHom.kummerCharacter of TauCeti.FieldTheory.Kummer.Character takes
its values in the roots of unity of a base field that is algebraically closed in the extension; the
base field here need not be, so the pairing below takes its values in the top field.
Main definitions #
TauCeti.kummerField: the subfieldK(Δ^{1/n})ofE.
Main results #
TauCeti.isAbelianGalois_kummerField:K(Δ^{1/n})/Kis abelian Galois.TauCeti.exponent_algEquiv_kummerField_dvd: its Galois group has exponent dividingn.TauCeti.finiteDimensional_kummerField: it is finite whenΔ ∩ (Kˣ)ⁿhas finite index inΔ.TauCeti.finrank_kummerField:[K(Δ^{1/n}) : K] = [Δ : Δ ∩ (Kˣ)ⁿ], when every element ofΔhas ann-th root inE.TauCeti.finrank_kummerField_le_relIndex_mul_finrank: for a finite subextensionLofE,[K(Δ^{1/n}) : K] ≤ [Δ : Δ ∩ (Lˣ)ⁿ] · [L : K].TauCeti.exists_eq_algebraMap_mul_of_pow_eq: over a domain containing then-th roots of unity, two elements of a field extension with the samen-th power differ by a unit from the base; so ifahas ann-th root in aK-algebraRmapping toM, everyn-th root ofainMcomes fromR(TauCeti.mem_range_algebraMap_of_pow_eq).TauCeti.adjoin_pow_eq_algebraMap_kummerField_eq_top:K(Δ^{1/n})is generated overKby then-th roots of elements ofΔthat it contains.AlgEquiv.apply_div_self_eq_of_pow_eq,AlgEquiv.apply_div_self_eq_mul_of_pow_eq,AlgEquiv.mul_apply_div_self_of_pow_eq: the Kummer pairingσ y / yonly depends ony ^ n, and it is multiplicative iny ^ nand inσ.
References #
- S. Lang, Algebra, Graduate Texts in Mathematics 211, Springer (2002), Chapter VI, §8, Theorem 8.1.
- J. S. Milne, Class Field Theory, Chapter VII, §5, where these extensions are used.
If the domain K contains the n-th roots of unity, then two elements of a field extension
of K with the same n-th power differ by a unit from K.
If the domain K contains the n-th roots of unity, a K-automorphism moves an
n-th root of an element of K by a unit from K.
If the domain K contains the n-th roots of unity, the ratio σ y / y of a
K-automorphism only depends on y ^ n, even when this power does not lie in K.
If the domain K contains the n-th roots of unity, the Kummer pairing σ y / y is
trivial when y ^ n is the n-th power of a unit of K.
If the domain K contains the n-th roots of unity, the ratio σ w / w is the product
of σ y / y and σ y' / y' whenever w ^ n = (y * y') ^ n.
If the domain K contains the n-th roots of unity, the Kummer pairing σ y / y at an
n-th root y of an element of K is multiplicative in σ.
An n-th root of a unit of K in a nontrivial K-algebra is nonzero.
If the base field contains the n-th roots of unity, an intermediate field contains
an n-th root of a exactly when it contains any chosen n-th root of a.
If the base field contains the n-th roots of unity and a has an n-th root in a
K-algebra R mapping to M, then every n-th root of a in M comes from R.
If every element of Δ has an n-th root in E, then it has one in K(Δ^{1/n}).
The Kummer field K(Δ^{1/n}) is generated over K by the n-th roots of the elements of Δ
that it contains, viewed as elements of K(Δ^{1/n}) itself.
K(Δ^{1/n}) is the smallest subfield containing the n-th roots of the elements of Δ.
K(Δ^{1/n})/K is finite when Δ ∩ (Kˣ)ⁿ has finite index in Δ: it is generated by the
n-th roots of finitely many representatives of Δ modulo n-th powers.
K(Δ^{1/n})/K is an abelian Galois extension when K contains the n-th roots of unity.
Each generator is a root of a separable binomial Xⁿ - a that splits in K(Δ^{1/n}), and each
automorphism multiplies each generator by a constant, so any two automorphisms commute.
The Galois group of a Kummer extension has exponent dividing the radical exponent.
Every K-automorphism of K(Δ^{1/n}), raised to the n-th power, fixes each radical generator.
The degree of a Kummer extension. If K contains the n-th roots of unity and every
element of Δ has an n-th root in E, then [K(Δ^{1/n}) : K] = [Δ : Δ ∩ (Kˣ)ⁿ], the order of
the image of Δ in Kˣ ⧸ (Kˣ)ⁿ, as soon as this index is finite.
The elements of Δ that become n-th powers in a subfield L. If every element of Δ
has an n-th root in E and L is a finite subextension of E, then
[K(Δ^{1/n}) : K] ≤ [Δ : Δ ∩ (Lˣ)ⁿ] · [L : K], where Δ ∩ (Lˣ)ⁿ consists of the elements of Δ
that are n-th powers in L.