feat(algebra/*, * : [regular, smul_with_zero, module/basic]): introdu…

…ce `mul_action_with_zero` and `M`-regular elements (#6590)

This PR has been split and there are now two separate PRs.

* #6590, this one, introducing `smul_with_zero` and `mul_action_with_zero`: two typeclasses to deal with multiplicative actions of `monoid_with_zero`, without the need to assume the presence of an addition!
* #6659, introducing `M`-regular elements, called `smul_regular`: the analogue of `is_left_regular`, but defined for an action of `monoid_with_zero` on a module `M`.


This PR is a preparation for introducing `M`-regular elements.

From the doc-string:

### Introduce `smul_with_zero`

In analogy with the usual monoid action on a Type `M`, we introduce an action of a `monoid_with_zero` on a Type with `0`.

In particular, for Types `R` and `M`, both containing `0`, we define `smul_with_zero R M` to be the typeclass where the products `r • 0` and `0 • m` vanish for all `r ∈ R` and all `m ∈ M`.

Moreover, in the case in which `R` is a `monoid_with_zero`, we introduce the typeclass `mul_action_with_zero R M`, mimicking group actions and having an absorbing `0` in `R`.  Thus, the action is required to be compatible with

* the unit of the monoid, acting as the identity;
* the zero of the monoid_with_zero, acting as zero;
* associativity of the monoid.

Next, in a separate file, I introduce `M`-regular elements for a `monoid_with_zero R` with a `mul_action_with_zero` on a module `M`.  The definition is simply to require that an element `a : R` is `M`-regular if the smultiplication `M → M`, given by `m ↦ a • m` is injective.

We also prove some basic facts about `M`-regular elements.

The PR further changes three further the files

* `data/polynomial/coeffs`;
* `topology/algebra/module.lean`;
* `analysis/normed_space/bounded_linear_maps`.

The changes are prompted by a failure in CI.  In each case, the change was tiny, mostly having to do with an exchange of a multiplication by a smultiplication or vice-versa.



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

src/algebra/module/basic.lean

@@ -5,18 +5,16 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import algebra.big_operators.basic
 import algebra.group.hom
-import algebra.ring.basic
-import data.rat.cast
 import group_theory.group_action.group
-import tactic.nth_rewrite
+import algebra.smul_with_zero
 
 /-!
 # Modules over a ring
 
 In this file we define
 
 * `semimodule R M` : an additive commutative monoid `M` is a `semimodule` over a
-  `semiring` `R` if for `r : R` and `x : M` their "scalar multiplication `r • x : M` is defined, and
+  `semiring R` if for `r : R` and `x : M` their "scalar multiplication `r • x : M` is defined, and
   the operation `•` satisfies some natural associativity and distributivity axioms similar to those
   on a ring.
 
@@ -57,9 +55,16 @@ variables {R : Type u} {k : Type u'} {S : Type v} {M : Type w} {M₂ : Type x} {
 section add_comm_monoid
 variables [semiring R] [add_comm_monoid M] [semimodule R M] (r s : R) (x y : M)
 
+/-- A semimodule over a semiring automatically inherits a `mul_action_with_zero` structure. -/
+@[priority 100] -- see Note [lower instance priority]
+instance semimodule.to_mul_action_with_zero :
+  mul_action_with_zero R M :=
+{ smul_zero := smul_zero,
+  zero_smul := semimodule.zero_smul,
+  ..(infer_instance : mul_action R M) }
+
 theorem add_smul : (r + s) • x = r • x + s • x := semimodule.add_smul r s x
 variables (R)
-@[simp] theorem zero_smul : (0 : R) • x = 0 := semimodule.zero_smul x
 
 theorem two_smul : (2 : R) • x = x + x := by rw [bit0, add_smul, one_smul]
 

src/algebra/regular.lean

@@ -227,6 +227,18 @@ end
 lemma is_regular.ne_zero [nontrivial R] (la : is_regular a) : a ≠ 0 :=
 la.left.ne_zero
 
+/--  In a non-trivial ring, the element `0` is not left-regular -- with typeclasses. -/
+lemma not_is_left_regular_zero [nR : nontrivial R] : ¬ is_left_regular (0 : R) :=
+not_is_left_regular_zero_iff.mpr nR
+
+/--  In a non-trivial ring, the element `0` is not right-regular -- with typeclasses. -/
+lemma not_is_right_regular_zero [nR : nontrivial R] : ¬ is_right_regular (0 : R) :=
+not_is_right_regular_zero_iff.mpr nR
+
+/--  In a non-trivial ring, the element `0` is not regular -- with typeclasses. -/
+lemma not_is_regular_zero [nontrivial R] : ¬ is_regular (0 : R) :=
+λ h, is_regular.ne_zero h rfl
+
 end mul_zero_class
 
 section comm_semigroup

src/algebra/smul_with_zero.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2021 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+import group_theory.group_action.defs
+/-!
+# Introduce `smul_with_zero`
+
+In analogy with the usual monoid action on a Type `M`, we introduce an action of a
+`monoid_with_zero` on a Type with `0`.
+
+In particular, for Types `R` and `M`, both containing `0`, we define `smul_with_zero R M` to
+be the typeclass where the products `r • 0` and `0 • m` vanish for all `r : R` and all `m : M`.
+
+Moreover, in the case in which `R` is a `monoid_with_zero`, we introduce the typeclass
+`mul_action_with_zero R M`, mimicking group actions and having an absorbing `0` in `R`.
+Thus, the action is required to be compatible with
+
+* the unit of the monoid, acting as the identity;
+* the zero of the monoid_with_zero, acting as zero;
+* associativity of the monoid.
+
+We also add `instances`:
+
+* any `monoid_with_zero` has a `mul_action_with_zero R R` acting on itself;
+-/
+
+variables (R M : Type*)
+
+section has_zero
+
+variable [has_zero M]
+
+/--  `smul_with_zero` is a class consisting of a Type `R` with `0 : R` and a scalar multiplication
+of `R` on a Type `M` with `0`, such that the equality `r • m = 0` holds if at least one among `r`
+or `m` equals `0`. -/
+class smul_with_zero [has_zero R] extends has_scalar R M :=
+(smul_zero : ∀ r : R, r • (0 : M) = 0)
+(zero_smul : ∀ m : M, (0 : R) • m = 0)
+
+variables {M}
+
+@[simp] lemma zero_smul [has_zero R] [smul_with_zero R M] (m : M) :
+  (0 : R) • m = 0 :=
+smul_with_zero.zero_smul m
+
+variables (M)
+
+section monoid_with_zero
+
+variable [monoid_with_zero R]
+
+/--  An action of a monoid with zero `R` on a Type `M`, also with `0`, compatible with `0`
+(both in `R` and in `M`), with `1 ∈ R`, and with associativity of multiplication on the
+monoid `M`. -/
+class mul_action_with_zero extends mul_action R M :=
+-- these fields are copied from `smul_with_zero`, as `extends` behaves poorly
+(smul_zero : ∀ r : R, r • (0 : M) = 0)
+(zero_smul : ∀ m : M, (0 : R) • m = 0)
+
+@[priority 100] -- see Note [lower instance priority]
+instance mul_action_with_zero.to_smul_with_zero [m : mul_action_with_zero R M] :
+  smul_with_zero R M :=
+{..m}
+
+instance monoid_with_zero.to_mul_action_with_zero : mul_action_with_zero R R :=
+{ smul_zero := mul_zero,
+  zero_smul := zero_mul,
+  ..monoid.to_mul_action R }
+
+end monoid_with_zero
+
+end has_zero

src/analysis/normed_space/bounded_linear_maps.lean

@@ -279,7 +279,7 @@ lemma is_bounded_bilinear_map_smul {𝕜' : Type*} [normed_field 𝕜']
 
 lemma is_bounded_bilinear_map_mul :
   is_bounded_bilinear_map 𝕜 (λ (p : 𝕜 × 𝕜), p.1 * p.2) :=
-is_bounded_bilinear_map_smul
+by simp_rw ← smul_eq_mul; exact is_bounded_bilinear_map_smul
 
 lemma is_bounded_bilinear_map_comp :
   is_bounded_bilinear_map 𝕜 (λ(p : (E →L[𝕜] F) × (F →L[𝕜] G)), p.2.comp p.1) :=

src/data/polynomial/coeff.lean

@@ -178,7 +178,7 @@ begin
   rw [← f.sum_single] {occs := occurrences.pos [1]},
   refine sum_mem _ (λ i hi, _),
   change monomial i _ ∈ span _ _,
-  rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul],
+  rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← smul_eq_mul],
   exact smul_mem _ _ (subset_span ⟨i, rfl⟩),
 end
 

src/topology/algebra/module.lean

@@ -820,7 +820,7 @@ variables [has_continuous_add M₂]
 instance : semimodule S (M →L[R] M₂) :=
 { smul_zero := λ _, ext $ λ _, smul_zero _,
   zero_smul := λ _, ext $ λ _, zero_smul _ _,
-  one_smul  := λ _, ext $ λ _, one_smul _ _,
+  one_smul  := λ _, ext $ λ _, by exact one_smul _ _,
   mul_smul  := λ _ _ _, ext $ λ _, mul_smul _ _ _,
   add_smul  := λ _ _ _, ext $ λ _, add_smul _ _ _,
   smul_add  := λ _ _ _, ext $ λ _, smul_add _ _ _ }