Galois theory for cyclotomic fields

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

Let n be an integer. There is an isomorphism between Gal(ℚ(ζₙ)/ℚ) and (ℤ/nℤ)ˣ that sends σ to a_σ such that σ (ζₙ) = ζₙ ^ a_σ.

Following [Washington][washington.cyclotomic], we define the bijection between subfields of ℚ(ζₙ) and subgroups of the group Xₙ of Dirichlet characters of level n such that F corresponds to Y if and only if the subgroup H of (ℤ/nℤ)ˣ corresponding to F by the above isomorphism is the orthogonal of Y for the nondegenerate pairing on (ℤ/nℤ)ˣ × Xₙ defined by (n, χ) ↦ χ n.

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].
• IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar: the bijection between the intermediate fields of ℚ(ζₙ)/ℚ and subgroups of Xₙ.
• IsCyclotomicExtension.Rat.mem_intermediateFieldEquivSubgroupChar_iff_conductor_dvd: assume that m ∣ n, then the image of ℚ(ζₘ) ⊆ ℚ(ζₙ) by intermediateFieldEquivSubgroupChar is the set of characters whose conductor divides m.

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

Equations

• IsCyclotomicExtension.Rat.galEquivZMod n K = IsCyclotomicExtension.autEquivPow K ⋯

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)

noncomputable def IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [CommRing R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] : Subgroup Gal(K/ℚ) ≃o (Subgroup (DirichletCharacter R n))ᵒᵈ

The bijection between the subgroups of Gal(ℚ(ζₙ)/ℚ) and the subgroups of the group of Dirichlet characters of level n.

Equations

• IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar n K R = (IsCyclotomicExtension.Rat.galEquivZMod n K).mapSubgroup.trans (MulChar.subgroupOrderIsoSubgroupMulChar (ZMod n) R)

@[simp]

theorem IsCyclotomicExtension.Rat.mem_subgroupGalEquivSubgroupChar_iff (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [CommRing R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] (χ : DirichletCharacter R n) (H : Subgroup Gal(K/ℚ)) : χ ∈ OrderDual.ofDual ((subgroupGalEquivSubgroupChar n K R) H) ↔ ∀ σ ∈ H, χ ↑((galEquivZMod n K) σ) = 1

@[simp]

theorem IsCyclotomicExtension.Rat.mem_subgroupGalEquivSubgroupChar_symm_iff (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [CommRing R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] (σ : Gal(K/ℚ)) (Y : Subgroup (DirichletCharacter R n)) : σ ∈ (subgroupGalEquivSubgroupChar n K R).symm (OrderDual.toDual Y) ↔ ∀ χ ∈ Y, χ ↑((galEquivZMod n K) σ) = 1

noncomputable def IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [CommRing R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [IsGalois ℚ K] : IntermediateField ℚ K ≃o Subgroup (DirichletCharacter R n)

The bijection between the intermediate fields of ℚ(ζₙ)/ℚ and the subgroups of the group of Dirichlet characters of level n.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsCyclotomicExtension.Rat.mem_intermediateFieldEquivSubgroupChar_iff (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [CommRing R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [IsGalois ℚ K] (F : IntermediateField ℚ K) (χ : DirichletCharacter R n) : χ ∈ (intermediateFieldEquivSubgroupChar n K R) F ↔ ∀ σ ∈ F.fixingSubgroup, χ ↑((galEquivZMod n K) σ) = 1

theorem IsCyclotomicExtension.Rat.mem_intermediateFieldEquivSubgroupChar_iff_conductor_dvd (n : ℕ) [NeZero n] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [CommRing R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [IsGalois ℚ K] (F : IntermediateField ℚ K) {m : ℕ} [NeZero m] [IsGalois ℚ ↥F] [IsCyclotomicExtension {m} ℚ ↥F] (hdiv : m ∣ n) (χ : DirichletCharacter R n) : χ ∈ (intermediateFieldEquivSubgroupChar n K R) F ↔ χ.conductor ∣ m

Assume that m ∣ n, then the image of ℚ(ζₘ) ⊆ ℚ(ζₙ) by intermediateFieldEquivSubgroupChar is the set of characters whose conductor divides m.