Finite-dimensional vector spaces

Basic properties of finite-dimensional vector spaces, of their dimensions, and of linear maps on such spaces.

Main definitions

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

• submodules (FiniteDimensional.finiteDimensional_submodule)
• quotients (for the dimension of a quotient, see Submodule.finrank_quotient_add_finrank in Mathlib/LinearAlgebra/Dimension/RankNullity.lean)
• linear equivs, in LinearEquiv.finiteDimensional

Basic properties of linear maps of a finite-dimensional vector space are given. Notably, the equivalence of injectivity and surjectivity is proved in LinearMap.injective_iff_surjective, and the equivalence between left-inverse and right-inverse in LinearMap.mul_eq_one_comm and LinearMap.comp_eq_id_comm.

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 finitely generated modules (see Mathlib/RingTheory/Finiteness/Basic.lean) or Noetherian modules (see Mathlib/RingTheory/Noetherian/Basic.lean).

theorem LinearIndependent.lt_aleph0_of_finiteDimensional {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type w} [FiniteDimensional K V] {v : ι → V} (h : LinearIndependent K v) : Cardinal.mk ι < Cardinal.aleph0

theorem Submodule.eq_top_of_finrank_eq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {S : Submodule K V} (h : Module.finrank K ↥S = Module.finrank K V) : S = ⊤

If a submodule has maximal dimension in a finite-dimensional space, then it is equal to the whole space.

theorem FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card {L : Type u_1} [Field L] [LinearOrder L] [IsStrictOrderedRing L] {W : Type v} [AddCommGroup W] [Module L W] [FiniteDimensional L W] {t : Finset W} (h : Module.finrank L W + 1 < t.card) : ∃ (f : W → L), ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, 0 < f x

A slight strengthening of exists_nontrivial_relation_sum_zero_of_rank_succ_lt_card available when working over an ordered field: we can ensure a positive coefficient, not just a nonzero coefficient.

noncomputable def FiniteDimensional.basisSingleton {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : Module.finrank K V = 1) (v : V) (hv : v ≠ 0) : Module.Basis ι K V

In a vector space with dimension 1, each set {v} is a basis for v ≠ 0.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FiniteDimensional.basisSingleton_repr_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : Module.finrank K V = 1) (v : V) (hv : v ≠ 0) (w : V) : (basisSingleton ι h v hv).repr w = Finsupp.single default (((Module.basisUnique ι h).repr w) default / ((Module.basisUnique ι h).repr v) default)

@[simp]

theorem FiniteDimensional.basisSingleton_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : Module.finrank K V = 1) (v : V) (hv : v ≠ 0) (i : ι) : (basisSingleton ι h v hv) i = v

@[simp]

