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

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

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.

• smul : R → M → M
• one_smul : ∀ (b : M), 1 • b = b
• mul_smul : ∀ (x y : R) (b : M), (x * y) • b = x • y • b
• smul_zero : ∀ (a : R), a • 0 = 0
• smul_add : ∀ (a : R) (x y : M), a • (x + y) = a • x + a • y
• add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x

  Scalar multiplication distributes over addition from the right.

• zero_smul : ∀ (x : M), 0 • x = 0

  Scalar multiplication by zero gives zero.

theorem Module.ext {R : Type u} {M : Type v} {inst✝ : Semiring R} {inst✝¹ : AddCommMonoid M} {x y : Module R M} (smul : SMul.smul = SMul.smul) : x = y

@[instance 100]

instance Module.toMulActionWithZero {R : Type u_5} {M : Type u_6} {x✝ : Semiring R} {x✝¹ : AddCommMonoid M} [Module R M] : MulActionWithZero R M

A module over a semiring automatically inherits a MulActionWithZero structure.

Equations

• Module.toMulActionWithZero = MulActionWithZero.mk ⋯ ⋯

theorem add_smul {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (r s : R) (x : M) : (r + s) • x = r • x + s • x

theorem Convex.combo_self {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {a b : R} (h : a + b = 1) (x : M) : a • x + b • x = x

theorem two_smul (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : 2 • x = x + x

@[reducible, inline]

abbrev Function.Injective.module (R : Type u_1) {M : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [SMul R M₂] (f : M₂ →+ M) (hf : Function.Injective ⇑f) (smul : ∀ (c : R) (x : M₂), f (c • x) = c • f x) : Module R M₂

Pullback a Module structure along an injective additive monoid homomorphism. See note [reducible non-instances].

Equations

• Function.Injective.module R f hf smul = Module.mk ⋯ ⋯

@[reducible, inline]

abbrev Function.Surjective.module (R : Type u_1) {M : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [SMul R M₂] (f : M →+ M₂) (hf : Function.Surjective ⇑f) (smul : ∀ (c : R) (x : M), f (c • x) = c • f x) : Module R M₂

Pushforward a Module structure along a surjective additive monoid homomorphism. See note [reducible non-instances].

Equations

• Function.Surjective.module R f hf smul = Module.mk ⋯ ⋯

theorem Module.eq_zero_of_zero_eq_one {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) (zero_eq_one : 0 = 1) : x = 0

@[simp]

theorem smul_add_one_sub_smul {M : Type u_3} [AddCommMonoid M] {R : Type u_5} [Ring R] [Module R M] {r : R} {m : M} : r • m + (1 - r) • m = m

theorem Convex.combo_eq_smul_sub_add {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] {x y : M} {a b : R} (h : a + b = 1) : a • x + b • y = b • (y - x) + x

theorem Module.ext' {R : Type u_5} [Semiring R] {M : Type u_6} [AddCommMonoid M] (P Q : Module R M) (w : ∀ (r : R) (m : M), r • m = r • m) : P = Q

A variant of Module.ext that's convenient for term-mode.

@[simp]

theorem neg_smul {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (r : R) (x : M) : -r • x = -(r • x)

theorem neg_smul_neg {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (r : R) (x : M) : -r • -x = r • x

theorem neg_one_smul (R : Type u_1) {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (x : M) : -1 • x = -x

theorem sub_smul {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (r s : R) (y : M) : (r - s) • y = r • y - s • y

theorem Module.subsingleton (R : Type u_5) (M : Type u_6) [Semiring R] [Subsingleton R] [AddCommMonoid M] [Module R M] : Subsingleton M

A module over a Subsingleton semiring is a Subsingleton. We cannot register this as an instance because Lean has no way to guess R.

theorem Module.nontrivial (R : Type u_5) (M : Type u_6) [Semiring R] [Nontrivial M] [AddCommMonoid M] [Module R M] : Nontrivial R

A semiring is Nontrivial provided that there exists a nontrivial module over this semiring.

@[instance 910]

instance Semiring.toModule {R : Type u_1} [Semiring R] : Module R R

Equations

• Semiring.toModule = Module.mk ⋯ ⋯

instance instDistribSMul {R : Type u_1} [NonUnitalNonAssocSemiring R] : DistribSMul R R

Equations

• instDistribSMul = DistribSMul.mk ⋯