The auxiliary Kummer idele subgroup

Let S and T be finite sets of finite places of a number field K. The auxiliary Kummer idele subgroup E_{S,T} consists of the ideles that are n-th powers at S and at every infinite place, arbitrary at T \ S, and integral units outside S ∪ T; the power condition continues to apply on S ∩ T. This is the subgroup used in the Kummer proof of the second fundamental inequality. The freedom at T \ S is what allows those places to split completely in the extension under consideration.

The index of E_{S,T} in the group of (S ∪ T)-ideles is the product of the power-class counts at S and at the infinite places. If K contains the n-th roots of unity and S contains the places above n, the product formula evaluates this index as

n ^ (2 * (#S + r₁ + r₂)).

If an extension has exponent dividing n, splits at T \ S, and is unramified outside S ∪ T, then E_{S,T} consists of idele norms. Thus its image in the idele class group is contained in the idele-class norm subgroup.

Main definitions

• TauCeti.ClassFieldTheory.auxiliaryKummerIdeleSubgroup: the subgroup E_{S,T}.
• TauCeti.ClassFieldTheory.auxiliaryKummerIdeleClassSubgroup: its image in the idele class group.

Main results

• TauCeti.ClassFieldTheory.relIndex_auxiliaryKummerIdeleSubgroup: the exact local-product formula for the index of E_{S,T}.
• TauCeti.ClassFieldTheory.relIndex_auxiliaryKummerIdeleSubgroup_eq_pow: the evaluation of that product when K contains the n-th roots of unity.
• TauCeti.ClassFieldTheory.auxiliaryKummerIdeleSubgroup_le_range_ideleNormMap: E_{S,T} consists of norms under the split and unramified hypotheses.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §6, Lemmas 6.4 and 6.6.

theorem TauCeti.ClassFieldTheory.relIndex_auxiliaryKummerIdeleSubgroup_eq_pow {K : Type u_1} [Field K] [NumberField K] (S T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity K n] (hS : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ↑n ∈ v.asIdeal → v ∈ S) : (auxiliaryKummerIdeleSubgroup S T n).relIndex (auxiliaryKummerIdeleSubgroup S T 1) = n ^ (2 * (S.card + Fintype.card (NumberField.InfinitePlace K)))

If K contains the n-th roots of unity and S contains every place above n, then the relative index of E_{S,T} in the (S ∪ T)-ideles is n ^ (2 * (#S + r₁ + r₂)).

theorem TauCeti.ClassFieldTheory.auxiliaryKummerIdeleSubgroup_le_range_ideleNormMap (K : Type) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {n : ℕ} (hn : Monoid.exponent Gal(L/K) ∣ n) (S T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hT : ∀ v ∈ T, v ∉ S → ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w) = 1) (hU : ∀ v ∉ S, v ∉ T → ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) (↑w).asIdeal) : auxiliaryKummerIdeleSubgroup S T n ≤ (GlobalNumberFields.ideleNormMap K L).range

The auxiliary Kummer ideles are norms. If the exponent of Gal(L/K) divides n, the places in T \ S split locally in L, and L/K is unramified outside S ∪ T, then every idele in E_{S,T} is a norm from L.

theorem TauCeti.ClassFieldTheory.auxiliaryKummerIdeleClassSubgroup_le_range_ideleClassNormMap (K : Type) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {n : ℕ} (hn : Monoid.exponent Gal(L/K) ∣ n) (S T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hT : ∀ v ∈ T, v ∉ S → ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w) = 1) (hU : ∀ v ∉ S, v ∉ T → ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) (↑w).asIdeal) : auxiliaryKummerIdeleClassSubgroup S T n ≤ (↑(GlobalNumberFields.ideleClassNormMap K L)).range

Under the split and unramified hypotheses, the image of E_{S,T} in the idele class group is contained in the idele-class norm subgroup.

theorem TauCeti.ClassFieldTheory.index_range_ideleClassNormMap_dvd_index_auxiliaryKummerIdeleClassSubgroup (K : Type) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {n : ℕ} (hn : Monoid.exponent Gal(L/K) ∣ n) (S T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hT : ∀ v ∈ T, v ∉ S → ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w) = 1) (hU : ∀ v ∉ S, v ∉ T → ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) (↑w).asIdeal) : (↑(GlobalNumberFields.ideleClassNormMap K L)).range.index ∣ (auxiliaryKummerIdeleClassSubgroup S T n).index

The idele-class norm index divides the index of the image of E_{S,T}.