Module structure on TotallyDefiniteQuaternionAlgebra.AutomorphicForm

Author: Ruben-VandeVelde

FLT/AutomorphicForm/QuaternionAlgebra.lean

@@ -136,23 +136,26 @@ variable [SMulCommClass R Dˣ W]
 
 def smul (r : R) (φ : AutomorphicForm F D R W U χ) :
     AutomorphicForm F D R W U χ where
-      toFun g := r • φ g
-      left_invt := by simp [left_invt, smul_comm]
-      has_character g z := by
-        simp_all [has_character]
-        rw [smul_comm] -- makes simp loop :-/
-      right_invt := by simp_all [right_invt]
+  toFun g := r • φ g
+  left_invt := by simp [left_invt, smul_comm]
+  has_character g z := by
+    simp_all [has_character]
+    rw [smul_comm] -- makes simp loop :-/
+  right_invt := by simp_all [right_invt]
 
 instance : SMul R (AutomorphicForm F D R W U χ) where
   smul := smul
 
+lemma smul_apply (r : R) (φ : AutomorphicForm F D R W U χ) (g : (D ⊗[F] FiniteAdeleRing (𝓞 F) F)ˣ) :
+    (r • φ) g = r • (φ g) := rfl
+
 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
+  one_smul g := by ext; simp [smul_apply]
+  mul_smul r s g := by ext; simp [smul_apply, mul_smul]
+  smul_zero r := by ext; simp [smul_apply]
+  smul_add r f g := by ext; simp [smul_apply]
+  add_smul r s g := by ext; simp [smul_apply, add_smul]
+  zero_smul g := by ext; simp [smul_apply]
 
 
 end AutomorphicForm

blueprint/src/chapter/QuaternionAlgebraProject.tex

@@ -98,6 +98,7 @@ \section{Introduction and goal}
   \lean{TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup}
   \label{TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup}
   \uses{TotallyDefiniteQuaternionAlgebra.AutomorphicForm}
+  \leanok
   Pointwise addition $(f_1+f_2)(g):=f_1(g)+f_2(g)$ makes $S_{W,\chi}(U;R)$ into an additive
   abelian group.
 \end{definition}
@@ -107,6 +108,7 @@ \section{Introduction and goal}
   \label{TotallyDefiniteQuaternionAlgebra.AutomorphicForm.module}
   \uses{TotallyDefiniteQuaternionAlgebra.AutomorphicForm,
     TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup}
+  \leanok
   Pointwise scalar multiplication $(r\cdot f)(g):= r\cdot(f(g))$ makes
   $S_{W,\chi}(U;R)$ into an $R$-module.
 \end{definition}