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 on 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. Scalar multiplications involving 0 are, of course, all trivial.

The defining property is that an element a ∈ R is M-regular if the scalar multiplication map M → M, defined by 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_3) [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.

Equations

IsSMulRegular M c = Function.Injective fun (x : M) => c • x

Instances For

def IsVAddRegular {R : Type u_1} (M : Type u_3) [VAdd R M] (c : R) :

An M-regular element is an element c such that left vector addition by c is an injective map M → M.

Equations

IsVAddRegular M c = Function.Injective fun (x : M) => c +ᵥ x

Instances For

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

IsSMulRegular R c

theorem IsAddLeftRegular.isVAddRegular {R : Type u_1} [Add R] {c : R} (h : IsAddLeftRegular c) :

IsVAddRegular R c

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

IsLeftRegular a ↔ IsSMulRegular R a

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

theorem isAddLeftRegular_iff {R : Type u_1} [Add R] {a : R} :

IsAddLeftRegular a ↔ IsVAddRegular R a

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

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

IsSMulRegular R (MulOpposite.op c)

theorem IsAddRightRegular.isVAddRegular {R : Type u_1} [Add R] {c : R} (h : IsAddRightRegular c) :

IsVAddRegular R (AddOpposite.op c)

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

IsRightRegular a ↔ IsSMulRegular R (MulOpposite.op a)

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

theorem isAddRightRegular_iff {R : Type u_1} [Add R] {a : R} :

IsAddRightRegular a ↔ IsVAddRegular R (AddOpposite.op a)

Right-regular addition on R is equivalent to Rᵃᵒᵖ-regularity of R itself.

theorem isSMulRegular_map {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [SMul R M] [SMul S M] (f : R → S) (smul : ∀ (m : M), f a • m = a • m) :

IsSMulRegular M (f a) ↔ IsSMulRegular M a

theorem isVAddRegular_map {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [VAdd R M] [VAdd S M] (f : R → S) (vadd : ∀ (m : M), f a +ᵥ m = a +ᵥ m) :

IsVAddRegular M (f a) ↔ IsVAddRegular M a

theorem IsSMulRegular.of_map {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [SMul R M] [SMul S M] (f : R → S) (smul : ∀ (m : M), f a • m = a • m) :

IsSMulRegular M (f a) → IsSMulRegular M a

Alias of the forward direction of isSMulRegular_map.

theorem IsSMulRegular.map {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [SMul R M] [SMul S M] (f : R → S) (smul : ∀ (m : M), f a • m = a • m) :

IsSMulRegular M a → IsSMulRegular M (f a)

Alias of the reverse direction of isSMulRegular_map.

theorem IsVAddRegular.of_map {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [VAdd R M] [VAdd S M] (f : R → S) (vadd : ∀ (m : M), f a +ᵥ m = a +ᵥ m) :

IsVAddRegular M (f a) → IsVAddRegular M a

Alias of the forward direction of isVAddRegular_map.

theorem IsVAddRegular.map {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [VAdd R M] [VAdd S M] (f : R → S) (vadd : ∀ (m : M), f a +ᵥ m = a +ᵥ m) :

IsVAddRegular M a → IsVAddRegular M (f a)

Alias of the reverse direction of isVAddRegular_map.

theorem isAddTorsionFree_iff' {M : Type u_3} [AddMonoid M] :

IsAddTorsionFree M ↔ ∀ (n : ℕ), n ≠ 0 → IsSMulRegular M n

theorem IsSMulRegular.nat_of_isAddTorsionFree {M : Type u_3} [AddMonoid M] [IsAddTorsionFree M] {n : ℕ} (h : n ≠ 0) :

IsSMulRegular M n

@[simp]

theorem IsSMulRegular.natAbs_iff {M : Type u_3} [SubtractionMonoid M] {n : ℤ} :

IsSMulRegular M n.natAbs ↔ IsSMulRegular M n

theorem IsSMulRegular.smul {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} {s : S} [SMul R M] [SMul R S] [SMul S M] [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 IsVAddRegular.vadd {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} {s : S} [VAdd R M] [VAdd R S] [VAdd S M] [VAddAssocClass R S M] (ra : IsVAddRegular M a) (rs : IsVAddRegular M s) :

IsVAddRegular M (a +ᵥ s)

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

theorem IsSMulRegular.of_smul {R : Type u_1} {S : Type u_2} {M : Type u_3} {s : S} [SMul R M] [SMul R S] [SMul S M] [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.

theorem IsVAddRegular.of_vadd {R : Type u_1} {S : Type u_2} {M : Type u_3} {s : S} [VAdd R M] [VAdd R S] [VAdd S M] [VAddAssocClass R S M] (a : R) (ab : IsVAddRegular M (a +ᵥ s)) :

IsVAddRegular M s

If an element b becomes M-regular after left vector addition by an M-regular element, then b is M-regular.

@[simp]

theorem IsSMulRegular.smul_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [SMul R M] [SMul R S] [SMul S M] [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.

@[simp]

theorem IsVAddRegular.vadd_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [VAdd R M] [VAdd R S] [VAdd S M] [VAddAssocClass R S M] (b : S) (ha : IsVAddRegular M a) :

IsVAddRegular M (a +ᵥ b) ↔ IsVAddRegular M b

An element is M-regular if and only if left vector addition by an M-regular element is M-regular.

theorem IsSMulRegular.isLeftRegular {R : Type u_1} [Mul R] {a : R} (h : IsSMulRegular R a) :

IsLeftRegular a

theorem IsVAddRegular.isAddLeftRegular {R : Type u_1} [Add R] {a : R} (h : IsVAddRegular R a) :

IsAddLeftRegular a

theorem IsSMulRegular.isRightRegular {R : Type u_1} [Mul R] {a : R} (h : IsSMulRegular R (MulOpposite.op a)) :

IsRightRegular a

theorem IsVAddRegular.isAddRightRegular {R : Type u_1} [Add R] {a : R} (h : IsVAddRegular R (AddOpposite.op a)) :

IsAddRightRegular a

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

IsSMulRegular M (a * b)

theorem IsVAddRegular.add {R : Type u_1} {M : Type u_3} {a b : R} [VAdd R M] [Add R] [VAddAssocClass R R M] (ra : IsVAddRegular M a) (rb : IsVAddRegular M b) :

IsVAddRegular M (a + b)

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

IsSMulRegular M b

theorem IsVAddRegular.of_add {R : Type u_1} {M : Type u_3} {a b : R} [VAdd R M] [Add R] [VAddAssocClass R R M] (ab : IsVAddRegular M (a + b)) :

IsVAddRegular M b

@[simp]

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

IsSMulRegular M (a * b) ↔ IsSMulRegular M b

@[simp]

theorem IsVAddRegular.add_iff_right {R : Type u_1} {M : Type u_3} {a b : R} [VAdd R M] [Add R] [VAddAssocClass R R M] (ha : IsVAddRegular M a) :

IsVAddRegular M (a + b) ↔ IsVAddRegular M b

theorem IsSMulRegular.mul_and_mul_iff {R : Type u_1} {M : Type u_3} {a b : R} [SMul R M] [Mul R] [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.

theorem IsVAddRegular.add_and_add_iff {R : Type u_1} {M : Type u_3} {a b : R} [VAdd R M] [Add R] [VAddAssocClass R R M] :

IsVAddRegular M (a + b) ∧ IsVAddRegular M (b + a) ↔ IsVAddRegular M a ∧ IsVAddRegular M b

Two elements a and b are M-regular if and only if both sums a + b and b + a are M-regular.

@[simp]

theorem IsSMulRegular.one {R : Type u_1} (M : Type u_3) [Monoid R] [MulAction R M] :

IsSMulRegular M 1

One is always M-regular.

@[simp]

theorem IsVAddRegular.zero {R : Type u_1} (M : Type u_3) [AddMonoid R] [AddAction R M] :

IsVAddRegular M 0

Zero is always M-regular.

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

IsSMulRegular M b

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

theorem IsVAddRegular.of_add_eq_zero {R : Type u_1} {M : Type u_3} {a b : R} [AddMonoid R] [AddAction R M] (h : a + b = 0) :

IsVAddRegular M b

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

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

IsSMulRegular M (a ^ n)

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

theorem IsVAddRegular.nsmul {R : Type u_1} {M : Type u_3} {a : R} [AddMonoid R] [AddAction R M] (n : ℕ) (ra : IsVAddRegular M a) :

IsVAddRegular M (n • a)

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

theorem IsSMulRegular.pow_iff {R : Type u_1} {M : Type u_3} {a : R} [Monoid R] [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 IsVAddRegular.nsmul_iff {R : Type u_1} {M : Type u_3} {a : R} [AddMonoid R] [AddAction R M] {n : ℕ} (n0 : 0 < n) :

IsVAddRegular M (n • a) ↔ IsVAddRegular M a

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

theorem IsSMulRegular.of_smul_eq_one {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} {s : S} [Monoid S] [SMul R M] [SMul R S] [MulAction S M] [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 IsVAddRegular.of_vadd_eq_zero {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} {s : S} [AddMonoid S] [VAdd R M] [VAdd R S] [AddAction S M] [VAddAssocClass R S M] (h : a +ᵥ s = 0) :

IsVAddRegular M s

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

theorem IsSMulRegular.mul_iff {R : Type u_1} {M : Type u_3} {a b : R} [CommSemigroup R] [SMul R M] [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 IsVAddRegular.add_iff {R : Type u_1} {M : Type u_3} {a b : R} [AddCommSemigroup R] [VAdd R M] [VAddAssocClass R R M] :

IsVAddRegular M (a + b) ↔ IsVAddRegular M a ∧ IsVAddRegular M b

A sum is M-regular if and only if the summands are.

theorem IsSMulRegular.all {R : Type u_1} {M : Type u_3} [SMul R M] [IsLeftCancelSMul R M] (a : R) :

IsSMulRegular M a

If scalar multiplication is left cancellative, every element is regular.

theorem IsVAddRegular.all {R : Type u_1} {M : Type u_3} [VAdd R M] [IsLeftCancelVAdd R M] (a : R) :

IsVAddRegular M a

If left vector addition is cancellative, every element is regular.

@[deprecated IsSMulRegular.all (since := "2026-09-08")]

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

IsSMulRegular R g

An element of a group acting on a type is regular.

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

IsSMulRegular M ↑a

Any element in Rˣ is M-regular.

theorem AddUnits.isVAddRegular {R : Type u_1} (M : Type u_3) [AddMonoid R] [AddAction R M] (a : AddUnits R) :

IsVAddRegular M ↑a

Any element in AddUnits R is M-regular.

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

IsSMulRegular M a

A unit is M-regular.

theorem IsAddUnit.isVAddRegular {R : Type u_1} (M : Type u_3) {a : R} [AddMonoid R] [AddAction R M] (ua : IsAddUnit a) :

IsVAddRegular M a

An additive unit is M-regular.

theorem Equiv.isSMulRegular_congr {R : Type u_4} {S : Type u_5} {M : Type u_6} {M' : Type u_7} [SMul R M] [SMul S M'] {e : M ≃ M'} {r : R} {s : S} (h : ∀ (x : M), e (r • x) = s • e x) :

IsSMulRegular M r ↔ IsSMulRegular M' s

theorem Equiv.isVAddRegular_congr {R : Type u_4} {S : Type u_5} {M : Type u_6} {M' : Type u_7} [VAdd R M] [VAdd S M'] {e : M ≃ M'} {r : R} {s : S} (h : ∀ (x : M), e (r +ᵥ x) = s +ᵥ e x) :

IsVAddRegular M r ↔ IsVAddRegular M' s