# mathlibdocumentation

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 #

• submodule.induction_on_rank: if M is free and finitely generated, if P holds for ⊥ : submodule R M and if P N follows from P N' for all N' that are of lower rank, then P holds on all submodules

• submodule.exists_basis_of_pid: if M is free and finitely generated and R is a PID, then N : submodule R M is 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] [ M] {ι : Type u_1} (b : R M) (N : M) (rank_eq : ∀ {m : } (v : fin mN), (coe v)m = 0) :
N =
theorem eq_bot_of_generator_maximal_map_eq_zero {R : Type u} {M : Type v} [comm_ring R] [ M] {ι : Type u_1} (b : R M) {N : M} {ϕ : M →ₗ[R] R} (hϕ : ∀ (ψ : M →ₗ[R] R), = ) [ N).is_principal] (hgen : = 0) :
N =
theorem generator_map_dvd_of_mem {R : Type u} {M : Type v} [comm_ring R] [ M] {N : M} (ϕ : M →ₗ[R] R) [ N).is_principal] {x : M} (hx : x N) :
theorem not_mem_of_ortho {R : Type u_2} {M : Type u_3} [ M] {x : M} {N : M} (ortho : ∀ (c : R) (y : M), y Nc x + y = 0c = 0) :
x N
theorem ne_zero_of_ortho {R : Type u_2} {M : Type u_3} [ M] {x : M} {N : 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} {M : Type u_3} [ M] (b : R M) (P : MSort u_4) (ih : Π (N : M), (Π (N' : M), N' NΠ (x : M), x N(∀ (c : R) (y : M), y N'c x + y = 0c = 0)P N')P N) (n : ) (N : M) (rank_le : ∀ {m : } (v : fin mN), (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
• n N rank_le = nat.rec (λ (N : M) (rank_le : ∀ {m : } (v : fin mN), (coe v)m 0), _.mpr (ih (λ (N : M) (N_le : N ) (x : M) (x_mem : x ) (x_ortho : ∀ (c : R) (y : M), y Nc x + y = 0c = 0), false.rec (P N) _))) (λ (n : ) (rank_ih : Π (N : M), (∀ {m : } (v : fin mN), (coe v)m n)P N) (N : M) (rank_le : ∀ {m : } (v : fin mN), (coe v)m n.succ), ih N (λ (N' : M) (N'_le : N' N) (x : M) (x_mem : x N) (x_ortho : ∀ (c : R) (y : M), y N'c x + y = 0c = 0), rank_ih N' _)) n N rank_le
theorem basis.card_le_card_of_linear_independent_aux {R : Type u_1} (n : ) {m : } (v : fin mfin n → R) :
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} {R : Type u_1} [ M] {ι : Type u_2} [fintype ι] (b : R M) {ι' : Type u_4} [fintype ι'] {v : ι' → M} (hv : v) :
def basis.index_equiv {M : Type u_3} {R : Type u_1} {ι : Type u_2} {ι' : Type u_4} [ M] [fintype ι] [fintype ι'] (b : 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} {M : Type u_3} [ M] [fintype ι] (b : R M) (P : MSort u_4) (ih : Π (N : M), (Π (N' : M), N' NΠ (x : M), x N(∀ (c : R) (y : M), y N'c x + y = 0c = 0)P N')P N) (N : 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} {M : Type u_3} [ M] {ι : Type u_1} [fintype ι] (b : R M) (N : 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} {M : Type u_3} [ M] {ι : Type u_1} [fintype ι] {N O : M} (hNO : N O) (b : 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
• = submodule.basis_of_pid_of_le._match_1 hNO N))
• submodule.basis_of_pid_of_le._match_1 hNO n, bN'⟩ = n, bN'.map
def submodule.basis_of_pid_of_le_span {R : Type u_2} {M : Type u_3} [ M] {ι : Type u_1} [fintype ι] {b : ι → M} (hb : b) {N : M} (le : N (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} {M : Type u_3} [ M] [fintype ι] {s : ι → M} (hs : (set.range s) = )  :
Σ (n : ), basis (fin n) R M

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

Equations
• = 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 : (λ (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 (s '' module.free_of_finite_type_torsion_free._proof_2.some))), id (λ (indepI : (s coe)), id (λ (hI : ∀ (i : ι), i I(∃ (a : R), a 0 a s i (s '' I))), let N : M := (set.range (s coe)), sI : I → N := λ (i : I), s i.val, _⟩, sI_basis : R N := basis.span indepI in (λ (_x : ∀ (i : ι), (λ (i : ι), i 0 (λ (i : ι), i s i N), let A : R := ∏ (i : ι), (λ (i : ι), i, φ : M →ₗ[R] M := M) A, ψ : M ≃ₗ[R] (φ.range) := in 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} {M : Type u_3} [ M] [ 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} [semiring S] [ S] [ M] [ M] [ M] (hinj : function.injective S)) {v : ι → M} (li : 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.