mathlib documentation

algebra.module.basic

Modules over a ring #

In this file we define

Implementation notes #

Tags #

semimodule, module, vector space

@[class]
structure semimodule (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] :
Type (max u v)

A semimodule 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
@[instance]

A semimodule over a semiring automatically inherits a mul_action_with_zero structure.

Equations
theorem add_smul {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] (r s : R) (x : M) :
(r + s) x = r x + s x
theorem two_smul (R : Type u) {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] (x : M) :
2 x = x + x
theorem two_smul' (R : Type u) {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] (x : M) :
2 x = bit0 x
def function.injective.semimodule (R : Type u) {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [semimodule 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) :
semimodule R M₂

Pullback a semimodule structure along an injective additive monoid homomorphism.

Equations
def function.surjective.semimodule (R : Type u) {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [semimodule 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) :
semimodule R M₂

Pushforward a semimodule structure along a surjective additive monoid homomorphism.

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

Compose a semimodule with a ring_hom, with action f s • m

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

(•) as an add_monoid_hom.

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

An add_comm_monoid that is a semimodule over a ring carries a natural add_comm_group structure.

Equations
@[nolint]
structure semimodule.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 semimodule, 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 semimodule structure by checking less properties, in semimodule.of_core.

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

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

Equations
def module (R : Type u) (M : Type v) [ring R] [add_comm_group M] :
Type (max u v)

A module is the same as a semimodule, except the scalar semiring is actually a ring. This is the traditional generalization of spaces like ℤ^n, which have a natural addition operation and a way to multiply them by elements of a ring, but no multiplication operation between vectors.

@[ext]
theorem semimodule_ext {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] (P Q : semimodule R M) (w : ∀ (r : R) (m : M), r m = r m) :
P = Q

To prove two semimodule structures on a fixed add_comm_monoid agree, it suffices to check the scalar multiplications agree.

@[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)
theorem neg_one_smul (R : Type u) {M : Type w} [ring R] [add_comm_group M] [module R M] (x : M) :
(-1) x = -x
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
theorem semimodule.subsingleton (R : Type u_1) (M : Type u_2) [semiring R] [subsingleton R] [add_comm_monoid M] [semimodule R M] :

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

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

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

Equations
def vector_space (R : Type u) (M : Type v) [field R] [add_comm_group M] :
Type (max u v)

A vector space is the same as a module, except the scalar ring is actually a field. (This adds commutativity of the multiplication and existence of inverses.) This is the traditional generalization of spaces like ℝ^n, which have a natural addition operation and a way to multiply them by real numbers, but no multiplication operation between vectors.

theorem nsmul_eq_smul_cast (R : Type u) {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] (n : ) (b : M) :
n b = n b

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

@[instance]
def add_comm_monoid.nat_is_scalar_tower {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] :
@[instance]
def add_comm_monoid.nat_smul_comm_class {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] :
@[instance]
def add_comm_monoid.nat_smul_comm_class' {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] :
@[instance]

The natural ℤ-module structure on any add_comm_group.

Equations
theorem gsmul_def {M : Type w} [add_comm_group M] (n : ) (x : M) :
n •ℤ x = n x

gsmul is defined as the smul action of add_comm_group.int_module.

theorem gsmul_eq_smul_cast (R : Type u) {M : Type w} [ring R] [add_comm_group M] [semimodule R M] (n : ) (b : M) :
n •ℤ b = n b

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

theorem gsmul_eq_smul {M : Type w} [add_comm_group M] [semimodule M] (n : ) (b : M) :
n •ℤ b = n b

gsmul is equal to any -module structure.

@[instance]

All -module structures are equal.

@[instance]
@[instance]
@[instance]
theorem add_monoid_hom.map_int_module_smul {M : Type w} {M₂ : Type x} [add_comm_group M] [add_comm_group M₂] [module M] [module M₂] (f : M →+ M₂) (x : ) (a : M) :
f (x a) = x f a
theorem add_monoid_hom.map_int_cast_smul {R : Type u} {M : Type w} {M₂ : Type x} [ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂] (f : M →+ M₂) (x : ) (a : M) :
f (x a) = x f a
theorem add_monoid_hom.map_nat_cast_smul {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →+ M₂) (x : ) (a : M) :
f (x a) = x f a
theorem add_monoid_hom.map_rat_cast_smul {R : Type u_1} [division_ring R] [char_zero R] {E : Type u_2} [add_comm_group E] [module R E] {F : Type u_3} [add_comm_group F] [module R F] (f : E →+ F) (c : ) (x : E) :
f (c x) = c f x
theorem add_monoid_hom.map_rat_module_smul {E : Type u_1} [add_comm_group E] [vector_space E] {F : Type u_2} [add_comm_group F] [module F] (f : E →+ F) (c : ) (x : E) :
f (c x) = c f x
@[simp]
theorem add_monoid_hom.int_smul_apply {M : Type w} {M₂ : Type x} [add_monoid M] [add_comm_group M₂] [module (M →+ M₂)] [module M₂] (n : ) (f : M →+ M₂) (a : M) :
(n f) a = n f a

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).

@[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 = 0c = 0 x = 0

no_zero_smul_divisors R M states that a scalar multiple is 0 only if either argument is 0.

The main application of no_zero_smul_divisors R M, when M is a semimodule, 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
@[simp]
theorem smul_eq_zero {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] [no_zero_smul_divisors R M] {c : R} {x : M} :
c x = 0 c = 0 x = 0
theorem smul_ne_zero {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] [no_zero_smul_divisors R M] {c : R} {x : M} :
c x 0 c 0 x 0
theorem eq_zero_of_smul_two_eq_zero (R : Type u) {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] [no_zero_smul_divisors R M] [char_zero R] {v : M} (hv : 2 v = 0) :
v = 0
theorem smul_injective {R : Type u} {M : Type w} [semiring R] [add_comm_group M] [semimodule R M] [no_zero_smul_divisors R M] {c : R} (hc : c 0) :
function.injective (λ (x : M), c x)
theorem eq_zero_of_eq_neg (R : Type u) {M : Type w} [semiring R] [add_comm_group M] [semimodule R M] [no_zero_smul_divisors R M] [char_zero R] {v : M} (hv : v = -v) :
v = 0
theorem ne_neg_of_ne_zero {R : Type u} [ring R] [char_zero R] [no_zero_divisors R] {v : R} (hv : v 0) :
v -v
@[instance]
@[simp]
theorem nat.smul_one_eq_coe {R : Type u_1} [semiring R] (m : ) :
m 1 = m
@[simp]
theorem int.smul_one_eq_coe {R : Type u_1} [ring R] [semimodule R] (m : ) :
m 1 = m