Free modules #
finsupp.total_id_surjective to prove that any module is the quotient of a free module.
Main definition #
module.free R M: the class of free
module.free R M is the statement that the
M is free.
[finite_free R M] then
choose_basis : ι → M is the basis.
ι = choose_basis_index R M.
The universal property of free modules: giving a functon
(choose_basis_index R M) → N, for
R-module, is the same as giving an
M →ₗ[R] N.
This definition is parameterized over an extra
smul_comm_class R S M' holds.
R is commutative, you can set
S := R; if
R is not commutative,
you can recover an
add_equiv by setting
S := ℕ.
See library note [bundled maps over different rings].
A variation of
of_equiv: the assumption
module.free R P here is explicit rather than an