Merge branch 'main' into auto-update/patch-j21d0pf

Author: pitmonticone

FLT/MathlibExperiments/FrobeniusRiou.lean

@@ -138,16 +138,16 @@ theorem F_monic [Nontrivial B] (b : B) : (F G b).Monic := by
   have := Fintype.ofFinite G
   rw [Monic, F_spec, finprod_eq_prod_of_fintype, leadingCoeff_prod'] <;> simp
 
-variable (G) in
-theorem F_degree (b : B) [Nontrivial B] : (F G b).degree = Nat.card G := by
-  unfold F
-  -- need (∏ᶠ fᵢ).degree = ∑ᶠ (fᵢ.degree)
-  -- then it should be easy
-  sorry
-
 theorem F_natdegree [Nontrivial B] (b : B) : (F G b).natDegree = Nat.card G := by
-  rw [← degree_eq_iff_natDegree_eq_of_pos Nat.card_pos]
-  exact F_degree G b
+  have := Fintype.ofFinite G
+  rw [F_spec, finprod_eq_prod_of_fintype, natDegree_prod_of_monic _ _ (fun _ _ => monic_X_sub_C _)]
+  simp only [natDegree_X_sub_C, Finset.sum_const, Finset.card_univ, Fintype.card_eq_nat_card,
+    nsmul_eq_mul, mul_one, Nat.cast_id]
+
+variable (G) in
+theorem F_degree [Nontrivial B] (b : B) : (F G b).degree = Nat.card G := by
+  have := Fintype.ofFinite G
+  rw [degree_eq_iff_natDegree_eq_of_pos Nat.card_pos, F_natdegree]
 
 theorem F_smul_eq_self (σ : G) (b : B) : σ • (F G b) = F G b := calc
   σ • F G b = σ • ∏ᶠ τ : G, (X - C (τ • b)) := by rw [F_spec]
@@ -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,26 +241,28 @@ theorem M_coeff_card (b : B) :
   · intro d _ hd
     exact coeff_monomial_of_ne (splitting_of_full hFull ((F G b).coeff d)) hd
 
-theorem M_deg_eq_F_deg (b : B) : (M hFull b).degree = (F G b).degree := by
+-- **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)
-  -- hopefully not too hard from previous two lemmas
-  sorry
+  rw [F_degree]
+  have := M_coeff_card hFull b
+  refine le_degree_of_ne_zero ?h
+  rw [this]
+  exact one_ne_zero
 
-theorem M_deg (b : B) : (M hFull b).degree = Nat.card G := by
+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
   have this3 : 0 < Nat.card G := Nat.card_pos
   rw [← F_natdegree b] at this2 this3
   -- then the hypos say deg(M)<=n, coefficient of X^n is 1 in M
   have this4 : (M hFull b).natDegree ≤ (F G b).natDegree := natDegree_le_natDegree this1
-  clear this1
-  -- Now it's just a logic puzzle. If deg(F)=n>0 then we
-  -- know deg(M)<=n and the coefficient of X^n is 1 in M
-  sorry
+  exact Polynomial.monic_of_natDegree_le_of_coeff_eq_one _ this4 this2
 
 omit [Nontrivial B] in
 theorem M_spec (b : B) : ((M hFull b : A[X]) : B[X]) = F G b := by
@@ -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
@@ -289,11 +294,13 @@ theorem M_spec' (b : B) : (map (algebraMap A B) (M G hFull b)) = F G b :=
   (F_descent_monic hFull b).choose_spec.1
 
 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

@@ -1,4 +1,4 @@
-\chapter{A project: Frobenius elements}
+\chapter{A project: Frobenius elements}\label{Frobenius_project}
 
 \section{Introduction and goal}
 
@@ -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
@@ -161,17 +174,22 @@ \section{The extension $B/A$.}
   \label{MulSemiringAction.CharacteristicPolynomial.M_deg}
   \lean{MulSemiringAction.CharacteristicPolynomial.M_deg}
   \uses{MulSemiringAction.CharacteristicPolynomial.M}
+  \leanok
   $M_b$ has degree $n$.
 \end{lemma}
-\begin{proof} Exercise.
+\begin{proof}
+  \leanok
+  Exercise.
 \end{proof}
 \begin{lemma}
   \lean{MulSemiringAction.CharacteristicPolynomial.M_monic}
   \label{MulSemiringAction.CharacteristicPolynomial.M_monic}
   \uses{MulSemiringAction.CharacteristicPolynomial.M}
+  \leanok
   $M_b$ is monic.
 \end{lemma}
 \begin{proof}
+  \leanok
   Exercise.
 \end{proof}