minor tinkering

Author: kbuzzard

FLT/MathlibExperiments/FrobeniusRiou.lean

@@ -183,6 +183,9 @@ 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
+-- replaced by the commented-out code below (lines 275-296 currently)
+
 /-- This "splitting" function from B to A will only ever be evaluated on
 G-invariant elements of B, and the two key facts about it are
 that it lifts such an element to `A`, and for reasons of
@@ -238,6 +241,7 @@ 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 (b : B) : (M hFull b).degree = (F G b).degree := by
   apply le_antisymm (M_deg_le hFull b)
   -- hopefully not too hard from previous two lemmas
@@ -247,6 +251,7 @@ theorem M_deg (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
@@ -268,7 +273,7 @@ theorem M_spec (b : B) : ((M hFull b : A[X]) : B[X]) = F G b := by
   simp_rw [finset_sum_coeff, ← lcoeff_apply, lcoeff_apply, coeff_monomial]
   aesop
 
-/--
+/-
 private theorem F_descent_monic
   (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) (b : B) :
     ∃ M : A[X], (M : B[X]) = F G b ∧ Monic M := by
@@ -291,9 +296,11 @@ theorem M_spec' (b : B) : (map (algebraMap A B) (M G hFull b)) = F G b :=
 theorem M_monic (b : B) : (M G hFull b).Monic := (F_descent_monic hFull b).choose_spec.2
 --/
 
+omit [Nontrivial B] in
 theorem coe_poly_as_map (p : A[X]) : (p : B[X]) = map (algebraMap A B) p := rfl
 
 
+omit [Nontrivial B] in
 theorem M_eval_eq_zero (b : B) : (M hFull b).eval₂ (algebraMap A B) b = 0 := by
   rw [eval₂_eq_eval_map, ← coe_poly_as_map, M_spec, F_eval_eq_zero]
 
@@ -334,6 +341,7 @@ theorem Nontrivial_of_exists_prime {R : Type*} [CommRing R]
   apply Subsingleton.elim
 
 -- (Part a of Théorème 2 in section 2 of chapter 5 of Bourbaki Alg Comm)
+omit   [Nontrivial B] in
 theorem part_a [SMulCommClass G A B]
     (hPQ : Ideal.comap (algebraMap A B) P = Ideal.comap (algebraMap A B) Q)
     (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) :
@@ -670,7 +678,7 @@ noncomputable def residueFieldExtensionPolynomial [DecidableEq L] (x : L) : K[X]
   -- `Algebra.exists_dvd_nonzero_if_isIntegral` above, and then use Mbar
   -- scaled appropriately.
 
-theorem f [DecidableEq L] (l : L) :
+theorem f_exists [DecidableEq L] (l : L) :
     ∃ f : K[X], f.Monic ∧ f.degree = Nat.card G ∧
     eval₂ (algebraMap K L) l f = 0 ∧ f.Splits (algebraMap K L) := by
   use Bourbaki52222.residueFieldExtensionPolynomial G L K l
@@ -699,6 +707,9 @@ theorem Algebra.isAlgebraic_of_subring_isAlgebraic {R k K : Type*} [CommRing R]
   apply IsAlgebraic.mul (h r)
   exact IsAlgebraic.invLoc (h s)
 
+-- this uses `Algebra.isAlgebraic_of_subring_isAlgebraic` but I think we're going to have
+-- to introduce `f` anyway because we need not just that the extension is algebraic but
+-- that every element satisfies a poly of degree <= |G|.
 theorem algebraic {A : Type*} [CommRing A] {B : Type*} [Nontrivial B] [CommRing B] [Algebra A B]
   [Algebra.IsIntegral A B] {G : Type*} [Group G] [Finite G] [MulSemiringAction G B] (Q : Ideal B)
   [Q.IsPrime] (P : Ideal A) [P.IsPrime] [Algebra (A ⧸ P) (B ⧸ Q)]

blueprint/lean_decls

@@ -62,6 +62,7 @@ AutomorphicForm.GLn.AutomorphicFormForGLnOverQ
 Bourbaki52222.stabilizer.toGaloisGroup
 Bourbaki52222.MulAction.stabilizer_surjective_of_action
 MulSemiringAction.CharacteristicPolynomial.F
+MulSemiringAction.CharacteristicPolynomial.F_degree
 MulSemiringAction.CharacteristicPolynomial.M
 MulSemiringAction.CharacteristicPolynomial.M_eval_eq_zero
 MulSemiringAction.CharacteristicPolynomial.M_deg

blueprint/src/chapter/FrobeniusProject.tex

@@ -19,7 +19,7 @@ \section{Statement of the theorem}
 Note that $G$ naturally acts on the ideals of $B$. Let's define the
 \emph{decomposition group} $D_Q$ of $Q$ to be the subgroup of $G$ which
 stabilizes $Q$ (just to be clear: $g\in D_Q$ means
-$\{g\cdot q\, :\, q \in Q\}=Q$, not $\forall q\in Q, g\cdot q=qs$).
+$\{g\cdot q\, :\, q \in Q\}=Q$, not $\forall q\in Q, g\cdot q=q$).
 
 Let $L$ be the field of fractions of the integral domain $B/Q$, and let $K$ be the
 field of fractions of the subring $A/P$. Then $L$ is naturally a $K$-algebra.