theorem FiniteDimensional.range_basisSingleton {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (ι : Type u_1) [Unique ι] (h : Module.finrank K V = 1) (v : V) (hv : v ≠ 0) : Set.range ⇑(basisSingleton ι h v hv) = {v}

theorem FiniteDimensional.of_rank_eq_nat {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (h : Module.rank K V = ↑n) : FiniteDimensional K V

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

theorem FiniteDimensional.of_rank_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : Module.rank K V = 1) : FiniteDimensional K V

instance finiteDimensional_bot (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] : FiniteDimensional K ↥⊥

theorem Submodule.finiteDimensional_of_le {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S₁ S₂ : Submodule K V} [FiniteDimensional K ↥S₂] (h : S₁ ≤ S₂) : FiniteDimensional K ↥S₁

A submodule contained in a finite-dimensional submodule is finite-dimensional.

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

The inf of two submodules, the first finite-dimensional, is finite-dimensional.

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

The inf of two submodules, the second finite-dimensional, is finite-dimensional.

instance Submodule.finiteDimensional_sup {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (S₁ S₂ : Submodule K V) [h₁ : FiniteDimensional K ↥S₁] [h₂ : FiniteDimensional K ↥S₂] : FiniteDimensional K ↥(S₁ ⊔ S₂)

The sup of two finite-dimensional submodules is finite-dimensional.

instance Submodule.finiteDimensional_finset_sup {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} (s : Finset ι) (S : ι → Submodule K V) [∀ (i : ι), FiniteDimensional K ↥(S i)] : FiniteDimensional K ↥(s.sup S)

The submodule generated by a finite supremum of finite-dimensional submodules is finite-dimensional.

Note that strictly this only needs ∀ i ∈ s, FiniteDimensional K (S i), but that doesn't work well with typeclass search.

instance Submodule.finiteDimensional_iSup {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Sort u_1} [Finite ι] (S : ι → Submodule K V) [∀ (i : ι), FiniteDimensional K ↥(S i)] : FiniteDimensional K ↥(⨆ (i : ι), S i)

The submodule generated by a supremum of finite-dimensional submodules, indexed by a finite sort is finite-dimensional.

instance finiteDimensional_finsupp {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Finite ι] [FiniteDimensional K V] : FiniteDimensional K (ι →₀ V)

theorem Submodule.eq_of_le_of_finrank_le {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S₁ S₂ : Submodule K V} [FiniteDimensional K ↥S₂] (hle : S₁ ≤ S₂) (hd : Module.finrank K ↥S₂ ≤ Module.finrank K ↥S₁) : S₁ = S₂

If a submodule is contained in a finite-dimensional submodule with the same or smaller dimension, they are equal.

theorem Submodule.eq_of_le_of_finrank_eq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S₁ S₂ : Submodule K V} [FiniteDimensional K ↥S₂] (hle : S₁ ≤ S₂) (hd : Module.finrank K ↥S₁ = Module.finrank K ↥S₂) : S₁ = S₂

If a submodule is contained in a finite-dimensional submodule with the same dimension, they are equal.

theorem Subalgebra.eq_of_le_of_finrank_le {K : Type u_1} {L : Type u_2} [Field K] [Ring L] [Algebra K L] {F E : Subalgebra K L} [hfin : FiniteDimensional K ↥E] (h_le : F ≤ E) (h_finrank : Module.finrank K ↥E ≤ Module.finrank K ↥F) : F = E

If a subalgebra is contained in a finite-dimensional subalgebra with the same or smaller dimension, they are equal.

theorem Subalgebra.eq_of_le_of_finrank_eq {K : Type u_1} {L : Type u_2} [Field K] [Ring L] [Algebra K L] {F E : Subalgebra K L} [hfin : FiniteDimensional K ↥E] (h_le : F ≤ E) (h_finrank : Module.finrank K ↥F = Module.finrank K ↥E) : F = E

If a subalgebra is contained in a finite-dimensional subalgebra with the same dimension, they are equal.

theorem LinearMap.surjective_of_injective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} (hinj : Function.Injective ⇑f) : Function.Surjective ⇑f

On a finite-dimensional space, an injective linear map is surjective.

theorem LinearMap.finiteDimensional_of_surjective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂) (hf : f.range = ⊤) : FiniteDimensional K V₂

The image under an onto linear map of a finite-dimensional space is also finite-dimensional.

instance LinearMap.finiteDimensional_range {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂) : FiniteDimensional K ↥f.range

The range of a linear map defined on a finite-dimensional space is also finite-dimensional.

theorem LinearMap.injective_iff_surjective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} : Function.Injective ⇑f ↔ Function.Surjective ⇑f

On a finite-dimensional space, a linear map is injective if and only if it is surjective.

theorem LinearMap.injOn_iff_surjOn {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {p : Submodule K V} [FiniteDimensional K ↥p] {f : V →ₗ[K] V} (h : ∀ x ∈ p, f x ∈ p) : Set.InjOn ⇑f ↑p ↔ Set.SurjOn ⇑f ↑p ↑p

theorem LinearMap.ker_eq_bot_iff_range_eq_top {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} : f.ker = ⊥ ↔ f.range = ⊤

@[instance 100]

instance LinearMap.instIsStablyFiniteRing {K : Type u} [DivisionRing K] : IsStablyFiniteRing K

Any division ring is stably finite.

instance LinearMap.instIsStablyFiniteRingEnd (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] [IsStablyFiniteRing R] : IsStablyFiniteRing (Module.End R M)

theorem Module.End.injective_of_surjective (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] [Module.Finite R M] [IsStablyFiniteRing R] {f : End R M} (hf : Function.Surjective ⇑f) : Function.Injective ⇑f

theorem LinearMap.comp_eq_id_comm (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] [IsStablyFiniteRing R] {f g : M →ₗ[R] M} : f ∘ₗ g = id ↔ g ∘ₗ f = id

In a finite-rank free module over a stably finite semiring, linear maps are inverse to each other on one side if and only if they are inverse to each other on the other side.

@[deprecated IsDedekindFiniteMonoid.mul_eq_one_symm (since := "2025-11-30")]

theorem LinearMap.mul_eq_one_of_mul_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f g : V →ₗ[K] V} (hfg : f * g = 1) : g * f = 1

