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):

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):

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):

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):

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):

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):

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):

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):

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

Ah ok I see. That's fine then.

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

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):

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):

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):

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):

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

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):

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):

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):

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 :=

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