Merge pull request #135 from ImperialCollegeLondon/kbuzzard-frobenius2

Some Frobenius, some action topology

FLT/AutomorphicForm/QuaternionAlgebra.lean

@@ -53,11 +53,13 @@ instance [Module.Free R D]  : Module.Free A (D ⊗[R] A) := sorry
 -- #synth Ring (D ⊗[F] FiniteAdeleRing (𝓞 F) F)
 
 end missing_instances
--- your work
+
 instance : TopologicalSpace (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) := actionTopology (FiniteAdeleRing (𝓞 F) F) _
 instance : IsActionTopology (FiniteAdeleRing (𝓞 F) F) (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) := ⟨rfl⟩
 instance : TopologicalRing (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) :=
-  ActionTopology.Module.topologicalRing (FiniteAdeleRing (𝓞 F) F) _--moobar (FiniteAdeleRing (𝓞 F) F) (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))
+  -- this def would be a dangerous instance
+  -- (it can't guess R) but it's just a Prop so we can easily add it here
+  ActionTopology.Module.topologicalRing (FiniteAdeleRing (𝓞 F) F) _
 
 namespace TotallyDefiniteQuaternionAlgebra
 

FLT/ForMathlib/ActionTopology.lean

@@ -523,10 +523,10 @@ open scoped TensorProduct
 
 @[continuity, fun_prop]
 theorem continuous_mul'
-    (R) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
+    (R : Type*) [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) :=
-  Module.continuous_bilinear_of_finite (LinearMap.mul R D : D →ₗ[R] D →ₗ[R] D)
+    [IsActionTopology R D] : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) :=
+  Module.continuous_bilinear_of_finite (LinearMap.mul R D)
 
 def topologicalSemiring : TopologicalSemiring D where
   continuous_add := (isActionTopology_continuousAdd R D).1
@@ -536,7 +536,8 @@ end semiring_algebra
 
 section ring_algebra
 
--- these shouldn't be rings, they should be semirings
+-- confusion about whether these are rings or semirings should ideally be resolved
+-- Is it: for D finite free R can be a semiring but for D finite it has to be a ring?
 variable (R) [CommRing R] [TopologicalSpace R] [TopologicalRing R]
 variable (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D]
 variable [TopologicalSpace D] [IsActionTopology R D]

FLT/MathlibExperiments/FrobeniusRiou.lean

@@ -51,37 +51,161 @@ Frob_P in G.
 
 
 variable {A : Type*} [CommRing A]
-  {B : Type*} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B]
+  {B : Type*} [CommRing B] [Algebra A B] --[Algebra.IsIntegral A B]
   {G : Type*} [Group G] [Finite G] [MulSemiringAction G B]
 
+
+
 open scoped algebraMap
 
-variable (hGalois : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ a : A, b = a)
+--variable (hFull : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ a : A, b = a)
+--variable (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a)
 
-section part_a
+section misc
 
-variable (P Q : Ideal B) [P.IsPrime] [Q.IsPrime]
-  (hPQ : Ideal.comap (algebraMap A B) P = Ideal.comap (algebraMap A B) Q)
+variable {A : Type*} [CommRing A]
+  {B : Type*} [CommRing B] [Algebra A B]
+  {G : Type*} [Group G] [MulSemiringAction G B]
+  [SMulCommClass G A B]
 
 open scoped Pointwise
 
-private theorem norm_fixed (b : B) (g : G) : g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, σ • b := calc
+/-
+If you're happy to stick to finite G, it's just this:
+
+private theorem norm_fixed' (b : B) (g : G) [Finite G] : g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, σ • b := calc
   g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, g • (σ • b) := smul_finprod' _
   _                     = ∏ᶠ σ : G, σ • b := finprod_eq_of_bijective (g • ·) (MulAction.bijective g)
                                                fun x ↦ smul_smul g x b
 
