Mathlib.LinearAlgebra.FiniteDimensional.Defs

Module docstring

{"# 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)
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)

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.

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 notherian modules, and they can be found in Mathlib.LinearAlgebra.FreeModule.Finite.Rank and Mathlib.RingTheory.Noetherian. "}

FiniteDimensional abbrev

(K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]

Full source

/-- `FiniteDimensional` vector spaces are defined to be finite modules.
Use `FiniteDimensional.of_fintype_basis` to prove finite dimension from another definition. -/
abbrev FiniteDimensional (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V] :=
  Module.Finite K V

Definition of Finite-Dimensional Vector Space

Informal description

A vector space $V$ over a division ring $K$ is called *finite-dimensional* if it is finitely generated as a $K$-module. This means there exists a finite set of vectors in $V$ whose linear span over $K$ is the entire space $V$.

FiniteDimensional.of_injective theorem

(f : V →ₗ[K] V₂) (w : Function.Injective f) [FiniteDimensional K V₂] : FiniteDimensional K V

Full source

/-- If the codomain of an injective linear map is finite dimensional, the domain must be as well. -/
theorem of_injective (f : V →ₗ[K] V₂) (w : Function.Injective f) [FiniteDimensional K V₂] :
    FiniteDimensional K V :=
  Module.Finite.of_injective f w

Injective Linear Maps Preserve Finite-Dimensionality (Domain)

Informal description

Let $V$ and $V_2$ be vector spaces over a division ring $K$, and let $f \colon V \to V_2$ be an injective linear map. If $V_2$ is finite-dimensional, then $V$ is also finite-dimensional.

FiniteDimensional.of_surjective theorem

(f : V →ₗ[K] V₂) (w : Function.Surjective f) [FiniteDimensional K V] : FiniteDimensional K V₂

Full source

/-- If the domain of a surjective linear map is finite dimensional, the codomain must be as well. -/
theorem of_surjective (f : V →ₗ[K] V₂) (w : Function.Surjective f) [FiniteDimensional K V] :
    FiniteDimensional K V₂ :=
  Module.Finite.of_surjective f w

Surjective Linear Maps Preserve Finite-Dimensionality

Informal description

Let $V$ and $V_2$ be vector spaces over a division ring $K$, and let $f : V \to V_2$ be a surjective linear map. If $V$ is finite-dimensional, then $V_2$ is also finite-dimensional.

FiniteDimensional.finiteDimensional_pi instance

{ι : Type*} [Finite ι] : FiniteDimensional K (ι → K)

Full source

instance finiteDimensional_pi {ι : Type*} [Finite ι] : FiniteDimensional K (ι → K) :=
  Finite.pi

Finite-Dimensionality of Function Spaces over Finite Types

Informal description

For any finite type $\iota$ and division ring $K$, the function space $\iota \to K$ is a finite-dimensional vector space over $K$.

FiniteDimensional.finiteDimensional_pi' instance

 {ι : Type*} [Finite ι] (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module K (M i)]
  [∀ i, FiniteDimensional K (M i)] : FiniteDimensional K (∀ i, M i)

Full source

instance finiteDimensional_pi' {ι : Type*} [Finite ι] (M : ι → Type*) [∀ i, AddCommGroup (M i)]
    [∀ i, Module K (M i)] [∀ i, FiniteDimensional K (M i)] : FiniteDimensional K (∀ i, M i) :=
  Finite.pi

Finite-Dimensionality of Product Spaces

Informal description

For any finite index type $\iota$ and a family of finite-dimensional vector spaces $M_i$ over a division ring $K$ indexed by $\iota$, the product space $\prod_{i} M_i$ is also finite-dimensional over $K$.

FiniteDimensional.of_fintype_basis theorem

{ι : Type w} [Finite ι] (h : Basis ι K V) : FiniteDimensional K V

Full source

/-- If a vector space has a finite basis, then it is finite-dimensional. -/
theorem of_fintype_basis {ι : Type w} [Finite ι] (h : Basis ι K V) : FiniteDimensional K V :=
  Module.Finite.of_basis h

Finite-dimensionality from finite basis

Informal description

