Documentation

TauCeti.NumberTheory.ClassFieldTheory.KummerLayer

The Kummer layer of a subgroup of Kˣ #

Let K be a field containing the n-th roots of unity and Δ a subgroup of Kˣ with finite image in Kˣ ⧸ (Kˣ)ⁿ. The Kummer field K(Δ^{1/n}) inside the separable closure Kˢ is a finite abelian Galois extension of K (TauCeti.isAbelianGalois_kummerField), so it is the class field of an open normal subgroup of the absolute Galois group G_K. This file names that subgroup, the Kummer layer kummerLayer n Δ, and records its characteristic properties: it cuts out K(Δ^{1/n}), it is an abelian layer, its degree is the index [Δ : Δ ∩ (Kˣ)ⁿ], and the quotient G_K ⧸ kummerLayer n Δ has exponent dividing n.

Kummer layers are the layers on which the Kummer-theoretic steps of class field theory take place: over a number field containing the p-th roots of unity, the layer of the S-units cutting out K(U_S^{1/p}) is the abelian extension realizing the norm subgroup of the Kummer idele group in the proof of global existence, and the extension whose Frobenius elements are counted in the Kummer case of the second fundamental inequality.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.ClassFieldTheory.kummerLayer {K : Type u_1} [Field K] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity K n] (Δ : Subgroup Kˣ) [(powMonoidHom n).range.IsFiniteRelIndex Δ] :
OpenNormalSubgroup (AbsoluteGaloisGroup K)

The Kummer layer of a subgroup Δ of Kˣ, for K containing the n-th roots of unity and Δ of finite image in Kˣ ⧸ (Kˣ)ⁿ: the open normal subgroup of the absolute Galois group G_K fixing the Kummer field K(Δ^{1/n}) in the separable closure.

Instances For
    source
    theorem TauCeti.ClassFieldTheory.kummerLayer_toSubgroup {K : Type u_1} [Field K] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity K n] (Δ : Subgroup Kˣ) [(powMonoidHom n).range.IsFiniteRelIndex Δ] :
    ↑(kummerLayer n Δ).toOpenSubgroup = (kummerField (SeparableClosure K) n Δ).fixingSubgroup

    The subgroup underlying the Kummer layer is the fixing subgroup of K(Δ^{1/n}).

    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.classField_kummerLayer {K : Type u_1} [Field K] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity K n] (Δ : Subgroup Kˣ) [(powMonoidHom n).range.IsFiniteRelIndex Δ] :
    classField K (kummerLayer n Δ) = kummerField (SeparableClosure K) n Δ

    The Kummer layer cuts out the Kummer field: the class field of kummerLayer n Δ is K(Δ^{1/n}).

    source
    theorem TauCeti.ClassFieldTheory.mem_kummerLayer_iff {K : Type u_1} [Field K] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity K n] {Δ : Subgroup Kˣ} [(powMonoidHom n).range.IsFiniteRelIndex Δ] {σ : AbsoluteGaloisGroup K} :
    σ ∈ kummerLayer n Δ ↔ ∀ a ∈ Δ, ∀ (x : SeparableClosure K), x ^ n = (algebraMap K (SeparableClosure K)) ↑a → σ x = x

    An element of G_K lies in the Kummer layer of Δ exactly when it fixes every n-th root in Kˢ of every element of Δ.

    source
    theorem TauCeti.ClassFieldTheory.kummerLayer_antitone {K : Type u_1} [Field K] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity K n] {Δ : Subgroup Kˣ} [(powMonoidHom n).range.IsFiniteRelIndex Δ] {Δ' : Subgroup Kˣ} [(powMonoidHom n).range.IsFiniteRelIndex Δ'] (h : Δ ≤ Δ') :
    kummerLayer n Δ' ≤ kummerLayer n Δ

    Enlarging Δ shrinks the Kummer layer: a larger group of radicands cuts out a larger Kummer field.

    source
    theorem TauCeti.ClassFieldTheory.pow_mem_kummerLayer {K : Type u_1} [Field K] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity K n] (Δ : Subgroup Kˣ) [(powMonoidHom n).range.IsFiniteRelIndex Δ] (σ : AbsoluteGaloisGroup K) :
    σ ^ n ∈ kummerLayer n Δ

    The quotient G_K ⧸ kummerLayer n Δ has exponent dividing n: for every σ ∈ G_K, the power σ ^ n lies in the Kummer layer, since σ multiplies each n-th root of an element of Δ by an n-th root of unity.

    source
    theorem TauCeti.ClassFieldTheory.isAbelianClassFieldLayer_kummerLayer {K : Type} [Field K] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity K n] (Δ : Subgroup Kˣ) [(powMonoidHom n).range.IsFiniteRelIndex Δ] :
    (kummerLayer n Δ).IsAbelianClassFieldLayer

    The Kummer layer is abelian: K(Δ^{1/n})/K is an abelian extension.

    source
    theorem TauCeti.ClassFieldTheory.degree_kummerLayer {K : Type} [Field K] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity K n] (Δ : Subgroup Kˣ) [(powMonoidHom n).range.IsFiniteRelIndex Δ] :
    (NormalLayer.ofOpenNormal (kummerLayer n Δ)).degree = (powMonoidHom n).range.relIndex Δ

    The degree of the Kummer layer is [Δ : Δ ∩ (Kˣ)ⁿ], the order of the image of Δ in Kˣ ⧸ (Kˣ)ⁿ.