chore(group_theory/group_action): introduce smul_comm_class (#4770)

src/algebra/algebra/basic.lean

@@ -1086,25 +1086,19 @@ by rw [←(one_smul A m), ←smul_assoc, algebra.smul_def, mul_one, one_smul]
 
 variable {A}
 
-lemma smul_algebra_smul_comm (r : R) (a : A) (m : M) : a • r • m = r • a • m :=
-by rw [algebra_compatible_smul A r (a • m), smul_smul, algebra.commutes, mul_smul,
-  ←algebra_compatible_smul]
-
-@[simp] lemma map_smul_eq_smul_map (f : M →ₗ[A] N) (r : R) (m : M) :
-  f (r • m) = r • f m :=
-by rw [algebra_compatible_smul A r m, linear_map.map_smul, ←algebra_compatible_smul A r (f m)]
+@[priority 100] -- see Note [lower instance priority]
+instance is_scalar_tower.to_smul_comm_class : smul_comm_class R A M :=
+⟨λ r a m, by rw [algebra_compatible_smul A r (a • m), smul_smul, algebra.commutes, mul_smul,
+  ←algebra_compatible_smul]⟩
 
-namespace linear_map
+@[priority 100] -- see Note [lower instance priority]
+instance is_scalar_tower.to_smul_comm_class' : smul_comm_class A R M :=
+smul_comm_class.symm _ _ _
 
-variables (R) {A M N}
-
-/-- The `R`-linear map induced by an `A`-linear map when `A` is an algebra over `R`. -/
-def restrict_scalars (f : M →ₗ[A] N) : M →ₗ[R] N :=
-{ to_fun := f,
-  map_add' := λ x y, f.map_add x y,
-  map_smul' := λ c x, map_smul_eq_smul_map _ _ _ }
+lemma smul_algebra_smul_comm (r : R) (a : A) (m : M) : a • r • m = r • a • m :=
+smul_comm _ _ _
 
-variables (R A M N)
+namespace linear_map
 
 instance coe_is_scalar_tower : has_coe (M →ₗ[A] N) (M →ₗ[R] N) :=
 ⟨restrict_scalars R⟩
@@ -1130,52 +1124,6 @@ end linear_map
 
 end is_scalar_tower
 
-namespace linear_map
-
-variables (R : Type*) (A : Type*) (M : Type*) (N : Type*)
-variables [comm_semiring R] [semiring A] [algebra R A]
-variables [add_comm_monoid M] [semimodule A M]
-variables [add_comm_monoid N] [semimodule A N] [semimodule R N] [is_scalar_tower R A N]
-
-/--
-For `r : R`, and `f : M →ₗ[A] N` (where `A` is an `R`-algebra) we define
-`(r • f) m = f (r • m)`.
--/
-@[priority 500]
-instance algebra_has_scalar : has_scalar R (M →ₗ[A] N) :=
-{ smul := λ r f,
-  { to_fun := λ v, r • f v,
-    map_add' := λ x y, by simp [smul_add],
-    map_smul' := λ s v, by simp [smul_smul, algebra.commutes, smul_algebra_smul_comm], } }
-
-/-- The `R`-module structure on `A`-linear maps, for `A` an `R`-algebra. -/
-@[priority 500]
-instance algebra_module : semimodule R (M →ₗ[A] N) :=
-{ one_smul := λ f, by { ext v, simp only [(•), coe_mk, one_smul] },
-  mul_smul := λ r r' f, by { ext v, simp only [(•), mul_smul, coe_mk, map_smul_eq_smul_map] },
-  smul_zero := λ r, by { ext v, simp only [(•), coe_mk, zero_apply, smul_zero] },
-  smul_add := λ r f g, by { ext v, simp only [(•), coe_mk, add_apply, smul_add] },
-  zero_smul := λ f, by { ext v, simp only [(•), coe_mk, zero_smul, map_zero, zero_apply] },
-  add_smul := λ r r' f, by { ext v, simp only [(•), add_smul, map_add, coe_mk, add_apply] } }
-
-/-
-Check that two module structures on `M →ₗ[R] N` are defeq.
-
-- On the LHS we have the new instance, defined above, and we feed it `R` as algebra over itself.
-- On the RHS we have the ordinary instance for linear maps between `R`-modules.
- -/
-example [semimodule R M] :
-  @linear_map.algebra_module R R M N _ _ _ _ _ _ _ _ _ =
-  @linear_map.semimodule R M N _ _ _ _ _ := rfl
-
-variables {R A M N}
-
-lemma algebra_module.smul_apply (c : R) (f : M →ₗ[A] N) (m : M) :
-  (c • f) m = (c • (f m) : N) :=
-by simp only [(•), coe_mk, map_smul_eq_smul_map]
-
-end linear_map
-
 section restrict_scalars
 /- In this section, we describe restriction of scalars: if `S` is an algebra over `R`, then
 `S`-modules are also `R`-modules. -/
@@ -1301,45 +1249,12 @@ variables (R : Type*) [comm_semiring R] (S : Type*) [semiring S] [algebra R S]
   (V : Type*) [add_comm_monoid V] [semimodule R V]
   (W : Type*) [add_comm_monoid W] [semimodule R W] [semimodule S W] [is_scalar_tower R S W]
 
-/-- The set of `R`-linear maps admits an `S`-action by left multiplication -/
-@[priority 500]
-instance has_scalar_extend_scalars :
-  has_scalar S (V →ₗ[R] W) :=
-{ smul := λ r f,
-  { to_fun := λ v, r • f v,
-    map_add' := by simp [smul_add],
-    map_smul' := λ c x, by rw [map_smul, smul_algebra_smul_comm] } }
-
-/-- The set of `R`-linear maps is an `S`-module-/
-@[priority 500]
-instance module_extend_scalars :
-  semimodule S (V →ₗ[R] W) :=
-{ one_smul := λ f, by { ext v, simp only [(•), coe_mk, one_smul] },
-  mul_smul := λ r r' f, by { ext v, simp only [(•), mul_smul, coe_mk, map_smul_eq_smul_map] },
-  smul_zero := λ r, by { ext v, simp only [(•), coe_mk, zero_apply, smul_zero] },
-  smul_add := λ r f g, by { ext v, simp only [(•), coe_mk, add_apply, smul_add] },
-  zero_smul := λ f, by { ext v, simp only [(•), coe_mk, zero_smul, map_zero, zero_apply] },
-  add_smul := λ r r' f, by { ext v, simp only [(•), add_smul, map_add, coe_mk, add_apply] } }
-
-/-
-Check that two module structures on `V →ₗ[R] W` are defeq.
-
-- On the LHS we have the new instance, defined above, and we feed it `R` as algebra over itself.
-- On the RHS we have the ordinary instance for linear maps between `R`-modules.
- -/
-example : @linear_map.module_extend_scalars R _ R _ _ V _ _ W _ _ _ _ =
-          @linear_map.semimodule R V W _ _ _ _ _ := rfl
-
 instance is_scalar_tower_extend_scalars :
   is_scalar_tower R S (V →ₗ[R] W) :=
 { smul_assoc := λ r s f, by simp only [(•), coe_mk, smul_assoc] }
 
 variables {R S V W}
 
-lemma smul_apply' (c : R) (f : V →ₗ[R] W) (v : V) :
-  (c • f) v = (c • (f v) : W) :=
-by simp only [(•), coe_mk, map_smul_eq_smul_map]
-
 /-- When `f` is a linear map taking values in `S`, then `λb, f b • x` is a linear map. -/
 def smul_algebra_right (f : V →ₗ[R] S) (x : W) : V →ₗ[R] W :=
 { to_fun := λb, f b • x,

src/algebra/module/linear_map.lean

@@ -120,6 +120,13 @@ variables (f g)
 
 @[simp] lemma map_smul (c : R) (x : M) : f (c • x) = c • f x := f.map_smul' c x
 
+@[simp, priority 900]
+lemma map_smul_of_tower {R S : Type*} [semiring S] [has_scalar R S] [has_scalar R M]
+  [semimodule S M] [is_scalar_tower R S M] [has_scalar R M₂] [semimodule S M₂]
+  [is_scalar_tower R S M₂] (f : M →ₗ[S] M₂) (c : R) (x : M) :
+  f (c • x) = c • f x :=
+by simp only [← smul_one_smul S c x, ← smul_one_smul S c (f x), map_smul]
+
 @[simp] lemma map_zero : f 0 = 0 :=
 by rw [← zero_smul R, map_smul f 0 0, zero_smul]
 
@@ -136,6 +143,21 @@ def to_add_monoid_hom : M →+ M₂ :=
 @[simp] lemma to_add_monoid_hom_coe :
   (f.to_add_monoid_hom : M → M₂) = f := rfl
 
+variable (R)
+
+/-- If `M` and `M₂` are both `R`-semimodules and `S`-semimodules and `R`-semimodule structures
+are defined by an action of `R` on `S` (formally, we have two scalar towers), then any `S`-linear
+map from `M` to `M₂` is `R`-linear.
+
+See also `linear_map.map_smul_of_tower`. -/
+def restrict_scalars {S : Type*} [has_scalar R S] [semiring S] [semimodule S M] [semimodule S M₂]
+  [is_scalar_tower R S M] [is_scalar_tower R S M₂] (f : M →ₗ[S] M₂) : M →ₗ[R] M₂ :=
+{ to_fun := f,
+  map_add' := f.map_add,
+  map_smul' := f.map_smul_of_tower }
+
+variable {R}
+
 @[simp] lemma map_sum {ι} {t : finset ι} {g : ι → M} :
   f (∑ i in t, g i) = (∑ i in t, f (g i)) :=
 f.to_add_monoid_hom.map_sum _ _

src/analysis/convex/basic.lean

@@ -709,7 +709,7 @@ begin
   calc
     c • f (a • x + b • y) ≤ c • (a • f x + b • f y)
       : smul_le_smul_of_nonneg (hf.2 hx hy ha hb hab) hc
-    ... = a • (c • f x) + b • (c • f y) : by simp only [smul_add, smul_comm]
+    ... = a • (c • f x) + b • (c • f y) : by simp only [smul_add, smul_comm c]
 end
 
 lemma concave_on.smul [ordered_semimodule ℝ β] {f : E → β} {c : ℝ} (hc : 0 ≤ c)

src/data/complex/module.lean

@@ -74,10 +74,6 @@ instance module.real_complex_tower (E : Type*) [add_comm_group E] [module ℂ E]
   is_scalar_tower ℝ ℂ E :=
 restrict_scalars.is_scalar_tower ℝ ℂ E
 
-instance (E : Type*) [add_comm_group E] [module ℝ E]
-  (F : Type*) [add_comm_group F] [module ℂ F] : module ℂ (E →ₗ[ℝ] F) :=
-linear_map.module_extend_scalars _ _ _ _
-
 @[priority 100]
 instance finite_dimensional.complex_to_real (E : Type*) [add_comm_group E] [module ℂ E]
   [finite_dimensional ℂ E] : finite_dimensional ℝ E :=

src/group_theory/group_action.lean

@@ -21,16 +21,27 @@ infixr ` • `:73 := has_scalar.smul
 (one_smul : ∀ b : β, (1 : α) • b = b)
 (mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b)
 
+/-- A typeclass mixin saying that two actions on the same space commute. -/
+class smul_comm_class (M N α : Type*) [has_scalar M α] [has_scalar N α] : Prop :=
+(smul_comm : ∀ (m : M) (n : N) (a : α), m • n • a = n • m • a)
+
+export mul_action (mul_smul) smul_comm_class (smul_comm)
+
+/-- Commutativity of actions is a symmetric relation. This lemma can't be an instance because this
+would cause a loop in the instance search graph. -/
+lemma smul_comm_class.symm (M N α : Type*) [has_scalar M α] [has_scalar N α]
+  [smul_comm_class M N α] : smul_comm_class N M α :=
+⟨λ a' a b, (smul_comm a a' b).symm⟩
+
+instance smul_comm_class_self (M α : Type*) [comm_monoid M] [mul_action M α] :
+  smul_comm_class M M α :=
+⟨λ a a' b, by rw [← mul_smul, mul_comm, mul_smul]⟩
+
 section
 variables [monoid α] [mul_action α β]
 
-theorem mul_smul (a₁ a₂ : α) (b : β) : (a₁ * a₂) • b = a₁ • a₂ • b := mul_action.mul_smul _ _ _
-
 lemma smul_smul (a₁ a₂ : α) (b : β) : a₁ • a₂ • b = (a₁ * a₂) • b := (mul_smul _ _ _).symm
 
-lemma smul_comm {α : Type u} {β : Type v} [comm_monoid α] [mul_action α β] (a₁ a₂ : α) (b : β) :
-  a₁ • a₂ • b = a₂ • a₁ • b := by rw [←mul_smul, ←mul_smul, mul_comm]
-
 variable (α)
 @[simp] theorem one_smul (b : β) : (1 : α) • b = b := mul_action.one_smul _
 
@@ -110,18 +121,21 @@ end
 
 section compatible_scalar
 
-variables (R M N : Type*) [has_scalar R M] [has_scalar M N] [has_scalar R N]
-
-/-- An instance of `is_scalar_tower R M N` states that the multiplicative
-action of `R` on `N` is determined by the multiplicative actions of `R` on `M`
-and `M` on `N`. -/
-class is_scalar_tower : Prop :=
-(smul_assoc : ∀ (x : R) (y : M) (z : N), (x • y) • z = x • (y • z))
-
-variables {R M N}
-
-@[simp] lemma smul_assoc [is_scalar_tower R M N] (x : R) (y : M) (z : N) :
-  (x • y) • z = x • y • z := is_scalar_tower.smul_assoc x y z
+/-- An instance of `is_scalar_tower M N α` states that the multiplicative
+action of `M` on `α` is determined by the multiplicative actions of `M` on `N`
+and `N` on `α`. -/
+class is_scalar_tower (M N α : Type*) [has_scalar M N] [has_scalar N α] [has_scalar M α] : Prop :=
+(smul_assoc : ∀ (x : M) (y : N) (z : α), (x • y) • z = x • (y • z))
+
+@[simp] lemma smul_assoc {M N} [has_scalar M N] [has_scalar N α] [has_scalar M α]
+  [is_scalar_tower M N α] (x : M) (y : N) (z : α) :
+  (x • y) • z = x • y • z :=
+is_scalar_tower.smul_assoc x y z
+
+@[simp] lemma smul_one_smul {M} (N) [monoid N] [has_scalar M N] [mul_action N α] [has_scalar M α]
+  [is_scalar_tower M N α] (x : M) (y : α) :
+  (x • (1 : N)) • y = x • y :=
+by rw [smul_assoc, one_smul]
 
 end compatible_scalar
 

src/linear_algebra/basic.lean

@@ -352,38 +352,75 @@ lemma comp_sub (g : M →ₗ[R] M₂) (h : M₂ →ₗ[R] M₃) :
 
 end add_comm_group
 
+section has_scalar
+variables {S : Type*} [semiring R] [monoid S]
+  [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃]
+  [semimodule R M] [semimodule R M₂] [semimodule R M₃]
+  [distrib_mul_action S M₂] [smul_comm_class R S M₂]
+  (f : M →ₗ[R] M₂)
+
+instance : has_scalar S (M →ₗ[R] M₂) :=
+⟨λ a f, ⟨λ b, a • f b, λ x y, by rw [f.map_add, smul_add],
+  λ c x, by simp only [f.map_smul, smul_comm c]⟩⟩
+
+@[simp] lemma smul_apply (a : S) (x : M) : (a • f) x = a • f x := rfl
+
+instance : distrib_mul_action S (M →ₗ[R] M₂) :=
+{ one_smul := λ f, ext $ λ _, one_smul _ _,
+  mul_smul := λ c c' f, ext $ λ _, mul_smul _ _ _,
+  smul_add := λ c f g, ext $ λ x, smul_add _ _ _,
+  smul_zero := λ c, ext $ λ x, smul_zero _ }
+
+theorem smul_comp (a : S) (g : M₃ →ₗ[R] M₂) (f : M →ₗ[R] M₃) : (a • g).comp f = a • (g.comp f) :=
+rfl
+
+end has_scalar
+
+section semimodule
+
+variables {S : Type*} [semiring R] [semiring S]
+  [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃]
+  [semimodule R M] [semimodule R M₂] [semimodule R M₃]
+  [semimodule S M₂] [semimodule S M₃] [smul_comm_class R S M₂] [smul_comm_class R S M₃]
+  (f : M →ₗ[R] M₂)
+
+instance : semimodule S (M →ₗ[R] M₂) :=
+{ add_smul := λ a b f, ext $ λ x, add_smul _ _ _,
+  zero_smul := λ f, ext $ λ x, zero_smul _ _ }
+
+variable (S)
+
+/-- Applying a linear map at `v : M`, seen as `S`-linear map from `M →ₗ[R] M₂` to `M₂`.
+
+ See `applyₗ` for a version where `S = R` -/
+def applyₗ' (v : M) : (M →ₗ[R] M₂) →ₗ[S] M₂ :=
+{ to_fun := λ f, f v,
+  map_add' := λ f g, f.add_apply g v,
+  map_smul' := λ x f, f.smul_apply x v }
+
+end semimodule
+
 section comm_semiring
+
 variables [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃]
 variables [semimodule R M] [semimodule R M₂] [semimodule R M₃]
 variables (f g : M →ₗ[R] M₂)
 include R
 
-instance : has_scalar R (M →ₗ[R] M₂) := ⟨λ a f,
-  ⟨λ b, a • f b, by simp [smul_add], by simp [smul_smul, mul_comm]⟩⟩
-
-@[simp] lemma smul_apply (a : R) (x : M) : (a • f) x = a • f x := rfl
-
-instance : semimodule R (M →ₗ[R] M₂) :=
-by refine { smul := (•), .. }; intros; ext; simp [smul_add, add_smul, smul_smul]
+theorem comp_smul (g : M₂ →ₗ[R] M₃) (a : R) : g.comp (a • f) = a • (g.comp f) :=
+ext $ assume b, by rw [comp_apply, smul_apply, g.map_smul]; refl
 
 /-- Composition by `f : M₂ → M₃` is a linear map from the space of linear maps `M → M₂`
 to the space of linear maps `M₂ → M₃`. -/
 def comp_right (f : M₂ →ₗ[R] M₃) : (M →ₗ[R] M₂) →ₗ[R] (M →ₗ[R] M₃) :=
-⟨linear_map.comp f,
+⟨f.comp,
 λ _ _, linear_map.ext $ λ _, f.2 _ _,
 λ _ _, linear_map.ext $ λ _, f.3 _ _⟩
 
-theorem smul_comp (g : M₂ →ₗ[R] M₃) (a : R) : (a • g).comp f = a • (g.comp f) :=
-rfl
-
-theorem comp_smul (g : M₂ →ₗ[R] M₃) (a : R) : g.comp (a • f) = a • (g.comp f) :=
-ext $ assume b, by rw [comp_apply, smul_apply, g.map_smul]; refl
-
-/-- Applying a linear map at `v : M`, seen as a linear map from `M →ₗ[R] M₂` to `M₂`. -/
+/-- Applying a linear map at `v : M`, seen as a linear map from `M →ₗ[R] M₂` to `M₂`.
+See also `linear_map.applyₗ'` for a version that works with two different semirings. -/
 def applyₗ (v : M) : (M →ₗ[R] M₂) →ₗ[R] M₂ :=
-{ to_fun := λ f, f v,
-  map_add' := λ f g, f.add_apply g v,
-  map_smul' := λ x f, f.smul_apply x v }
+applyₗ' R v
 
 end comm_semiring
 

src/linear_algebra/matrix.lean

@@ -420,7 +420,7 @@ def is_basis.det : multilinear_map R (λ i : ι, M) R :=
   end,
   map_smul' := begin
     intros u i c x,
-    simp only [he.to_matrix_update, algebra.id.smul_eq_mul, map_smul_eq_smul_map],
+    simp only [he.to_matrix_update, algebra.id.smul_eq_mul, map_smul_of_tower],
     apply det_update_column_smul
   end }
 

src/representation_theory/maschke.lean

@@ -125,7 +125,7 @@ include h
 
 lemma equivariant_projection_condition (v : V) : (π.equivariant_projection G) (i v) = v :=
 begin
-  rw [equivariant_projection, linear_map.algebra_module.smul_apply, sum_of_conjugates_equivariant,
+  rw [equivariant_projection, smul_apply, sum_of_conjugates_equivariant,
     equivariant_of_linear_of_comm_apply, sum_of_conjugates],
   rw [linear_map.sum_apply],
   simp only [conjugate_i π i h],

src/ring_theory/derivation.lean

@@ -110,10 +110,7 @@ instance derivation.Rsemimodule : semimodule R (derivation R A M) :=
 @[simp] lemma Rsmul_apply : (r • D) a = r • D a := rfl
 
 instance : semimodule A (derivation R A M) :=
-{ smul := λ a D, ⟨⟨λ b, a • D b,
-    λ a1 a2, by rw [D.map_add, smul_add],
-    λ a1 a2, by rw [D.map_smul, smul_algebra_smul_comm]⟩,
-    λ b c, by { dsimp, simp only [smul_add, leibniz, smul_comm, add_comm] }⟩,
+{ smul := λ a D, ⟨a • D, λ b c, by { dsimp, simp only [smul_add, leibniz, smul_comm a, add_comm] }⟩,
   mul_smul := λ a1 a2 D, ext $ λ b, mul_smul _ _ _,
   one_smul := λ D, ext $ λ b, one_smul A _,
   smul_add := λ a D1 D2, ext $ λ b, smul_add _ _ _,
@@ -198,7 +195,7 @@ variables [is_scalar_tower R A M] [is_scalar_tower R A N]
 def comp_der (f : M →ₗ[A] N) (D : derivation R A M) : derivation R A N :=
 { to_fun := λ a, f (D a),
   map_add' := λ a1 a2, by rw [D.map_add, f.map_add],
-  map_smul' := λ r a, by rw [derivation.map_smul, map_smul_eq_smul_map],
+  map_smul' := λ r a, by rw [derivation.map_smul, map_smul_of_tower],
   leibniz' := λ a b, by simp only [derivation.leibniz, linear_map.map_smul, linear_map.map_add, add_comm] }
 
 @[simp] lemma comp_der_apply (f : M →ₗ[A] N) (D : derivation R A M) (a : A) :