+But the below proof works in general.
+-/
+
+private theorem norm_fixed (b : B) (g : G) : g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, σ • b := by
+  obtain (hfin | hinf) := em <| Finite G
+  · calc
+    g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, g • (σ • b) := smul_finprod' _
+    _                     = ∏ᶠ σ : G, σ • b := finprod_eq_of_bijective (g • ·) (MulAction.bijective g)
+                                                 fun x ↦ smul_smul g x b
+  · obtain (rfl | hb) := eq_or_ne b 1
+    · simp
+    · suffices (Function.mulSupport ((· • b) : G → B)).Infinite by
+        classical
+        simp [finprod_def, dif_neg this]
+      have htop : (⊤ : Set G).Infinite := by simpa using Set.infinite_univ_iff.mpr ({ not_finite := hinf })
+      convert htop
+      rw [eq_top_iff]
+      intro g _
+      simp only [Function.mem_mulSupport]
+      contrapose! hb
+      apply_fun (fun x ↦ g⁻¹ • x) at hb
+      simpa using hb
+
 theorem _root_.Ideal.IsPrime.finprod_mem_iff_exists_mem {R S : Type*} [Finite R] [CommSemiring S]
     (I : Ideal S) [hI : I.IsPrime] (f : R → S)  :
     ∏ᶠ x, f x ∈ I ↔ ∃ p, f p ∈ I := by
   have := Fintype.ofFinite R
   rw [finprod_eq_prod_of_fintype, Finset.prod_eq_multiset_prod, hI.multiset_prod_mem_iff_exists_mem]
   simp
 
