Documentation

Mathlib.LinearAlgebra.FreeModule.Basic

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 #

class Module.Free (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [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} :
    ∀ {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M} [self : Module.Free R M], 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) :

    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
    Instances For

      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) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] :

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

      Equations
      Instances For
        noncomputable def Module.Free.repr (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] :

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

        Equations
        Instances For
          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] :

          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
          Instances For
            @[instance 100]
            Equations
            • =
            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) :
            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] :

            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] :

            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] :
            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] :
            Equations
            • =
            @[instance 100]
            Equations
            • =
            @[instance 100]
            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) {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [Module.Free S M] [AddCommMonoid N] [Module R N] [Module.Free R N] :
            Equations
            • =