mathlib3 documentation

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 #

theorem module.free_def (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] [small M] :
module.free R M (I : Type w), nonempty (basis I R M)
theorem module.free_iff_set (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] :
module.free R M (S : set M), nonempty (basis S R M)
theorem module.free.of_basis {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] {ι : Type w} (b : basis ι R 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] [add_comm_monoid M] [module R M] [module.free R 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] [add_comm_monoid M] [module R M] [module.free R 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] [add_comm_monoid M] [module R M] [module.free R M] [add_comm_monoid N] [module R N] {S : Type z} [semiring S] [module S N] [smul_comm_class R S 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
@[protected, instance]
theorem module.free.of_equiv {R : Type u} {M : Type v} {N : Type z} [semiring R] [add_comm_monoid M] [module R M] [module.free R M] [add_comm_monoid N] [module R N] (e : M ≃ₗ[R] N) :
theorem module.free.of_equiv' {R : Type u} {N : Type z} [semiring R] [add_comm_monoid N] [module R N] {P : Type v} [add_comm_monoid P] [module R P] (h : module.free R P) (e : P ≃ₗ[R] 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] :

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] [add_comm_monoid M] [module R M] [module.free R M] [add_comm_monoid N] [module R N] [module.free R N] :
module.free R (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 : ι), module R (M i)] [ (i : ι), module.free R (M i)] :
module.free R (Π (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] [add_comm_monoid M] [module R M] [module.free R M] {m : Type u_1} {n : Type u_2} [finite m] [finite n] :

The module of finite matrices is free.

@[protected, instance]
def module.free.function (ι : Type u_1) (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] [module.free R M] [finite ι] :
module.free R 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] [add_comm_monoid M] [module R M] [module.free R M] :
@[protected, instance]
@[protected, instance]
@[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 : ι), module R (M i)] [ (i : ι), module.free R (M i)] :
module.free R (Π₀ (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 : ι), module R (M i)] [ (i : ι), module.free R (M i)] :
module.free R (direct_sum ι (λ (i : ι), M i))
@[protected, instance]
def module.free.tensor (R : Type u) (M : Type v) (N : Type z) [comm_ring R] [add_comm_group M] [module R M] [module.free R M] [add_comm_group N] [module R N] [module.free R N] :
@[protected, instance]