Quaternion algebras project (#170)

* start on quat alg project

* fix

* More quat alg

* fix build

Author: kbuzzard

FLT/AutomorphicForm/QuaternionAlgebra.lean

@@ -1,14 +1,9 @@
 /-
 Copyright (c) 2024 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kevin Buzzard, Ludwig Monnerjahn, Hannah Scholz
+Authors: Kevin Buzzard
 -/
-import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
-import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
-import Mathlib.NumberTheory.NumberField.Basic
-import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
-import Mathlib.Algebra.Group.Subgroup.Pointwise
-import FLT.ForMathlib.ActionTopology
+import FLT.TotallyDefiniteQuaternionAlgebra.Finiteness
 
 /-
 
@@ -18,136 +13,112 @@ import FLT.ForMathlib.ActionTopology
 
 suppress_compilation
 
-variable (F : Type*) [Field F] [NumberField F]
+variable (F : Type*) [Field F] [NumberField F] --[NumberField.IsTotallyReal F]
 
-variable (D : Type*) [Ring D] [Algebra F D]
+variable (D : Type*) [Ring D] [Algebra F D] --[IsCentralSimple F D] [FiniteDimensional F D]
 
-open DedekindDomain
-
-open scoped NumberField
-
-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]
-    intro a b
-    apply TensorProduct.induction_on (motive := fun b ↦ 1 ⊗ₜ[R] a * b = b * 1 ⊗ₜ[R] a)
-    · simp only [mul_zero, zero_mul]
-    · intro d a'
-      simp only [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_one]
-      rw [NonUnitalCommSemiring.mul_comm]
-    · intro x y hx hy
-      rw [left_distrib, hx, hy, right_distrib]
-    )
-
-instance [Module.Finite R D] : Module.Finite A (D ⊗[R] A) := sorry
-instance [Module.Free R D]  : Module.Free A (D ⊗[R] A) := sorry
+namespace TotallyDefiniteQuaternionAlgebra
 
--- #synth Ring (D ⊗[F] FiniteAdeleRing (𝓞 F) F)
+-- noncomputable example : D →+* (D ⊗[F] FiniteAdeleRing (𝓞 F) F) :=
+--   Algebra.TensorProduct.includeLeftRingHom
 
-end missing_instances
+open scoped TensorProduct NumberField
 
-instance : TopologicalSpace (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) := actionTopology (FiniteAdeleRing (𝓞 F) F) _
-instance : IsActionTopology (FiniteAdeleRing (𝓞 F) F) (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) := ⟨rfl⟩
-instance [FiniteDimensional F D] : 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) _
+open DedekindDomain
 
