Outstanding Tasks, V4

Stream: FLT

[Kevin Buzzard]

So I don't have time for FLT right now, because I have two big administrative tasks to deal with in July and I'm also doing a bunch of travelling. However I do have a clear idea about something we need, and this is Frobenius elements. When I was in Bonn I spent some time thinking about these and even made #14155 , but Joel Riou pointed out to me that we'd be better off working in greater generality, and pointed me to Théorème 2 in section 2 of chapter 5 of Bourbaki Alg Comm. Sorry I don't have the English version:

Screenshot-from-2024-07-06-21-45-15.png
Screenshot-from-2024-07-06-21-45-32.png
Screenshot-from-2024-07-06-21-45-47.png

Right now this is a major blocker for stating the existence of Galois representations attached to certain automorphic forms. This theorem should not be in the FLT repo, this is something which should go to mathlib directly. Some of the work in #14155 will be useful for the second part, but let's start with the first part.

Here's the claim in English. If $B$ is an $A$-algebra (all rings are commutative) and $G$ is a finite group acting by ring automorphisms on $B$ with invariants equal to (the image of) $A$, and if $B/A$ is integral, and if $P'$ and $Q'$ are two prime ideals of $B$ whose preimages in $A$ are equal, then amazingly, there's some $\sigma\in G$ such that $\sigma(P')=Q'$.

The proof uses the following lemmas.

Task 1) If $R$ is a commutative ring, if $\mathfrak{a}$ is a subset of $R$ closed under addition and multiplication (for example, an ideal), if $P_1$, $P_2$, \ldots, $P_n$ are a nonempty finite collection of ideals of $R$ and if all of them are prime apart from possibly two of them (!), and if $\mathfrak{a}$ is a subset of the union of the $P_i$, then $\mathfrak{a}$ is in fact contained in one of the $P_i$.

This is Bourbaki Alg Comm chapter 2 section 1 Prop 2, and it's also the last exercise in Chapter 1 of Matsumura IIRC (Matsumura assumes $P_3$, $P_4$, \ldots, $P_n$ are prime and I remember when I was a grad student initially assuming that this 3 was a typo). In the application all of the $P_i$ are prime and I'm not sure I've ever seen an application when the $P_i$ aren't all prime, perhaps the thing to do is to prove the result the way Matsumura states it and then deduce it for a general finite set of ideals all of which are prime but now not indexed by Fin n.

The proof is induction on the size of the index set. The base case is obvious. For the inductive step the observation is that if we can find $j$ such that $\mathfrak{a}\cap P_j$ is a subset of the union of $P_i$ for $i\not=j$ then a purely set-theoretic argument shows that $\mathfrak{a}$ is also a subset of this union, so we're done by induction. We prove that $j$ exists by contradiction; if not then for all $j$ we can choose $a_j\in\mathfrak{a}\cap P_j$ such that $a_j\not\in P_i$ if $i\not=j$. Now choose $k$ in the index set which is arbitrary if the index set has size 2, and for which $P_k$ is prime if the index set has size 3 or more (probably this means that the induction should deal with the case n=2 separately). The trick is to consider $z:=a_k+\prod_{i\not=k} a_i\in\mathfrak{a}$ and to verify that $z\not\in P_i$ for any $i$ (consider the cases $i=k$ and $i\not=k$ separately), contradicting our hypothesis.

Task 2) If $A\to B$ makes $B$ an integral $A$-algebra, and if $Q\subseteq B$ is a prime ideal with preimage $P\subseteq A$, then $Q$ is maximal iff $P$ is.

This follows from the assertion that if $K\subseteq L$ is an extension of integral domains with $L$ integral over $K$, then $K$ is a field iff $L$ is. For all I know we have stuff like this. Here's the proof (this is Lemme 2 in Chapter 5 section 2 no 1 of Bourbaki Alg Comm, p32): if $K$ is a field then for any $x\in L$, $x$ is integral over $K$ and hence $K[x]$ is an integral domain finite-dimensional over a field and thus a field, so $x$ is invertible, meaning that $L$ is a field. Conversely if $L$ is a field and $z\in K$ is nonzero then $z^{-1}\in L$, so it's integral over $K$, and writing down the equation $z^{-n}+a_1z^{1-n}+\cdots=0$ and then multiplying both sides by $z^{n-1}$ gives that $z^{-1}\in K$, so $K$ is a field.

