Finite dimension of vector spaces #
Definition of the rank of a module, or dimension of a vector space, as a natural number.
Main definitions #
Defined is FiniteDimensional.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.
The definition of finrank does not assume a FiniteDimensional instance, but lemmas might.
Import LinearAlgebra.FiniteDimensional to get access to these additional lemmas.
Formulas for the dimension are given for linear equivs, in LinearEquiv.finrank_eq.
Implementation notes #
Most results are deduced from the corresponding results for the general dimension (as a cardinal),
in Dimension.lean. Not all results have been ported yet.
You should not assume that there has been any effort to state lemmas as generally as possible.
noncomputable def
FiniteDimensional.finrank
(R : Type u_1)
(V : Type u_2)
[Semiring R]
[AddCommGroup V]
[Module R V]
:
The rank of a module as a natural number.
Defined by convention to be 0 if the space has infinite rank.
For a vector space V over a field K, this is the same as the finite dimension
of V over K.
Equations
- FiniteDimensional.finrank R V = ↑Cardinal.toNat (Module.rank R V)
Instances For
theorem
FiniteDimensional.finrank_eq_of_rank_eq
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
{n : ℕ}
(h : Module.rank K V = ↑n)
:
FiniteDimensional.finrank K V = n
theorem
FiniteDimensional.rank_eq_one_iff_finrank_eq_one
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
:
Module.rank K V = 1 ↔ FiniteDimensional.finrank K V = 1
theorem
FiniteDimensional.rank_eq_ofNat_iff_finrank_eq_ofNat
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
(n : ℕ)
[Nat.AtLeastTwo n]
:
Module.rank K V = OfNat.ofNat n ↔ FiniteDimensional.finrank K V = OfNat.ofNat n
This is like rank_eq_one_iff_finrank_eq_one but works for 2, 3, 4, ...
theorem
FiniteDimensional.finrank_le_of_rank_le
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
{n : ℕ}
(h : Module.rank K V ≤ ↑n)
:
FiniteDimensional.finrank K V ≤ n
theorem
FiniteDimensional.finrank_lt_of_rank_lt
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
{n : ℕ}
(h : Module.rank K V < ↑n)
:
FiniteDimensional.finrank K V < n
theorem
FiniteDimensional.lt_rank_of_lt_finrank
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
{n : ℕ}
(h : n < FiniteDimensional.finrank K V)
:
↑n < Module.rank K V
theorem
FiniteDimensional.one_lt_rank_of_one_lt_finrank
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
(h : 1 < FiniteDimensional.finrank K V)
:
1 < Module.rank K V
theorem
FiniteDimensional.finrank_le_finrank_of_rank_le_rank
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
{V₂ : Type v'}
[AddCommGroup V₂]
[Module K V₂]
(h : Cardinal.lift.{v', v} (Module.rank K V) ≤ Cardinal.lift.{v, v'} (Module.rank K V₂))
(h' : Module.rank K V₂ < Cardinal.aleph0)
:
theorem
FiniteDimensional.nontrivial_of_finrank_pos
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
[Nontrivial K]
[NoZeroSMulDivisors K V]
(h : 0 < FiniteDimensional.finrank K V)
:
A finite dimensional space is nontrivial if it has positive finrank.
theorem
FiniteDimensional.nontrivial_of_finrank_eq_succ
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
[Nontrivial K]
[NoZeroSMulDivisors K V]
{n : ℕ}
(hn : FiniteDimensional.finrank K V = Nat.succ n)
:
A finite dimensional space is nontrivial if it has finrank equal to the successor of a
natural number.
theorem
FiniteDimensional.finrank_zero_of_subsingleton
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
[Nontrivial K]
[NoZeroSMulDivisors K V]
[h : Subsingleton V]
:
FiniteDimensional.finrank K V = 0
A (finite dimensional) space that is a subsingleton has zero finrank.
theorem
FiniteDimensional.finrank_eq_card_basis
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
[StrongRankCondition K]
{ι : Type w}
[Fintype ι]
(h : Basis ι K V)
:
If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the cardinality of the basis.
theorem
FiniteDimensional.finrank_eq_card_finset_basis
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
[StrongRankCondition K]
{ι : Type w}
{b : Finset ι}
(h : Basis { x // x ∈ b } K V)
:
If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the
cardinality of the basis. This lemma uses a Finset instead of indexed types.
@[simp]
theorem
FiniteDimensional.finrank_self
(K : Type u)
[Ring K]
[StrongRankCondition K]
:
FiniteDimensional.finrank K K = 1
A ring satisfying StrongRankCondition (such as a DivisionRing) is one-dimensional as a
module over itself.
@[simp]
theorem
FiniteDimensional.finrank_fintype_fun_eq_card
(K : Type u)
[Ring K]
[StrongRankCondition K]
{ι : Type v}
[Fintype ι]
:
FiniteDimensional.finrank K (ι → K) = Fintype.card ι
The vector space of functions on a Fintype ι has finrank equal to the cardinality of ι.
theorem
FiniteDimensional.finrank_fin_fun
(K : Type u)
[Ring K]
[StrongRankCondition K]
{n : ℕ}
:
FiniteDimensional.finrank K (Fin n → K) = n
The vector space of functions on Fin n has finrank equal to n.
theorem
FiniteDimensional.Basis.subset_extend
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
(hs : LinearIndependent K Subtype.val)
:
s ⊆ LinearIndependent.extend hs (_ : s ⊆ Set.univ)
theorem
finrank_eq_zero_of_basis_imp_not_finite
{K : Type u}
{V : Type v}
[Ring K]
[StrongRankCondition K]
[AddCommGroup V]
[Module K V]
[Module.Free K V]
(h : ∀ (s : Set V), Basis (↑s) K V → ¬Set.Finite s)
:
FiniteDimensional.finrank K V = 0
theorem
finrank_eq_zero_of_basis_imp_false
{K : Type u}
{V : Type v}
[Ring K]
[StrongRankCondition K]
[AddCommGroup V]
[Module K V]
[Module.Free K V]
(h : ∀ (s : Finset V), Basis (↑↑s) K V → False)
:
FiniteDimensional.finrank K V = 0
theorem
finrank_eq_zero_of_not_exists_basis
{K : Type u}
{V : Type v}
[Ring K]
[StrongRankCondition K]
[AddCommGroup V]
[Module K V]
[Module.Free K V]
(h : ¬∃ s, Nonempty (Basis (↑↑s) K V))
:
FiniteDimensional.finrank K V = 0
theorem
finrank_eq_zero_of_not_exists_basis_finite
{K : Type u}
{V : Type v}
[Ring K]
[StrongRankCondition K]
[AddCommGroup V]
[Module K V]
[Module.Free K V]
(h : ¬∃ s x, Set.Finite s)
:
FiniteDimensional.finrank K V = 0
theorem
finrank_eq_zero_of_not_exists_basis_finset
{K : Type u}
{V : Type v}
[Ring K]
[StrongRankCondition K]
[AddCommGroup V]
[Module K V]
[Module.Free K V]
(h : ¬∃ s, Nonempty (Basis { x // x ∈ s } K V))
:
FiniteDimensional.finrank K V = 0
theorem
LinearEquiv.finrank_eq
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[Ring R]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R M₂]
(f : M ≃ₗ[R] M₂)
:
The dimension of a finite dimensional space is preserved under linear equivalence.
theorem
LinearEquiv.finrank_map_eq
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[Ring R]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R M₂]
(f : M ≃ₗ[R] M₂)
(p : Submodule R M)
:
FiniteDimensional.finrank R { x // x ∈ Submodule.map (↑f) p } = FiniteDimensional.finrank R { x // x ∈ p }
Pushforwards of finite-dimensional submodules along a LinearEquiv have the same finrank.
theorem
LinearMap.finrank_range_of_inj
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
{V₂ : Type v'}
[AddCommGroup V₂]
[Module K V₂]
{f : V →ₗ[K] V₂}
(hf : Function.Injective ↑f)
:
FiniteDimensional.finrank K { x // x ∈ LinearMap.range f } = FiniteDimensional.finrank K V
The dimensions of the domain and range of an injective linear map are equal.
@[simp]
theorem
finrank_bot
(K : Type u)
(V : Type v)
[Ring K]
[AddCommGroup V]
[Module K V]
[Nontrivial K]
:
FiniteDimensional.finrank K { x // x ∈ ⊥ } = 0
@[simp]
theorem
finrank_top
(K : Type u)
(V : Type v)
[Ring K]
[AddCommGroup V]
[Module K V]
:
FiniteDimensional.finrank K { x // x ∈ ⊤ } = FiniteDimensional.finrank K V
theorem
Submodule.lt_of_le_of_finrank_lt_finrank
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
{s : Submodule K V}
{t : Submodule K V}
(le : s ≤ t)
(lt : FiniteDimensional.finrank K { x // x ∈ s } < FiniteDimensional.finrank K { x // x ∈ t })
:
s < t
theorem
Submodule.lt_top_of_finrank_lt_finrank
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
{s : Submodule K V}
(lt : FiniteDimensional.finrank K { x // x ∈ s } < FiniteDimensional.finrank K V)
:
noncomputable def
Set.finrank
(K : Type u)
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(s : Set V)
:
The rank of a set of vectors as a natural number.
Equations
- Set.finrank K s = FiniteDimensional.finrank K { x // x ∈ Submodule.span K s }
Instances For
theorem
finrank_span_le_card
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(s : Set V)
[Fintype ↑s]
:
FiniteDimensional.finrank K { x // x ∈ Submodule.span K s } ≤ Finset.card (Set.toFinset s)
theorem
finrank_span_finset_le_card
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(s : Finset V)
:
Set.finrank K ↑s ≤ Finset.card s
theorem
finrank_range_le_card
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{ι : Type u_1}
[Fintype ι]
{b : ι → V}
:
Set.finrank K (Set.range b) ≤ Fintype.card ι
theorem
finrank_span_eq_card
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{ι : Type u_1}
[Fintype ι]
{b : ι → V}
(hb : LinearIndependent K b)
:
FiniteDimensional.finrank K { x // x ∈ Submodule.span K (Set.range b) } = Fintype.card ι
theorem
finrank_span_set_eq_card
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(s : Set V)
[Fintype ↑s]
(hs : LinearIndependent K Subtype.val)
:
FiniteDimensional.finrank K { x // x ∈ Submodule.span K s } = Finset.card (Set.toFinset s)
theorem
finrank_span_finset_eq_card
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(s : Finset V)
(hs : LinearIndependent K Subtype.val)
:
FiniteDimensional.finrank K { x // x ∈ Submodule.span K ↑s } = Finset.card s
theorem
span_lt_of_subset_of_card_lt_finrank
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
[Fintype ↑s]
{t : Submodule K V}
(subset : s ⊆ ↑t)
(card_lt : Finset.card (Set.toFinset s) < FiniteDimensional.finrank K { x // x ∈ t })
:
Submodule.span K s < t
theorem
span_lt_top_of_card_lt_finrank
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
[Fintype ↑s]
(card_lt : Finset.card (Set.toFinset s) < FiniteDimensional.finrank K V)
:
Submodule.span K s < ⊤
theorem
exists_linearIndependent_snoc_of_lt_finrank
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{n : ℕ}
{v : Fin n → V}
(hv : LinearIndependent K v)
(h : n < FiniteDimensional.finrank K V)
:
∃ x, LinearIndependent K (Fin.snoc v x)
Given a family of n linearly independent vectors in a finite-dimensional space of
dimension > n, one may extend the family by another vector while retaining linear independence.
theorem
exists_linearIndependent_cons_of_lt_finrank
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{n : ℕ}
{v : Fin n → V}
(hv : LinearIndependent K v)
(h : n < FiniteDimensional.finrank K V)
:
∃ x, LinearIndependent K (Fin.cons x v)
Given a family of n linearly independent vectors in a finite-dimensional space of
dimension > n, one may extend the family by another vector while retaining linear independence.
theorem
exists_linearIndependent_pair_of_one_lt_finrank
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(h : 1 < FiniteDimensional.finrank K V)
{x : V}
(hx : x ≠ 0)
:
∃ y, LinearIndependent K ![x, y]
Given a nonzero vector in a finite-dimensional space of dimension > 1, one may find another
vector linearly independent of the first one.
theorem
linearIndependent_of_top_le_span_of_card_eq_finrank
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{ι : Type u_1}
[Fintype ι]
{b : ι → V}
(spans : ⊤ ≤ Submodule.span K (Set.range b))
(card_eq : Fintype.card ι = FiniteDimensional.finrank K V)
:
theorem
linearIndependent_iff_card_eq_finrank_span
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{ι : Type u_1}
[Fintype ι]
{b : ι → V}
:
LinearIndependent K b ↔ Fintype.card ι = Set.finrank K (Set.range b)
A finite family of vectors is linearly independent if and only if its cardinality equals the dimension of its span.
theorem
linearIndependent_iff_card_le_finrank_span
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{ι : Type u_1}
[Fintype ι]
{b : ι → V}
:
LinearIndependent K b ↔ Fintype.card ι ≤ Set.finrank K (Set.range b)
noncomputable def
basisOfTopLeSpanOfCardEqFinrank
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{ι : Type u_1}
[Fintype ι]
(b : ι → V)
(le_span : ⊤ ≤ Submodule.span K (Set.range b))
(card_eq : Fintype.card ι = FiniteDimensional.finrank K V)
:
Basis ι K V
A family of finrank K V vectors forms a basis if they span the whole space.
Equations
- basisOfTopLeSpanOfCardEqFinrank b le_span card_eq = Basis.mk (_ : LinearIndependent K b) le_span
Instances For
@[simp]
theorem
coe_basisOfTopLeSpanOfCardEqFinrank
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{ι : Type u_1}
[Fintype ι]
(b : ι → V)
(le_span : ⊤ ≤ Submodule.span K (Set.range b))
(card_eq : Fintype.card ι = FiniteDimensional.finrank K V)
:
↑(basisOfTopLeSpanOfCardEqFinrank b le_span card_eq) = b
@[simp]
theorem
finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Finset V}
(le_span : ⊤ ≤ Submodule.span K ↑s)
(card_eq : Finset.card s = FiniteDimensional.finrank K V)
:
∀ (a : V),
↑(finsetBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a = ↑(LinearIndependent.repr (_ : LinearIndependent K Subtype.val))
(↑(LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id
(_ : ∀ (x : V), ↑LinearMap.id x ∈ Submodule.span K (Set.range Subtype.val)))
a)
noncomputable def
finsetBasisOfTopLeSpanOfCardEqFinrank
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Finset V}
(le_span : ⊤ ≤ Submodule.span K ↑s)
(card_eq : Finset.card s = FiniteDimensional.finrank K V)
:
Basis (↑↑s) K V
A finset of finrank K V vectors forms a basis if they span the whole space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
setBasisOfTopLeSpanOfCardEqFinrank_repr_apply
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
[Fintype ↑s]
(le_span : ⊤ ≤ Submodule.span K s)
(card_eq : Finset.card (Set.toFinset s) = FiniteDimensional.finrank K V)
:
∀ (a : V),
↑(setBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a = ↑(LinearIndependent.repr (_ : LinearIndependent K Subtype.val))
(↑(LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id
(_ : ∀ (x : V), ↑LinearMap.id x ∈ Submodule.span K (Set.range Subtype.val)))
a)
noncomputable def
setBasisOfTopLeSpanOfCardEqFinrank
{K : Type u}
{V : Type v}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
[Fintype ↑s]
(le_span : ⊤ ≤ Submodule.span K s)
(card_eq : Finset.card (Set.toFinset s) = FiniteDimensional.finrank K V)
:
Basis (↑s) K V
A set of finrank K V vectors forms a basis if they span the whole space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
finrank_eq_one
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
[NoZeroSMulDivisors K V]
[StrongRankCondition K]
(v : V)
(n : v ≠ 0)
(h : ∀ (w : V), ∃ c, c • v = w)
:
FiniteDimensional.finrank K V = 1
If there is a nonzero vector and every other vector is a multiple of it, then the module has dimension one.
theorem
finrank_le_one
{K : Type u}
{V : Type v}
[Ring K]
[AddCommGroup V]
[Module K V]
[NoZeroSMulDivisors K V]
[StrongRankCondition K]
(v : V)
(h : ∀ (w : V), ∃ c, c • v = w)
:
FiniteDimensional.finrank K V ≤ 1
If every vector is a multiple of some v : V, then V has dimension at most one.
@[simp]
theorem
Subalgebra.rank_toSubmodule
{F : Type u_1}
{E : Type u_2}
[CommRing F]
[Ring E]
[Algebra F E]
(S : Subalgebra F E)
:
Module.rank F { x // x ∈ ↑Subalgebra.toSubmodule S } = Module.rank F { x // x ∈ S }
@[simp]
theorem
Subalgebra.finrank_toSubmodule
{F : Type u_1}
{E : Type u_2}
[CommRing F]
[Ring E]
[Algebra F E]
(S : Subalgebra F E)
:
FiniteDimensional.finrank F { x // x ∈ ↑Subalgebra.toSubmodule S } = FiniteDimensional.finrank F { x // x ∈ S }
theorem
subalgebra_top_rank_eq_submodule_top_rank
{F : Type u_1}
{E : Type u_2}
[CommRing F]
[Ring E]
[Algebra F E]
:
Module.rank F { x // x ∈ ⊤ } = Module.rank F { x // x ∈ ⊤ }
theorem
subalgebra_top_finrank_eq_submodule_top_finrank
{F : Type u_1}
{E : Type u_2}
[CommRing F]
[Ring E]
[Algebra F E]
:
FiniteDimensional.finrank F { x // x ∈ ⊤ } = FiniteDimensional.finrank F { x // x ∈ ⊤ }
theorem
Subalgebra.rank_top
{F : Type u_1}
{E : Type u_2}
[CommRing F]
[Ring E]
[Algebra F E]
:
Module.rank F { x // x ∈ ⊤ } = Module.rank F E
@[simp]
theorem
Subalgebra.rank_bot
{F : Type u_1}
{E : Type u_2}
[CommRing F]
[Ring E]
[Algebra F E]
[StrongRankCondition F]
[NoZeroSMulDivisors F E]
[Nontrivial E]
:
Module.rank F { x // x ∈ ⊥ } = 1
@[simp]
theorem
Subalgebra.finrank_bot
{F : Type u_1}
{E : Type u_2}
[CommRing F]
[Ring E]
[Algebra F E]
[StrongRankCondition F]
[NoZeroSMulDivisors F E]
[Nontrivial E]
:
FiniteDimensional.finrank F { x // x ∈ ⊥ } = 1