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.linearCombination_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 Module.Free (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop

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

• exists_basis : Nonempty ((I : Type v) × Basis I R M)

theorem Module.Free.exists_set (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] : ∃ (S : Set M), Nonempty (Basis (↑S) R M)

theorem Module.free_iff_set (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Free R M ↔ ∃ (S : Set M), Nonempty (Basis (↑S) R M)

theorem Module.free_def (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Small.{w, v} M] : Free R M ↔ ∃ (I : Type w), Nonempty (Basis I R M)

If M fits in universe w, then freeness is equivalent to existence of a basis in that universe.

Note that if M does not fit in w, the reverse direction of this implication is still true as Module.Free.of_basis.

theorem Module.Free.of_basis {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type w} (b : Basis ι R M) : Free R M

def Module.Free.ChooseBasisIndex (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] : Type v

If Module.Free R M then ChooseBasisIndex R M is the ι which indexes the basis ι → M. Note that this is defined such that this type is finite if R is trivial.

Equations

• Module.Free.ChooseBasisIndex R M = ↑⋯.choose

noncomputable instance Module.Free.instDecidableEqChooseBasisIndex (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] : DecidableEq (ChooseBasisIndex R M)

There is no hope of computing this, but we add the instance anyway to avoid fumbling with open scoped Classical.

Equations

• Module.Free.instDecidableEqChooseBasisIndex R M = Classical.decEq (Module.Free.ChooseBasisIndex R M)

noncomputable def Module.Free.chooseBasis (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] : Basis (ChooseBasisIndex R M) R M

If Module.Free R M then chooseBasis : ι → M is the basis. Here ι = ChooseBasisIndex R M.

Equations

• Module.Free.chooseBasis R M = ⋯.some

@[deprecated Module.Free.chooseBasis (since := "2025-08-01")]

noncomputable def Module.Free.repr (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] : M ≃ₗ[R] ChooseBasisIndex R M →₀ R

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

Equations

• Module.Free.repr R M = (Module.Free.chooseBasis R M).repr

noncomputable def Module.Free.constr (R : Type u) (M : Type v) (N : Type z) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] [AddCommMonoid N] [Module R N] {S : Type z} [Semiring S] [Module S N] [SMulCommClass R S N] : (ChooseBasisIndex R M → N) ≃ₗ[S] M →ₗ[R] N

The universal property of free modules: giving a function (ChooseBasisIndex 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 SMulCommClass R S M' holds. If R is commutative, you can set S := R; if R is not commutative, you can recover an AddEquiv by setting S := ℕ. See library note [bundled maps over different rings].

Equations

• Module.Free.constr R M N = (Module.Free.chooseBasis R M).constr S

@[instance 100]

instance Module.Free.noZeroSMulDivisors (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] [NoZeroDivisors R] : NoZeroSMulDivisors R M

instance Module.Free.instNonemptyChooseBasisIndexOfNontrivial (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] [Nontrivial M] : Nonempty (ChooseBasisIndex R M)

theorem Module.Free.infinite (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] [Infinite R] [Nontrivial M] : Infinite M

instance Module.Free.instFaithfulSMulOfNontrivial (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] [Nontrivial M] : FaithfulSMul R M

theorem Module.Free.of_equiv {R : Type u} {M : Type v} {N : Type z} [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) : Free R N

theorem Module.Free.of_equiv' {R : Type u} {N : Type z} [Semiring R] [AddCommMonoid N] [Module R N] {P : Type v} [AddCommMonoid P] [Module R P] : Free R P → ∀ (e : P ≃ₗ[R] N), Free R N

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

theorem Module.Free.of_ringEquiv {R : Type u_2} {R' : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R'] [AddCommMonoid M'] [Module R' M'] (e₁ : R ≃+* R') (e₂ : M ≃ₛₗ[↑e₁] M') [Free R M] : Free R' M'

theorem Module.Free.iff_of_ringEquiv {R : Type u_2} {R' : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R'] [AddCommMonoid M'] [Module R' M'] (e₁ : R ≃+* R') (e₂ : M ≃ₛₗ[↑e₁] M') : Free R M ↔ Free R' M'

instance Module.Free.self (R : Type u) [Semiring R] : Free R R

The module structure provided by Semiring.toModule is free.

instance Module.Free.ulift (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] : Free R (ULift.{u_2, v} M)

@[instance 100]

instance Module.Free.of_subsingleton (R : Type u) (N : Type z) [Semiring R] [AddCommMonoid N] [Module R N] [Subsingleton N] : Free R N

theorem Module.Free.of_subsingleton' (R : Type u) (N : Type z) [Semiring R] [AddCommMonoid N] [Module R N] [Subsingleton R] : Free R N

theorem Module.Basis.repr_algebraMap {R : Type u} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {ι : Type u_3} {B : Basis ι R S} {i : ι} (hBi : B i = 1) (r : R) : B.repr ((algebraMap R S) r) = Finsupp.single i r

If B is a basis of the R-algebra S such that B i = 1 for some index i, then each r : R gets represented as s • B i as an element of S.