Let $V$ be a vector space over a division ring $K$. If there exists a basis $\{v_i\}_{i \in \iota}$ for $V$ indexed by a finite type $\iota$, then $V$ is finite-dimensional over $K$.

FiniteDimensional.fintypeBasisIndex definition

{ι : Type*} [FiniteDimensional K V] (b : Basis ι K V) : Fintype ι

Full source

/-- If a vector space is `FiniteDimensional`, all bases are indexed by a finite type -/
noncomputable def fintypeBasisIndex {ι : Type*} [FiniteDimensional K V] (b : Basis ι K V) :
    Fintype ι :=
  @Fintype.ofFinite _ (Module.Finite.finite_basis b)

Finiteness of basis index in finite-dimensional vector spaces

Informal description

For any finite-dimensional vector space $V$ over a division ring $K$ and any basis $b$ of $V$ indexed by type $\iota$, the index type $\iota$ is finite. In other words, every basis of a finite-dimensional vector space is indexed by a finite type.

FiniteDimensional.instFintypeElemOfVectorSpaceIndex instance

[FiniteDimensional K V] : Fintype (Basis.ofVectorSpaceIndex K V)

Full source

/-- If a vector space is `FiniteDimensional`, `Basis.ofVectorSpace` is indexed by
  a finite type. -/
noncomputable instance [FiniteDimensional K V] : Fintype (Basis.ofVectorSpaceIndex K V) :=
  fintypeBasisIndex (Basis.ofVectorSpace K V)

Finiteness of Basis Index in Finite-Dimensional Vector Spaces

Informal description

For any finite-dimensional vector space $V$ over a division ring $K$, the index set of the basis obtained from `Basis.ofVectorSpace` is finite.

FiniteDimensional.of_finite_basis theorem

{ι : Type w} {s : Set ι} (h : Basis s K V) (hs : Set.Finite s) : FiniteDimensional K V

Full source

/-- If a vector space has a basis indexed by elements of a finite set, then it is
finite-dimensional. -/
theorem of_finite_basis {ι : Type w} {s : Set ι} (h : Basis s K V) (hs : Set.Finite s) :
    FiniteDimensional K V :=
  haveI := hs.fintype
  of_fintype_basis h

Finite-dimensionality from basis indexed by finite set

Informal description

Let $V$ be a vector space over a division ring $K$. If there exists a basis $\{v_i\}_{i \in s}$ for $V$ indexed by a finite set $s \subset \iota$, then $V$ is finite-dimensional over $K$.

FiniteDimensional.finiteDimensional_submodule instance

[FiniteDimensional K V] (S : Submodule K V) : FiniteDimensional K S

Full source

/-- 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_submodule [FiniteDimensional K V] (S : Submodule K V) :
    FiniteDimensional K S := by
  infer_instance

Finite-Dimensionality of Subspaces

Informal description

Every subspace $S$ of a finite-dimensional vector space $V$ over a division ring $K$ is itself finite-dimensional.

FiniteDimensional.finiteDimensional_quotient instance

[FiniteDimensional K V] (S : Submodule K V) : FiniteDimensional K (V ⧸ S)

Full source

/-- A quotient of a finite-dimensional space is also finite-dimensional. -/
instance finiteDimensional_quotient [FiniteDimensional K V] (S : Submodule K V) :
    FiniteDimensional K (V ⧸ S) :=
  Module.Finite.quotient K S

Finite-Dimensionality of Quotient Spaces

Informal description

For any finite-dimensional vector space $V$ over a division ring $K$ and any submodule $S$ of $V$, the quotient space $V/S$ is also finite-dimensional.

FiniteDimensional.of_finrank_pos theorem

(h : 0 < finrank K V) : FiniteDimensional K V

Full source

theorem of_finrank_pos (h : 0 < finrank K V) : FiniteDimensional K V :=
  Module.finite_of_finrank_pos h

Finite-Dimensionality from Positive Dimension

Informal description

If the dimension $\text{finrank}_K V$ of a vector space $V$ over a division ring $K$ is positive, then $V$ is finite-dimensional.

FiniteDimensional.of_finrank_eq_succ theorem

{n : ℕ} (hn : finrank K V = n.succ) : FiniteDimensional K V

Full source

