Module structure on TotallyDefiniteQuaternionAlgebra.AutomorphicForm (#…

…171)

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}