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 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_def (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Small.{w, v} M] : Module.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_iff_set (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid 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] [AddCommMonoid M] [Module R M] {ι : Type w} (b : Basis ι R M) : Module.Free R M

def Module.Free.ChooseBasisIndex (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.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 = ↑(Exists.choose ⋯)

noncomputable instance Module.Free.instDecidableEqChooseBasisIndex (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] : DecidableEq (Module.Free.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] [Module.Free R M] : Basis (Module.Free.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 = Nonempty.some ⋯

noncomputable def Module.Free.repr (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] : M ≃ₗ[R] Module.Free.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] [Module.Free R M] [AddCommMonoid N] [Module R N] {S : Type z} [Semiring S] [Module S N] [SMulCommClass R S N] : (Module.Free.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 = Basis.constr (Module.Free.chooseBasis R M) S

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

theorem Module.Free.of_equiv {R : Type u} {M : Type v} {N : Type z} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) : Module.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] : Module.Free R P → (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.

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

The module structure provided by Semiring.toModule is free.

Equations

• ⋯ = ⋯

instance Module.Free.prod (R : Type u) (M : Type v) (N : Type z) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [AddCommMonoid N] [Module R N] [Module.Free R N] : Module.Free R (M × N)

Equations

• ⋯ = ⋯

instance Module.Free.pi {ι : Type u_1} (R : Type u) [Semiring R] (M : ι → Type u_2) [Finite ι] [(i : ι) → AddCommMonoid (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.

Equations

• ⋯ = ⋯

instance Module.Free.matrix (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] {m : Type u_2} {n : Type u_3} [Finite m] [Finite n] : Module.Free R (Matrix m n M)

The module of finite matrices is free.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance Module.Free.function (ι : Type u_1) (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid 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).

Equations

• ⋯ = ⋯

instance Module.Free.finsupp (ι : Type u_1) (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] : Module.Free R (ι →₀ M)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance Module.Free.dfinsupp (R : Type u) [Semiring R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] : Module.Free R (Π₀ (i : ι), M i)

Equations

• ⋯ = ⋯

instance Module.Free.directSum (R : Type u) [Semiring R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] : Module.Free R (DirectSum ι fun (i : ι) => M i)

Equations

• ⋯ = ⋯

instance Module.Free.tensor (R : Type u) (M : Type v) (N : Type z) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [AddCommMonoid N] [Module R N] [Module.Free R N] : Module.Free R (TensorProduct R M N)

Equations

• ⋯ = ⋯