Merge branch 'main' into start_on_localization

Author: kbuzzard

FLT/FLT_files.lean

@@ -1,9 +1,28 @@
+import FLT.AutomorphicForm.QuaternionAlgebra
+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
 import FLT.GlobalLanglandsConjectures.GLnDefs
+import FLT.GlobalLanglandsConjectures.GLzero
 import FLT.GroupScheme.FiniteFlat
+import FLT.HIMExperiments.ContinuousSMul_topology
+import FLT.HIMExperiments.dual_topology
+import FLT.HIMExperiments.flatness
+import FLT.HIMExperiments.module_topology
+import FLT.HIMExperiments.right_module_topology
 import FLT.Hard.Results
+import FLT.MathlibExperiments.Coalgebra.Monoid
+import FLT.MathlibExperiments.Coalgebra.Sweedler
+import FLT.MathlibExperiments.Coalgebra.TensorProduct
+import FLT.MathlibExperiments.Frobenius
+import FLT.MathlibExperiments.Frobenius2
+import FLT.MathlibExperiments.FrobeniusRiou
+import FLT.MathlibExperiments.HopfAlgebra.Basic
+import FLT.MathlibExperiments.IsCentralSimple
+import FLT.MathlibExperiments.IsFrobenius
 import FLT.TateCurve.TateCurve
-import FLT.AutomorphicRepresentation.Example
-import FLT.mathlibExperiments.IsCentralSimple

FLT/HIMExperiments/ContinuousSMul_topology.lean

@@ -80,6 +80,8 @@ functions from `A` (now considered only as an index set, so with no topology) to
 
 -/
 
+namespace ContinuousSMul_topology
+
 section continuous_smul
 
 variable {R : Type} [τR : TopologicalSpace R]
@@ -188,7 +190,7 @@ variable {R : Type} [τR : TopologicalSpace R]
 variable {M : Type} [Zero M] [SMul R M] [aM : TopologicalSpace M] [IsActionTopology R M]
 variable {N : Type} [Zero N] [SMul R N] [aN : TopologicalSpace N] [IsActionTopology R N]
 
-open TopologicalSpace in
+open _root_.TopologicalSpace in
 lemma prod [MulOneClass.{0} R] : IsActionTopology.{0} R (M × N) := by
   constructor
   -- goal: to prove product topology is action topology.
@@ -216,46 +218,44 @@ lemma prod [MulOneClass.{0} R] : IsActionTopology.{0} R (M × N) := by
     sorry
   sorry
 
-#exit
-
 
     -- idea: map R x M -> M is R x M -> R x M x N, τR x σ
     -- R x M has topology τR x (m ↦ Prod.mk m (0 : N))^*σ
     -- M x N -> M is pr₁⋆σ
     -- is pr1_*sigma=Prod.mk' 0^*sigma
     --rw [← continuous_id_iff_le]
-    have := isActionTopology R M
-    let τ1 : TopologicalSpace M := (actionTopology R (M × N)).coinduced (Prod.fst)
-    have foo : aM ≤ τ1 := by
-      rw [this]
-      apply sInf_le
-      unfold_let
-      constructor
-      rw [continuous_iff_coinduced_le]
-      --rw [continuous_iff_le_induced]
-      --rw [instTopologicalSpaceProd]
-      have := ActionTopology.continuousSMul R (M × N)
-      obtain ⟨h⟩ := this
-      rw [continuous_iff_coinduced_le] at h
-      have h2 := coinduced_mono (f := (Prod.fst : M × N → M)) h
-      refine le_trans ?_ h2
-      rw [@coinduced_compose]
-      --rw [coinduced_le_iff_le_induced]
-      rw [show ((Prod.fst : M × N → M) ∘ (fun p ↦ p.1 • p.2 : R × M × N → M × N)) =
-        (fun rm ↦ rm.1 • rm.2) ∘ (fun rmn ↦ (rmn.1, rmn.2.1)) by
-        ext ⟨r, m, n⟩
-        rfl]
-      rw [← @coinduced_compose]
-      apply coinduced_mono
-      rw [← continuous_id_iff_le]
-      have this2 := @Continuous.prod_map R M R M τR ((TopologicalSpace.coinduced Prod.fst (actionTopology R (M × N)))) τR aM id id ?_ ?_
-      swap; fun_prop
-      swap; sorry -- action top ≤ coinduced Prod.fst (action)
-      convert this2
-      sorry -- action top on M now equals coinduced Prod.fst
-      sorry -- same
-      -- so we're going around in circles
-    sorry
+    -- have := isActionTopology R M
+    -- let τ1 : TopologicalSpace M := (actionTopology R (M × N)).coinduced (Prod.fst)
+    -- have foo : aM ≤ τ1 := by
+    --   rw [this]
+    --   apply sInf_le
+    --   unfold_let
+    --   constructor
+    --   rw [continuous_iff_coinduced_le]
+    --   --rw [continuous_iff_le_induced]
+    --   --rw [instTopologicalSpaceProd]
+    --   have := ActionTopology.continuousSMul R (M × N)
+    --   obtain ⟨h⟩ := this
+    --   rw [continuous_iff_coinduced_le] at h
+    --   have h2 := coinduced_mono (f := (Prod.fst : M × N → M)) h
+    --   refine le_trans ?_ h2
+    --   rw [@coinduced_compose]
+    --   --rw [coinduced_le_iff_le_induced]
+    --   rw [show ((Prod.fst : M × N → M) ∘ (fun p ↦ p.1 • p.2 : R × M × N → M × N)) =
+    --     (fun rm ↦ rm.1 • rm.2) ∘ (fun rmn ↦ (rmn.1, rmn.2.1)) by
+    --     ext ⟨r, m, n⟩
+    --     rfl]
+    --   rw [← @coinduced_compose]
+    --   apply coinduced_mono
+    --   rw [← continuous_id_iff_le]
+    --   have this2 := @Continuous.prod_map R M R M τR ((TopologicalSpace.coinduced Prod.fst (actionTopology R (M × N)))) τR aM id id ?_ ?_
+    --   swap; fun_prop
+    --   swap; sorry -- action top ≤ coinduced Prod.fst (action)
+    --   convert this2
+    --   sorry -- action top on M now equals coinduced Prod.fst
+    --   sorry -- same
+    --   -- so we're going around in circles
+    -- sorry
     -- let τ2 : TopologicalSpace M := (actionTopology R (M × N)).induced (fun m ↦ (m, 0))
     -- have moo : τ1 = τ2 := by
     --   unfold_let
