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 < ⊤)
:
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]
:
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]
:
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)
:
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)
:
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)
:
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₂)
:
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)
:
Given the subspaces p q, if p.quotient ≃ₗ[K] q, then q.quotient ≃ₗ[K] p
Equations
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₂)
:
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)
:
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₂}
:
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₂}
:
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₂)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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 : ℕ)
: