feat(algebra/module/linear_map): `linear_(map|equiv).restrict_scalars…

…` is injective (#7725)

So as not to repeat them for the lemmas, I moved the typeclasses into a `variables` statement.

src/algebra/module/linear_map.lean

@@ -174,19 +174,32 @@ def to_add_monoid_hom : M →+ M₂ :=
 
 @[simp] lemma to_add_monoid_hom_coe : ⇑f.to_add_monoid_hom = f := rfl
 
-variable (R)
+section restrict_scalars
+
+variables (R) [semiring S] [module S M] [module S M₂] [compatible_smul M M₂ R S]
 
 /-- If `M` and `M₂` are both `R`-modules and `S`-modules and `R`-module 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*} [semiring S] [module S M] [module S M₂]
-  [compatible_smul M M₂ R S] (f : M →ₗ[S] M₂) : M →ₗ[R] M₂ :=
+@[simps]
+def restrict_scalars (f : M →ₗ[S] M₂) : M →ₗ[R] M₂ :=
 { to_fun := f,
   map_add' := f.map_add,
   map_smul' := f.map_smul_of_tower }
 
+lemma restrict_scalars_injective :
+  function.injective (restrict_scalars R : (M →ₗ[S] M₂) → (M →ₗ[R] M₂)) :=
+λ f g h, ext (linear_map.congr_fun h : _)
+
+@[simp]
+lemma restrict_scalars_inj (f g : M →ₗ[S] M₂) :
+  f.restrict_scalars R = g.restrict_scalars R ↔ f = g :=
+(restrict_scalars_injective R).eq_iff
+
+end restrict_scalars
+
 variable {R}
 
 @[simp] lemma map_sum {ι} {t : finset ι} {g : ι → M} :
@@ -555,23 +568,35 @@ def of_involutive [module R M] (f : M →ₗ[R] M) (hf : involutive f) : M ≃
   ⇑(of_involutive f hf) = f :=
 rfl
 
-variables (R)
+section restrict_scalars
+
+variables (R) [module R M] [module R M₂] [semiring S] [module S M] [module S M₂]
+  [linear_map.compatible_smul M M₂ R S]
 
 /-- 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
 equivalence from `M` to `M₂` is also an `R`-linear equivalence.
 
 See also `linear_map.restrict_scalars`. -/
 @[simps]
-def restrict_scalars [module R M] [module R M₂]
-  {S : Type*} [semiring S] [module S M] [module S M₂]
-  [linear_map.compatible_smul M M₂ R S] (f : M ≃ₗ[S] M₂) : M ≃ₗ[R] M₂ :=
+def restrict_scalars (f : M ≃ₗ[S] M₂) : M ≃ₗ[R] M₂ :=
 { to_fun := f,
   inv_fun := f.symm,
   left_inv := f.left_inv,
   right_inv := f.right_inv,
   .. f.to_linear_map.restrict_scalars R }
 
+lemma restrict_scalars_injective :
+  function.injective (restrict_scalars R : (M ≃ₗ[S] M₂) → (M ≃ₗ[R] M₂)) :=
+λ f g h, ext (linear_equiv.congr_fun h : _)
+
+@[simp]
+lemma restrict_scalars_inj (f g : M ≃ₗ[S] M₂) :
+  f.restrict_scalars R = g.restrict_scalars R ↔ f = g :=
+(restrict_scalars_injective R).eq_iff
+
+end restrict_scalars
+
 end add_comm_monoid
 
 end linear_equiv