Free modules #
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.
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 #
-
submodule.induction_on_rank: ifMis free and finitely generated, ifPholds for⊥ : submodule R Mand ifP Nfollows fromP N'for allN'that are of lower rank, thenPholds on all submodules -
submodule.exists_basis_of_pid: ifMis free and finitely generated andRis a PID, thenN : submodule R Mis free and finitely generated. This is the first part of the structure theorem for modules.
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 m → ↥N), linear_independent R (coe ∘ v) → m = 0) :
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 ψ N → submodule.map ψ N = submodule.map ϕ N)
[(submodule.map ϕ N).is_principal]
(hgen : submodule.is_principal.generator (submodule.map ϕ N) = 0) :
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) :
submodule.is_principal.generator (submodule.map ϕ N) ∣ ⇑ϕ x
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 ∈ N → c • x + y = 0 → c = 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 ∈ N → c • x + y = 0 → c = 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 M → Sort 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 = 0 → c = 0) → P N') → P N)
(n : ℕ)
(N : submodule R M)
(rank_le : ∀ {m : ℕ} (v : fin m → ↥N), 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
- submodule.induction_on_rank_aux b P ih n N rank_le = nat.rec (λ (N : submodule R M) (rank_le : ∀ {m : ℕ} (v : fin m → ↥N), linear_independent R (coe ∘ v) → m ≤ 0), _.mpr (ih ⊥ (λ (N : submodule R M) (N_le : N ≤ ⊥) (x : M) (x_mem : x ∈ ⊥) (x_ortho : ∀ (c : R) (y : M), y ∈ N → c • x + y = 0 → c = 0), false.rec (P N) _))) (λ (n : ℕ) (rank_ih : Π (N : submodule R M), (∀ {m : ℕ} (v : fin m → ↥N), linear_independent R (coe ∘ v) → m ≤ n) → P N) (N : submodule R M) (rank_le : ∀ {m : ℕ} (v : fin m → ↥N), linear_independent R (coe ∘ v) → m ≤ n.succ), ih N (λ (N' : submodule R M) (N'_le : N' ≤ N) (x : M) (x_mem : x ∈ N) (x_ortho : ∀ (c : R) (y : M), y ∈ N' → c • x + y = 0 → c = 0), rank_ih N' _)) n N rank_le
theorem
basis.card_le_card_of_linear_independent_aux
{R : Type u_1}
[integral_domain R]
(n : ℕ)
{m : ℕ}
(v : fin m → fin n → R) :
linear_independent R v → m ≤ n
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) :
fintype.card ι' ≤ fintype.card ι
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 M → Sort 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 = 0 → c = 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
- submodule.induction_on_rank b P ih N = submodule.induction_on_rank_aux b P ih (fintype.card ι) N _
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) :
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
- submodule.basis_of_pid b N = submodule.induction_on_rank b (λ (N : submodule R M), Σ (n : ℕ), basis (fin n) R ↥N) (λ (N : submodule R M) (ih : Π (N' : submodule R M), N' ≤ N → Π (x : M), x ∈ N → (∀ (c : R) (y : M), y ∈ N' → c • x + y = 0 → c = 0) → (Σ (n : ℕ), basis (fin n) R ↥N')), let ϕ : M →ₗ[R] R := Exists.some _ in dite (N = ⊥) (λ (N_bot : N = ⊥), _.mpr ⟨0, basis.empty ↥⊥ submodule.basis_of_pid._proof_4⟩) (λ (N_bot : ¬N = ⊥), dite (submodule.is_principal.generator (submodule.map ϕ N) = 0) (λ (a_zero : submodule.is_principal.generator (submodule.map ϕ N) = 0), absurd _ N_bot) (λ (a_zero : ¬submodule.is_principal.generator (submodule.map ϕ N) = 0), let y : M := Exists.some _ in and.dcases_on _ (λ (y_mem : Exists.some _ ∈ ↑N) (ϕy_eq : ⇑ϕ (Exists.some _) = submodule.is_principal.generator (submodule.map ϕ N)), (ih (ϕ.ker ⊓ N) _ y y_mem _).cases_on (λ (nN' : ℕ) (bN' : basis (fin nN') R ↥(ϕ.ker ⊓ N)), ⟨nN'.succ, id (let bN'y : fin nN'.succ → ↥N := fin.cons ⟨y, y_mem⟩ (⇑(submodule.of_le _) ∘ ⇑bN') in basis.mk _ _)⟩))))) N
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) :
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
- submodule.basis_of_pid_of_le hNO b = submodule.basis_of_pid_of_le._match_1 hNO (submodule.basis_of_pid b (submodule.comap O.subtype N))
- submodule.basis_of_pid_of_le._match_1 hNO ⟨n, bN'⟩ = ⟨n, bN'.map (submodule.comap_subtype_equiv_of_le hNO)⟩
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)) :
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] :
A finite type torsion free module over a PID is free.
Equations
- module.free_of_finite_type_torsion_free hs = let I : set ι := module.free_of_finite_type_torsion_free._proof_1.some in and.dcases_on module.free_of_finite_type_torsion_free._proof_3 (λ (indepI : linear_independent R (λ (x : ↥(module.free_of_finite_type_torsion_free._proof_2.some)), s ↑x)) (hI : ∀ (i : ι), i ∉ module.free_of_finite_type_torsion_free._proof_2.some → (∃ (a : R), a ≠ 0 ∧ a • s i ∈ submodule.span R (s '' module.free_of_finite_type_torsion_free._proof_2.some))), id (λ (indepI : linear_independent R (s ∘ coe)), id (λ (hI : ∀ (i : ι), i ∉ I → (∃ (a : R), a ≠ 0 ∧ a • s i ∈ submodule.span R (s '' I))), let N : submodule R M := submodule.span R (set.range (s ∘ coe)), sI : ↥I → ↥N := λ (i : ↥I), ⟨s i.val, _⟩, sI_basis : basis ↥I R ↥N := basis.span indepI in (λ (_x : ∀ (i : ι), (λ (i : ι), classical.some _) i ≠ 0 ∧ (λ (i : ι), classical.some _) i • s i ∈ N), let A : R := ∏ (i : ι), (λ (i : ι), classical.some _) i, φ : M →ₗ[R] M := ⇑(linear_map.lsmul R M) A, ψ : M ≃ₗ[R] ↥(φ.range) := linear_equiv.of_injective φ _ in (submodule.basis_of_pid_of_le _ sI_basis).cases_on (λ (n : ℕ) (b : basis (fin n) R ↥(φ.range)), ⟨n, b.map ψ.symm⟩)) _) hI) indepI)
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] :
A finite type torsion free module over a PID is free.
Equations
- module.free_of_finite_type_torsion_free' = module.free_of_finite_type_torsion_free module.free_of_finite_type_torsion_free'._proof_3
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.