Mathlib.Algebra.Regular.SMul

IsSMulRegular definition

[SMul R M] (c : R)

Full source

/-- An `M`-regular element is an element `c` such that multiplication on the left by `c` is an
injective map `M → M`. -/
def IsSMulRegular [SMul R M] (c : R) :=
  Function.Injective ((c • ·) : M → M)

$ M $-regular element

Informal description

An element $ c $ of a type $ R $ is called $ M $-regular if the scalar multiplication map $ M \to M $ defined by $ m \mapsto c \bullet m $ is injective. Here, $ R $ is equipped with a scalar multiplication operation on $ M $.

IsLeftRegular.isSMulRegular theorem

[Mul R] {c : R} (h : IsLeftRegular c) : IsSMulRegular R c

Full source

theorem IsLeftRegular.isSMulRegular [Mul R] {c : R} (h : IsLeftRegular c) : IsSMulRegular R c :=
  h

Left regularity implies scalar regularity

Informal description

Let $R$ be a type with a multiplication operation. If an element $c \in R$ is left regular (i.e., left multiplication by $c$ is injective), then $c$ is $R$-regular (i.e., scalar multiplication by $c$ on $R$ is injective).

isLeftRegular_iff theorem

[Mul R] {a : R} : IsLeftRegular a ↔ IsSMulRegular R a

Full source

/-- Left-regular multiplication on `R` is equivalent to `R`-regularity of `R` itself. -/
theorem isLeftRegular_iff [Mul R] {a : R} : IsLeftRegularIsLeftRegular a ↔ IsSMulRegular R a :=
  Iff.rfl

Equivalence of Left Regularity and Scalar Regularity in $R$

Informal description

Let $R$ be a type with a multiplication operation. An element $a \in R$ is left regular (i.e., left multiplication by $a$ is injective) if and only if $a$ is $R$-regular (i.e., scalar multiplication by $a$ on $R$ is injective).

IsRightRegular.isSMulRegular theorem

[Mul R] {c : R} (h : IsRightRegular c) : IsSMulRegular R (MulOpposite.op c)

Full source

theorem IsRightRegular.isSMulRegular [Mul R] {c : R} (h : IsRightRegular c) :
    IsSMulRegular R (MulOpposite.op c) :=
  h

Right regularity implies opposite scalar regularity

Informal description

Let $R$ be a type with a multiplication operation. If an element $c \in R$ is right regular (i.e., right multiplication by $c$ is injective), then the element $\text{op}(c)$ in the multiplicative opposite $R^\text{op}$ is $R$-regular (i.e., scalar multiplication by $\text{op}(c)$ on $R$ is injective).

isRightRegular_iff theorem

[Mul R] {a : R} : IsRightRegular a ↔ IsSMulRegular R (MulOpposite.op a)

Full source

/-- Right-regular multiplication on `R` is equivalent to `Rᵐᵒᵖ`-regularity of `R` itself. -/
theorem isRightRegular_iff [Mul R] {a : R} :
    IsRightRegularIsRightRegular a ↔ IsSMulRegular R (MulOpposite.op a) :=
  Iff.rfl

Equivalence of Right Regularity and Opposite Scalar Regularity

Informal description

Let $R$ be a type with a multiplication operation. An element $a \in R$ is right regular (i.e., right multiplication by $a$ is injective) if and only if the element $\text{op}(a)$ in the multiplicative opposite $R^\text{op}$ is $R$-regular (i.e., scalar multiplication by $\text{op}(a)$ on $R$ is injective).

IsSMulRegular.smul theorem

(ra : IsSMulRegular M a) (rs : IsSMulRegular M s) : IsSMulRegular M (a • s)

Full source

/-- The product of `M`-regular elements is `M`-regular. -/
theorem smul (ra : IsSMulRegular M a) (rs : IsSMulRegular M s) : IsSMulRegular M (a • s) :=
  fun _ _ ab => rs (ra ((smul_assoc _ _ _).symm.trans (ab.trans (smul_assoc _ _ _))))

Product of $M$-regular elements is $M$-regular

