Prove Mbar_eval_eq_zero, update blueprint (#156)

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
 

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