Finite-dimensional vector spaces

This file defines finite-dimensional vector spaces and shows our definition is equivalent to alternative definitions.

Main definitions

Assume V is a vector space over a division ring K. There are (at least) three equivalent definitions of finite-dimensionality of V:

• it admits a finite basis.
• it is finitely generated.
• it is Noetherian, i.e., every subspace is finitely generated.

We introduce a typeclass FiniteDimensional K V capturing this property. For ease of transfer of proof, it is defined using the second point of view, i.e., as Module.Finite. However, we prove that all these points of view are equivalent, with the following lemmas (in the namespace FiniteDimensional):

• Module.finBasis and Module.finBasisOfFinrankEq are bases for finite-dimensional vector spaces, where the index type is Fin (in Mathlib/LinearAlgebra/Dimension/Free.lean)
• fintypeBasisIndex states that a finite-dimensional vector space has a finite basis
• of_fintype_basis states that the existence of a basis indexed by a finite type implies finite-dimensionality
• of_finite_basis states that the existence of a basis indexed by a finite set implies finite-dimensionality
• of_finrank_pos states that a nonzero finrank (implying non-infinite dimension) implies finite-dimensionality
• IsNoetherian.iff_fg states that the space is finite-dimensional if and only if it is Noetherian (in Mathlib/FieldTheory/Finiteness.lean)

We make use of finrank, the dimension of a finite-dimensional space, returning a Nat, as opposed to Module.rank, which returns a Cardinal. When the space has infinite dimension, its finrank is by convention set to 0. finrank is not defined using FiniteDimensional. For basic results that do not need the FiniteDimensional class, import Mathlib/LinearAlgebra/Finrank.lean.

Preservation of finite-dimensionality and formulas for the dimension are given for

• submodules (FiniteDimensional.finiteDimensional_submodule)
• linear equivs, in LinearEquiv.finiteDimensional

Implementation notes

You should not assume that there has been any effort to state lemmas as generally as possible.

Plenty of the results hold for general fg modules or Noetherian modules, and they can be found in Mathlib/LinearAlgebra/FreeModule/Finite/Rank.lean and Mathlib/RingTheory/Noetherian.lean.

@[reducible, inline]

abbrev FiniteDimensional (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop

FiniteDimensional vector spaces are defined to be finite modules. Use FiniteDimensional.of_fintype_basis to prove finite dimension from another definition.

Equations

• FiniteDimensional K V = Module.Finite K V

theorem FiniteDimensional.of_injective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V →ₗ[K] V₂) (w : Function.Injective ⇑f) [FiniteDimensional K V₂] : FiniteDimensional K V

If the codomain of an injective linear map is finite dimensional, the domain must be as well.

theorem FiniteDimensional.of_surjective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V →ₗ[K] V₂) (w : Function.Surjective ⇑f) [FiniteDimensional K V] : FiniteDimensional K V₂

If the domain of a surjective linear map is finite dimensional, the codomain must be as well.

instance FiniteDimensional.finiteDimensional_pi (K : Type u) [DivisionRing K] {ι : Type u_1} [Finite ι] : FiniteDimensional K (ι → K)

instance FiniteDimensional.finiteDimensional_pi' (K : Type u) [DivisionRing K] {ι : Type u_1} [Finite ι] (M : ι → Type u_2) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module K (M i)] [∀ (i : ι), FiniteDimensional K (M i)] : FiniteDimensional K ((i : ι) → M i)

theorem FiniteDimensional.of_fintype_basis {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type w} [Finite ι] (h : Module.Basis ι K V) : FiniteDimensional K V

If a vector space has a finite basis, then it is finite-dimensional.