Informal description

Let $R$ be a type equipped with a scalar multiplication operation on a type $M$, and let $a, s \in R$. If $a$ is $M$-regular and $s$ is $M$-regular, then the scalar product $a \bullet s$ is also $M$-regular.

IsSMulRegular.of_smul theorem

(a : R) (ab : IsSMulRegular M (a • s)) : IsSMulRegular M s

Full source

/-- If an element `b` becomes `M`-regular after multiplying it on the left by an `M`-regular
element, then `b` is `M`-regular. -/
theorem of_smul (a : R) (ab : IsSMulRegular M (a • s)) : IsSMulRegular M s :=
  @Function.Injective.of_comp _ _ _ (fun m : M => a • m) _ fun c d cd => by
  dsimp only [Function.comp_def] at cd
  rw [← smul_assoc, ← smul_assoc] at cd
  exact ab cd

Regularity of Scalar Factor Implies Regularity of Element

Informal description

Let $R$ be a type equipped with a scalar multiplication operation on a type $M$, and let $a, s \in R$. If the scalar product $a \bullet s$ is $M$-regular (i.e., the map $m \mapsto (a \bullet s) \bullet m$ is injective), then $s$ is $M$-regular.

IsSMulRegular.smul_iff theorem

(b : S) (ha : IsSMulRegular M a) : IsSMulRegular M (a • b) ↔ IsSMulRegular M b

Full source

/-- An element is `M`-regular if and only if multiplying it on the left by an `M`-regular element
is `M`-regular. -/
@[simp]
theorem smul_iff (b : S) (ha : IsSMulRegular M a) : IsSMulRegularIsSMulRegular M (a • b) ↔ IsSMulRegular M b :=
  ⟨of_smul _, ha.smul⟩

Equivalence of $M$-regularity for scalar product $a \bullet b$ and $b$ when $a$ is $M$-regular

Informal description

Let $R$ be a type equipped with a scalar multiplication operation on a type $M$, and let $a \in R$ be $M$-regular. For any $b \in S$, the scalar product $a \bullet b$ is $M$-regular if and only if $b$ is $M$-regular.

IsSMulRegular.isLeftRegular theorem

[Mul R] {a : R} (h : IsSMulRegular R a) : IsLeftRegular a

Full source

theorem isLeftRegular [Mul R] {a : R} (h : IsSMulRegular R a) : IsLeftRegular a :=
  h

$R$-regular elements are left-regular

Informal description

Let $R$ be a type equipped with a multiplication operation, and let $a \in R$. If the scalar multiplication map $R \to R$ defined by $x \mapsto a \bullet x$ is injective (i.e., $a$ is $R$-regular), then $a$ is left-regular, meaning that for all $x, y \in R$, $a * x = a * y$ implies $x = y$.

IsSMulRegular.isRightRegular theorem

[Mul R] {a : R} (h : IsSMulRegular R (MulOpposite.op a)) : IsRightRegular a

Full source

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

$R$-regularity in the opposite implies right-regularity

Informal description

Let $R$ be a type equipped with a multiplication operation, and let $a \in R$. If the element $\text{op}(a)$ in the multiplicative opposite $R^\text{op}$ is $R$-regular (i.e., the scalar multiplication map $R \to R$ defined by $x \mapsto \text{op}(a) \bullet x$ is injective), then $a$ is right-regular, meaning that for all $x, y \in R$, $x * a = y * a$ implies $x = y$.

IsSMulRegular.mul theorem

[Mul R] [IsScalarTower R R M] (ra : IsSMulRegular M a) (rb : IsSMulRegular M b) : IsSMulRegular M (a * b)

Full source

theorem mul [Mul R] [IsScalarTower R R M] (ra : IsSMulRegular M a) (rb : IsSMulRegular M b) :
    IsSMulRegular M (a * b) :=
  ra.smul rb

Product of $M$-regular elements is $M$-regular under scalar multiplication tower property

Informal description

