feat(algebra,linear_algebra): {smul,lmul,lsmul}_injective (#6588)

This PR proves a few injectivity results for (scalar) multiplication in the setting of modules and algebras over a ring.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/algebra/algebra/basic.lean

@@ -1188,6 +1188,31 @@ instance linear_map.semimodule' (R : Type u) [comm_semiring R]
 
 end algebra
 
+section ring
+
+namespace algebra
+
+variables {R A : Type*} [comm_semiring R] [ring A] [algebra R A]
+
+lemma lmul_left_injective [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
+  function.injective (lmul_left R x) :=
+by { letI : domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
+     exact mul_right_injective' hx }
+
+lemma lmul_right_injective [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
+  function.injective (lmul_right R x) :=
+by { letI : domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
+     exact mul_left_injective' hx }
+
+lemma lmul_injective [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
+  function.injective (lmul R A x) :=
+by { letI : domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
+     exact mul_right_injective' hx }
+
+end algebra
+
+end ring
+
 section nat
 
 variables (R : Type*) [semiring R]

src/algebra/algebra/tower.lean

@@ -309,3 +309,18 @@ le_antisymm (span_le.2 $ λ x hx, let ⟨p, q, hps, hqt, hpqx⟩ := set.mem_smul
 end submodule
 
 end semiring
+
+section ring
+
+namespace algebra
+
+variables [comm_semiring R] [ring A] [algebra R A]
+variables [add_comm_group M] [module A M] [semimodule R M] [is_scalar_tower R A M]
+
+lemma lsmul_injective [no_zero_smul_divisors A M] {x : A} (hx : x ≠ 0) :
+  function.injective (lsmul R M x) :=
+smul_injective hx
+
+end algebra
+
+end ring

src/algebra/group_with_zero/defs.lean

@@ -74,6 +74,12 @@ cancel_monoid_with_zero.mul_left_cancel_of_ne_zero ha h
 lemma mul_right_cancel' (hb : b ≠ 0) (h : a * b = c * b) : a = c :=
 cancel_monoid_with_zero.mul_right_cancel_of_ne_zero hb h
 
+lemma mul_right_injective' (ha : a ≠ 0) : function.injective ((*) a) :=
+λ b c, mul_left_cancel' ha
+
+lemma mul_left_injective' (hb : b ≠ 0) : function.injective (λ a, a * b) :=
+λ a c, mul_right_cancel' hb
+
 end cancel_monoid_with_zero
 
 /-- A type `M` is a commutative “monoid with zero” if it is a commutative monoid with zero

src/algebra/module/basic.lean

@@ -505,9 +505,15 @@ end nat
 
 end semimodule
 
-section module
+section add_comm_group -- `R` can still be a semiring here
+
+variables [semiring R] [add_comm_group M] [semimodule R M]
 
-variables [ring R] [add_comm_group M] [module R M]
+lemma smul_injective [no_zero_smul_divisors R M] {c : R} (hc : c ≠ 0) :
+  function.injective (λ (x : M), c • x) :=
+λ x y h, sub_eq_zero.mp ((smul_eq_zero.mp
+  (calc c • (x - y) = c • x - c • y : smul_sub c x y
+                ... = 0 : sub_eq_zero.mpr h)).resolve_left hc)
 
 section nat
 
@@ -525,7 +531,15 @@ begin
   abel
 end
 
-variables {R}
+end nat
+
+end add_comm_group
+
+section module
+
+section nat
+
+variables {R} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] [char_zero R]
 
 lemma ne_neg_of_ne_zero [no_zero_divisors R] {v : R} (hv : v ≠ 0) : v ≠ -v :=
 λ h, have semimodule ℕ R := add_comm_monoid.nat_semimodule, by exactI hv (eq_zero_of_eq_neg R h)

src/linear_algebra/tensor_product.lean

@@ -190,6 +190,16 @@ variables {R M}
 
 end comm_semiring
 
+section comm_ring
+
+variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]
+
+lemma lsmul_injective [no_zero_smul_divisors R M] {x : R} (hx : x ≠ 0) :
+  function.injective (lsmul R M x) :=
+smul_injective hx
+
+end comm_ring
+
 end linear_map
 
 section semiring