mathlib documentation

linear_algebra.free_module_pid

Free modules over PID #

A free R-module M is a module with a basis over R, equivalently it is an R-module linearly equivalent to ι →₀ R for some ι.

This file proves a submodule of a free R-module of finite rank is also a free R-module of finite rank, if R is a principal ideal domain (PID), i.e. we have instances [integral_domain R] [is_principal_ideal_ring R]. We express "free R-module of finite rank" as a module M which has a basis b : ι → R, where ι is a fintype. We call the cardinality of ι the rank of M in this file; it would be equal to finrank R M if R is a field and M is a vector space.

Main results #

Tags #

free module, finitely generated module, rank, structure theorem

theorem eq_bot_of_rank_eq_zero {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {ι : Type u_1} [no_zero_divisors R] (b : basis ι R M) (N : submodule R M) (rank_eq : ∀ {m : } (v : fin mN), linear_independent R (coe v)m = 0) :
N =
theorem eq_bot_of_generator_maximal_map_eq_zero {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {ι : Type u_1} (b : basis ι R M) {N : submodule R M} {ϕ : M →ₗ[R] R} (hϕ : ∀ (ψ : M →ₗ[R] R), submodule.map ϕ N submodule.map ψ Nsubmodule.map ψ N = submodule.map ϕ N) [(submodule.map ϕ N).is_principal] (hgen : submodule.is_principal.generator (submodule.map ϕ N) = 0) :
N =
theorem generator_map_dvd_of_mem {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N : submodule R M} (ϕ : M →ₗ[R] R) [(submodule.map ϕ N).is_principal] {x : M} (hx : x N) :
theorem not_mem_of_ortho {R : Type u_2} [integral_domain R] {M : Type u_3} [add_comm_group M] [module R M] {x : M} {N : submodule R M} (ortho : ∀ (c : R) (y : M), y Nc x + y = 0c = 0) :
x N
theorem ne_zero_of_ortho {R : Type u_2} [integral_domain R] {M : Type u_3} [add_comm_group M] [module R M] {x : M} {N : submodule R M} (ortho : ∀ (c : R) (y : M), y Nc x + y = 0c = 0) :
x 0
def submodule.induction_on_rank_aux {ι : Type u_1} {R : Type u_2} [integral_domain R] {M : Type u_3} [add_comm_group M] [module R M] (b : basis ι R M) (P : submodule R MSort u_4) (ih : Π (N : submodule R M), (Π (N' : submodule R M), N' NΠ (x : M), x N(∀ (c : R) (y : M), y N'c x + y = 0c = 0)P N')P N) (n : ) (N : submodule R M) (rank_le : ∀ {m : } (v : fin mN), linear_independent R (coe v)m n) :
P N

If N is a submodule with finite rank, do induction on adjoining a linear independent element to a submodule.

Equations
theorem basis.card_le_card_of_linear_independent_aux {R : Type u_1} [integral_domain R] (n : ) {m : } (v : fin mfin n → R) :

In an n-dimensional space, the rank is at most m.

theorem basis.card_le_card_of_linear_independent {M : Type u_3} [add_comm_group M] {R : Type u_1} [integral_domain R] [module R M] {ι : Type u_2} [fintype ι] (b : basis ι R M) {ι' : Type u_4} [fintype ι'] {v : ι' → M} (hv : linear_independent R v) :
def basis.index_equiv {M : Type u_3} [add_comm_group M] {R : Type u_1} {ι : Type u_2} {ι' : Type u_4} [integral_domain R] [module R M] [fintype ι] [fintype ι'] (b : basis ι R M) (b' : basis ι' R M) :
ι ι'

If we have two bases on the same space, their indices are in bijection.

Equations
def submodule.induction_on_rank {ι : Type u_1} {R : Type u_2} [integral_domain R] {M : Type u_3} [add_comm_group M] [module R M] [fintype ι] (b : basis ι R M) (P : submodule R MSort u_4) (ih : Π (N : submodule R M), (Π (N' : submodule R M), N' NΠ (x : M), x N(∀ (c : R) (y : M), y N'c x + y = 0c = 0)P N')P N) (N : submodule R M) :
P N

If N is a submodule in a free, finitely generated module, do induction on adjoining a linear independent element to a submodule.

Equations
def submodule.basis_of_pid {R : Type u_2} [integral_domain R] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] {ι : Type u_1} [fintype ι] (b : basis ι R M) (N : submodule R M) :
Σ (n : ), basis (fin n) R N

A submodule of a free R-module of finite rank is also a free R-module of finite rank, if R is a principal ideal domain.

Equations
def submodule.basis_of_pid_of_le {R : Type u_2} [integral_domain R] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] {ι : Type u_1} [fintype ι] {N O : submodule R M} (hNO : N O) (b : basis ι R O) :
Σ (n : ), basis (fin n) R N

A submodule inside a free R-submodule of finite rank is also a free R-module of finite rank, if R is a principal ideal domain.

Equations
def submodule.basis_of_pid_of_le_span {R : Type u_2} [integral_domain R] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] {ι : Type u_1} [fintype ι] {b : ι → M} (hb : linear_independent R b) {N : submodule R M} (le : N submodule.span R (set.range b)) :
Σ (n : ), basis (fin n) R N

A submodule inside the span of a linear independent family is a free R-module of finite rank, if R is a principal ideal domain.

Equations
def module.free_of_finite_type_torsion_free {ι : Type u_1} {R : Type u_2} [integral_domain R] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] [fintype ι] {s : ι → M} (hs : submodule.span R (set.range s) = ) [no_zero_smul_divisors R M] :
Σ (n : ), basis (fin n) R M

A finite type torsion free module over a PID is free.

Equations
def module.free_of_finite_type_torsion_free' {R : Type u_2} [integral_domain R] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] [module.finite R M] [no_zero_smul_divisors R M] :
Σ (n : ), basis (fin n) R M

A finite type torsion free module over a PID is free.

Equations
theorem linear_independent.restrict_scalars_algebras {R : Type u_1} {S : Type u_2} {M : Type u_3} {ι : Type u_4} [comm_semiring R] [semiring S] [add_comm_monoid M] [algebra R S] [module R M] [module S M] [is_scalar_tower R S M] (hinj : function.injective (algebra_map R S)) {v : ι → M} (li : linear_independent S v) :

A set of linearly independent vectors in a module M over a semiring S is also linearly independent over a subring R of K.