theorem of_finrank_eq_succ {n : ℕ} (hn : finrank K V = n.succ) :
    FiniteDimensional K V :=
  Module.finite_of_finrank_eq_succ hn

Finite-Dimensionality from Dimension $n+1$

Informal description

For any vector space $V$ over a division ring $K$, if the dimension of $V$ is equal to $n+1$ for some natural number $n$, then $V$ is finite-dimensional.

FiniteDimensional.of_fact_finrank_eq_succ theorem

(n : ℕ) [hn : Fact (finrank K V = n + 1)] : FiniteDimensional K V

Full source

/-- We can infer `FiniteDimensional K V` in the presence of `[Fact (finrank K V = n + 1)]`. Declare
this as a local instance where needed. -/
theorem of_fact_finrank_eq_succ (n : ℕ) [hn : Fact (finrank K V = n + 1)] :
    FiniteDimensional K V :=
  of_finrank_eq_succ hn.out

Finite-Dimensionality from Dimension $n+1$ via Fact

Informal description

For any vector space $V$ over a division ring $K$, if the dimension $\text{finrank}_K V$ is equal to $n + 1$ for some natural number $n$, then $V$ is finite-dimensional.

Module.finrank_eq_rank' theorem

[FiniteDimensional K V] : (finrank K V : Cardinal.{v}) = Module.rank K V

Full source

/-- 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 finrank_eq_rank' [FiniteDimensional K V] : (finrank K V : CardinalCardinal.{v}) = Module.rank K V :=
  finrank_eq_rank _ _

Equality of Finite Rank and Dimension in Finite-Dimensional Vector Spaces

Informal description

For a finite-dimensional vector space $V$ over a division ring $K$, the dimension of $V$ as a cardinal number equals its finite-dimensional rank, i.e., $\text{finrank}_K V = \text{rank}_K V$.

Module.finrank_of_infinite_dimensional theorem

(h : ¬FiniteDimensional K V) : finrank K V = 0

Full source

theorem finrank_of_infinite_dimensional (h : ¬FiniteDimensional K V) : finrank K V = 0 :=
  Module.finrank_of_not_finite h

Finite Rank of Infinite-Dimensional Vector Space is Zero

Informal description

For a vector space $V$ over a division ring $K$ that is not finite-dimensional, the finite rank of $V$ is defined to be $0$.

