mathlib3 documentation

algebra.regular.smul

Action of regular elements on a module #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We introduce M-regular elements, in the context of an R-module M. The corresponding predicate is called is_smul_regular.

There are very limited typeclass assumptions on R and M, but the "mathematical" case of interest is a commutative ring R acting an a module M. Since the properties are "multiplicative", there is no actual requirement of having an addition, but there is a zero in both R and M. Smultiplications involving 0 are, of course, all trivial.

The defining property is that an element a ∈ R is M-regular if the smultiplication map M → M, defined by m ↦ a • m, is injective.

This property is the direct generalization to modules of the property is_left_regular defined in algebra/regular. Lemma is_smul_regular.is_left_regular_iff shows that indeed the two notions coincide.

def is_smul_regular {R : Type u_1} (M : Type u_3) [has_smul R M] (c : R) :

Prop

An M-regular element is an element c such that multiplication on the left by c is an injective map M → M.

Equations

is_smul_regular M c = function.injective (has_smul.smul c)

theorem is_left_regular.is_smul_regular {R : Type u_1} [has_mul R] {c : R} (h : is_left_regular c) :

is_smul_regular R c

theorem is_left_regular_iff {R : Type u_1} [has_mul R] {a : R} :

is_left_regular a ↔ is_smul_regular R a

Left-regular multiplication on R is equivalent to R-regularity of R itself.

theorem is_right_regular.is_smul_regular {R : Type u_1} [has_mul R] {c : R} (h : is_right_regular c) :

is_smul_regular R (mul_opposite.op c)

theorem is_right_regular_iff {R : Type u_1} [has_mul R] {a : R} :

is_right_regular a ↔ is_smul_regular R (mul_opposite.op a)

Right-regular multiplication on R is equivalent to Rᵐᵒᵖ-regularity of R itself.

theorem is_smul_regular.smul {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} {s : S} [has_smul R M] [has_smul R S] [has_smul S M] [is_scalar_tower R S M] (ra : is_smul_regular M a) (rs : is_smul_regular M s) :

is_smul_regular M (a • s)

The product of M-regular elements is M-regular.

theorem is_smul_regular.of_smul {R : Type u_1} {S : Type u_2} {M : Type u_3} {s : S} [has_smul R M] [has_smul R S] [has_smul S M] [is_scalar_tower R S M] (a : R) (ab : is_smul_regular M (a • s)) :

is_smul_regular M s

If an element b becomes M-regular after multiplying it on the left by an M-regular element, then b is M-regular.

@[simp]

theorem is_smul_regular.smul_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [has_smul R M] [has_smul R S] [has_smul S M] [is_scalar_tower R S M] (b : S) (ha : is_smul_regular M a) :

is_smul_regular M (a • b) ↔ is_smul_regular M b

An element is M-regular if and only if multiplying it on the left by an M-regular element is M-regular.

theorem is_smul_regular.is_left_regular {R : Type u_1} [has_mul R] {a : R} (h : is_smul_regular R a) :

is_left_regular a

theorem is_smul_regular.is_right_regular {R : Type u_1} [has_mul R] {a : R} (h : is_smul_regular R (mul_opposite.op a)) :

is_right_regular a

theorem is_smul_regular.mul {R : Type u_1} {M : Type u_3} {a b : R} [has_smul R M] [has_mul R] [is_scalar_tower R R M] (ra : is_smul_regular M a) (rb : is_smul_regular M b) :

is_smul_regular M (a * b)

theorem is_smul_regular.of_mul {R : Type u_1} {M : Type u_3} {a b : R} [has_smul R M] [has_mul R] [is_scalar_tower R R M] (ab : is_smul_regular M (a * b)) :

is_smul_regular M b

@[simp]

theorem is_smul_regular.mul_iff_right {R : Type u_1} {M : Type u_3} {a b : R} [has_smul R M] [has_mul R] [is_scalar_tower R R M] (ha : is_smul_regular M a) :

is_smul_regular M (a * b) ↔ is_smul_regular M b

