End of caseI

Stream: FLT-regular

[Riccardo Brasca]

We are very close to finish caseI, but the end of the proof may be quite painful to formalize, so let me resume the situation to see if anyone has any idea to simplify the proof. This is purely a Lean question, mathematically there is almost nothing to prove.

The situation is the following: we have a prime p such that p ≥ 5, a b c : ℤ such that ¬ p ∣ a * b * c, ¬a ≡ b [ZMOD p] and is_unit (({a, b, c} : finset ℤ).gcd id). We suppose that a * b * c ≠ 0 and we want to prove a ^ p + b ^ p ≠ c ^ p. The precise Lean statement is

theorem caseI_easier {a b c : ℤ} (hpri : p.prime)
  (hreg : is_regular_number p hpri.pos) (hp5 : 5 ≤ p) (hprod : a * b * c ≠ 0)
  (hgcd : is_unit (({a, b, c} : finset ℤ).gcd id))
  (hab : ¬a ≡ b [ZMOD p]) (caseI : ¬ ↑p ∣ a * b * c) : a ^ p + b ^ p ≠ c ^ p :=

(we already know this implies caseI).

[Riccardo Brasca]

Now, the math proof is the following: let $\zeta$ be a primitive $p$-th root of unity and let $K$ be $\mathbb{Q}(ζ)$, with ring of integers $R$. Using the regularity assumption, we can find $u ∈ R^\ast$ and $\alpha \in R$ such that $x+y\zeta=u \alpha$. This is also formalized (modulo a sorried statement, but this is irrelevant) as

theorem is_principal {a b c : ℤ} {ζ : R} (hreg : is_regular_number p hpri.pos) (hp5 : 5 ≤ p)
  (hgcd : is_unit (({a, b, c} : finset ℤ).gcd id)) (caseI : ¬ ↑p ∣ a * b * c)
  (H : a ^ p + b ^ p = c ^ p) (hζ : is_primitive_root ζ p) :
  ∃ (u : Rˣ) (α : R), ↑u * (α ^ p) = ↑a + ζ * ↑b

[Riccardo Brasca]

Now, this implies that there is $k \in \mathbb{Z}$ such that $a + b\zeta -\zeta^{2k}a -\zeta^{2k-1}b \equiv 0 \bmod{p}$. The end of the proof is the following: If $1,\zeta,\zeta^{2k},\zeta^{2k-1}$ are distinct, then this Lemma says that (since $p \geq 5$) $p$ divides $a,b$, contrary to our assumption. So they cannot be distinct, but checking each case leads to a contradiction, therefore there cannot be any such solutions.

[Riccardo Brasca]

I've formalized the Lemma as follows:

lemma dvd_coeff_cycl_integer [hp : fact (p : ℕ).prime] {ζ : L} (hζ : is_primitive_root ζ p)
  {f : fin p → ℤ} {i : fin p} (hf : f i = 0) {m : ℤ}
  (hdiv : ↑m ∣ ∑ j, f j • (⟨ζ, hζ.is_integral p.pos⟩ : 𝓞 L) ^ (j : ℕ)) : ∀ j, m ∣ f j

[Riccardo Brasca]

And the existence of $k$ as follows:

