diff --git a/FLT/MathlibExperiments/Frobenius2.lean b/FLT/MathlibExperiments/Frobenius2.lean index 580e0ddb..2c08eb82 100644 --- a/FLT/MathlibExperiments/Frobenius2.lean +++ b/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 --/ diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean index d71950c2..befb716c 100644 --- a/FLT/MathlibExperiments/FrobeniusRiou.lean +++ b/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 diff --git a/blueprint/src/chapter/FrobeniusProject.tex b/blueprint/src/chapter/FrobeniusProject.tex index f4820c23..74ec3f92 100644 --- a/blueprint/src/chapter/FrobeniusProject.tex +++ 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.