Merge pull request #2 from morrison-daniel/ImperialCollegeLondon-main

Imperial college london main

FLT/AutomorphicForm/QuaternionAlgebra.lean

@@ -8,11 +8,12 @@ import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
 import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
 import Mathlib.Algebra.Group.Subgroup.Pointwise
-import FLT.HIMExperiments.module_topology
+import FLT.ForMathlib.ActionTopology
 
 /-
 
 # Definition of automorphic forms on a totally definite quaternion algebra
+
 -/
 
 suppress_compilation
@@ -25,16 +26,14 @@ open DedekindDomain
 
 open scoped NumberField
 
--- my work (two PRs)
-instance : TopologicalSpace (FiniteAdeleRing (𝓞 F) F) := sorry
-instance : TopologicalRing (FiniteAdeleRing (𝓞 F) F) := sorry
-
 open scoped TensorProduct
 
 section missing_instances
 
 variable {R D A : Type*} [CommRing R] [Ring D] [CommRing A] [Algebra R D] [Algebra R A]
 
+#synth Algebra A (A ⊗[R] D)
+-- does this make a diamond?
 instance : Algebra A (D ⊗[R] A) :=
   Algebra.TensorProduct.includeRight.toRingHom.toAlgebra' (by
     simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.includeRight_apply]
@@ -54,9 +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)) := Module.topology (FiniteAdeleRing (𝓞 F) F)
-instance : TopologicalRing (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) := moobar (FiniteAdeleRing (𝓞 F) F) (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))
+
+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)) :=
+  -- 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
 
@@ -87,7 +90,7 @@ instance : CoeFun (AutomorphicForm F D M) (fun _ ↦ Dfx F D → M) where
 attribute [coe] AutomorphicForm.toFun
 
 @[ext]
-lemma ext (φ ψ : AutomorphicForm F D M) (h : ∀ x, φ x = ψ x) : φ = ψ := by
+theorem ext (φ ψ : AutomorphicForm F D M) (h : ∀ x, φ x = ψ x) : φ = ψ := by
   cases φ; cases ψ; simp only [mk.injEq]; ext; apply h
 
 def zero : (AutomorphicForm F D M) where
@@ -99,7 +102,7 @@ instance : Zero (AutomorphicForm F D M) where
   zero := zero
 
 @[simp]
-lemma zero_apply (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
+theorem zero_apply (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
     (0 : AutomorphicForm F D M) x = 0 := rfl
 
 def neg (φ : AutomorphicForm F D M) : AutomorphicForm F D M where
@@ -117,7 +120,7 @@ instance : Neg (AutomorphicForm F D M) where
   neg := neg
 
 @[simp, norm_cast]
-lemma neg_apply (φ : AutomorphicForm F D M) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
+theorem neg_apply (φ : AutomorphicForm F D M) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
     (-φ : AutomorphicForm F D M) x = -(φ x) := rfl
 
 instance add (φ ψ : AutomorphicForm F D M) : AutomorphicForm F D M where
@@ -141,7 +144,7 @@ instance : Add (AutomorphicForm F D M) where
   add := add
 
 @[simp, norm_cast]
-lemma add_apply (φ ψ : AutomorphicForm F D M) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
+theorem add_apply (φ ψ : AutomorphicForm F D M) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
     (φ + ψ) x = (φ x) + (ψ x) := rfl
 
 instance addCommGroup : AddCommGroup (AutomorphicForm F D M) where
@@ -159,10 +162,10 @@ instance addCommGroup : AddCommGroup (AutomorphicForm F D M) where
 open ConjAct
 open scoped Pointwise
 
-lemma conjAct_mem {G: Type*}  [Group G] (U: Subgroup G) (g: G) (x : G):
+theorem conjAct_mem {G: Type*}  [Group G] (U: Subgroup G) (g: G) (x : G):
   x ∈ toConjAct g • U ↔ ∃ u ∈ U, g * u * g⁻¹ = x := by rfl
 
-lemma toConjAct_open {G : Type*} [Group G] [TopologicalSpace G] [TopologicalGroup G]
+theorem toConjAct_open {G : Type*} [Group G] [TopologicalSpace G] [TopologicalGroup G]
     (U : Subgroup G) (hU : IsOpen (U : Set G)) (g : G) : IsOpen (toConjAct g • U : Set G) := by
   have this1 := continuous_mul_left g⁻¹
   have this2 := continuous_mul_right g
@@ -201,7 +204,7 @@ instance : SMul (Dfx F D) (AutomorphicForm F D M) where
   }
 
 @[simp]
-lemma sMul_eval (g : Dfx F D) (f : AutomorphicForm F D M) (x : (D ⊗[F] FiniteAdeleRing (𝓞 F) F)ˣ) :
+theorem sMul_eval (g : Dfx F D) (f : AutomorphicForm F D M) (x : (D ⊗[F] FiniteAdeleRing (𝓞 F) F)ˣ) :
   (g • f) x = f (x * g) := rfl
 
 instance : MulAction (Dfx F D) (AutomorphicForm F D M) where