feat(ring_theory/tensor_product): the base change of a linear map alo…

…ng an algebra (#4773)

Co-authored-by: kckennylau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Oliver Nash <github@olivernash.org>

src/algebra/lie/weights.lean

@@ -110,13 +110,13 @@ begin
   let f₁ : module.End R (M₁ ⊗[R] M₂) := (to_endomorphism R L M₁ x - (χ₁ x) • 1).rtensor M₂,
   let f₂ : module.End R (M₁ ⊗[R] M₂) := (to_endomorphism R L M₂ x - (χ₂ x) • 1).ltensor M₁,
   have h_comm_square : F.comp ↑g = (g : M₁ ⊗[R] M₂ →ₗ[R] M₃).comp (f₁ + f₂),
-  { ext m₁ m₂, simp only [← g.map_lie x (m₁ ⊗ₜ m₂), add_smul, tensor_product.sub_tmul,
-      tensor_product.tmul_sub, tensor_product.smul_tmul, lie_tmul_right, tensor_product.tmul_smul,
-      to_endomorphism_apply_apply, tensor_product.mk_apply, lie_module_hom.map_smul,
-      linear_map.one_apply, lie_module_hom.coe_to_linear_map, linear_map.compr₂_apply, pi.add_apply,
-      linear_map.smul_apply, function.comp_app, linear_map.coe_comp, linear_map.rtensor_tmul,
-      lie_module_hom.map_add, linear_map.add_apply, lie_module_hom.map_sub, linear_map.sub_apply,
-      linear_map.ltensor_tmul], abel, },
+  { ext m₁ m₂, simp only [← g.map_lie x (m₁ ⊗ₜ m₂), add_smul, sub_tmul, tmul_sub, smul_tmul,
+      lie_tmul_right, tmul_smul, to_endomorphism_apply_apply, lie_module_hom.map_smul,
+      linear_map.one_apply, lie_module_hom.coe_to_linear_map, linear_map.smul_apply,
+      function.comp_app, linear_map.coe_comp, linear_map.rtensor_tmul, lie_module_hom.map_add,
+      linear_map.add_apply, lie_module_hom.map_sub, linear_map.sub_apply, linear_map.ltensor_tmul,
+      algebra_tensor_module.curry_apply, curry_apply, linear_map.to_fun_eq_coe,
+      linear_map.coe_restrict_scalars_eq_coe], abel, },
   suffices : ∃ k, ((f₁ + f₂)^k) (m₁ ⊗ₜ m₂) = 0,
   { obtain ⟨k, hk⟩ := this, use k,
     rw [← linear_map.comp_apply, linear_map.commute_pow_left_of_commute h_comm_square,
@@ -134,12 +134,9 @@ begin
   /- It's now just an application of the binomial theorem. -/
   use k₁ + k₂ - 1,
   have hf_comm : commute f₁ f₂,
-  { ext m₁ m₂,
-    simp only [smul_comm (χ₁ x) (χ₂ x), linear_map.rtensor_smul, to_endomorphism_apply_apply,
-      tensor_product.mk_apply, linear_map.mul_apply, linear_map.one_apply, linear_map.ltensor_sub,
-      linear_map.compr₂_apply, linear_map.smul_apply, linear_map.ltensor_smul,
-      linear_map.rtensor_tmul, linear_map.map_sub, linear_map.map_smul, linear_map.rtensor_sub,
-      linear_map.sub_apply, linear_map.ltensor_tmul], },
+  { ext m₁ m₂, simp only [linear_map.mul_apply, linear_map.rtensor_tmul, linear_map.ltensor_tmul,
+      algebra_tensor_module.curry_apply, linear_map.to_fun_eq_coe, linear_map.ltensor_tmul,
+      curry_apply, linear_map.coe_restrict_scalars_eq_coe], },
   rw hf_comm.add_pow',
   simp only [tensor_product.map_incl, submodule.subtype_apply, finset.sum_apply,
     submodule.coe_mk, linear_map.coe_fn_sum, tensor_product.map_tmul, linear_map.smul_apply],

src/linear_algebra/tensor_product.lean

@@ -221,8 +221,8 @@ variables {M : Type*} {N : Type*} {P : Type*} {Q : Type*} {S : Type*}
 variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q]
   [add_comm_monoid S]
 variables [module R M] [module R N] [module R P] [module R Q] [module R S]
-variables [distrib_mul_action R' M] [distrib_mul_action R' N]
-variables [module R'' M] [module R'' N]
+variables [distrib_mul_action R' M]
+variables [module R'' M]
 include R
 
 variables (M N)
@@ -325,7 +325,7 @@ Note that `module R' (M ⊗[R] N)` is available even without this typeclass on `
 needed if `tensor_product.smul_tmul`, `tensor_product.smul_tmul'`, or `tensor_product.tmul_smul` is
 used.
 -/
-class compatible_smul :=
+class compatible_smul [distrib_mul_action R' N] :=
 (smul_tmul : ∀ (r : R') (m : M) (n : N), (r • m) ⊗ₜ n = m ⊗ₜ[R] (r • n))
 
 end
@@ -334,7 +334,7 @@ end
 `mul_action.is_scalar_tower.left`. -/
 @[priority 100]
 instance compatible_smul.is_scalar_tower
-  [has_scalar R' R] [is_scalar_tower R' R M] [is_scalar_tower R' R N] :
+  [has_scalar R' R] [is_scalar_tower R' R M] [distrib_mul_action R' N] [is_scalar_tower R' R N] :
   compatible_smul R R' M N :=
 ⟨λ r m n, begin
   conv_lhs {rw ← one_smul R m},
@@ -344,7 +344,7 @@ instance compatible_smul.is_scalar_tower
 end⟩
 
 /-- `smul` can be moved from one side of the product to the other .-/
-lemma smul_tmul [compatible_smul R R' M N] (r : R') (m : M) (n : N) :
+lemma smul_tmul [distrib_mul_action R' N] [compatible_smul R R' M N] (r : R') (m : M) (n : N) :
   (r • m) ⊗ₜ n = m ⊗ₜ[R] (r • n) :=
 compatible_smul.smul_tmul _ _ _
 
@@ -356,14 +356,22 @@ theorem smul.aux_of {R' : Type*} [has_scalar R' M] (r : R') (m : M) (n : N) :
   smul.aux r (free_add_monoid.of (m, n)) = (r • m) ⊗ₜ[R] n :=
 rfl
 
-variables [smul_comm_class R R' M] [smul_comm_class R R' N]
-variables [smul_comm_class R R'' M] [smul_comm_class R R'' N]
+variables [smul_comm_class R R' M]
+variables [smul_comm_class R R'' M]
 
--- Most of the time we want the instance below this one, which is easier for typeclass resolution
--- to find. The `unused_arguments` is from one of the two comm_classes - while we only make use
--- of one, it makes sense to make the API symmetric.
-@[nolint unused_arguments]
-instance has_scalar' : has_scalar R' (M ⊗[R] N) :=
+/-- Given two modules over a commutative semiring `R`, if one of the factors carries a
+(distributive) action of a second type of scalars `R'`, which commutes with the action of `R`, then
+the tensor product (over `R`) carries an action of `R'`.
+
+This instance defines this `R'` action in the case that it is the left module which has the `R'`
+action. Two natural ways in which this situation arises are:
+ * Extension of scalars
+ * A tensor product of a group representation with a module not carrying an action
+
+Note that in the special case that `R = R'`, since `R` is commutative, we just get the usual scalar
+action on a tensor product of two modules. This special case is important enough that, for
+performance reasons, we define it explicitly below. -/
+instance left_has_scalar : has_scalar R' (M ⊗[R] N) :=
 ⟨λ r, (add_con_gen (tensor_product.eqv R M N)).lift (smul.aux r : _ →+ M ⊗[R] N) $
 add_con.add_con_gen_le $ λ x y hxy, match x, y, hxy with
 | _, _, (eqv.of_zero_left n)       := (add_con.ker_rel _).2 $
@@ -380,7 +388,7 @@ add_con.add_con_gen_le $ λ x y hxy, match x, y, hxy with
     by simp_rw [add_monoid_hom.map_add, add_comm]
 end⟩
 
-instance : has_scalar R (M ⊗[R] N) := tensor_product.has_scalar'
+instance : has_scalar R (M ⊗[R] N) := tensor_product.left_has_scalar
 
 protected theorem smul_zero (r : R') : (r • 0 : M ⊗[R] N) = 0 :=
 add_monoid_hom.map_zero _
@@ -416,9 +424,7 @@ instance : add_comm_monoid (M ⊗[R] N) :=
   nsmul_succ' := by simp [nat.succ_eq_one_add, tensor_product.one_smul, tensor_product.add_smul],
   .. tensor_product.add_comm_semigroup _ _, .. tensor_product.add_zero_class _ _}
 
--- Most of the time we want the instance below this one, which is easier for typeclass resolution
--- to find.
-instance distrib_mul_action' : distrib_mul_action R' (M ⊗[R] N) :=
+instance left_distrib_mul_action : distrib_mul_action R' (M ⊗[R] N) :=
 have ∀ (r : R') (m : M) (n : N), r • (m ⊗ₜ[R] n) = (r • m) ⊗ₜ n := λ _ _ _, rfl,
 { smul := (•),
   smul_add := λ r x y, tensor_product.smul_add r x y,
@@ -429,35 +435,30 @@ have ∀ (r : R') (m : M) (n : N), r • (m ⊗ₜ[R] n) = (r • m) ⊗ₜ n :=
   one_smul := tensor_product.one_smul,
   smul_zero := tensor_product.smul_zero }
 
-instance : distrib_mul_action R (M ⊗[R] N) := tensor_product.distrib_mul_action'
+instance : distrib_mul_action R (M ⊗[R] N) := tensor_product.left_distrib_mul_action
 
--- note that we don't actually need `compatible_smul` here, but we include it for symmetry
--- with `tmul_smul` to avoid exposing our asymmetric definition.
-@[nolint unused_arguments]
-theorem smul_tmul' [compatible_smul R R' M N] (r : R') (m : M) (n : N) :
+theorem smul_tmul' (r : R') (m : M) (n : N) :
   r • (m ⊗ₜ[R] n) = (r • m) ⊗ₜ n :=
 rfl
 
-@[simp] lemma tmul_smul [compatible_smul R R' M N] (r : R') (x : M) (y : N) :
+@[simp] lemma tmul_smul
+  [distrib_mul_action R' N] [compatible_smul R R' M N] (r : R') (x : M) (y : N) :
   x ⊗ₜ (r • y) = r • (x ⊗ₜ[R] y) :=
 (smul_tmul _ _ _).symm
 
--- Most of the time we want the instance below this one, which is easier for typeclass resolution
--- to find.
-instance module' : module R'' (M ⊗[R] N) :=
+instance left_module : module R'' (M ⊗[R] N) :=
 { smul := (•),
   add_smul := tensor_product.add_smul,
   zero_smul := tensor_product.zero_smul,
-  ..tensor_product.distrib_mul_action' }
+  ..tensor_product.left_distrib_mul_action }
 
-instance : module R (M ⊗[R] N) := tensor_product.module'
+instance : module R (M ⊗[R] N) := tensor_product.left_module
 
 section
 
 -- Like `R'`, `R'₂` provides a `distrib_mul_action R'₂ (M ⊗[R] N)`
-variables {R'₂ : Type*} [monoid R'₂] [distrib_mul_action R'₂ M] [distrib_mul_action R'₂ N]
-variables [smul_comm_class R R'₂ M] [smul_comm_class R R'₂ N]
-variables [has_scalar R'₂ R'] [compatible_smul R R' M N] [compatible_smul R R'₂ M N]
+variables {R'₂ : Type*} [monoid R'₂] [distrib_mul_action R'₂ M]
+variables [smul_comm_class R R'₂ M] [has_scalar R'₂ R']
 
 /-- `is_scalar_tower R'₂ R' M` implies `is_scalar_tower R'₂ R' (M ⊗[R] N)` -/
 instance is_scalar_tower_left [is_scalar_tower R'₂ R' M] :
@@ -467,6 +468,9 @@ instance is_scalar_tower_left [is_scalar_tower R'₂ R' M] :
   (λ m n, by rw [smul_tmul', smul_tmul', smul_tmul', smul_assoc])
   (λ x y ihx ihy, by rw [smul_add, smul_add, smul_add, ihx, ihy])⟩
 
+variables [distrib_mul_action R'₂ N] [distrib_mul_action R' N]
+variables [compatible_smul R R'₂ M N] [compatible_smul R R' M N]
+
 /-- `is_scalar_tower R'₂ R' N` implies `is_scalar_tower R'₂ R' (M ⊗[R] N)` -/
 instance is_scalar_tower_right [is_scalar_tower R'₂ R' N] :
     is_scalar_tower R'₂ R' (M ⊗[R] N) :=
@@ -479,7 +483,7 @@ end
 
 /-- A short-cut instance for the common case, where the requirements for the `compatible_smul`
 instances are sufficient. -/
-instance is_scalar_tower [has_scalar R' R] [is_scalar_tower R' R M] [is_scalar_tower R' R N] :
+instance is_scalar_tower [has_scalar R' R] [is_scalar_tower R' R M] :
   is_scalar_tower R' R (M ⊗[R] N) :=
 tensor_product.is_scalar_tower_left  -- or right
 
@@ -663,6 +667,9 @@ def curry (f : M ⊗ N →ₗ P) : M →ₗ N →ₗ P := lcurry R M N P f
 @[simp] theorem curry_apply (f : M ⊗ N →ₗ[R] P) (m : M) (n : N) :
   curry f m n = f (m ⊗ₜ n) := rfl
 
+lemma curry_injective : function.injective (curry : (M ⊗[R] N →ₗ[R] P) → (M →ₗ[R] N →ₗ[R] P)) :=
+λ g h H, mk_compr₂_inj H
+
 theorem ext_threefold {g h : (M ⊗[R] N) ⊗[R] P →ₗ[R] Q}
   (H : ∀ x y z, g ((x ⊗ₜ y) ⊗ₜ z) = h ((x ⊗ₜ y) ⊗ₜ z)) : g = h :=
 begin
@@ -904,6 +911,12 @@ by { ext m n, simp only [compr₂_apply, mk_apply, comp_apply, ltensor_tmul] }
 lemma rtensor_comp : (g.comp f).rtensor M = (g.rtensor M).comp (f.rtensor M) :=
 by { ext m n, simp only [compr₂_apply, mk_apply, comp_apply, rtensor_tmul] }
 
+lemma ltensor_mul (f g : module.End R N) : (f * g).ltensor M = (f.ltensor M) * (g.ltensor M) :=
+ltensor_comp M f g
+
+lemma rtensor_mul (f g : module.End R N) : (f * g).rtensor M = (f.rtensor M) * (g.rtensor M) :=
+rtensor_comp M f g
+
 variables (N)
 
 @[simp] lemma ltensor_id : (id : N →ₗ[R] N).ltensor M = id := map_id
@@ -1030,7 +1043,7 @@ lemma sub_tmul (m₁ m₂ : M) (n : N) : (m₁ - m₂) ⊗ₜ n = (m₁ ⊗ₜ[R
 /--
 While the tensor product will automatically inherit a ℤ-module structure from
 `add_comm_group.int_module`, that structure won't be compatible with lemmas like `tmul_smul` unless
-we use a `ℤ-module` instance provided by `tensor_product.module'`.
+we use a `ℤ-module` instance provided by `tensor_product.left_module`.
 
 When `R` is a `ring` we get the required `tensor_product.compatible_smul` instance through
 `is_scalar_tower`, but when it is only a `semiring` we need to build it from scratch.