# Zulip Chat Archive

## Stream: FLT-regular

### Topic: Case I

#### Riccardo Brasca (Sep 07 2022 at 08:18):

We should be ready to think about a strategy to attack case I.

Looking at the blueprint, the first sorried result is

```
lemma flt_fact_2 {p : ℕ} [fact (p : ℕ).prime] (ph : 5 ≤ p) {x y z : ℤ} {i j : ℤ} (h : i ≠ j)
(hp : is_coprime x y) (h : x ^ p + y ^ p = z ^ p) : flt_ideals n x y i + flt_ideals n x y j = ⊤ :=
```

is anyone working/interested in working on this?

#### Riccardo Brasca (Sep 07 2022 at 08:37):

(note that I am renaming it to `flt_ideals_coprime`

.)

#### Eric Rodriguez (Sep 07 2022 at 14:05):

I think the definition of `flt_ideals`

was not yet too sure. I'm not sure how much time I'll have in the near future, but I'm trying to get the splitting field diamond merged in the background

#### Riccardo Brasca (Sep 07 2022 at 14:08):

This is already very nice! Can you link the PRs here?

#### Alex J. Best (Sep 07 2022 at 14:12):

I'm happy to have a go at this, maybe on the weekend, I've written some similarish proofs recently so hopefully it'll be ok (famous last words)

#### Eric Rodriguez (Sep 07 2022 at 14:15):

The current one holding stuff up is Anne's #16123, #16132 also by Anne continues this theme ~~but I'm not super sure whether it;'s necessary for the proof~~ and is necessary for the fix. When these are merged, I'll be able to PR the diamond fix properly

#### Riccardo Brasca (Sep 07 2022 at 14:27):

The definition of `flt_ideals`

looks reasonable to me. Maybe there is no need to use `zeta_runity`

, and `zeta`

is enough.

#### Riccardo Brasca (Sep 07 2022 at 14:27):

We can generalize it to the ring of integers of any cyclotomic extension of `ℚ`

, but I don't thinks it is necessary.

#### Riccardo Brasca (Sep 09 2022 at 15:15):

Also, we are missing the statement of Lemma 4.4 (that is called `exists_int_sum_eq_zero`

in the tex file, I suggest to keep the same name in Lean) and Lemma 4.5 (called `may_assume_coprime`

). Then all the statements leading to case I will be formalized.

#### Riccardo Brasca (Sep 09 2022 at 15:15):

I will do this next week if nobody does it during the weekend.

#### Riccardo Brasca (Sep 28 2022 at 08:19):

@Chris Birkbeck Am I right in saying that in lemma 4.3 of the blueprint we need to assume that $a_i = 0$ for some $i$? Otherwise I don't understand the proof...

#### Riccardo Brasca (Sep 28 2022 at 08:27):

I am actually even more confused: you write $\alpha = a_0 + a_1 \zeta + \cdots + a_{p-1}\zeta^{p-1}$, but we can always suppose that $a_{p-1} = 0$, since the other already form a basis. Let me think a little bit.

#### Riccardo Brasca (Sep 28 2022 at 08:28):

Oh, you mean that you take *any* way of writing $\alpha$ in that way, the $a_i$'s are not coordinates.

#### Riccardo Brasca (Sep 28 2022 at 08:29):

So I need to change the Lean statement.

#### Riccardo Brasca (Sep 28 2022 at 08:33):

In any case the assumption $a_i = 0$ for some $i$ seems necessary (and Washington has it).

#### Riccardo Brasca (Sep 30 2022 at 12:12):

The proof is now formalized.

#### Chris Birkbeck (Sep 30 2022 at 12:15):

Oh amazing!

#### Riccardo Brasca (Sep 30 2022 at 12:16):

Interestingly enough, I had to modify the proof written in the blueprint. The sentence "any subset of $\{1,\zeta, \ldots, \zeta^{p-1}\}$ with $p-1$ elements is a $\mathbb{Z}$-basis of the ring of integers" is the typical thing that it is a nightmare to formalize.

#### Chris Birkbeck (Sep 30 2022 at 12:18):

Yeah, I'm sorry, maybe I sloppy there

#### Riccardo Brasca (Sep 30 2022 at 12:23):

It's mathematically OK (Washington does the same), it's just that "basis" is a strange concept. Anyway, do you confirm we can assume $a_i=0$ for some $i$?

#### Riccardo Brasca (Sep 30 2022 at 12:29):

Also, `p > 3`

is not needed.

#### Chris Birkbeck (Sep 30 2022 at 12:32):

Yes I think thats fine. Also it should say "any subset of p-2 elements" in the blueprint, thats a typo

#### Chris Birkbeck (Sep 30 2022 at 12:33):

Riccardo Brasca said:

Also,

`p > 3`

is not needed.

oh yes nice, I think I just added it since we had it for the final goal

#### Riccardo Brasca (Sep 30 2022 at 12:38):

My next step is to (state and) prove Lemma 4.4 and Lemma 4.5. I think it is better to wait before proving Lemma 4.1, since the statement may need to be modified, and so it's probably a good idea to use it to prove Case I.

#### Chris Birkbeck (Sep 30 2022 at 13:07):

That sounds good. I have time for this next week so I can try and help do one of these lemmas. I might also try and think about a strategy for case 2

#### Riccardo Brasca (Sep 30 2022 at 13:11):

In lemma 4.4 `x`

and `y`

are real, right?

#### Riccardo Brasca (Sep 30 2022 at 13:11):

Well, maybe even integers

#### Riccardo Brasca (Sep 30 2022 at 13:11):

But in any case fixed under complex conjugation

#### Chris Birkbeck (Sep 30 2022 at 13:12):

Yes they are integers.

#### Riccardo Brasca (Sep 30 2022 at 13:14):

Good, the proof seems quite Leanable

#### Chris Birkbeck (Sep 30 2022 at 13:15):

FYI the proof is from page 6 of Washington

#### Riccardo Brasca (Sep 30 2022 at 13:26):

May I suppose `i`

is a natural number or do you think we need it to be an integer?

#### Riccardo Brasca (Sep 30 2022 at 13:29):

Mmm, I need anyway to consider integer powers, so it doesn't matter

#### Riccardo Brasca (Sep 30 2022 at 13:46):

The statement of Lemma 4.4 looks quite ugly. Suggestions to improve it are welcome

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

#### Riccardo Brasca (Sep 30 2022 at 13:53):

Ah, we have `is_primitive_root.unit'`

, nice

#### Riccardo Brasca (Sep 30 2022 at 13:56):

```
lemma exists_int_sum_eq_zero (h : 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 -
(hζ.unit' ^ (2 * k - i) : (𝓞 K)ˣ) * y ∈ span ({p} : set (𝓞 K)) :=
```

