Finite dimensional vector spaces

This file contains some further development of finite dimensional vector spaces, their dimensions, and linear maps on such spaces.

Definitions are in Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean and results that require fewer imports are in Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean.

theorem Submodule.finrank_lt {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s : Submodule K V} (h : s ≠ ⊤) : Module.finrank K ↥s < Module.finrank K V

The dimension of a strict submodule is strictly bounded by the dimension of the ambient space.

See also Submodule.length_lt.

theorem Submodule.finrank_sup_add_finrank_inf_eq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s t : Submodule K V) [FiniteDimensional K ↥s] [FiniteDimensional K ↥t] : Module.finrank K ↥(s ⊔ t) + Module.finrank K ↥(s ⊓ t) = Module.finrank K ↥s + Module.finrank K ↥t

The sum of the dimensions of s + t and s ∩ t is the sum of the dimensions of s and t

theorem Submodule.finrank_add_le_finrank_add_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s t : Submodule K V) [FiniteDimensional K ↥s] [FiniteDimensional K ↥t] : Module.finrank K ↥(s ⊔ t) ≤ Module.finrank K ↥s + Module.finrank K ↥t

theorem Submodule.finrank_add_finrank_le_of_disjoint {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s t : Submodule K V} (hdisjoint : Disjoint s t) : Module.finrank K ↥s + Module.finrank K ↥t ≤ Module.finrank K V

theorem Submodule.eq_top_of_disjoint {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (s t : Submodule K V) (hdim : Module.finrank K V ≤ Module.finrank K ↥s + Module.finrank K ↥t) (hdisjoint : Disjoint s t) : s ⊔ t = ⊤

theorem Submodule.isCompl_iff_disjoint {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (s t : Submodule K V) (hdim : Module.finrank K V ≤ Module.finrank K ↥s + Module.finrank K ↥t) : IsCompl s t ↔ Disjoint s t

noncomputable def FiniteDimensional.LinearEquiv.quotEquivOfEquiv {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] {p : Subspace K V} {q : Subspace K V₂} (f₁ : ↥p ≃ₗ[K] ↥q) (f₂ : V ≃ₗ[K] V₂) : (V ⧸ p) ≃ₗ[K] V₂ ⧸ q

Given isomorphic subspaces p q of vector spaces V and V₁ respectively, p.quotient is isomorphic to q.quotient.

noncomputable def FiniteDimensional.LinearEquiv.quotEquivOfQuotEquiv {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {p q : Subspace K V} (f : (V ⧸ p) ≃ₗ[K] ↥q) : (V ⧸ q) ≃ₗ[K] ↥p

Given the subspaces p q, if p.quotient ≃ₗ[K] q, then q.quotient ≃ₗ[K] p

theorem LinearMap.finrank_range_add_finrank_ker {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₂) : Module.finrank K ↥(range f) + Module.finrank K ↥(ker f) = Module.finrank K V

rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to the dimension of the source space.

theorem LinearMap.ker_ne_bot_of_finrank_lt {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂} (h : Module.finrank K V₂ < Module.finrank K V) : ker f ≠ ⊥

theorem LinearMap.injective_iff_surjective_of_finrank_eq_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] (H : Module.finrank K V = Module.finrank K V₂) {f : V →ₗ[K] V₂} : Function.Injective ⇑f ↔ Function.Surjective ⇑f

theorem LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] (H : Module.finrank K V = Module.finrank K V₂) {f : V →ₗ[K] V₂} : ker f = ⊥ ↔ range f = ⊤

noncomputable def LinearMap.linearEquivOfInjective {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] (f : V →ₗ[K] V₂) (hf : Function.Injective ⇑f) (hdim : Module.finrank K V = Module.finrank K V₂) : V ≃ₗ[K] V₂

Given a linear map f between two vector spaces with the same dimension, if ker f = ⊥ then linearEquivOfInjective is the induced isomorphism between the two vector spaces.

@[simp]

theorem LinearMap.linearEquivOfInjective_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂} (hf : Function.Injective ⇑f) (hdim : Module.finrank K V = Module.finrank K V₂) (x : V) : (f.linearEquivOfInjective hf hdim) x = f x

