Splitting of primes in rings of integers

Stream: new members

[Barinder S Banwait]

Hi everyone, I've been trying to formalise certain factorisations in the ring of integers of the quadratic field $\mathbb{Q}(\sqrt{-7})$. The ring of integers is $\Z[\frac{1+\sqrt{-7}}{2}]$, and my goal is to show that 2 splits as a product of the two irreducible (=prime since the class number is 1) elements

$$2 = \left(\frac{1 + \sqrt{-7}}{2}\right)\cdot\left(\frac{1 - \sqrt{-7}}{2}\right)$$

That's the basic question. For my subsequent purpose, it'll be important to know that the two numbers on the right here are prime in the ring of integers.

[Barinder S Banwait]

Here's what I've done so far on this.

I know mathlib4 has rings of integers, so I thought there should be a relatively painless way of doing the above. I googled around and quickly found the paper Certifying rings of integers in Number Fields by Baanen, Villarello and Dahmen; using their codebase I was able to formally verify that the ring of integers is as stated above. Their codebase has sage files that generates lean code to do these verifications. By working in one of these output files, and with a fair amount of vibe-coding, I was able to prove the above factorisation of 2 as a product of elements in the ring of integers in an extremely long-winded way (if interested, see this file, specifically the two_splits_explicitly theorem; note it won't compile without a file showing irreducibility of $X^2 + 7$, which is also generated by the authors, and which i can provide if anyone wants); though still lacking is the further step that this is a prime factorisation.

I have a feeling that this rather elementary fact in algebraic number theory should have a much shorter and easier formal proof than what i've got so far, hence my asking here.

[Kenny Lau]

we have the new QuadraticAlgebra

[Barinder S Banwait]

thanks @Kenny Lau for a quick response. could you perhaps provide a simple example of how QuadraticAlgebra works for rings of integers of quadratic fields? i'd appreciate being able to learn from that

[Kenny Lau]

it's new so we don't have that result yet, but $\mathbb{Z}\left[\dfrac{1+\sqrt{1+4k}}2\right]$ is $\mathbb{Z}[x]/(x^2-x-k)$

[Kenny Lau]

so we should first prove that if $1+4k$ is prime then QuadraticAlgebra k 1 is "the" ring of integers of $\mathbb{Q}(\sqrt{1+4k})$

[Riccardo Brasca]

We now have a more or less usable form of kummer-dedekind criterion for the splitting of (p), see the file ## Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind.

[Riccardo Brasca]

The computation of the ring of integers of a quadratic extension of the rationals would be a very welcome addition anyway

[Kevin Buzzard]

@Barinder S Banwait the easiest way to communicate on this forum is to post code which everyone can run. You've linked to a file but this file has lots of local imports. How about you remove all these imports, replace all the proofs which you're not asking about and are no longer imported with sorry, and then ask your question by posting a small code block using #backticks which everyone else can then run at the click of a button?

[Barinder S Banwait]

Kevin Buzzard said:

Barinder S Banwait the easiest way to communicate on this forum is to post code which everyone can run. You've linked to a file but this file has lots of local imports. How about you remove all these imports, replace all the proofs which you're not asking about and are no longer imported with sorry, and then ask your question by posting a small code block using #backticks which everyone else can then run at the click of a button?

gotcha, will do shortly ...

[Barinder S Banwait]

ok, below is as much as i've been able to trim the file. i removed local imports, and copy/pasted over what i needed from them. i sorry'd out as much as I could. it's still not exactly a "small code block", but it does compile using only mathlib imports.

i did slightly edit the builder structs of Baanen--Villarello--Dahmen (Specifically, removed hc_le) because I couldn't figure out what to import to have this work. This had a knock-on effect on my proof: two haves no longer compiled, so i just sorry'd them.

hopefully the below still gives the sense of how i've tried to do this. what I'm asking about is roughly the second half of what i've pasted below.

[Barinder S Banwait]

import Mathlib.Tactic.NormNum.Prime
import Mathlib.NumberTheory.NumberField.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
import Mathlib.RingTheory.IsAdjoinRoot

open Polynomial

def Finsupp.ofList {R : Type*} [DecidableEq R] [Zero R] (xs : List R) : ℕ →₀ R where
  toFun := (fun i => xs.getD i 0)
  support := (Finset.range xs.length).filter (fun i => xs.getD i 0 ≠ 0)
  mem_support_toFun a := by sorry

/-- Sends the list `[a₀, …, aₙ]` to the polynomial `a₀ + … + aₙ * X ^ n`.  -/
def Polynomial.ofList {R : Type*} [Semiring R] [DecidableEq R] (xs : List R) : R[X] :=
  ⟨Finsupp.ofList xs⟩

def List.dropTrailingZeros [Zero R] [DecidableEq R] : List R → List R
  | [] => []
  | x :: xs => if x ≠ 0 ∨ xs.any (fun x => x ≠ 0) then x :: xs.dropTrailingZeros else []

def List.dropTrailingZeros' [Zero R][DecidableEq R] : List R → List R
  | [] => []
  | (a :: as) => if List.getLast _ (List.cons_ne_nil a as) ≠ 0 then (a :: as)
    else (a :: as).dropTrailingZeros

structure SubalgebraBuilder
    (n : ℕ) [NeZero n] (R Q K : Type*) [CommRing R] [IsDomain R]
    [Field Q][CommRing K][Algebra Q K] [Algebra R Q][Algebra R K]
    [IsScalarTower R Q K] [IsFractionRing R Q] (T : R[X]) where
  (d : R)
  (hdeg : T.natDegree = n)
  (hm : coeff T n = 1)
  (B : Fin n →  R[X])
  (a : Fin n → Fin n → Fin n → R)
  (s : Fin n → Fin n → R[X])
  (c : Matrix (Fin n) (Fin n) R)
  (h : IsAdjoinRoot K (map (algebraMap R Q) T))
  (honed : B 0 = C d)
  (hd : d ≠ 0)
  (hpoly : ∀ j, B j = ∑ i : Fin n, C (c i j) * X ^ (i : ℕ))
  (hcc : ∀ i j, j < i → c i j = 0 )
  (hin : ∀ i, c i i ≠ 0)
  (hsymma : ∀ i j , a i j = a j i)

structure SubalgebraBuilderLists
  (n : ℕ) [NeZero n] (R Q K : Type*) [CommRing R] [IsDomain R]
  [DecidableEq R] [Field Q][CommRing K][Algebra Q K]
  [Algebra R Q][Algebra R K] [IsScalarTower R Q K]
  [IsFractionRing R Q] (T : R[X]) (l : List R) where
  (d : R)
  (hlen : l.length = n + 1)
  (htr : l = l.dropTrailingZeros')
  (hofL : T = ofList l)
  (hm : l.getLast (List.ne_nil_of_length_eq_add_one hlen) = 1)
  (B : Fin n → (Fin n → R))
  (a : Fin n → Fin n → Fin n → R)
  (s : Fin n → Fin n → List R)
  (h : IsAdjoinRoot K (map (algebraMap R Q) T))
  (honed : (List.ofFn (B 0)).dropTrailingZeros' = [d])
  (hd : d ≠ 0)
  (hcc : ∀ i j, j < i → B j i = 0 )
  (hin : ∀ i, B i i ≠ 0)
  (hsymma : ∀ i j , a i j = a j i)

variable {n : ℕ} [NeZero n] {R Q K : Type*} [CommRing R]
[IsDomain R]
[Field Q][CommRing K][Algebra Q K]
[Algebra R Q][Algebra R K]
[IsScalarTower R Q K]
[IsFractionRing R Q]

noncomputable def subalgebraOfPolysInt [IsFractionRing R Q]: Subalgebra R K := by sorry

noncomputable def subalgebraOfBuilder
  (T : R[X])
  (A : SubalgebraBuilder n R Q K T) : Subalgebra R K := by sorry

/-- Constructs the corresponding term `SubalgebraBuilder` from `SubalgebraBuilderLists`· -/
noncomputable def SubalgebraBuilderOfList [DecidableEq R](T : R[X])(l : List R)
  (A : SubalgebraBuilderLists n R Q K T l) : SubalgebraBuilder n R Q K T :=
  {d := A.d,
    hdeg := by sorry,
    hm := by sorry,
    B := fun i => ofList (List.ofFn (A.B i)),
    a := A.a,
    s := fun i j => ofList (A.s i j),
    h := A.h,
    c := fun i => fun j => A.B j i,
    honed := by sorry,
    hd := A.hd,
    hpoly := by sorry,
    hcc := A.hcc,
    hin := A.hin,
    hsymma := A.hsymma
}

noncomputable def basisOfBuilder
  (T : R[X])
  (A : SubalgebraBuilder n R Q K T) : Basis (Fin n) R (subalgebraOfBuilder T A) := by sorry

/-- The subalgebra obtained from the `SubalgebraBuilderLists`· -/
noncomputable def subalgebraOfBuilderLists [DecidableEq R](T : R[X])(l : List R)
    (A : SubalgebraBuilderLists n R Q K T l) :  Subalgebra R K :=
    subalgebraOfBuilder T (SubalgebraBuilderOfList T l A)

/-- The basis for the subalgebra obtained from the `SubalgebraBuilderLists`· -/
noncomputable def basisOfBuilderLists [DecidableEq R](T : R[X])(l : List R)
    (A : SubalgebraBuilderLists n R Q K T l) : Basis (Fin n) R (subalgebraOfBuilderLists T l A) :=
    basisOfBuilder T (SubalgebraBuilderOfList T l A)

/-- The basis is precisely `wⱼ  = (1/d) * Bⱼ(θ) ` -/
lemma basisOfBuilderLists_apply [DecidableEq R](T : R[X])(l : List R)
    (A : SubalgebraBuilderLists n R Q K T l)(i : Fin n) :
    ((basisOfBuilderLists T l A) i).val =
    (A.h).map (C (algebraMap R Q A.d)⁻¹ * map (algebraMap R Q) (ofList (List.ofFn (A.B i)))) := by sorry

/--
  Everything above this has been copy/pasted from Baanen--Villarello--Dahmen.
  Below is what I'm asking about.
-/

noncomputable def T : ℤ[X] := X^2 + 7
lemma T_def : T = X^2 + 7 := rfl

local notation "K" => AdjoinRoot (map (algebraMap ℤ ℚ) T)
local notation "l" => [7, 0, 1]

noncomputable def Adj : IsAdjoinRoot K (map (algebraMap ℤ ℚ) T) :=
   AdjoinRoot.isAdjoinRoot _

local notation "θ" => Adj.root

lemma T_ofList : ofList l = T := by sorry

-- We build the subalgebra with integral basis (1, 1/2*a + 1/2)

noncomputable def BQ : SubalgebraBuilderLists 2 ℤ  ℚ K T l where
 d :=  2
 hlen := rfl
 htr := rfl
 hofL := T_ofList.symm
 hm := rfl
 B := ![![2, 0], ![1, 1]]
 a := ![ ![![1, 0],![0, 1]],
![![0, 1],![-2, 1]]]
 s := ![![[], []],![[], [-1]]]
 h := Adj
 honed := by decide!
 hd := by norm_num
 hcc := by decide
 hin := by decide
 hsymma := by decide

lemma T_monic : Monic T := by sorry

lemma T_irreducible : Irreducible T := sorry

noncomputable def O := subalgebraOfBuilderLists T l BQ

noncomputable def B : Basis (Fin 2) ℤ O := basisOfBuilderLists T l BQ

instance : Fact $ (Irreducible (map (algebraMap ℤ ℚ) T)) where
out :=  (Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map (T_monic)).1 T_irreducible

theorem  O_ringOfIntegers' : O = NumberField.RingOfIntegers K := by sorry

-- Let α = (1 + θ) / 2, which is our basis element `B 1`
noncomputable def α : O := B 1

-- Let α_bar = (1 - θ) / 2, which is `1 - α` or `B 0 - B 1`
noncomputable def α_bar : O := B 0 - B 1

lemma Adj_map_C_eq_id (r : ℚ) : Adj.map (C r) = (r : K) := by
  unfold IsAdjoinRoot.map
  exact rfl

/-- Formally proves that 2 = ( (1 + θ)/2 ) * ( (1 - θ)/2 ) inside the ring O -/
theorem two_splits_explicitly : (2 : O) = α * α_bar := by
  -- We prove this by "lifting" the calculation to the field K,
  -- where we can use division and `field_simp`.
  apply Subtype.ext -- Proves equality in O by proving equality of the underlying K elements

  -- The goal is now in K: `(2 : K) = α.val * α_bar.val`
  simp
  -- We need the values of the basis elements B 0 and B 1 in K
  have hB0 : (B 0).val = (1 : K) := by
    calc
      (B 0).val = ((basisOfBuilderLists T [7, 0, 1] BQ) 0).val := by
        -- Unfold B, which also unfolds l
        rw [B]
        rfl
      _ = ((basisOfBuilderLists T l BQ) 0).val := by
        -- Fold [7, 0, 1] back into l
        rfl
      _ = (1 / BQ.d) * (BQ.B 0 0 * θ ^ 0 + BQ.B 0 1 * θ ^ 1) := by
        rw [basisOfBuilderLists_apply]
        simp [BQ]
        have fact1 : Adj.map (Polynomial.C 2⁻¹) = (1/2 : K) := by
          rw [Adj_map_C_eq_id]
          ring
        sorry -- previously this was `exact congrFun (congrArg HMul.hMul fact1) (Adj.map 2)` but after removing `hc_le` from the builder structs this doesn't work anymore
      _ = (1 / (2:ℚ)) * ( (2:ℚ) * θ ^ 0 + (0:ℚ) * θ ^ 1) := by
        -- Unfold BQ and access the matrix elements
        simp only [BQ, Fin.val_zero, Fin.val_one, Matrix.cons_val_zero]
        norm_num
      _ = (1 / (2:ℚ)) * ( (2:ℚ) * 1 + 0) := by
        -- Simplify powers of θ and multiplication by 0
        simp only [pow_zero, pow_one, mul_zero, add_zero]
        norm_num
      _ = (1 / (2:ℚ)) * (2:ℚ) := by
         -- Simplify multiplication by 1
        rw [mul_one]
        simp
      _ = 1 := by
        ring

  have hB1 : (B 1).val = (1 + θ) / 2 := by
    calc
      (B 1).val = ((basisOfBuilderLists T [7, 0, 1] BQ) 1).val := by
        rw [B]
        rfl
      _ = ((basisOfBuilderLists T l BQ) 1).val := by
        rfl
      _ = (1 / BQ.d) * (BQ.B 1 0 * θ ^ 0 + BQ.B 1 1 * θ ^ 1) := by
        rw [basisOfBuilderLists_apply]
        -- We need to prove `Adj.map (C 2⁻¹ * (C 1 + C 1 * X)) = (1 / 2) * (1 * 1 + 1 * θ)`
        -- `simp` can handle this by unfolding definitions and using lemmas
        simp [BQ, map_add, map_mul, Adj_map_C_eq_id]
        have fact1 : Adj.map (Polynomial.C 2⁻¹) = (1/2 : K) := by
          rw [Adj_map_C_eq_id]
          ring
        rw [←congrFun (congrArg HMul.hMul fact1) (1 + Adj.root)]
        sorry -- previously this was finished with rfl
      _ = (1 / (2:ℚ)) * ( (1:ℚ) * θ ^ 0 + (1:ℚ) * θ ^ 1) := by
        -- Unfold BQ and access the matrix elements
        simp only [BQ, Fin.val_zero, Fin.val_one]
        norm_num
      _ = (1 / (2:ℚ)) * ( (1:ℚ) * 1 + (1:ℚ) * θ) := by
        -- Simplify powers of θ
        simp only [pow_zero, pow_one]
      _ = (1 / (2:ℚ)) * (1 + θ) := by
        -- Simplify multiplication by 1
        simp only [mul_one, one_mul]
        norm_num
      _ = (1 + θ) / 2 := by
        -- Rearrange to the `div` form
        rw [div_eq_inv_mul, mul_comm]
        ring

  have hB2 : (B 0 - B 1).val = (1 - θ) / 2 := by
    calc
      (B 0 - B 1).val = (B 0).val - (B 1).val := by
        rw [Subalgebra.coe_sub]
      _ = 1 - (1 + θ) / 2 := by rw [hB0, hB1]
      _ = (2/2) - (1 + θ) / 2 := by norm_num
      _ = (2 - (1 + θ)) / 2 := by
        rw [div_sub_div_same]
      _ = (1 - θ) / 2 := by
        rw [sub_add_eq_sub_sub_swap]
        ring
  rw [α]
  rw [α_bar]
  rw [hB2, hB1]
  -- -- Now we can use `field_simp` to finish the calculation in K
  -- ring_nf
  have h_theta_sq : θ ^ 2 = - (7 : K) := by
    -- This follows from the fact that θ is a root of T
    have h_root : aeval θ (map (algebraMap ℤ ℚ) T) = 0 :=
      Adj.aeval_root
    simp [T_def] at h_root
    exact Eq.symm (neg_eq_of_add_eq_zero_left h_root)
  symm
  calc
    (1 + θ) / 2 * ((1 - θ) / 2) = (1 - θ ^ 2) / 4 := by ring
    _ = (1 - (-7 : K)) / 4       := by rw [h_theta_sq]
    _ = (8 : K) / 4              := by norm_num
    _ = 2                        := by norm_num

[Kevin Buzzard]

If you click on the "view in Lean 4 playground" link at the top right of your code then you'll see all the errors which are currently in your code (which means that it's still not a #mwe ). You can just edit the code, no need to re-post. Also note that you'll see some variables initialised in grey (for example the first instance of this is on line 18) -- these sometimes indicate that you're not quite doing what you mean to do; in mathlib these would be further errors. You can make these go away with variable commands.

Finally, you say "what I'm asking about is roughly the second half of what i've pasted below." but what is your precise question about this code?

[Kevin Buzzard]

PS thanks a lot for your minimisation work so far -- it greatly increases the chances you'll get an answer to your question!

[Riccardo Brasca]

@Barinder S Banwait do you want to use the various implementations of the paper or would you be happy to use mathlib? I think it's really not that difficult to prove the statement you want in current mathlib

[Riccardo Brasca]

I mean something like

import Mathlib

namespace foo

open Polynomial NumberField QuadraticAlgebra RingOfIntegers Algebra Nat Ideal
  UniqueFactorizationMonoid

notation "K" => QuadraticAlgebra ℚ 0 (-7)

instance : Fact (∀ (r : ℚ), r^2 ≠ 0 + (-7)*r) := by
  sorry

instance : NumberField K := by
  sorry

notation "R" => (𝓞 K)

lemma is_integral_ω : IsIntegral ℤ (ω : K) := by
  sorry

set_option quotPrecheck false in
notation "θ" => (⟨ω, is_integral_ω⟩ : 𝓞 K)

lemma minpoly : minpoly ℤ θ = X ^ 2 - X + 2 := by
  sorry

lemma span_eq_top : adjoin ℤ {θ} = ⊤ := by
  sorry

lemma exponent : exponent θ = 1 := by
  rw [exponent_eq_one_iff, span_eq_top]

lemma ne_dvd_exponent (p : ℕ) [hp : Fact p.Prime] : ¬ (p ∣ RingOfIntegers.exponent θ) := by
  rw [exponent, dvd_one]
  exact hp.1.ne_one

lemma factors : monicFactorsMod θ 2 = {X, X - 1} := by
  have : (X ^ 2 - X + 2 : ℤ[X]).map (Int.castRingHom (ZMod 2)) = X * (X - 1) := by
    calc (X ^ 2 - X + 2 : ℤ[X]).map (Int.castRingHom (ZMod 2)) = X ^ 2 - X := by
          simp [CharTwo.two_eq_zero]
                                                        _ = X * (X - 1) := by ring
  rw [monicFactorsMod, minpoly, this, normalizedFactors_mul X_ne_zero sorry, Multiset.toFinset_add,
    normalizedFactors_irreducible irreducible_X, normalizedFactors_irreducible sorry,
    Monic.normalize_eq_self (by monicity), Monic.normalize_eq_self (by monicity)]
  rfl

end foo

[Riccardo Brasca]

All the sorry should be very easy except span_eq_top, that is the computation of the ring of integers. Then, since you know monicFactorsMod θ 2 you can use NumberField.Ideal.primesOverSpanEquivMonicFactorsMod to get completely explicitly the set of ideals over (2).

[Barinder S Banwait]

If you click on the "view in Lean 4 playground" link at the top right of your code

That's a cool feature!

then you'll see all the errors which are currently in your code (which means that it's still not a #mwe ).

hmmm, it compiles locally for me. Note that I've been working in the project environment of the aforementioned authors, where the lean-toolchain is leanprover/lean4:v4.14.0-rc2 which i think means it's using a much older version of lean and/or mathlib. i did observe that doing lake update introduced lots of errors in the project.

Also note that you'll see some variables initialised in grey (for example the first instance of this is on line 18) -- these sometimes indicate that you're not quite doing what you mean to do; in mathlib these would be further errors. You can make these go away with variable commands.

thanks for that additional info :+1:

Finally, you say "what I'm asking about is roughly the second half of what i've pasted below." but what is your precise question about this code?

The precise question is "Is there a simpler way of doing this that isn't so long?" And @Riccardo Brasca's code shows that to be the case

[Barinder S Banwait]

@Riccardo Brasca thank you so much for providing this code and template, it's a huge help! especially as it's using latest Mathlib. indeed, I don't need to be using the code of the paper; that's just what I was first led to, and i wanted to see it through. i'll work on fleshing out your code and removing the sorry's :working_on_it:

[Ruben Van de Velde]

Just as a heads-up: we won't be able to help with issues that are specific to lean 4.14

[Barinder S Banwait]

yep that makes sense ... as i wrote in response to Riccardo, i'm not wedded to using that code written in older mathlib, and will proceed with the latest version