Let $R$ be a type equipped with a multiplication operation and a scalar multiplication action on a type $M$, such that the scalar multiplication satisfies the tower property (i.e., $(a * b) \bullet m = a \bullet (b \bullet m)$ for all $a, b \in R$ and $m \in M$). If $a$ and $b$ are $M$-regular elements (i.e., the maps $m \mapsto a \bullet m$ and $m \mapsto b \bullet m$ are injective), then their product $a * b$ is also $M$-regular.

IsSMulRegular.of_mul theorem

[Mul R] [IsScalarTower R R M] (ab : IsSMulRegular M (a * b)) : IsSMulRegular M b

Full source

theorem of_mul [Mul R] [IsScalarTower R R M] (ab : IsSMulRegular M (a * b)) :
    IsSMulRegular M b := by
  rw [← smul_eq_mul] at ab
  exact ab.of_smul _

Regularity of Product Implies Regularity of Right Factor in Scalar Multiplication Tower

Informal description

Let $R$ be a type equipped with a multiplication operation and a scalar multiplication action on a type $M$, such that the scalar multiplication satisfies the tower property (i.e., $(a * b) \bullet m = a \bullet (b \bullet m)$ for all $a, b \in R$ and $m \in M$). If the product $a * b$ is $M$-regular (i.e., the map $m \mapsto (a * b) \bullet m$ is injective), then $b$ is $M$-regular.

IsSMulRegular.mul_iff_right theorem

[Mul R] [IsScalarTower R R M] (ha : IsSMulRegular M a) : IsSMulRegular M (a * b) ↔ IsSMulRegular M b

Full source

@[simp]
theorem mul_iff_right [Mul R] [IsScalarTower R R M] (ha : IsSMulRegular M a) :
    IsSMulRegularIsSMulRegular M (a * b) ↔ IsSMulRegular M b :=
  ⟨of_mul, ha.mul⟩

Product of $M$-regular elements is $M$-regular if and only if right factor is $M$-regular

Informal description

Let $R$ be a type with a multiplication operation and a scalar multiplication action on a type $M$, such that the scalar multiplication satisfies the tower property (i.e., $(a * b) \bullet m = a \bullet (b \bullet m)$ for all $a, b \in R$ and $m \in M$). If $a$ is $M$-regular (i.e., the map $m \mapsto a \bullet m$ is injective), then the product $a * b$ is $M$-regular if and only if $b$ is $M$-regular.

IsSMulRegular.mul_and_mul_iff theorem

 [Mul R] [IsScalarTower R R M] :
  IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b

Full source

/-- Two elements `a` and `b` are `M`-regular if and only if both products `a * b` and `b * a`
are `M`-regular. -/
theorem mul_and_mul_iff [Mul R] [IsScalarTower R R M] :
    IsSMulRegularIsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b := by
  refine ⟨?_, ?_⟩
  · rintro ⟨ab, ba⟩
    exact ⟨ba.of_mul, ab.of_mul⟩
  · rintro ⟨ha, hb⟩
    exact ⟨ha.mul hb, hb.mul ha⟩

Equivalence of $M$-regularity for products and factors under scalar multiplication tower property

Informal description

Let $R$ be a type equipped with a multiplication operation and a scalar multiplication action on a type $M$, such that the scalar multiplication satisfies the tower property (i.e., $(a * b) \bullet m = a \bullet (b \bullet m)$ for all $a, b \in R$ and $m \in M$). Then, for any elements $a, b \in R$, the following are equivalent: 1. Both products $a * b$ and $b * a$ are $M$-regular (i.e., the maps $m \mapsto (a * b) \bullet m$ and $m \mapsto (b * a) \bullet m$ are injective). 2. Both $a$ and $b$ are $M$-regular (i.e., the maps $m \mapsto a \bullet m$ and $m \mapsto b \bullet m$ are injective).

IsSMulRegular.of_injective theorem

 {N F} [SMul R N] [FunLike F M N] [MulActionHomClass F R M N] (f : F) {r : R} (h1 : Function.Injective f)
  (h2 : IsSMulRegular N r) : IsSMulRegular M r

Full source