theorem Submodule.finrank_lt_finrank_of_lt {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Submodule K V} [FiniteDimensional K ↥t] (hst : s < t) : Module.finrank K ↥s < Module.finrank K ↥t

theorem Submodule.finrank_strictMono {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : StrictMono fun (s : Submodule K V) => Module.finrank K ↥s

theorem Submodule.finrank_add_eq_of_isCompl {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {U W : Submodule K V} (h : IsCompl U W) : Module.finrank K ↥U + Module.finrank K ↥W = Module.finrank K V

theorem LinearIndependent.span_eq_top_of_card_eq_finrank' {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Fintype ι] [FiniteDimensional K V] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) : Submodule.span K (Set.range b) = ⊤

theorem LinearIndependent.span_eq_top_of_card_eq_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) : Submodule.span K (Set.range b) = ⊤

noncomputable def basisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) : Module.Basis ι K V

A linear independent family of finrank K V vectors forms a basis.

@[simp]

theorem basisOfLinearIndependentOfCardEqFinrank_repr_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) (a✝ : V) : (basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr a✝ = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range b)) LinearMap.id ⋯) a✝)

@[simp]

theorem coe_basisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) : ⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = b

noncomputable def basisOfPiSpaceOfLinearIndependent {K : Type u} [DivisionRing K] {ι : Type u_1} [Fintype ι] [Decidable (Nonempty ι)] {b : ι → ι → K} (hb : LinearIndependent K b) : Module.Basis ι K (ι → K)

In a vector space ι → K, a linear independent family indexed by ι is a basis.

@[simp]

theorem coe_basisOfPiSpaceOfLinearIndependent {K : Type u} [DivisionRing K] {ι : Type u_1} [Fintype ι] {b : ι → ι → K} (hb : LinearIndependent K b) : ⇑(basisOfPiSpaceOfLinearIndependent hb) = b

noncomputable def finsetBasisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (hs : s.Nonempty) (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.card = Module.finrank K V) : Module.Basis { x : V // x ∈ s } K V

A linear independent finset of finrank K V vectors forms a basis.

@[simp]

theorem finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (hs : s.Nonempty) (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.card = Module.finrank K V) (a✝ : V) : (finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq).repr a✝ = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a✝)

@[simp]

theorem coe_finsetBasisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (hs : s.Nonempty) (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.card = Module.finrank K V) : ⇑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) = Subtype.val

noncomputable def setBasisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Nonempty ↑s] [Fintype ↑s] (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.toFinset.card = Module.finrank K V) : Module.Basis (↑s) K V

A linear independent set of finrank K V vectors forms a basis.

@[simp]

theorem setBasisOfLinearIndependentOfCardEqFinrank_repr_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Nonempty ↑s] [Fintype ↑s] (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.toFinset.card = Module.finrank K V) (a✝ : V) : (setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr a✝ = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a✝)

@[simp]

theorem coe_setBasisOfLinearIndependentOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Nonempty ↑s] [Fintype ↑s] (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.toFinset.card = Module.finrank K V) : ⇑(setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = Subtype.val

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

theorem is_simple_module_of_finrank_eq_one {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {A : Type u_1} [Semiring A] [Module A V] [SMul K A] [IsScalarTower K A V] (h : Module.finrank K V = 1) : IsSimpleOrder (Submodule A V)

Any K-algebra module that is 1-dimensional over K is simple.

theorem Subalgebra.isSimpleOrder_of_finrank {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] (hr : Module.finrank F E = 2) : IsSimpleOrder (Subalgebra F E)

theorem Module.End.exists_ker_pow_eq_ker_pow_succ {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) : ∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)

theorem Module.End.ker_pow_eq_ker_pow_finrank_of_le {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : End K V} {m : ℕ} (hm : finrank K V ≤ m) : LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)

theorem Module.End.ker_pow_le_ker_pow_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) (m : ℕ) : LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)