-namespace TotallyDefiniteQuaternionAlgebra
+abbrev Dfx := (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ
 
-noncomputable example : D →+* (D ⊗[F] FiniteAdeleRing (𝓞 F) F) :=
-  Algebra.TensorProduct.includeLeftRingHom
+noncomputable abbrev incl₁ : Dˣ →* Dfx F D :=
+  Units.map Algebra.TensorProduct.includeLeftRingHom.toMonoidHom
 
-abbrev Dfx := (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ
-noncomputable abbrev incl : Dˣ →* Dfx F D := Units.map Algebra.TensorProduct.includeLeftRingHom.toMonoidHom
+noncomputable abbrev incl₂ : (FiniteAdeleRing (𝓞 F) F)ˣ →* Dfx F D :=
+  Units.map Algebra.TensorProduct.rightAlgebra'.toMonoidHom
 
-structure AutomorphicForm (M : Type*) [AddCommGroup M] where
-  toFun : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ → M
-  left_invt : ∀ (d : Dˣ) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ),
-    toFun (Units.map Algebra.TensorProduct.includeLeftRingHom.toMonoidHom d * x) = toFun x
-  loc_cst : ∃ U : Subgroup (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ,
-    IsOpen (U : Set (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) ∧
-    ∀ (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ),
-    ∀ u ∈ U, toFun (x * u) = toFun x
+/-!
+This definition is made in mathlib-generality but is *not* the definition of an automorphic
+form unless Dˣ is compact mod centre at infinity. This hypothesis will be true if `D` is a
+totally definite quaternion algebra.
+-/
+structure AutomorphicForm
+  -- defined over R
+  (R : Type*) [CommRing R]
+  -- of weight W
+  (W : Type*) [AddCommGroup W] [Module R W] [MulAction Dˣ W]
+  -- and level U
+  (U : Subgroup (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ)
+  -- and character χ
+  (χ : (FiniteAdeleRing (𝓞 F) F)ˣ →* R) where
+  -- definition
+  toFun : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ → W
+  left_invt : ∀ (δ : Dˣ) (g : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ),
+    toFun (Units.map Algebra.TensorProduct.includeLeftRingHom.toMonoidHom δ * g) = δ • (toFun g)
+  has_character : ∀ (g : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) (z : (FiniteAdeleRing (𝓞 F) F)ˣ),
+    toFun (g * incl₂ F D z) = χ z • toFun g
+  right_invt : ∀ (g : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ),
+    ∀ u ∈ U, toFun (g * u) = toFun g
 
 namespace AutomorphicForm
 
-variable {M : Type*} [AddCommGroup M]
+-- defined over R
+variable  (R : Type*) [CommRing R]
+  -- weight
+  (W : Type*) [AddCommGroup W] [Module R W] [MulAction Dˣ W] -- actions should commute in practice
+  -- level
+  (U : Subgroup (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) -- subgroup should be compact and open
+  -- character
+  (χ : (FiniteAdeleRing (𝓞 F) F)ˣ →* R)
 
-variable {F D}
+variable {F D R W U χ}
 
-instance : CoeFun (AutomorphicForm F D M) (fun _ ↦ Dfx F D → M) where
+instance : CoeFun (AutomorphicForm F D R W U χ) (fun _ ↦ Dfx F D → W) where
   coe := toFun
 
 attribute [coe] AutomorphicForm.toFun
 
 @[ext]
-theorem ext (φ ψ : AutomorphicForm F D M) (h : ∀ x, φ x = ψ x) : φ = ψ := by
+theorem ext (φ ψ : AutomorphicForm F D R W U χ) (h : ∀ x, φ x = ψ x) : φ = ψ := by
   cases φ; cases ψ; simp only [mk.injEq]; ext; apply h
 
-def zero [FiniteDimensional F D] : (AutomorphicForm F D M) where
+def zero : (AutomorphicForm F D R W U χ) where
   toFun := 0
-  left_invt := by simp
-  loc_cst := by use ⊤; simp
+  left_invt := sorry
+  has_character := sorry
+  right_invt := sorry
 
-instance [FiniteDimensional F D] : Zero (AutomorphicForm F D M) where
+instance : Zero (AutomorphicForm F D R W U χ) where
   zero := zero
 
 @[simp]
-theorem zero_apply [FiniteDimensional F D] (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
-    (0 : AutomorphicForm F D M) x = 0 := rfl
+theorem zero_apply (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
+    (0 : AutomorphicForm F D R W U χ) x = 0 := rfl
 
-def neg (φ : AutomorphicForm F D M) : AutomorphicForm F D M where
+def neg (φ : AutomorphicForm F D R W U χ) : AutomorphicForm F D R W U χ where
   toFun x := - φ x
-  left_invt := by
-    intro d x
-    simp only [RingHom.toMonoidHom_eq_coe, neg_inj]
-    exact φ.left_invt d x
-  loc_cst := by
-    rcases φ.loc_cst with ⟨U, openU, hU⟩
-    use U
-    exact ⟨openU, fun x u umem ↦ by rw [neg_inj]; exact hU x u umem⟩
-
-instance : Neg (AutomorphicForm F D M) where
+  left_invt := sorry
+  has_character := sorry
+  right_invt := sorry
+
+instance : Neg (AutomorphicForm F D R W U χ) where
   neg := neg
 
 @[simp, norm_cast]
-theorem neg_apply (φ : AutomorphicForm F D M) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
-    (-φ : AutomorphicForm F D M) x = -(φ x) := rfl
+theorem neg_apply (φ : AutomorphicForm F D R W U χ) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
+    (-φ : AutomorphicForm F D R W U χ) x = -(φ x) := rfl
 
-instance add (φ ψ : AutomorphicForm F D M) : AutomorphicForm F D M where
+instance add (φ ψ : AutomorphicForm F D R W U χ) : AutomorphicForm F D R W U χ where
   toFun x := φ x + ψ x
-  left_invt := by
-    intro d x
-    simp only [← φ.left_invt d x, ← ψ.left_invt d x]
-  loc_cst := by
-    rcases φ.loc_cst with ⟨U, openU, hU⟩
-    rcases ψ.loc_cst with ⟨V, openV, hV⟩
-    use U ⊓ V
-    constructor
-    · unfold Subgroup.instInf Submonoid.instInf
-      simp only [Subgroup.coe_toSubmonoid, Subgroup.coe_set_mk]
-      exact IsOpen.inter openU openV
-    · intro x u ⟨umemU, umemV⟩
-      simp only
-      rw [hU x u umemU, hV x u umemV]
-
-instance : Add (AutomorphicForm F D M) where
+  left_invt := sorry
+  has_character := sorry
+  right_invt := sorry
+
+instance : Add (AutomorphicForm F D R W U χ) where
   add := add
 
 @[simp, norm_cast]
-theorem add_apply (φ ψ : AutomorphicForm F D M) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
+theorem add_apply (φ ψ : AutomorphicForm F D R W U χ) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
     (φ + ψ) x = (φ x) + (ψ x) := rfl
 
-instance addCommGroup [FiniteDimensional F D] : AddCommGroup (AutomorphicForm F D M) where
+instance addCommGroup : AddCommGroup (AutomorphicForm F D R W U χ) where
   add := (· + ·)
   add_assoc := by intros; ext; simp [add_assoc];
   zero := 0
@@ -159,55 +130,41 @@ instance addCommGroup [FiniteDimensional F D] : AddCommGroup (AutomorphicForm F
   neg_add_cancel := by intros; ext; simp
   add_comm := by intros; ext; simp [add_comm]
 
-open ConjAct
-open scoped Pointwise
-
-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
-
-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
-  rw [continuous_def] at this1 this2
-  specialize this2 U hU
-  specialize this1 _ this2
-  convert this1 using 1
-  ext x
-  convert conjAct_mem _ _ _ using 1
-  simp only [Set.mem_preimage, SetLike.mem_coe]
-  refine ⟨?_, ?_⟩ <;> intro h
-  · use g⁻¹ * x * g -- duh
-    simp [h]
-    group
-  · rcases h with ⟨u, hu, rfl⟩
-    group
-    exact hu
-
-instance [FiniteDimensional F D] : SMul (Dfx F D) (AutomorphicForm F D M) where
-  smul g φ :=   { -- (g • f) (x) := f(xg) -- x(gf)=(xg)f
-    toFun := fun x => φ (x * g)
-    left_invt := by
-      intros d x
-      simp only [← φ.left_invt d x, mul_assoc]
-      exact φ.left_invt d (x * g)
-    loc_cst := by
-      rcases φ.loc_cst with ⟨U, openU, hU⟩
-      use toConjAct g • U
-      constructor
-      · apply toConjAct_open _ openU
-      · intros x u umem
-        simp only
-        rw[conjAct_mem] at umem
-        obtain ⟨ugu, hugu, eq⟩ := umem
-        rw[←eq, ←mul_assoc, ←mul_assoc, inv_mul_cancel_right, hU (x*g) ugu hugu]
-  }
+-- from this point we need the Dˣ-action on W to be R-linear
+variable [SMulCommClass R Dˣ W]
 
-@[simp]
-theorem sMul_eval [FiniteDimensional F D] (g : Dfx F D) (f : AutomorphicForm F D M) (x : (D ⊗[F] FiniteAdeleRing (𝓞 F) F)ˣ) :
-  (g • f) x = f (x * g) := rfl
+def smul (r : R) (φ : AutomorphicForm F D R W U χ) :
+    AutomorphicForm F D R W U χ where
+      toFun g := r • φ g
+      left_invt := sorry
+      has_character := sorry
+      right_invt := sorry
+
+instance : SMul R (AutomorphicForm F D R W U χ) where
+  smul := smul
+
+instance module : Module R (AutomorphicForm F D R W U χ) where
+  one_smul := sorry
+  mul_smul := sorry
+  smul_zero := sorry
+  smul_add := sorry
+  add_smul := sorry
+  zero_smul := sorry
+
+
+end AutomorphicForm
+
+-- Now assume R is a field.
+
+variable  (R : Type*) [Field R]
+  -- weight
+  (W : Type*) [AddCommGroup W] [Module R W] [MulAction Dˣ W] -- actions should commute in practice
+  -- level
+  (U : Subgroup (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) -- subgroup should be compact and open
+  -- character
+  (χ : (FiniteAdeleRing (𝓞 F) F)ˣ →* R)
+
+theorem AutomorphicForm.finiteDimensional [FiniteDimensional R W] :
+    FiniteDimensional R (AutomorphicForm F D R W U χ) := sorry
 
-instance [FiniteDimensional F D] : MulAction (Dfx F D) (AutomorphicForm F D M) where
-  smul := (· • ·)
-  one_smul := by intros; ext; simp only [sMul_eval, mul_one]
-  mul_smul := by intros; ext; simp only [sMul_eval, mul_assoc]
+end TotallyDefiniteQuaternionAlgebra

FLT/FLT_files.lean

@@ -23,6 +23,6 @@ import FLT.MathlibExperiments.Frobenius
 import FLT.MathlibExperiments.Frobenius2
 import FLT.MathlibExperiments.FrobeniusRiou
 import FLT.MathlibExperiments.HopfAlgebra.Basic
-import FLT.MathlibExperiments.IsCentralSimple
+--import FLT.MathlibExperiments.IsCentralSimple
 import FLT.MathlibExperiments.IsFrobenius
 import FLT.TateCurve.TateCurve

FLT/NumberField/IsTotallyReal.lean

@@ -0,0 +1,5 @@
+import Mathlib.NumberTheory.NumberField.Basic
+import Mathlib.Data.Complex.Basic
+
+class NumberField.IsTotallyReal (F : Type*) [Field F] [NumberField F] : Prop where
+  isTotallyReal : ∀ τ : F →+* ℂ, ∀ f : F, ∃ r : ℝ, τ f = r