I don't understand why I have to write `hζ.unit' ^ i : (𝓞 K)ˣ`

, but if I don't do it Lean uses the coercion to `𝓞 K`

before taking the power, and so it complains.

#### Riccardo Brasca (Sep 30 2022 at 16:54):

(deleted)

#### Riccardo Brasca (Oct 01 2022 at 11:43):

This is now proved. The proof is a little messy because of the coercions `(𝓞 K)ˣ → 𝓞 K → K`

, but that's life. It is also rather annoying since we don't have an updated version of mathlib. @Eric Rodriguez do you think it will be possible to update mathlib soon?

#### Eric Rodriguez (Oct 01 2022 at 11:48):

I mean I don't think we actually use the diamond fix

#### Eric Rodriguez (Oct 01 2022 at 11:48):

we can bump mathlib soon

#### Eric Rodriguez (Oct 01 2022 at 11:48):

hopefully the splitting_field diamodn stuff will come to main soon

#### Riccardo Brasca (Oct 01 2022 at 12:07):

So do you think we can just do the bump now?

#### Eric Rodriguez (Oct 01 2022 at 12:24):

yeah, if something breaks that isn't obviously fixable give me a ping and i'll try fix it asap, but i'm super busy this week

#### Riccardo Brasca (Oct 01 2022 at 12:24):

OK, I am doing it

#### Riccardo Brasca (Oct 01 2022 at 13:18):

It's done.

#### Riccardo Brasca (Oct 03 2022 at 12:54):

I am modifying the file `flt_regular`

to use `a b c : ℤ`

. It think it is much better, and probably even needed in cerain proofs.

#### Riccardo Brasca (Oct 03 2022 at 23:14):

I've a proof of the following:

```
def caseI_slightly_easier : Prop := ∀ ⦃a b c : ℤ⦄ ⦃p : ℕ⦄ (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
def caseI : Prop := ∀ ⦃a b c : ℤ⦄ ⦃p : ℕ⦄ (hpri : p.prime) (hreg : is_regular_number p hpri.pos)
(hodd : p ≠ 2) (hprod : a * b * c ≠ 0) (caseI : ¬ ↑p ∣ a * b * c), a ^ p + b ^ p ≠ c ^ p
lemma may_assume : caseI_slightly_easier → caseI :=
```

#### Riccardo Brasca (Oct 03 2022 at 23:15):

@Chris Birkbeck can you please check this is the statement of Lemma 4.5 in the blueprint?

#### Riccardo Brasca (Oct 03 2022 at 23:16):

(there are various "we may assume" that are not very precise)

#### Riccardo Brasca (Oct 03 2022 at 23:24):

If this is correct, we are ready to prove caseI. I mean, to attack the last proof. (There is still a prerequisite to prove, the the ideals are coprime, but I prefer to wait to see if the statement is correct).

#### Riccardo Brasca (Oct 03 2022 at 23:25):

I have to sleep now, but tomorrow I will clean some stuff, making more clear what we have to do.

#### Chris Birkbeck (Oct 04 2022 at 08:33):

Yep that looks good. I assume ` (hgcd : is_unit (({a, b, c} : finset ℤ).gcd id))`

says that they are pairwise coprime? i.e. doing `gcd`

on a `finset`

just does the pairwise gcds?

#### Chris Birkbeck (Oct 04 2022 at 08:34):

I guess technically lemma 4.5 doesnt need the regularity assumption, but if we want to use it for `may_assume`

then we probably want it there (?)

#### Riccardo Brasca (Oct 04 2022 at 08:38):

`(({a, b, c} : finset ℤ).gcd id))`

is the gcd of `a`

, `b`

and `c`

. I don't think we have `is_coprime`

for `finset`

. The API for `finset.gcd`

is rather small, I think we will have to add stuff, but the definition should be the correct one.

#### Chris Birkbeck (Oct 04 2022 at 08:45):

Ah ok I see. That's fine then.

#### Riccardo Brasca (Oct 04 2022 at 08:50):

It's surprisingly painful to work with the `gcd`

of a finset. I think because docs#finset.gcd_eq_gcd_image works for `ℕ`

but not for `ℤ`

(and to be honest I don't even understand if it is true or not).

#### Yaël Dillies (Oct 04 2022 at 08:53):

The general rule is that if it is true for the nullary and binary cases, it's true for the finitary case. Nullary case here is easy, so is it true for binary?

#### Riccardo Brasca (Oct 04 2022 at 08:59):

Since there is `is_idempotent α gcd_monoid.gcd`

(that is surely false in `ℤ`

) I guess it's not. It's likely that my mental model for `finset.fold`

is not good.

#### Chris Birkbeck (Oct 04 2022 at 09:02):

Yes I don't really understand what `finset.fold gcd_monoid.gcd 0 f s`

does in `finset.gcd`

.

#### Yaël Dillies (Oct 04 2022 at 09:04):

It does `gcd 0 (gcd (f a) (gcd (f b) ...)`

for `a, b, ...`

an arbitrary enumeration of `s`

.

#### Chris Birkbeck (Oct 04 2022 at 09:07):

Aha I see, thanks!

#### Riccardo Brasca (Oct 04 2022 at 09:13):

OK, this is `s.gcd f`

. And what is `(finset.image f s).gcd id`

?

#### Riccardo Brasca (Oct 04 2022 at 09:13):

I can be confused, but they look the same to me.

#### Chris Birkbeck (Oct 04 2022 at 09:14):

Riccardo Brasca said:

If this is correct, we are ready to prove caseI. I mean, to attack the last proof. (There is still a prerequisite to prove, the the ideals are coprime, but I prefer to wait to see if the statement is correct).

I want to play around with `flt_ideals_coprime`

to see if I can understand how the ideal API works. I'll also check the statement

#### Yaël Dillies (Oct 04 2022 at 09:14):

Oh that's quite different. It's `gcd 0 (gcd a (gcd b ...)`

for `a, b, ...`

an arbitrary enumeration of `s.image f`

. So in particular duplicates are lost.

#### Yaël Dillies (Oct 04 2022 at 09:16):

Hence the idempotency condition. If `gcd a a = a`

, then you can erase any duplicates and both things are the same.

#### Riccardo Brasca (Oct 04 2022 at 09:16):

Ah, it's because duplicate are lost!

#### Yaël Dillies (Oct 04 2022 at 09:18):

But I think that it's still true for `ℤ`

, because everything gets normalized to positive stuff

#### Riccardo Brasca (Oct 04 2022 at 09:18):

Still, I am wondering if this is true, since it *is* true that `gcd(0, gcd(a, a)) = gcd(0,a).`

#### Yaël Dillies (Oct 04 2022 at 09:19):

`gcd(0, gcd(a, a)) = gcd(0, a)`

you mean

#### Yaël Dillies (Oct 04 2022 at 09:19):

I don't have a good intuition for what `normalize`

does, but yes it's something that sounds reasonable to expect.

#### Riccardo Brasca (Oct 04 2022 at 09:20):

It's the absolute value

#### Yaël Dillies (Oct 04 2022 at 09:20):

In general monoids as well??

#### Riccardo Brasca (Oct 04 2022 at 09:20):

I mean, in `ℤ`

.

#### Yaël Dillies (Oct 04 2022 at 09:20):

Ah right

#### Yaël Dillies (Oct 04 2022 at 09:21):

You can definitely prove that `s.gcd f`

and `(finset.image f s).gcd id`

are associated. And then depending on the conditions properties of `normalize`

you can turn that into an actual equality.

#### Yaël Dillies (Oct 04 2022 at 09:21):

Surely if `a`

and `b`

are associated then `normalize a = normalize b`

?

#### Riccardo Brasca (Oct 04 2022 at 09:22):

In general is nonsense, it is just a convenient thing when we have a way to normalize. In practice it is the absolute value on `ℤ`

, the identity on `ℕ`

and divide by leading coefficient on `K[X]`

.

#### Riccardo Brasca (Oct 04 2022 at 09:23):

Yaël Dillies said:

Surely if

`a`

and`b`

are associated then`normalize a = normalize b`

?

No, it's the opposite. `a`

and `normalize a`

are associated. It picks a representative in any equivalence class for "being associated".

#### Yaël Dillies (Oct 04 2022 at 09:23):

Both statements can be true, right?

#### Yaël Dillies (Oct 04 2022 at 09:24):

I'm saying that you should always pick the same representative out of an equivalence class.

#### Yaël Dillies (Oct 04 2022 at 09:24):

"If two equivalence classes are the same then their representative is the same"

#### Riccardo Brasca (Oct 04 2022 at 09:24):

Oh sure, what I said is nonsense.

#### Riccardo Brasca (Oct 04 2022 at 09:25):

They're associated iff have the same normalization, sorry.

#### Yaël Dillies (Oct 04 2022 at 09:25):

If `associated a b → normalize a = normalize b`

is not currently true in the generality of `normalized_monoid`

, I would seriously consider adding it as an axiom. Otherwise you can't really say `normalize`

picks representatives.

#### Riccardo Brasca (Oct 04 2022 at 09:26):

To be honest I have no idea what the class formally is. In my mind there are just three examples, and I know what `normalize`

does in this cases.

#### Yaël Dillies (Oct 04 2022 at 09:26):

And in all three cases `associated a b → normalize a = normalize b`

is true, right?

#### Riccardo Brasca (Oct 04 2022 at 09:27):

Yes yes

#### Riccardo Brasca (Oct 04 2022 at 09:27):

We have docs#associated_normalize

#### Riccardo Brasca (Oct 04 2022 at 09:28):

So by transitivity what you say is true

#### Yaël Dillies (Oct 04 2022 at 09:28):

Ahah! docs#normalize_eq_normalize_iff

#### Yaël Dillies (Oct 04 2022 at 09:28):

Not sure why this doesn't use `associated`

, but we have it.

#### Yaël Dillies (Oct 04 2022 at 09:29):

Riccardo Brasca said:

We have docs#associated_normalize

I don't see how that's relevant. We know that `associated x y → associated (normalize x) (normalize y)`

but they could still be different.

#### Riccardo Brasca (Oct 04 2022 at 09:30):

Is this always the same as associated? Even in some cray non cancellative non commutative monoid?

#### Riccardo Brasca (Oct 04 2022 at 09:31):

Ahahahahah, that's again because for me it's obvious that if the normalizations are associated then the normalizations must be equal

#### Riccardo Brasca (Oct 04 2022 at 09:31):

But this is just in my head

#### Riccardo Brasca (Oct 04 2022 at 09:31):

It's a proof by terminology.

#### Yaël Dillies (Oct 04 2022 at 09:33):

Riccardo Brasca said:

Is this always the same as associated? Even in some cray non cancellative non commutative monoid?

This statement does not seem to exist but it's true by docs#associated.dvd_iff_dvd_left

#### Patrick Massot (Oct 04 2022 at 09:38):

Riccardo Brasca said:

It's a proof by terminology.

It reminds me I forgot to PR the proof that Xavier asked for yesterday. It was also a proof by terminology, he wanted to know that a complete topological field is completable.

#### Patrick Massot (Oct 04 2022 at 09:39):

```
instance completable_top_field_of_complete (L : Type*) [field L]
[uniform_space L] [topological_division_ring L] [separated_space L] [complete_space L] :
completable_top_field L :=
by terminology
```

#### Yaël Dillies (Oct 04 2022 at 09:45):

I will PR the generalisation you want, Riccardo.

#### Riccardo Brasca (Oct 04 2022 at 09:48):

Which one?

#### Yaël Dillies (Oct 04 2022 at 09:52):

Of docs#finset.gcd_eq_gcd_image

#### Riccardo Brasca (Oct 04 2022 at 09:53):

Thanks! If you want you can also add the result here, whose proof can (I think) be golfed with the generalization.

#### Yaël Dillies (Oct 04 2022 at 09:54):

Oh I don't think I have access to flt-regular yet.

#### Riccardo Brasca (Oct 04 2022 at 09:55):

I am not sure if we can generalize the statement, since we want a `division_thing`

to be able to write `/`

, but also a `normalized_gcd_thing`

, and we don't have a good typeclass for that. Again there are essentially three examples, and the result for `ℕ`

is there.

#### Riccardo Brasca (Oct 04 2022 at 09:55):

Yaël Dillies said:

Oh I don't think I have access to flt-regular yet.

I am giving you access, but you should at least be able to read the file.

#### Yaël Dillies (Oct 04 2022 at 09:55):

Maybe it's time to have a proper typeclass for that, yeah.

#### Yaël Dillies (Oct 04 2022 at 10:27):

@Riccardo Brasca, #16795

#### Yaël Dillies (Oct 04 2022 at 10:28):

And the lemmas I didn't even end up using

```
variables [cancel_comm_monoid_with_zero α] [normalization_monoid α] {a b : α}
@[simp] lemma normalize_eq_normalize_iff' : normalize a = normalize b ↔ associated a b :=
normalize_eq_normalize_iff.trans dvd_dvd_iff_associated
alias normalize_eq_normalize_iff' ↔ _ associated.normalize_eq
```

#### Riccardo Brasca (Oct 04 2022 at 15:03):

I've moved some stuff and updated the dependency graph. The main statement of caseI is `caseI_easier`

in `caseI.statement`

. All the prerequisites are formalized (at least the statements, there is only one missing proof, that the ideals are coprime), so we can start working on the last step.

#### Chris Birkbeck (Oct 04 2022 at 15:33):

Great! I've been thinking about the coprime ideal proof. I wondered if one could cheat at prove that the ideals are coprime directly, i.e by finding some `a,b`

such that $a(x+\zeta^iy) +b (x+\zeta^j y)=1$ but I dont know how hard that is (at least I couldnt find anyone doing it this way). We might just have to do the proof with ideal division/containment

#### Riccardo Brasca (Oct 04 2022 at 15:37):

There is now an isolated lemma in the graph (with a weird name). Can you have a look?

#### Chris Birkbeck (Oct 04 2022 at 15:38):

oh yes sorry thats mine. I'm not finished with it yet, one sec

#### Riccardo Brasca (Oct 04 2022 at 15:43):

Do you see any problem with the proof in the blueprint (for the coprimality)? We have that $(1-\zeta)$ is prime.

#### Chris Birkbeck (Oct 04 2022 at 15:44):

Oh no it should be fine. I just wondered if I could quickly see a "one line proof"

#### Eric Rodriguez (Oct 04 2022 at 15:49):

We'd actually need span of a singleton as a ring hom for that first, which I think is nice to have regardless

#### Chris Birkbeck (Oct 04 2022 at 15:50):

Sorry, I'm not sure what you mean by "span of a singleton as a ring hom "

#### Riccardo Brasca (Oct 04 2022 at 15:51):

The set of ideals is a semiring :D

#### Chris Birkbeck (Oct 04 2022 at 15:52):

oh ha I see :)

#### Riccardo Brasca (Oct 04 2022 at 15:53):

Do we really miss something or it is just a matter of writing the bundled hom?

#### Chris Birkbeck (Oct 04 2022 at 15:57):

Sorry, so you mean we'd need this for what I suggested? I was writing an equality of elements, not ideals (although that wasn't clear :P). Maybe I'm just confused

#### Riccardo Brasca (Oct 04 2022 at 16:13):

The equality $z^p = (x+y)(x+\zeta y)\cdots(x+\zeta^{p-1}y)$ is somewhere, right? I think @Alex J. Best worked on this.

#### Chris Birkbeck (Oct 04 2022 at 16:14):

yes its `pow_add_pow_eq_prod_add_zeta_runity_mul `

#### Riccardo Brasca (Oct 04 2022 at 16:15):

OK, we *really* need `span`

as a bundled hom.

#### Riccardo Brasca (Oct 04 2022 at 16:16):

Otherwise we will end up rewriting a lot of stupid proofs.

#### Riccardo Brasca (Oct 04 2022 at 16:20):

But we already have it! docs#submodule.span.ring_hom

#### Riccardo Brasca (Oct 04 2022 at 16:21):

Hmm, more or less

#### Kevin Buzzard (Oct 04 2022 at 16:27):

span of a singleton isn't a ring hom, span(a+b) isn't span(a)+span(b)=span(a,b)

#### Riccardo Brasca (Oct 04 2022 at 16:30):

Ah yes, as bundled `mul_hom`

then.

#### Michael Stoll (Oct 04 2022 at 16:34):

It is even a `monoid_hom`

.

#### Eric Rodriguez (Oct 04 2022 at 17:24):

oh, I wanted to use docs#is_coprime.map but that doesn't seem to apply

#### Eric Rodriguez (Oct 04 2022 at 17:24):

I guess we need that specific result then for `span`

#### Riccardo Brasca (Oct 05 2022 at 09:26):

I am going to work on the proof of caseI. Let's see how many things we are missing :D

#### Riccardo Brasca (Oct 05 2022 at 12:11):

First problem: the definition

```
def flt_ideals [fact ((p : ℕ).prime)] (x y i : ℤ) : ideal RR :=
ideal.span ({ x + y * ((zeta_runity p ℤ RR) ^ i : RRˣ) } : set RR)
```

uses `zeta`

. This is bad for two reasons:

- first of all we should
*always*use a generic primitive root of unity, we've already noticed this several times. - this is true (and important) even if we replace
`zeta`

by any`p`

-th root of unity, right? I mean, even for`1`

.

#### Riccardo Brasca (Oct 05 2022 at 12:12):

Hmm, it's not stated as I though, let me find a reasonable statement.

#### Riccardo Brasca (Oct 05 2022 at 12:25):

@Chris Birkbeck I am going to modify the statement of `flt_ideals_coprime`

as follows:

```
local notation `R` := 𝓞 (cyclotomic_field p ℚ)
def flt_ideals [fact ((p : ℕ).prime)] (x y : ℤ) {η : R}
(hη : η ∈ nth_roots_finset p R) : ideal R :=
ideal.span ({ x + y * η } : set R)
lemma flt_ideals_coprime [fact (p : ℕ).prime] (ph : 5 ≤ p) {x y : ℤ} {η₁ η₂ : R}
(hη₁ : η₁ ∈ nth_roots_finset p R) (hη₂ : η₂ ∈ nth_roots_finset p R) (hdiff : η₁ ≠ η₂)
(hp : is_coprime x y) : is_coprime (flt_ideals p x y hη₁) (flt_ideals p x y hη₂) :=
```

since this is what we get in working on caseI. Let me know if you see any problem with it.

#### Chris Birkbeck (Oct 05 2022 at 12:44):

I think to prove that lemma we probably need something like x,y not divisible by p or something, but I'll figure that out as I work out the proof. But that statement should be fine

#### Riccardo Brasca (Oct 05 2022 at 12:46):

In practice `x`

and `y`

will be `a`

and `b`

in

```
theorem caseI_easier {a b c : ℤ} {p : ℕ} (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)
```

So feel free to add any assumption already present in this lemma.

#### Chris Birkbeck (Oct 05 2022 at 12:46):

Yeah exactly, one of those assumptions is needed for the proof (at least for the proof we have in the blueprint)

#### Riccardo Brasca (Oct 05 2022 at 12:47):

I think it's a good idea to state them exactly as in `caseI_easier`

if possible (for example we have several way of saying `¬a ≡ b [ZMOD p]`

).

#### Riccardo Brasca (Oct 05 2022 at 13:01):

Wait, do you really need `is_coprime x y`

?

#### Riccardo Brasca (Oct 05 2022 at 13:01):

Or `¬ p ∣ x * y`

is enough?

#### Riccardo Brasca (Oct 05 2022 at 13:03):

Ah, it's needed, but it's easy to prove.

#### Chris Birkbeck (Oct 05 2022 at 13:11):

Riccardo Brasca said:

Wait, do you really need

`is_coprime x y`

?

No I think you really do need this and that $p \nmid x + y$ (at least thats what Washington uses)

#### Riccardo Brasca (Oct 05 2022 at 13:38):

Now I am confused. I am talking about the proof that the ideals are coprime. Can you try to write down a Lean statement?

#### Riccardo Brasca (Oct 05 2022 at 13:38):

In the statement in the blueprint there is no `z`

, but `z`

is in the proof, so we also need `x ^ p + y ^ p = z ^ p`

?

#### Chris Birkbeck (Oct 05 2022 at 13:43):

So in the proof you end up showing that if they werent coprime, then $x + y \equiv 0 \mod p$, which then implies that $x+y \equiv x^p + y^p \equiv z^p \equiv 0 \mod p$ and then you get your contradiction as $p \nmid z$ (under the assumptions of `caseI`

). So to prove the coprime lemma we just need to add the assumption $x + y \ne 0 \mod p$

#### Riccardo Brasca (Oct 05 2022 at 13:43):

Checking the proof what we need seems to be that `{x,y,z}`

are coprime, `x^p + y^p = z^p`

and `¬ p ∣ x*y*z`

, which in turn implies that `is_coprime x y`

and `¬ x + y ≡ 0 [ZMOD p]`

#### Chris Birkbeck (Oct 05 2022 at 13:45):

Riccardo Brasca said:

In the statement in the blueprint there is no

`z`

, but`z`

is in the proof, so we also need`x ^ p + y ^ p = z ^ p`

?

yes sorry, the proof in the blueprint is under the assumption that we are in `caseI`

#### Riccardo Brasca (Oct 05 2022 at 13:49):

I am sorry but we really need a Lean statement.

```
lemma flt_ideals_coprime [fact (p : ℕ).prime] (p5 : 5 ≤ p) {x y z : ℤ}
(H : x ^ (p : ℕ) + y ^ (p : ℕ) = z ^ (p : ℕ)) {η₁ η₂ : R} (hxy : is_coprime x y)
(hη₁ : η₁ ∈ nth_roots_finset p R) (hη₂ : η₂ ∈ nth_roots_finset p R) (hdiff : η₁ ≠ η₂)
(caseI : ¬ ↑p ∣ x * y * z) : is_coprime (flt_ideals p x y hη₁) (flt_ideals p x y hη₂) :=
```

is OK?

#### Chris Birkbeck (Oct 05 2022 at 13:49):

its my fault for being sloppy, when making the blueprint I cut up the proof into these lemmas and didn't pay enough attention to the exact assumptions for each lemma, as in my head we were always in `caseI`

.

#### Riccardo Brasca (Oct 05 2022 at 13:49):

we have caseI with the assumption that `x`

and `y`

are coprime.

#### Riccardo Brasca (Oct 05 2022 at 13:50):

Don't worry, this is way we are writing things in Lean!

#### Chris Birkbeck (Oct 05 2022 at 13:50):

```
lemma flt_ideals_coprime2 [fact (p : ℕ).prime] (ph : 5 ≤ p) {x y : ℤ} {η₁ η₂ : R}
(hη₁ : η₁ ∈ nth_roots_finset p R) (hη₂ : η₂ ∈ nth_roots_finset p R) (hdiff : η₁ ≠ η₂)
(hp : is_coprime x y) (hp2 : ¬ x + y ≡ 0 [ZMOD p]) :
is_coprime (flt_ideals p x y hη₁) (flt_ideals p x y hη₂) :=
```

#### Chris Birkbeck (Oct 05 2022 at 13:51):

this is enough and all the assumptions follow from the ones in `caseI`

#### Riccardo Brasca (Oct 05 2022 at 13:52):

`hp2`

can be removed, right? I know we have all of them, but I am trying to state a reasonable result.

#### Chris Birkbeck (Oct 05 2022 at 13:54):

hmm no, I think that if we don't want to mention `z`

in the coprime lemma then we need `hp2`

. Or are you saying this follows from the other hypothesis in the lemma?

#### Riccardo Brasca (Oct 05 2022 at 13:57):

Sorry, I misread.

#### Riccardo Brasca (Oct 05 2022 at 13:58):

Let's keep this one.

```
lemma flt_ideals_coprime [fact (p : ℕ).prime] (p5 : 5 ≤ p) {x y z : ℤ}
(H : x ^ (p : ℕ) + y ^ (p : ℕ) = z ^ (p : ℕ)) {η₁ η₂ : R} (hxy : is_coprime x y)
(hη₁ : η₁ ∈ nth_roots_finset p R) (hη₂ : η₂ ∈ nth_roots_finset p R) (hdiff : η₁ ≠ η₂)
(caseI : ¬ ↑p ∣ x * y * z) : is_coprime (flt_ideals p x y hη₁) (flt_ideals p x y hη₂)
```

#### Chris Birkbeck (Oct 05 2022 at 13:59):

Sure, that also works :)

#### Riccardo Brasca (Oct 05 2022 at 13:59):

It's easy enough to apply, and proving ` ¬ x + y ≡ 0 [ZMOD p]`

should be trivial.

#### Chris Birkbeck (Oct 05 2022 at 13:59):

wait..the one you sent doesnt have that?

#### Chris Birkbeck (Oct 05 2022 at 14:00):

oh sorry, I see what you mean

#### Chris Birkbeck (Oct 05 2022 at 14:00):

yes thats easy enough

#### Chris Birkbeck (Oct 05 2022 at 14:34):

where is the fact that $1- \zeta$ is prime?

#### Chris Birkbeck (Oct 05 2022 at 14:35):

on nvm found it its in `zeta_sub_one_prime`

:p

#### Riccardo Brasca (Oct 05 2022 at 14:38):

The current statement is

```
lemma flt_ideals_coprime [fact (p : ℕ).prime] (p5 : 5 ≤ p) {x y z : ℤ}
(H : x ^ (p : ℕ) + y ^ (p : ℕ) = z ^ (p : ℕ)) {η₁ η₂ : R} (hxy : is_coprime x y)
(hη₁ : η₁ ∈ nth_roots_finset p R) (hη₂ : η₂ ∈ nth_roots_finset p R) (hdiff : η₁ ≠ η₂)
(caseI : ¬ ↑p ∣ x * y * z) : is_coprime (flt_ideals p x y hη₁) (flt_ideals p x y hη₂) :=
```

`¬ x + y ≡ 0 [ZMOD p]`

follows because if `p`

divides `x+y`

then it divides `z`

and so the product, and there is `caseI`

.

#### Riccardo Brasca (Oct 05 2022 at 14:39):

we will need a mini-lemma for this, but it should be trivial

#### Chris Birkbeck (Oct 05 2022 at 14:40):

I'm currently working on the proof of this. But I'm pretty slow, so someone might beat me to it.

#### Riccardo Brasca (Oct 05 2022 at 14:47):

I've added a (very slow, I will try to improve it) proof of

```
theorem exist_ideal {a b c : ℤ} (h5p : 5 ≤ p)
(H : a ^ p + b ^ p = c ^ p)
(hgcd : is_unit (({a, b, c} : finset ℤ).gcd id))
(caseI : ¬ ↑p ∣ a * b * c) :
∀ i ∈ nth_roots_finset p R, ∃ I, span ({a + i * b} : set R) = I ^ p
```

is `caseI.statement`

. This is the only place (I think) where we need `flt_ideals_coprime`

. If you modify the statement make sure this one still compiles.

#### Chris Birkbeck (Oct 05 2022 at 14:48):

sure thing!

#### Riccardo Brasca (Oct 05 2022 at 15:38):

Don't hesitate to create a lot of small sorried lemma and to push them. This will surely speed up the job

#### Chris Birkbeck (Oct 05 2022 at 18:04):

yeah well I've added lots of sorries to a proof of the version I was working on and which gives the version we want (up to a trivial sorry I've not yet filled in). I wont be able to look at this until friday, but I think it should be doable without too much pain.

#### Riccardo Brasca (Oct 05 2022 at 18:33):

Nice !

#### Riccardo Brasca (Oct 05 2022 at 18:34):

It's reasonable to finish this proof in October I think

#### Riccardo Brasca (Oct 06 2022 at 10:22):

`git blame`

says that @Eric Rodriguez is to blame for

```
instance : is_principal_ideal_ring (𝓞 L) := sorry
```

:rolling_on_the_floor_laughing:

#### Riccardo Brasca (Oct 06 2022 at 10:23):

wait, there is even a proof!

#### Riccardo Brasca (Oct 06 2022 at 10:26):

Let me remove it, hopefully it wasn't used.

#### Riccardo Brasca (Oct 06 2022 at 10:26):

OK, maybe it was true with some assumption on `L`

(currently `L`

is any number field...) and then this assumption was removed, so in practice now we have a false instance around

#### Eric Rodriguez (Oct 06 2022 at 10:26):

That is for L an 2nd cyclotomic extension :)

#### Eric Rodriguez (Oct 06 2022 at 10:27):

(aka Q)

#### Riccardo Brasca (Oct 06 2022 at 10:30):

But `[is_cyclotomic_extension {2} K L]`

wasn't included, since there is no `K`

in the statement... so this instance really simplified the proof that the relevant ideal is principal.

#### Eric Rodriguez (Oct 06 2022 at 10:32):

Oops...

#### Riccardo Brasca (Oct 06 2022 at 14:54):

We now have

```
theorem is_principal {a b c : ℤ} {ζ : R} (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) (H : a ^ p + b ^ p = c ^ p) (hζ : is_primitive_root ζ p) :
∃ (u : Rˣ) (α : R), ↑u * (α ^ p) = ↑a + ζ * ↑b :=
```

that depends on only one sorry (I hope), that the ideals are coprime. This is a very good news, since this is the crucial step where we use regularity of `p`

. The rest should be quite elementary, even if the sentence "checking each case leads to a contradiction" may be annoying.

#### Chris Birkbeck (Oct 06 2022 at 18:49):

Awesome! I'll try to do some more on the coprime ideal lemma tomorrow

#### Chris Birkbeck (Oct 10 2022 at 12:33):

Do we have something like this somewhere?

```
lemma zeta_sub_one_dvb_p [fact (p : ℕ).prime] (ph : 5 ≤ p) {η : R} (hη : η ∈ nth_roots_finset p R)
(hne1 : η ≠ 1): (1 - η) ∣ (p : R) :=
```

Here `R = 𝓞 (cyclotomic_field p ℚ)`

.

#### Riccardo Brasca (Oct 10 2022 at 13:37):

It should be easy. We know the norm of `1 - ζ`

, and we know that the norm is the product of conjugates

#### Riccardo Brasca (Oct 10 2022 at 13:38):

But I have the impression of having already proved it

#### Eric Rodriguez (Oct 10 2022 at 13:38):

I think it's proved for the case of primitive roots, but the proof should be easy to generalise

#### Chris Birkbeck (Oct 10 2022 at 13:39):

Hmm yeah I was looking at that. The problem is that its stated for fields not the rings of integers. I was worried it would be annoying to go from field elements to ring elements

#### Michael Stoll (Oct 10 2022 at 13:39):

Evaluate $(X^p - 1)/(X - 1)$ at $1$?

#### Riccardo Brasca (Oct 10 2022 at 13:39):

you have to use `norm'`

#### Chris Birkbeck (Oct 10 2022 at 13:40):

Riccardo Brasca said:

you have to use

`norm'`

Oh I hadn't seen `norm'`

let me have a look

#### Riccardo Brasca (Oct 10 2022 at 13:41):

It the norm defined on the ring of integers, taking values in `ℤ`

#### Riccardo Brasca (Oct 10 2022 at 13:42):

```
lemma dvd_norm [is_galois K L] : x ∣ algebra_map (𝓞 K) (𝓞 L) (norm' K x)
```

is what you want

#### Chris Birkbeck (Oct 10 2022 at 13:43):

yep thats what I want.

#### Riccardo Brasca (Oct 10 2022 at 13:43):

With docs#is_primitive_root.sub_one_norm_prime_ne_two

#### Riccardo Brasca (Oct 10 2022 at 13:44):

I mean, it's already there

#### Chris Birkbeck (Oct 10 2022 at 13:44):

what `dvd_norm`

is already there?

#### Riccardo Brasca (Oct 10 2022 at 13:44):

yes

#### Riccardo Brasca (Oct 10 2022 at 13:45):

in `src/norm/norm_of_units.lean`

#### Chris Birkbeck (Oct 10 2022 at 13:45):

oh great, thanks!

#### Riccardo Brasca (Oct 10 2022 at 13:46):

It was part of the proof that `1 -ζ`

is prime avoiding defining the norm of an ideal

#### Riccardo Brasca (Oct 10 2022 at 20:15):

@Chris Birkbeck your `prim_coe `

can be proved as

```
lemma prim_coe (ζ : R) (hζ : is_primitive_root ζ p) :
is_primitive_root (ζ : (cyclotomic_field p ℚ)) p :=
coe_submonoid_class_iff.mpr hζ
```

I've pushed this proof (and removed a linter error). I think we can just replace it by its proof, but that's up to you.

#### Riccardo Brasca (Oct 10 2022 at 20:16):

(BTW I really like lemmas stated using the new classes for morphisms!)

#### Chris Birkbeck (Oct 10 2022 at 20:17):

Oh great, I knew that had to be somewhere! I just put it there cuz I thought I'd maybe need it again, but the proof is so short I don't think I'll need to have it separate

#### Chris Birkbeck (Oct 10 2022 at 20:18):

I'm not sure I know what these new classes for morphisms are?

#### Riccardo Brasca (Oct 10 2022 at 20:44):

See section 6.3 in https://arxiv.org/pdf/2202.01629.pdf

#### Riccardo Brasca (Oct 12 2022 at 16:38):

The three edge cases are done (I mean I proved they're impossibile). The main case will be slightly more difficult, but I don't expect any bad surprise.

#### Riccardo Brasca (Sep 07 2022 at 08:18):

We should be ready to think about a strategy to attack case I.

Looking at the blueprint, the first sorried result is

```
lemma flt_fact_2 {p : ℕ} [fact (p : ℕ).prime] (ph : 5 ≤ p) {x y z : ℤ} {i j : ℤ} (h : i ≠ j)
(hp : is_coprime x y) (h : x ^ p + y ^ p = z ^ p) : flt_ideals n x y i + flt_ideals n x y j = ⊤ :=
```

is anyone working/interested in working on this?

#### Riccardo Brasca (Sep 07 2022 at 08:37):

(note that I am renaming it to `flt_ideals_coprime`

.)

#### Eric Rodriguez (Sep 07 2022 at 14:05):

I think the definition of `flt_ideals`

was not yet too sure. I'm not sure how much time I'll have in the near future, but I'm trying to get the splitting field diamond merged in the background

#### Riccardo Brasca (Sep 07 2022 at 14:08):

This is already very nice! Can you link the PRs here?

#### Alex J. Best (Sep 07 2022 at 14:12):

I'm happy to have a go at this, maybe on the weekend, I've written some similarish proofs recently so hopefully it'll be ok (famous last words)

#### Eric Rodriguez (Sep 07 2022 at 14:15):

The current one holding stuff up is Anne's #16123, #16132 also by Anne continues this theme ~~but I'm not super sure whether it;'s necessary for the proof~~ and is necessary for the fix. When these are merged, I'll be able to PR the diamond fix properly

#### Riccardo Brasca (Sep 07 2022 at 14:27):

The definition of `flt_ideals`

looks reasonable to me. Maybe there is no need to use `zeta_runity`

, and `zeta`

is enough.

#### Riccardo Brasca (Sep 07 2022 at 14:27):

We can generalize it to the ring of integers of any cyclotomic extension of `ℚ`

, but I don't thinks it is necessary.

#### Riccardo Brasca (Sep 09 2022 at 15:15):

Also, we are missing the statement of Lemma 4.4 (that is called `exists_int_sum_eq_zero`

in the tex file, I suggest to keep the same name in Lean) and Lemma 4.5 (called `may_assume_coprime`

). Then all the statements leading to case I will be formalized.

#### Riccardo Brasca (Sep 09 2022 at 15:15):

I will do this next week if nobody does it during the weekend.

#### Riccardo Brasca (Sep 28 2022 at 08:19):

@Chris Birkbeck Am I right in saying that in lemma 4.3 of the blueprint we need to assume that $a_i = 0$ for some $i$? Otherwise I don't understand the proof...

#### Riccardo Brasca (Sep 28 2022 at 08:27):

I am actually even more confused: you write $\alpha = a_0 + a_1 \zeta + \cdots + a_{p-1}\zeta^{p-1}$, but we can always suppose that $a_{p-1} = 0$, since the other already form a basis. Let me think a little bit.

#### Riccardo Brasca (Sep 28 2022 at 08:28):

Oh, you mean that you take *any* way of writing $\alpha$ in that way, the $a_i$'s are not coordinates.

#### Riccardo Brasca (Sep 28 2022 at 08:29):

So I need to change the Lean statement.

#### Riccardo Brasca (Sep 28 2022 at 08:33):

In any case the assumption $a_i = 0$ for some $i$ seems necessary (and Washington has it).

#### Riccardo Brasca (Sep 30 2022 at 12:12):

The proof is now formalized.

#### Chris Birkbeck (Sep 30 2022 at 12:15):

Oh amazing!

#### Riccardo Brasca (Sep 30 2022 at 12:16):

Interestingly enough, I had to modify the proof written in the blueprint. The sentence "any subset of $\{1,\zeta, \ldots, \zeta^{p-1}\}$ with $p-1$ elements is a $\mathbb{Z}$-basis of the ring of integers" is the typical thing that it is a nightmare to formalize.

#### Chris Birkbeck (Sep 30 2022 at 12:18):

Yeah, I'm sorry, maybe I sloppy there

#### Riccardo Brasca (Sep 30 2022 at 12:23):

It's mathematically OK (Washington does the same), it's just that "basis" is a strange concept. Anyway, do you confirm we can assume $a_i=0$ for some $i$?

#### Riccardo Brasca (Sep 30 2022 at 12:29):

Also, `p > 3`

is not needed.

#### Chris Birkbeck (Sep 30 2022 at 12:32):

Yes I think thats fine. Also it should say "any subset of p-2 elements" in the blueprint, thats a typo

#### Chris Birkbeck (Sep 30 2022 at 12:33):

Riccardo Brasca said:

Also,

`p > 3`

is not needed.

oh yes nice, I think I just added it since we had it for the final goal

#### Riccardo Brasca (Sep 30 2022 at 12:38):

My next step is to (state and) prove Lemma 4.4 and Lemma 4.5. I think it is better to wait before proving Lemma 4.1, since the statement may need to be modified, and so it's probably a good idea to use it to prove Case I.

#### Chris Birkbeck (Sep 30 2022 at 13:07):

That sounds good. I have time for this next week so I can try and help do one of these lemmas. I might also try and think about a strategy for case 2

#### Riccardo Brasca (Sep 30 2022 at 13:11):

In lemma 4.4 `x`

and `y`

are real, right?

#### Riccardo Brasca (Sep 30 2022 at 13:11):

Well, maybe even integers

#### Riccardo Brasca (Sep 30 2022 at 13:11):

But in any case fixed under complex conjugation

#### Chris Birkbeck (Sep 30 2022 at 13:12):

Yes they are integers.

#### Riccardo Brasca (Sep 30 2022 at 13:14):

Good, the proof seems quite Leanable

#### Chris Birkbeck (Sep 30 2022 at 13:15):

FYI the proof is from page 6 of Washington

#### Riccardo Brasca (Sep 30 2022 at 13:26):

May I suppose `i`

is a natural number or do you think we need it to be an integer?

#### Riccardo Brasca (Sep 30 2022 at 13:29):

Mmm, I need anyway to consider integer powers, so it doesn't matter

#### Riccardo Brasca (Sep 30 2022 at 13:46):

The statement of Lemma 4.4 looks quite ugly. Suggestions to improve it are welcome

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

#### Riccardo Brasca (Sep 30 2022 at 13:53):

Ah, we have `is_primitive_root.unit'`

, nice

#### Riccardo Brasca (Sep 30 2022 at 13:56):

```
lemma exists_int_sum_eq_zero (h : 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 -
(hζ.unit' ^ (2 * k - i) : (𝓞 K)ˣ) * y ∈ span ({p} : set (𝓞 K)) :=
```

I don't understand why I have to write `hζ.unit' ^ i : (𝓞 K)ˣ`

, but if I don't do it Lean uses the coercion to `𝓞 K`

before taking the power, and so it complains.

#### Riccardo Brasca (Sep 30 2022 at 16:54):

(deleted)

#### Riccardo Brasca (Oct 01 2022 at 11:43):

This is now proved. The proof is a little messy because of the coercions `(𝓞 K)ˣ → 𝓞 K → K`

, but that's life. It is also rather annoying since we don't have an updated version of mathlib. @Eric Rodriguez do you think it will be possible to update mathlib soon?

#### Eric Rodriguez (Oct 01 2022 at 11:48):

I mean I don't think we actually use the diamond fix

#### Eric Rodriguez (Oct 01 2022 at 11:48):

we can bump mathlib soon

#### Eric Rodriguez (Oct 01 2022 at 11:48):

hopefully the splitting_field diamodn stuff will come to main soon

#### Riccardo Brasca (Oct 01 2022 at 12:07):

So do you think we can just do the bump now?

#### Eric Rodriguez (Oct 01 2022 at 12:24):

yeah, if something breaks that isn't obviously fixable give me a ping and i'll try fix it asap, but i'm super busy this week

#### Riccardo Brasca (Oct 01 2022 at 12:24):

OK, I am doing it

#### Riccardo Brasca (Oct 01 2022 at 13:18):

It's done.

#### Riccardo Brasca (Oct 03 2022 at 12:54):

I am modifying the file `flt_regular`

to use `a b c : ℤ`

. It think it is much better, and probably even needed in cerain proofs.

#### Riccardo Brasca (Oct 03 2022 at 23:14):

I've a proof of the following:

```
def caseI_slightly_easier : Prop := ∀ ⦃a b c : ℤ⦄ ⦃p : ℕ⦄ (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
def caseI : Prop := ∀ ⦃a b c : ℤ⦄ ⦃p : ℕ⦄ (hpri : p.prime) (hreg : is_regular_number p hpri.pos)
(hodd : p ≠ 2) (hprod : a * b * c ≠ 0) (caseI : ¬ ↑p ∣ a * b * c), a ^ p + b ^ p ≠ c ^ p
lemma may_assume : caseI_slightly_easier → caseI :=
```

#### Riccardo Brasca (Oct 03 2022 at 23:15):

@Chris Birkbeck can you please check this is the statement of Lemma 4.5 in the blueprint?

#### Riccardo Brasca (Oct 03 2022 at 23:16):

(there are various "we may assume" that are not very precise)

#### Riccardo Brasca (Oct 03 2022 at 23:24):

If this is correct, we are ready to prove caseI. I mean, to attack the last proof. (There is still a prerequisite to prove, the the ideals are coprime, but I prefer to wait to see if the statement is correct).

#### Riccardo Brasca (Oct 03 2022 at 23:25):

I have to sleep now, but tomorrow I will clean some stuff, making more clear what we have to do.

#### Chris Birkbeck (Oct 04 2022 at 08:33):

Yep that looks good. I assume ` (hgcd : is_unit (({a, b, c} : finset ℤ).gcd id))`

says that they are pairwise coprime? i.e. doing `gcd`

on a `finset`

just does the pairwise gcds?

#### Chris Birkbeck (Oct 04 2022 at 08:34):

I guess technically lemma 4.5 doesnt need the regularity assumption, but if we want to use it for `may_assume`

then we probably want it there (?)

#### Riccardo Brasca (Oct 04 2022 at 08:38):

`(({a, b, c} : finset ℤ).gcd id))`

is the gcd of `a`

, `b`

and `c`

. I don't think we have `is_coprime`

for `finset`

. The API for `finset.gcd`

is rather small, I think we will have to add stuff, but the definition should be the correct one.

#### Chris Birkbeck (Oct 04 2022 at 08:45):

Ah ok I see. That's fine then.

#### Riccardo Brasca (Oct 04 2022 at 08:50):

It's surprisingly painful to work with the `gcd`

of a finset. I think because docs#finset.gcd_eq_gcd_image works for `ℕ`

but not for `ℤ`

(and to be honest I don't even understand if it is true or not).

#### Yaël Dillies (Oct 04 2022 at 08:53):

The general rule is that if it is true for the nullary and binary cases, it's true for the finitary case. Nullary case here is easy, so is it true for binary?

#### Riccardo Brasca (Oct 04 2022 at 08:59):

Since there is `is_idempotent α gcd_monoid.gcd`

(that is surely false in `ℤ`

) I guess it's not. It's likely that my mental model for `finset.fold`

is not good.

#### Chris Birkbeck (Oct 04 2022 at 09:02):

Yes I don't really understand what `finset.fold gcd_monoid.gcd 0 f s`

does in `finset.gcd`

.

#### Yaël Dillies (Oct 04 2022 at 09:04):

It does `gcd 0 (gcd (f a) (gcd (f b) ...)`

for `a, b, ...`

an arbitrary enumeration of `s`

.

#### Chris Birkbeck (Oct 04 2022 at 09:07):

Aha I see, thanks!

#### Riccardo Brasca (Oct 04 2022 at 09:13):

OK, this is `s.gcd f`

. And what is `(finset.image f s).gcd id`

?

#### Riccardo Brasca (Oct 04 2022 at 09:13):

I can be confused, but they look the same to me.

#### Chris Birkbeck (Oct 04 2022 at 09:14):

Riccardo Brasca said:

I want to play around with `flt_ideals_coprime`

to see if I can understand how the ideal API works. I'll also check the statement

#### Yaël Dillies (Oct 04 2022 at 09:14):

Oh that's quite different. It's `gcd 0 (gcd a (gcd b ...)`

for `a, b, ...`

an arbitrary enumeration of `s.image f`

. So in particular duplicates are lost.

#### Yaël Dillies (Oct 04 2022 at 09:16):

Hence the idempotency condition. If `gcd a a = a`

, then you can erase any duplicates and both things are the same.

#### Riccardo Brasca (Oct 04 2022 at 09:16):

Ah, it's because duplicate are lost!

#### Yaël Dillies (Oct 04 2022 at 09:18):

But I think that it's still true for `ℤ`

, because everything gets normalized to positive stuff

#### Riccardo Brasca (Oct 04 2022 at 09:18):

Still, I am wondering if this is true, since it *is* true that `gcd(0, gcd(a, a)) = gcd(0,a).`

#### Yaël Dillies (Oct 04 2022 at 09:19):

`gcd(0, gcd(a, a)) = gcd(0, a)`

you mean

#### Yaël Dillies (Oct 04 2022 at 09:19):

I don't have a good intuition for what `normalize`

does, but yes it's something that sounds reasonable to expect.

#### Riccardo Brasca (Oct 04 2022 at 09:20):

It's the absolute value

#### Yaël Dillies (Oct 04 2022 at 09:20):

In general monoids as well??

#### Riccardo Brasca (Oct 04 2022 at 09:20):

I mean, in `ℤ`

.

#### Yaël Dillies (Oct 04 2022 at 09:20):

Ah right

#### Yaël Dillies (Oct 04 2022 at 09:21):

You can definitely prove that `s.gcd f`

and `(finset.image f s).gcd id`

are associated. And then depending on the conditions properties of `normalize`

you can turn that into an actual equality.

#### Yaël Dillies (Oct 04 2022 at 09:21):

Surely if `a`

and `b`

are associated then `normalize a = normalize b`

?

#### Riccardo Brasca (Oct 04 2022 at 09:22):

In general is nonsense, it is just a convenient thing when we have a way to normalize. In practice it is the absolute value on `ℤ`

, the identity on `ℕ`

and divide by leading coefficient on `K[X]`

.

#### Riccardo Brasca (Oct 04 2022 at 09:23):

Yaël Dillies said:

Surely if

`a`

and`b`

are associated then`normalize a = normalize b`

?

No, it's the opposite. `a`

and `normalize a`

are associated. It picks a representative in any equivalence class for "being associated".

#### Yaël Dillies (Oct 04 2022 at 09:23):

Both statements can be true, right?

#### Yaël Dillies (Oct 04 2022 at 09:24):

I'm saying that you should always pick the same representative out of an equivalence class.

#### Yaël Dillies (Oct 04 2022 at 09:24):

"If two equivalence classes are the same then their representative is the same"

#### Riccardo Brasca (Oct 04 2022 at 09:24):

Oh sure, what I said is nonsense.

#### Riccardo Brasca (Oct 04 2022 at 09:25):

They're associated iff have the same normalization, sorry.

#### Yaël Dillies (Oct 04 2022 at 09:25):

If `associated a b → normalize a = normalize b`

is not currently true in the generality of `normalized_monoid`

, I would seriously consider adding it as an axiom. Otherwise you can't really say `normalize`

picks representatives.

#### Riccardo Brasca (Oct 04 2022 at 09:26):

To be honest I have no idea what the class formally is. In my mind there are just three examples, and I know what `normalize`

does in this cases.

#### Yaël Dillies (Oct 04 2022 at 09:26):

And in all three cases `associated a b → normalize a = normalize b`

is true, right?

#### Riccardo Brasca (Oct 04 2022 at 09:27):

Yes yes

#### Riccardo Brasca (Oct 04 2022 at 09:27):

We have docs#associated_normalize

#### Riccardo Brasca (Oct 04 2022 at 09:28):

So by transitivity what you say is true

#### Yaël Dillies (Oct 04 2022 at 09:28):

Ahah! docs#normalize_eq_normalize_iff

#### Yaël Dillies (Oct 04 2022 at 09:28):

Not sure why this doesn't use `associated`

, but we have it.

#### Yaël Dillies (Oct 04 2022 at 09:29):

Riccardo Brasca said:

We have docs#associated_normalize

I don't see how that's relevant. We know that `associated x y → associated (normalize x) (normalize y)`

but they could still be different.

#### Riccardo Brasca (Oct 04 2022 at 09:30):

Is this always the same as associated? Even in some cray non cancellative non commutative monoid?

#### Riccardo Brasca (Oct 04 2022 at 09:31):

Ahahahahah, that's again because for me it's obvious that if the normalizations are associated then the normalizations must be equal

#### Riccardo Brasca (Oct 04 2022 at 09:31):

But this is just in my head

#### Riccardo Brasca (Oct 04 2022 at 09:31):

It's a proof by terminology.

#### Yaël Dillies (Oct 04 2022 at 09:33):

Riccardo Brasca said:

Is this always the same as associated? Even in some cray non cancellative non commutative monoid?

This statement does not seem to exist but it's true by docs#associated.dvd_iff_dvd_left

#### Patrick Massot (Oct 04 2022 at 09:38):

Riccardo Brasca said:

It's a proof by terminology.

It reminds me I forgot to PR the proof that Xavier asked for yesterday. It was also a proof by terminology, he wanted to know that a complete topological field is completable.

#### Patrick Massot (Oct 04 2022 at 09:39):

```
instance completable_top_field_of_complete (L : Type*) [field L]
[uniform_space L] [topological_division_ring L] [separated_space L] [complete_space L] :
completable_top_field L :=
by terminology
```

#### Yaël Dillies (Oct 04 2022 at 09:45):

I will PR the generalisation you want, Riccardo.

#### Riccardo Brasca (Oct 04 2022 at 09:48):

Which one?

#### Yaël Dillies (Oct 04 2022 at 09:52):

Of docs#finset.gcd_eq_gcd_image

#### Riccardo Brasca (Oct 04 2022 at 09:53):

Thanks! If you want you can also add the result here, whose proof can (I think) be golfed with the generalization.

#### Yaël Dillies (Oct 04 2022 at 09:54):

Oh I don't think I have access to flt-regular yet.

#### Riccardo Brasca (Oct 04 2022 at 09:55):

I am not sure if we can generalize the statement, since we want a `division_thing`

to be able to write `/`

, but also a `normalized_gcd_thing`

, and we don't have a good typeclass for that. Again there are essentially three examples, and the result for `ℕ`

is there.

#### Riccardo Brasca (Oct 04 2022 at 09:55):

Yaël Dillies said:

Oh I don't think I have access to flt-regular yet.

I am giving you access, but you should at least be able to read the file.

#### Yaël Dillies (Oct 04 2022 at 09:55):

Maybe it's time to have a proper typeclass for that, yeah.

#### Yaël Dillies (Oct 04 2022 at 10:27):

@Riccardo Brasca, #16795

#### Yaël Dillies (Oct 04 2022 at 10:28):

And the lemmas I didn't even end up using

```
variables [cancel_comm_monoid_with_zero α] [normalization_monoid α] {a b : α}
@[simp] lemma normalize_eq_normalize_iff' : normalize a = normalize b ↔ associated a b :=
normalize_eq_normalize_iff.trans dvd_dvd_iff_associated
alias normalize_eq_normalize_iff' ↔ _ associated.normalize_eq
```

#### Riccardo Brasca (Oct 04 2022 at 15:03):

I've moved some stuff and updated the dependency graph. The main statement of caseI is `caseI_easier`

in `caseI.statement`

. All the prerequisites are formalized (at least the statements, there is only one missing proof, that the ideals are coprime), so we can start working on the last step.

#### Chris Birkbeck (Oct 04 2022 at 15:33):

Great! I've been thinking about the coprime ideal proof. I wondered if one could cheat at prove that the ideals are coprime directly, i.e by finding some `a,b`

such that $a(x+\zeta^iy) +b (x+\zeta^j y)=1$ but I dont know how hard that is (at least I couldnt find anyone doing it this way). We might just have to do the proof with ideal division/containment

#### Riccardo Brasca (Oct 04 2022 at 15:37):

There is now an isolated lemma in the graph (with a weird name). Can you have a look?

#### Chris Birkbeck (Oct 04 2022 at 15:38):

oh yes sorry thats mine. I'm not finished with it yet, one sec

#### Riccardo Brasca (Oct 04 2022 at 15:43):

Do you see any problem with the proof in the blueprint (for the coprimality)? We have that $(1-\zeta)$ is prime.

#### Chris Birkbeck (Oct 04 2022 at 15:44):

Oh no it should be fine. I just wondered if I could quickly see a "one line proof"

#### Eric Rodriguez (Oct 04 2022 at 15:49):

We'd actually need span of a singleton as a ring hom for that first, which I think is nice to have regardless

#### Chris Birkbeck (Oct 04 2022 at 15:50):

Sorry, I'm not sure what you mean by "span of a singleton as a ring hom "

#### Riccardo Brasca (Oct 04 2022 at 15:51):

The set of ideals is a semiring :D

#### Chris Birkbeck (Oct 04 2022 at 15:52):

oh ha I see :)

#### Riccardo Brasca (Oct 04 2022 at 15:53):

Do we really miss something or it is just a matter of writing the bundled hom?

#### Chris Birkbeck (Oct 04 2022 at 15:57):

Sorry, so you mean we'd need this for what I suggested? I was writing an equality of elements, not ideals (although that wasn't clear :P). Maybe I'm just confused

#### Riccardo Brasca (Oct 04 2022 at 16:13):

The equality $z^p = (x+y)(x+\zeta y)\cdots(x+\zeta^{p-1}y)$ is somewhere, right? I think @Alex J. Best worked on this.

#### Chris Birkbeck (Oct 04 2022 at 16:14):

yes its `pow_add_pow_eq_prod_add_zeta_runity_mul `

#### Riccardo Brasca (Oct 04 2022 at 16:15):

OK, we *really* need `span`

as a bundled hom.

#### Riccardo Brasca (Oct 04 2022 at 16:16):

Otherwise we will end up rewriting a lot of stupid proofs.

#### Riccardo Brasca (Oct 04 2022 at 16:20):

But we already have it! docs#submodule.span.ring_hom

#### Riccardo Brasca (Oct 04 2022 at 16:21):

Hmm, more or less

#### Kevin Buzzard (Oct 04 2022 at 16:27):

span of a singleton isn't a ring hom, span(a+b) isn't span(a)+span(b)=span(a,b)

#### Riccardo Brasca (Oct 04 2022 at 16:30):

Ah yes, as bundled `mul_hom`

then.

#### Michael Stoll (Oct 04 2022 at 16:34):

It is even a `monoid_hom`

.

#### Eric Rodriguez (Oct 04 2022 at 17:24):

oh, I wanted to use docs#is_coprime.map but that doesn't seem to apply

#### Eric Rodriguez (Oct 04 2022 at 17:24):

I guess we need that specific result then for `span`

#### Riccardo Brasca (Oct 05 2022 at 09:26):

I am going to work on the proof of caseI. Let's see how many things we are missing :D

#### Riccardo Brasca (Oct 05 2022 at 12:11):

First problem: the definition

```
def flt_ideals [fact ((p : ℕ).prime)] (x y i : ℤ) : ideal RR :=
ideal.span ({ x + y * ((zeta_runity p ℤ RR) ^ i : RRˣ) } : set RR)
```

uses `zeta`

. This is bad for two reasons:

- first of all we should
*always*use a generic primitive root of unity, we've already noticed this several times. - this is true (and important) even if we replace
`zeta`

by any`p`

-th root of unity, right? I mean, even for`1`

.

#### Riccardo Brasca (Oct 05 2022 at 12:12):

Hmm, it's not stated as I though, let me find a reasonable statement.

#### Riccardo Brasca (Oct 05 2022 at 12:25):

@Chris Birkbeck I am going to modify the statement of `flt_ideals_coprime`

as follows:

```
local notation `R` := 𝓞 (cyclotomic_field p ℚ)
def flt_ideals [fact ((p : ℕ).prime)] (x y : ℤ) {η : R}
(hη : η ∈ nth_roots_finset p R) : ideal R :=
ideal.span ({ x + η * y } : set R)
lemma flt_ideals_coprime [fact (p : ℕ).prime] (ph : 5 ≤ p) {x y : ℤ} {η₁ η₂ : R}
(hη₁ : η₁ ∈ nth_roots_finset p R) (hη₂ : η₂ ∈ nth_roots_finset p R) (hdiff : η₁ ≠ η₂)
(hp : is_coprime x y) : is_coprime (flt_ideals p x y hη₁) (flt_ideals p x y hη₂) :=
```

since this is what we get in working on caseI. Let me know if you see any problem with it.

#### Chris Birkbeck (Oct 05 2022 at 12:44):

I think to prove that lemma we probably need something like x,y not divisible by p or something, but I'll figure that out as I work out the proof. But that statement should be fine

#### Riccardo Brasca (Oct 05 2022 at 12:46):

In practice `x`

and `y`

will be `a`

and `b`

in

```
theorem caseI_easier {a b c : ℤ} {p : ℕ} (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)
```

So feel free to add any assumption already present in this lemma.

#### Chris Birkbeck (Oct 05 2022 at 12:46):

Yeah exactly, one of those assumptions is needed for the proof (at least for the proof we have in the blueprint)

#### Riccardo Brasca (Oct 05 2022 at 12:47):

I think it's a good idea to state them exactly as in `caseI_easier`

if possible (for example we have several way of saying `¬a ≡ b [ZMOD p]`

).

#### Riccardo Brasca (Oct 05 2022 at 13:01):

Wait, do you really need `is_coprime x y`

?

#### Riccardo Brasca (Oct 05 2022 at 13:01):

Or `¬ p ∣ x * y`

is enough?

#### Riccardo Brasca (Oct 05 2022 at 13:03):

Ah, it's needed, but it's easy to prove.

#### Chris Birkbeck (Oct 05 2022 at 13:11):

Riccardo Brasca said:

Wait, do you really need

`is_coprime x y`

?

No I think you really do need this and that $p \nmid x + y$ (at least thats what Washington uses)

#### Riccardo Brasca (Oct 05 2022 at 13:38):

Now I am confused. I am talking about the proof that the ideals are coprime. Can you try to write down a Lean statement?

#### Riccardo Brasca (Oct 05 2022 at 13:38):

In the statement in the blueprint there is no `z`

, but `z`

is in the proof, so we also need `x ^ p + y ^ p = z ^ p`

?

#### Chris Birkbeck (Oct 05 2022 at 13:43):

So in the proof you end up showing that if they werent coprime, then $x + y \equiv 0 \mod p$, which then implies that $x+y \equiv x^p + y^p \equiv z^p \equiv 0 \mod p$ and then you get your contradiction as $p \nmid z$ (under the assumptions of `caseI`

). So to prove the coprime lemma we just need to add the assumption $x + y \ne 0 \mod p$

#### Riccardo Brasca (Oct 05 2022 at 13:43):

Checking the proof what we need seems to be that `{x,y,z}`

are coprime, `x^p + y^p = z^p`

and `¬ p ∣ x*y*z`

, which in turn implies that `is_coprime x y`

and `¬ x + y ≡ 0 [ZMOD p]`

#### Chris Birkbeck (Oct 05 2022 at 13:45):

Riccardo Brasca said:

`z`

, but`z`

is in the proof, so we also need`x ^ p + y ^ p = z ^ p`

?

yes sorry, the proof in the blueprint is under the assumption that we are in `caseI`

#### Riccardo Brasca (Oct 05 2022 at 13:49):

I am sorry but we really need a Lean statement.

```
lemma flt_ideals_coprime [fact (p : ℕ).prime] (p5 : 5 ≤ p) {x y z : ℤ}
(H : x ^ (p : ℕ) + y ^ (p : ℕ) = z ^ (p : ℕ)) {η₁ η₂ : R} (hxy : is_coprime x y)
(hη₁ : η₁ ∈ nth_roots_finset p R) (hη₂ : η₂ ∈ nth_roots_finset p R) (hdiff : η₁ ≠ η₂)
(caseI : ¬ ↑p ∣ x * y * z) : is_coprime (flt_ideals p x y hη₁) (flt_ideals p x y hη₂) :=
```

is OK?

#### Chris Birkbeck (Oct 05 2022 at 13:49):

its my fault for being sloppy, when making the blueprint I cut up the proof into these lemmas and didn't pay enough attention to the exact assumptions for each lemma, as in my head we were always in `caseI`

.

#### Riccardo Brasca (Oct 05 2022 at 13:49):

we have caseI with the assumption that `x`

and `y`

are coprime.

#### Riccardo Brasca (Oct 05 2022 at 13:50):

Don't worry, this is way we are writing things in Lean!

#### Chris Birkbeck (Oct 05 2022 at 13:50):

```
lemma flt_ideals_coprime2 [fact (p : ℕ).prime] (ph : 5 ≤ p) {x y : ℤ} {η₁ η₂ : R}
(hη₁ : η₁ ∈ nth_roots_finset p R) (hη₂ : η₂ ∈ nth_roots_finset p R) (hdiff : η₁ ≠ η₂)
(hp : is_coprime x y) (hp2 : ¬ x + y ≡ 0 [ZMOD p]) :
is_coprime (flt_ideals p x y hη₁) (flt_ideals p x y hη₂) :=
```

#### Chris Birkbeck (Oct 05 2022 at 13:51):

this is enough and all the assumptions follow from the ones in `caseI`

#### Riccardo Brasca (Oct 05 2022 at 13:52):

`hp2`

can be removed, right? I know we have all of them, but I am trying to state a reasonable result.

#### Chris Birkbeck (Oct 05 2022 at 13:54):

hmm no, I think that if we don't want to mention `z`

in the coprime lemma then we need `hp2`

. Or are you saying this follows from the other hypothesis in the lemma?

#### Riccardo Brasca (Oct 05 2022 at 13:57):

Sorry, I misread.

#### Riccardo Brasca (Oct 05 2022 at 13:58):

Let's keep this one.

```
lemma flt_ideals_coprime [fact (p : ℕ).prime] (p5 : 5 ≤ p) {x y z : ℤ}
(H : x ^ (p : ℕ) + y ^ (p : ℕ) = z ^ (p : ℕ)) {η₁ η₂ : R} (hxy : is_coprime x y)
(hη₁ : η₁ ∈ nth_roots_finset p R) (hη₂ : η₂ ∈ nth_roots_finset p R) (hdiff : η₁ ≠ η₂)
(caseI : ¬ ↑p ∣ x * y * z) : is_coprime (flt_ideals p x y hη₁) (flt_ideals p x y hη₂)
```

#### Chris Birkbeck (Oct 05 2022 at 13:59):

Sure, that also works :)

#### Riccardo Brasca (Oct 05 2022 at 13:59):

It's easy enough to apply, and proving ` ¬ x + y ≡ 0 [ZMOD p]`

should be trivial.

#### Chris Birkbeck (Oct 05 2022 at 13:59):

wait..the one you sent doesnt have that?

#### Chris Birkbeck (Oct 05 2022 at 14:00):

oh sorry, I see what you mean

#### Chris Birkbeck (Oct 05 2022 at 14:00):

yes thats easy enough

#### Chris Birkbeck (Oct 05 2022 at 14:34):

where is the fact that $1- \zeta$ is prime?

#### Chris Birkbeck (Oct 05 2022 at 14:35):

on nvm found it its in `zeta_sub_one_prime`

:p

#### Riccardo Brasca (Oct 05 2022 at 14:38):

The current statement is

```
lemma flt_ideals_coprime [fact (p : ℕ).prime] (p5 : 5 ≤ p) {x y z : ℤ}
(H : x ^ (p : ℕ) + y ^ (p : ℕ) = z ^ (p : ℕ)) {η₁ η₂ : R} (hxy : is_coprime x y)
(hη₁ : η₁ ∈ nth_roots_finset p R) (hη₂ : η₂ ∈ nth_roots_finset p R) (hdiff : η₁ ≠ η₂)
(caseI : ¬ ↑p ∣ x * y * z) : is_coprime (flt_ideals p x y hη₁) (flt_ideals p x y hη₂) :=
```

`¬ x + y ≡ 0 [ZMOD p]`

follows because if `p`

divides `x+y`

then it divides `z`

and so the product, and there is `caseI`

.

#### Riccardo Brasca (Oct 05 2022 at 14:39):

we will need a mini-lemma for this, but it should be trivial

#### Chris Birkbeck (Oct 05 2022 at 14:40):

I'm currently working on the proof of this. But I'm pretty slow, so someone might beat me to it.

#### Riccardo Brasca (Oct 05 2022 at 14:47):

I've added a (very slow, I will try to improve it) proof of

```
theorem exist_ideal {a b c : ℤ} (h5p : 5 ≤ p)
(H : a ^ p + b ^ p = c ^ p)
(hgcd : is_unit (({a, b, c} : finset ℤ).gcd id))
(caseI : ¬ ↑p ∣ a * b * c) :
∀ i ∈ nth_roots_finset p R, ∃ I, span ({a + i * b} : set R) = I ^ p
```

is `caseI.statement`

. This is the only place (I think) where we need `flt_ideals_coprime`

. If you modify the statement make sure this one still compiles.

#### Chris Birkbeck (Oct 05 2022 at 14:48):

sure thing!

#### Riccardo Brasca (Oct 05 2022 at 15:38):

Don't hesitate to create a lot of small sorried lemma and to push them. This will surely speed up the job

#### Chris Birkbeck (Oct 05 2022 at 18:04):

yeah well I've added lots of sorries to a proof of the version I was working on and which gives the version we want (up to a trivial sorry I've not yet filled in). I wont be able to look at this until friday, but I think it should be doable without too much pain.

#### Riccardo Brasca (Oct 05 2022 at 18:33):

Nice !

#### Riccardo Brasca (Oct 05 2022 at 18:34):

It's reasonable to finish this proof in October I think

#### Riccardo Brasca (Oct 06 2022 at 10:22):

`git blame`

says that @Eric Rodriguez is to blame for

```
instance : is_principal_ideal_ring (𝓞 L) := sorry
```

:rolling_on_the_floor_laughing:

#### Riccardo Brasca (Oct 06 2022 at 10:23):

wait, there is even a proof!

#### Riccardo Brasca (Oct 06 2022 at 10:26):

Let me remove it, hopefully it wasn't used.

#### Riccardo Brasca (Oct 06 2022 at 10:26):

OK, maybe it was true with some assumption on `L`

(currently `L`

is any number field...) and then this assumption was removed, so in practice now we have a false instance around

#### Eric Rodriguez (Oct 06 2022 at 10:26):

That is for L an 2nd cyclotomic extension :)

#### Eric Rodriguez (Oct 06 2022 at 10:27):

(aka Q)

#### Riccardo Brasca (Oct 06 2022 at 10:30):

But `[is_cyclotomic_extension {2} K L]`

wasn't included, since there is no `K`

in the statement... so this instance really simplified the proof that the relevant ideal is principal.

#### Eric Rodriguez (Oct 06 2022 at 10:32):

Oops...

#### Riccardo Brasca (Oct 06 2022 at 14:54):

We now have

```
theorem is_principal {a b c : ℤ} {ζ : R} (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) (H : a ^ p + b ^ p = c ^ p) (hζ : is_primitive_root ζ p) :
∃ (u : Rˣ) (α : R), ↑u * (α ^ p) = ↑a + ζ * ↑b :=
```

that depends on only one sorry (I hope), that the ideals are coprime. This is a very good news, since this is the crucial step where we use regularity of `p`

. The rest should be quite elementary, even if the sentence "checking each case leads to a contradiction" may be annoying.

#### Chris Birkbeck (Oct 06 2022 at 18:49):

Awesome! I'll try to do some more on the coprime ideal lemma tomorrow

#### Chris Birkbeck (Oct 10 2022 at 12:33):

Do we have something like this somewhere?

```
lemma zeta_sub_one_dvb_p [fact (p : ℕ).prime] (ph : 5 ≤ p) {η : R} (hη : η ∈ nth_roots_finset p R)
(hne1 : η ≠ 1): (1 - η) ∣ (p : R) :=
```

Here `R = 𝓞 (cyclotomic_field p ℚ)`

.

#### Riccardo Brasca (Oct 10 2022 at 13:37):

It should be easy. We know the norm of `1 - ζ`

, and we know that the norm is the product of conjugates

#### Riccardo Brasca (Oct 10 2022 at 13:38):

But I have the impression of having already proved it

#### Eric Rodriguez (Oct 10 2022 at 13:38):

I think it's proved for the case of primitive roots, but the proof should be easy to generalise

#### Chris Birkbeck (Oct 10 2022 at 13:39):

Hmm yeah I was looking at that. The problem is that its stated for fields not the rings of integers. I was worried it would be annoying to go from field elements to ring elements

#### Michael Stoll (Oct 10 2022 at 13:39):

Evaluate $(X^p - 1)/(X - 1)$ at $1$?

#### Riccardo Brasca (Oct 10 2022 at 13:39):

you have to use `norm'`

#### Chris Birkbeck (Oct 10 2022 at 13:40):

Riccardo Brasca said:

you have to use

`norm'`

Oh I hadn't seen `norm'`

let me have a look

#### Riccardo Brasca (Oct 10 2022 at 13:41):

It the norm defined on the ring of integers, taking values in `ℤ`

#### Riccardo Brasca (Oct 10 2022 at 13:42):

```
lemma dvd_norm [is_galois K L] : x ∣ algebra_map (𝓞 K) (𝓞 L) (norm' K x)
```

is what you want

#### Chris Birkbeck (Oct 10 2022 at 13:43):

yep thats what I want.

#### Riccardo Brasca (Oct 10 2022 at 13:43):

With docs#is_primitive_root.sub_one_norm_prime_ne_two

#### Riccardo Brasca (Oct 10 2022 at 13:44):

I mean, it's already there

#### Chris Birkbeck (Oct 10 2022 at 13:44):

what `dvd_norm`

is already there?

#### Riccardo Brasca (Oct 10 2022 at 13:44):

yes

#### Riccardo Brasca (Oct 10 2022 at 13:45):

in `src/norm/norm_of_units.lean`

#### Chris Birkbeck (Oct 10 2022 at 13:45):

oh great, thanks!

#### Riccardo Brasca (Oct 10 2022 at 13:46):

It was part of the proof that `1 -ζ`

is prime avoiding defining the norm of an ideal

#### Riccardo Brasca (Oct 10 2022 at 20:15):

@Chris Birkbeck your `prim_coe `

can be proved as

```
lemma prim_coe (ζ : R) (hζ : is_primitive_root ζ p) :
is_primitive_root (ζ : (cyclotomic_field p ℚ)) p :=
coe_submonoid_class_iff.mpr hζ
```

I've pushed this proof (and removed a linter error). I think we can just replace it by its proof, but that's up to you.

#### Riccardo Brasca (Oct 10 2022 at 20:16):

(BTW I really like lemmas stated using the new classes for morphisms!)

#### Chris Birkbeck (Oct 10 2022 at 20:17):

Oh great, I knew that had to be somewhere! I just put it there cuz I thought I'd maybe need it again, but the proof is so short I don't think I'll need to have it separate

#### Chris Birkbeck (Oct 10 2022 at 20:18):

I'm not sure I know what these new classes for morphisms are?

#### Riccardo Brasca (Oct 10 2022 at 20:44):

See section 6.3 in https://arxiv.org/pdf/2202.01629.pdf

#### Riccardo Brasca (Oct 12 2022 at 16:38):

The three edge cases are done (I mean I proved they're impossibile). The main case will be slightly more difficult, but I don't expect any bad surprise.

Last updated: Dec 20 2023 at 11:08 UTC