Algebraic Number Theory Facts

The following lemmas encode number-theoretic facts about the ring of integers of ℚ(√-7) that are used in the proof of the Ramanujan-Nagell theorem but require algebraic number theory machinery beyond what is currently available in Mathlib.

Reference: These facts can be found in standard algebraic number theory textbooks. The class number of ℚ(√-7) being 1 is part of the Heegner-Stark theorem which classifies all imaginary quadratic fields with class number 1: d = -1, -2, -3, -7, -11, -19, -43, -67, -163.

@[reducible, inline]

abbrev f_minpoly : Polynomial ℚ

The minimal polynomial of θ: X² - X + 2. Its discriminant is -7, so it is irreducible over ℚ.

Equations

• f_minpoly = Polynomial.X ^ 2 - Polynomial.X + Polynomial.C 2

instance instFactIrreduciblePolynomialRatF_minpoly : Fact (Irreducible f_minpoly)

def termK : Lean.ParserDescr

Equations

• termK = Lean.ParserDescr.node `termK 1024 (Lean.ParserDescr.symbol "K")

instance instFactForallNeRatHPowOfNatHAddNegHMul_ramanujanNagell : Fact (∀ (r : ℚ), r ^ 2 ≠ -2 + 1 * r)

instance instNumberFieldQuadraticAlgebraRatNegOfNat_ramanujanNagell : NumberField K

def termR : Lean.ParserDescr

Equations

• termR = Lean.ParserDescr.node `termR 1024 (Lean.ParserDescr.symbol "R")

theorem is_integral_ω : IsIntegral ℤ QuadraticAlgebra.omega

def termθ : Lean.ParserDescr

Equations

• termθ = Lean.ParserDescr.node `termθ 1024 (Lean.ParserDescr.symbol "θ")

theorem is_integral_one_sub_ω : IsIntegral ℤ (1 - QuadraticAlgebra.omega)

def termθ' : Lean.ParserDescr

Equations

• termθ' = Lean.ParserDescr.node `termθ' 1024 (Lean.ParserDescr.symbol "θ'")

theorem my_minpoly : minpoly ℤ ⟨QuadraticAlgebra.omega, is_integral_ω⟩ = Polynomial.X ^ 2 - Polynomial.X + 2

theorem my_minpoly_theta_prime : minpoly ℤ ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ = Polynomial.X ^ 2 - Polynomial.X + 2

theorem K_degree_2 : Module.finrank ℚ K = 2

theorem K_nrRealPlaces_zero : NumberField.InfinitePlace.nrRealPlaces K = 0

theorem K_nrComplexPlaces_2 : NumberField.InfinitePlace.nrComplexPlaces K = 1

theorem span_eq_top : Algebra.adjoin ℤ {⟨QuadraticAlgebra.omega, is_integral_ω⟩} = ⊤

theorem K_discriminant : NumberField.discr K = -7

theorem units_pm_one (u : (NumberField.RingOfIntegers K)ˣ) : u = 1 ∨ u = -1

theorem class_number_one_PID : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

theorem class_number_one : UniqueFactorizationMonoid (NumberField.RingOfIntegers K)

theorem algebra_norm_eq_quadratic_norm (z : K) : (Algebra.norm ℚ) z = QuadraticAlgebra.norm z

theorem exponent : RingOfIntegers.exponent ⟨QuadraticAlgebra.omega, is_integral_ω⟩ = 1

theorem ne_dvd_exponent (p : ℕ) [hp : Fact (Nat.Prime p)] : ¬p ∣ RingOfIntegers.exponent ⟨QuadraticAlgebra.omega, is_integral_ω⟩

theorem two_factorisation_R : ⟨QuadraticAlgebra.omega, is_integral_ω⟩ * (1 - ⟨QuadraticAlgebra.omega, is_integral_ω⟩) = 2

theorem norm_isUnit_iff (x : NumberField.RingOfIntegers K) : IsUnit ((Algebra.norm ℤ) x) ↔ IsUnit x

theorem norm_eq_coeff_zero_minpoly (x : NumberField.RingOfIntegers K) (h_deg : (minpoly ℤ x).natDegree = 2) : (Algebra.norm ℤ) x = (-1) ^ (minpoly ℤ x).natDegree * (minpoly ℤ x).coeff 0

Facts about θ

blah

theorem norm_theta_eq_two : (Algebra.norm ℤ) ⟨QuadraticAlgebra.omega, is_integral_ω⟩ = 2

theorem norm_theta_prime_eq_two : (Algebra.norm ℤ) ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ = 2

theorem theta_not_unit : ¬IsUnit ⟨QuadraticAlgebra.omega, is_integral_ω⟩

theorem theta_prime_not_unit : ¬IsUnit ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩

theorem theta_irreducible : Irreducible ⟨QuadraticAlgebra.omega, is_integral_ω⟩

Exercise 3: In the UFD R, if α · β = θ^m · θ'^m and gcd(α, β) = 1, then α = ±θ^m or α = ±θ'^m. This combines two steps: (1) unique factorization (class_number_one) implies α is associate to θ^m or θ'^m, and (2) the only units are ±1 (units_pm_one), pinning down the sign.

theorem theta'_irreducible : Irreducible ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩

theorem theta_theta'_not_associated : ¬Associated ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩

theorem theta_not_dvd_theta' : ¬⟨QuadraticAlgebra.omega, is_integral_ω⟩ ∣ ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩

theorem theta'_not_dvd_theta : ¬⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ∣ ⟨QuadraticAlgebra.omega, is_integral_ω⟩

theorem theta_pow_dvd_of_coprime_prod (α β : NumberField.RingOfIntegers K) (m : ℕ) (h_prod : α * β = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m * ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m) (h_coprime : IsCoprime α β) : ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m ∣ α ∨ ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m ∣ β

theorem associated_of_theta_pow_dvd (α β : NumberField.RingOfIntegers K) (m : ℕ) (h_prod : α * β = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m * ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m) (h_coprime : IsCoprime α β) (hα : ¬IsUnit α) (hβ : ¬IsUnit β) (h_dvd : ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m ∣ α) : Associated α (⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m)

theorem associated_of_theta_pow_dvd_right (α β : NumberField.RingOfIntegers K) (m : ℕ) (h_prod : α * β = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m * ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m) (h_coprime : IsCoprime α β) (hα : ¬IsUnit α) (hβ : ¬IsUnit β) (h_dvd : ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m ∣ β) : Associated α (⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m)

theorem ufd_associated_dichotomy (α β : NumberField.RingOfIntegers K) (m : ℕ) (h_prod : α * β = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m * ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m) (h_coprime : IsCoprime α β) (hα : ¬IsUnit α) (hβ : ¬IsUnit β) : Associated α (⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m) ∨ Associated α (⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m)

theorem associated_eq_or_neg (α γ : NumberField.RingOfIntegers K) (h : Associated α γ) : α = γ ∨ α = -γ

theorem ufd_power_association (α β : NumberField.RingOfIntegers K) (m : ℕ) (h_prod : α * β = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m * ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m) (h_coprime : IsCoprime α β) (hα : ¬IsUnit α) (hβ : ¬IsUnit β) : (α = ⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m ∨ α = -⟨QuadraticAlgebra.omega, is_integral_ω⟩ ^ m) ∨ α = ⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m ∨ α = -⟨1 - QuadraticAlgebra.omega, is_integral_one_sub_ω⟩ ^ m