linear_algebra.dimension

def vector_space.dim (K : Type u) (V : Type v) [field K] [add_comm_group V] [vector_space K V] :

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} (hv : is_basis K v) (hJ : submodule.span K J = ⊤) :

# ↥(set.range v) ≤ # ↥J

source

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} (hv : is_basis K v) (hv' : is_basis K v') :

(# ι).lift = (# ι').lift

dimension theorem

source

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} (hv : is_basis K v) (hv' : is_basis K v') :

# ι = # ι'

source

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} (h : is_basis K v) :

# ι = vector_space.dim K V

source

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} (h : is_basis K v) :

# ↥(set.range v) = vector_space.dim K V

source

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} (h : is_basis K v) :

(# ι).lift = (vector_space.dim K V).lift

source

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} (h : is_basis K v) :

(# ι).lift = (vector_space.dim K V).lift

source

theorem dim_le {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {n : ℕ} (H : ∀ (s : finset V), linear_independent K (λ (i : ↥↑s), ↑i) → s.card ≤ n) :

vector_space.dim K V ≤ ↑n

source

theorem linear_equiv.lift_dim_eq {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') :

(vector_space.dim K V).lift = (vector_space.dim K V').lift

Two linearly equivalent vector spaces have the same dimension, a version with different universes.

source

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₁] (f : V ≃ₗ[K] V₁) :

vector_space.dim K V = vector_space.dim K V₁

Two linearly equivalent vector spaces have the same dimension.

source

theorem nonempty_linear_equiv_of_lift_dim_eq {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'] (cond : (vector_space.dim K V).lift = (vector_space.dim K V').lift) :

nonempty (V ≃ₗ[K] V')

Two vector spaces are isomorphic if they have the same dimension.

source

theorem nonempty_linear_equiv_of_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₁] (cond : vector_space.dim K V = vector_space.dim K V₁) :

nonempty (V ≃ₗ[K] V₁)

Two vector spaces are isomorphic if they have the same dimension.

source

def linear_equiv.of_lift_dim_eq {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'] (cond : (vector_space.dim K V).lift = (vector_space.dim K V').lift) :

V ≃ₗ[K] V'

Two vector spaces are isomorphic if they have the same dimension.

Equations

linear_equiv.of_lift_dim_eq V V' cond = classical.choice _

source

def linear_equiv.of_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₁] (cond : vector_space.dim K V = vector_space.dim K V₁) :

V ≃ₗ[K] V₁

Two vector spaces are isomorphic if they have the same dimension.

Equations

linear_equiv.of_dim_eq V V₁ cond = classical.choice _

source

theorem linear_equiv.nonempty_equiv_iff_lift_dim_eq {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'] :

nonempty (V ≃ₗ[K] V') ↔ (vector_space.dim K V).lift = (vector_space.dim K V').lift

Two vector spaces are isomorphic if and only if they have the same dimension.

source

theorem linear_equiv.nonempty_equiv_iff_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₁] :

nonempty (V ≃ₗ[K] V₁) ↔ vector_space.dim K V = vector_space.dim K V₁

Two vector spaces are isomorphic if and only if they have the same dimension.

source

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

source

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

source

theorem dim_of_field (K : Type u_1) [field K] :

vector_space.dim K K = 1

source

theorem dim_span {K : Type u} {V : Type v} {ι : Type w} [field K] [add_comm_group V] [vector_space K V] {v : ι → V} (hv : linear_independent K v) :

vector_space.dim K ↥(submodule.span K (set.range v)) = # ↥(set.range v)

source

theorem dim_span_set {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {s : set V} (hs : linear_independent K (λ (x : ↥s), ↑x)) :

vector_space.dim K ↥(submodule.span K s) = # ↥s

source

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} (hv : linear_independent K v) :

(# ι).lift ≤ (vector_space.dim K V).lift

source

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} (hv : linear_independent K v) :

# ι ≤ vector_space.dim K V

source

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} (hs : linear_independent K (λ (x : ↥s), ↑x)) :

# ↥s ≤ vector_space.dim K V

source

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

source

theorem dim_span_of_finset {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (s : finset V) :

vector_space.dim K ↥(submodule.span K ↑s) < cardinal.omega

source

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₁

source

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

source

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

source

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

source

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

source

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

source

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') (h : function.surjective ⇑f) :

vector_space.dim K ↥(f.range) = vector_space.dim K V'

source

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₁) (h : function.surjective ⇑f) :

