The field-theoretic part of Kummer's lemma

This file constructs Kummer's auxiliary polynomial and proves the associated splitting field is unramified.

theorem zeta_sub_one_pow_dvd_poly {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) : Polynomial.C ((hζ.toInteger - 1) ^ p) ∣ (Polynomial.C (hζ.toInteger - 1) * Polynomial.X - 1) ^ p + Polynomial.C ↑u

theorem KummersLemma.natDegree_poly_aux {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) : ((Polynomial.C (hζ.toInteger - 1) * Polynomial.X - 1) ^ p + Polynomial.C ↑u).natDegree = p

theorem KummersLemma.monic_poly_aux {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) : ((Polynomial.C (hζ.toInteger - 1) * Polynomial.X - 1) ^ p + Polynomial.C ↑u).leadingCoeff = (hζ.toInteger - 1) ^ p

noncomputable def KummersLemma.poly {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) : Polynomial (NumberField.RingOfIntegers K)

The monic polynomial used in Kummer's lemma after dividing by (ζ - 1)^p.

Equations

• KummersLemma.poly hp hζ u hcong = Exists.choose ⋯

theorem KummersLemma.poly_spec {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) : Polynomial.C ((hζ.toInteger - 1) ^ p) * poly hp hζ u hcong = (Polynomial.C (hζ.toInteger - 1) * Polynomial.X - 1) ^ p + Polynomial.C ↑u

theorem KummersLemma.monic_poly {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) : (poly hp hζ u hcong).Monic

theorem KummersLemma.natDegree_poly {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) : (poly hp hζ u hcong).natDegree = p

theorem KummersLemma.map_poly {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) : Polynomial.map (algebraMap (NumberField.RingOfIntegers K) K) (poly hp hζ u hcong) = (Polynomial.X - Polynomial.C (1 / (ζ - 1))) ^ p + Polynomial.C ((algebraMap (NumberField.RingOfIntegers K) K) ↑u / (ζ - 1) ^ p)

theorem KummersLemma.irreducible_map_poly {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) (hu : ∀ (v : K), v ^ p ≠ (algebraMap (NumberField.RingOfIntegers K) K) ↑u) : Irreducible (Polynomial.map (algebraMap (NumberField.RingOfIntegers K) K) (poly hp hζ u hcong))

theorem KummersLemma.aeval_poly {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) {L : Type u_2} [Field L] [Algebra K L] (α : L) (e : α ^ p = (algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) (m : ℕ) : (Polynomial.aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) (poly hp hζ u hcong) = 0

def KummersLemma.polyRoot {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) {L : Type u_2} [Field L] [Algebra K L] (α : L) (e : α ^ p = (algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) (m : ℕ) : NumberField.RingOfIntegers L

The integral root obtained by the Kummer transform from a p-th root of u.

Equations

• KummersLemma.polyRoot hp hζ u hcong α e m = ⟨(1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1), ⋯⟩

theorem KummersLemma.roots_poly {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) {L : Type u_2} [Field L] [Algebra K L] (α : L) (e : α ^ p = (algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) : (Polynomial.map (algebraMap (NumberField.RingOfIntegers K) L) (poly hp hζ u hcong)).roots = Multiset.map (fun (i : ℕ) => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range p).val

theorem KummersLemma.splits_poly {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) {L : Type u_2} [Field L] [Algebra K L] (α : L) (e : α ^ p = (algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) : (Polynomial.map (algebraMap (NumberField.RingOfIntegers K) L) (poly hp hζ u hcong)).Splits

theorem KummersLemma.map_poly_eq_prod {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) {L : Type u_2} [Field L] [Algebra K L] (α : L) (e : α ^ p = (algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) : Polynomial.map (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) (poly hp hζ u hcong) = ∏ i ∈ Finset.range p, (Polynomial.X - Polynomial.C (polyRoot hp hζ u hcong α e i))

theorem KummersLemma.minpoly_polyRoot'' {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) (hu : ∀ (v : K), v ^ p ≠ (algebraMap (NumberField.RingOfIntegers K) K) ↑u) {L : Type u_2} [Field L] [Algebra K L] (α : L) (e : α ^ p = (algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) (i : ℕ) : minpoly K ↑(polyRoot hp hζ u hcong α e i) = Polynomial.map (algebraMap (NumberField.RingOfIntegers K) K) (poly hp hζ u hcong)

theorem KummersLemma.minpoly_polyRoot' {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) (hu : ∀ (v : K), v ^ p ≠ (algebraMap (NumberField.RingOfIntegers K) K) ↑u) [NumberField K] {L : Type u_2} [Field L] [Algebra K L] (α : L) (e : α ^ p = (algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) (i : ℕ) : minpoly (NumberField.RingOfIntegers K) ↑(polyRoot hp hζ u hcong α e i) = poly hp hζ u hcong

theorem KummersLemma.separable_poly_aux {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) {L : Type u_2} [Field L] [Algebra K L] (α : L) (e : α ^ p = (algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) : (Polynomial.map (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) (poly hp hζ u hcong)).Separable

theorem KummersLemma.separable_poly {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) (hu : ∀ (v : K), v ^ p ≠ (algebraMap (NumberField.RingOfIntegers K) K) ↑u) (I : Ideal (NumberField.RingOfIntegers K)) [I.IsMaximal] : (Polynomial.map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable

theorem KummersLemma.polyRoot_spec {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) {L : Type u_2} [Field L] [Algebra K L] (α : L) (e : α ^ p = (algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) (i : ℕ) : α = (ζ ^ i)⁻¹ • (1 - (ζ - 1) • ↑(polyRoot hp hζ u hcong α e i))

theorem KummersLemma.mem_adjoin_polyRoot {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) {L : Type u_2} [Field L] [Algebra K L] (α : L) (e : α ^ p = (algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) (i : ℕ) : α ∈ K[↑(polyRoot hp hζ u hcong α e i)]

theorem KummersLemma.isUnramified {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (NumberField.RingOfIntegers K)ˣ) (hcong : (hζ.toInteger - 1) ^ p ∣ ↑u - 1) (hu : ∀ (v : K), v ^ p ≠ (algebraMap (NumberField.RingOfIntegers K) K) ↑u) [NumberField K] (L : Type u_2) [Field L] [Algebra K L] [Polynomial.IsSplittingField K L (Polynomial.X ^ p - Polynomial.C ((algebraMap (NumberField.RingOfIntegers K) K) ↑u))] : Algebra.Unramified (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)