Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Module docstring

{"# Finite and free modules

We provide some instances for finite and free modules.

Main results

Module.Free.ChooseBasisIndex.fintype : If a free module is finite, then any basis is finite.
Module.Finite.of_basis : A free module with a basis indexed by a Fintype is finite. "}

Module.Free.ChooseBasisIndex.fintype instance

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

Full source

/-- If a free module is finite, then the arbitrary basis is finite. -/
noncomputable instance Module.Free.ChooseBasisIndex.fintype (R : Type u) (M : Type v)
    [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] :
    Fintype (Module.Free.ChooseBasisIndex R M) := by
  refine @Fintype.ofFinite _ ?_
  cases subsingleton_or_nontrivial R
  · have := Module.subsingleton R M
    rw [ChooseBasisIndex]
    infer_instance
  · exact Module.Finite.finite_basis (chooseBasis _ _)

Finiteness of Basis Index Set for Finitely Generated Free Modules

Informal description

For any finitely generated free module $M$ over a semiring $R$, the index set of any basis of $M$ is finite.

Module.Finite.of_basis theorem

{R M ι : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [_root_.Finite ι] (b : Basis ι R M) : Module.Finite R M

Full source

/-- A free module with a basis indexed by a `Fintype` is finite. -/
theorem Module.Finite.of_basis {R M ι : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
    [_root_.Finite ι] (b : Basis ι R M) : Module.Finite R M := by
  cases nonempty_fintype ι
  classical
    refine ⟨⟨Finset.univ.image b, ?_⟩⟩
    simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]

Finitely Generated Module from Finite Basis

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. If $M$ has a basis indexed by a finite type $\iota$, then $M$ is finitely generated as an $R$-module.

Module.Finite.matrix instance

 {R ι₁ ι₂ M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M]
  [_root_.Finite ι₁] [_root_.Finite ι₂] : Module.Finite R (Matrix ι₁ ι₂ M)

Full source

instance Module.Finite.matrix {R ι₁ ι₂ M : Type*}
    [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M]
    [_root_.Finite ι₁] [_root_.Finite ι₂] :
    Module.Finite R (Matrix ι₁ ι₂ M) := by
  cases nonempty_fintype ι₁
  cases nonempty_fintype ι₂
  exact Module.Finite.of_basis <| (Free.chooseBasis _ _).matrix _ _

Finitely Generated Matrix Module over Free Module

Informal description

For any semiring $R$, free $R$-module $M$, and finite types $\iota_1$ and $\iota_2$, the matrix space $\text{Matrix}_{\iota_1 \times \iota_2}(M)$ is a finitely generated $R$-module.