vector_space.dim K V = vector_space.dim K V₁ + vector_space.dim K ↥(f.ker)

source

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₁) (h : function.surjective ⇑f) :

vector_space.dim K V₁ ≤ vector_space.dim K V

source

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₁) (h : function.injective ⇑f) :

vector_space.dim K V = vector_space.dim K ↥(f.range)

source

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

source

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₁) (h : function.injective ⇑f) :

vector_space.dim K V ≤ vector_space.dim K V₁

source

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) (h : s ≤ t) :

vector_space.dim K ↥s ≤ vector_space.dim K ↥t

source

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} (hv : linear_independent K v) :

(# ι).lift ≤ (vector_space.dim K V).lift

source

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} (hs : linear_independent K v) :

(# ι).lift ≤ (vector_space.dim K V).lift

source

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₃) (hde : ⊤ ≤ db.range ⊔ eb.range) (hgd : cd.ker = ⊥) (eq : db.comp cd = eb.comp ce) (eq₂ : ∀ (d : V₂) (e : V₃), ⇑db d = ⇑eb e → (∃ (c : V₁), ⇑cd c = d ∧ ⇑ce c = e)) :

vector_space.dim K V + vector_space.dim K V₁ = vector_space.dim K V₂ + vector_space.dim K V₃

This is mostly an auxiliary lemma for dim_sup_add_dim_inf_eq.

source

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

source

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

source

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

source

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

source

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

source

theorem dim_fun' {K : Type u} {η : Type u₁'} [field K] [fintype η] :

vector_space.dim K (η → K) = ↑(fintype.card η)

source

theorem dim_fin_fun {K : Type u} [field K] (n : ℕ) :

vector_space.dim K (fin n → K) = ↑n

source

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} (h : s ≠ ⊥) :

∃ (b : V), b ∈ s ∧ b ≠ 0

source

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} (h : 0 < vector_space.dim K ↥s) :

∃ (b : V), b ∈ s ∧ b ≠ 0

source

theorem exists_is_basis_fintype {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (h : vector_space.dim K V < cardinal.omega) :

∃ (s : set V), is_basis K subtype.val ∧ nonempty (fintype ↥s)

source

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'] (f : V →ₗ[K] V') :

cardinal

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)

source

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

source

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₁

source

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') :

rank (f + g) ≤ rank f + rank g

source

@[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'] :

rank 0 = 0

source

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')) :

rank (∑ (d : η) in s, f d) ≤ ∑ (d : η) in s, rank (f d)

source

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'') :

rank (f.comp g) ≤ rank f

source

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'₁) :

rank (f.comp g) ≤ rank g

source

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

source

theorem dim_zero_iff {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] :

vector_space.dim K V = 0 ↔ subsingleton V

source

theorem is_basis_of_dim_eq_zero {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type u_1} (h : ¬nonempty ι) (hV : vector_space.dim K V = 0) :

is_basis K (λ (x : ι), 0)

source

theorem is_basis_of_dim_eq_zero' {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (hV : vector_space.dim K V = 0) :

is_basis K (λ (x : fin 0), 0)

source

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

source

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

source

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

source

theorem le_dim_iff_exists_linear_independent {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {c : cardinal} :

c ≤ vector_space.dim K V ↔ ∃ (s : set V), # ↥s = c ∧ linear_independent K coe

source

theorem le_dim_iff_exists_linear_independent_finset {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {n : ℕ} :

↑n ≤ vector_space.dim K V ↔ ∃ (s : finset V), s.card = n ∧ linear_independent K coe

source

theorem le_rank_iff_exists_linear_independent {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'] {c : cardinal} {f : V →ₗ[K] V'} :

c ≤ rank f ↔ ∃ (s : set V), (# ↥s).lift = c.lift ∧ linear_independent K (λ (x : ↥s), ⇑f ↑x)

source

theorem le_rank_iff_exists_linear_independent_finset {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'] {n : ℕ} {f : V →ₗ[K] V'} :

↑n ≤ rank f ↔ ∃ (s : finset V), s.card = n ∧ linear_independent K (λ (x : ↥↑s), ⇑f ↑x)

source

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.

source

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.

source

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.

source

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] (f : V ≃ₗ[K] E) :

(vector_space.dim K V).lift = (vector_space.dim K E).lift

Version of linear_equiv.dim_eq without universe constraints.

mathlib documentation

Dimension of modules and vector spaces #

Main definitions #

Main statements #

Implementation notes #