lemma of_injective {N F} [SMul R N] [FunLike F M N] [MulActionHomClass F R M N]
    (f : F) {r : R} (h1 : Function.Injective f) (h2 : IsSMulRegular N r) :
    IsSMulRegular M r := fun x y h3 => h1 <| h2 <|
  (map_smulₛₗ f r x).symm.trans ((congrArg f h3).trans (map_smulₛₗ f r y))

Inheritance of Regularity via Injective Homomorphism

Informal description

Let $R$ be a type equipped with a scalar multiplication operation on $M$ and $N$, and let $F$ be a type of homomorphisms from $M$ to $N$ that preserve the scalar multiplication. Given an injective homomorphism $f \colon M \to N$ in $F$ and an element $r \in R$ that is $N$-regular (i.e., the map $n \mapsto r \bullet n$ is injective on $N$), then $r$ is also $M$-regular (i.e., the map $m \mapsto r \bullet m$ is injective on $M$).

IsSMulRegular.one theorem

: IsSMulRegular M (1 : R)

Full source

/-- One is always `M`-regular. -/
@[simp]
theorem one : IsSMulRegular M (1 : R) := fun a b ab => by
  dsimp only [Function.comp_def] at ab
  rw [one_smul, one_smul] at ab
  assumption

Multiplicative Identity is $M$-Regular

Informal description

The multiplicative identity element $1$ in $R$ is $M$-regular, meaning the scalar multiplication map $M \to M$ defined by $m \mapsto 1 \cdot m$ is injective.

IsSMulRegular.of_mul_eq_one theorem

(h : a * b = 1) : IsSMulRegular M b

Full source

/-- An element of `R` admitting a left inverse is `M`-regular. -/
theorem of_mul_eq_one (h : a * b = 1) : IsSMulRegular M b :=
  of_mul (a := a) (by rw [h]; exact one M)

Left Inverse Implies $M$-Regularity

Informal description

Let $R$ be a type with a multiplication operation and a scalar multiplication action on a type $M$. If $a, b \in R$ satisfy $a * b = 1$, then $b$ is $M$-regular (i.e., the scalar multiplication map $M \to M$ defined by $m \mapsto b \bullet m$ is injective).

IsSMulRegular.pow theorem

(n : ℕ) (ra : IsSMulRegular M a) : IsSMulRegular M (a ^ n)

Full source

