mathlib documentation

algebra.module.basic

Modules over a ring #

In this file we define

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 add_comm_group. If R is a field and M an add_comm_group, 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 mathlib, we had separate semimodule and vector_space abbreviations. 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

source
theorem module.ext {R : Type u} {M : Type v} {_inst_1 : semiring R} {_inst_2 : add_comm_monoid M} (x y : module R M) (h : module.to_distrib_mul_action = module.to_distrib_mul_action) :
x = y
source
@[ext, class]
structure module (R : Type u) (M : Type v) [semiring R] [add_comm_monoid 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.

Instances
source
theorem module.ext_iff {R : Type u} {M : Type v} {_inst_1 : semiring R} {_inst_2 : add_comm_monoid M} (x y : module R M) :
x = y ↔ module.to_distrib_mul_action = module.to_distrib_mul_action
source
@[protected, instance]
def module.to_mul_action_with_zero {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] :
mul_action_with_zero R M

A module over a semiring automatically inherits a mul_action_with_zero structure.

Equations
source
@[protected, instance]
def add_comm_monoid.nat_module {M : Type w} [add_comm_monoid M] :
module ℕ M
Equations
source
theorem add_smul {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] (r s : R) (x : M) :
(r + s) • x = r • x + s • x
source
theorem convex.combo_self {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] {a b : R} (h : a + b = 1) (x : M) :
a • x + b • x = x
source
theorem two_smul (R : Type u) {M : Type w} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
2 • x = x + x
source
theorem two_smul' (R : Type u) {M : Type w} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
2 • x = bit0 x
source
@[simp]
theorem inv_of_two_smul_add_inv_of_two_smul (R : Type u) {M : Type w} [semiring R] [add_comm_monoid M] [module R M] [invertible 2] (x : M) :
⅟ 2 • x + ⅟ 2 • x = x
source
@[protected]
def function.injective.module (R : Type u) {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [has_scalar 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
source
@[protected]
def function.surjective.module (R : Type u) {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid M₂] [has_scalar 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.

Equations
source
def function.surjective.module_left {R : Type u_1} {S : Type u_2} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] [semiring S] [has_scalar S M] (f : R →+* S) (hf : function.surjective ⇑f) (hsmul : ∀ (c : R) (x : M), ⇑f c • x = c • x) :
module S M

Push forward the action of R on M along a compatible surjective map f : R →+* S.

See also function.surjective.mul_action_left and function.surjective.distrib_mul_action_left.

Equations
source
def module.comp_hom {R : Type u} {S : Type v} (M : Type w) [semiring R] [add_comm_monoid M] [module R M] [semiring S] (f : S →+* R) :
module S M

Compose a module with a ring_hom, with action f s • m.

See note [reducible non-instances].

Equations
source
@[simp]
theorem module.to_add_monoid_End_apply_apply (R : Type u) (M : Type w) [semiring R] [add_comm_monoid M] [module R M] (ᾰ : R) (ᾰ_1 : M) :
⇑(⇑(module.to_add_monoid_End R M) ᾰ) ᾰ_1 = ᾰ • ᾰ_1
source
def module.to_add_monoid_End (R : Type u) (M : Type w) [semiring R] [add_comm_monoid M] [module R M] :
R →+* add_monoid.End M

(•) as an add_monoid_hom.

This is a stronger version of distrib_mul_action.to_add_monoid_End

Equations
source
def smul_add_hom (R : Type u) (M : Type w) [semiring R] [add_comm_monoid M] [module R M] :
R →+ M →+ M

A convenience alias for module.to_add_monoid_End as an add_monoid_hom, usually to allow the use of add_monoid_hom.flip.

Equations
source
@[simp]
theorem smul_add_hom_apply {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] (r : R) (x : M) :
⇑(⇑(smul_add_hom R M) r) x = r • x
source
theorem module.eq_zero_of_zero_eq_one {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] (x : M) (zero_eq_one : 0 = 1) :
x = 0
source
theorem list.sum_smul {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] {l : list R} {x : M} :
l.sum • x = (list.map (λ (r : R), r • x) l).sum
source
theorem multiset.sum_smul {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] {l : multiset R} {x : M} :
l.sum • x = (multiset.map (λ (r : R), r • x) l).sum
source
theorem finset.sum_smul {R : Type u} {M : Type w} {ι : Type z} [semiring R] [add_comm_monoid M] [module R M] {f : ι → R} {s : finset ι} {x : M} :
(∑ (i : ι) in s, f i) • x = ∑ (i : ι) in s, f i • x
source
def module.add_comm_monoid_to_add_comm_group (R : Type u) {M : Type w} [ring R] [add_comm_monoid M] [module R M] :
add_comm_group M

An add_comm_monoid that is a module over a ring carries a natural add_comm_group structure. See note [reducible non-instances].

Equations
source
@[protected, instance]
def add_comm_group.int_module (M : Type w) [add_comm_group M] :
module ℤ M
Equations
source
@[nolint]
structure module.core (R : Type u) (M : Type w) [semiring R] [add_comm_group M] :
Type (max u w)
  • to_has_scalar : has_scalar R M
  • smul_add : ∀ (r : R) (x y : M), r • (x + y) = r • x + r • y
  • add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x
  • mul_smul : ∀ (r s : R) (x : M), (r * s) • x = r • s • x
  • one_smul : ∀ (x : M), 1 • x = x

A structure containing most informations as in a module, except the fields zero_smul and smul_zero. As these fields can be deduced from the other ones when M is an add_comm_group, this provides a way to construct a module structure by checking less properties, in module.of_core.

source
def module.of_core {R : Type u} {M : Type w} [semiring R] [add_comm_group M] (H : module.core R M) :
module R M

Define module without proving zero_smul and smul_zero by using an auxiliary structure module.core, when the underlying space is an add_comm_group.

Equations
source
theorem module.ext' {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid 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.

source
@[simp]
theorem neg_smul {R : Type u} {M : Type w} [ring R] [add_comm_group M] [module R M] (r : R) (x : M) :
-r • x = -(r • x)
source
@[simp]
theorem neg_smul_neg {R : Type u} {M : Type w} [ring R] [add_comm_group M] [module R M] (r : R) (x : M) :
-r • -x = r • x
source
@[simp]
theorem units.neg_smul {R : Type u} {M : Type w} [ring R] [add_comm_group M] [module R M] (u : Rˣ) (x : M) :
-u • x = -(u • x)
source
theorem neg_one_smul (R : Type u) {M : Type w} [ring R] [add_comm_group M] [module R M] (x : M) :
(-1) • x = -x
source
theorem sub_smul {R : Type u} {M : Type w} [ring R] [add_comm_group M] [module R M] (r s : R) (y : M) :
(r - s) • y = r • y - s • y
source
@[protected]
theorem module.subsingleton (R : Type u_1) (M : Type u_2) [semiring R] [subsingleton R] [add_comm_monoid 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.

source
@[protected]
theorem module.nontrivial (R : Type u_1) (M : Type u_2) [semiring R] [nontrivial M] [add_comm_monoid M] [module R M] :
nontrivial R

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

source
@[protected, instance]
def semiring.to_module {R : Type u} [semiring R] :
module R R
Equations
source
@[protected, instance]
def semiring.to_opposite_module {R : Type u} [semiring R] :
module Rᵐᵒᵖ R

Like semiring.to_module, but multiplies on the right.

Equations
source
def ring_hom.to_module {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :
module R S

A ring homomorphism f : R →+* M defines a module structure by r • x = f r * x.

Equations
source
@[protected, instance]
def ring_hom.apply_distrib_mul_action {R : Type u} [semiring R] :
distrib_mul_action (R →+* R) R

The tautological action by R →+* R on R.

This generalizes function.End.apply_mul_action.

Equations
source
@[protected, simp]
theorem ring_hom.smul_def {R : Type u} [semiring R] (f : R →+* R) (a : R) :
f • a = ⇑f a
source
@[protected, instance]
def ring_hom.apply_has_faithful_scalar {R : Type u} [semiring R] :
has_faithful_scalar (R →+* R) R

ring_hom.apply_distrib_mul_action is faithful.

source
theorem nsmul_eq_smul_cast (R : Type u) {M : Type w} [semiring R] [add_comm_monoid M] [module R M] (n : ℕ) (b : M) :
n • b = ↑n • b

nsmul is equal to any other module structure via a cast.

source
theorem nat_smul_eq_nsmul {M : Type w} [add_comm_monoid M] (h : module ℕ M) (n : ℕ) (x : M) :
n • x = n • x

Convert back any exotic ℕ-smul to the canonical instance. This should not be needed since in mathlib all add_comm_monoids should normally have exactly one ℕ-module structure by design.

source
def add_comm_monoid.nat_module.unique {M : Type w} [add_comm_monoid M] :
unique (module ℕ M)

All ℕ-module structures are equal. Not an instance since in mathlib all add_comm_monoid should normally have exactly one ℕ-module structure by design.

Equations
source
@[protected, instance]
def add_comm_monoid.nat_is_scalar_tower {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] :
is_scalar_tower ℕ R M
source
theorem zsmul_eq_smul_cast (R : Type u) {M : Type w} [ring R] [add_comm_group M] [module R M] (n : ℤ) (b : M) :
n • b = ↑n • b

zsmul is equal to any other module structure via a cast.

source
theorem int_smul_eq_zsmul {M : Type w} [add_comm_group M] (h : module ℤ M) (n : ℤ) (x : M) :
n • x = n • x

Convert back any exotic ℤ-smul to the canonical instance. This should not be needed since in mathlib all add_comm_groups should normally have exactly one ℤ-module structure by design.

source
def add_comm_group.int_module.unique {M : Type w} [add_comm_group M] :
unique (module ℤ M)

All ℤ-module structures are equal. Not an instance since in mathlib all add_comm_group should normally have exactly one ℤ-module structure by design.

Equations
source
theorem map_int_cast_smul {M : Type w} {M₂ : Type x} [add_comm_group M] [add_comm_group M₂] {F : Type u_1} [add_monoid_hom_class F M M₂] (f : F) (R : Type u_2) (S : Type u_3) [ring R] [ring S] [module R M] [module S M₂] (x : ℤ) (a : M) :
⇑f (↑x • a) = ↑x • ⇑f a
source
theorem map_nat_cast_smul {M : Type w} {M₂ : Type x} [add_comm_monoid M] [add_comm_monoid M₂] {F : Type u_1} [add_monoid_hom_class F M M₂] (f : F) (R : Type u_2) (S : Type u_3) [semiring R] [semiring S] [module R M] [module S M₂] (x : ℕ) (a : M) :
⇑f (↑x • a) = ↑x • ⇑f a
source
theorem map_inv_int_cast_smul {M : Type w} {M₂ : Type x} [add_comm_group M] [add_comm_group M₂] {F : Type u_1} [add_monoid_hom_class F M M₂] (f : F) (R : Type u_2) (S : Type u_3) [division_ring R] [division_ring S] [module R M] [module S M₂] (n : ℤ) (x : M) :
⇑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ⇑f x
source
theorem map_inv_nat_cast_smul {M : Type w} {M₂ : Type x} [add_comm_group M] [add_comm_group M₂] {F : Type u_1} [add_monoid_hom_class F M M₂] (f : F) (R : Type u_2) (S : Type u_3) [division_ring R] [division_ring S] [module R M] [module S M₂] (n : ℕ) (x : M) :
⇑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ⇑f x
source
theorem map_rat_cast_smul {M : Type w} {M₂ : Type x} [add_comm_group M] [add_comm_group M₂] {F : Type u_1} [add_monoid_hom_class F M M₂] (f : F) (R : Type u_2) (S : Type u_3) [division_ring R] [division_ring S] [module R M] [module S M₂] (c : ℚ) (x : M) :
⇑f (↑c • x) = ↑c • ⇑f x
source
theorem map_rat_smul {M : Type w} {M₂ : Type x} [add_comm_group M] [add_comm_group M₂] [module ℚ M] [module ℚ M₂] {F : Type u_1} [add_monoid_hom_class F M M₂] (f : F) (c : ℚ) (x : M) :
⇑f (c • x) = c • ⇑f x
source
theorem subsingleton_rat_module (E : Type u_1) [add_comm_group E] :
subsingleton (module ℚ E)

There can be at most one module ℚ E structure on an additive commutative group. This is not an instance because simp becomes very slow if we have many subsingleton instances, see [gh-6025].

source
theorem inv_int_cast_smul_eq {E : Type u_1} (R : Type u_2) (S : Type u_3) [add_comm_group E] [division_ring R] [division_ring S] [module R E] [module S E] (n : ℤ) (x : E) :
(↑n)⁻¹ • x = (↑n)⁻¹ • x

If E is a vector space over two division rings R and S, then scalar multiplications agree on inverses of integer numbers in R and S.

source
theorem inv_nat_cast_smul_eq {E : Type u_1} (R : Type u_2) (S : Type u_3) [add_comm_group E] [division_ring R] [division_ring S] [module R E] [module S E] (n : ℕ) (x : E) :
(↑n)⁻¹ • x = (↑n)⁻¹ • x

If E is a vector space over two division rings R and S, then scalar multiplications agree on inverses of natural numbers in R and S.

source
theorem inv_int_cast_smul_comm {α : Type u_1} {E : Type u_2} (R : Type u_3) [add_comm_group E] [division_ring R] [monoid α] [module R E] [distrib_mul_action α E] (n : ℤ) (s : α) (x : E) :
(↑n)⁻¹ • s • x = s • (↑n)⁻¹ • x

If E is a vector space over a division rings R and has a monoid action by α, then that action commutes by scalar multiplication of inverses of integers in R

source
theorem inv_nat_cast_smul_comm {α : Type u_1} {E : Type u_2} (R : Type u_3) [add_comm_group E] [division_ring R] [monoid α] [module R E] [distrib_mul_action α E] (n : ℕ) (s : α) (x : E) :
(↑n)⁻¹ • s • x = s • (↑n)⁻¹ • x

If E is a vector space over a division rings R and has a monoid action by α, then that action commutes by scalar multiplication of inverses of natural numbers in R.

source
theorem rat_cast_smul_eq {E : Type u_1} (R : Type u_2) (S : Type u_3) [add_comm_group E] [division_ring R] [division_ring S] [module R E] [module S E] (r : ℚ) (x : E) :
↑r • x = ↑r • x

If E is a vector space over two division rings R and S, then scalar multiplications agree on rational numbers in R and S.

source
@[protected, instance]
def add_comm_group.int_is_scalar_tower {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] :
is_scalar_tower ℤ R M
source
@[protected, instance]
def is_scalar_tower.rat {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] [module ℚ R] [module ℚ M] :
is_scalar_tower ℚ R M
source
@[protected, instance]
def smul_comm_class.rat {R : Type u} {M : Type v} [semiring R] [add_comm_group M] [module R M] [module ℚ M] :
smul_comm_class ℚ R M
source
@[protected, instance]
def smul_comm_class.rat' {R : Type u} {M : Type v} [semiring R] [add_comm_group M] [module R M] [module ℚ M] :
smul_comm_class R ℚ M

no_zero_smul_divisors #

This section defines the no_zero_smul_divisors class, and includes some tests for the vanishing of elements (especially in modules over division rings).

source
@[class]
structure no_zero_smul_divisors (R : Type u_1) (M : Type u_2) [has_zero R] [has_zero M] [has_scalar R M] :
Prop
  • eq_zero_or_eq_zero_of_smul_eq_zero : ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0

no_zero_smul_divisors R M states that a scalar multiple is 0 only if either argument is 0. This a version of saying that M is torsion free, without assuming R is zero-divisor free.

The main application of no_zero_smul_divisors R M, when M is a module, is the result smul_eq_zero: a scalar multiple is 0 iff either argument is 0.

It is a generalization of the no_zero_divisors class to heterogeneous multiplication.

Instances
source
theorem function.injective.no_zero_smul_divisors {R : Type u_1} {M : Type u_2} {N : Type u_3} [has_zero R] [has_zero M] [has_zero N] [has_scalar R M] [has_scalar R N] [no_zero_smul_divisors R N] (f : M → N) (hf : function.injective f) (h0 : f 0 = 0) (hs : ∀ (c : R) (x : M), f (c • x) = c • f x) :
no_zero_smul_divisors R M

Pullback a no_zero_smul_divisors instance along an injective function.

source
@[protected, instance]
def no_zero_smul_divisors.of_no_zero_divisors {R : Type u} [semiring R] [no_zero_divisors R] :
no_zero_smul_divisors R R
source
@[simp]
theorem smul_eq_zero {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] [no_zero_smul_divisors R M] {c : R} {x : M} :
c • x = 0 ↔ c = 0 ∨ x = 0
source
theorem smul_ne_zero {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [module R M] [no_zero_smul_divisors R M] {c : R} {x : M} :
c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0
source
theorem nat.no_zero_smul_divisors (R : Type u) (M : Type w) [semiring R] [add_comm_monoid M] [module R M] [no_zero_smul_divisors R M] [char_zero R] :
no_zero_smul_divisors ℕ M
source
@[simp]
theorem two_nsmul_eq_zero (R : Type u) (M : Type w) [semiring R] [add_comm_monoid M] [module R M] [no_zero_smul_divisors R M] [char_zero R] {v : M} :
2 • v = 0 ↔ v = 0
source
theorem char_zero.of_module (R : Type u) (M : Type w) [semiring R] [add_comm_monoid M] [module R M] [has_one M] [char_zero M] :
char_zero R

If M is an R-module with one and M has characteristic zero, then R has characteristic zero as well. Usually M is an R-algebra.

source
theorem smul_right_injective {R : Type u} (M : Type w) [semiring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {c : R} (hc : c ≠ 0) :
function.injective (has_scalar.smul c)
source
theorem smul_right_inj {R : Type u} {M : Type w} [semiring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {c : R} (hc : c ≠ 0) {x y : M} :
c • x = c • y ↔ x = y
source
theorem self_eq_neg (R : Type u) (M : Type w) [semiring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] [char_zero R] {v : M} :
v = -v ↔ v = 0
source
theorem neg_eq_self (R : Type u) (M : Type w) [semiring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] [char_zero R] {v : M} :
-v = v ↔ v = 0
source
theorem self_ne_neg (R : Type u) (M : Type w) [semiring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] [char_zero R] {v : M} :
v ≠ -v ↔ v ≠ 0
source
theorem neg_ne_self (R : Type u) (M : Type w) [semiring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] [char_zero R] {v : M} :
-v ≠ v ↔ v ≠ 0
source
theorem smul_left_injective (R : Type u) {M : Type w} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {x : M} (hx : x ≠ 0) :
function.injective (λ (c : R), c • x)
source
@[protected, instance]
def no_zero_smul_divisors.of_division_ring {R : Type u} {M : Type w} [division_ring R] [add_comm_group M] [module R M] :
no_zero_smul_divisors R M
source
@[simp]
theorem nat.smul_one_eq_coe {R : Type u_1} [semiring R] (m : ℕ) :
m • 1 = ↑m
source
@[simp]
theorem int.smul_one_eq_coe {R : Type u_1} [ring R] (m : ℤ) :
m • 1 = ↑m