From 3ab2c723812ac7aa4f45c1d9abde301a31174e1e Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu, 3 Oct 2024 15:25:02 +0200 Subject: [PATCH] Prove Mbar_eval_eq_zero, update blueprint (#156) --- FLT/MathlibExperiments/FrobeniusRiou.lean | 36 +++++++++++-- blueprint/src/chapter/FrobeniusProject.tex | 59 ++++++++++++++++------ 2 files changed, 74 insertions(+), 21 deletions(-) diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean index f08eaaec..c63f6290 100644 --- a/FLT/MathlibExperiments/FrobeniusRiou.lean +++ b/FLT/MathlibExperiments/FrobeniusRiou.lean @@ -450,9 +450,31 @@ theorem Ideal.Quotient.eq_zero_iff_mem' (x : A) : section B_mod_Q_over_A_mod_P_stuff +section Mathlib.RingTheory.Ideal.Quotient + +namespace Ideal + +variable {R : Type*} [CommRing R] {I : Ideal R} + +protected noncomputable +def Quotient.out (x : R ⧸ I) := + Quotient.out' x + +theorem Quotient.out_eq (x : R ⧸ I) : Ideal.Quotient.mk I (Ideal.Quotient.out x) = x := by + simp only [Ideal.Quotient.out, Ideal.Quotient.mk, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, + Submodule.Quotient.mk, Quotient.out_eq'] + +@[elab_as_elim] +protected theorem Quotient.induction_on + {p : R ⧸ I → Prop} (x : R ⧸ I) (h : ∀ a, p (Ideal.Quotient.mk I a)) : p x := + Quotient.inductionOn x h + +end Ideal + +end Mathlib.RingTheory.Ideal.Quotient + namespace MulSemiringAction.CharacteristicPolynomial -example : Function.Surjective (Ideal.Quotient.mk Q) := Ideal.Quotient.mk_surjective open Polynomial /- @@ -466,8 +488,7 @@ variable {Q} in noncomputable def Mbar (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) (bbar : B ⧸ Q) : (A ⧸ P)[X] := - Polynomial.map (Ideal.Quotient.mk P) <| M hFull' <| - (Ideal.Quotient.mk_surjective bbar).choose + Polynomial.map (Ideal.Quotient.mk P) <| M hFull' <| Ideal.Quotient.out bbar variable (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) @@ -486,8 +507,13 @@ theorem Mbar_deg [Nontrivial A] [Nontrivial B] (bbar : B ⧸ Q) : · rw [(M_monic hFull' _).leadingCoeff] simp only [map_one, ne_eq, one_ne_zero, not_false_eq_true] -theorem Mbar_eval_eq_zero (bbar : B ⧸ Q) : eval₂ (algebraMap (A ⧸ P) (B ⧸ Q)) bbar (Mbar P hFull' bbar) = 0 := by - sorry +omit [SMulCommClass G A B] [Q.IsPrime] [P.IsPrime] in +theorem Mbar_eval_eq_zero [Nontrivial A] [Nontrivial B] (bbar : B ⧸ Q) : + eval₂ (algebraMap (A ⧸ P) (B ⧸ Q)) bbar (Mbar P hFull' bbar) = 0 := by + have h := congr_arg (algebraMap B (B ⧸ Q)) (M_eval_eq_zero hFull' (Ideal.Quotient.out bbar)) + rw [map_zero, hom_eval₂, Ideal.Quotient.algebraMap_eq, Ideal.Quotient.out_eq] at h + simpa [Mbar, eval₂_map, ← Ideal.Quotient.algebraMap_eq, + ← IsScalarTower.algebraMap_eq A (A ⧸ P) (B ⧸ Q), IsScalarTower.algebraMap_eq A B (B ⧸ Q)] end CharacteristicPolynomial diff --git a/blueprint/src/chapter/FrobeniusProject.tex b/blueprint/src/chapter/FrobeniusProject.tex index 62d65b17..d619e79c 100644 --- a/blueprint/src/chapter/FrobeniusProject.tex +++ b/blueprint/src/chapter/FrobeniusProject.tex @@ -144,7 +144,9 @@ \section{The extension \texorpdfstring{$B/A$}{B/A}.} \leanok If $B$ is nontrivial then $F_b$ is monic. \end{lemma} -\begin{proof} Obvious. +\begin{proof} + \leanok + Obvious. \end{proof} It's also clear that $F_b$ has degree $|G|$ and has $b$ as a root. @@ -157,6 +159,7 @@ \section{The extension \texorpdfstring{$B/A$}{B/A}.} \begin{definition} \lean{MulSemiringAction.CharacteristicPolynomial.M} \label{MulSemiringAction.CharacteristicPolynomial.M} + \uses{MulSemiringAction.CharacteristicPolynomial.F} \leanok $M_b$ is any monic degree $|G|$ polynomial in $A[X]$ whose image in $B[X]$ is $F_b$. @@ -166,9 +169,12 @@ \section{The extension \texorpdfstring{$B/A$}{B/A}.} \label{MulSemiringAction.CharacteristicPolynomial.M_eval_eq_zero} \lean{MulSemiringAction.CharacteristicPolynomial.M_eval_eq_zero} \uses{MulSemiringAction.CharacteristicPolynomial.M} + \leanok $M_b$ has $b$ as a root. \end{lemma} -\begin{proof} Follows from the fact that $F_b$ has $b$ as a root. +\begin{proof} + \leanok + Follows from the fact that $F_b$ has $b$ as a root. \end{proof} \begin{lemma} \label{MulSemiringAction.CharacteristicPolynomial.M_deg} @@ -178,6 +184,7 @@ \section{The extension \texorpdfstring{$B/A$}{B/A}.} $M_b$ has degree $n$. \end{lemma} \begin{proof} + \uses{MulSemiringAction.CharacteristicPolynomial.F_degree} \leanok Exercise. \end{proof} @@ -196,11 +203,14 @@ \section{The extension \texorpdfstring{$B/A$}{B/A}.} \begin{theorem} \lean{MulSemiringAction.CharacteristicPolynomial.isIntegral} \label{MulSemiringAction.CharacteristicPolynomial.isIntegral} - \uses{MulSemiringAction.CharacteristicPolynomial.M, - MulSemiringAction.CharacteristicPolynomial.M_monic} + \uses{MulSemiringAction.CharacteristicPolynomial.M} + \leanok $B/A$ is integral. \end{theorem} -\begin{proof} Use $M_b$. +\begin{proof} + \uses{MulSemiringAction.CharacteristicPolynomial.M_monic} + \leanok + Use $M_b$. \end{proof} \section{The extension \texorpdfstring{$(B/Q)/(A/P)$}{(B/Q)/(A/P)}.} @@ -223,38 +233,53 @@ \section{The extension \texorpdfstring{$(B/Q)/(A/P)$}{(B/Q)/(A/P)}.} \begin{theorem} \lean{MulSemiringAction.CharacteristicPolynomial.Mbar_deg} \label{MulSemiringAction.CharacteristicPolynomial.Mbar_deg} - \uses{MulSemiringAction.CharacteristicPolynomial.M} + \uses{MulSemiringAction.CharacteristicPolynomial.Mbar} + \leanok $\overline{M}_{\overline{b}}$ has degree $|G|$. \end{theorem} -\begin{proof} Exercise. +\begin{proof} + \uses{MulSemiringAction.CharacteristicPolynomial.M_deg, + MulSemiringAction.CharacteristicPolynomial.M_monic} + \leanok + Exercise. \end{proof} \begin{theorem} \lean{MulSemiringAction.CharacteristicPolynomial.Mbar_monic} \label{MulSemiringAction.CharacteristicPolynomial.Mbar_monic} - \uses{MulSemiringAction.CharacteristicPolynomial.M} - $\overline{M}_{\overline{b}}$ is monic. + \uses{MulSemiringAction.CharacteristicPolynomial.Mbar} + \leanok + $\overline{M}_{\overline{b}}$ is monic. \end{theorem} -\begin{proof} Exercise (note that integral domains are nontrivial). +\begin{proof} + \uses{MulSemiringAction.CharacteristicPolynomial.M_monic} + \leanok + Exercise (note that integral domains are nontrivial). \end{proof} \begin{theorem} \lean{MulSemiringAction.CharacteristicPolynomial.Mbar_eval_eq_zero} \label{MulSemiringAction.CharacteristicPolynomial.Mbar_eval_eq_zero} - \uses{MulSemiringAction.CharacteristicPolynomial.M} + \uses{MulSemiringAction.CharacteristicPolynomial.Mbar} + \leanok $\overline{M}_{\overline{b}}$ has $\overline{b}$ as a root. \end{theorem} -\begin{proof} Exercise. +\begin{proof} + \uses{MulSemiringAction.CharacteristicPolynomial.M_eval_eq_zero} + \leanok + Exercise. \end{proof} \begin{theorem} \lean{MulSemiringAction.reduction_isIntegral} \label{MulSemiringAction.reduction_isIntegral} - \uses{MulSemiringAction.CharacteristicPolynomial.M} + \uses{MulSemiringAction.CharacteristicPolynomial.Mbar} + \leanok $(B/Q)/(A/P)$ is an integral extension. \end{theorem} \begin{proof} - \uses{MulSemiringAction.CharacteristicPolynomial.Mbar_monic} + \uses{MulSemiringAction.CharacteristicPolynomial.Mbar_monic, + MulSemiringAction.CharacteristicPolynomial.Mbar_eval_eq_zero} Use $\overline{M}_{\overline{b}}$. \end{proof} @@ -263,11 +288,13 @@ \section{The extension \texorpdfstring{$(B/Q)/(A/P)$}{(B/Q)/(A/P)}.} \begin{corollary} \lean{Algebra.exists_dvd_nonzero_if_isIntegral} \label{Algebra.exists_dvd_nonzero_if_isIntegral} - \uses{MulSemiringAction.reduction_isIntegral} + \leanok If $\beta\in B/Q$ is nonzero then there's some nonzero $\alpha\in A/P$ such that $\beta$ divides the image of $\alpha$ in $B/Q$. \end{corollary} -\begin{proof} Note: Is this in mathlib already? This proof works for any +\begin{proof} + \uses{MulSemiringAction.reduction_isIntegral} + Note: Is this in mathlib already? This proof works for any integral extension if the top ring has no zero divisors. Let $\beta$ be nonzero, and