Outstanding Tasks, V5: Frobenius elements

Stream: FLT

[Kevin Buzzard]

As of today I am employed to work on FLT and not much else, so things are going to be much more active from now on, at least at my end. Like Tao I'm going to try switching to github issues to make part of this job easier. All issues relevant to this thread start with FROBENIUS. You can take a look at them here.

I'm going to run things in terms of "projects", small chunks of the proof which are ready to be worked on. And today's project is getting a proof of Bourbaki Comm Alg Chapter V, Section 2, no. 2, Theorem 2(ii) formalised. This is an abstract statement in algebra which implies the existence of Frobenius elements (and much more). You can read the mathematical argument (still not quite complete) here although that link does not look particularly stable to me. In the blueprint it's "8 A project: Frobenius elements".

If you want to work on an issue then claim it to avoid duplication. The official way to claim an issue is assign it to yourself on github. I will attempt to update the post below to keep track but please look on github before working on anything. I will link to issues individually below.

The easiest way of summarising what needs doing is: look at FrobeniusRiou and fill in the sorries. More precisely:

1) DONE issue If $b\in B$ and $F_b\in B[X]$ is $\prod_g(X-gb)$ then the degre of $F$ is $|G|$. Done by @Ruben Van de Velde

2) DONE issue. $F_b$ descends to $A[X]$ and so does the property of being monic of degree $|G|$. Done by @Ruben Van de Velde

3) issue. $M_b$ descends to $\overline{M}_b\in (A/P)[X]$ and again we need to prove that it's monic of degree $|G|$ and has $b$ as a root.

4) issue. A lemma I seem to need: if $S/R$ is an integral extension and $S$ is an integral domain then any nonzero element of $S$ divides (the image of) some nonzero element of $R$. This is some straightforward-on-paper algebra explained in the issue and for all I know it's already in mathlib (I couldn't find it though). This is Algebra.exists_dvd_nonzero_if_isIntegral in the Lean file.

5) issue. If $\lambda\in L$ then we need the definition of a polynomial $f_\lambda\in K[X]$ which is monic of degree $|G|$, has $\lambda$ as a root, and splits completely in $L$. If $\lambda\in B/Q$ then this is just $\overline{M}_\lambda$ but more generally one has to write $\lambda=n/d$ with $d\in A/P$ (see previous issue) and then scale $\overline{M}_n$ by an appropriate factor of $d$.

6) issue L/K is normal. Follows from the previous issue.

7) issue The maximal separable subextension of L/K is finite of degree at most |G|. Again this follows from the existence of $f_\lambda$ above, plus the theorem and finite and separable implies simple.

I'll add more later; this doesn't cover all of the sorries in the file, but it's a place to start!

[Ruben Van de Velde]

I'm guessing it's fine to assume [NoZeroDivisors B] for 1?

[Ruben Van de Velde]

(FLT#149)

[Patrick Massot]

Kevin Buzzard said:

here although that link does not look particularly stable to me. In the blueprint it's "8 A project: Frobenius elements".

I think you should be able to get a nicer link by putting a \label at the beginning of your section.

[Kevin Buzzard]

Ruben Van de Velde said:

I'm guessing it's fine to assume [NoZeroDivisors B] for 1?

I'm not sure it is -- why do we need it? Product of monics is monic in general.

The beauty of the result is that there are no hypotheses on $B$ whatsoever.

[Yaël Dillies]

But X^2 - 1 has four roots in $\mathbb Z / 8$

[Kevin Buzzard]

But it's still monic of degree 2 with -1 as a root, which is the only sort of thing that we need. The claim is that the product of $n$ things of the form $(X-t)$ is monic of degree $n$ assuming only that $B$ is nontrivial (which is implied by the existence of a prime ideal, something we assume in the statement of the main theorem)

[Ruben Van de Velde]

No, Kevin is right, will push a better proof in a moment

[Daniel Morrison]

I don't think I can assign issues to myself, apparently only those with write access can assign an issue. Should we comment on the issue to claim?

[Ruben Van de Velde]

Sounds like a good idea

[Kevin Buzzard]

oh I hadn't realised that! Thanks for letting me know!

[Notification Bot]

3 messages were moved from this topic to #FLT > Project Dashboard by Pietro Monticone.

[Ruben Van de Velde]

I pushed FLT#156, out now

[Daniel Morrison]

I did issue 4 in FLT#157

[Alex Brodbelt]

I will work on task 5) if that's ok :)

