# 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) [] [] [Module R M] :

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

Instances
theorem Module.Free.exists_basis {R : Type u} {M : Type v} [] [] [Module R M] [self : ] :
Nonempty ((I : Type v) × Basis I R M)
theorem Module.free_def (R : Type u) (M : Type v) [] [] [Module 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) [] [] [Module R M] :
∃ (S : Set M), Nonempty (Basis (S) R M)
theorem Module.Free.of_basis {R : Type u} {M : Type v} [] [] [Module R M] {ι : Type w} (b : Basis ι R M) :
def Module.Free.ChooseBasisIndex (R : Type u) (M : Type v) [] [] [Module R M] [] :

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
• = .choose
Instances For
noncomputable instance Module.Free.instDecidableEqChooseBasisIndex (R : Type u) (M : Type v) [] [] [Module R M] [] :

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

Equations
noncomputable def Module.Free.chooseBasis (R : Type u) (M : Type v) [] [] [Module R M] [] :

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

Equations
• = .some
Instances For
noncomputable def Module.Free.repr (R : Type u) (M : Type v) [] [] [Module R M] [] :

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

Equations
• = ().repr
Instances For
noncomputable def Module.Free.constr (R : Type u) (M : Type v) (N : Type z) [] [] [Module R M] [] [] [Module R N] {S : Type z} [] [Module S 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
• = ().constr S
Instances For
@[instance 100]
instance Module.Free.noZeroSMulDivisors (R : Type u) (M : Type v) [] [] [Module R M] [] [] :
Equations
• =
instance Module.Free.instNonemptyChooseBasisIndexOfNontrivial (R : Type u) (M : Type v) [] [] [Module R M] [] [] :
Equations
• =
theorem Module.Free.infinite (R : Type u) (M : Type v) [] [] [Module R M] [] [] [] :
theorem Module.Free.of_equiv {R : Type u} {M : Type v} {N : Type z} [] [] [Module R M] [] [] [Module R N] (e : M ≃ₗ[R] N) :
theorem Module.Free.of_equiv' {R : Type u} {N : Type z} [] [] [Module R N] {P : Type v} [] [Module R P] :
(P ≃ₗ[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) [] :

The module structure provided by Semiring.toModule is free.

Equations
• =
instance Module.Free.prod (R : Type u) (M : Type v) (N : Type z) [] [] [Module R M] [] [] [Module R N] [] :
Module.Free R (M × N)
Equations
• =
instance Module.Free.pi {ι : Type u_1} (R : Type u) [] (M : ιType u_2) [] [(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) [] [] [Module R M] [] {m : Type u_2} {n : Type u_3} [] [] :

The module of finite matrices is free.

Equations
• =
instance Module.Free.ulift (R : Type u) (M : Type v) [] [] [Module R M] [] :
Equations
• =
instance Module.Free.function (ι : Type u_1) (R : Type u) (M : Type v) [] [] [Module R M] [] [] :
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) [] [] [Module R M] [] :
Equations
• =
@[instance 100]
instance Module.Free.of_subsingleton (R : Type u) (N : Type z) [] [] [Module R N] [] :
Equations
• =
@[instance 100]
instance Module.Free.of_subsingleton' (R : Type u) (N : Type z) [] [] [Module R N] [] :
Equations
• =
instance Module.Free.dfinsupp (R : Type u) [] {ι : 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) [] {ι : 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) [] [] [Module R M] [] [] [Module R N] [] :
Equations
• =