theorem is_smul_regular.mul_and_mul_iff {R : Type u_1} {M : Type u_3} {a b : R} [has_smul R M] [has_mul R] [is_scalar_tower R R M] :

is_smul_regular M (a * b) ∧ is_smul_regular M (b * a) ↔ is_smul_regular M a ∧ is_smul_regular M b

Two elements a and b are M-regular if and only if both products a * b and b * a are M-regular.

@[simp]

theorem is_smul_regular.one {R : Type u_1} (M : Type u_3) [monoid R] [mul_action R M] :

is_smul_regular M 1

One is M-regular always.

theorem is_smul_regular.of_mul_eq_one {R : Type u_1} {M : Type u_3} {a b : R} [monoid R] [mul_action R M] (h : a * b = 1) :

is_smul_regular M b

An element of R admitting a left inverse is M-regular.

theorem is_smul_regular.pow {R : Type u_1} {M : Type u_3} {a : R} [monoid R] [mul_action R M] (n : ℕ) (ra : is_smul_regular M a) :

is_smul_regular M (a ^ n)

Any power of an M-regular element is M-regular.

theorem is_smul_regular.pow_iff {R : Type u_1} {M : Type u_3} {a : R} [monoid R] [mul_action R M] {n : ℕ} (n0 : 0 < n) :

is_smul_regular M (a ^ n) ↔ is_smul_regular M a

An element a is M-regular if and only if a positive power of a is M-regular.

theorem is_smul_regular.of_smul_eq_one {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} {s : S} [monoid S] [has_smul R M] [has_smul R S] [mul_action S M] [is_scalar_tower R S M] (h : a • s = 1) :

is_smul_regular M s

An element of S admitting a left inverse in R is M-regular.

@[protected]

theorem is_smul_regular.subsingleton {R : Type u_1} {M : Type u_3} [monoid_with_zero R] [has_zero M] [mul_action_with_zero R M] (h : is_smul_regular M 0) :

The element 0 is M-regular if and only if M is trivial.

theorem is_smul_regular.zero_iff_subsingleton {R : Type u_1} {M : Type u_3} [monoid_with_zero R] [has_zero M] [mul_action_with_zero R M] :

is_smul_regular M 0 ↔ subsingleton M

The element 0 is M-regular if and only if M is trivial.

theorem is_smul_regular.not_zero_iff {R : Type u_1} {M : Type u_3} [monoid_with_zero R] [has_zero M] [mul_action_with_zero R M] :

¬is_smul_regular M 0 ↔ nontrivial M

The 0 element is not M-regular, on a non-trivial module.

theorem is_smul_regular.zero {R : Type u_1} {M : Type u_3} [monoid_with_zero R] [has_zero M] [mul_action_with_zero R M] [sM : subsingleton M] :

is_smul_regular M 0

The element 0 is M-regular when M is trivial.

theorem is_smul_regular.not_zero {R : Type u_1} {M : Type u_3} [monoid_with_zero R] [has_zero M] [mul_action_with_zero R M] [nM : nontrivial M] :

¬is_smul_regular M 0

The 0 element is not M-regular, on a non-trivial module.

theorem is_smul_regular.mul_iff {R : Type u_1} {M : Type u_3} {a b : R} [comm_semigroup R] [has_smul R M] [is_scalar_tower R R M] :

is_smul_regular M (a * b) ↔ is_smul_regular M a ∧ is_smul_regular M b

A product is M-regular if and only if the factors are.

theorem is_smul_regular_of_group {R : Type u_1} {G : Type u_4} [group G] [mul_action G R] (g : G) :

is_smul_regular R g

An element of a group acting on a Type is regular. This relies on the availability of the inverse given by groups, since there is no left_cancel_smul typeclass.

theorem units.is_smul_regular {R : Type u_1} (M : Type u_3) [monoid R] [mul_action R M] (a : Rˣ) :

is_smul_regular M ↑a

Any element in Rˣ is M-regular.

theorem is_unit.is_smul_regular {R : Type u_1} (M : Type u_3) {a : R} [monoid R] [mul_action R M] (ua : is_unit a) :

is_smul_regular M a

A unit is M-regular.