lemma exists_int_sum_eq_zero (hpodd : p ≠ 2) [hp : fact(p : ℕ).prime] {x y i : ℤ} {u : (𝓞 K)ˣ}
  {α : 𝓞 K} (h : (x : 𝓞 K) + y * (hζ.unit' ^ i : (𝓞 K)ˣ) = u * α ^ (p : ℕ)) :
  ∃ k : ℤ, (x : 𝓞 K) + y * (hζ.unit' ^ i : (𝓞 K)ˣ) - (hζ.unit' ^ (2 * k) : (𝓞 K)ˣ) *
    (x + y * (hζ.unit' ^ -i : (𝓞 K)ˣ)) ∈ ideal.span ({p} : set (𝓞 K))

here hζ.unit' is the primitive root as a unit of the ring of integers (this is necessary to take integer-valued powers).

[Riccardo Brasca]

There are several problem to glue these two statements. First of all, in exists_int_sum_eq_zero the exponents are integers, not elements of fin p (it is necessary to go through fin p at some moment, since the proof of dvd_coeff_cycl_integer uses the power basis given by $\zeta$, that is indexed over fin p). Of course we can modify exists_int_sum_eq_zero to use fin p exponents, but and this is what I started doing.

[Riccardo Brasca]

Then one has to build f to apply dvd_coeff_cycl_integer, and this is going to be a pain I think. Then we one has to consider the remaining cases (when the $1,\zeta,\zeta^{2k},\zeta^{2k-1}$ are not all distinct), and also this will be a pain I am afraid.

[Riccardo Brasca]

My current idea is to avoid dvd_coeff_cycl_integer completely, at least in the form it is stated now and proving that p ∣ a and p ∣ b (leading to a contradiction) by hand, reusing the proof of dvd_coeff_cycl_integer`.

[Riccardo Brasca]

In practice, it shouldn't be too hard to prove that p divides the coefficient of 1 in the expansion of $a + b\zeta -\zeta^{2k}a -\zeta^{2k-1}b$. This coefficients is a unless \zeta^{2k} = 1 or \zeta^{2k-1}= 1 (that is impossible, and this should be proved before). Then proceed similarly for b. There will still be four preliminary thing to prove, but at least we can avoid building f.

[Riccardo Brasca]

Sorry for the long message, but if anyone has any better idea I am very happy to listen to any suggestion.

[Eric Rodriguez]

(I'm currently bumping, and btw: using linarith to show that p = 2 is not true when p ≥ 5 is super expensive timewise)

[Ruben Van de Velde]

Ai isn't putting us all out of jobs yet, huh

[Eric Rodriguez]

norm_num is fine though

[Eric Rodriguez]

I'll try to have some sort of a closer look at this tonight, but I may not get a chance so don't depend on it...

[Riccardo Brasca]

Is it because of pnat?

[Eric Rodriguez]

I'm not sure, I just know that two statements were taking super long until I removed linarith...

[Eric Rodriguez]

i think it's probably not "obvious" and the goal states are huge so it often traverses them all in an expensive way until it realises that that's the issue we want

[Eric Rodriguez]

on a state with just n, h: n = 2 and hp : 5 ≤ n, it takes ~500ms, which is not terrible

[Riccardo Brasca]

Oh really, they were super slow because of linarith?! I wanted to speed them up, but I thought the culprit was convert.

[Riccardo Brasca]

So well done!

[Patrick Stevens]

Out of pure curiosity, does linarith only still take 500ms?

[Eric Rodriguez]

linarith only is a thing? probably not, then

[Riccardo Brasca]

I tried avoiding defining f : fin p → R but it's a pain. I will see tomorrow if defining f on fin p giving the values on 0, 1 and p-1 is also painful... in any case I am sure that the end of case I is just a matter of perseverance.

[Kevin Buzzard]

I thought about this a bit. Can't you define f to be the sum of "if x=0 then a else if x=1 then b else 0" and "if x=2k then -a else if x=2k-1 then -b else 0" and then split on whether 2k=0?

[Riccardo Brasca]

Yes, that's the idea. I also thought about using docs#set.indicator. I have to try to see how annoying is to connect the sum over fin p to the actual sum of four elements and similar things.

[Riccardo Brasca]

This approach is definitely better, even if not completely painless. See here for a precise question.

[Riccardo Brasca]

Using @Floris van Doorn's suggestion everything it's much much better!

[Riccardo Brasca]

I've finished the proof of the main statement of caseI.

This means that the only sorry left is flt_ideals_coprime. @Chris Birkbeck what is the situation with this lemma? Do you think we're close to it?

[Riccardo Brasca]

Well, it seems we are very close. I am working on the sorry in src/number_theory/cyclotomic/cycl_rat.lean

[Riccardo Brasca]

We were indeed really close.

theorem caseI {a b c : ℤ} {p : ℕ} (hpri : p.prime) (hreg : is_regular_number p hpri.pos)
  (hodd : p ≠ 2) (caseI : ¬ ↑p ∣ a * b * c) : a ^ p + b ^ p ≠ c ^ p :=
flt_regular.caseI.may_assume (λ x y z p₁ Hpri Hreg HP5 Hunit Hxy HI,
    caseI_easier Hpri Hreg HP5 Hunit Hxy HI) hpri hreg hodd caseI

#print axioms caseI --propext quot.sound classical.choice

[Riccardo Brasca]

It's probably a good idea to do some cleanup and reorganize certain files before starting thinking about caseII. Also, quite a lot of stuff is more or less suitable to be PRed, and I think it's better to do it sooner than later.

[Riccardo Brasca]

For example I started using (hpri: p.prime) instead of fact for some reason, but fact is surely better.

[Kevin Buzzard]

Is the blueprint updated to say case 1 is done? When there's something I can point to and tweet about I'll tweet about it

[Riccardo Brasca]

Yes, the blueprint is updated, and also the dependency graph is (at least for case 1, for case 2 it's still just a very preliminary draft).

[Kevin Buzzard]

Why do you assume p odd?

[Kevin Buzzard]

hreg : is_regular_number p hpri.pos -- you didn't ever define is_regular_prime p? It would read much better!

[Riccardo Brasca]

The statement is not optimized at all. As I said we need to improve a lot of stuff. The fact that p is prime should be a fact instance, so it should disappear, it's there because I was lazy. But I can change is_regular_prime quickly, let me do it.

[Riccardo Brasca]

Now the statement is

theorem caseI {a b c : ℤ} {p : ℕ} [fact p.prime] (hreg : is_regular_prime p)
  (hodd : p ≠ 2) (caseI : ¬ ↑p ∣ a * b * c) : a ^ p + b ^ p ≠ c ^ p :=
flt_regular.caseI.may_assume (λ x y z p₁ Hpri Hreg Hp5 Hunit Hxy HI H,
  by exactI caseI_easier p₁ Hreg Hp5 Hunit Hxy HI H) hreg hodd caseI

I am done for today, but anyone who wants to remove hodd is welcome to do so. It should be very easy.

[Chris Birkbeck]

Sorry I just saw this now. I think yes we should be really close. The coprime ideal bits shouldn't be hard. I'll try and do some more tomorrow!

[Chris Birkbeck]

Oh wait? Did you fill these sorries? I'm on mobile right now and can't check

[Kevin Buzzard]

yeah that theorem is sorry-free!

[Chris Birkbeck]

Oh great!! Then I won't do that tomorrow:)

[Chris Birkbeck]

I'll think more about case ii then

[Riccardo Brasca]

I propose to ignore kummer's lemma for now, and prove it for strongly regular primes (or whatever the name we chose)

[Johan Commelin]

Congratulations to everyone involved!!! :octopus: :tada: :beers:

[Chris Birkbeck]

[Quoting…]
Yeah I agree, the thing is the proof I've seen also uses that if $p$ is regular then $p \nmid h^+$ where $h^+$ is the class number of $\mathbb{Q}(\zeta_p+\zeta_p^{-1})$ and I think the proof of this also uses CFT (or at least the proof in Washington)

[Kevin Buzzard]

But CFT didn't exist in 1847

[Chris Birkbeck]

True. There are other proofs, but for example for Kummers lemma the other proof I know uses some $p$-adic regulator and such, which is also quite annoying

[Chris Birkbeck]

But I've not yet gone through all the proofs!

[Kevin Buzzard]

Why do you need CFT for this statement? If p divides h+ then there's some unram degree p extension of the totally real field which gives you an unram degree p extension of the cyclo field

[Kevin Buzzard]

Aah is the point that you need CFT to make the unram extension from the class group

[Chris Birkbeck]

yes exactly

[Chris Birkbeck]

but actually I think I'm wrong about needing CFT. If we use strongly regular prime or whatever, then I think one can prove this without that. but I've not gone through the details yet

[Riccardo Brasca]

I think we can follow the notes by Keith Conrad, modulo kummer's lemma the proof seems more or less elementary

[Chris Birkbeck]

Hmm you're right, it doesn't even seem to mention $h^+$.

[Riccardo Brasca]

Of course in 2 years it would be nice to connect regularity to Bernoulli's numbers, so we can prove 5 is regular...

[Chris Birkbeck]

In fact, what's in Conrads notes doesn't even need the link to Bernoulli numbers (as I don't think you need them for Kummers lemma).

[Riccardo Brasca]

The connection is nice to prove that a given prime is regular

[Riccardo Brasca]

At least, it gives a very simple criterion

[Chris Birkbeck]

Sure thats true. I just find it weird the Washington seems to have to work a lot harder for case II even using Kummers lemma. In particular those proofs go via this $h^+$ thing

[Chris Birkbeck]

@Riccardo Brasca can you change the name of aux.lean to something else? Windows doesn't like that name and wont let me pull the updates (or at least thats what I think the problem is (from my googling))

[Riccardo Brasca]

Strange error, but no problem

[Chris Birkbeck]

windows does let you name files aux.blah apparently...

[Riccardo Brasca]

done

[Riccardo Brasca]

its aux_lemmas.lean

[Riccardo Brasca]

I hope it's ok. In any case you can also change it online using github interface I think

[Chris Birkbeck]

that worked! thank you!

[Eric Rodriguez]

it's the same thing as con1 and stuff I think

[Eric Rodriguez]

some really old compatibility nonsense

[Thomas Browning]

Chris Birkbeck said:

[Quoting…]
Yeah I agree, the thing is the proof I've seen also uses that if $p$ is regular then $p \nmid h^+$ where $h^+$ is the class number of $\mathbb{Q}(\zeta_p+\zeta_p^{-1})$ and I think the proof of this also uses CFT (or at least the proof in Washington)

I think you might be able to use Proposition 1.2.1 from https://sites.math.washington.edu/~greenber/book.pdf
The idea is that the composition $Cl_{\mathbb{Q}(\zeta_p+\zeta_p^{-1})}\to Cl_{\mathbb{Q}(\zeta_p)}\to Cl_{\mathbb{Q}(\zeta_p+\zeta_p^{-1})}$ is given by squaring.

[Thomas Browning]

So the first map can only kill off powers of 2, but not any factors of p.

[Chris Birkbeck]

Oh that's neat! Looking at Conrad's notes it seems we might not need anything about $h^+$ but this is good to know :)

[Riccardo Brasca]

We are very close to finish caseI, but the end of the proof may be quite painful to formalize, so let me resume the situation to see if anyone has any idea to simplify the proof. This is purely a Lean question, mathematically there is almost nothing to prove.

The situation is the following: we have a prime p such that p ≥ 5, a b c : ℤ such that ¬ p ∣ a * b * c, ¬a ≡ b [ZMOD p] and is_unit (({a, b, c} : finset ℤ).gcd id). We suppose that a * b * c ≠ 0 and we want to prove a ^ p + b ^ p ≠ c ^ p. The precise Lean statement is

theorem caseI_easier {a b c : ℤ} (hpri : p.prime)
  (hreg : is_regular_number p hpri.pos) (hp5 : 5 ≤ p) (hprod : a * b * c ≠ 0)
  (hgcd : is_unit (({a, b, c} : finset ℤ).gcd id))
  (hab : ¬a ≡ b [ZMOD p]) (caseI : ¬ ↑p ∣ a * b * c) : a ^ p + b ^ p ≠ c ^ p :=

(we already know this implies caseI).

[Riccardo Brasca]

Now, the math proof is the following: let $\zeta$ be a primitive $p$-th root of unity and let $K$ be $\mathbb{Q}(ζ)$, with ring of integers $R$. Using the regularity assumption, we can find $u ∈ R^\ast$ and $\alpha \in R$ such that $x+y\zeta=u \alpha$. This is also formalized (modulo a sorried statement, but this is irrelevant) as

theorem is_principal {a b c : ℤ} {ζ : R} (hreg : is_regular_number p hpri.pos) (hp5 : 5 ≤ p)
  (hgcd : is_unit (({a, b, c} : finset ℤ).gcd id)) (caseI : ¬ ↑p ∣ a * b * c)
  (H : a ^ p + b ^ p = c ^ p) (hζ : is_primitive_root ζ p) :
  ∃ (u : Rˣ) (α : R), ↑u * (α ^ p) = ↑a + ζ * ↑b

[Riccardo Brasca]

Now, this implies that there is $k \in \mathbb{Z}$ such that $a + b\zeta -\zeta^{2k}a -\zeta^{2k-1}b \equiv 0 \bmod{p}$. The end of the proof is the following: If $1,\zeta,\zeta^{2k},\zeta^{2k-1}$ are distinct, then this Lemma says that (since $p \geq 5$) $p$ divides $a,b$, contrary to our assumption. So they cannot be distinct, but checking each case leads to a contradiction, therefore there cannot be any such solutions.

[Riccardo Brasca]

I've formalized the Lemma as follows:

lemma dvd_coeff_cycl_integer [hp : fact (p : ℕ).prime] {ζ : L} (hζ : is_primitive_root ζ p)
  {f : fin p → ℤ} {i : fin p} (hf : f i = 0) {m : ℤ}
  (hdiv : ↑m ∣ ∑ j, f j • (⟨ζ, hζ.is_integral p.pos⟩ : 𝓞 L) ^ (j : ℕ)) : ∀ j, m ∣ f j

[Riccardo Brasca]

And the existence of $k$ as follows:

lemma exists_int_sum_eq_zero (hpodd : p ≠ 2) [hp : fact(p : ℕ).prime] {x y i : ℤ} {u : (𝓞 K)ˣ}
  {α : 𝓞 K} (h : (x : 𝓞 K) + y * (hζ.unit' ^ i : (𝓞 K)ˣ) = u * α ^ (p : ℕ)) :
  ∃ k : ℤ, (x : 𝓞 K) + y * (hζ.unit' ^ i : (𝓞 K)ˣ) - (hζ.unit' ^ (2 * k) : (𝓞 K)ˣ) *
    (x + y * (hζ.unit' ^ -i : (𝓞 K)ˣ)) ∈ ideal.span ({p} : set (𝓞 K))

here hζ.unit' is the primitive root as a unit of the ring of integers (this is necessary to take integer-valued powers).

[Riccardo Brasca]

There are several problem to glue these two statements. First of all, in exists_int_sum_eq_zero the exponents are integers, not elements of fin p (it is necessary to go through fin p at some moment, since the proof of dvd_coeff_cycl_integer uses the power basis given by $\zeta$, that is indexed over fin p). Of course we can modify exists_int_sum_eq_zero to use fin p exponents, but and this is what I started doing.

[Riccardo Brasca]

Then one has to build f to apply dvd_coeff_cycl_integer, and this is going to be a pain I think. Then we one has to consider the remaining cases (when the $1,\zeta,\zeta^{2k},\zeta^{2k-1}$ are not all distinct), and also this will be a pain I am afraid.

[Riccardo Brasca]

My current idea is to avoid dvd_coeff_cycl_integer completely, at least in the form it is stated now and proving that p ∣ a and p ∣ b (leading to a contradiction) by hand, reusing the proof of dvd_coeff_cycl_integer`.

[Riccardo Brasca]

In practice, it shouldn't be too hard to prove that p divides the coefficient of 1 in the expansion of $a + b\zeta -\zeta^{2k}a -\zeta^{2k-1}b$. This coefficients is a unless \zeta^{2k} = 1 or \zeta^{2k-1}= 1 (that is impossible, and this should be proved before). Then proceed similarly for b. There will still be four preliminary thing to prove, but at least we can avoid building f.

[Riccardo Brasca]

Sorry for the long message, but if anyone has any better idea I am very happy to listen to any suggestion.

[Eric Rodriguez]

(I'm currently bumping, and btw: using linarith to show that p = 2 is not true when p ≥ 5 is super expensive timewise)

[Ruben Van de Velde]

Ai isn't putting us all out of jobs yet, huh

[Eric Rodriguez]

norm_num is fine though

[Eric Rodriguez]

I'll try to have some sort of a closer look at this tonight, but I may not get a chance so don't depend on it...

[Riccardo Brasca]

Is it because of pnat?

[Eric Rodriguez]

I'm not sure, I just know that two statements were taking super long until I removed linarith...

[Eric Rodriguez]

i think it's probably not "obvious" and the goal states are huge so it often traverses them all in an expensive way until it realises that that's the issue we want

[Eric Rodriguez]

on a state with just n, h: n = 2 and hp : 5 ≤ n, it takes ~500ms, which is not terrible

[Riccardo Brasca]

Oh really, they were super slow because of linarith?! I wanted to speed them up, but I thought the culprit was convert.

[Riccardo Brasca]

So well done!

[Patrick Stevens]

Out of pure curiosity, does linarith only still take 500ms?

[Eric Rodriguez]

linarith only is a thing? probably not, then

[Riccardo Brasca]

I tried avoiding defining f : fin p → R but it's a pain. I will see tomorrow if defining f on fin p giving the values on 0, 1 and p-1 is also painful... in any case I am sure that the end of case I is just a matter of perseverance.

[Kevin Buzzard]

I thought about this a bit. Can't you define f to be the sum of "if x=0 then a else if x=1 then b else 0" and "if x=2k then -a else if x=2k-1 then -b else 0" and then split on whether 2k=0?

[Riccardo Brasca]

Yes, that's the idea. I also thought about using docs#set.indicator. I have to try to see how annoying is to connect the sum over fin p to the actual sum of four elements and similar things.

[Riccardo Brasca]

This approach is definitely better, even if not completely painless. See here for a precise question.

[Riccardo Brasca]

Using @Floris van Doorn's suggestion everything it's much much better!

[Riccardo Brasca]

I've finished the proof of the main statement of caseI.

This means that the only sorry left is flt_ideals_coprime. @Chris Birkbeck what is the situation with this lemma? Do you think we're close to it?

[Riccardo Brasca]

Well, it seems we are very close. I am working on the sorry in src/number_theory/cyclotomic/cycl_rat.lean

[Riccardo Brasca]

We were indeed really close.

theorem caseI {a b c : ℤ} {p : ℕ} (hpri : p.prime) (hreg : is_regular_number p hpri.pos)
  (hodd : p ≠ 2) (caseI : ¬ ↑p ∣ a * b * c) : a ^ p + b ^ p ≠ c ^ p :=
flt_regular.caseI.may_assume (λ x y z p₁ Hpri Hreg HP5 Hunit Hxy HI,
    caseI_easier Hpri Hreg HP5 Hunit Hxy HI) hpri hreg hodd caseI

#print axioms caseI --propext quot.sound classical.choice

[Riccardo Brasca]

It's probably a good idea to do some cleanup and reorganize certain files before starting thinking about caseII. Also, quite a lot of stuff is more or less suitable to be PRed, and I think it's better to do it sooner than later.

[Riccardo Brasca]

For example I started using (hpri: p.prime) instead of fact for some reason, but fact is surely better.

[Kevin Buzzard]

Is the blueprint updated to say case 1 is done? When there's something I can point to and tweet about I'll tweet about it

[Riccardo Brasca]

Yes, the blueprint is updated, and also the dependency graph is (at least for case 1, for case 2 it's still just a very preliminary draft).

[Kevin Buzzard]

Why do you assume p odd?

[Kevin Buzzard]

hreg : is_regular_number p hpri.pos -- you didn't ever define is_regular_prime p? It would read much better!

[Riccardo Brasca]

The statement is not optimized at all. As I said we need to improve a lot of stuff. The fact that p is prime should be a fact instance, so it should disappear, it's there because I was lazy. But I can change is_regular_prime quickly, let me do it.

[Riccardo Brasca]

Now the statement is

theorem caseI {a b c : ℤ} {p : ℕ} [fact p.prime] (hreg : is_regular_prime p)
  (hodd : p ≠ 2) (caseI : ¬ ↑p ∣ a * b * c) : a ^ p + b ^ p ≠ c ^ p :=
flt_regular.caseI.may_assume (λ x y z p₁ Hpri Hreg Hp5 Hunit Hxy HI H,
  by exactI caseI_easier p₁ Hreg Hp5 Hunit Hxy HI H) hreg hodd caseI

I am done for today, but anyone who wants to remove hodd is welcome to do so. It should be very easy.

[Chris Birkbeck]

Sorry I just saw this now. I think yes we should be really close. The coprime ideal bits shouldn't be hard. I'll try and do some more tomorrow!

[Chris Birkbeck]

Oh wait? Did you fill these sorries? I'm on mobile right now and can't check

[Kevin Buzzard]

yeah that theorem is sorry-free!

[Chris Birkbeck]

Oh great!! Then I won't do that tomorrow:)

[Chris Birkbeck]

I'll think more about case ii then

[Riccardo Brasca]

I propose to ignore kummer's lemma for now, and prove it for strongly regular primes (or whatever the name we chose)

[Johan Commelin]

Congratulations to everyone involved!!! :octopus: :tada: :beers:

[Chris Birkbeck]

[Quoting…]
Yeah I agree, the thing is the proof I've seen also uses that if $p$ is regular then $p \nmid h^+$ where $h^+$ is the class number of $\mathbb{Q}(\zeta_p+\zeta_p^{-1})$ and I think the proof of this also uses CFT (or at least the proof in Washington)

[Kevin Buzzard]

But CFT didn't exist in 1847

[Chris Birkbeck]

True. There are other proofs, but for example for Kummers lemma the other proof I know uses some $p$-adic regulator and such, which is also quite annoying

[Chris Birkbeck]

But I've not yet gone through all the proofs!

[Kevin Buzzard]

Why do you need CFT for this statement? If p divides h+ then there's some unram degree p extension of the totally real field which gives you an unram degree p extension of the cyclo field

[Kevin Buzzard]

Aah is the point that you need CFT to make the unram extension from the class group

[Chris Birkbeck]

yes exactly

[Chris Birkbeck]

but actually I think I'm wrong about needing CFT. If we use strongly regular prime or whatever, then I think one can prove this without that. but I've not gone through the details yet

[Riccardo Brasca]

I think we can follow the notes by Keith Conrad, modulo kummer's lemma the proof seems more or less elementary

[Chris Birkbeck]

Hmm you're right, it doesn't even seem to mention $h^+$.

[Riccardo Brasca]

Of course in 2 years it would be nice to connect regularity to Bernoulli's numbers, so we can prove 5 is regular...

[Chris Birkbeck]

In fact, what's in Conrads notes doesn't even need the link to Bernoulli numbers (as I don't think you need them for Kummers lemma).

[Riccardo Brasca]

The connection is nice to prove that a given prime is regular

[Riccardo Brasca]

At least, it gives a very simple criterion

[Chris Birkbeck]

Sure thats true. I just find it weird the Washington seems to have to work a lot harder for case II even using Kummers lemma. In particular those proofs go via this $h^+$ thing

[Chris Birkbeck]

@Riccardo Brasca can you change the name of aux.lean to something else? Windows doesn't like that name and wont let me pull the updates (or at least thats what I think the problem is (from my googling))

[Riccardo Brasca]

Strange error, but no problem

[Chris Birkbeck]

windows does let you name files aux.blah apparently...

[Riccardo Brasca]

done

[Riccardo Brasca]

its aux_lemmas.lean

[Riccardo Brasca]

I hope it's ok. In any case you can also change it online using github interface I think

[Chris Birkbeck]

that worked! thank you!

[Eric Rodriguez]

it's the same thing as con1 and stuff I think

[Eric Rodriguez]

some really old compatibility nonsense

[Thomas Browning]

Chris Birkbeck said:

[Quoting…]
Yeah I agree, the thing is the proof I've seen also uses that if $p$ is regular then $p \nmid h^+$ where $h^+$ is the class number of $\mathbb{Q}(\zeta_p+\zeta_p^{-1})$ and I think the proof of this also uses CFT (or at least the proof in Washington)

I think you might be able to use Proposition 1.2.1 from https://sites.math.washington.edu/~greenber/book.pdf
The idea is that the composition $Cl_{\mathbb{Q}(\zeta_p+\zeta_p^{-1})}\to Cl_{\mathbb{Q}(\zeta_p)}\to Cl_{\mathbb{Q}(\zeta_p+\zeta_p^{-1})}$ is given by squaring.

[Thomas Browning]

So the first map can only kill off powers of 2, but not any factors of p.

[Chris Birkbeck]

Oh that's neat! Looking at Conrad's notes it seems we might not need anything about $h^+$ but this is good to know :)