Modules over a ring
In this file we define
semimodule R M: an additive commutative monoidMis asemimoduleover asemiringRif forr : Randx : Mtheir "scalar multiplicationr • x : Mis defined, and the operation•satisfies some natural associativity and distributivity axioms similar to those on a ring.module R M: same assemimodule R Mbut assumes thatRis aringandMis an additive commutative group.vector_space k M: same assemimodule k Mandmodule k Mbut assumes thatkis afieldandMis an additive commutative group.linear_map R M M₂,M →ₗ[R] M₂: a linear map between two R-semimodules.is_linear_map R f: predicate saying thatf : M → M₂is a linear map.
Implementation notes
vector_spaceandmoduleare abbreviations forsemimodule R M.
Tags
semimodule, module, vector space, linear map
@[class]
- to_distrib_mul_action : distrib_mul_action R M
- add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x
- zero_smul : ∀ (x : M), 0 • x = 0
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
- lie_algebra.to_semimodule
- ordered_semimodule.to_semimodule
- order_dual.semimodule
- derivation.derivation.Rsemimodule
- algebra.to_semimodule
- semiring.to_semimodule
- normed_space.to_semimodule
- add_comm_monoid.nat_semimodule
- punit.semimodule
- pi.semimodule
- pi.semimodule'
- prod.semimodule
- submodule.semimodule
- finsupp.semimodule
- linear_map.semimodule
- submodule.quotient.semimodule
- matrix.semimodule
- tensor_product.semimodule
- semimodule.restrict_scalars.module_orig
- semimodule.restrict_scalars.semimodule
- linear_map.module_extend_scalars
- monoid_algebra.semimodule
- add_monoid_algebra.semimodule
- polynomial.semimodule
- mv_polynomial.semimodule
- submodule.semimodule_set
- submodule.semimodule_submodule
- direct_sum.semimodule
- module.direct_limit.semimodule
- ulift.semimodule
- ulift.semimodule'
- bounded_continuous_function.semimodule
- multilinear_map.semimodule
- multilinear_map.semimodule_ring
- continuous_multilinear_map.semimodule
- continuous_semimodule
- continuous_map_semimodule
- holor.semimodule
- filter.germ.semimodule
- filter.germ.semimodule'
- measure_theory.outer_measure.semimodule
- measure_theory.measure.semimodule
- measure_theory.simple_func.semimodule
- measure_theory.ae_eq_fun.semimodule
- measure_theory.l1.semimodule
- derivation.semimodule
- mv_power_series.semimodule
- power_series.semimodule
@[simp]
theorem
zero_smul
(R : Type u)
{M : Type w}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(x : M) :
theorem
two_smul
(R : Type u)
{M : Type w}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(x : M) :
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
- function.injective.semimodule R f hf smul = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul _inst_5}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
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
- function.surjective.semimodule R f hf smul = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul _inst_5}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
(•) as an add_monoid_hom.
Equations
- smul_add_hom R M = {to_fun := const_smul_hom M semimodule.to_distrib_mul_action, map_zero' := _, map_add' := _}
@[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) :
theorem
list.sum_smul
{R : Type u}
{M : Type w}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{l : list R}
{x : M} :
theorem
multiset.sum_smul
{R : Type u}
{M : Type w}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{l : multiset R}
{x : M} :
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} :
@[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] :
semimodule.core R M → semimodule 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
- semimodule.of_core H = let _inst : has_scalar R M := H.to_has_scalar in {to_distrib_mul_action := {to_mul_action := {to_has_scalar := H.to_has_scalar, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
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
- module.complex_to_real
- add_comm_group.int_module
- Module.is_module
- Module.module_obj
- Module.limit_module
- ideal.module_pi
- bilin_form.to_module
- linear_map.module
- affine_map.module
- continuous_linear_map.module
- bounded_continuous_function.module'
- continuous_linear_map.module_extend_scalars
- formal_multilinear_series.module
- continuous_module'
- continuous_map_module'
- module.dual.inst
- quadratic_form.module
- sesq_form.to_module
@[ext]
To prove two module structures on a fixed add_comm_group agree,
it suffices to check the scalar multiplications agree.
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} :
@[instance]
Equations
- semiring.to_semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_mul.mul (distrib.to_has_mul R)}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
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
- f.to_semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (r : R) (x : S), ⇑f r * x}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
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
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)
- to_fun : M → M₂
- map_add' : ∀ (x y : M), c.to_fun (x + y) = c.to_fun x + c.to_fun y
- map_smul' : ∀ (c_1 : R) (x : M), c.to_fun (c_1 • x) = c_1 • c.to_fun 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. 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.
@[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₂] :
has_coe_to_fun (M →ₗ[R] M₂)
Equations
- linear_map.has_coe_to_fun = {F := λ (x : M →ₗ[R] M₂), M → M₂, coe := linear_map.to_fun _inst_6}
@[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) :
Identity map as a linear_map
theorem
linear_map.id_apply
{R : Type u}
{M : Type w}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(x : M) :
⇑linear_map.id x = x
@[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₂) :
is_linear_map R ⇑f
theorem
linear_map.coe_inj
{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₂} :
@[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₂} :
theorem
linear_map.coe_fn_congr
{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} :
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₂} :
@[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) :
@[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) :
@[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₂) :
@[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₂) :
Equations
- _ = _
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₂} :
convert a linear map to an additive map
@[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₂) :
⇑(f.to_add_monoid_hom) = ⇑f
@[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} :
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₃} :
Composition of two linear maps is a linear map
@[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) :
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₂) :
@[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) :
@[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) :
@[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₂) :
Equations
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
@[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) :
⇑(is_linear_map.mk' f H) x = f x
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 f → f 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) :
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) :
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.
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.
@[instance]
The natural ℕ-semimodule structure on any add_comm_monoid.
Equations
- add_comm_monoid.nat_semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := nsmul (add_monoid.to_has_zero M)}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[instance]
The natural ℤ-module structure on any add_comm_group.
Equations
- add_comm_group.int_module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := gsmul (add_comm_group.to_add_group M)}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[instance]
Equations
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) :
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) :
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) :
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) :
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) :
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) :
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) :
def
add_monoid_hom.to_int_linear_map
{M : Type w}
{M₂ : Type x}
[add_comm_group M]
[add_comm_group M₂] :
Reinterpret an additive homomorphism as a ℤ-linear map.
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₂] :
Reinterpret an additive homomorphism as a ℚ-linear map.