add more details to blueprint about Frobenius project

FLT/MathlibExperiments/Frobenius2.lean

@@ -290,60 +290,3 @@ lemma Frob_Q : Frob A Q isGalois P • Q = Q := by
   have this := Q.sub_mem hy2 <| Frob_spec A Q isGalois P
   simp only [sub_sub_cancel] at this
   exact y_not_in_Q A Q <| Ideal.IsPrime.mem_of_pow_mem (show Q.IsPrime by infer_instance) _ this
-
-lemma _root_.Ideal.Quotient.coe_eq_coe_iff_sub_mem {R : Type*} [CommRing R] {I : Ideal R} (x y : R) :
-  (x : R ⧸ I) = y ↔ x - y ∈ I := Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _
-
-lemma coething (A B : Type*) [CommSemiring A] [Ring B] [Algebra A B] (a : A) (n : ℕ) :
-    (a ^ n : A) = (a : B) ^ n := by
-  --change algebraMap A B a ^ n = algebraMap A B (a ^ n)
-  --symm
-  exact map_pow _ _ _
---  simp only [map_pow]
-
---attribute [norm_cast] map_pow
-
-#exit
-
-lemma Frob_Q_eq_pow_card (x : B) : Frob A Q isGalois P x - x^(Fintype.card (A⧸P)) ∈ Q := by
-  by_cases hx : x ∈ Q
-  · refine Q.sub_mem ?_ (Q.pow_mem_of_mem hx _ Fintype.card_pos)
-    nth_rw 2 [← Frob_Q A Q isGalois P]
-    change (Frob A Q isGalois P) • x ∈ _
-    rw [Ideal.map_eq_comap_symm, Ideal.mem_comap]
-    convert hx
-    exact inv_smul_smul _ _
-  ·
-    have foo : (x : B ⧸ Q) ≠ 0 :=
-      mt (fun h ↦ (Submodule.Quotient.mk_eq_zero Q).mp h) hx
-    let foobar : Field (B⧸Q) := ((Ideal.Quotient.maximal_ideal_iff_isField_quotient Q).mp ‹_›).toField
-    let xbar : (B ⧸ Q)ˣ := Units.mk0 (x : B ⧸ Q) foo
-    obtain ⟨n, (hn : g Q ^ n = xbar)⟩ := g_spec Q xbar
-    have hn2 : (g Q : B ⧸ Q) ^ n = xbar := by exact_mod_cast hn
-    change _ = (x : B ⧸ Q) at hn2
-    rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem]
-    change ((Frob A Q isGalois P) x : B ⧸ Q) = x ^ Fintype.card (A ⧸ P)
-    rw [← hn2]
-    have fact1 := Frob_spec A Q isGalois P
-    have fact2 : y A Q = (g Q : B⧸Q) := y_mod_Q A Q
-    rw [← fact2]
-    rw [← Ideal.Quotient.coe_eq_coe_iff_sub_mem] at fact1
-    push_cast at fact1
-    rw [pow_right_comm]
-    rw [← fact1]
-    norm_cast
-    rw [Ideal.Quotient.coe_eq_coe_iff_sub_mem]
-    have fact3 := Frob_Q A Q isGalois P
-    rw [← smul_pow']
-    change (Frob A Q isGalois P) • x - _ ∈ _
-    rw [← smul_sub]
-    nth_rw 3 [ ← fact3]
-    suffices (x - y A Q ^ n) ∈ Q by
-      exact? says exact Ideal.smul_mem_pointwise_smul_iff.mpr this
-    sorry
-
-/- maths proof:
-
-2) σ is x ^ #A/P mod Q
-3) Application to number fields
--/

FLT/MathlibExperiments/FrobeniusRiou.lean

@@ -183,7 +183,7 @@ section full_descent
 
 variable (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a)
 
--- **IMPORTANT** The `splitting_of_full` approach is lousy and should be
+-- Remark: the `splitting_of_full` approach is lousy and should be
 -- replaced by the commented-out code below (lines 275-296 currently)
 
 /-- This "splitting" function from B to A will only ever be evaluated on
@@ -241,7 +241,6 @@ theorem M_coeff_card (b : B) :
   · intro d _ hd
     exact coeff_monomial_of_ne (splitting_of_full hFull ((F G b).coeff d)) hd
 
--- **IMPORTANT** `M` should be refactored before proving this. See commented out code below.
 theorem M_deg_eq_F_deg [Nontrivial A] (b : B) : (M hFull b).degree = (F G b).degree := by
   apply le_antisymm (M_deg_le hFull b)
   rw [F_degree]
@@ -254,7 +253,6 @@ theorem M_deg [Nontrivial A] (b : B) : (M hFull b).degree = Nat.card G := by
   rw [M_deg_eq_F_deg hFull b]
   exact F_degree G b
 
--- **IMPORTANT** `M` should be refactored before proving this. See commented out code below.
 theorem M_monic (b : B) : (M hFull b).Monic := by
   have this1 := M_deg_le hFull b
   have this2 := M_coeff_card hFull b

blueprint/src/chapter/FrobeniusProject.tex