[Ahmad Alkhalawi]

I did issue 6 in FLT#160

[Kevin Buzzard]

Thanks! Travelling today so busy/ropey internet; may not get to these until tomorrow but thanks a lot!

[Kevin Buzzard]

Over the weekend I'll finish writing a completely new project in case people are now bored of this one.

[Ruben Van de Velde]

Not sure about bored, but all the issues in this thread are fixed or claimed :)

[Kevin Buzzard]

It's been a funny week. I had hoped that this would be the first week when I'd really start working on FLT properly but somehow I managed to book five talks in it :-/

[Ruben Van de Velde]

How many for next week? :innocent:

[Kevin Buzzard]

I now have three very light weeks (usually I'm spending October teaching 300 1st years!) and then a trip to the US.

[Thomas Browning]

Just wanted to record a few thoughts regarding this Frobenius elements business (which I've been working on since I need them for a different project of mine).
1) For part a, there's a slightly more direct proof that avoids polynomials and integrality (e.g., here: https://math.stackexchange.com/questions/1845110).
2) The clearing denominators trick (Corollary 8.15 in the blueprint) only requires algebraic, not integral.
3) I think there's also a slightly more direct proof of part b that avoids dealing with the maximal separable extension. The idea is that we already have docs#FixedPoints.toAlgHom_bijective which tells you that H=Stab Q surjects onto Aut(L/L^H). But we want to show that H surjects onto Aut(L/K). So we just need to show that any f in Aut(L/K) actually fixes L^H pointwise. So suppose that you have an element b of L^H. We just need to show f b = b. The clearing denominators trick lets us assume that b is in (B / Q)^H. Then the CRT result (Theorem 8.24 in the blueprint) lets you pick a lift whose characteristic polynomial mod Q is just (X - b)^|H| * X^(|G|-|H|). But the characteristic polynomial has coefficients in A, so b must be fixed by f. (In essence, this is basically showing that L^H/K is purely inseparable by hand).

I've formalized everything except for the CRT result here: https://github.com/leanprover-community/mathlib4/compare/tb_eq (sorry, it's a bit messy, but roughly follows the same framework as the FLT file, and copies some of the code). I was hoping to get this wrapped up over the weekend before Kevin starts issuing new tasks, but that probably won't happen at this rate, so I thought I'd give everyone a heads up to avoid duplication of effort. Feel free to move anything to the FLT project.

[Kevin Buzzard]

I was going to start an entirely new project today rather than interfering with this one. Ultimately the location of the proofs should definitely be mathlib rather than the FLT repo, this seems to be an important result (and the fact that you independently need it reinforces this).

[Ruben Van de Velde]

Can you add copyright and make a pr? I'm happy to help get it ready for review

[Thomas Browning]

Well, it's not really ready for review yet, since the CRT result is still sorried (and also the code is a mess). But feel free to push to the branch or leave review comments.

[Thomas Browning]

#17717

[Thomas Browning]

It's now sorry-free. I'll work on cleaning it up and getting it ready for review over the next few days.

[Alex Brodbelt]

I'm a bit stuck on the task I claimed (5 - 8.16 in the blueprint) as I'm not familiar with this part of mathlib and cannot figure out for the life of me how to use
Algebra.exists_dvd_nonzero_if_isIntegral

I switched from using residueFieldExtensionPolynomial as I cannot use obtain or rcases in the definition of the polynomial.

I am learning a lot through this task (both maths and lean) and hope to learn some more, so if this task is not too pressing could I get some help on how to finish it off ?? :sweat_smile:

Also I'm not sure if this is still relevant given Thomas' PR(?)

