# mathlibdocumentation

linear_algebra.free_module

# Free modules #

We introduce a class module.free R M, for R a semiring and M an R-module and we provide several basic instances for this class.

Use 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 R-modules.
@[class]
structure module.free (R : Type u) (M : Type v) [semiring R] [ M] :
Prop
• exists_basis : nonempty (Σ (I : Type ?), R M)

module.free R M is the statement that the R-module M is free.

Instances
theorem module.free_def (R : Type u) (M : Type v) [semiring R] [ M] [small M] :
M ∃ (I : Type w), nonempty (basis I R M)
theorem module.free_iff_set (R : Type u) (M : Type v) [semiring R] [ M] :
M ∃ (S : set M), nonempty (basis S R M)
theorem module.free.of_basis {R : Type u} {M : Type v} [semiring R] [ M] {ι : Type w} (b : R M) :
M
@[nolint]
def module.free.choose_basis_index (R : Type u) (M : Type v) [semiring R] [ M] [ M] :
Type v

If [finite_free R M] then choose_basis_index R M is the ι which indexes the basis ι → M.

Equations
def module.free.choose_basis (R : Type u) (M : Type v) [semiring R] [ M] [ M] :
M

If [finite_free R M] then choose_basis : ι → M is the basis. Here ι = choose_basis_index R M.

Equations
def module.free.repr (R : Type u) (M : Type v) [semiring R] [ M] [ M] :

The isomorphism M ≃ₗ[R] (choose_basis_index R M →₀ R).

Equations
def module.free.constr (R : Type u) (M : Type v) (N : Type z) [semiring R] [ M] [ M] [ N] {S : Type z} [semiring S] [ N] [ N] :
→ N) ≃ₗ[S] M →ₗ[R] N

The universal property of free modules: giving a functon (choose_basis_index R M) → N, for N an R-module, is the same as giving an R-linear map M →ₗ[R] N.

This definition is parameterized over an extra semiring S, such that smul_comm_class R S M' holds. If 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].

Equations
• N = S
@[instance]
def module.free.no_zero_smul_divisors (R : Type u) (M : Type v) [semiring R] [ M] [ M]  :
theorem module.free.of_equiv {R : Type u} {M : Type v} {N : Type z} [semiring R] [ M] [ M] [ N] (e : M ≃ₗ[R] N) :
N
theorem module.free.of_equiv' {R : Type u} {N : Type z} [semiring R] [ N] {P : Type v} [ P] (h : P) (e : P ≃ₗ[R] N) :
N

A variation of of_equiv: the assumption module.free R P here is explicit rather than an instance.

@[instance]
def module.free.finsupp.free (R : Type u) [semiring R] {ι : Type v} :
→₀ R)
@[instance]
def module.free.pi.free (R : Type u) [semiring R] {ι : Type v} [fintype ι] :
(ι → R)
@[instance]
def module.free.prod (R : Type u) (M : Type v) (N : Type z) [semiring R] [ M] [ M] [ N] [ N] :
(M × N)
@[instance]
def module.free.self (R : Type u) [semiring R] :
R
@[instance]
def module.free.of_subsingleton (R : Type u) (N : Type z) [semiring R] [ N] [subsingleton N] :
N
@[instance]
def module.free.dfinsupp (R : Type u) [semiring R] {ι : Type u_1} (M : ι → Type u_2) [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] [∀ (i : ι), (M i)] :
(Π₀ (i : ι), M i)
@[instance]
def module.free.direct_sum (R : Type u) [semiring R] {ι : Type u_1} (M : ι → Type u_2) [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] [∀ (i : ι), (M i)] :
(⨁ (i : ι), M i)
@[instance]
def module.free.pi (R : Type u) [semiring R] {ι : Type u_1} [fintype ι] {M : ι → Type u_2} [Π (i : ι), add_comm_group (M i)] [Π (i : ι), (M i)] [∀ (i : ι), (M i)] :
(Π (i : ι), M i)
@[instance]
def module.free.tensor (R : Type u) (M : Type v) (N : Type z) [comm_ring R] [ M] [ N] [ M] [ N] :
(M N)
@[instance]
def module.free.of_division_ring (R : Type u) (M : Type v) [ M] :
M