Mathlib.Algebra.Module.Defs

Module docstring

{"# Modules over a ring

In this file we define

Module R M : an additive commutative monoid M is a Module over a 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.

Implementation notes

In typical mathematical usage, our definition of Module corresponds to \"semimodule\", and the word \"module\" is reserved for Module R M where R is a Ring and M an AddCommGroup. If R is a Field and M an AddCommGroup, M would be called an R-vector space. Since those assumptions can be made by changing the typeclasses applied to R and M, without changing the axioms in Module, mathlib calls everything a Module.

In older versions of mathlib3, we had separate abbreviations for semimodules and vector spaces. This caused inference issues in some cases, while not providing any real advantages, so we decided to use a canonical Module typeclass throughout.

Tags

semimodule, module, vector space "}

Module structure

(R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] extends
  DistribMulAction R M

Full source

/-- A module is a generalization of vector spaces to a scalar semiring.
  It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
  connected by a "scalar multiplication" operation `r • x : M`
  (where `r : R` and `x : M`) with some natural associativity and
  distributivity axioms similar to those on a ring. -/
@[ext]
class Module (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] extends
  DistribMulAction R M where
  /-- Scalar multiplication distributes over addition from the right. -/
  protected add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x
  /-- Scalar multiplication by zero gives zero. -/
  protected zero_smul : ∀ x : M, (0 : R) • x = 0

Module over a semiring

Informal description

A module over a semiring $R$ consists of an additive commutative monoid $M$ equipped with a scalar multiplication operation $r \bullet x \in M$ for $r \in R$ and $x \in M$, satisfying the following properties: 1. Distributivity of scalar multiplication over addition in $R$: $(r + s) \bullet x = r \bullet x + s \bullet x$ 2. Distributivity of scalar multiplication over addition in $M$: $r \bullet (x + y) = r \bullet x + r \bullet y$ 3. Compatibility with multiplication in $R$: $(r \cdot s) \bullet x = r \bullet (s \bullet x)$ 4. Identity element acts as identity: $1 \bullet x = x$ This structure generalizes vector spaces by allowing the scalar ring $R$ to be a semiring rather than requiring it to be a field.

Module.toMulActionWithZero instance

{R M} {_ : Semiring R} {_ : AddCommMonoid M} [Module R M] : MulActionWithZero R M

Full source

/-- A module over a semiring automatically inherits a `MulActionWithZero` structure. -/
instance (priority := 100) Module.toMulActionWithZero
  {R M} {_ : Semiring R} {_ : AddCommMonoid M} [Module R M] : MulActionWithZero R M :=
  { (inferInstance : MulAction R M) with
    smul_zero := smul_zero
    zero_smul := Module.zero_smul }

Modules as Multiplicative Actions with Zero

Informal description

Every module $M$ over a semiring $R$ inherits a multiplicative action with zero structure, where the scalar multiplication operation $\bullet$ is compatible with the zero element of $R$ and $M$.

add_smul theorem

: (r + s) • x = r • x + s • x

Full source

theorem add_smul : (r + s) • x = r • x + s • x :=
  Module.add_smul r s x

Distributivity of Scalar Multiplication over Addition in a Module

Informal description

For any elements $r, s$ in a semiring $R$ and any element $x$ in an $R$-module $M$, the scalar multiplication satisfies the distributive property $(r + s) \bullet x = r \bullet x + s \bullet x$.

Convex.combo_self theorem

{a b : R} (h : a + b = 1) (x : M) : a • x + b • x = x

Full source

theorem Convex.combo_self {a b : R} (h : a + b = 1) (x : M) : a • x + b • x = x := by
  rw [← add_smul, h, one_smul]

Convex Combination Identity: $a \bullet x + b \bullet x = x$ when $a + b = 1$

Informal description

For any elements $a, b$ in a semiring $R$ such that $a + b = 1$, and any element $x$ in an $R$-module $M$, the convex combination $a \bullet x + b \bullet x$ equals $x$.

two_smul theorem

: (2 : R) • x = x + x

Full source

theorem two_smul : (2 : R) • x = x + x := by rw [← one_add_one_eq_two, add_smul, one_smul]

Scalar Multiplication by Two: $2 \bullet x = x + x$

Informal description

For any element $x$ in an $R$-module $M$, where $R$ is a semiring, the scalar multiplication by $2$ satisfies $2 \bullet x = x + x$.

Function.Injective.module abbrev

 [AddCommMonoid M₂] [SMul R M₂] (f : M₂ →+ M) (hf : Injective f) (smul : ∀ (c : R) (x), f (c • x) = c • f x) :
  Module R M₂

Full source

/-- Pullback a `Module` structure along an injective additive monoid homomorphism.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.module [AddCommMonoid M₂] [SMul R M₂] (f : M₂ →+ M)
    (hf : Injective f) (smul : ∀ (c : R) (x), f (c • x) = c • f x) : Module R M₂ :=
  { hf.distribMulAction f smul with
    add_smul := fun c₁ c₂ x => hf <| by simp only [smul, f.map_add, add_smul]
    zero_smul := fun x => hf <| by simp only [smul, zero_smul, f.map_zero] }

Module structure induced by an injective scalar-multiplication-preserving homomorphism

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. Given an additive commutative monoid $M_2$ with a scalar multiplication operation, and an injective additive monoid homomorphism $f \colon M_2 \to M$ that preserves scalar multiplication (i.e., $f(c \bullet x) = c \bullet f(x)$ for all $c \in R$ and $x \in M_2$), then $M_2$ inherits an $R$-module structure from $M$ via $f$.

Function.Surjective.module abbrev

 [AddCommMonoid M₂] [SMul R M₂] (f : M →+ M₂) (hf : Surjective f) (smul : ∀ (c : R) (x), f (c • x) = c • f x) :
  Module R M₂

Full source

/-- Pushforward a `Module` structure along a surjective additive monoid homomorphism.
See note [reducible non-instances]. -/
protected abbrev Function.Surjective.module [AddCommMonoid M₂] [SMul R M₂] (f : M →+ M₂)
    (hf : Surjective f) (smul : ∀ (c : R) (x), f (c • x) = c • f x) : Module R M₂ :=
  { toDistribMulAction := hf.distribMulAction f smul
    add_smul := fun c₁ c₂ x => by
      rcases hf x with ⟨x, rfl⟩
      simp only [add_smul, ← smul, ← f.map_add]
    zero_smul := fun x => by
      rcases hf x with ⟨x, rfl⟩
      rw [← f.map_zero, ← smul, zero_smul] }

Pushforward of Module Structure Along a Surjective Homomorphism

Informal description

Let $R$ be a semiring, $M$ be an $R$-module, and $M_2$ be an additive commutative monoid equipped with a scalar multiplication operation $\bullet \colon R \times M_2 \to M_2$. Given a surjective additive monoid homomorphism $f \colon M \to M_2$ such that $f(r \bullet x) = r \bullet f(x)$ for all $r \in R$ and $x \in M$, then $M_2$ inherits an $R$-module structure from $M$ via $f$.

smul_add_one_sub_smul theorem

{R : Type*} [Ring R] [Module R M] {r : R} {m : M} : r • m + (1 - r) • m = m

Full source

@[simp]
theorem smul_add_one_sub_smul {R : Type*} [Ring R] [Module R M] {r : R} {m : M} :
    r • m + (1 - r) • m = m := by rw [← add_smul, add_sub_cancel, one_smul]

Linear Combination Identity in Modules: $r \bullet m + (1 - r) \bullet m = m$

Informal description

Let $R$ be a ring and $M$ be an $R$-module. For any element $r \in R$ and $m \in M$, we have the identity $r \bullet m + (1 - r) \bullet m = m$.

Convex.combo_eq_smul_sub_add theorem

[Module R M] {x y : M} {a b : R} (h : a + b = 1) : a • x + b • y = b • (y - x) + x

Full source

theorem Convex.combo_eq_smul_sub_add [Module R M] {x y : M} {a b : R} (h : a + b = 1) :
    a • x + b • y = b • (y - x) + x :=
  calc
    a • x + b • y = b • y - b • x + (a • x + b • x) := by rw [sub_add_add_cancel, add_comm]
    _ = b • (y - x) + x := by rw [smul_sub, Convex.combo_self h]

Convex Combination Identity: $a \bullet x + b \bullet y = b \bullet (y - x) + x$ when $a + b = 1$

Informal description

Let $R$ be a semiring and $M$ an $R$-module. For any elements $x, y \in M$ and $a, b \in R$ such that $a + b = 1$, we have the identity: $$a \bullet x + b \bullet y = b \bullet (y - x) + x$$

Module.ext' theorem

 {R : Type*} [Semiring R] {M : Type*} [AddCommMonoid M] (P Q : Module R M)
  (w :
    ∀ (r : R) (m : M),
      (haveI := P;
        r • m) =
        (haveI := Q;
        r • m)) :
  P = Q

Full source

/-- A variant of `Module.ext` that's convenient for term-mode. -/
theorem Module.ext' {R : Type*} [Semiring R] {M : Type*} [AddCommMonoid M] (P Q : Module R M)
    (w : ∀ (r : R) (m : M), (haveI := P; r • m) = (haveI := Q; r • m)) :
    P = Q := by
  ext
  exact w _ _

Module Structure Equality via Scalar Multiplication Identity

Informal description

Let $R$ be a semiring and $M$ an additive commutative monoid. For two module structures $P$ and $Q$ on $M$ over $R$, if for all $r \in R$ and $m \in M$ the scalar multiplication $r \bullet m$ is the same under both structures, then $P = Q$.

neg_smul theorem

: -r • x = -(r • x)

Full source

@[simp]
theorem neg_smul : -r • x = -(r • x) :=
  eq_neg_of_add_eq_zero_left <| by rw [← add_smul, neg_add_cancel, zero_smul]

Negative Scalar Multiplication Property: $-r \bullet x = -(r \bullet x)$

Informal description

For any element $r$ in a semiring $R$ and any element $x$ in an $R$-module $M$, the scalar multiplication satisfies $-r \bullet x = -(r \bullet x)$.

neg_smul_neg theorem

: -r • -x = r • x

Full source

theorem neg_smul_neg : -r • -x = r • x := by rw [neg_smul, smul_neg, neg_neg]

Double Negation Scalar Multiplication Identity: $-r \bullet (-x) = r \bullet x$

Informal description

For any element $r$ in a semiring $R$ and any element $x$ in an $R$-module $M$, the scalar multiplication satisfies $-r \bullet (-x) = r \bullet x$.

neg_one_smul theorem

(x : M) : (-1 : R) • x = -x

Full source

theorem neg_one_smul (x : M) : (-1 : R) • x = -x := by simp

Scalar Multiplication by Negative One: $(-1) \bullet x = -x$

Informal description

For any element $x$ in an $R$-module $M$, the scalar multiplication of $-1 \in R$ with $x$ equals the additive inverse of $x$, i.e., $(-1) \bullet x = -x$.

sub_smul theorem

(r s : R) (y : M) : (r - s) • y = r • y - s • y

Full source

theorem sub_smul (r s : R) (y : M) : (r - s) • y = r • y - s • y := by
  simp [add_smul, sub_eq_add_neg]

Distributivity of Scalar Multiplication over Subtraction: $(r - s) \bullet y = r \bullet y - s \bullet y$

Informal description

For any elements $r, s$ in a semiring $R$ and any element $y$ in an $R$-module $M$, the scalar multiplication satisfies $(r - s) \bullet y = r \bullet y - s \bullet y$.

Module.subsingleton theorem

(R M : Type*) [MonoidWithZero R] [Subsingleton R] [Zero M] [MulActionWithZero R M] : Subsingleton M

Full source

/-- A module over a `Subsingleton` semiring is a `Subsingleton`. We cannot register this
as an instance because Lean has no way to guess `R`. -/
protected theorem Module.subsingleton (R M : Type*) [MonoidWithZero R] [Subsingleton R] [Zero M]
    [MulActionWithZero R M] : Subsingleton M :=
  MulActionWithZero.subsingleton R M

Subsingleton Module over Subsingleton Semiring

Informal description

Let $R$ be a monoid with zero and $M$ be a type with zero and a multiplicative action with zero by $R$. If $R$ is a subsingleton (i.e., all elements of $R$ are equal), then $M$ is also a subsingleton (all elements of $M$ are equal).

Module.nontrivial theorem

(R M : Type*) [MonoidWithZero R] [Nontrivial M] [Zero M] [MulActionWithZero R M] : Nontrivial R

Full source

/-- A semiring is `Nontrivial` provided that there exists a nontrivial module over this semiring. -/
protected theorem Module.nontrivial (R M : Type*) [MonoidWithZero R] [Nontrivial M] [Zero M]
    [MulActionWithZero R M] : Nontrivial R :=
  MulActionWithZero.nontrivial R M

Nontriviality of the base ring for a nontrivial module

Informal description

Let $R$ be a monoid with zero and $M$ be a nontrivial module over $R$ with a zero element and a multiplicative action with zero by $R$. Then $R$ is nontrivial (i.e., contains at least two distinct elements).

Semiring.toModule instance

[Semiring R] : Module R R

Full source

instance (priority := 910) Semiring.toModule [Semiring R] : Module R R where
  smul_add := mul_add
  add_smul := add_mul
  zero_smul := zero_mul
  smul_zero := mul_zero

Semiring as a Module over Itself

Informal description

Every semiring $R$ is a module over itself, where the scalar multiplication is given by the multiplication operation in $R$.

instDistribSMul instance

[NonUnitalNonAssocSemiring R] : DistribSMul R R

Full source

instance [NonUnitalNonAssocSemiring R] : DistribSMul R R where
  smul_add := left_distrib

Distributive Scalar Multiplication on Non-Unital Non-Associative Semirings

Informal description

For any non-unital non-associative semiring $R$, $R$ is equipped with a distributive scalar multiplication structure where the scalar multiplication is given by the multiplication in $R$ itself.