Thanks (:

theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
    ∃ r : R, r ≠ 0 ∧ s ∣ (r : S) := by
  sorry

variable (L : Type*) [Field L] [Algebra (B ⧸ Q) L] [IsFractionRing (B ⧸ Q) L]
  -- Now top left triangle: A / P → B / Q → L commutes
  [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L]
  -- now introduce K
  (K : Type*) [Field K] [Algebra (A ⧸ P) K] [IsFractionRing (A ⧸ P) K]
  -- now make bottom triangle commute
  [Algebra K L] [IsScalarTower (A ⧸ P) K L]
  -- So now both squares commute.

-- do I need this?
--  [Algebra A K] [IsScalarTower A (A ⧸ P) K]

-- Do I need this:
--  [Algebra B L] [IsScalarTower B (B ⧸ Q) L]

variable [Nontrivial B]

noncomputable local instance : Algebra (A ⧸ P)[X] K[X] :=
  RingHom.toAlgebra (Polynomial.mapRingHom (Algebra.toRingHom))

noncomputable local instance : Algebra (A ⧸ P) (B ⧸ Q) :=  RingHom.toAlgebra RingHom.smulOneHom

variable (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) in
variable (bbar : B ⧸ Q) in
theorem f_exists [DecidableEq L] [Nontrivial K] (l : L) [IsFractionRing (B ⧸ Q) L]
  [IsFractionRing (A ⧸ P) K] [Algebra (A ⧸ P) (B ⧸ Q)] [Algebra (A ⧸ P) K]
  (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) (bbar : B ⧸ Q) : -- added in nontrivial assumption
    ∃ f : K[X], f.Monic ∧ f.degree = Nat.card G ∧
    eval₂ (algebraMap K L) l f = 0 ∧ f.Splits (algebraMap K L) := by
  by_cases h : l = 0
  · use monomial (Nat.card G) 1
    refine ⟨?_, ?_, ?_, ?_⟩
    · rw [Monic, leadingCoeff, Polynomial.natDegree_monomial_eq, coeff_monomial_same]
      exact one_ne_zero
    · rw [Polynomial.degree_monomial]
      exact one_ne_zero
    · simp only [eval₂_monomial, map_one, one_mul, pow_eq_zero_iff', ne_eq, true_and, ← ne_eq]
      constructor
      apply h
      refine Nat.ne_zero_iff_zero_lt.mpr Nat.card_pos
    · rw [Polynomial.splits_iff_exists_multiset, map_monomial, map_one]
      simp_rw [leadingCoeff]; rw [Polynomial.natDegree_monomial_eq _ one_ne_zero, coeff_monomial_same]
      simp only [map_one, one_mul]
      use List.replicate (Nat.card G) (0:L)
      simp only [Multiset.map_coe, List.map_replicate, map_zero, sub_zero, Multiset.prod_coe,
        List.prod_replicate]
      rw [monomial_one_right_eq_X_pow]
  · have : ∃ β₁, ∃ β₂ ∈ nonZeroDivisors (B ⧸ Q),  algebraMap (B ⧸ Q) L β₁ / algebraMap (B ⧸ Q) L β₂ = l := by apply IsFractionRing.div_surjective
    obtain ⟨β₁, β₂, β₂_non_zero_divisor, hβ⟩ := this
    have hβ₂ : β₂ ≠ 0 := by exact nonZeroDivisors.ne_zero β₂_non_zero_divisor
    -- have : CommRing (A ⧸ P) := by exact Ideal.Quotient.commRing P
    -- have : CommRing (B ⧸ Q) := by exact Ideal.Quotient.commRing Q
    -- instantiate something to have the inclusion of A ⧸ P into B ⧸ Q
    -- algebraMap (A ⧸ P) (B ⧸ Q)
    have : ∃ α: A ⧸ P, α ≠ 0 ∧ (β₂ : B ⧸ Q) ∣ (algebraMap (A ⧸ P) (B ⧸ Q) α) := by apply Algebra.exists_dvd_nonzero_if_isIntegral --(R := (A ⧸ P)) (S := B ⧸ Q) (s := β₂) (hs := hβ₂)
    obtain ⟨α, hα, β₁_dvd_α⟩ := this
    -- let α_inv := IsFractionRing.inv α
    let f : (A ⧸ P)[X] := Mbar P hFull' (α • bbar) -- may have to depend on l rather than bbar?
    use algebraMap (A ⧸ P)[X] K[X] f
    refine ⟨?_, ?_, ?_, ?_⟩
    · sorry -- division of the leading term yields a monic
    · sorry -- deg( α^(-|G|) M ) = deg(M) and then use `Mbar_deg`
    · sorry -- I'm not sure yet how l relates to bbar
    · sorry -- unfold definition of Mbar and eventually use `Polynomial.splits_iff_exists_multiset`

[Andrew Yang]

I think this is covered in Thomas's PR, but I think it is still useful for yourself to do it once if you want to use this as a opportunity to learn Lean.
That said, I can't quite understand your question. Does the code you pasted fail? (I cannot check as this is not a #mwe) If so, what's the error message? If not, I think you have successfully applied the lemma in Lean? Is your question then a mathematical question of how to apply the lemma in the later steps of the proof?

[Alex Brodbelt]

Andrew Yang said:

I think this is covered in Thomas's PR, but I think it is still useful for yourself to do it once if you want to use this as a opportunity to learn Lean.
That said, I can't quite understand your question. Does the code you pasted fail? (I cannot check as this is not a #mwe) If so, what's the error message? If not, I think you have successfully applied the lemma in Lean? Is your question then a mathematical question of how to apply the lemma in the later steps of the proof?

Agh I figured it would not be an mwe... sorry about that - the error is the following:

tactic 'apply' failed, failed to unify
  ∃ r, r ≠ 0 ∧ ?s ∣ ↑r
with
  ∃ α, α ≠ 0 ∧ β₂ ∣ (algebraMap (A ⧸ P) (B ⧸ Q)) α

I tried manually coercing with α : (B ⧸ Q) got the following error message:

application type mismatch
  Algebra.exists_dvd_nonzero_if_isIntegral R (?m.1802422 R) β₂
argument
  β₂
has type
  B ⧸ Q : Type u_5
but is expected to have type
  ?m.1802422 R : Type

...so quotients lift to a different universe? I'm new to using quotients in lean so I'm not sure whats going on.

and then I tried with ↑α and got the following error:

application type mismatch
  Algebra.exists_dvd_nonzero_if_isIntegral R (?m.1802389 R) β₂
argument
  β₂
has type
  B ⧸ Q : Type u_5
but is expected to have type
  ?m.1802389 R : Type

Additionally, it fails to synthesize the quotient as a commutative ring, tried adding in a have statement with CommRing (A ⧸ P)

It's probably not easy to help me pin point what the problem is given I can't really provide a mwe, but if you have advice on what to learn or what to look out for I'd value that greatly (:

Thanks

[Andrew Yang]

Judging by the information you gave, my best guess would be to replace (R S : Type) with (R S : Type*) in Algebra.exists_dvd_nonzero_if_isIntegral.

Also, you should use let inst : CommRing _ := _ instead of have because have is for propositions, and giving a ring structure on a set contains data.

[Alex Brodbelt]

That makes sense - thank you

[Aaron Hill]

Are all of these tasks currently claimed?

[Daniel Morrison]

Yes, you can follow who has claimed what on the issues tab of the GitHub repository.

[Kevin Buzzard]

Right now I'm in the process of making some new outstanding tasks in a new mini-project about quaternion algebras. I had hoped that these would be up right now but I'm having problems finding the time to write the latex and also there are issues running the project because I made the decision to host it on imperial's GitHub and this has caused poor old Pietro all manner of problems

[Daniel Morrison]

Is writing latex something I can help with? I have too much extra time at the moment so I'm happy to help if possible.

[Daniel Morrison]

Alex Brodbelt said:

the error is the following:

tactic 'apply' failed, failed to unify
  ∃ r, r ≠ 0 ∧ ?s ∣ ↑r
with
  ∃ α, α ≠ 0 ∧ β₂ ∣ (algebraMap (A ⧸ P) (B ⧸ Q)) α

When I did Algebra.exists_dvd_nonzero_if_isIntegral I changed the coercion to (algebraMap R S) r because as you've seen Lean isn't great at using the coercion. If you update your work with the additions to the main repository, I was able to make it work with

have : ∃ α: A ⧸ P, α ≠ 0 ∧ (β₂ : B ⧸ Q) ∣ (algebraMap (A ⧸ P) (B ⧸ Q) α) := by
      apply Algebra.exists_dvd_nonzero_if_isIntegral (A ⧸ P) (B ⧸ Q) β₂ hβ₂
obtain ⟨α, hα, β₁_dvd_α⟩ := this

after adding the assumption [Algebra.IsIntegral (A ⧸ P) (B ⧸ Q)].

[Ruben Van de Velde]

Daniel Morrison said:

Is writing latex something I can help with? I have too much extra time at the moment so I'm happy to help if possible.

I think "writing latex" is a euphemism for "explaining the mathematics in simple enough terms that a Muppet like myself can translate it into lean"

[Daniel Morrison]

Haha I thought that might be the case

[Kevin Buzzard]

Yes. In contrast to the Carleson project which started with 150 pages of latex, I'm having to write everything on the fly

[Patrick Massot]

I think it is important to be precise here. The Carleson project did not start with 150 pages. The original preprint was around 30 pages long I think (@Floris van Doorn can probably tell us the exact number). Turning it into 150 pages was already a very important part of the Carleson project itself.

[Floris van Doorn]

When I joined the project there was a 64-page draft preprint with the generalized version of Carleson's theorem + some applications; the proof of Carleson's theorem was 37 pages. This was a draft, and still contained some notes of the form "todo: check" or "todo: clarify", but the written proof was essentially complete.

At first we actually tried to start the formalization with that document, and I already wrote a bunch of definitions from that document (you can look at some old history from the Carleson project).
The problem was that I had to ask questions about precise arguments all the time. One afternoon we spent an hour formalizing the sentence "By (1.4) we have <some equation>" and I had to ask multiple times what step to do next.

We (mostly Christoph Thiele) realized that this wasn't going to scale at all, and so the harmonic analysis group spent another few months writing out the proof in a lot more detail. Patrick is completely correct that writing the blueprint was a very important part of the Carleson project, and my "announcement" of the Carleson project was really an announcement of the formalizing part of the Carleson project. And by then I had also already spent half a year preparing the formalization (i.e. definitions, theorem statement, some proofs).

[Kevin Buzzard]

For me that 6 month preparation period is happening now. Two things that are not so obvious to outsiders is that (1) all the other noise in my life is now much more under control than it was (and I've started saying no to things) and (2) there are more people working on the project than is apparent. I've quickly realised that for masters and PhD students working on aspects of FLT there is no need to put their work into the blueprint mechanism and indeed this is a disadvantage in doing this, namely that other people will then disrupt their work which will make examining it far more complex. The medium term public plan is to define a Hecke algebra and prove things about it, and this is proceeding slightly more slowly than I'd like but for the most part this is because I'm still tying up loose ends which I'd hoped to get off my plate by September but which were severely disrupted by the new Zelda game coming out, which I've now 100%ed and thus lost interest in

[Chris Birkbeck]

Re: Hecke algebras. I have some WIP defining Hecke rings which should be useful for this. It's not too far from being done other than me finding time to finish it

[Ruben Van de Velde]

Re: your students, would it make sense to add those projects in the blueprint just as a single (or whatever) high level theorem with note "someone is working on this", just to have a clearer high level view?

[Terence Tao]

With the equational theories project I've learned that these projects can be decentralized to a far greater extent than with more conventional projects. For instance, I have almost zero involvement in "front end" projects like developing nice visualization tools for the equational implication graph, or "back end" projects like how to automatically manage computer generated submissions and how to represent the graph in Lean code or in exported files; but I also have not been significantly involved in some of the mathematical developments, such as the exploration of confluent theories. Perhaps there is some non-core portion of the FLT project which could conceivably be handled, not by a single masters or PhD student, but by a subgroup of the public collaboration who could not only perform the Lean formalization but also some of the blueprint writing and the overall direction of the subproject? In which case one would only need to lay out some broad description of the goals of the subproject and allow others to take it from there.