@@ -270,7 +270,7 @@ lemma prod [MulOneClass.{0} R] : IsActionTopology.{0} R (M × N) := by
     --   ·
     --     sorry
     -- sorry
-  · apply actionTopology_le
+  -- · apply actionTopology_le
 --     --have foo : @Continuous (M × N) (M × N) _ _ _ := @Continuous.prod_map M N M N (σMN.coinduced Prod.fst) (σMN.coinduced Prod.snd) aM aN id id ?_ ?_-- Z * W -> X * Y
 --     -- conjecture: pushforward of σMN is continuous
 --     -- ⊢ instTopologicalSpaceProd ≤ σMN
@@ -499,3 +499,5 @@ instance Module.topologicalRing : @TopologicalRing D (Module.rtopology A D) _ :=
       sorry }
 
 end commutative
+
+end ContinuousSMul_topology

FLT/HIMExperiments/dual_topology.lean

@@ -90,6 +90,8 @@ functions from `A` (now considered only as an index set, so with no topology) to
 
 -/
 
+namespace dual_topology
+
 section basics
 
 variable (R : Type*) [Monoid R] [TopologicalSpace R] [ContinuousMul R]
@@ -340,3 +342,5 @@ instance moobar : @TopologicalRing D (Module.topology A) _ :=
       apply Module.continuous_bilinear A (LinearMap.mul A D)
     -- finally negation is continuous because it's linear.
     continuous_neg := Module.continuous_linear A (-LinearMap.id) }
+
+end dual_topology

FLT/HIMExperiments/right_module_topology.lean

@@ -35,6 +35,9 @@ functions from `M` (now considered only as an index set, so with no topology) to
 
 -/
 
+-- See FLT.ForMathlib.ActionTopology for a parallel development.
+namespace right_module_topology
+
 section defs
 
 class IsActionTopology (R M : Type*) [SMul R M]
@@ -190,3 +193,5 @@ end what_i_want
 -- possible hints at https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/HIMExperiments/module_topology.lean
 -- except there the topology is *different* so the work does not apply
 end ActionTopology
+
+end right_module_topology

FLT/MathlibExperiments/Coalgebra/Monoid.lean

@@ -5,7 +5,7 @@ Authors: Yunzhou Xie, Yichen Feng, Yanqiao Zhou, Jujian Zhang
 -/
 
 import Mathlib.RingTheory.TensorProduct.Basic
-import FLT.mathlibExperiments.Coalgebra.Sweedler
+import FLT.MathlibExperiments.Coalgebra.Sweedler
 import Mathlib.RingTheory.HopfAlgebra
 
 /-!

FLT/MathlibExperiments/Coalgebra/TensorProduct.lean

@@ -6,7 +6,7 @@ Authors: Yunzhou Xie, Yichen Feng, Yanqiao Zhou, Jujian Zhang
 
 import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.RingTheory.Bialgebra.Basic
-import FLT.mathlibExperiments.Coalgebra.Sweedler
+import FLT.MathlibExperiments.Coalgebra.Sweedler
 
 /-!
 

FLT/MathlibExperiments/HopfAlgebra/Basic.lean

@@ -5,8 +5,8 @@ Authors: Yunzhou Xie, Yichen Feng, Yanqiao Zhou, Jujian Zhang
 -/
 
 import Mathlib.RingTheory.HopfAlgebra
-import FLT.mathlibExperiments.Coalgebra.Monoid
-import FLT.mathlibExperiments.Coalgebra.TensorProduct
+import FLT.MathlibExperiments.Coalgebra.Monoid
+import FLT.MathlibExperiments.Coalgebra.TensorProduct
 import Mathlib.Tactic.Group
 
 /-!
@@ -16,7 +16,7 @@ For an `R`-hopf algebra `A`, we prove in this file the following basic propertie
 - the antipodal map is anticommutative;
 - the antipodal map is unique linear map whose convolution inverse is the identity `𝟙 A`.
   (Note that, confusingly, the identity linear map `x ↦ x` is not actually the unit in the monoid
-  structure of linear maps. See `mathlibExperiments/Coalgebra/Monoid.lean`)
+  structure of linear maps. See `MathlibExperiments/Coalgebra/Monoid.lean`)
 if we further assume `A` is commutative then
 - the `R`-algebra homomorphisms from `A` to `L` has a group structure where multiplication is
   convolution, and inverse of `f `is `f ∘ antipode`