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

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

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

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, Nonempty (Basis I R M)

theorem Module.free_iff_set (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Module.Free R M ↔ ∃ S, 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 (_ : ∃ S, Nonempty (Basis (↑S) R M)))

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 (_ : Nonempty (Basis (↑(Exists.choose (_ : ∃ S, Nonempty (Basis (↑S) R M)))) R M))

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

• Module.Free.noZeroSMulDivisors = Module.Free.noZeroSMulDivisors.proof_1

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

• Module.Free.instNonemptyChooseBasisIndex = Module.Free.instNonemptyChooseBasisIndex.proof_1

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

• Module.Free.self = Module.Free.self.proof_1

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

• Module.Free.prod = Module.Free.prod.proof_1

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

• @Module.Free.pi = @Module.Free.pi.proof_1

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

• Module.Free.matrix = Module.Free.matrix.proof_1

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

• Module.Free.ulift = Module.Free.ulift.proof_1

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

• Module.Free.function = Module.Free.function.proof_1

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

• Module.Free.finsupp = Module.Free.finsupp.proof_1

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

• Module.Free.of_subsingleton = Module.Free.of_subsingleton.proof_1

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

• Module.Free.of_subsingleton' = Module.Free.of_subsingleton'.proof_1

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

• Module.Free.dfinsupp = Module.Free.dfinsupp.proof_1

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 (⨁ (i : ι), M i)

Equations

• Module.Free.directSum = Module.Free.directSum.proof_1

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

Equations

• Module.Free.tensor = Module.Free.tensor.proof_1