[Kevin Buzzard]

Task 3) What we actually need is the following corollary of Task 2: if $A\to B$ is integral, if $Q\subseteq I$ are ideals of $B$ with $Q$ prime, and if $Q\cap A=I\cap A=P$ is prime, then $Q=I$.

The proof is: localise at $S:=A-P$ to get $S^{-1}P$ a maximal ideal of $S^{-1}A$, and $S^{-1}B$ integral over $S^{-1}A$. Then $S^{-1}Q\subseteq S^{-1}I$ are ideals of $S^{-1}B$ above $S^{-1}P$ and $S^{-1}Q$ is prime so by task 2, $S^{-1}Q$ is maximal, thus $S^{-1}Q=S^{-1}I$ from which it follows that $Q=I$ by a standard property of localisation which hopefully we have.

Task 4) The claim is true (i.e. if $P'$ and $Q'$ are two prime ideals of $B$ with the same pullback to $A$ then they're in the same Galois orbit).

The proof (following the screenshot above): It suffices to prove that $Q'$ is a subset of the union over all $g$ of the $gP'$. For then by task 1 we have $Q'\subseteq gP'$ for some $g$, so by task 3 we have $Q'=gP'$.

To prove this, say $x\in Q'$; then $\prod_{\sigma\in G}\sigma x\in Q'\cap A=P\subseteq P'$ (we don't need that $A\to B$ is injective as far as I can see), so $\sigma x\in P'$ for some $\sigma$, and we just let $g=\sigma^{-1}$.

This is what we need to make progress here.

[Junyan Xu]

Task 1) is Ideal.subset_union_prime except that it assumes Ideal rather than a MulMemClass+AddMemClass.

[Junyan Xu]

@loogle Algebra.IsIntegral, Ideal.IsMaximal

[loogle]

:search: Ideal.isMaximal_comap_of_isIntegral_of_isMaximal, Ideal.isMaximal_of_isIntegral_of_isMaximal_comap, and 1 more

[Junyan Xu]

These solves Task 2), and it seems docs#Ideal.comap_lt_comap_of_integral_mem_sdiff directly solves Task 3).

[Kevin Buzzard]

Oh nice :-)

[Kevin Buzzard]

import Mathlib.RingTheory.Ideal.Pointwise
import Mathlib.RingTheory.IntegralClosure
import Mathlib.RingTheory.Ideal.Over

variable {A : Type*} [CommRing A]
  {B : Type*} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B]
  {G : Type*} [Group G] [Finite G] [MulSemiringAction G B]

open scoped algebraMap

variable (hGalois : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ a : A, b = a)

variable (P Q : Ideal B) [P.IsPrime] [Q.IsPrime]
  (hPQ : Ideal.comap (algebraMap A B) P = Ideal.comap (algebraMap A B) Q)

open scoped Pointwise

private lemma norm_fixed (b : B) (g : G) : g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, σ • b := calc
  g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, g • (σ • b) := sorry -- #14483
  _                     = ∏ᶠ σ : G, σ • b := finprod_eq_of_bijective (g • .) (MulAction.bijective g)
                                               fun x ↦ smul_smul g x b

theorem foo : ∃ g : G, Q = g • P := by
  cases nonempty_fintype G
  suffices ∃ g : G, Q ≤ g • P by
    obtain ⟨g, hg⟩ := this
    use g
    by_contra! hQ
    have : Q < g • P := lt_of_le_of_ne hg hQ
    obtain ⟨x, hxP, hxQ⟩ := Set.exists_of_ssubset <| this
    apply (Ideal.comap_lt_comap_of_integral_mem_sdiff (R := A) hg ⟨hxP, hxQ⟩ <|
      Algebra.isIntegral_def.1 inferInstance x).ne
    rw [← hPQ]
    ext x
    specialize hGalois (algebraMap A B x)
    have := hGalois.2 ⟨x, rfl⟩
    simp only [Ideal.mem_comap]
    nth_rw 2 [← this]
    exact Ideal.smul_mem_pointwise_smul_iff.symm
  suffices ∃ g ∈ (⊤ : Finset G), Q ≤ g • P by
    convert this; simp
  rw [← Ideal.subset_union_prime 1 1 <| fun g _ _ _ ↦ ?_]; swap
  · sorry -- g • P is defined as a map, but g is in a group so it's a comap
  intro x hx
  specialize hGalois (∏ᶠ σ : G, σ • x)
  obtain ⟨a, ha⟩ := hGalois.1 (norm_fixed _)
  -- a ∈ Q ∩ A ⊆ P by hPQ, so ha and primality of P says σ • x ∈ P for some σ
  -- now let i = σ⁻¹
  sorry

