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 #

source
@[class]
structure module.free (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] :
Prop

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

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

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
source
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] :
basis (module.free.choose_basis_index R M) R M

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

Equations
source
noncomputable def module.free.repr (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] [module.free R M] :
M ≃ₗ[R] module.free.choose_basis_index R M →₀ R

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

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

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

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

The module structure provided by semiring.to_module is free.

source
@[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)
source
@[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.

source
@[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] :
module.free R (matrix m n M)

The module of finite matrices is free.

source
@[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).

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