Module.finiteDimensional_iff_of_rank_eq_nsmul theorem

 {W} [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

Full source

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

Finite-Dimensionality Criterion via Rank Multiples

Informal description

Let $V$ and $W$ be vector spaces over a division ring $K$, and let $n$ be a nonzero natural number. If the rank of $V$ over $K$ is equal to $n$ times the rank of $W$ over $K$, then $V$ is finite-dimensional over $K$ if and only if $W$ is finite-dimensional over $K$.

Module.finrank_eq_card_basis' theorem

[FiniteDimensional K V] {ι : Type w} (h : Basis ι K V) : (finrank K V : Cardinal.{w}) = #ι

Full source

/-- If a vector space is finite-dimensional, then the cardinality of any basis is equal to its
`finrank`. -/
theorem finrank_eq_card_basis' [FiniteDimensional K V] {ι : Type w} (h : Basis ι K V) :
    (finrank K V : CardinalCardinal.{w}) = #ι :=
  Module.mk_finrank_eq_card_basis h

Finrank Equals Cardinality of Basis in Finite-Dimensional Vector Spaces

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$. For any basis $\{v_i\}_{i \in \iota}$ of $V$ indexed by a type $\iota$, the finrank of $V$ over $K$ is equal to the cardinality of the index set $\iota$, i.e., $\text{finrank}_K V = |\iota|$.

FiniteDimensional.finiteDimensional_self instance

: FiniteDimensional K K

Full source

instance finiteDimensional_self : FiniteDimensional K K := inferInstance

A Division Ring is Finite-Dimensional Over Itself

Informal description

For any division ring $K$, $K$ is a finite-dimensional vector space over itself.

FiniteDimensional.span_of_finite theorem

{A : Set V} (hA : Set.Finite A) : FiniteDimensional K (Submodule.span K A)

Full source

/-- The submodule generated by a finite set is finite-dimensional. -/
theorem span_of_finite {A : Set V} (hA : Set.Finite A) : FiniteDimensional K (Submodule.span K A) :=
  Module.Finite.span_of_finite K hA

Finite-Dimensionality of Span of Finite Set

Informal description

For any finite set $A$ of vectors in a vector space $V$ over a division ring $K$, the submodule $\text{span}_K(A)$ generated by $A$ is finite-dimensional.

FiniteDimensional.span_singleton instance

(x : V) : FiniteDimensional K (K ∙ x)

Full source

/-- The submodule generated by a single element is finite-dimensional. -/
instance span_singleton (x : V) : FiniteDimensional K (K ∙ x) :=
  Module.Finite.span_singleton K x

Finite-Dimensionality of the Span of a Single Vector

Informal description

For any vector $x$ in a vector space $V$ over a division ring $K$, the submodule $K \cdot x$ (the span of $\{x\}$) is finite-dimensional.

FiniteDimensional.span_finset instance

(s : Finset V) : FiniteDimensional K (span K (s : Set V))

Full source

/-- The submodule generated by a finset is finite-dimensional. -/
instance span_finset (s : Finset V) : FiniteDimensional K (span K (s : Set V)) :=
  Module.Finite.span_finset K s

Finite-Dimensionality of the Span of a Finite Set

Informal description

For any finite set $s$ of vectors in a vector space $V$ over a division ring $K$, the submodule spanned by $s$ is finite-dimensional.

FiniteDimensional.instSubtypeMemSubmoduleMapLinearMapId instance

(f : V →ₗ[K] V₂) (p : Submodule K V) [FiniteDimensional K p] : FiniteDimensional K (p.map f)

Full source

/-- Pushforwards of finite-dimensional submodules are finite-dimensional. -/
instance (f : V →ₗ[K] V₂) (p : Submodule K V) [FiniteDimensional K p] :
    FiniteDimensional K (p.map f) :=
  Module.Finite.map _ _

Finite-Dimensionality of Pushforward Submodules under Linear Maps

Informal description

For any linear map $f \colon V \to V_2$ between vector spaces over a division ring $K$ and any finite-dimensional submodule $p$ of $V$, the image of $p$ under $f$ is also finite-dimensional.

FiniteDimensional.trans theorem

[FiniteDimensional F K] [FiniteDimensional K A] : FiniteDimensional F A

Full source

theorem trans [FiniteDimensional F K] [FiniteDimensional K A] : FiniteDimensional F A :=
  Module.Finite.trans K A

Transitivity of Finite-Dimensionality for Vector Spaces

Informal description

Let $F$, $K$, and $A$ be division rings such that $K$ is a finite-dimensional vector space over $F$, and $A$ is a finite-dimensional vector space over $K$. Then $A$ is a finite-dimensional vector space over $F$.

Submodule.fg_iff_finiteDimensional theorem

(s : Submodule K V) : s.FG ↔ FiniteDimensional K s

Full source

/-- A submodule is finitely generated if and only if it is finite-dimensional -/
theorem fg_iff_finiteDimensional (s : Submodule K V) : s.FG ↔ FiniteDimensional K s :=
  (fg_top s).symm.trans Module.finite_def.symm

Finite Generation Equivalence for Submodules: $s$ is finitely generated iff $s$ is finite-dimensional

Informal description

For any submodule $s$ of a vector space $V$ over a division ring $K$, $s$ is finitely generated if and only if $s$ is finite-dimensional.

LinearEquiv.finiteDimensional theorem

(f : V ≃ₗ[K] V₂) [FiniteDimensional K V] : FiniteDimensional K V₂

Full source

/-- Finite dimensionality is preserved under linear equivalence. -/
protected theorem finiteDimensional (f : V ≃ₗ[K] V₂) [FiniteDimensional K V] :
    FiniteDimensional K V₂ :=
  Module.Finite.equiv f

Finite-dimensionality is preserved under linear isomorphism

Informal description

Let $V$ and $V_2$ be vector spaces over a division ring $K$, and let $f \colon V \simeq V_2$ be a linear isomorphism. If $V$ is finite-dimensional, then $V_2$ is also finite-dimensional.