I need to sleep now but we're close to part (i) of the Bourbaki result. The beginning of the proof of part (ii) of the theorem is in #14155 .

[Ruben Van de Velde]

Ah, if you're going to post sorrys, I'm not going to be able to resist :)

  · -- g • P is defined as a map, but g is in a group so it's a comap
    have : (g⁻¹ • g • P).IsPrime := by
      simp only [smul_smul, mul_left_inv, one_smul]
      infer_instance
    rw [Ideal.isPrime_iff] at this ⊢
    obtain ⟨h1, h2⟩ := this
    constructor
    · contrapose! h1
      rw [h1]
      ext
      simp [Ideal.mem_pointwise_smul_iff_inv_smul_mem]
    · intro x y hxy
      simp only [smul_smul, mul_left_inv, one_smul] at h2
      simp [Ideal.mem_pointwise_smul_iff_inv_smul_mem]
      apply h2
      rw [← MulSemiringAction.smul_mul]
      rwa [← Ideal.mem_pointwise_smul_iff_inv_smul_mem]

(probably can be golfed a lot)

[Ruben Van de Velde]

A bit of the other one:

  obtain ⟨σ, hσ⟩ : ∃ σ : G, σ • x ∈ P := sorry
  simp only [Finset.top_eq_univ, Finset.coe_univ, Set.mem_univ, Set.iUnion_true, Set.mem_iUnion,
    SetLike.mem_coe]
  use σ⁻¹
  rwa [Ideal.mem_inv_pointwise_smul_iff]

[Ruben Van de Velde]

theorem _root_.Ideal.IsPrime.finprod_mem_iff_exists_mem {R S : Type*} [Finite R] [CommSemiring S]
    (I : Ideal S) [hI : I.IsPrime] (f : R → S)  :
    ∏ᶠ x, f x ∈ I ↔ ∃ p, f p ∈ I := by
  have := Fintype.ofFinite R
  rw [finprod_eq_prod_of_fintype, Finset.prod_eq_multiset_prod, hI.multiset_prod_mem_iff_exists_mem]
  simp

theorem Ideal.ext_iff {α : Type*} [Semiring α] {I J : Ideal α} : I = J ↔ ∀ x, x ∈ I ↔ x ∈ J := by
  refine ⟨?_, ext⟩
  rintro rfl
  simp

theorem extracted_1
    {B : Type*} [CommRing B] {G : Type*} [Group G] [MulSemiringAction G B] (P : Ideal B) (g : G) :
    (g • P).IsPrime ↔ P.IsPrime := by
  simp_rw [Ideal.isPrime_iff]
  apply and_congr
  · refine Iff.not ?_
    constructor <;>
      simp only [Ideal.ext_iff, Submodule.mem_top, iff_true] <;>
      intro h x
    · simpa using h (g • x)
    · simpa [Ideal.mem_pointwise_smul_iff_inv_smul_mem] using h (g⁻¹ • x)
  · constructor
    · intro h x y hxy
      specialize @h (g • x) (g • y)
      simp only [Ideal.smul_mem_pointwise_smul_iff] at h
      apply h
      rwa [← MulSemiringAction.smul_mul, Ideal.smul_mem_pointwise_smul_iff]
    · intro h x y hxy
      specialize @h (g⁻¹ • x) (g⁻¹ • y)
      simp_rw [← Ideal.mem_pointwise_smul_iff_inv_smul_mem] at h
      apply h
      rwa [← MulSemiringAction.smul_mul, ← Ideal.mem_pointwise_smul_iff_inv_smul_mem]