+end misc
+
+section charpoly
+
+open Polynomial BigOperators
+
+variable {A : Type*} [CommRing A]
+  {B : Type*} [CommRing B] [Algebra A B]
+  {G : Type*} [Group G] [MulSemiringAction G B] --[SMulCommClass G A B]
+
+
+variable (G) in
+/-- `F : B[X]` defined to be a product of linear factors `(X - τ • α)`; where
+`τ` runs over `L ≃ₐ[K] L`, and `α : B` is an element which generates `(B ⧸ Q)ˣ`
+and lies in `τ • Q` for all `τ ∉ (decomposition_subgroup_Ideal'  A K L B Q)`.-/
+private noncomputable abbrev F (b : B) : B[X] := ∏ᶠ τ : G, (X - C (τ • b))
+
+private theorem F_spec (b : B) : F G b = ∏ᶠ τ : G, (X - C (τ • b)) := rfl
+
+private theorem F_smul_eq_self [Finite G] (σ : G) (b : B) : σ • (F G b) = F G b := calc
+  σ • F G b = σ • ∏ᶠ τ : G, (X - C (τ • b)) := by rw [F_spec]
+  _         = ∏ᶠ τ : G, σ • (X - C (τ • b)) := smul_finprod' _
+  _         = ∏ᶠ τ : G, (X - C ((σ * τ) • b)) := by simp [smul_sub, smul_smul]
+  _         = ∏ᶠ τ' : G, (X - C (τ' • b)) := finprod_eq_of_bijective (fun τ ↦ σ * τ)
+                                               (Group.mulLeft_bijective σ) (fun _ ↦ rfl)
+  _         = F G b := by rw [F_spec]
+
+private theorem F_eval_eq_zero [Finite G] (b : B) : (F G b).eval b = 0 := by
+  let foo := Fintype.ofFinite G
+  simp [F_spec,finprod_eq_prod_of_fintype,eval_prod]
+  apply @Finset.prod_eq_zero _ _ _ _ _ (1 : G) (Finset.mem_univ 1)
+  simp
+
+open scoped algebraMap
+
+noncomputable local instance : Algebra A[X] B[X] :=
+  RingHom.toAlgebra (Polynomial.mapRingHom (Algebra.toRingHom))
+
+@[simp, norm_cast]
+theorem coe_monomial (n : ℕ) (a : A) : ((monomial n a : A[X]) : B[X]) = monomial n (a : B) :=
+  map_monomial _
+
+private theorem F_descent [Finite G]
+    (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) (b : B) :
+    ∃ M : A[X], (M : B[X]) = F G b := by
+  choose f hf using fun b ↦ (hFull b)
+  classical
+  let f' : B → A := fun b ↦ if h : ∀ σ : G, σ • b = b then f b h else 37
+  use (∑ x ∈ (F G b).support, (monomial x) (f' ((F G b).coeff x)))
+  ext N
+  push_cast
+  simp_rw [finset_sum_coeff, ← lcoeff_apply, lcoeff_apply, coeff_monomial]
+  simp only [Finset.sum_ite_eq', mem_support_iff, ne_eq, ite_not, f']
+  symm
+  split
+  · next h => exact h
+  · next h1 =>
+    rw [dif_pos <| fun σ ↦ ?_]
+    · refine hf ?_ ?_
+    · nth_rw 2 [← F_smul_eq_self σ]
+      rfl
+
+variable (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) [Finite G]
+variable (G) in
+noncomputable def M [Finite G] (b : B) : A[X] := (F_descent hFull b).choose
+
+theorem M_spec (b : B) : ((M G hFull b : A[X]) : B[X]) = F G b := (F_descent hFull b).choose_spec
+
+theorem M_monic (b : B) : (M G hFull b).Monic := sorry -- finprodmonic
+
+theorem M_eval_eq_zero (b : B) : (M G hFull b).eval₂ (algebraMap A B) b = 0 := by
+  sorry -- follows from `F_eval_eq_zero`
+
+end charpoly
+
+section part_a
+
+variable {A : Type*} [CommRing A]
+  {B : Type*} [CommRing B] [Algebra A 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) :
+    Algebra.IsIntegral A B where
+  isIntegral b := ⟨M G hFull b, M_monic hFull b, M_eval_eq_zero hFull b⟩
+
+variable (P Q : Ideal B) [P.IsPrime] [Q.IsPrime]
+  --
+  (hPQ : Ideal.comap (algebraMap A B) P = Ideal.comap (algebraMap A B) Q)
+
+-- Algebra.IsIntegral A B
+open scoped Pointwise
+
 -- (Part a of Théorème 2 in section 2 of chapter 5 of Bourbaki Alg Comm)
-theorem part_a
+theorem part_a [SMulCommClass G A B]
     (hPQ : Ideal.comap (algebraMap A B) P = Ideal.comap (algebraMap A B) Q)
-    (hGalois : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ a : A, b = a) :
+    (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a : A, b = a) :
     ∃ g : G, Q = g • P := by
+  haveI : Algebra.IsIntegral A B := isIntegral_of_Full hFull'
   cases nonempty_fintype G
   suffices ∃ g : G, Q ≤ g • P by
     obtain ⟨g, hg⟩ := this
@@ -93,8 +217,9 @@ theorem part_a
       Algebra.isIntegral_def.1 inferInstance x).ne
     rw [← hPQ]
     ext x
-    specialize hGalois (algebraMap A B x)
-    have := hGalois.2 ⟨x, rfl⟩
+    specialize hFull' (algebraMap A B x)
+    have : ∀ (g : G), g • (algebraMap A B x) = (algebraMap A B x) := fun g ↦ by
+      rw [Algebra.algebraMap_eq_smul_one, smul_comm, smul_one]
     simp only [Ideal.mem_comap]
     nth_rw 2 [← this]
     exact Ideal.smul_mem_pointwise_smul_iff.symm
@@ -103,8 +228,8 @@ theorem part_a
   rw [← Ideal.subset_union_prime 1 1 <| fun g _ _ _ ↦ ?_]; swap
   · exact Ideal.map_isPrime_of_equiv (MulSemiringAction.toRingEquiv _ _ g)
   intro x hx
-  specialize hGalois (∏ᶠ σ : G, σ • x)
-  obtain ⟨a, ha⟩ := hGalois.1 (norm_fixed _)
+  specialize hFull' (∏ᶠ σ : G, σ • x)
+  obtain ⟨a, ha⟩ := hFull' (norm_fixed _)
   have : (a : B) ∈ Q := by
     rw [← ha, Ideal.IsPrime.finprod_mem_iff_exists_mem]
     use 1
@@ -167,6 +292,12 @@ end part_a
 
 section part_b
 
+
+
+variable {A : Type*} [CommRing A]
+  {B : Type*} [CommRing B] [Algebra A B]
+  {G : Type*} [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B]
+
 -- set-up for part (b) of the lemma. G acts on B with invariants A (or more precisely the
 -- image of A). Warning: `P` was a prime ideal of `B` in part (a) but it's a prime ideal
 -- of `A` here, in fact it's Q ∩ A, the preimage of Q in A.
@@ -232,69 +363,8 @@ example : --[Algebra A k] [IsScalarTower A (A ⧸ p) k] [Algebra k K] [IsScalarT
 
 open Polynomial BigOperators
 
-variable (G) in
-/-- `F : B[X]` defined to be a product of linear factors `(X - τ • α)`; where
-`τ` runs over `L ≃ₐ[K] L`, and `α : B` is an element which generates `(B ⧸ Q)ˣ`
-and lies in `τ • Q` for all `τ ∉ (decomposition_subgroup_Ideal'  A K L B Q)`.-/
-private noncomputable abbrev F (b : B) : B[X] := ∏ᶠ τ : G, (X - C (τ • b))
-
-omit [Finite G] in
-private theorem F_spec (b : B) : F G b = ∏ᶠ τ : G, (X - C (τ • b)) := rfl
-
-private 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]
-  _         = ∏ᶠ τ : G, σ • (X - C (τ • b)) := smul_finprod' _
-  _         = ∏ᶠ τ : G, (X - C ((σ * τ) • b)) := by simp [smul_sub, smul_smul]
-  _         = ∏ᶠ τ' : G, (X - C (τ' • b)) := finprod_eq_of_bijective (fun τ ↦ σ * τ)
-                                               (Group.mulLeft_bijective σ) (fun _ ↦ rfl)
-  _         = F G b := by rw [F_spec]
-
-private theorem F_eval_eq_zero (b : B) : (F G b).eval b = 0 := by
-  let foo := Fintype.ofFinite G
-  simp [F_spec,finprod_eq_prod_of_fintype,eval_prod]
-  apply @Finset.prod_eq_zero _ _ _ _ _ (1 : G) (Finset.mem_univ 1)
-  simp
-
 open scoped algebraMap
 
