Project update

Stream: FLT-regular

[Riccardo Brasca]

Just a quick update: everything that was in cyclotomic.basic is now in mathlib. I will start PRing the definition and basic properties of zeta this week: this will allow to having the computation of the discriminant in mathlib.

Concerning the general advancement, I've almost finished proving the Eiseistein criterion for the ring of integers, lemma 2.13 of the blueprint. With this result the computation of the ring of integers is morally done, even we will need some glue to convince Lean. After that we will probable need to think a little bit about the general strategy, but this will already be a nice milestone.

[Riccardo Brasca]

instance {p : ℕ+} [hp : fact (p : ℕ).prime] (hodd : p ≠ 2) :
  is_integral_closure (cyclotomic_ring p ℤ ℚ) ℤ (cyclotomic_field p ℚ) :=

is proved (of course this holds also for p=2, but that should be easy). By definition

def cyclotomic_ring : Type w := adjoin A { b : (cyclotomic_field n K) | b ^ (n : ℕ) = 1 }

So this gives the usual description of the ring of integers of a cyclotomic field.

[Riccardo Brasca]

We will probably need some reformulation, maybe using is_cyclotomic_extension, but mathematically it is done.

[Kevin Buzzard]

Speaking as someone who once had to plough through several research papers which started with the words "let p be an odd prime" because I had to make all the arguments work for p=2, I'm interested in knowing why the proof you formalised didn't work for p=2.

[Riccardo Brasca]

Nothing special: the proof is the usual argument via the discriminant: an element x in the ring of integer lies in ℤ[ζ - 1] after multiplication by the discriminant, that is some power of p is p ≠ 2. But the minimal polynomial of ζ - 1 is Eiseinstein at p, so this implies that x is in ℤ [ζ - 1]. docs#is_cyclotomic_extension.discr_odd_prime is not true for p=2.

[Riccardo Brasca]

Of course for p=2 there is nothing to prove :D

[Riccardo Brasca]

I think that everything boils down to docs#is_primitive_root.norm_eq_one not holding if n=2

[Kevin Buzzard]

One thing I really like about Lean is that we tend to keep track of these things. "Let p be an odd prime" is such an evil way to start a paper, because 95% of the proofs work fine when p=2 and it's only a few of them which break, however if the paper in question is Ribet's paper which proves level-lowering for odd primes and you need it for p=2 to prove some old conjecture of Artin then it's really painful to find out what you need to do because you need to check all the references of the paper for p>2 hypotheses as well. With formalisation all these problems are answered instantly because you just remove the hypotheses and immediately see what breaks.

[Kevin Buzzard]

Riccardo Brasca said:

I think that everything boils down to docs#is_primitive_root.norm_eq_one not holding if n=2

That theorem should say $N(\zeta_p)=(-1)^{p-1}$ then ;-)

[Riccardo Brasca]

I don't have a lot of time to work on flt because of teaching, but

lemma discr_odd_prime_pow [is_cyclotomic_extension {p ^ (k + 1)} K L] [hp : fact (p : ℕ).prime]
  (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))
  (hirr₁ : irreducible (cyclotomic (p : ℕ) K))
  (hodd : p ≠ 2) : discr K (hζ.power_basis K).basis =
  (-1) ^ (((p : ℕ) - 1) / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1))

is now proved. This is the last discriminant computation I want to do for this project (the general case is really harder). In next days I hope I will have the time to put everything together and PR this and the description of the ring of integers.

[Johan Commelin]

Nice! That will be a good milestone!

[Riccardo Brasca]

Just a quick update: everything that was in cyclotomic.basic is now in mathlib. I will start PRing the definition and basic properties of zeta this week: this will allow to having the computation of the discriminant in mathlib.

Concerning the general advancement, I've almost finished proving the Eiseistein criterion for the ring of integers, lemma 2.13 of the blueprint. With this result the computation of the ring of integers is morally done, even we will need some glue to convince Lean. After that we will probable need to think a little bit about the general strategy, but this will already be a nice milestone.

[Riccardo Brasca]

instance {p : ℕ+} [hp : fact (p : ℕ).prime] (hodd : p ≠ 2) :
  is_integral_closure (cyclotomic_ring p ℤ ℚ) ℤ (cyclotomic_field p ℚ) :=

is proved (of course this holds also for p=2, but that should be easy). By definition

def cyclotomic_ring : Type w := adjoin A { b : (cyclotomic_field n K) | b ^ (n : ℕ) = 1 }

So this gives the usual description of the ring of integers of a cyclotomic field.

[Riccardo Brasca]

We will probably need some reformulation, maybe using is_cyclotomic_extension, but mathematically it is done.

[Kevin Buzzard]

Speaking as someone who once had to plough through several research papers which started with the words "let p be an odd prime" because I had to make all the arguments work for p=2, I'm interested in knowing why the proof you formalised didn't work for p=2.

[Riccardo Brasca]

Nothing special: the proof is the usual argument via the discriminant: an element x in the ring of integers lies in ℤ[ζ - 1] after multiplication by the discriminant, that is some power of p if p ≠ 2. But the minimal polynomial of ζ - 1 is Eiseinstein at p, so this implies that x is in ℤ [ζ - 1]. docs#is_cyclotomic_extension.discr_odd_prime is not true for p=2.

[Riccardo Brasca]

Of course for p=2 there is nothing to prove :D

[Riccardo Brasca]

I think that everything boils down to docs#is_primitive_root.norm_eq_one not holding if n=2

[Kevin Buzzard]

One thing I really like about Lean is that we tend to keep track of these things. "Let p be an odd prime" is such an evil way to start a paper, because 95% of the proofs work fine when p=2 and it's only a few of them which break, however if the paper in question is Ribet's paper which proves level-lowering for odd primes and you need it for p=2 to prove some old conjecture of Artin then it's really painful to find out what you need to do because you need to check all the references of the paper for p>2 hypotheses as well. With formalisation all these problems are answered instantly because you just remove the hypotheses and immediately see what breaks.

[Kevin Buzzard]

Riccardo Brasca said:

I think that everything boils down to docs#is_primitive_root.norm_eq_one not holding if n=2

That theorem should say $N(\zeta_p)=(-1)^{p-1}$ then ;-)

[Riccardo Brasca]

I don't have a lot of time to work on flt because of teaching, but

lemma discr_odd_prime_pow [is_cyclotomic_extension {p ^ (k + 1)} K L] [hp : fact (p : ℕ).prime]
  (hζ : is_primitive_root ζ ↑(p ^ (k + 1))) (hirr : irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))
  (hirr₁ : irreducible (cyclotomic (p : ℕ) K))
  (hodd : p ≠ 2) : discr K (hζ.power_basis K).basis =
  (-1) ^ (((p : ℕ) - 1) / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1))

is now proved. This is the last discriminant computation I want to do for this project (the general case is really harder). In next days I hope I will have the time to put everything together and PR this and the description of the ring of integers.

[Johan Commelin]

Nice! That will be a good milestone!