chore(number_theory/modular_forms/slash_invariant_forms): golf and re…

…name (#18933)

In the `slash_action` namespace, this renames:

* `right_action` to `slash_mul` (and reverses the direction), to match `slash_one`
* `add_action` to `add_slash`, to match `zero_slash`
* `smul_action` to `smul_slash`, to match `zero_slash`

src/number_theory/modular_forms/slash_actions.lean

@@ -39,9 +39,9 @@ class slash_action (β G α γ : Type*) [group G] [add_monoid α] [has_smul γ 
 (map : β → G → α → α)
 (zero_slash : ∀ (k : β) (g : G), map k g 0 = 0)
 (slash_one : ∀ (k : β) (a : α) , map k 1 a = a)
-(right_action : ∀ (k : β) (g h : G) (a : α), map k h (map k g a) = map k (g * h) a )
-(smul_action : ∀ (k : β) (g : G) (a : α) (z : γ), map k g (z • a) = z • (map k g a))
-(add_action : ∀ (k : β) (g : G) (a b : α), map k g (a + b) = map k g a + map k g b)
+(slash_mul : ∀ (k : β) (g h : G) (a : α), map k (g * h) a =map k h (map k g a))
+(smul_slash : ∀ (k : β) (g : G) (a : α) (z : γ), map k g (z • a) = z • (map k g a))
+(add_slash : ∀ (k : β) (g : G) (a b : α), map k g (a + b) = map k g a + map k g b)
 
 localized "notation (name := modular_form.slash) f ` ∣[`:100 k `;` γ `] `:0 a :100 :=
   slash_action.map γ k a f" in modular_form
@@ -52,28 +52,28 @@ localized "notation (name := modular_form.slash_complex) f ` ∣[`:100 k `] `:0
 @[simp] lemma slash_action.neg_slash {β G α γ : Type*} [group G] [add_group α] [has_smul γ α]
   [slash_action β G α γ] (k : β) (g : G) (a : α) :
   (-a) ∣[k;γ] g = - (a ∣[k;γ] g) :=
-eq_neg_of_add_eq_zero_left $ by rw [←slash_action.add_action, add_left_neg, slash_action.zero_slash]
+eq_neg_of_add_eq_zero_left $ by rw [←slash_action.add_slash, add_left_neg, slash_action.zero_slash]
 
 @[simp] lemma slash_action.smul_slash_of_tower {R β G α : Type*} (γ : Type*) [group G] [add_group α]
   [monoid γ] [mul_action γ α]
   [has_smul R γ] [has_smul R α] [is_scalar_tower R γ α]
   [slash_action β G α γ] (k : β) (g : G) (a : α) (r : R) :
   (r • a) ∣[k;γ] g = r • (a ∣[k;γ] g) :=
-by rw [←smul_one_smul γ r a, slash_action.smul_action, smul_one_smul]
+by rw [←smul_one_smul γ r a, slash_action.smul_slash, smul_one_smul]
 
 attribute [simp]
   slash_action.zero_slash slash_action.slash_one
-  slash_action.smul_action slash_action.add_action
+  slash_action.smul_slash slash_action.add_slash
 
 /--Slash_action induced by a monoid homomorphism.-/
 def monoid_hom_slash_action {β G H α γ : Type*} [group G] [add_monoid α] [has_smul γ α]
   [group H] [slash_action β G α γ] (h : H →* G) : slash_action β H α γ :=
 { map := λ k g, slash_action.map γ k (h g),
   zero_slash := λ k g, slash_action.zero_slash k (h g),
   slash_one := λ k a, by simp only [map_one, slash_action.slash_one],
-  right_action := λ k g gg a, by simp only [map_mul, slash_action.right_action],
-  smul_action := λ _ _, slash_action.smul_action _ _,
-  add_action := λ _ g _ _, slash_action.add_action _ (h g) _ _,}
+  slash_mul := λ k g gg a, by simp only [map_mul, slash_action.slash_mul],
+  smul_slash := λ _ _, slash_action.smul_slash _ _,
+  add_slash := λ _ g _ _, slash_action.add_slash _ (h g) _ _,}
 
 namespace modular_form
 
@@ -90,8 +90,8 @@ section
 -- temporary notation until the instance is built
 local notation f ` ∣[`:100 k `]`:0 γ :100 := modular_form.slash k γ f
 
-private lemma slash_right_action (k : ℤ) (A B : GL(2, ℝ)⁺) (f : ℍ → ℂ) :
-  (f ∣[k] A) ∣[k] B = f ∣[k] (A * B) :=
+private lemma slash_mul (k : ℤ) (A B : GL(2, ℝ)⁺) (f : ℍ → ℂ) :
+  f ∣[k] (A * B) = (f ∣[k] A) ∣[k] B :=
 begin
   ext1,
   simp_rw [slash,(upper_half_plane.denom_cocycle A B x)],
@@ -109,7 +109,7 @@ begin
   simp_rw [this, ← mul_assoc, ←mul_zpow],
 end
 
-private lemma slash_add (k : ℤ) (A : GL(2, ℝ)⁺) (f g : ℍ → ℂ) :
+private lemma add_slash (k : ℤ) (A : GL(2, ℝ)⁺) (f g : ℍ → ℂ) :
   (f + g) ∣[k] A = (f ∣[k] A) + (g ∣[k] A) :=
 begin
   ext1,
@@ -140,9 +140,9 @@ instance : slash_action ℤ GL(2, ℝ)⁺ (ℍ → ℂ) ℂ :=
 { map := slash,
   zero_slash := zero_slash,
   slash_one := slash_one,
-  right_action := slash_right_action,
-  smul_action := smul_slash,
-  add_action := slash_add }
+  slash_mul := slash_mul,
+  smul_slash := smul_slash,
+  add_slash := add_slash }
 
 end
 

