mathlib documentation

algebra.module.basic

Modules over a ring

In this file we define

Implementation notes

Tags

semimodule, module, vector space, linear map

@[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
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

@[simp]
theorem zero_smul (R : Type u) {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] (x : M) :
0 x = 0

theorem two_smul (R : Type u) {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] (x : M) :
2 x = x + 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) :
function.injective f(∀ (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₂) :
function.surjective f(∀ (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 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) :
0 = 1x = 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

@[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] :

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.

Instances
@[ext]
theorem module_ext {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] (P Q : module R M) :
(∀ (r : R) (m : M), r m = r m)P = Q

To prove two module structures on a fixed add_comm_group 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 smul_eq_zero {R : Type u_1} {E : Type u_2} [division_ring R] [add_comm_group E] [module R E] {c : R} {x : E} :
c x = 0 c = 0 x = 0

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.

@[simp]
theorem smul_eq_mul {R : Type u} [semiring R] {a a' : R} :
a a' = a * a'

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

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

Equations
structure is_linear_map (R : Type u) {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M → M₂) → Prop
  • map_add : ∀ (x y : M), f (x + y) = f x + f y
  • map_smul : ∀ (c : R) (x : M), f (c x) = c f x

A map f between semimodules over a semiring is linear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = c • f x. The predicate is_linear_map R f asserts this property. A bundled version is available with linear_map, and should be favored over is_linear_map most of the time.

structure linear_map (R : Type u) (M : Type v) (M₂ : Type w) [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
Type (max v w)

A map f between semimodules over a semiring is linear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = c • f x. Elements of linear_map R M M₂ (available under the notation M →ₗ[R] M₂) are bundled versions of such maps. An unbundled version is available with the predicate is_linear_map, but it should be avoided most of the time.

def linear_map.to_add_hom {R : Type u} {M : Type v} {M₂ : Type w} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M →ₗ[R] M₂)add_hom M M₂

The add_hom underlying a linear_map.

@[instance]
def linear_map.has_coe_to_fun {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₂] :

Equations
@[simp]
theorem linear_map.coe_mk {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₂) (h₁ : ∀ (x y : M), f (x + y) = f x + f y) (h₂ : ∀ (c : R) (x : M), f (c x) = c f x) :
{to_fun := f, map_add' := h₁, map_smul' := h₂} = f

def linear_map.id {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] :

Identity map as a linear_map

Equations
theorem linear_map.id_apply {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] (x : M) :

@[simp]
theorem linear_map.id_coe {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] :

@[simp]
theorem linear_map.to_fun_eq_coe {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) :

theorem linear_map.is_linear {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) :

theorem linear_map.coe_injective {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} :
function.injective (λ (f : M →ₗ[R] M₂), show M → M₂, from f)

@[ext]
theorem linear_map.ext {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {f g : M →ₗ[R] M₂} :
(∀ (x : M), f x = g x)f = g

theorem linear_map.congr_arg {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {f : M →ₗ[R] M₂} {x x' : M} :
x = x'f x = f x'

theorem linear_map.congr_fun {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {f g : M →ₗ[R] M₂} (h : f = g) (x : M) :
f x = g x

If two linear maps are equal, they are equal at each point.

theorem linear_map.ext_iff {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {f g : M →ₗ[R] M₂} :
f = g ∀ (x : M), f x = g x

@[simp]
theorem linear_map.map_add {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) (x y : M) :
f (x + y) = f x + f y

@[simp]
theorem linear_map.map_smul {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) (c : R) (x : M) :
f (c x) = c f x

@[simp]
theorem linear_map.map_zero {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) :
f 0 = 0

@[instance]
def linear_map.is_add_monoid_hom {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) :

def linear_map.to_add_monoid_hom {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} :
(M →ₗ[R] M₂)M →+ M₂

convert a linear map to an additive map

Equations
@[simp]
theorem linear_map.to_add_monoid_hom_coe {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) :

@[simp]
theorem linear_map.map_sum {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) {ι : Type u_1} {t : finset ι} {g : ι → M} :
f (∑ (i : ι) in t, g i) = ∑ (i : ι) in t, f (g i)

theorem linear_map.to_add_monoid_hom_injective {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} :

@[ext]
theorem linear_map.ext_ring {R : Type u} {M : Type w} [semiring R] [add_comm_monoid M] {semimodule_M : semimodule R M} {f g : R →ₗ[R] M} :
f 1 = g 1f = g

If two R-linear maps from R are equal on 1, then they are equal.

def linear_map.comp {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {semimodule_M₃ : semimodule R M₃} :
(M₂ →ₗ[R] M₃)(M →ₗ[R] M₂)(M →ₗ[R] M₃)

Composition of two linear maps is a linear map

Equations
@[simp]
theorem linear_map.comp_apply {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {semimodule_M₃ : semimodule R M₃} (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) (x : M) :
(f.comp g) x = f (g x)

theorem linear_map.comp_coe {R : Type u} {M : Type w} {M₂ : Type x} {M₃ : Type y} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} {semimodule_M₃ : semimodule R M₃} (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) :
f g = (f.comp g)

@[simp]
theorem linear_map.map_neg {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_group M] [add_comm_group M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) (x : M) :
f (-x) = -f x

@[simp]
theorem linear_map.map_sub {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_group M] [add_comm_group M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) (x y : M) :
f (x - y) = f x - f y

@[instance]
def linear_map.is_add_group_hom {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_group M] [add_comm_group M₂] {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule R M₂} (f : M →ₗ[R] M₂) :

def is_linear_map.mk' {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₂) :
is_linear_map R f(M →ₗ[R] M₂)

Convert an is_linear_map predicate to a linear_map

Equations
@[simp]
theorem is_linear_map.mk'_apply {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₂} (H : is_linear_map R f) (x : M) :

theorem is_linear_map.is_linear_map_smul {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [semimodule R M] (c : R) :
is_linear_map R (λ (z : M), c z)

theorem is_linear_map.is_linear_map_smul' {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] (a : M) :
is_linear_map R (λ (c : R), c a)

theorem is_linear_map.map_zero {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₂} :
is_linear_map R ff 0 = 0

theorem is_linear_map.is_linear_map_neg {R : Type u} {M : Type w} [semiring R] [add_comm_group M] [semimodule R M] :
is_linear_map R (λ (z : M), -z)

theorem is_linear_map.map_neg {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_group M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] {f : M → M₂} (lin : is_linear_map R f) (x : M) :
f (-x) = -f x

theorem is_linear_map.map_sub {R : Type u} {M : Type w} {M₂ : Type x} [semiring R] [add_comm_group M] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] {f : M → M₂} (lin : is_linear_map R f) (x y : M) :
f (x - y) = f x - f y

def module.End (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule R M] :
Type v

Ring of linear endomorphismsms of a module.

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.

Instances
@[instance]

The natural ℕ-semimodule structure on any add_comm_monoid.

Equations
@[instance]

The natural ℤ-module structure on any add_comm_group.

Equations
@[instance]

theorem semimodule.smul_eq_smul (R : Type u_1) [semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] (n : ) (b : M) :
n b = n b

theorem semimodule.nsmul_eq_smul (R : Type u_1) [semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] (n : ) (b : M) :
n •ℕ b = n b

theorem nat.smul_def {M : Type u_1} [add_comm_monoid M] (n : ) (x : M) :
n x = n •ℕ x

theorem gsmul_eq_smul {M : Type u_1} [add_comm_group M] (n : ) (x : M) :
n •ℤ x = n x

theorem module.gsmul_eq_smul_cast (R : Type u_1) [ring R] {M : Type u_2} [add_comm_group M] [module R M] (n : ) (b : M) :
n •ℤ b = n b

theorem module.gsmul_eq_smul {M : Type u_1} [add_comm_group M] [module M] (n : ) (b : M) :
n •ℤ b = n b

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

def add_monoid_hom.to_int_linear_map {M : Type w} {M₂ : Type x} [add_comm_group M] [add_comm_group M₂] :
(M →+ M₂)(M →ₗ[] M₂)

Reinterpret an additive homomorphism as a -linear map.

Equations
def add_monoid_hom.to_rat_linear_map {M : Type w} {M₂ : Type x} [add_comm_group M] [vector_space M] [add_comm_group M₂] [vector_space M₂] :
(M →+ M₂)(M →ₗ[] M₂)

Reinterpret an additive homomorphism as a -linear map.

Equations