/-- Any power of an `M`-regular element is `M`-regular. -/
theorem pow (n : ℕ) (ra : IsSMulRegular M a) : IsSMulRegular M (a ^ n) := by
  induction n with
  | zero => rw [pow_zero]; simp only [one]
  | succ n hn =>
    rw [pow_succ']
    exact (ra.smul_iff (a ^ n)).mpr hn

Powers of $M$-regular elements are $M$-regular

Informal description

Let $R$ be a type equipped with a scalar multiplication operation on a type $M$, and let $a \in R$ be $M$-regular (i.e., the map $m \mapsto a \bullet m$ is injective). Then for any natural number $n$, the power $a^n$ is also $M$-regular.

IsSMulRegular.pow_iff theorem

{n : ℕ} (n0 : 0 < n) : IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a

Full source

/-- An element `a` is `M`-regular if and only if a positive power of `a` is `M`-regular. -/
theorem pow_iff {n : ℕ} (n0 : 0 < n) : IsSMulRegularIsSMulRegular M (a ^ n) ↔ IsSMulRegular M a := by
  refine ⟨?_, pow n⟩
  rw [← Nat.succ_pred_eq_of_pos n0, pow_succ, ← smul_eq_mul]
  exact of_smul _

Equivalence of $M$-regularity for an element and its positive powers: $a^n$ is $M$-regular $\leftrightarrow$ $a$ is $M$-regular for $n > 0$

Informal description

Let $R$ be a type equipped with a scalar multiplication operation on a type $M$, and let $a \in R$. For any positive natural number $n > 0$, the power $a^n$ is $M$-regular if and only if $a$ is $M$-regular. Here, an element $c \in R$ is called $M$-regular if the scalar multiplication map $M \to M$ defined by $m \mapsto c \bullet m$ is injective.

IsSMulRegular.of_smul_eq_one theorem

(h : a • s = 1) : IsSMulRegular M s

Full source

/-- An element of `S` admitting a left inverse in `R` is `M`-regular. -/
theorem of_smul_eq_one (h : a • s = 1) : IsSMulRegular M s :=
  of_smul a
    (by
      rw [h]
      exact one M)

Element with Left Inverse is $M$-Regular

Informal description

Let $R$ be a type equipped with a scalar multiplication operation on a type $M$, and let $a, s \in R$. If the scalar product $a \bullet s$ equals the multiplicative identity $1$, then $s$ is $M$-regular (i.e., the map $m \mapsto s \bullet m$ is injective).

IsSMulRegular.subsingleton theorem

(h : IsSMulRegular M (0 : R)) : Subsingleton M

Full source

/-- The element `0` is `M`-regular if and only if `M` is trivial. -/
protected theorem subsingleton (h : IsSMulRegular M (0 : R)) : Subsingleton M :=
  ⟨fun a b => h (by dsimp only [Function.comp_def]; repeat' rw [MulActionWithZero.zero_smul])⟩

Triviality of Module under Regularity of Zero Scalar Multiplication

Informal description

If the zero element $0$ in $R$ is $M$-regular (i.e., the scalar multiplication map $m \mapsto 0 \bullet m$ is injective), then the module $M$ is trivial (i.e., it has at most one element).

IsSMulRegular.zero_iff_subsingleton theorem

: IsSMulRegular M (0 : R) ↔ Subsingleton M

Full source

/-- The element `0` is `M`-regular if and only if `M` is trivial. -/
theorem zero_iff_subsingleton : IsSMulRegularIsSMulRegular M (0 : R) ↔ Subsingleton M :=
  ⟨fun h => h.subsingleton, fun H a b _ => @Subsingleton.elim _ H a b⟩

Zero is $M$-regular if and only if $M$ is trivial

Informal description

The zero element $0$ in $R$ is $M$-regular (i.e., the scalar multiplication map $m \mapsto 0 \bullet m$ is injective) if and only if the module $M$ is trivial (i.e., it has at most one element).

IsSMulRegular.not_zero_iff theorem

: ¬IsSMulRegular M (0 : R) ↔ Nontrivial M

Full source

/-- The `0` element is not `M`-regular, on a non-trivial module. -/
theorem not_zero_iff : ¬IsSMulRegular M (0 : R)¬IsSMulRegular M (0 : R) ↔ Nontrivial M := by
  rw [nontrivial_iff, not_iff_comm, zero_iff_subsingleton, subsingleton_iff]
  push_neg
  exact Iff.rfl

Non-regularity of Zero Scalar Multiplication in Nontrivial Modules

Informal description

The zero element $0$ in $R$ is not $M$-regular (i.e., the scalar multiplication map $m \mapsto 0 \bullet m$ is not injective) if and only if the module $M$ is nontrivial (i.e., it contains at least two distinct elements).

IsSMulRegular.zero theorem

[sM : Subsingleton M] : IsSMulRegular M (0 : R)

Full source

/-- The element `0` is `M`-regular when `M` is trivial. -/
theorem zero [sM : Subsingleton M] : IsSMulRegular M (0 : R) :=
  zero_iff_subsingleton.mpr sM

Zero is $M$-regular for trivial modules

Informal description

If the module $M$ is trivial (i.e., it has at most one element), then the zero element $0 \in R$ is $M$-regular (i.e., the scalar multiplication map $m \mapsto 0 \bullet m$ is injective).

IsSMulRegular.not_zero theorem

[nM : Nontrivial M] : ¬IsSMulRegular M (0 : R)

Full source

/-- The `0` element is not `M`-regular, on a non-trivial module. -/
theorem not_zero [nM : Nontrivial M] : ¬IsSMulRegular M (0 : R) :=
  not_zero_iff.mpr nM

Non-regularity of Zero in Nontrivial Modules

Informal description

If $M$ is a nontrivial module over a ring $R$, then the zero element $0 \in R$ is not $M$-regular, i.e., the scalar multiplication map $m \mapsto 0 \bullet m$ is not injective.

IsSMulRegular.mul_iff theorem

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

Full source

/-- A product is `M`-regular if and only if the factors are. -/
theorem mul_iff : IsSMulRegularIsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b := by
  rw [← mul_and_mul_iff]
  exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩

Product is $M$-regular if and only if factors are $M$-regular

Informal description

Let $R$ be a type with a multiplication operation and a scalar multiplication action on a type $M$. For any elements $a, b \in R$, the product $a * b$ is $M$-regular (i.e., the map $m \mapsto (a * b) \bullet m$ is injective) if and only if both $a$ and $b$ are $M$-regular (i.e., the maps $m \mapsto a \bullet m$ and $m \mapsto b \bullet m$ are injective).

isSMulRegular_of_group theorem

[MulAction G R] (g : G) : IsSMulRegular R g

Full source

/-- 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 isSMulRegular_of_group [MulAction G R] (g : G) : IsSMulRegular R g := by
  intro x y h
  convert congr_arg (g⁻¹ • ·) h using 1 <;> simp [← smul_assoc]

Group Elements Act Regularly on Modules

Informal description

Let $G$ be a group acting on a type $R$ via a multiplicative action. Then every element $g \in G$ is $R$-regular, meaning the scalar multiplication map $R \to R$ defined by $r \mapsto g \bullet r$ is injective.

Units.isSMulRegular theorem

(a : Rˣ) : IsSMulRegular M (a : R)

Full source

/-- Any element in `Rˣ` is `M`-regular. -/
theorem Units.isSMulRegular (a : Rˣ) : IsSMulRegular M (a : R) :=
  IsSMulRegular.of_mul_eq_one a.inv_val

Units are $M$-regular

Informal description

For any invertible element $a$ in the group of units $R^\times$ of a monoid $R$, the scalar multiplication map $M \to M$ defined by $m \mapsto a \bullet m$ is injective. In other words, every unit in $R$ is $M$-regular.

IsUnit.isSMulRegular theorem

(ua : IsUnit a) : IsSMulRegular M a

Full source

/-- A unit is `M`-regular. -/
theorem IsUnit.isSMulRegular (ua : IsUnit a) : IsSMulRegular M a := by
  rcases ua with ⟨a, rfl⟩
  exact a.isSMulRegular M

Units are $M$-regular

Informal description

If an element $a$ of a monoid $R$ is a unit (i.e., invertible), then $a$ is $M$-regular, meaning the scalar multiplication map $M \to M$ defined by $m \mapsto a \bullet m$ is injective.

Equiv.isSMulRegular_congr theorem

 {R S M M'} [SMul R M] [SMul S M'] {e : M ≃ M'} {r : R} {s : S} (h : ∀ x, e (r • x) = s • e x) :
  IsSMulRegular M r ↔ IsSMulRegular M' s

Full source

lemma Equiv.isSMulRegular_congr {R S M M'} [SMul R M] [SMul S M'] {e : M ≃ M'}
    {r : R} {s : S} (h : ∀ x, e (r • x) = s • e x) :
    IsSMulRegularIsSMulRegular M r ↔ IsSMulRegular M' s :=
  (e.comp_injective _).symm.trans  <|
    (iff_of_eq <| congrArg _ <| funext h).trans <| e.injective_comp _

Equivalence of Regularity under Scalar Multiplication via Equivalence: $r$ is $M$-regular $\leftrightarrow$ $s$ is $M'$-regular

Informal description

Let $R$ and $S$ be types equipped with scalar multiplication operations on $M$ and $M'$ respectively, and let $e : M \simeq M'$ be an equivalence between $M$ and $M'$. For elements $r \in R$ and $s \in S$ such that $e(r \bullet x) = s \bullet e(x)$ for all $x \in M$, the element $r$ is $M$-regular if and only if $s$ is $M'$-regular.