Documentation

Mathlib.Algebra.Regular.SMul

Action of regular elements on a module #

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

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∈ R is M-regular if the smultiplication map M → M→ M, defined by m ↦ a • m↦ a • m, is injective.

This property is the direct generalization to modules of the property IsLeftRegular defined in Algebra/Regular. Lemma isLeftRegular_iff shows that indeed the two notions coincide.

def IsSMulRegular {R : Type u_1} (M : Type u_2) [inst : SMul R M] (c : R) :

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

Equations

IsSMulRegular M c = Function.Injective fun x => c • x

theorem IsLeftRegular.isSMulRegular {R : Type u_1} [inst : Mul R] {c : R} (h : IsLeftRegular c) :

IsSMulRegular R c

theorem isLeftRegular_iff {R : Type u_1} [inst : Mul R] {a : R} :

IsLeftRegular a ↔ IsSMulRegular R a

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

theorem IsRightRegular.isSMulRegular {R : Type u_1} [inst : Mul R] {c : R} (h : IsRightRegular c) :

IsSMulRegular R { unop := c }

theorem isRightRegular_iff {R : Type u_1} [inst : Mul R] {a : R} :

IsRightRegular a ↔ IsSMulRegular R { unop := a }

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

theorem IsSMulRegular.smul {R : Type u_1} {S : Type u_3} {M : Type u_2} {a : R} {s : S} [inst : SMul R M] [inst : SMul R S] [inst : SMul S M] [inst : IsScalarTower R S M] (ra : IsSMulRegular M a) (rs : IsSMulRegular M s) :

IsSMulRegular M (a • s)

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

theorem IsSMulRegular.of_smul {R : Type u_3} {S : Type u_1} {M : Type u_2} {s : S} [inst : SMul R M] [inst : SMul R S] [inst : SMul S M] [inst : IsScalarTower R S M] (a : R) (ab : IsSMulRegular M (a • s)) :

IsSMulRegular 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 IsSMulRegular.smul_iff {R : Type u_1} {S : Type u_3} {M : Type u_2} {a : R} [inst : SMul R M] [inst : SMul R S] [inst : SMul S M] [inst : IsScalarTower R S M] (b : S) (ha : IsSMulRegular M a) :

IsSMulRegular M (a • b) ↔ IsSMulRegular 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 IsSMulRegular.isLeftRegular {R : Type u_1} [inst : Mul R] {a : R} (h : IsSMulRegular R a) :

IsLeftRegular a

theorem IsSMulRegular.isRightRegular {R : Type u_1} [inst : Mul R] {a : R} (h : IsSMulRegular R { unop := a }) :

IsRightRegular a

theorem IsSMulRegular.mul {R : Type u_1} {M : Type u_2} {a : R} {b : R} [inst : SMul R M] [inst : Mul R] [inst : IsScalarTower R R M] (ra : IsSMulRegular M a) (rb : IsSMulRegular M b) :

IsSMulRegular M (a * b)

theorem IsSMulRegular.of_mul {R : Type u_1} {M : Type u_2} {a : R} {b : R} [inst : SMul R M] [inst : Mul R] [inst : IsScalarTower R R M] (ab : IsSMulRegular M (a * b)) :

IsSMulRegular M b

@[simp]

theorem IsSMulRegular.mul_iff_right {R : Type u_1} {M : Type u_2} {a : R} {b : R} [inst : SMul R M] [inst : Mul R] [inst : IsScalarTower R R M] (ha : IsSMulRegular M a) :

IsSMulRegular M (a * b) ↔ IsSMulRegular M b

theorem IsSMulRegular.mul_and_mul_iff {R : Type u_1} {M : Type u_2} {a : R} {b : R} [inst : SMul R M] [inst : Mul R] [inst : IsScalarTower R R M] :

IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular 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 IsSMulRegular.one {R : Type u_1} (M : Type u_2) [inst : Monoid R] [inst : MulAction R M] :

IsSMulRegular M 1

One is always M-regular.

theorem IsSMulRegular.of_mul_eq_one {R : Type u_1} {M : Type u_2} {a : R} {b : R} [inst : Monoid R] [inst : MulAction R M] (h : a * b = 1) :

IsSMulRegular M b

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

theorem IsSMulRegular.pow {R : Type u_1} {M : Type u_2} {a : R} [inst : Monoid R] [inst : MulAction R M] (n : ℕ) (ra : IsSMulRegular M a) :

IsSMulRegular M (a ^ n)

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

theorem IsSMulRegular.pow_iff {R : Type u_1} {M : Type u_2} {a : R} [inst : Monoid R] [inst : MulAction R M] {n : ℕ} (n0 : 0 < n) :

IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a

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

theorem IsSMulRegular.of_smul_eq_one {R : Type u_2} {S : Type u_1} {M : Type u_3} {a : R} {s : S} [inst : Monoid S] [inst : SMul R M] [inst : SMul R S] [inst : MulAction S M] [inst : IsScalarTower R S M] (h : a • s = 1) :

IsSMulRegular M s

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

theorem IsSMulRegular.subsingleton {R : Type u_1} {M : Type u_2} [inst : MonoidWithZero R] [inst : Zero M] [inst : MulActionWithZero R M] (h : IsSMulRegular M 0) :

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

theorem IsSMulRegular.zero_iff_subsingleton {R : Type u_1} {M : Type u_2} [inst : MonoidWithZero R] [inst : Zero M] [inst : MulActionWithZero R M] :

IsSMulRegular M 0 ↔ Subsingleton M

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

theorem IsSMulRegular.not_zero_iff {R : Type u_1} {M : Type u_2} [inst : MonoidWithZero R] [inst : Zero M] [inst : MulActionWithZero R M] :

¬IsSMulRegular M 0 ↔ Nontrivial M

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

theorem IsSMulRegular.zero {R : Type u_2} {M : Type u_1} [inst : MonoidWithZero R] [inst : Zero M] [inst : MulActionWithZero R M] [sM : Subsingleton M] :

IsSMulRegular M 0

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

theorem IsSMulRegular.not_zero {R : Type u_2} {M : Type u_1} [inst : MonoidWithZero R] [inst : Zero M] [inst : MulActionWithZero R M] [nM : Nontrivial M] :

¬IsSMulRegular M 0

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

theorem IsSMulRegular.mul_iff {R : Type u_1} {M : Type u_2} {a : R} {b : R} [inst : CommSemigroup R] [inst : SMul R M] [inst : IsScalarTower R R M] :

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

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

theorem isSMulRegular_of_group {R : Type u_2} {G : Type u_1} [inst : Group G] [inst : MulAction G R] (g : G) :

IsSMulRegular 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 LeftCancelSMul typeclass.

theorem Units.isSMulRegular {R : Type u_1} (M : Type u_2) [inst : Monoid R] [inst : MulAction R M] (a : Rˣ) :

IsSMulRegular M ↑a

Any element in Rˣ is M-regular.

theorem IsUnit.isSMulRegular {R : Type u_1} (M : Type u_2) {a : R} [inst : Monoid R] [inst : MulAction R M] (ua : IsUnit a) :

IsSMulRegular M a

A unit is M-regular.