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
• mul_smul (x y : R) (b : M) : (x * y) • b = x • y • b
• one_smul (b : M) : 1 • b = 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_iff {R : Type u} {M : Type v} {inst✝ : Semiring R} {inst✝¹ : AddCommMonoid M} {x y : Module R M} : x = y ↔ SMul.smul = SMul.smul

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_reducible, instance 100]

instance Module.toMulActionWithZero {R : Type u_4} {M : Type u_5} {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 = { toMulAction := inferInstance, smul_zero := ⋯, zero_smul := ⋯ }

theorem add_smul {R : Type u_1} {M : Type u_2} [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_2} [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_2} [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_2} {M₂ : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [SMul R M₂] (f : M₂ →+ M) (hf : 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 = { toDistribMulAction := Function.Injective.distribMulAction f hf smul, add_smul := ⋯, zero_smul := ⋯ }

@[reducible, inline]

abbrev Function.Surjective.module (R : Type u_1) {M : Type u_2} {M₂ : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [SMul R M₂] (f : M →+ M₂) (hf : 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 = { toDistribMulAction := Function.Surjective.distribMulAction f hf smul, add_smul := ⋯, zero_smul := ⋯ }

theorem Module.eq_zero_of_zero_eq_one {R : Type u_1} {M : Type u_2} [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_2} [AddCommMonoid M] {R : Type u_4} [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_2} [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_4} [Semiring R] {M : Type u_5} [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_2} [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_2} [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_2} [Ring R] [AddCommGroup M] [Module R M] (x : M) : -1 • x = -x

theorem sub_smul {R : Type u_1} {M : Type u_2} [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_4) (M : Type u_5) [MonoidWithZero R] [Subsingleton R] [Zero M] [MulActionWithZero 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_4) (M : Type u_5) [MonoidWithZero R] [Nontrivial M] [Zero M] [MulActionWithZero R M] : Nontrivial R

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

@[instance_reducible, instance 1100]

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

Equations

• Semiring.toModule = { toMulAction := Monoid.toMulAction R, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

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

Equations

• instDistribSMul = { toSMulZeroClass := (MulZeroClass.toSMulWithZero R).toSMulZeroClass, smul_add := ⋯ }