@@ -46,9 +46,9 @@ \section{Statement of the theorem}
   The map $g\mapsto \phi_g$ from $D_Q$ to $\Aut_K(L)$ defined above is surjective.
 \end{theorem}
 
-The goal of this project is to get this theorem into mathlib.
+The goal of this project is to get this theorem formalised and ideally into mathlib.
 
-In particular, $\Aut_K(L)$ is finite, although we prove this along the way and not
+In particular, $\Aut_K(L)$ is finite, although we prove this beforehand and not
 as a corollary. What is so striking about this theorem to me is that the only finiteness hypothesis
 is on the group $G$ which acts; there are no finiteness hypotheses on the rings at all.
 
@@ -89,7 +89,7 @@ \subsection{Examples}
 An example which demonstrates that things can get a bit stranger in characteristic $p$ is the
 following (we restrict to $p=2$ but a generalisation of this pathology exists for all $p>0$).
 We let $B=\mathbb{F}_2[X,Y]$ and $G=\{1,\tau\}$ with the involution $\tau$
-fixing $Y$ and switching $X$, $X+Y$, i.e., $(\tau f)(X,Y)=f(X,X+Y)$.
+fixing $Y$ and switching $X$, $X+Y$, i.e., $(\tau f)(X,Y)=f(X+Y, Y)$.
 Hence $\tau$ fixes the sum and product of these two polynomials, and thus
 $A\supset \mathbb{F}_2[X^2+XY,Y]$. One can check (and this needs checking) that this
 is in fact an equality, and I believe that $B$ is free of
@@ -134,8 +134,21 @@ \section{The extension $B/A$.}
   $F_b(X) \in B[X]$ of $b$ to be $\prod_{g\in G}(X-g\cdot b)$.
 \end{definition}
 
-Clearly $F_b$ is a monic polynomial of degree $|G|$. Note also
-that $F_b$ is $G$-invariant, because acting by some $\gamma\in G$
+Clearly $F_b$ is a monic polynomial of degree $|G|$. In fact this isn't clear:
+if $B$ is the zero ring then $F_b=0$ has degree less than $|G|$.
+
+\begin{lemma}
+  \label{MulSemiringAction.CharacteristicPolynomial.F_degree}
+  \lean{MulSemiringAction.CharacteristicPolynomial.F_degree}
+  \uses{MulSemiringAction.CharacteristicPolynomial.F}
+  \leanok
+  If $B$ is nontrivial then $F_b$ is monic.
+\end{lemma}
+\begin{proof} Obvious.
+\end{proof}
+
+It's also clear that $F_b$ has degree $|G|$ and has $b$ as a root.
+Also $F_b$ is $G$-invariant, because acting by some $\gamma\in G$
 just permutes the order of the factors. Hence we can descend $F_b$
 to a monic polynomial $M_b(X)$ of degree $|G|$ in $A[X]$. We will
 also refer to $M_b$ as the characteristic polynomial of $b$, even though