From 8e6d79b4873ef93b2e7603f7977c36db7e15de3f Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Tue, 1 Oct 2024 11:30:43 +0200
Subject: [PATCH 1/2] Prove F_degree, M_deg_eq_F_deg, M_monic

Fixes #141
---
 FLT/MathlibExperiments/FrobeniusRiou.lean  | 53 ++++++++++++----------
 blueprint/src/chapter/FrobeniusProject.tex |  7 ++-
 2 files changed, 34 insertions(+), 26 deletions(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index 2454306b..d170cf5f 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -139,13 +139,13 @@ theorem F_monic [Nontrivial B] (b : B) : (F G b).Monic := by
   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_degree [Nontrivial B] [NoZeroDivisors B] (b : B) : (F G b).degree = Nat.card G := by
+  have := Fintype.ofFinite G
+  rw [F_spec, finprod_eq_prod_of_fintype, Polynomial.degree_prod]
+  simp only [degree_X_sub_C, Finset.sum_const, Finset.card_univ, Fintype.card_eq_nat_card,
+    nsmul_eq_mul, mul_one]
 
-theorem F_natdegree [Nontrivial B] (b : B) : (F G b).natDegree = Nat.card G := by
+theorem F_natdegree [Nontrivial B] [NoZeroDivisors 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
 
@@ -220,7 +220,8 @@ theorem M_deg_le (b : B) : (M hFull b).degree ≤ (F G b).degree := by
   apply le_trans (degree_monomial_le n _) ?_
   exact le_degree_of_mem_supp n hn
 
-variable [Nontrivial B] [Finite G]
+section
+variable [Nontrivial B] [NoZeroDivisors B] [Finite G]
 
 theorem M_coeff_card (b : B) :
     (M hFull b).coeff (Nat.card G) = 1 := by
@@ -242,12 +243,15 @@ theorem M_coeff_card (b : B) :
     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
+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
 
@@ -259,12 +263,11 @@ theorem M_monic (b : B) : (M hFull b).Monic := by
   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
+end
+
+variable [Finite G]
 
-omit [Nontrivial B] in
 theorem M_spec (b : B) : ((M hFull b : A[X]) : B[X]) = F G b := by
   unfold M
   ext N
@@ -294,18 +297,16 @@ 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]
 
 include hFull in
-theorem isIntegral : Algebra.IsIntegral A B where
+theorem isIntegral [Nontrivial B] [NoZeroDivisors B] : Algebra.IsIntegral A B where
   isIntegral b := ⟨M hFull b, M_monic hFull b, M_eval_eq_zero hFull b⟩
 
 end full_descent
@@ -322,7 +323,8 @@ variable {A : Type*} [CommRing A]
   {B : Type*} [CommRing B] [Algebra A B] [Nontrivial B]
   {G : Type*} [Group G] [Finite G] [MulSemiringAction G B]
 
-theorem isIntegral_of_Full (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) :
+theorem isIntegral_of_Full [NoZeroDivisors B]
+    (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) :
     Algebra.IsIntegral A B where
   isIntegral b := ⟨M hFull b, M_monic hFull b, M_eval_eq_zero hFull b⟩
 
@@ -341,8 +343,8 @@ 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]
+omit [Nontrivial B] in
+theorem part_a [SMulCommClass G A B] [NoZeroDivisors 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) :
     ∃ g : G, Q = g • P := by
@@ -710,8 +712,9 @@ theorem Algebra.isAlgebraic_of_subring_isAlgebraic {R k K : Type*} [CommRing R]
 -- 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)