In a finite-dimensional space, if linear maps are inverse to each other on one side then they are also inverse to each other on the other side.

@[deprecated mul_eq_one_comm (since := "2025-11-30")]

theorem LinearMap.mul_eq_one_comm {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f g : V →ₗ[K] V} : f * g = 1 ↔ g * f = 1

In a finite-dimensional space, linear maps are inverse to each other on one side if and only if they are inverse to each other on the other side.

theorem LinearMap.comap_eq_sup_ker_of_disjoint {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {p : Submodule K V} [FiniteDimensional K ↥p] {f : V →ₗ[K] V} (h : ∀ x ∈ p, f x ∈ p) (h' : Disjoint p f.ker) : Submodule.comap f p = p ⊔ f.ker

theorem LinearMap.ker_comp_eq_of_commute_of_disjoint_ker {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f g : V →ₗ[K] V} (h : Commute f g) (h' : Disjoint f.ker g.ker) : (f ∘ₗ g).ker = f.ker ⊔ g.ker

theorem LinearMap.ker_noncommProd_eq_of_supIndep_ker {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type u_1} {f : ι → V →ₗ[K] V} (s : Finset ι) (comm : (↑s).Pairwise (Function.onFun Commute f)) (h : s.SupIndep fun (i : ι) => (f i).ker) : (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker

noncomputable def LinearEquiv.ofInjectiveEndo {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ⇑f) : V ≃ₗ[K] V

The linear equivalence corresponding to an injective endomorphism.

Equations

• LinearEquiv.ofInjectiveEndo f h_inj = LinearEquiv.ofBijective f ⋯

@[simp]

theorem LinearEquiv.coe_ofInjectiveEndo {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ⇑f) : ⇑(ofInjectiveEndo f h_inj) = ⇑f

@[simp]

theorem LinearEquiv.ofInjectiveEndo_right_inv {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ⇑f) : f * ↑(ofInjectiveEndo f h_inj).symm = 1

@[simp]

theorem LinearEquiv.ofInjectiveEndo_left_inv {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ⇑f) : ↑(ofInjectiveEndo f h_inj).symm * f = 1

noncomputable def LinearEquiv.ofInjectiveOfFinrankEq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V' : Type u_1} [AddCommGroup V'] [Module K V'] [FiniteDimensional K V'] (f : V →ₗ[K] V') (hinj : Function.Injective ⇑f) (hrank : Module.finrank K V = Module.finrank K V') : V ≃ₗ[K] V'

An injective linear map between finite-dimensional modules of equal rank is a linear equivalence.

Unlike LinearEquiv.ofFinrankEq (which creates an abstract linear equivalence from V to V'), this lemma improves a given injective linear map to a linear equivalence.

Equations

• LinearEquiv.ofInjectiveOfFinrankEq f hinj hrank = (LinearEquiv.ofInjective f hinj).trans (LinearEquiv.ofTop f.range ⋯)

@[simp]

theorem LinearEquiv.coe_ofInjectiveOfFinrankEq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V' : Type u_1} [AddCommGroup V'] [Module K V'] [FiniteDimensional K V'] (f : V →ₗ[K] V') (hinj : Function.Injective ⇑f) (hrank : Module.finrank K V = Module.finrank K V') : ↑(ofInjectiveOfFinrankEq f hinj hrank) = f

theorem LinearMap.isUnit_iff_ker_eq_bot {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) : IsUnit f ↔ f.ker = ⊥

theorem LinearMap.isUnit_iff_range_eq_top {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) : IsUnit f ↔ f.range = ⊤

theorem finrank_zero_iff_forall_zero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : Module.finrank K V = 0 ↔ ∀ (x : V), x = 0

noncomputable def basisOfFinrankZero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type u_1} [IsEmpty ι] (hV : Module.finrank K V = 0) : Module.Basis ι K V

If ι is an empty type and V is zero-dimensional, there is a unique ι-indexed basis.

Equations

• basisOfFinrankZero hV = Module.Basis.empty V

theorem FiniteDimensional.exists_mul_eq_one (F : Type u_1) {K : Type u_2} [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] {x : K} (H : x ≠ 0) : ∃ (y : K), x * y = 1

noncomputable def divisionRingOfFiniteDimensional (F : Type u_1) (K : Type u_2) [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] : DivisionRing K

A domain that is module-finite as an algebra over a field is a division ring.

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteDimensional.isUnit (F : Type u_1) {K : Type u_2} [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] {x : K} (H : x ≠ 0) : IsUnit x

noncomputable def fieldOfFiniteDimensional (F : Type u_1) (K : Type u_2) [Field F] [h : CommRing K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] : Field K

An integral domain that is module-finite as an algebra over a field is a field.

Equations

• One or more equations did not get rendered due to their size.

theorem finrank_span_singleton {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {v : V} (hv : v ≠ 0) : Module.finrank K ↥(K ∙ v) = 1

theorem exists_smul_eq_of_finrank_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : Module.finrank K V = 1) {x : V} (hx : x ≠ 0) (y : V) : ∃ (c : K), c • x = y

In a one-dimensional space, any vector is a multiple of any nonzero vector

theorem Set.finrank_mono {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s t : Set V} (h : s ⊆ t) : Set.finrank K s ≤ Set.finrank K t

We now give characterisations of finrank K V = 1 and finrank K V ≤ 1.

theorem finrank_eq_one_iff_of_nonzero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (nz : v ≠ 0) : Module.finrank K V = 1 ↔ K ∙ v = ⊤

A vector space with a nonzero vector v has dimension 1 iff v spans.

theorem finrank_eq_one_iff_of_nonzero' {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (nz : v ≠ 0) : Module.finrank K V = 1 ↔ ∀ (w : V), ∃ (c : K), c • v = w

A module with a nonzero vector v has dimension 1 iff every vector is a multiple of v.

theorem surjective_of_nonzero_of_finrank_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {W : Type u_1} {A : Type u_2} [Semiring A] [Module A V] [AddCommGroup W] [Module K W] [Module A W] [LinearMap.CompatibleSMul V W K A] (h : Module.finrank K W = 1) {f : V →ₗ[A] W} (w : f ≠ 0) : Function.Surjective ⇑f

theorem Subalgebra.finiteDimensional_toSubmodule {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} : FiniteDimensional F ↥(toSubmodule S) ↔ FiniteDimensional F ↥S

A Subalgebra is FiniteDimensional iff it is FiniteDimensional as a submodule.

theorem FiniteDimensional.of_subalgebra_toSubmodule {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} : FiniteDimensional F ↥(Subalgebra.toSubmodule S) → FiniteDimensional F ↥S

Alias of the forward direction of Subalgebra.finiteDimensional_toSubmodule.

---

A Subalgebra is FiniteDimensional iff it is FiniteDimensional as a submodule.

theorem FiniteDimensional.subalgebra_toSubmodule {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} : FiniteDimensional F ↥S → FiniteDimensional F ↥(Subalgebra.toSubmodule S)

Alias of the reverse direction of Subalgebra.finiteDimensional_toSubmodule.

---

A Subalgebra is FiniteDimensional iff it is FiniteDimensional as a submodule.

instance FiniteDimensional.finiteDimensional_subalgebra {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] [FiniteDimensional F E] (S : Subalgebra F E) : FiniteDimensional F ↥S

theorem Module.End.ker_pow_constant {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {f : End K V} {k : ℕ} (h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)) (m : ℕ) : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + m))