From daeb3a9e5aa8e766d61a74c9699a452a55e5ea58 Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Mon, 9 Sep 2024 18:41:14 +0100
Subject: [PATCH 1/5] Define new localizated rings and immediately run into
 diamond trouble

---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 83 ++++++++++++++++++++---
 1 file changed, 74 insertions(+), 9 deletions(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index 3a4371f2..00a49cff 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -1,13 +1,54 @@
--- Frobenius elements following Joel Riou's idea to use a very general lemma
--- from Bourbaki comm alg
--- (Théorème 2 in section 2 of chapter 5 of Bourbaki Alg Comm)
--- (see https://leanprover.zulipchat.com/#narrow/stream/416277-FLT/topic/Outstanding.20Tasks.2C.20V4/near/449562398)
-
-
+/-
+Copyright (c) 2024 Jou Glasheen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jou Glasheen, Amelia Livingston, Jujian Zhang, Kevin Buzzard
+-/
+import Mathlib.FieldTheory.Cardinality
+import Mathlib.RingTheory.DedekindDomain.Ideal
+import Mathlib.RingTheory.Ideal.Pointwise
+import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.RingTheory.Ideal.Pointwise
 import Mathlib.RingTheory.Ideal.Over
 import Mathlib.FieldTheory.Normal
 import Mathlib
+import Mathlib.RingTheory.OreLocalization.Ring
+
+/-!
+
+# Frobenius elements.
+
+This file proves a general result in commutative algebra which can be used to define Frobenius
+elements of Galois groups of local or fields (for example number fields).
+
+KB was alerted to this very general result (which needs no Noetherian or finiteness assumptions
+on the rings, just on the Galois group) by Joel Riou
+here https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Uses.20of.20Frobenius.20elements.20in.20mathematics/near/448934112
+
+## Mathematical details
+
+### The general commutative algebra result
+
+This is Theorem 2 in Chapter V, Section 2, number 2 of Bourbaki Alg Comm. It says the following.
+Let `A → B` be commutative rings and let `G` be a finite group acting on `B` by ring automorphisms,
+such that the `G`-invariants of `B` are exactly the image of `A`.
+
+The two claims of the theorem are:
+(i) If `P` is a prime ideal of `A` then `G` acts transitively on the primes of `B` above `P`.
+(ii) If `Q` is a prime ideal of `B` lying over `P` then the canonica map from the stabilizer of `Q`
+in `G` to the automorphism group of the residue field extension `Frac(B/Q) / Frac(A/P)` is
+surjective.
+
+We say "automorphism group" rather than "Galois group" because the extension might not be
+separable (it is algebraic and normal however, but it can be infinite; however its maximal
+separable subextension is finite).
+
+This result means that if the inertia group I_Q is trivial and the residue fields are finite,
+there's a Frobenius element Frob_Q in the stabiliser of Q, and a Frobenius conjugacy class
+Frob_P in G.
+
+-/
+
 
 variable {A : Type*} [CommRing A]
   {B : Type*} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B]
@@ -80,11 +121,11 @@ theorem part_a
 
 end part_a
 
-section normal_elements
+-- section normal_elements
 
-variable (K : Type*) [Field K] {L : Type*} [Field L] [Algebra K L]
+-- variable (K : Type*) [Field K] {L : Type*} [Field L] [Algebra K L]
 
-open Polynomial
+-- open Polynomial
 
 -- I've commented out the next section because ACL suggested
 -- reading up-to-date Bourbaki here https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/poly.20whose.20roots.20are.20the.20products.20of.20the.20roots.20of.20polys/near/468585267
@@ -327,6 +368,30 @@ theorem main_result : Function.Surjective
     (baz2 Q P L K : MulAction.stabilizer G Q → (L ≃ₐ[K] L)) := by
   sorry
 
+section localization
+
+/-
+
+In this section we reduce to the case where P and Q are maximal.
+More precisely, we set `S := A - P` and localize everything in sight by `S`
+We then construct a group isomophism
+`MulAction.stabilizer G Q ≃ MulAction.stabilizer G SQ` where `SQ` is the prime ideal of `S⁻¹B`
+obtained by localizing `Q` at `S`, and show that it commutes with the maps currently called
+`baz2 Q P L K` and `baz2 SQ SP L K`.
+
+-/
+
+abbrev S := P.primeCompl
+abbrev SA := A[(S P)⁻¹]
+
+abbrev SB := B[(S P)⁻¹]
+
+-- didn't work, maybe need to remove irreducibility of smul
+-- instance : Algebra (A[(S P)⁻¹]) (B[(S P)⁻¹]) where
+--   __ := OreLocalization.instModule (R := A) (X := B) (S := P.primeCompl)
+
+
+end localization
 
 -- In Frobenius2.lean in this dir (Jou's FM24 project) there's a proof of surjectivity
 -- assuming B/Q is finite and P is maximal.

From 9358f1dad584887d7bf00f597b31ee44e74e6c1a Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Mon, 9 Sep 2024 19:04:41 +0100
Subject: [PATCH 2/5] fix FLT_files

---
 FLT/FLT_files.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
index 30a35313..c697d35d 100644
--- a/FLT/FLT_files.lean
+++ b/FLT/FLT_files.lean
@@ -3,7 +3,6 @@ import FLT.AutomorphicRepresentation.Example
 import FLT.Basic.Reductions
 import FLT.EllipticCurve.Torsion
 import FLT.ForMathlib.ActionTopology
-import FLT.ForMathlib.FGModuleTopology
 import FLT.ForMathlib.MiscLemmas
 import FLT.GaloisRepresentation.Cyclotomic
 import FLT.GaloisRepresentation.HardlyRamified
@@ -12,6 +11,7 @@ import FLT.GlobalLanglandsConjectures.GLzero
 import FLT.GroupScheme.FiniteFlat
 import FLT.HIMExperiments.ContinuousSMul_topology
 import FLT.HIMExperiments.dual_topology
+import FLT.HIMExperiments.FGModuleTopology
 import FLT.HIMExperiments.flatness
 import FLT.HIMExperiments.module_topology
 import FLT.HIMExperiments.right_module_topology

From 1cea479e99b0e554e174060d7df0a434d15d0d6d Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Mon, 9 Sep 2024 19:16:46 +0100
Subject: [PATCH 3/5] remove lemmas in two more files

---
 FLT/ForMathlib/ActionTopology.lean       | 28 ++++++++++-----------
 FLT/HIMExperiments/FGModuleTopology.lean | 32 ++++++++++++------------
 2 files changed, 30 insertions(+), 30 deletions(-)

diff --git a/FLT/ForMathlib/ActionTopology.lean b/FLT/ForMathlib/ActionTopology.lean
index c0ec7e7e..4476fbfb 100644
--- a/FLT/ForMathlib/ActionTopology.lean
+++ b/FLT/ForMathlib/ActionTopology.lean
@@ -95,13 +95,13 @@ the action topology. See `actionTopology` for more discussion of the action topo
 class IsActionTopology [τA : TopologicalSpace A] : Prop where
   isActionTopology' : τA = actionTopology R A
 
-lemma isActionTopology [τA : TopologicalSpace A] [IsActionTopology R A] :
+theorem isActionTopology [τA : TopologicalSpace A] [IsActionTopology R A] :
     τA = actionTopology R A :=
   IsActionTopology.isActionTopology' (R := R) (A := A)
 
 /-- Scalar multiplication `• : R × A → A` is continuous if `R` is a topological
 ring, and `A` is an `R` module with the action topology. -/
-lemma ActionTopology.continuousSMul : @ContinuousSMul R A _ _ (actionTopology R A) :=
+theorem ActionTopology.continuousSMul : @ContinuousSMul R A _ _ (actionTopology R A) :=
   -- Proof: We need to prove that the product topology is finer than the pullback
   -- of the action topology. But the action topology is an Inf and thus a limit,
   -- and pullback is a right adjoint, so it preserves limits.
@@ -112,16 +112,16 @@ lemma ActionTopology.continuousSMul : @ContinuousSMul R A _ _ (actionTopology R
 
 /-- Addition `+ : A × A → A` is continuous if `R` is a topological
 ring, and `A` is an `R` module with the action topology. -/
-lemma ActionTopology.continuousAdd : @ContinuousAdd A (actionTopology R A) _ :=
+theorem ActionTopology.continuousAdd : @ContinuousAdd A (actionTopology R A) _ :=
   continuousAdd_sInf <| fun _ _ ↦ by simp_all only [Set.mem_setOf_eq]
 
 instance instIsActionTopology_continuousSMul [TopologicalSpace A] [IsActionTopology R A] :
     ContinuousSMul R A := isActionTopology R A ▸ ActionTopology.continuousSMul R A
 
-lemma isActionTopology_continuousAdd [TopologicalSpace A] [IsActionTopology R A] :
+theorem isActionTopology_continuousAdd [TopologicalSpace A] [IsActionTopology R A] :
     ContinuousAdd A := isActionTopology R A ▸ ActionTopology.continuousAdd R A
 
-lemma actionTopology_le [τA : TopologicalSpace A] [ContinuousSMul R A] [ContinuousAdd A] :
+theorem actionTopology_le [τA : TopologicalSpace A] [ContinuousSMul R A] [ContinuousAdd A] :
     actionTopology R A ≤ τA := sInf_le ⟨‹ContinuousSMul R A›, ‹ContinuousAdd A›⟩
 
 end basics
@@ -195,7 +195,7 @@ variable {B : Type*} [AddCommMonoid B] [Module R B] [τB : TopologicalSpace B]
 -- this is horrible. Why isn't it easy?
 -- One reason: we are rolling our own continuous linear equivs!
 -- **TODO** Ask about making continuous linear equivs properly
-lemma iso (ehomeo : A ≃ₜ B) (elinear : A ≃ₗ[R] B) (he : ∀ a, ehomeo a = elinear a) :
+theorem iso (ehomeo : A ≃ₜ B) (elinear : A ≃ₗ[R] B) (he : ∀ a, ehomeo a = elinear a) :
     IsActionTopology R B where
   isActionTopology' := by
     simp_rw [ehomeo.symm.inducing.1, isActionTopology R A, actionTopology, induced_sInf]
@@ -237,7 +237,7 @@ variable {B : Type*} [AddCommMonoid B] [Module R B] [aB : TopologicalSpace B] [I
 
 /-- Every `R`-linear map between two `R`-modules with the canonical topology is continuous. -/
 @[fun_prop, continuity]
-lemma continuous_of_distribMulActionHom (φ : A →+[R] B) : Continuous φ := by
+theorem continuous_of_distribMulActionHom (φ : A →+[R] B) : Continuous φ := by
   -- the proof: We know that `+ : B × B → B` and `• : R × B → B` are continuous for the action
   -- topology on `B`, and two earlier theorems (`induced_continuous_smul` and
   -- `induced_continuous_add`) say that hence `+` and `•` on `A` are continuous if `A`
@@ -249,11 +249,11 @@ lemma continuous_of_distribMulActionHom (φ : A →+[R] B) : Continuous φ := by
     induced_continuous_add φ.toAddMonoidHom⟩
 
 @[fun_prop, continuity]
-lemma continuous_of_linearMap (φ : A →ₗ[R] B) : Continuous φ :=
+theorem continuous_of_linearMap (φ : A →ₗ[R] B) : Continuous φ :=
   continuous_of_distribMulActionHom φ.toDistribMulActionHom
 
 variable (R) in
-lemma continuous_neg (C : Type*) [AddCommGroup C] [Module R C] [TopologicalSpace C]
+theorem continuous_neg (C : Type*) [AddCommGroup C] [Module R C] [TopologicalSpace C]
     [IsActionTopology R C] : Continuous (fun a ↦ -a : C → C) :=
   continuous_of_linearMap (LinearEquiv.neg R).toLinearMap
 
@@ -267,7 +267,7 @@ variable {B : Type*} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [Is
 
 -- Here I need the lemma about how quotients are open so I do need groups
 -- because this relies on translates of an open being open
-lemma coinduced_of_surjective {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) :
+theorem coinduced_of_surjective {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) :
     TopologicalSpace.coinduced φ (actionTopology R A) = actionTopology R B := by
   have : Continuous φ := continuous_of_linearMap φ
   rw [continuous_iff_coinduced_le, isActionTopology R A, isActionTopology R B] at this
@@ -401,7 +401,7 @@ variable {A : Type*} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [Is
 variable {B : Type*} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [IsActionTopology R B]
 variable {C : Type*} [AddCommGroup C] [Module R C] [aC : TopologicalSpace C] [IsActionTopology R C]
 
-lemma Module.continuous_bilinear_of_pi_finite (ι : Type*) [Finite ι]
+theorem Module.continuous_bilinear_of_pi_finite (ι : Type*) [Finite ι]
     (bil : (ι → R) →ₗ[R] B →ₗ[R] C) : Continuous (fun ab ↦ bil ab.1 ab.2 : ((ι → R) × B → C)) := by
   classical
   have foo : (fun fb ↦ bil fb.1 fb.2 : ((ι → R) × B → C)) =
@@ -431,7 +431,7 @@ lemma Module.continuous_bilinear_of_pi_finite (ι : Type*) [Finite ι]
   simp [Set.toFinite _]
 
 -- Probably this can be beefed up to semirings.
-lemma Module.continuous_bilinear_of_finite_free [TopologicalSemiring R] [Module.Finite R A] [Module.Free R A]
+theorem Module.continuous_bilinear_of_finite_free [TopologicalSemiring R] [Module.Finite R A] [Module.Free R A]
     (bil : A →ₗ[R] B →ₗ[R] C) : Continuous (fun ab ↦ bil ab.1 ab.2 : (A × B → C)) := by
   let ι := Module.Free.ChooseBasisIndex R A
   let hι : Fintype ι := Module.Free.ChooseBasisIndex.fintype R A
@@ -460,7 +460,7 @@ variable {B : Type*} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [Is
 variable {C : Type*} [AddCommGroup C] [Module R C] [aC : TopologicalSpace C] [IsActionTopology R C]
 
 -- This needs rings though
-lemma Module.continuous_bilinear_of_finite [Module.Finite R A]
+theorem Module.continuous_bilinear_of_finite [Module.Finite R A]
     (bil : A →ₗ[R] B →ₗ[R] C) : Continuous (fun ab ↦ bil ab.1 ab.2 : (A × B → C)) := by
   obtain ⟨m, f, hf⟩ := Module.Finite.exists_fin' R A
   let bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil.comp f
@@ -494,7 +494,7 @@ variable [TopologicalSpace D] [IsActionTopology R D]
 open scoped TensorProduct
 
 @[continuity, fun_prop]
-lemma continuous_mul'
+theorem continuous_mul'
     (R) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
     (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D] [Module.Free R D] [TopologicalSpace D]
     [IsActionTopology R D]: Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) := by
diff --git a/FLT/HIMExperiments/FGModuleTopology.lean b/FLT/HIMExperiments/FGModuleTopology.lean
index b17ac8d8..2e13c380 100644
--- a/FLT/HIMExperiments/FGModuleTopology.lean
+++ b/FLT/HIMExperiments/FGModuleTopology.lean
@@ -50,7 +50,7 @@ class IsModuleTopology [τA : TopologicalSpace A] : Prop where
 
 -- because default binders for isModuleTopology' are wrong and currently
 -- there is no way to change this. There's a Lean 4 issue for this IIRC **TODO** where?
-lemma isModuleTopology [τA : TopologicalSpace A] [IsModuleTopology R A] :
+theorem isModuleTopology [τA : TopologicalSpace A] [IsModuleTopology R A] :
     τA = moduleTopology R A :=
   IsModuleTopology.isModuleTopology' (R := R) (A := A)
 
@@ -88,14 +88,14 @@ variable {B : Type*} [AddCommMonoid B] [Module R B] [aB : TopologicalSpace B] [I
 
 /-- Every `A`-linear map between two `A`-modules with the canonical topology is continuous. -/
 @[continuity, fun_prop]
-lemma continuous_of_linearMap (f : A →ₗ[R] B) : Continuous f := by
+theorem continuous_of_linearMap (f : A →ₗ[R] B) : Continuous f := by
   rw [isModuleTopology R A, isModuleTopology R B, continuous_iff_le_induced]
   apply iSup_le <| fun n ↦ iSup_le <| fun φ ↦ ?_
   rw [← coinduced_le_iff_le_induced, coinduced_compose]
   exact le_iSup_of_le n <| le_iSup_of_le (f.comp φ) le_rfl
 
 -- should this be in the API?
-lemma continuous_of_linearMap' {A : Type*} [AddCommMonoid A] [Module R A]
+theorem continuous_of_linearMap' {A : Type*} [AddCommMonoid A] [Module R A]
     {B : Type*} [AddCommMonoid B] [Module R B] (f : A →ₗ[R] B) :
     @Continuous _ _ (moduleTopology R A) (moduleTopology R B) f := by
   letI : TopologicalSpace A := moduleTopology R A
@@ -133,7 +133,7 @@ end linear_map
 
 section continuous_neg
 
-lemma continuous_neg
+theorem continuous_neg
     (R : Type*) [TopologicalSpace R] [Ring R]
     (A : Type*) [AddCommGroup A] [Module R A] [TopologicalSpace A] [IsModuleTopology R A] :
     Continuous (-· : A → A) :=
@@ -146,7 +146,7 @@ section surj
 variable {R : Type*} [τR : TopologicalSpace R] [Semiring R] [TopologicalSemiring R]
 variable {A : Type*} [AddCommMonoid A] [Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A]
 
-lemma coinduced_of_surjectivePiFin {n : ℕ} {φ : ((Fin n) → R) →ₗ[R] A} (hφ : Function.Surjective φ) :
+theorem coinduced_of_surjectivePiFin {n : ℕ} {φ : ((Fin n) → R) →ₗ[R] A} (hφ : Function.Surjective φ) :
     TopologicalSpace.coinduced φ Pi.topologicalSpace = moduleTopology R A := by
   apply le_antisymm
   · rw [← continuous_iff_coinduced_le, ← isModuleTopology R A]
@@ -161,7 +161,7 @@ lemma coinduced_of_surjectivePiFin {n : ℕ} {φ : ((Fin n) → R) →ₗ[R] A}
     exact continuous_of_linearMap α
 
 /-- Any surjection between finite R-modules is coinducing for the R-module topology. -/
-lemma coinduced_of_surjective {B : Type*} [AddCommMonoid B] [aB : TopologicalSpace B] [Module R B]
+theorem coinduced_of_surjective {B : Type*} [AddCommMonoid B] [aB : TopologicalSpace B] [Module R B]
     [IsModuleTopology R B] [Module.Finite R A] {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) :
     TopologicalSpace.coinduced φ (moduleTopology R A) = moduleTopology R B := by
   obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R A
@@ -173,7 +173,7 @@ lemma coinduced_of_surjective {B : Type*} [AddCommMonoid B] [aB : TopologicalSpa
 
 -- do I need this? Yes, I need (fin n) × fin m -> R
 -- **^TODO** why didn't have/let linter warn me
-lemma coinduced_of_surjectivePiFinite {ι : Type*} [Finite ι] {φ : (ι → R) →ₗ[R] A}
+theorem coinduced_of_surjectivePiFinite {ι : Type*} [Finite ι] {φ : (ι → R) →ₗ[R] A}
     (hφ : Function.Surjective φ) :
     TopologicalSpace.coinduced φ Pi.topologicalSpace = moduleTopology R A := by
   rw [(instPiFinite R ι).isModuleTopology']
@@ -188,7 +188,7 @@ variable {A : Type*} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [Is
 
 variable (R A) in
 @[continuity, fun_prop]
-lemma continuous_add [Module.Finite R A] : Continuous (fun ab ↦ ab.1 + ab.2 : A × A → A) := by
+theorem continuous_add [Module.Finite R A] : Continuous (fun ab ↦ ab.1 + ab.2 : A × A → A) := by
   rw [continuous_iff_coinduced_le, isModuleTopology R A]
   obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R A
   rw [← coinduced_of_surjectivePiFin hf]
@@ -213,7 +213,7 @@ lemma continuous_add [Module.Finite R A] : Continuous (fun ab ↦ ab.1 + ab.2 :
 
 variable (R A) in
 @[continuity, fun_prop]
-lemma continuous_sum_finset (ι : Type*) [DecidableEq ι] (s : Finset ι) [Module.Finite R A] :
+theorem continuous_sum_finset (ι : Type*) [DecidableEq ι] (s : Finset ι) [Module.Finite R A] :
     Continuous (fun as ↦ ∑ i ∈ s, as i : (∀ (_ : ι), A) → A) := by
   induction s using Finset.induction
   · simp only [Finset.sum_empty]
@@ -227,7 +227,7 @@ lemma continuous_sum_finset (ι : Type*) [DecidableEq ι] (s : Finset ι) [Modul
 attribute [local instance] Fintype.ofFinite
 variable (R A) in
 @[continuity, fun_prop]
-lemma continuous_sum_finite (ι : Type*) [Finite ι] [Module.Finite R A] :
+theorem continuous_sum_finite (ι : Type*) [Finite ι] [Module.Finite R A] :
     Continuous (fun as ↦ ∑ i, as i : (∀ (_ : ι), A) → A) := by
   classical
   exact continuous_sum_finset R A ι _
@@ -316,7 +316,7 @@ noncomputable def isom'' (R : Type*) [CommRing R] (m n : Type*) [Finite m] [Deci
 
 variable (m n : Type*) [Finite m] [DecidableEq m] (a1 : m → R)
     (b1 : n → R) (f : (m → R) →ₗ[R] A) (g : (n → R) →ₗ[R] B) in
-lemma key : ((TensorProduct.map f g ∘ₗ
+theorem key : ((TensorProduct.map f g ∘ₗ
     (isom'' R m n).symm.toLinearMap) fun mn ↦ a1 mn.1 * b1 mn.2) = f a1 ⊗ₜ[R] g b1 := by
   sorry
 
@@ -336,7 +336,7 @@ lemma key : ((TensorProduct.map f g ∘ₗ
 -- I don't know whether finiteness is needed on `B` here. Removing it here would enable
 -- removal in `continuous_bilinear`.
 @[continuity, fun_prop]
-lemma Module.continuous_tprod [Module.Finite R A] [Module.Finite R B] :
+theorem Module.continuous_tprod [Module.Finite R A] [Module.Finite R B] :
     Continuous (fun (ab : A × B) ↦ ab.1 ⊗ₜ ab.2 : A × B → A ⊗[R] B) := by
   -- reduce to R^m x R^n -> R^m ⊗ R^n
   -- then check explicitly
@@ -377,7 +377,7 @@ lemma Module.continuous_tprod [Module.Finite R A] [Module.Finite R B] :
     rfl
 
 -- did I really use finiteness of B?
-lemma Module.continuous_bilinear [Module.Finite R A] [Module.Finite R B]
+theorem Module.continuous_bilinear [Module.Finite R A] [Module.Finite R B]
     {C : Type*} [AddCommGroup C] [Module R C] [TopologicalSpace C] [IsModuleTopology R C]
     (bil : A →ₗ[R] B →ₗ[R] C) : Continuous (fun ab ↦ bil ab.1 ab.2 : (A × B → C)) := by
   letI : TopologicalSpace (A ⊗[R] B) := moduleTopology R _
@@ -390,7 +390,7 @@ variable (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D]
 variable [TopologicalSpace D] [IsModuleTopology R D]
 
 @[continuity, fun_prop]
-lemma continuous_mul (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D] [TopologicalSpace D]
+theorem continuous_mul (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D] [TopologicalSpace D]
     [IsModuleTopology R D] : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) := by
   letI : TopologicalSpace (D ⊗[R] D) := moduleTopology R _
   haveI : IsModuleTopology R (D ⊗[R] D) := { isModuleTopology' := rfl }
@@ -403,7 +403,7 @@ def Module.topologicalRing : TopologicalRing D where
 
 end commutative
 
-lemma continuousSMul (R : Type*) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
+theorem continuousSMul (R : Type*) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
     (A : Type*) [AddCommGroup A] [Module R A] [Module.Finite R A] [TopologicalSpace A]
     [IsModuleTopology R A] :
     ContinuousSMul R A := by
@@ -420,7 +420,7 @@ I can only prove that `SMul : R × A → A` is continuous for the module topolog
 commutative (because my proof uses tensor products) and if `A` is finite (because
 I reduce to a basis check ). Is it true in general? I'm assuming not.
 
-lemma continuousSMul (R : Type*) [Ring R] [TopologicalSpace R] [TopologicalRing R]
+theorem continuousSMul (R : Type*) [Ring R] [TopologicalSpace R] [TopologicalRing R]
     (A : Type*) [AddCommGroup A] [Module R A] : @ContinuousSMul R A _ _ (moduleTopology R A) := by
   refine @ContinuousSMul.mk ?_ ?_ ?_ ?_ ?_ ?_
   haveI : IsModuleTopology R R := inferInstance

From 6f33c8dcc52c3155f505b34d95f4431bbf09dcaf Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Mon, 9 Sep 2024 19:31:45 +0100
Subject: [PATCH 4/5] final tidy-ups

---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index 00a49cff..50bee89f 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -13,6 +13,7 @@ import Mathlib.RingTheory.Ideal.Over
 import Mathlib.FieldTheory.Normal
 import Mathlib
 import Mathlib.RingTheory.OreLocalization.Ring
+import FLT.ForMathlib.Algebra
 
 /-!
 
@@ -386,11 +387,14 @@ abbrev SA := A[(S P)⁻¹]
 
 abbrev SB := B[(S P)⁻¹]
 
--- didn't work, maybe need to remove irreducibility of smul
--- instance : Algebra (A[(S P)⁻¹]) (B[(S P)⁻¹]) where
---   __ := OreLocalization.instModule (R := A) (X := B) (S := P.primeCompl)
-
+-- Currently stuck here
+--instance : Algebra (A[(S P)⁻¹]) (B[(S P)⁻¹]) where
+--  sorry--__ := OreLocalization.instModule (R := A) (X := B) (S := P.primeCompl)
 
+/-
+failed to synthesize
+  Semiring (OreLocalization (S P) B)
+-/
 end localization
 
 -- In Frobenius2.lean in this dir (Jou's FM24 project) there's a proof of surjectivity

From c3a40783fdf00982db61359370cf019e17345d5c Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Mon, 9 Sep 2024 19:35:04 +0100
Subject: [PATCH 5/5] don't need the ore localization algebra import yet, move
 elsewhere

---
 FLT/MathlibExperiments/FrobeniusRiou.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index 50bee89f..87f5eb98 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -13,7 +13,6 @@ import Mathlib.RingTheory.Ideal.Over
 import Mathlib.FieldTheory.Normal
 import Mathlib
 import Mathlib.RingTheory.OreLocalization.Ring
-import FLT.ForMathlib.Algebra
 
 /-!