+theorem algebraic {A : Type*} [CommRing A] {B : Type*} [Nontrivial B] [CommRing B]
+  [NoZeroDivisors 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)]
   [IsScalarTower A (A ⧸ P) (B ⧸ Q)] (L : Type*) [Field L] [Algebra (B ⧸ Q) L]
   [IsFractionRing (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L]
diff --git a/blueprint/src/chapter/FrobeniusProject.tex b/blueprint/src/chapter/FrobeniusProject.tex
index ab72589b..58f24e32 100644
--- a/blueprint/src/chapter/FrobeniusProject.tex
+++ b/blueprint/src/chapter/FrobeniusProject.tex
@@ -174,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}
 

From 03c3f5d363ba124e2b64d1f4617568dc6ece3257 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Tue, 1 Oct 2024 13:36:23 +0200
Subject: [PATCH 2/2] generalize

---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 39 +++++++++++------------
 1 file changed, 18 insertions(+), 21 deletions(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index d170cf5f..d71950c2 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/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 [Nontrivial B] [NoZeroDivisors B] (b : B) : (F G b).degree = Nat.card G := by
+theorem F_natdegree [Nontrivial B] (b : B) : (F G b).natDegree = Nat.card G := by
   have := Fintype.ofFinite G
-  rw [F_spec, finprod_eq_prod_of_fintype, Polynomial.degree_prod]
-  simp only [degree_X_sub_C, Finset.sum_const, Finset.card_univ, Fintype.card_eq_nat_card,
-    nsmul_eq_mul, mul_one]
+  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]
 
-theorem F_natdegree [Nontrivial B] [NoZeroDivisors 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
+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]
@@ -220,8 +220,7 @@ theorem M_deg_le (b : B) : (M hFull b).degree ≤ (F G b).degree := by
   apply le_trans (degree_monomial_le n _) ?_
   exact le_degree_of_mem_supp n hn
 
-section
-variable [Nontrivial B] [NoZeroDivisors B] [Finite G]
+variable [Nontrivial B] [Finite G]
 
 theorem M_coeff_card (b : B) :
     (M hFull b).coeff (Nat.card G) = 1 := by
@@ -264,10 +263,8 @@ theorem M_monic (b : B) : (M hFull b).Monic := by
   -- 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
   exact Polynomial.monic_of_natDegree_le_of_coeff_eq_one _ this4 this2
-end
-
-variable [Finite G]
 
+omit [Nontrivial B] in
 theorem M_spec (b : B) : ((M hFull b : A[X]) : B[X]) = F G b := by
   unfold M
   ext N
@@ -299,14 +296,16 @@ 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]
 
 include hFull in
-theorem isIntegral [Nontrivial B] [NoZeroDivisors B] : Algebra.IsIntegral A B where
+theorem isIntegral : Algebra.IsIntegral A B where
   isIntegral b := ⟨M hFull b, M_monic hFull b, M_eval_eq_zero hFull b⟩
 
 end full_descent
@@ -323,8 +322,7 @@ variable {A : Type*} [CommRing A]
   {B : Type*} [CommRing B] [Algebra A B] [Nontrivial B]
   {G : Type*} [Group G] [Finite G] [MulSemiringAction G B]
 
-theorem isIntegral_of_Full [NoZeroDivisors B]
-    (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) :
+theorem isIntegral_of_Full (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) :
     Algebra.IsIntegral A B where
   isIntegral b := ⟨M hFull b, M_monic hFull b, M_eval_eq_zero hFull b⟩
 
@@ -343,8 +341,8 @@ 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] [NoZeroDivisors B]
+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) :
     ∃ g : G, Q = g • P := by
@@ -712,9 +710,8 @@ theorem Algebra.isAlgebraic_of_subring_isAlgebraic {R k K : Type*} [CommRing R]
 -- 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]
-  [NoZeroDivisors B] [Algebra A B] [Algebra.IsIntegral A B]
-  {G : Type*} [Group G] [Finite G] [MulSemiringAction G B] (Q : Ideal B)
+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)]
   [IsScalarTower A (A ⧸ P) (B ⧸ Q)] (L : Type*) [Field L] [Algebra (B ⧸ Q) L]
   [IsFractionRing (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L]