Merge branch 'main' of github.com:ImperialCollegeLondon/FLT into main

Author: kbuzzard

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

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,33 @@ 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)⁻¹]
+
+-- 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
 -- assuming B/Q is finite and P is maximal.