theorem foo : ∃ g : G, Q = g • P := by
  cases nonempty_fintype G
  suffices ∃ g : G, Q ≤ g • P by
    obtain ⟨g, hg⟩ := this
    use g
    by_contra! hQ
    have : Q < g • P := lt_of_le_of_ne hg hQ
    obtain ⟨x, hxP, hxQ⟩ := Set.exists_of_ssubset <| this
    apply (Ideal.comap_lt_comap_of_integral_mem_sdiff (R := A) hg ⟨hxP, hxQ⟩ <|
      Algebra.isIntegral_def.1 inferInstance x).ne
    rw [← hPQ]
    ext x
    specialize hGalois (algebraMap A B x)
    have := hGalois.2 ⟨x, rfl⟩
    simp only [Ideal.mem_comap]
    nth_rw 2 [← this]
    exact Ideal.smul_mem_pointwise_smul_iff.symm
  suffices ∃ g ∈ (⊤ : Finset G), Q ≤ g • P by
    convert this; simp
  rw [← Ideal.subset_union_prime 1 1 <| fun g _ _ _ ↦ ?_]; swap
  · rwa [extracted_1]
  intro x hx
  specialize hGalois (∏ᶠ σ : G, σ • x)
  obtain ⟨a, ha⟩ := hGalois.1 (norm_fixed _)
  have : (a : B) ∈ Q := by
    rw [← ha, Ideal.IsPrime.finprod_mem_iff_exists_mem]
    use 1
    simpa using hx
  have : (a : B) ∈ P := by
    unfold Algebra.cast
    rwa [← Ideal.mem_comap, hPQ, Ideal.mem_comap]
  rw [← ha, Ideal.IsPrime.finprod_mem_iff_exists_mem] at this
  obtain ⟨σ, hσ⟩ : ∃ σ : G, σ • x ∈ P := this
  simp only [Finset.top_eq_univ, Finset.coe_univ, Set.mem_univ, Set.iUnion_true, Set.mem_iUnion,
    SetLike.mem_coe]
  use σ⁻¹
  rwa [Ideal.mem_inv_pointwise_smul_iff]

[Ruben Van de Velde]

Ruben Van de Velde said:

Ah, if you're going to post sorrys, I'm not going to be able to resist :)

  · -- g • P is defined as a map, but g is in a group so it's a comap
    have : (g⁻¹ • g • P).IsPrime := by
      simp only [smul_smul, mul_left_inv, one_smul]
      infer_instance
    rw [Ideal.isPrime_iff] at this ⊢
    obtain ⟨h1, h2⟩ := this
    constructor
    · contrapose! h1
      rw [h1]
      ext
      simp [Ideal.mem_pointwise_smul_iff_inv_smul_mem]
    · intro x y hxy
      simp only [smul_smul, mul_left_inv, one_smul] at h2
      simp [Ideal.mem_pointwise_smul_iff_inv_smul_mem]
      apply h2
      rw [← MulSemiringAction.smul_mul]
      rwa [← Ideal.mem_pointwise_smul_iff_inv_smul_mem]

(probably can be golfed a lot)

Golfing:

  · apply Ideal.map_isPrime_of_equiv (MulSemiringAction.toRingEquiv _ _ g)

[Daniel Morrison]

I was curious and Google translated (ii):