src/number_theory/modular_forms/slash_invariant_forms.lean

@@ -85,7 +85,7 @@ instance slash_invariant_form_class.coe_to_fun [slash_invariant_form_class F Γ
   has_coe_to_fun F (λ _, ℍ → ℂ) := fun_like.has_coe_to_fun
 
 @[simp] lemma slash_action_eqn [slash_invariant_form_class F Γ k] (f : F) (γ : Γ) :
-   slash_action.map ℂ k γ ⇑f = ⇑f := slash_invariant_form_class.slash_action_eq f γ
+  ⇑f ∣[k] γ = ⇑f := slash_invariant_form_class.slash_action_eq f γ
 
 lemma slash_action_eqn' (k : ℤ) (Γ : subgroup SL(2, ℤ)) [slash_invariant_form_class F Γ k] (f : F)
   (γ : Γ) (z : ℍ) : f (γ • z) = ((↑ₘ[ℤ]γ 1 0 : ℂ) * z +(↑ₘ[ℤ]γ 1 1 : ℂ))^k * f z :=
@@ -103,7 +103,7 @@ instance [slash_invariant_form_class F Γ k] : has_coe_t F (slash_invariant_form
 instance has_add : has_add (slash_invariant_form Γ k) :=
 ⟨ λ f g,
   { to_fun := f + g,
-    slash_action_eq' := λ γ, by convert slash_action.add_action k γ (f : ℍ → ℂ) g; simp } ⟩
+    slash_action_eq' := λ γ, by rw [slash_action.add_slash, slash_action_eqn, slash_action_eqn] }⟩
 
 @[simp] lemma coe_add (f g : slash_invariant_form Γ k) : ⇑(f + g) = f + g := rfl
 @[simp] lemma add_apply (f g : slash_invariant_form Γ k) (z : ℍ) : (f + g) z = f z + g z := rfl
@@ -120,8 +120,7 @@ variables {α : Type*} [has_smul α ℂ] [is_scalar_tower α ℂ ℂ]
 instance has_smul : has_smul α (slash_invariant_form Γ k) :=
 ⟨ λ c f,
   { to_fun := c • f,
-    slash_action_eq' := λ γ, by rw [←smul_one_smul ℂ c ⇑f, slash_action.smul_action k γ ⇑f,
-                                    slash_action_eqn] }⟩
+    slash_action_eq' := λ γ, by rw [slash_action.smul_slash_of_tower, slash_action_eqn] }⟩
 
 @[simp] lemma coe_smul (f : slash_invariant_form Γ k) (n : α) : ⇑(n • f) = n • f := rfl
 @[simp] lemma smul_apply (f : slash_invariant_form Γ k) (n : α) (z : ℍ) :
@@ -132,8 +131,7 @@ end
 instance has_neg : has_neg (slash_invariant_form Γ k) :=
 ⟨ λ f,
   { to_fun := -f,
-    slash_action_eq' := λ γ, by simpa [modular_form.subgroup_slash,
-      slash_action.neg_slash] using f.slash_action_eq' γ } ⟩
+    slash_action_eq' := λ γ, by rw [slash_action.neg_slash, slash_action_eqn] } ⟩
 
 @[simp] lemma coe_neg (f : slash_invariant_form Γ k) : ⇑(-f) = -f := rfl
 @[simp] lemma neg_apply (f : slash_invariant_form Γ k) (z : ℍ) : (-f) z = - (f z) := rfl