Galois theory for cyclotomic fields

In this file, we study the Galois theory of cyclotomic extensions of ℚ.

Main definitions and results

• IsCyclotomicExtension.Rat.galEquivZMod: the isomorphism between Gal(ℚ(ζₙ)/ℚ) and (ℤ/nℤ)ˣ that sends σ to the class a such that σ (ζₙ) = ζₙ ^ a.

@[reducible, inline]

noncomputable abbrev IsCyclotomicExtension.Rat.galEquivZMod (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] : Gal(K/ℚ) ≃* (ZMod n)ˣ

The isomorphism between Gal(ℚ(ζₙ)/ℚ) and (ℤ/nℤ)ˣ that sends σ to the class a such that σ (ζₙ) = ζₙ ^ a.

theorem IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (σ : Gal(K/ℚ)) {x : K} (hx : x ^ n = 1) : σ x = x ^ (↑((galEquivZMod n K) σ)).val

theorem IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (σ : Gal(K/ℚ)) {x : NumberField.RingOfIntegers K} (hx : x ^ n = 1) : σ • x = x ^ (↑((galEquivZMod n K) σ)).val

theorem IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] {m : ℕ} [NeZero m] (F : Type u_2) [Field F] [NumberField F] [hF : IsCyclotomicExtension {m} ℚ F] [Algebra F K] [IsGalois ℚ F] (h : m ∣ n) (σ : Gal(K/ℚ)) : (galEquivZMod m F) (σ.restrictNormal F) = (ZMod.unitsMap h) ((galEquivZMod n K) σ)

Let m ∣ n. Then, the following diagram commutes: Gal(ℚ(ζₙ)/ℚ) → (ℤ/nℤ)ˣ ↓ ↓ Gal(ℚ(ζₘ)/ℚ) → (ℤ/mℤ)ˣ where the horizontal maps are galEquivZMod, the left map is the restriction map and the right map is the natural map.