-noncomputable local instance : Algebra A[X] B[X] :=
-  RingHom.toAlgebra (Polynomial.mapRingHom (Algebra.toRingHom))
-
--- PR?
-omit [Algebra.IsIntegral A B] in
-@[simp, norm_cast]
-theorem coe_monomial (n : ℕ) (a : A) : ((monomial n a : A[X]) : B[X]) = monomial n (a : B) :=
-  map_monomial _
-
-omit [Algebra.IsIntegral A B] in
-private theorem F_descent (hGalois : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ a : A, b = a) (b : B) :
-    ∃ M : A[X], (M : B[X]) = F G b := by
-  choose f hf using fun b ↦ (hGalois b).mp
-  classical
-  let f' : B → A := fun b ↦ if h : ∀ σ : G, σ • b = b then f b h else 37
-  use (∑ x ∈ (F G b).support, (monomial x) (f' ((F G b).coeff x)))
-  ext N
-  push_cast
-  simp_rw [finset_sum_coeff, ← lcoeff_apply, lcoeff_apply, coeff_monomial]
-  simp only [Finset.sum_ite_eq', mem_support_iff, ne_eq, ite_not, f']
-  symm
-  split
-  · next h => exact h
-  · next h1 =>
-    rw [dif_pos <| fun σ ↦ ?_]
-    · refine hf ?_ ?_
-    · nth_rw 2 [← F_smul_eq_self σ]
-      rfl
-
-variable (G) in
-noncomputable def M (b : B) : A[X] := (F_descent hGalois b).choose
-
-omit [Algebra.IsIntegral A B] in
-theorem M_spec (b : B) : ((M G hGalois b : A[X]) : B[X]) = F G b := (F_descent hGalois b).choose_spec
-
-theorem M_eval_eq_zero (b : B) : (M G hGalois b).eval₂ (algebraMap A[X] B[X]) b = 0 := by
-  sorry -- follows from `F_eval_eq_zero`
-
 theorem Algebra.isAlgebraic_of_subring_isAlgebraic {R k K : Type*} [CommRing R] [CommRing k]
     [CommRing K] [Algebra R K] [IsFractionRing R K] [Algebra k K]
     (h : ∀ x : R, IsAlgebraic k (x : K)) : Algebra.IsAlgebraic k K := by
@@ -359,6 +429,7 @@ noncomputable def baz2 : MulAction.stabilizer G Q →* (L ≃ₐ[K] L) where
   map_one' := sorry
   map_mul' := sorry
 
+variable (hFull : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ a : A, b = a) in
 theorem main_result : Function.Surjective
     (baz2 Q P L K : MulAction.stabilizer G Q → (L ≃ₐ[K] L)) := by
   sorry