noncomputable def FiniteDimensional.fintypeBasisIndex {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [FiniteDimensional K V] (b : Module.Basis ι K V) : Fintype ι

If a vector space is FiniteDimensional, all bases are indexed by a finite type

Equations

• FiniteDimensional.fintypeBasisIndex b = Fintype.ofFinite ι

noncomputable instance FiniteDimensional.instFintypeElemOfVectorSpaceIndex {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : Fintype ↑(Module.Basis.ofVectorSpaceIndex K V)

If a vector space is FiniteDimensional, Basis.ofVectorSpace is indexed by a finite type.

Equations

• FiniteDimensional.instFintypeElemOfVectorSpaceIndex = FiniteDimensional.fintypeBasisIndex (Module.Basis.ofVectorSpace K V)

theorem FiniteDimensional.of_finite_basis {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type w} {s : Set ι} (h : Module.Basis (↑s) K V) (hs : s.Finite) : FiniteDimensional K V

If a vector space has a basis indexed by elements of a finite set, then it is finite-dimensional.

instance FiniteDimensional.finiteDimensional_submodule {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (S : Submodule K V) : FiniteDimensional K ↥S

A subspace of a finite-dimensional space is also finite-dimensional.

This is a shortcut instance to simplify inference in the presence of [FiniteDimensional K V].

instance FiniteDimensional.finiteDimensional_quotient {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (S : Submodule K V) : FiniteDimensional K (V ⧸ S)

A quotient of a finite-dimensional space is also finite-dimensional.

theorem FiniteDimensional.of_finrank_pos {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : 0 < Module.finrank K V) : FiniteDimensional K V

theorem FiniteDimensional.of_finrank_eq_succ {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (hn : Module.finrank K V = n.succ) : FiniteDimensional K V

theorem FiniteDimensional.of_fact_finrank_eq_succ {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (n : ℕ) [hn : Fact (Module.finrank K V = n + 1)] : FiniteDimensional K V

We can infer FiniteDimensional K V in the presence of [Fact (finrank K V = n + 1)]. Use have : FiniteDimensional K V := .of_fact_finrank_eq_succ when needed.

This is not an instance because n cannot be inferred.

theorem Module.finrank_eq_rank' (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : ↑(finrank K V) = Module.rank K V

In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its finrank. This is a copy of finrank_eq_rank _ _ which creates easier typeclass searches.

theorem Module.finrank_of_infinite_dimensional {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : ¬FiniteDimensional K V) : finrank K V = 0

theorem Module.finiteDimensional_iff_of_rank_eq_nsmul {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {W : Type v} [AddCommGroup W] [Module K W] {n : ℕ} (hn : n ≠ 0) (hVW : Module.rank K V = n • Module.rank K W) : FiniteDimensional K V ↔ FiniteDimensional K W

theorem Module.finrank_eq_card_basis' {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type w} (h : Basis ι K V) : ↑(finrank K V) = Cardinal.mk ι

If a vector space is finite-dimensional, then the cardinality of any basis is equal to its finrank.

instance FiniteDimensional.finiteDimensional_self (K : Type u) [DivisionRing K] : FiniteDimensional K K

theorem FiniteDimensional.span_of_finite (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {A : Set V} (hA : A.Finite) : FiniteDimensional K ↥(Submodule.span K A)

The submodule generated by a finite set is finite-dimensional.

instance FiniteDimensional.span_singleton (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (x : V) : FiniteDimensional K ↥(Submodule.span K {x})

The submodule generated by a single element is finite-dimensional.

instance FiniteDimensional.span_finset (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Finset V) : FiniteDimensional K ↥(Submodule.span K ↑s)

The submodule generated by a finset is finite-dimensional.

instance FiniteDimensional.instSubtypeMemSubmoduleMapLinearMapId (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V) [FiniteDimensional K ↥p] : FiniteDimensional K ↥(Submodule.map f p)

Pushforwards of finite-dimensional submodules are finite-dimensional.

theorem FiniteDimensional.trans (F : Type u_1) (K : Type u_2) (A : Type u_3) [DivisionRing F] [DivisionRing K] [AddCommGroup A] [Module F K] [Module K A] [Module F A] [IsScalarTower F K A] [FiniteDimensional F K] [FiniteDimensional K A] : FiniteDimensional F A

theorem Submodule.fg_iff_finiteDimensional {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) : s.FG ↔ FiniteDimensional K ↥s

A submodule is finitely generated if and only if it is finite-dimensional

theorem LinearEquiv.finiteDimensional {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V ≃ₗ[K] V₂) [FiniteDimensional K V] : FiniteDimensional K V₂

Finite dimensionality is preserved under linear equivalence.