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.

• IsCyclotomicExtension.Rat.galEquivZMod_stabilizer: assume that the prime p does not divide n then, for any prime ideal P above p in ℚ(ζₙ), the image by galEquivZMod of the decomposition group of P is the cyclic subgroup of (ℤ/nℤ)ˣ generated by the Frobenius element [p].

@[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.

theorem IsCyclotomicExtension.Rat.mem_zpowers_galEquivZMod_of_mem_stabilizer (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (p : ℕ) [hp : Fact (Nat.Prime p)] (P : Ideal (NumberField.RingOfIntegers K)) [P.IsMaximal] [P.LiesOver (Ideal.span {↑p})] (hn : p.Coprime n) {σ : Gal(K/ℚ)} (hσ : σ ∈ MulAction.stabilizer Gal(K/ℚ) P) : (galEquivZMod n K) σ ∈ Subgroup.zpowers (ZMod.unitOfCoprime p hn)

theorem IsCyclotomicExtension.Rat.galEquivZMod_stabilizer (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (p : ℕ) [hp : Fact (Nat.Prime p)] (P : Ideal (NumberField.RingOfIntegers K)) [P.IsMaximal] [P.LiesOver (Ideal.span {↑p})] (hn : p.Coprime n) : (galEquivZMod n K).mapSubgroup (MulAction.stabilizer Gal(K/ℚ) P) = Subgroup.zpowers (ZMod.unitOfCoprime p hn)