@@ -340,30 +340,69 @@ \section{Proof of surjectivity.}
   with $M$ the maximal separable subextension of $L/K$.
 \end{definition}
 
+NB we do use nonzeroness at some point, and $y$ can be zero in the case $L=K$
+(this seems to have been missed by Bourbaki).
+
 Note that the existence of some $\lambda\in L$ with this property just comes from finite
 and separable implies simple; we can use the ``clear denominator'' technique introduced
 earlier to scale this by some nonzero $\alpha\in A$ into $B/Q$, as
 $K(\lambda)=K(\alpha\lambda)$.
 
-Here is a slightly delicate result whose proof I haven't thought too hard about.
+Our next goal is the following result:
 \begin{theorem} There exists some $x\in B$ and $\alpha\in A$ with the following
   properties.
   \begin{enumerate}
-  \item $x=\alpha y$ mod $Q$ and $\alpha$ isn't zero mod $Q$.
+  \item $x=\alpha y$ mod $Q$ and $\alpha$ isn't zero mod $P$.
   \item $x\in Q'$ for all $Q'\not=Q$ in the $G$-orbit of $Q$.
   \end{enumerate}
 \end{theorem}
+
+Bourbaki only prove this in the case that $P$ is maximal (and implicitly use $\alpha=1$),
+but this generalisation seems to be fine. To prove it, we need to talk a little about localization.
+
+Let $S$ be the complement of $P$, so $S$ is a multiplicative subset of $A$.
+Write $A[1/S]$ for the localisation of $A$ at $S$, and write $B[1/S]$
+for the localisation of $B$ at (the image of) $S$. I suspect that this is the
+same as $B\otimes_AA[1/S]$.
+
+\begin{lemma}
+  The prime ideals of $B[1/S]$ over $P[1/S] \subseteq A[1/S]$ biject naturally with
+  the prime ideals of $B$ over $P$. More precisely, the $B$-algebra $B[1/S]$
+  gives a canonical map $B\to B[1/S]$ and hence a canonical map from prime ideals
+  of $B[1/S]$ to prime ideals of $B$. The claim is that this map induces
+  a bijection between the primes of $B[1/S]$ above $P[1/S]$ and the primes
+  of $B$ above $P$.
+\end{lemma}
+\begin{proof}
+  Hopefully this is in mathlib in some form already. In general $\Spec(B[1/S])$ is just the subset of $\Spec(B)$
+  consisting of primes of $B$ which miss $S$ (i.e., whose intersection with $A$ is a subset of $P$).
+\end{proof}
+
+\begin{lemma}
+  The primes of $B[1/S]$ above $P[1/S]$ are all maximal.
+\end{lemma}
 \begin{proof}
-  Idea. Localise away from P, then all the $Q_i$ are maximal, use CRT and then clear denominators.
+  This follows from {\tt Algebra.IsIntegral.isField\_iff\_isField} and the fact
+  that an ideal is maximal iff the quotient by it is a field.
 \end{proof}
 
-We now choose some $x\in B[1/S]$ which is $y$ modulo $Q$ and $0$ modulo all the other
-primes of $B$ above $P$, and consider the monic degree $|G|$ polynomial $f$ in $K[X]$
-with $x$ and its conjugates as roots. If $\sigma\in\Aut_K(L)$ then $\sigma(\overline{x})$
+\begin{proof}(of theorem):
+Because all these ideals of $B[1/S]$ are maximal, they're pairwise coprime.
+So by the Chinese Remainder Theorem we can find an element of $B[1/S]$ which
+is equal to $y$ modulo $Q[1/S]$ and equal to $0$ modulo all the other primes.
+This element is of the form $x/\alpha$ for some $x\in B$ and $\alpha\in S$,
+and one now checks that everything works.
+\end{proof}
+
+It is probably worth remarking that the rest of the surjectivity argument was done
+by Jou Glasheen in the special case of number fields, in the file {\tt Frobenius2.lean}
+
+Briefly: we consider the monic degree $|G|$ polynomial $f_x$ in $K[X]$ or $\overline{M}_x$ in $(A/P)[X]$,
+which has $x$ and its G-conjugates as roots. If $\sigma\in\Aut_K(L)$ then $\sigma(\overline{x})$
 is a root of $f$ as $\sigma$ fixes $K$ pointwise. Hence $\sigma(\overline{x})=\overline{g(x)}$
-for some $g\in G$, and because $\sigma(\overline{x})\not=0$ we have $\overline{g(x)}\not=0$
+for some $g\in G$ (because we're over an integral domain), and because $\sigma(\overline{x})\not=0$ we have $\overline{g(x)}\not=0$
 and hence $g(x)\notin Q[1/S]$. Hence $x\notin g^{-1} Q[1/S]$ and thus $g^{-1}Q=Q$ and $g\in SD_Q$.
 Finally we have $\phi_g=\sigma$ on $K$ and on $y$, so they are equal on $M$ and hence on $L$ as
 $L/M$ is purely inseparable.
 
-This part of the argument seems weak.
+TODO: break this up into smaller pieces.