# mathlib3documentation

linear_algebra.free_module.basic

# Free modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Instances of this typeclass
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
def module.free.choose_basis_index (R : Type u) (M : Type v) [semiring R] [ M] [ M] :

If module.free R M then choose_basis_index R M is the ι which indexes the basis ι → M.

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

If module.free R M then choose_basis : ι → M is the basis. Here ι = choose_basis_index R M.

Equations
noncomputable 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
noncomputable 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] :

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
@[protected, instance]
def module.free.no_zero_smul_divisors (R : Type u) (M : Type v) [semiring R] [ M] [ M]  :
@[protected, instance]
def module.free.choose_basis_index.nonempty (R : Type u) (M : Type v) [semiring R] [ M] [ M] [nontrivial 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.

@[protected, instance]
def module.free.self (R : Type u) [semiring R] :
R

The module structure provided by semiring.to_module is free.

@[protected, instance]
def module.free.prod (R : Type u) (M : Type v) (N : Type z) [semiring R] [ M] [ M] [ N] [ N] :
(M × N)
@[protected, instance]
def module.free.pi {ι : Type u_1} (R : Type u) [semiring R] (M : ι Type u_2) [finite ι] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), (M i)] [ (i : ι), (M i)] :
(Π (i : ι), M i)

The product of finitely many free modules is free.

@[protected, instance]
def module.free.matrix (R : Type u) (M : Type v) [semiring R] [ M] [ M] {m : Type u_1} {n : Type u_2} [finite m] [finite n] :
(matrix m n M)

The module of finite matrices is free.

@[protected, instance]
def module.free.function (ι : Type u_1) (R : Type u) (M : Type v) [semiring R] [ M] [ M] [finite ι] :
M)

The product of finitely many free modules is free (non-dependent version to help with typeclass search).

@[protected, instance]
def module.free.finsupp (ι : Type u_1) (R : Type u) (M : Type v) [semiring R] [ M] [ M] :
→₀ M)
@[protected, instance]
def module.free.of_subsingleton (R : Type u) (N : Type z) [semiring R] [ N] [subsingleton N] :
N
@[protected, instance]
def module.free.of_subsingleton' (R : Type u) (N : Type z) [semiring R] [ N] [subsingleton R] :
N
@[protected, 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)
@[protected, 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))
@[protected, instance]
def module.free.tensor (R : Type u) (M : Type v) (N : Type z) [comm_ring R] [ M] [ M] [ N] [ N] :
M N)
@[protected, instance]
def module.free.of_division_ring (R : Type u) (M : Type v) [ M] :
M