Imaginary cyclic subextensions of prime-power cyclotomic extensions

A cyclotomic extension L/K of a number field of prime-power level ℓ ^ r > 2 has a totally complex intermediate field that is cyclic over the base and has relative index at most two (exists_isTotallyComplex_isCyclic_subextension_prime_pow).

When (ZMod (ℓ ^ r))ˣ is cyclic, that is, for ℓ odd and for ℓ ^ r = 4, the whole extension does: its Galois group embeds in (ZMod (ℓ ^ r))ˣ through the cyclotomic character, and it is totally complex because it contains a primitive root of unity of order greater than two. For the levels 2 ^ (n + 3) the group (ZMod (2 ^ (n + 3)))ˣ is not cyclic, and the subextension (exists_isTotallyComplex_isCyclic_subextension_two_pow) is the fixed field of the kernel of a character of the modular unit group that detects both the unit 5 and -1. The former bounds its kernel; the latter excludes real places of its fixed field. Characters are extended using TauCeti.CharacterModule.exists_apply_eq_inv_addOrderOf, and the order of 5 is Mathlib's ZMod.orderOf_five.

These are the cyclic cyclotomic extensions along which a primary Brauer class of K is split at every place.

Main results

• TauCeti.NumberField.exists_isTotallyComplex_isCyclic_subextension_two_pow: the subextension at the levels 2 ^ (n + 3).
• TauCeti.NumberField.exists_isTotallyComplex_isCyclic_subextension_prime_pow: the subextension at every prime-power level ℓ ^ r > 2.

Reference

• J. S. Milne, Class Field Theory, Chapter VII, Lemma 7.3, https://www.jmilne.org/math/CourseNotes/CFT.pdf.

theorem TauCeti.NumberField.exists_isTotallyComplex_isCyclic_subextension_two_pow (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] (n : ℕ) [IsCyclotomicExtension {2 ^ (n + 3)} K L] : ∃ (E : IntermediateField K L), IsGalois K ↥E ∧ IsCyclic Gal(↥E/K) ∧ Module.finrank (↥E) L ≤ 2 ∧ NumberField.IsTotallyComplex ↥E

A 2^(n+3)-cyclotomic extension of a number field contains a totally complex cyclic extension of the base whose relative index in the full extension is at most two. No irreducibility assumption on the cyclotomic polynomial over the base is required.

theorem TauCeti.NumberField.exists_isTotallyComplex_isCyclic_subextension_prime_pow (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] {ℓ r : ℕ} (hℓ : Nat.Prime ℓ) (hr : 2 < ℓ ^ r) [IsCyclotomicExtension {ℓ ^ r} K L] : ∃ (E : IntermediateField K L), IsGalois K ↥E ∧ IsCyclic Gal(↥E/K) ∧ Module.finrank (↥E) L ≤ 2 ∧ NumberField.IsTotallyComplex ↥E

A cyclotomic extension of a number field of prime-power level ℓ ^ r > 2 contains a totally complex cyclic extension of the base whose relative index in the full extension is at most two. No irreducibility assumption on the cyclotomic polynomial over the base is required.