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 and results that require fewer imports are in Mathlib.LinearAlgebra.FiniteDimensional.Basic.

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.

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.

Equations

• FiniteDimensional.LinearEquiv.quotEquivOfEquiv f₁ f₂ = LinearEquiv.ofFinrankEq (V ⧸ p) (V₂ ⧸ q) ⋯

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

Equations

• FiniteDimensional.LinearEquiv.quotEquivOfQuotEquiv f = LinearEquiv.ofFinrankEq (V ⧸ q) ↥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.

Equations

• f.linearEquivOfInjective hf hdim = LinearEquiv.ofBijective f ⋯

@[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) : Basis ι K V

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

Equations

• basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq = Basis.mk lin_ind ⋯

@[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) : Basis ι K (ι → K)

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

Equations

• basisOfPiSpaceOfLinearIndependent hb = if hι : Nonempty ι then basisOfLinearIndependentOfCardEqFinrank hb ⋯ else let_fun this := ⋯; Basis.empty (ι → K)

@[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) : Basis { x : V // x ∈ s } K V

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

Equations

• finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq = basisOfLinearIndependentOfCardEqFinrank lin_ind ⋯

@[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) : Basis (↑s) K V

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

Equations

• setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq = basisOfLinearIndependentOfCardEqFinrank lin_ind ⋯

@[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)