Ideals in rational cyclotomic fields

This file develops coprimality criteria for ideals generated by x + yη and a coefficient divisibility result for integral linear combinations of roots of unity.

noncomputable def fltIdeals (p : ℕ) (x y : ℤ) (η : NumberField.RingOfIntegers (CyclotomicField p ℚ)) : Ideal (NumberField.RingOfIntegers (CyclotomicField p ℚ))

The principal ideal generated by x + y ζ^i for integer x and y

Equations

• fltIdeals p x y η = Ideal.span {↑x + η * ↑y}

theorem mem_fltIdeals {p : ℕ} (x y : ℤ) (η : NumberField.RingOfIntegers (CyclotomicField p ℚ)) : ↑x + η * ↑y ∈ fltIdeals p x y η

theorem aux_lem_flt {p : ℕ} [Fact (Nat.Prime p)] {x y z : ℤ} (H : x ^ p + y ^ p = z ^ p) (caseI : ¬↑p ∣ x * y * z) : ¬↑p ∣ x + y

theorem diff_of_roots {p : ℕ} [hp : Fact (Nat.Prime p)] (ph : 5 ≤ p) {η₁ η₂ : NumberField.RingOfIntegers (CyclotomicField p ℚ)} (hη₁ : η₁ ∈ Polynomial.nthRootsFinset p 1) (hη₂ : η₂ ∈ Polynomial.nthRootsFinset p 1) (hdiff : η₁ ≠ η₂) (hwlog : η₁ ≠ 1) : ∃ (u : (NumberField.RingOfIntegers (CyclotomicField p ℚ))ˣ), η₁ - η₂ = ↑u * (1 - η₁)

theorem fltIdeals_coprime2_lemma {p : ℕ} [Fact (Nat.Prime p)] (ph : 5 ≤ p) {x y : ℤ} {η₁ η₂ : NumberField.RingOfIntegers (CyclotomicField p ℚ)} (hη₁ : η₁ ∈ Polynomial.nthRootsFinset p 1) (hη₂ : η₂ ∈ Polynomial.nthRootsFinset p 1) (hdiff : η₁ ≠ η₂) (hp : IsCoprime x y) (hp2 : ¬↑p ∣ x + y) (hwlog : η₁ ≠ 1) : fltIdeals p x y η₁ ⊔ fltIdeals p x y η₂ = ⊤

theorem fltIdeals_coprime2 {p : ℕ} [Fact (Nat.Prime p)] (ph : 5 ≤ p) {x y : ℤ} {η₁ η₂ : NumberField.RingOfIntegers (CyclotomicField p ℚ)} (hη₁ : η₁ ∈ Polynomial.nthRootsFinset p 1) (hη₂ : η₂ ∈ Polynomial.nthRootsFinset p 1) (hdiff : η₁ ≠ η₂) (hp : IsCoprime x y) (hp2 : ¬↑p ∣ x + y) (hwlog : η₁ ≠ 1) : IsCoprime (fltIdeals p x y η₁) (fltIdeals p x y η₂)

theorem fltIdeals_coprime {p : ℕ} (hpri : Nat.Prime p) (p5 : 5 ≤ p) {x y z : ℤ} (H : x ^ p + y ^ p = z ^ p) {η₁ η₂ : NumberField.RingOfIntegers (CyclotomicField p ℚ)} (hxy : IsCoprime x y) (hη₁ : η₁ ∈ Polynomial.nthRootsFinset p 1) (hη₂ : η₂ ∈ Polynomial.nthRootsFinset p 1) (hdiff : η₁ ≠ η₂) (caseI : ¬↑p ∣ x * y * z) : have this := ⋯; IsCoprime (fltIdeals p x y η₁) (fltIdeals p x y η₂)

theorem dvd_coeff_cycl_integer {p : ℕ} {L : Type u_1} [Field L] [CharZero L] [IsCyclotomicExtension {p} ℚ L] (hp : Nat.Prime p) {ζ : NumberField.RingOfIntegers L} (hζ : IsPrimitiveRoot ζ p) {f : Fin p → ℤ} (hf : ∃ (i : Fin p), f i = 0) {m : ℤ} (hdiv : ↑m ∣ ∑ j : Fin p, f j • ζ ^ ↑j) (j : Fin p) : m ∣ f j