Dimension of modules and vector spaces
Main definitions
- The dimension of a vector space is defined as
vector_space.dim : cardinal.
Main statements
mk_eq_mk_of_basis: the dimension theorem, any two bases of the same vector space have the same cardinality.dim_quotient_add_dim: if V₁ is a submodule of V, then dim (V/V₁) + dim V₁ = dim V.dim_range_add_dim_ker: the rank-nullity theorem.
Implementation notes
Many theorems in this file are not universe-generic when they relate dimensions
in different universes. They should be as general as they can be without
inserting lifts. The types V, V', ... all live in different universes,
and V₁, V₂, ... all live in the same universe.
the dimension of a vector space, defined as a term of type cardinal
Equations
- vector_space.dim K V = cardinal.min _ (λ (b : {b // is_basis K (λ (i : ↥b), ↑i)}), # ↥(b.val))
theorem
is_basis.le_span
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
{v : ι → V}
{J : set V} :
theorem
mk_eq_mk_of_basis
{K : Type u}
{V : Type v}
{ι : Type w}
{ι' : Type w'}
[field K]
[add_comm_group V]
[vector_space K V]
{v : ι → V}
{v' : ι' → V} :
dimension theorem
theorem
mk_eq_mk_of_basis'
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
{ι' : Type w}
{v : ι → V}
{v' : ι' → V} :
theorem
is_basis.mk_eq_dim''
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
{ι : Type v}
{v : ι → V} :
is_basis K v → # ι = vector_space.dim K V
theorem
is_basis.mk_range_eq_dim
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
{v : ι → V} :
theorem
is_basis.mk_eq_dim
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
{v : ι → V} :
theorem
is_basis.mk_eq_dim'
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
{v : ι → V} :
theorem
dim_le
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
{n : ℕ} :
(∀ (s : finset V), linear_independent K (λ (i : ↥↑s), ↑i) → s.card ≤ n) → vector_space.dim K V ≤ ↑n
theorem
linear_equiv.dim_eq
{K : Type u}
{V V₁ : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₁]
[vector_space K V₁] :
(V ≃ₗ[K] V₁) → vector_space.dim K V = vector_space.dim K V₁
Two linearly equivalent vector spaces have the same dimension.
@[simp]
theorem
dim_bot
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V] :
vector_space.dim K ↥⊥ = 0
@[simp]
theorem
dim_top
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V] :
vector_space.dim K ↥⊤ = vector_space.dim K V
theorem
dim_span
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
{v : ι → V} :
linear_independent K v → vector_space.dim K ↥(submodule.span K (set.range v)) = # ↥(set.range v)
theorem
dim_span_set
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
{s : set V} :
linear_independent K (λ (x : ↥s), ↑x) → vector_space.dim K ↥(submodule.span K s) = # ↥s
theorem
cardinal_lift_le_dim_of_linear_independent
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
{ι : Type w}
{v : ι → V} :
linear_independent K v → (# ι).lift ≤ (vector_space.dim K V).lift
theorem
cardinal_le_dim_of_linear_independent
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
{ι : Type v}
{v : ι → V} :
linear_independent K v → # ι ≤ vector_space.dim K V
theorem
cardinal_le_dim_of_linear_independent'
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
{s : set V} :
linear_independent K (λ (x : ↥s), ↑x) → # ↥s ≤ vector_space.dim K V
theorem
dim_span_le
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(s : set V) :
vector_space.dim K ↥(submodule.span K s) ≤ # ↥s
theorem
dim_span_of_finset
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(s : finset V) :
theorem
dim_prod
{K : Type u}
{V V₁ : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₁]
[vector_space K V₁] :
vector_space.dim K (V × V₁) = vector_space.dim K V + vector_space.dim K V₁
theorem
dim_quotient_add_dim
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(p : submodule K V) :
vector_space.dim K p.quotient + vector_space.dim K ↥p = vector_space.dim K V
theorem
dim_quotient_le
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(p : submodule K V) :
vector_space.dim K p.quotient ≤ vector_space.dim K V
theorem
dim_range_add_dim_ker
{K : Type u}
{V V₁ : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₁]
[vector_space K V₁]
(f : V →ₗ[K] V₁) :
vector_space.dim K ↥(f.range) + vector_space.dim K ↥(f.ker) = vector_space.dim K V
rank-nullity theorem
theorem
dim_range_le
{K : Type u}
{V V₁ : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₁]
[vector_space K V₁]
(f : V →ₗ[K] V₁) :
vector_space.dim K ↥(f.range) ≤ vector_space.dim K V
theorem
dim_map_le
{K : Type u}
{V V₁ : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₁]
[vector_space K V₁]
(f : V →ₗ[K] V₁)
(p : submodule K V) :
vector_space.dim K ↥(submodule.map f p) ≤ vector_space.dim K ↥p
theorem
dim_range_of_surjective
{K : Type u}
{V : Type v}
{V' : Type v'}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V']
[vector_space K V']
(f : V →ₗ[K] V') :
function.surjective ⇑f → vector_space.dim K ↥(f.range) = vector_space.dim K V'
theorem
dim_eq_of_surjective
{K : Type u}
{V V₁ : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₁]
[vector_space K V₁]
(f : V →ₗ[K] V₁) :
function.surjective ⇑f → vector_space.dim K V = vector_space.dim K V₁ + vector_space.dim K ↥(f.ker)
theorem
dim_le_of_surjective
{K : Type u}
{V V₁ : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₁]
[vector_space K V₁]
(f : V →ₗ[K] V₁) :
function.surjective ⇑f → vector_space.dim K V₁ ≤ vector_space.dim K V
theorem
dim_eq_of_injective
{K : Type u}
{V V₁ : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₁]
[vector_space K V₁]
(f : V →ₗ[K] V₁) :
function.injective ⇑f → vector_space.dim K V = vector_space.dim K ↥(f.range)
theorem
dim_submodule_le
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(s : submodule K V) :
vector_space.dim K ↥s ≤ vector_space.dim K V
theorem
dim_le_of_injective
{K : Type u}
{V V₁ : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₁]
[vector_space K V₁]
(f : V →ₗ[K] V₁) :
function.injective ⇑f → vector_space.dim K V ≤ vector_space.dim K V₁
theorem
dim_le_of_submodule
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(s t : submodule K V) :
s ≤ t → vector_space.dim K ↥s ≤ vector_space.dim K ↥t
theorem
linear_independent_le_dim
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
{v : ι → V} :
linear_independent K v → (# ι).lift ≤ (vector_space.dim K V).lift
theorem
linear_independent_le_dim'
{K : Type u}
{V : Type v}
{ι : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
{v : ι → V} :
linear_independent K v → (# ι).lift ≤ (vector_space.dim K V).lift
theorem
dim_add_dim_split
{K : Type u}
{V V₁ V₂ V₃ : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₁]
[vector_space K V₁]
[add_comm_group V₂]
[vector_space K V₂]
[add_comm_group V₃]
[vector_space K V₃]
(db : V₂ →ₗ[K] V)
(eb : V₃ →ₗ[K] V)
(cd : V₁ →ₗ[K] V₂)
(ce : V₁ →ₗ[K] V₃) :
This is mostly an auxiliary lemma for dim_sup_add_dim_inf_eq.
theorem
dim_sup_add_dim_inf_eq
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(s t : submodule K V) :
vector_space.dim K ↥(s ⊔ t) + vector_space.dim K ↥(s ⊓ t) = vector_space.dim K ↥s + vector_space.dim K ↥t
theorem
dim_add_le_dim_add_dim
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(s t : submodule K V) :
vector_space.dim K ↥(s ⊔ t) ≤ vector_space.dim K ↥s + vector_space.dim K ↥t
theorem
dim_pi
{K : Type u}
{η : Type u₁'}
{φ : η → Type u_1}
[field K]
[fintype η]
[Π (i : η), add_comm_group (φ i)]
[Π (i : η), vector_space K (φ i)] :
vector_space.dim K (Π (i : η), φ i) = cardinal.sum (λ (i : η), vector_space.dim K (φ i))
theorem
dim_fun
{K : Type u}
[field K]
{V η : Type u}
[fintype η]
[add_comm_group V]
[vector_space K V] :
vector_space.dim K (η → V) = (↑(fintype.card η)) * vector_space.dim K V
theorem
dim_fun_eq_lift_mul
{K : Type u}
{V : Type v}
{η : Type u₁'}
[field K]
[add_comm_group V]
[vector_space K V]
[fintype η] :
vector_space.dim K (η → V) = (↑(fintype.card η)) * (vector_space.dim K V).lift
theorem
dim_fun'
{K : Type u}
{η : Type u₁'}
[field K]
[fintype η] :
vector_space.dim K (η → K) = ↑(fintype.card η)
theorem
exists_mem_ne_zero_of_ne_bot
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
{s : submodule K V} :
theorem
exists_mem_ne_zero_of_dim_pos
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
{s : submodule K V} :
theorem
exists_is_basis_fintype
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V] :
vector_space.dim K V < cardinal.omega → (∃ (s : set V), is_basis K subtype.val ∧ nonempty (fintype ↥s))
def
rank
{K : Type u}
{V : Type v}
{V' : Type v'}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V']
[vector_space K V'] :
rank f is the rank of a linear_map f, defined as the dimension of f.range.
Equations
- rank f = vector_space.dim K ↥(f.range)
theorem
rank_le_domain
{K : Type u}
{V V₁ : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₁]
[vector_space K V₁]
(f : V →ₗ[K] V₁) :
rank f ≤ vector_space.dim K V
theorem
rank_le_range
{K : Type u}
{V V₁ : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V₁]
[vector_space K V₁]
(f : V →ₗ[K] V₁) :
rank f ≤ vector_space.dim K V₁
theorem
rank_add_le
{K : Type u}
{V : Type v}
{V' : Type v'}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V']
[vector_space K V']
(f g : V →ₗ[K] V') :
@[simp]
theorem
rank_zero
{K : Type u}
{V : Type v}
{V' : Type v'}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V']
[vector_space K V'] :
theorem
rank_finset_sum_le
{K : Type u}
{V : Type v}
{V' : Type v'}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V']
[vector_space K V']
{η : Type u_1}
(s : finset η)
(f : η → (V →ₗ[K] V')) :
theorem
rank_comp_le1
{K : Type u}
{V : Type v}
{V' : Type v'}
{V'' : Type v''}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V']
[vector_space K V']
[add_comm_group V'']
[vector_space K V'']
(g : V →ₗ[K] V')
(f : V' →ₗ[K] V'') :
theorem
rank_comp_le2
{K : Type u}
{V : Type v}
{V' V'₁ : Type v'}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V']
[vector_space K V']
[add_comm_group V'₁]
[vector_space K V'₁]
(g : V →ₗ[K] V')
(f : V' →ₗ[K] V'₁) :
theorem
dim_zero_iff_forall_zero
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V] :
vector_space.dim K V = 0 ↔ ∀ (x : V), x = 0
theorem
dim_pos_iff_exists_ne_zero
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V] :
0 < vector_space.dim K V ↔ ∃ (x : V), x ≠ 0
theorem
dim_pos_iff_nontrivial
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V] :
0 < vector_space.dim K V ↔ nontrivial V
theorem
dim_pos
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
[h : nontrivial V] :
0 < vector_space.dim K V
theorem
dim_le_one_iff
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V] :
vector_space.dim K V ≤ 1 ↔ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
A vector space has dimension at most 1 if and only if there is a
single vector of which all vectors are multiples.
theorem
dim_submodule_le_one_iff
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(s : submodule K V) :
vector_space.dim K ↥s ≤ 1 ↔ ∃ (v₀ : V) (H : v₀ ∈ s), s ≤ submodule.span K {v₀}
A submodule has dimension at most 1 if and only if there is a
single vector in the submodule such that the submodule is contained in
its span.
theorem
dim_submodule_le_one_iff'
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(s : submodule K V) :
vector_space.dim K ↥s ≤ 1 ↔ ∃ (v₀ : V), s ≤ submodule.span K {v₀}
A submodule has dimension at most 1 if and only if there is a
single vector, not necessarily in the submodule, such that the
submodule is contained in its span.
theorem
linear_equiv.dim_eq_lift
{K : Type u}
{V : Type v}
{E : Type v'}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group E]
[vector_space K E] :
(V ≃ₗ[K] E) → (vector_space.dim K V).lift = (vector_space.dim K E).lift
Version of linear_equiv.dim_eq without universe constraints.