Let $P'$ be a prime ideal of $A'$, $P = P' \cap A$, $k$ (resp. $k'$) the field of fractions of $A/P$ (resp. $A'/P'$). Then $k'$ is a quasi-Galois extension (*) of $k$, and the canonical homomorphism of $G^Z(P')$ in the group $\Gamma$ of $k$-automorphisms of $k'$ defines, by passing to the quotient, an isomorphism of $G^Z(P')/G^T(P')$ on $\Gamma$.

(*) In order to avoid confusion with other meanings of the word normal, we will henceforth use the terms "quasi-Galois extension" as synonyms for the terms "normal extension".

Does anyone know what $G^Z(P')$ and $G^T(P')$ mean?

[Kevin Buzzard]

They are the elements of G which send P' to P' and the kernel of the reduction map respectively. Sorry, this is all on hold for a while because I'm at a conference this week, and on an NSF panel and running a short lean course for the LMS next week. I'll have a few weeks for Fermat after that

[Kevin Buzzard]

I finally got back to this! There's no LaTeX blueprint (I think Frobenius elements should go straight into mathlib) but I have at least managed to formalise the statements of all of the parts of the Bourbaki lemma, and I've left plenty of sorries.

The file is FLT.MathlibExperiments.FrobeniusRiou. There are 12 sorries, many probably very easy, and at least one still quite difficult. In particular there is not even a sketch proof of surjectivity yet. But it occurred to me that other people might be happy filling in some sorrys. I've sketched some proofs in comments in the lean document.

An example of what we need: Let G act on ring B with invariants A, let Q be a prime of B above P of A. Let D be the stabiliser of Q for the action of G acting on the ideals of B. We need to write down the group hom from D to the A/P-auts of B/Q (sending b-bar to g*b-bar), and then another one from D to the K-auts of L, where K=Frac(A/P) and L=Frac(B/Q) (which comes from universal properties of fields of fractions). I've defined all the data but sorried all the commutativity proofs. I also need better names for these group homs.

If people want to work on the sorrys then please feel free to claim them here. I'll hopefully find the time to flesh out some of the ideas in the surjectivity proof this week; the others should be much easier.

[Daniel Morrison]

Here's what I got for the first sorry:

private theorem F_eval_eq_zero (b : B) : (F G b).eval b = 0 := by
  let foo := Fintype.ofFinite G
  simp [F_spec,finprod_eq_prod_of_fintype,eval_prod]
  apply @Finset.prod_eq_zero _ _ _ _ _ (1 : G) (Finset.mem_univ 1)
  simp

[Kevin Buzzard]

Thanks! Let me know if you just want me to cut and paste and push myself -- but if you have a GitHub account and want to be one of the first contributors to FLT then please feel free to make a PR from a fork! Let me know. Right now I'm personally concentrating on adding more sorries rather than filling them in.

[Ruben Van de Velde]

I've pushed FLT#124 to turn the CI green again

[Kevin Buzzard]

Thanks. Probably I need a better workflow here. I seem to definitely want some kind of "experiments" file where I want to feel free to define ten different topologies on something all with the same name, because I'm exploring the design space. The problem with putting these inside the FLT subdir of the project and then saying "please build everything" is that you get nameclashes. The problem with putting them outside FLT is that they then appear to be not part of the project in some sense. But some of these module topologies files are very old -- I am now convinced that I know which approach I want. I am loath to delete old files until something gets merged to mathlib though.

[Yaël Dillies]

Why don't you wrap them in namespace experiment1, namespace experiment2, ...?

[Kevin Buzzard]

Yes that's definitely another possibility!

[Ruben Van de Velde]

I'll do that

[Daniel Morrison]

I've made a PR for my addition. I think I did it correctly but please let me know if I'm doing something wrong.

[Kevin Buzzard]

I'm just learning about how CI works. Can you merge master? I've been goofing around trying to get my project to compile now I've understood the importance of this.

[Daniel Morrison]

I think I did what you're asking, I'm not great with GitHub

[Ruben Van de Velde]

You did fine, as far as I can tell - now @Kevin Buzzard needs to push the button again that says you're not doing anything naughty

[Kevin Buzzard]

I'm currently trying to get main to pass CI :-/ I'll be with you shortly

[Daniel Morrison]

I'm working on M_eval_eq_zero now. First, I think algebraMap A[X] B[X] should be algebraMap A B in the theorem statement. I also tried modifying M_spec to use algebraMap A B explicitly rather than casting since it was having some problems understanding the casting. Here's my code for reference:

omit [Algebra.IsIntegral A B] in
theorem M_spec (b : B) : ((M G hGalois b : A[X]) : B[X]) = F G b := (F_descent hGalois b).choose_spec

omit [Algebra.IsIntegral A B] in
theorem M_spec' (b : B) : (M G hGalois b : A[X]).map (algebraMap A B) = F G b :=
  (F_descent hGalois b).choose_spec

theorem M_eval_eq_zero (b : B) : (M G hGalois b).eval₂ (algebraMap A[X] B[X]) b = 0 := by
  sorry -- follows from `F_eval_eq_zero`

omit [Algebra.IsIntegral A B] in
theorem M_eval_eq_zero' (b : B) : (M G hGalois b).eval₂ (algebraMap A B) b = 0 := by
  rw [eval₂_eq_eval_map, M_spec', F_eval_eq_zero]

If the modifications are okay I can do another PR.

[Daniel Morrison]

I have kept working on some more of these tasks, my code so far is here. Here's a couple places I'm stuck:

• Algebra.isAlgebraic_of_subring_isAlgebraic is done besides needing a proof for the product of two algebraic elements is algebraic (I couldn't find it in Mathlib, but it does have inverse of algebraic element is algebraic)
• I have a start to part_b1 but I'm having trouble showing the polynomial is non-zero since it gets mapped through several rings. I think we might need to be more strict about the choice of M from F_descent.

If anyone has suggestions I'd be happy to hear them!

[Riccardo Brasca]

Strange if it is really missing, anyway you go via docs#isAlgebraic_iff_isIntegral and docs#IsIntegral.prod

[Kevin Buzzard]

The poly is nonzero because it's monic

[Damiano Testa]

... and the ring is non-trivial, maybe?

[Daniel Morrison]

I have that F G b : B[X] is monic (assuming non-trivial ring), the issue is when lifting to M : A[X] there isn't anything at the moment guaranteeing that we choose to lift to a monic polynomial. This should be possible but would require being more careful about choosing how to lift the coefficients.

[Riccardo Brasca]

IIRC we know we can lift monic polynomials to monic polynomials. Look at the file where polynomial.lift is defined

[Riccardo Brasca]

Polynomial.lifts_and_degree_eq_and_monic

[Daniel Morrison]

I found it, thank you!

[Daniel Morrison]

Okay, I was able to finish part_b1, thanks for the help!

[Kevin Buzzard]

Thanks! I'm currently traveling but I'll be back this weekend and will be back to pushing to get this stuff finished. From October I'm on this job full time so hopefully there will be regular progress from then on.

[Daniel Morrison]

I'm working on map_mul' in Pointwise.stabilizer.toGaloisGroup and I need to use the map_mul' property of quotientAlgebraActionMonoidHom, but I can't seem to get Lean to recognize that property. I tried doing quotientAlgebraActionMonoidHom.map_mul'but that didn't work. For context here's what I have so far:

noncomputable def Pointwise.stabilizer.toGaloisGroup : MulAction.stabilizer G Q →* (L ≃ₐ[K] L) where
  toFun gh := IsFractionRing.algEquiv_lift Q P L K (Pointwise.quotientAlgebraActionMonoidHom Q P gh)
  map_one' := sorry
  map_mul' := by
    intro ⟨x, hx⟩ ⟨y, hy⟩
    apply AlgEquiv.ext
    intro l; dsimp
    obtain ⟨r, s, _, rfl⟩ := @IsFractionRing.div_surjective (B ⧸ Q) _ _ L _ _ _ l
    unfold IsFractionRing.algEquiv_lift
    unfold IsFractionRing.fieldEquivOfRingEquiv
    simp

    sorry

[Kevin Buzzard]

Oh I didn't know that people were still thinking about this. I was going to relaunch this project on 1st October with a much more coherent plan for how to prove it. I'm pleased to note that on my branch which contains a whole bunch more stuff, that definition is still missing :-)

[Daniel Morrison]

I'm just playing around with it for fun. If you want I can do a pull request for a few pieces I figured out, and I'll wait to do more until October.

[Kevin Buzzard]

Yeah I was just warning you that things are currently in flux :-) Feel free to PR what you have! I am too busy to fix sorries right now, I am trying to put something coherent together for 1st Oct but unfortunately I'm giving two talks before the 1st, one talk on the 1st and then another one on the 4th, so I'm a bit snowed under

[Daniel Morrison]

PR has been created!