Finite dimensional vector spaces #
Definition and basic properties of finite dimensional vector spaces, of their dimensions, and of linear maps on such spaces.
Main definitions #
Assume V is a vector space over a field K. There are (at least) three equivalent definitions of
finite-dimensionality of V:
- it admits a finite basis.
- it is finitely generated.
- it is noetherian, i.e., every subspace is finitely generated.
We introduce a typeclass finite_dimensional K V capturing this property. For ease of transfer of
proof, it is defined using the second point of view, i.e., as finite. However, we prove
that all these points of view are equivalent, with the following lemmas
(in the namespace finite_dimensional):
fintype_basis_indexstates that a finite-dimensional vector space has a finite basisfinite_dimensional.fin_basisandfinite_dimensional.fin_basis_of_finrank_eqare bases for finite dimensional vector spaces, where the index type isfinof_fintype_basisstates that the existence of a basis indexed by a finite type implies finite-dimensionalityof_finset_basisstates that the existence of a basis indexed by afinsetimplies finite-dimensionalityof_finite_basisstates that the existence of a basis indexed by a finite set implies finite-dimensionalityis_noetherian.iff_fgstates that the space is finite-dimensional if and only if it is noetherian
Also defined is 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.
Preservation of finite-dimensionality and formulas for the dimension are given for
- submodules
- quotients (for the dimension of a quotient, see
finrank_quotient_add_finrank) - linear equivs, in
linear_equiv.finite_dimensionalandlinear_equiv.finrank_eq - image under a linear map (the rank-nullity formula is in
finrank_range_add_finrank_ker)
Basic properties of linear maps of a finite-dimensional vector space are given. Notably, the
equivalence of injectivity and surjectivity is proved in linear_map.injective_iff_surjective,
and the equivalence between left-inverse and right-inverse in linear_map.mul_eq_one_comm
and linear_map.comp_eq_id_comm.
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.
Much of this file could be generalised away from fields or division rings. You should not assume that there has been any effort to state lemmas as generally as possible.
One of the characterizations of finite-dimensionality is in terms of finite generation. This
property is currently defined only for submodules, so we express it through the fact that the
maximal submodule (which, as a set, coincides with the whole space) is finitely generated. This is
not very convenient to use, although there are some helper functions. However, this becomes very
convenient when speaking of submodules which are finite-dimensional, as this notion coincides with
the fact that the submodule is finitely generated (as a submodule of the whole space). This
equivalence is proved in submodule.fg_iff_finite_dimensional.
def
finite_dimensional
(K : Type u_1)
(V : Type u_2)
[division_ring K]
[add_comm_group V]
[module K V] :
Prop
finite_dimensional vector spaces are defined to be finite modules.
Use finite_dimensional.of_fintype_basis to prove finite dimension from another definition.
Equations
- finite_dimensional K V = module.finite K V
@[protected, instance]
def
finite_dimensional.finite_dimensional_pi
(K : Type u)
[division_ring K]
{ι : Type u_1}
[fintype ι] :
finite_dimensional K (ι → K)
noncomputable
def
finite_dimensional.fintype_of_fintype
(K : Type u)
(V : Type v)
[division_ring K]
[add_comm_group V]
[module K V]
[fintype K]
[finite_dimensional K V] :
fintype V
A finite dimensional vector space over a finite field is finite
Equations
theorem
finite_dimensional.of_fintype_basis
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type w}
[fintype ι]
(h : basis ι K V) :
If a vector space has a finite basis, then it is finite-dimensional.
noncomputable
def
finite_dimensional.fintype_basis_index
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[finite_dimensional K V]
(b : basis ι K V) :
fintype ι
If a vector space is finite_dimensional, all bases are indexed by a finite type
Equations
- finite_dimensional.fintype_basis_index b = let _inst : is_noetherian K V := finite_dimensional.fintype_basis_index._proof_1 in is_noetherian.fintype_basis_index b
@[protected, instance]
noncomputable
def
finite_dimensional.basis.of_vector_space_index.fintype
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
If a vector space is finite_dimensional, basis.of_vector_space is indexed by
a finite type.
Equations
- finite_dimensional.basis.of_vector_space_index.fintype = let _inst : is_noetherian K V := finite_dimensional.basis.of_vector_space_index.fintype._proof_1 in is_noetherian.basis.of_vector_space_index.fintype
theorem
finite_dimensional.of_finite_basis
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type w}
{s : set ι}
(h : basis ↥s K V)
(hs : s.finite) :
If a vector space has a basis indexed by elements of a finite set, then it is finite-dimensional.
theorem
finite_dimensional.of_finset_basis
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type w}
{s : finset ι}
(h : basis ↥s K V) :
If a vector space has a finite basis, then it is finite-dimensional, finset style.
@[protected, instance]
def
finite_dimensional.finite_dimensional_submodule
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(S : submodule K V) :
A subspace of a finite-dimensional space is also finite-dimensional.
@[protected, instance]
def
finite_dimensional.finite_dimensional_quotient
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(S : submodule K V) :
finite_dimensional K (V ⧸ S)
A quotient of a finite-dimensional space is also finite-dimensional.
noncomputable
def
finite_dimensional.finrank
(R : Type u_1)
(V : Type u_2)
[semiring R]
[add_comm_group 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
theorem
finite_dimensional.finrank_eq_dim
(K : Type u)
(V : Type v)
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
↑(finite_dimensional.finrank K V) = module.rank K V
In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its
finrank.
theorem
finite_dimensional.finrank_eq_of_dim_eq
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{n : ℕ}
(h : module.rank K V = ↑n) :
finite_dimensional.finrank K V = n
theorem
finite_dimensional.finrank_of_infinite_dimensional
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
(h : ¬finite_dimensional K V) :
finite_dimensional.finrank K V = 0
theorem
finite_dimensional.finite_dimensional_of_finrank
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
(h : 0 < finite_dimensional.finrank K V) :
theorem
finite_dimensional.finite_dimensional_of_finrank_eq_succ
{K : Type u_1}
{V : Type u_2}
[field K]
[add_comm_group V]
[module K V]
{n : ℕ}
(hn : finite_dimensional.finrank K V = n.succ) :
theorem
finite_dimensional.fact_finite_dimensional_of_finrank_eq_succ
{K : Type u_1}
{V : Type u_2}
[field K]
[add_comm_group V]
[module K V]
(n : ℕ)
[fact (finite_dimensional.finrank K V = n + 1)] :
We can infer finite_dimensional K V in the presence of [fact (finrank K V = n + 1)]. Declare
this as a local instance where needed.
theorem
finite_dimensional.finrank_eq_card_basis
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type w}
[fintype ι]
(h : basis ι K V) :
If a vector space has a finite basis, then its dimension is equal to the cardinality of the basis.
theorem
finite_dimensional.finrank_eq_card_basis'
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{ι : Type w}
(h : basis ι K V) :
↑(finite_dimensional.finrank K V) = # ι
If a vector space is finite-dimensional, then the cardinality of any basis is equal to its
finrank.
theorem
finite_dimensional.finrank_eq_card_finset_basis
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type w}
{b : finset ι}
(h : basis ↥b K V) :
finite_dimensional.finrank K V = b.card
If a vector space has a finite basis, then its dimension is equal to the cardinality of the
basis. This lemma uses a finset instead of indexed types.
noncomputable
def
finite_dimensional.fin_basis
(K : Type u)
(V : Type v)
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
basis (fin (finite_dimensional.finrank K V)) K V
A finite dimensional vector space has a basis indexed by fin (finrank K V).
Equations
- finite_dimensional.fin_basis K V = have h : fintype.card ↥(is_noetherian.finset_basis_index K V) = finite_dimensional.finrank K V, from _, (is_noetherian.finset_basis K V).reindex (fintype.equiv_fin_of_card_eq h)
noncomputable
def
finite_dimensional.fin_basis_of_finrank_eq
(K : Type u)
(V : Type v)
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{n : ℕ}
(hn : finite_dimensional.finrank K V = n) :
An n-dimensional vector space has a basis indexed by fin n.
Equations
noncomputable
def
finite_dimensional.basis_unique
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
(ι : Type u_1)
[unique ι]
(h : finite_dimensional.finrank K V = 1) :
basis ι K V
A module with dimension 1 has a basis with one element.
@[simp]
theorem
finite_dimensional.basis_unique.repr_eq_zero_iff
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[unique ι]
{h : finite_dimensional.finrank K V = 1}
{v : V}
{i : ι} :
theorem
finite_dimensional.cardinal_mk_le_finrank_of_linear_independent
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{ι : Type w}
{b : ι → V}
(h : linear_independent K b) :
# ι ≤ ↑(finite_dimensional.finrank K V)
theorem
finite_dimensional.fintype_card_le_finrank_of_linear_independent
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{ι : Type u_1}
[fintype ι]
{b : ι → V}
(h : linear_independent K b) :
theorem
finite_dimensional.finset_card_le_finrank_of_linear_independent
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{b : finset V}
(h : linear_independent K (λ (x : ↥b), ↑x)) :
b.card ≤ finite_dimensional.finrank K V
theorem
finite_dimensional.lt_omega_of_linear_independent
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type w}
[finite_dimensional K V]
{v : ι → V}
(h : linear_independent K v) :
theorem
finite_dimensional.not_linear_independent_of_infinite
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type w}
[inf : infinite ι]
[finite_dimensional K V]
(v : ι → V) :
theorem
finite_dimensional.finrank_pos_iff_exists_ne_zero
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
0 < finite_dimensional.finrank K V ↔ ∃ (x : V), x ≠ 0
A finite dimensional space has positive finrank iff it has a nonzero element.
theorem
finite_dimensional.finrank_pos_iff
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
0 < finite_dimensional.finrank K V ↔ nontrivial V
A finite dimensional space has positive finrank iff it is nontrivial.
theorem
finite_dimensional.nontrivial_of_finrank_pos
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
(h : 0 < finite_dimensional.finrank K V) :
A finite dimensional space is nontrivial if it has positive finrank.
theorem
finite_dimensional.nontrivial_of_finrank_eq_succ
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{n : ℕ}
(hn : finite_dimensional.finrank K V = n.succ) :
A finite dimensional space is nontrivial if it has finrank equal to the successor of a
natural number.
theorem
finite_dimensional.finrank_pos
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
[h : nontrivial V] :
0 < finite_dimensional.finrank K V
A nontrivial finite dimensional space has positive finrank.
theorem
finite_dimensional.finrank_zero_iff
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
finite_dimensional.finrank K V = 0 ↔ subsingleton V
A finite dimensional space has zero finrank iff it is a subsingleton.
This is the finrank version of dim_zero_iff.
theorem
finite_dimensional.finrank_zero_of_subsingleton
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[h : subsingleton V] :
finite_dimensional.finrank K V = 0
A finite dimensional space that is a subsingleton has zero finrank.
theorem
finite_dimensional.basis.subset_extend
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{s : set V}
(hs : linear_independent K coe) :
theorem
finite_dimensional.eq_top_of_finrank_eq
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{S : submodule K V}
(h : finite_dimensional.finrank K ↥S = finite_dimensional.finrank K V) :
If a submodule has maximal dimension in a finite dimensional space, then it is equal to the whole space.
@[simp]
theorem
finite_dimensional.finrank_self
(K : Type u)
[division_ring K] :
finite_dimensional.finrank K K = 1
A division_ring is one-dimensional as a vector space over itself.
@[protected, instance]
@[simp]
theorem
finite_dimensional.finrank_fintype_fun_eq_card
(K : Type u)
[division_ring K]
{ι : Type v}
[fintype ι] :
finite_dimensional.finrank K (ι → K) = fintype.card ι
The vector space of functions on a fintype ι has finrank equal to the cardinality of ι.
@[simp]
theorem
finite_dimensional.finrank_fin_fun
(K : Type u)
[division_ring K]
{n : ℕ} :
finite_dimensional.finrank K (fin n → K) = n
The vector space of functions on fin n has finrank equal to n.
theorem
finite_dimensional.span_of_finite
(K : Type u)
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{A : set V}
(hA : A.finite) :
finite_dimensional K ↥(submodule.span K A)
The submodule generated by a finite set is finite-dimensional.
@[protected, instance]
def
finite_dimensional.span_singleton
(K : Type u)
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
(x : V) :
finite_dimensional K ↥(submodule.span K {x})
The submodule generated by a single element is finite-dimensional.
@[protected, instance]
def
finite_dimensional.span_finset
(K : Type u)
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
(s : finset V) :
finite_dimensional K ↥(submodule.span K ↑s)
The submodule generated by a finset is finite-dimensional.
@[protected, instance]
def
finite_dimensional.submodule.map.finite_dimensional
(K : Type u)
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
(f : V →ₗ[K] V₂)
(p : submodule K V)
[h : finite_dimensional K ↥p] :
finite_dimensional K ↥(submodule.map f p)
Pushforwards of finite-dimensional submodules are finite-dimensional.
theorem
finite_dimensional.finrank_map_le
(K : Type u)
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
(f : V →ₗ[K] V₂)
(p : submodule K V)
[finite_dimensional K ↥p] :
Pushforwards of finite-dimensional submodules have a smaller finrank.
theorem
complete_lattice.independent.subtype_ne_bot_le_finrank_aux
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{ι : Type w}
{p : ι → submodule K V}
(hp : complete_lattice.independent p) :
noncomputable
def
complete_lattice.independent.fintype_ne_bot_of_finite_dimensional
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{ι : Type w}
{p : ι → submodule K V}
(hp : complete_lattice.independent p) :
If p is an independent family of subspaces of a finite-dimensional space V, then the
number of nontrivial subspaces in the family p is finite.
Equations
theorem
complete_lattice.independent.subtype_ne_bot_le_finrank
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{ι : Type w}
{p : ι → submodule K V}
(hp : complete_lattice.independent p)
[fintype {i // p i ≠ ⊥}] :
fintype.card {i // p i ≠ ⊥} ≤ finite_dimensional.finrank K V
If p is an independent family of subspaces of a finite-dimensional space V, then the
number of nontrivial subspaces in the family p is bounded above by the dimension of V.
Note that the fintype hypothesis required here can be provided by
complete_lattice.independent.fintype_ne_bot_of_finite_dimensional.
theorem
finite_dimensional.exists_nontrivial_relation_of_dim_lt_card
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{t : finset V}
(h : finite_dimensional.finrank K V < t.card) :
If a finset has cardinality larger than the dimension of the space, then there is a nontrivial linear relation amongst its elements.
theorem
finite_dimensional.exists_nontrivial_relation_sum_zero_of_dim_succ_lt_card
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{t : finset V}
(h : finite_dimensional.finrank K V + 1 < t.card) :
If a finset has cardinality larger than finrank + 1,
then there is a nontrivial linear relation amongst its elements,
such that the coefficients of the relation sum to zero.
theorem
finite_dimensional.exists_relation_sum_zero_pos_coefficient_of_dim_succ_lt_card
{L : Type u_1}
[linear_ordered_field L]
{W : Type v}
[add_comm_group W]
[module L W]
[finite_dimensional L W]
{t : finset W}
(h : finite_dimensional.finrank L W + 1 < t.card) :
A slight strengthening of exists_nontrivial_relation_sum_zero_of_dim_succ_lt_card
available when working over an ordered field:
we can ensure a positive coefficient, not just a nonzero coefficient.
noncomputable
def
finite_dimensional.basis_singleton
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(ι : Type u_1)
[unique ι]
(h : finite_dimensional.finrank K V = 1)
(v : V)
(hv : v ≠ 0) :
basis ι K V
In a vector space with dimension 1, each set {v} is a basis for v ≠ 0.
Equations
- finite_dimensional.basis_singleton ι h v hv = let b : basis ι K V := finite_dimensional.basis_unique ι h in b.map (linear_equiv.smul_of_unit (units.mk0 (⇑(⇑(b.repr) v) default) _))
@[simp]
theorem
finite_dimensional.basis_singleton_apply
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(ι : Type u_1)
[unique ι]
(h : finite_dimensional.finrank K V = 1)
(v : V)
(hv : v ≠ 0)
(i : ι) :
⇑(finite_dimensional.basis_singleton ι h v hv) i = v
@[simp]
theorem
finite_dimensional.range_basis_singleton
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(ι : Type u_1)
[unique ι]
(h : finite_dimensional.finrank K V = 1)
(v : V)
(hv : v ≠ 0) :
set.range ⇑(finite_dimensional.basis_singleton ι h v hv) = {v}
theorem
finite_dimensional_of_dim_eq_zero
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(h : module.rank K V = 0) :
theorem
finite_dimensional_of_dim_eq_one
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(h : module.rank K V = 1) :
theorem
finrank_eq_zero_of_dim_eq_zero
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(h : module.rank K V = 0) :
finite_dimensional.finrank K V = 0
theorem
finrank_eq_zero_of_basis_imp_not_finite
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(h : ∀ (s : set V), basis ↥s K V → ¬s.finite) :
finite_dimensional.finrank K V = 0
theorem
finrank_eq_zero_of_basis_imp_false
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(h : ∀ (s : finset V), basis ↥↑s K V → false) :
finite_dimensional.finrank K V = 0
theorem
finrank_eq_zero_of_not_exists_basis
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(h : ¬∃ (s : finset V), nonempty (basis ↥↑s K V)) :
finite_dimensional.finrank K V = 0
theorem
finrank_eq_zero_of_not_exists_basis_finite
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(h : ¬∃ (s : set V) (b : basis ↥s K V), s.finite) :
finite_dimensional.finrank K V = 0
theorem
finrank_eq_zero_of_not_exists_basis_finset
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(h : ¬∃ (s : finset V), nonempty (basis ↥s K V)) :
finite_dimensional.finrank K V = 0
@[protected, instance]
@[simp]
theorem
bot_eq_top_of_dim_eq_zero
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(h : module.rank K V = 0) :
@[simp]
theorem
dim_eq_zero
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{S : submodule K V} :
@[simp]
theorem
finrank_eq_zero
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{S : submodule K V}
[finite_dimensional K ↥S] :
theorem
submodule.fg_iff_finite_dimensional
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(s : submodule K V) :
s.fg ↔ finite_dimensional K ↥s
A submodule is finitely generated if and only if it is finite-dimensional
theorem
submodule.finite_dimensional_of_le
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{S₁ S₂ : submodule K V}
[finite_dimensional K ↥S₂]
(h : S₁ ≤ S₂) :
finite_dimensional K ↥S₁
A submodule contained in a finite-dimensional submodule is finite-dimensional.
@[protected, instance]
def
submodule.finite_dimensional_inf_left
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(S₁ S₂ : submodule K V)
[finite_dimensional K ↥S₁] :
finite_dimensional K ↥(S₁ ⊓ S₂)
The inf of two submodules, the first finite-dimensional, is finite-dimensional.
@[protected, instance]
def
submodule.finite_dimensional_inf_right
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(S₁ S₂ : submodule K V)
[finite_dimensional K ↥S₂] :
finite_dimensional K ↥(S₁ ⊓ S₂)
The inf of two submodules, the second finite-dimensional, is finite-dimensional.
@[protected, instance]
def
submodule.finite_dimensional_sup
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(S₁ S₂ : submodule K V)
[h₁ : finite_dimensional K ↥S₁]
[h₂ : finite_dimensional K ↥S₂] :
finite_dimensional K ↥(S₁ ⊔ S₂)
The sup of two finite-dimensional submodules is finite-dimensional.
@[protected, instance]
def
submodule.finite_dimensional_finset_sup
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
(s : finset ι)
(S : ι → submodule K V)
[∀ (i : ι), finite_dimensional K ↥(S i)] :
finite_dimensional K ↥(s.sup S)
The submodule generated by a finite supremum of finite dimensional submodules is finite-dimensional.
Note that strictly this only needs ∀ i ∈ s, finite_dimensional K (S i), but that doesn't
work well with typeclass search.
@[protected, instance]
def
submodule.finite_dimensional_supr
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
(S : ι → submodule K V)
[∀ (i : ι), finite_dimensional K ↥(S i)] :
finite_dimensional K (↥⨆ (i : ι), S i)
The submodule generated by a supremum of finite dimensional submodules, indexed by a finite type is finite-dimensional.
@[protected, instance]
def
submodule.finite_dimensional_supr_prop
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{P : Prop}
(S : P → submodule K V)
[∀ (h : P), finite_dimensional K ↥(S h)] :
finite_dimensional K (↥⨆ (h : P), S h)
The submodule generated by a supremum indexed by a proposition is finite-dimensional if the submodule is.
theorem
submodule.finrank_quotient_add_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(s : submodule K V) :
finite_dimensional.finrank K (V ⧸ s) + finite_dimensional.finrank K ↥s = finite_dimensional.finrank K V
In a finite-dimensional vector space, the dimensions of a submodule and of the corresponding quotient add up to the dimension of the space.
theorem
submodule.finrank_le
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(s : submodule K V) :
The dimension of a submodule is bounded by the dimension of the ambient space.
theorem
submodule.finrank_lt
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional 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_quotient_le
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(s : submodule K V) :
finite_dimensional.finrank K (V ⧸ s) ≤ finite_dimensional.finrank K V
The dimension of a quotient is bounded by the dimension of the ambient space.
theorem
submodule.dim_sup_add_dim_inf_eq
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(s t : submodule K V)
[finite_dimensional K ↥s]
[finite_dimensional K ↥t] :
finite_dimensional.finrank K ↥(s ⊔ t) + finite_dimensional.finrank K ↥(s ⊓ t) = finite_dimensional.finrank K ↥s + finite_dimensional.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.eq_top_of_disjoint
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(s t : submodule K V)
(hdim : finite_dimensional.finrank K ↥s + finite_dimensional.finrank K ↥t = finite_dimensional.finrank K V)
(hdisjoint : disjoint s t) :
@[protected]
theorem
linear_equiv.finite_dimensional
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
(f : V ≃ₗ[K] V₂)
[finite_dimensional K V] :
finite_dimensional K V₂
Finite dimensionality is preserved under linear equivalence.
theorem
linear_equiv.finrank_eq
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M ≃ₗ[R] M₂) :
The dimension of a finite dimensional space is preserved under linear equivalence.
theorem
linear_equiv.finrank_map_eq
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M ≃ₗ[R] M₂)
(p : submodule R M) :
Pushforwards of finite-dimensional submodules along a linear_equiv have the same finrank.
@[protected, instance]
def
finite_dimensional_finsupp
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
[h : finite_dimensional K V] :
finite_dimensional K (ι →₀ V)
theorem
finite_dimensional.nonempty_linear_equiv_of_finrank_eq
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
[finite_dimensional K V]
[finite_dimensional K V₂]
(cond : finite_dimensional.finrank K V = finite_dimensional.finrank K V₂) :
Two finite-dimensional vector spaces are isomorphic if they have the same (finite) dimension.
theorem
finite_dimensional.nonempty_linear_equiv_iff_finrank_eq
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
[finite_dimensional K V]
[finite_dimensional K V₂] :
nonempty (V ≃ₗ[K] V₂) ↔ finite_dimensional.finrank K V = finite_dimensional.finrank K V₂
Two finite-dimensional vector spaces are isomorphic if and only if they have the same (finite) dimension.
noncomputable
def
finite_dimensional.linear_equiv.of_finrank_eq
{K : Type u}
(V : Type v)
[field K]
[add_comm_group V]
[module K V]
(V₂ : Type v')
[add_comm_group V₂]
[module K V₂]
[finite_dimensional K V]
[finite_dimensional K V₂]
(cond : finite_dimensional.finrank K V = finite_dimensional.finrank K V₂) :
Two finite-dimensional vector spaces are isomorphic if they have the same (finite) dimension.
Equations
theorem
finite_dimensional.eq_of_le_of_finrank_le
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{S₁ S₂ : submodule K V}
[finite_dimensional K ↥S₂]
(hle : S₁ ≤ S₂)
(hd : finite_dimensional.finrank K ↥S₂ ≤ finite_dimensional.finrank K ↥S₁) :
S₁ = S₂
theorem
finite_dimensional.eq_of_le_of_finrank_eq
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{S₁ S₂ : submodule K V}
[finite_dimensional K ↥S₂]
(hle : S₁ ≤ S₂)
(hd : finite_dimensional.finrank K ↥S₁ = finite_dimensional.finrank K ↥S₂) :
S₁ = S₂
If a submodule is less than or equal to a finite-dimensional submodule with the same dimension, they are equal.
@[simp]
theorem
finite_dimensional.finrank_map_subtype_eq
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(p : subspace K V)
(q : subspace K ↥p) :
noncomputable
def
finite_dimensional.linear_equiv.quot_equiv_of_equiv
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
[finite_dimensional K V]
[finite_dimensional 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
- finite_dimensional.linear_equiv.quot_equiv_of_equiv f₁ f₂ = finite_dimensional.linear_equiv.of_finrank_eq (V ⧸ p) (V₂ ⧸ q) _
noncomputable
def
finite_dimensional.linear_equiv.quot_equiv_of_quot_equiv
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional 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
theorem
linear_map.surjective_of_injective
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{f : V →ₗ[K] V}
(hinj : function.injective ⇑f) :
On a finite-dimensional space, an injective linear map is surjective.
theorem
linear_map.injective_iff_surjective
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{f : V →ₗ[K] V} :
On a finite-dimensional space, a linear map is injective if and only if it is surjective.
theorem
linear_map.ker_eq_bot_iff_range_eq_top
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{f : V →ₗ[K] V} :
theorem
linear_map.mul_eq_one_of_mul_eq_one
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{f g : V →ₗ[K] V}
(hfg : f * g = 1) :
In a finite-dimensional space, if linear maps are inverse to each other on one side then they are also inverse to each other on the other side.
theorem
linear_map.mul_eq_one_comm
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{f g : V →ₗ[K] V} :
In a finite-dimensional space, linear maps are inverse to each other on one side if and only if they are inverse to each other on the other side.
theorem
linear_map.comp_eq_id_comm
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{f g : V →ₗ[K] V} :
f.comp g = linear_map.id ↔ g.comp f = linear_map.id
In a finite-dimensional space, linear maps are inverse to each other on one side if and only if they are inverse to each other on the other side.
theorem
linear_map.finite_dimensional_of_surjective
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
[h : finite_dimensional K V]
(f : V →ₗ[K] V₂)
(hf : f.range = ⊤) :
finite_dimensional K V₂
The image under an onto linear map of a finite-dimensional space is also finite-dimensional.
@[protected, instance]
def
linear_map.finite_dimensional_range
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
[h : finite_dimensional K V]
(f : V →ₗ[K] V₂) :
finite_dimensional K ↥(f.range)
The range of a linear map defined on a finite-dimensional space is also finite-dimensional.
theorem
linear_map.finrank_range_add_finrank_ker
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
[finite_dimensional 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
linear_map.finrank_range_of_inj
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
{f : V →ₗ[K] V₂}
(hf : function.injective ⇑f) :
The dimensions of the domain and range of an injective linear map are equal.
noncomputable
def
linear_equiv.of_injective_endo
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(f : V →ₗ[K] V)
(h_inj : function.injective ⇑f) :
The linear equivalence corresponging to an injective endomorphism.
Equations
- linear_equiv.of_injective_endo f h_inj = linear_equiv.of_bijective f h_inj _
@[simp]
theorem
linear_equiv.coe_of_injective_endo
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(f : V →ₗ[K] V)
(h_inj : function.injective ⇑f) :
⇑(linear_equiv.of_injective_endo f h_inj) = ⇑f
@[simp]
theorem
linear_equiv.of_injective_endo_right_inv
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(f : V →ₗ[K] V)
(h_inj : function.injective ⇑f) :
f * ↑((linear_equiv.of_injective_endo f h_inj).symm) = 1
@[simp]
theorem
linear_equiv.of_injective_endo_left_inv
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(f : V →ₗ[K] V)
(h_inj : function.injective ⇑f) :
(↑((linear_equiv.of_injective_endo f h_inj).symm)) * f = 1
theorem
linear_map.is_unit_iff_ker_eq_bot
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(f : V →ₗ[K] V) :
theorem
linear_map.is_unit_iff_range_eq_top
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(f : V →ₗ[K] V) :
@[simp]
theorem
finrank_zero_iff_forall_zero
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
finite_dimensional.finrank K V = 0 ↔ ∀ (x : V), x = 0
noncomputable
def
basis_of_finrank_zero
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{ι : Type u_1}
[is_empty ι]
(hV : finite_dimensional.finrank K V = 0) :
basis ι K V
If ι is an empty type and V is zero-dimensional, there is a unique ι-indexed basis.
Equations
theorem
linear_map.injective_iff_surjective_of_finrank_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
[finite_dimensional K V]
[finite_dimensional K V₂]
(H : finite_dimensional.finrank K V = finite_dimensional.finrank K V₂)
{f : V →ₗ[K] V₂} :
theorem
linear_map.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
[finite_dimensional K V]
[finite_dimensional K V₂]
(H : finite_dimensional.finrank K V = finite_dimensional.finrank K V₂)
{f : V →ₗ[K] V₂} :
theorem
linear_map.finrank_le_finrank_of_injective
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
[finite_dimensional K V]
[finite_dimensional K V₂]
{f : V →ₗ[K] V₂}
(hf : function.injective ⇑f) :
noncomputable
def
linear_map.linear_equiv_of_injective
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
[finite_dimensional K V]
[finite_dimensional K V₂]
(f : V →ₗ[K] V₂)
(hf : function.injective ⇑f)
(hdim : finite_dimensional.finrank K V = finite_dimensional.finrank K V₂) :
Given a linear map f between two vector spaces with the same dimension, if
ker f = ⊥ then linear_equiv_of_injective is the induced isomorphism
between the two vector spaces.
Equations
- f.linear_equiv_of_injective hf hdim = linear_equiv.of_bijective f hf _
@[simp]
theorem
linear_map.linear_equiv_of_injective_apply
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
[finite_dimensional K V]
[finite_dimensional K V₂]
{f : V →ₗ[K] V₂}
(hf : function.injective ⇑f)
(hdim : finite_dimensional.finrank K V = finite_dimensional.finrank K V₂)
(x : V) :
⇑(f.linear_equiv_of_injective hf hdim) x = ⇑f x
theorem
alg_hom.bijective
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
[finite_dimensional F E]
(ϕ : E →ₐ[F] E) :
noncomputable
def
alg_equiv_equiv_alg_hom
(F : Type u)
[field F]
(E : Type v)
[field E]
[algebra F E]
[finite_dimensional F E] :
Bijection between algebra equivalences and algebra homomorphisms
Equations
- alg_equiv_equiv_alg_hom F E = {to_fun := λ (ϕ : E ≃ₐ[F] E), ϕ.to_alg_hom, inv_fun := λ (ϕ : E →ₐ[F] E), alg_equiv.of_bijective ϕ _, left_inv := _, right_inv := _}
noncomputable
def
division_ring_of_finite_dimensional
(F : Type u_1)
(K : Type u_2)
[field F]
[ring K]
[is_domain K]
[algebra F K]
[finite_dimensional F K] :
A domain that is module-finite as an algebra over a field is a division ring.
Equations
- division_ring_of_finite_dimensional F K = {add := ring.add _inst_7, add_assoc := _, zero := ring.zero _inst_7, zero_add := _, add_zero := _, nsmul := ring.nsmul _inst_7, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg _inst_7, sub := ring.sub _inst_7, sub_eq_add_neg := _, zsmul := ring.zsmul _inst_7, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ring.mul _inst_7, mul_assoc := _, one := ring.one _inst_7, one_mul := _, mul_one := _, npow := ring.npow _inst_7, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := λ (x : K), dite (x = 0) (λ (H : x = 0), 0) (λ (H : ¬x = 0), classical.some _), div := div_inv_monoid.div._default ring.mul ring.mul_assoc ring.one ring.one_mul ring.mul_one ring.npow ring.npow_zero' ring.npow_succ' (λ (x : K), dite (x = 0) (λ (H : x = 0), 0) (λ (H : ¬x = 0), classical.some _)), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default ring.mul ring.mul_assoc ring.one ring.one_mul ring.mul_one ring.npow ring.npow_zero' ring.npow_succ' (λ (x : K), dite (x = 0) (λ (H : x = 0), 0) (λ (H : ¬x = 0), classical.some _)), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
noncomputable
def
field_of_finite_dimensional
(F : Type u_1)
(K : Type u_2)
[field F]
[comm_ring K]
[is_domain K]
[algebra F K]
[finite_dimensional F K] :
field K
An integral domain that is module-finite as an algebra over a field is a field.
Equations
- field_of_finite_dimensional F K = {add := division_ring.add (division_ring_of_finite_dimensional F K), add_assoc := _, zero := division_ring.zero (division_ring_of_finite_dimensional F K), zero_add := _, add_zero := _, nsmul := division_ring.nsmul (division_ring_of_finite_dimensional F K), nsmul_zero' := _, nsmul_succ' := _, neg := division_ring.neg (division_ring_of_finite_dimensional F K), sub := division_ring.sub (division_ring_of_finite_dimensional F K), sub_eq_add_neg := _, zsmul := division_ring.zsmul (division_ring_of_finite_dimensional F K), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := division_ring.mul (division_ring_of_finite_dimensional F K), mul_assoc := _, one := division_ring.one (division_ring_of_finite_dimensional F K), one_mul := _, mul_one := _, npow := division_ring.npow (division_ring_of_finite_dimensional F K), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := division_ring.inv (division_ring_of_finite_dimensional F K), div := division_ring.div (division_ring_of_finite_dimensional F K), div_eq_mul_inv := _, zpow := division_ring.zpow (division_ring_of_finite_dimensional F K), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
theorem
submodule.finrank_mono
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
monotone (λ (s : submodule K V), finite_dimensional.finrank K ↥s)
theorem
submodule.lt_of_le_of_finrank_lt_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s t : submodule K V}
(le : s ≤ t)
(lt : finite_dimensional.finrank K ↥s < finite_dimensional.finrank K ↥t) :
s < t
theorem
submodule.lt_top_of_finrank_lt_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : submodule K V}
(lt : finite_dimensional.finrank K ↥s < finite_dimensional.finrank K V) :
theorem
submodule.finrank_lt_finrank_of_lt
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{s t : submodule K V}
(hst : s < t) :
theorem
submodule.finrank_add_eq_of_is_compl
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{U W : submodule K V}
(h : is_compl U W) :
@[protected]
noncomputable
def
set.finrank
(K : Type u)
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(s : set V) :
The rank of a set of vectors as a natural number.
Equations
- set.finrank K s = finite_dimensional.finrank K ↥(submodule.span K s)
theorem
set.finrank_mono
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{s t : set V}
(h : s ⊆ t) :
set.finrank K s ≤ set.finrank K t
theorem
finrank_span_le_card
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(s : set V)
[fin : fintype ↥s] :
finite_dimensional.finrank K ↥(submodule.span K s) ≤ s.to_finset.card
theorem
finrank_span_finset_le_card
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(s : finset V) :
set.finrank K ↑s ≤ s.card
theorem
finrank_span_eq_card
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
{b : ι → V}
(hb : linear_independent K b) :
finite_dimensional.finrank K ↥(submodule.span K (set.range b)) = fintype.card ι
theorem
finrank_span_set_eq_card
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(s : set V)
[fin : fintype ↥s]
(hs : linear_independent K coe) :
finite_dimensional.finrank K ↥(submodule.span K s) = s.to_finset.card
theorem
finrank_span_finset_eq_card
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(s : finset V)
(hs : linear_independent K coe) :
finite_dimensional.finrank K ↥(submodule.span K ↑s) = s.card
theorem
span_lt_of_subset_of_card_lt_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : set V}
[fintype ↥s]
{t : submodule K V}
(subset : s ⊆ ↑t)
(card_lt : s.to_finset.card < finite_dimensional.finrank K ↥t) :
submodule.span K s < t
theorem
span_lt_top_of_card_lt_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : set V}
[fintype ↥s]
(card_lt : s.to_finset.card < finite_dimensional.finrank K V) :
submodule.span K s < ⊤
theorem
finrank_span_singleton
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{v : V}
(hv : v ≠ 0) :
finite_dimensional.finrank K ↥(submodule.span K {v}) = 1
theorem
linear_independent_of_span_eq_top_of_card_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
{b : ι → V}
(span_eq : submodule.span K (set.range b) = ⊤)
(card_eq : fintype.card ι = finite_dimensional.finrank K V) :
theorem
linear_independent_iff_card_eq_finrank_span
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
{b : ι → V} :
linear_independent 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.
noncomputable
def
basis_of_span_eq_top_of_card_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
(b : ι → V)
(span_eq : submodule.span K (set.range b) = ⊤)
(card_eq : fintype.card ι = finite_dimensional.finrank K V) :
basis ι K V
A family of finrank K V vectors forms a basis if they span the whole space.
Equations
- basis_of_span_eq_top_of_card_eq_finrank b span_eq card_eq = basis.mk _ span_eq
@[simp]
theorem
coe_basis_of_span_eq_top_of_card_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
(b : ι → V)
(span_eq : submodule.span K (set.range b) = ⊤)
(card_eq : fintype.card ι = finite_dimensional.finrank K V) :
⇑(basis_of_span_eq_top_of_card_eq_finrank b span_eq card_eq) = b
noncomputable
def
finset_basis_of_span_eq_top_of_card_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : finset V}
(span_eq : submodule.span K ↑s = ⊤)
(card_eq : s.card = finite_dimensional.finrank K V) :
A finset of finrank K V vectors forms a basis if they span the whole space.
Equations
- finset_basis_of_span_eq_top_of_card_eq_finrank span_eq card_eq = basis_of_span_eq_top_of_card_eq_finrank coe _ _
@[simp]
theorem
finset_basis_of_span_eq_top_of_card_eq_finrank_repr_symm_apply
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : finset V}
(span_eq : submodule.span K ↑s = ⊤)
(card_eq : s.card = finite_dimensional.finrank K V)
(ᾰ : ↥↑s →₀ K) :
⇑((finset_basis_of_span_eq_top_of_card_eq_finrank span_eq card_eq).repr.symm) ᾰ = ⇑(finsupp.total ↥s V K coe) ᾰ
@[simp]
theorem
finset_basis_of_span_eq_top_of_card_eq_finrank_repr_apply
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : finset V}
(span_eq : submodule.span K ↑s = ⊤)
(card_eq : s.card = finite_dimensional.finrank K V)
(ᾰ : V) :
⇑((finset_basis_of_span_eq_top_of_card_eq_finrank span_eq card_eq).repr) ᾰ = ⇑(_.repr) (⇑(linear_map.cod_restrict (submodule.span K (set.range coe)) linear_map.id _) ᾰ)
@[simp]
theorem
set_basis_of_span_eq_top_of_card_eq_finrank_repr_apply
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : set V}
[fintype ↥s]
(span_eq : submodule.span K s = ⊤)
(card_eq : s.to_finset.card = finite_dimensional.finrank K V)
(ᾰ : V) :
⇑((set_basis_of_span_eq_top_of_card_eq_finrank span_eq card_eq).repr) ᾰ = ⇑(_.repr) (⇑(linear_map.cod_restrict (submodule.span K (set.range coe)) linear_map.id _) ᾰ)
noncomputable
def
set_basis_of_span_eq_top_of_card_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : set V}
[fintype ↥s]
(span_eq : submodule.span K s = ⊤)
(card_eq : s.to_finset.card = finite_dimensional.finrank K V) :
A set of finrank K V vectors forms a basis if they span the whole space.
Equations
- set_basis_of_span_eq_top_of_card_eq_finrank span_eq card_eq = basis_of_span_eq_top_of_card_eq_finrank coe _ _
@[simp]
theorem
set_basis_of_span_eq_top_of_card_eq_finrank_repr_symm_apply
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : set V}
[fintype ↥s]
(span_eq : submodule.span K s = ⊤)
(card_eq : s.to_finset.card = finite_dimensional.finrank K V)
(ᾰ : ↥s →₀ K) :
⇑((set_basis_of_span_eq_top_of_card_eq_finrank span_eq card_eq).repr.symm) ᾰ = ⇑(finsupp.total ↥s V K coe) ᾰ
theorem
span_eq_top_of_linear_independent_of_card_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[hι : nonempty ι]
[fintype ι]
{b : ι → V}
(lin_ind : linear_independent K b)
(card_eq : fintype.card ι = finite_dimensional.finrank K V) :
submodule.span K (set.range b) = ⊤
noncomputable
def
basis_of_linear_independent_of_card_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[nonempty ι]
[fintype ι]
{b : ι → V}
(lin_ind : linear_independent K b)
(card_eq : fintype.card ι = finite_dimensional.finrank K V) :
basis ι K V
A linear independent family of finrank K V vectors forms a basis.
Equations
- basis_of_linear_independent_of_card_eq_finrank lin_ind card_eq = basis.mk lin_ind _
@[simp]
theorem
basis_of_linear_independent_of_card_eq_finrank_repr_apply
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[nonempty ι]
[fintype ι]
{b : ι → V}
(lin_ind : linear_independent K b)
(card_eq : fintype.card ι = finite_dimensional.finrank K V)
(ᾰ : V) :
⇑((basis_of_linear_independent_of_card_eq_finrank lin_ind card_eq).repr) ᾰ = ⇑(lin_ind.repr) (⇑(linear_map.cod_restrict (submodule.span K (set.range b)) linear_map.id _) ᾰ)
@[simp]
theorem
basis_of_linear_independent_of_card_eq_finrank_repr_symm_apply
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[nonempty ι]
[fintype ι]
{b : ι → V}
(lin_ind : linear_independent K b)
(card_eq : fintype.card ι = finite_dimensional.finrank K V)
(ᾰ : ι →₀ K) :
⇑((basis_of_linear_independent_of_card_eq_finrank lin_ind card_eq).repr.symm) ᾰ = ⇑(finsupp.total ι V K b) ᾰ
@[simp]
theorem
coe_basis_of_linear_independent_of_card_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[nonempty ι]
[fintype ι]
{b : ι → V}
(lin_ind : linear_independent K b)
(card_eq : fintype.card ι = finite_dimensional.finrank K V) :
⇑(basis_of_linear_independent_of_card_eq_finrank lin_ind card_eq) = b
@[simp]
theorem
finset_basis_of_linear_independent_of_card_eq_finrank_repr_symm_apply
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : finset V}
(hs : s.nonempty)
(lin_ind : linear_independent K coe)
(card_eq : s.card = finite_dimensional.finrank K V)
(ᾰ : {x // x ∈ s} →₀ K) :
⇑((finset_basis_of_linear_independent_of_card_eq_finrank hs lin_ind card_eq).repr.symm) ᾰ = ⇑(finsupp.total {x // x ∈ s} V K coe) ᾰ
@[simp]
theorem
finset_basis_of_linear_independent_of_card_eq_finrank_repr_apply
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : finset V}
(hs : s.nonempty)
(lin_ind : linear_independent K coe)
(card_eq : s.card = finite_dimensional.finrank K V)
(ᾰ : V) :
⇑((finset_basis_of_linear_independent_of_card_eq_finrank hs lin_ind card_eq).repr) ᾰ = ⇑(lin_ind.repr) (⇑(linear_map.cod_restrict (submodule.span K (set.range coe)) linear_map.id _) ᾰ)
noncomputable
def
finset_basis_of_linear_independent_of_card_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : finset V}
(hs : s.nonempty)
(lin_ind : linear_independent K coe)
(card_eq : s.card = finite_dimensional.finrank K V) :
A linear independent finset of finrank K V vectors forms a basis.
Equations
- finset_basis_of_linear_independent_of_card_eq_finrank hs lin_ind card_eq = basis_of_linear_independent_of_card_eq_finrank lin_ind _
@[simp]
theorem
coe_finset_basis_of_linear_independent_of_card_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : finset V}
(hs : s.nonempty)
(lin_ind : linear_independent K coe)
(card_eq : s.card = finite_dimensional.finrank K V) :
⇑(finset_basis_of_linear_independent_of_card_eq_finrank hs lin_ind card_eq) = coe
noncomputable
def
set_basis_of_linear_independent_of_card_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : set V}
[nonempty ↥s]
[fintype ↥s]
(lin_ind : linear_independent K coe)
(card_eq : s.to_finset.card = finite_dimensional.finrank K V) :
A linear independent set of finrank K V vectors forms a basis.
Equations
- set_basis_of_linear_independent_of_card_eq_finrank lin_ind card_eq = basis_of_linear_independent_of_card_eq_finrank lin_ind _
@[simp]
theorem
set_basis_of_linear_independent_of_card_eq_finrank_repr_symm_apply
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : set V}
[nonempty ↥s]
[fintype ↥s]
(lin_ind : linear_independent K coe)
(card_eq : s.to_finset.card = finite_dimensional.finrank K V)
(ᾰ : ↥s →₀ K) :
⇑((set_basis_of_linear_independent_of_card_eq_finrank lin_ind card_eq).repr.symm) ᾰ = ⇑(finsupp.total ↥s V K coe) ᾰ
@[simp]
theorem
set_basis_of_linear_independent_of_card_eq_finrank_repr_apply
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : set V}
[nonempty ↥s]
[fintype ↥s]
(lin_ind : linear_independent K coe)
(card_eq : s.to_finset.card = finite_dimensional.finrank K V)
(ᾰ : V) :
⇑((set_basis_of_linear_independent_of_card_eq_finrank lin_ind card_eq).repr) ᾰ = ⇑(lin_ind.repr) (⇑(linear_map.cod_restrict (submodule.span K (set.range coe)) linear_map.id _) ᾰ)
@[simp]
theorem
coe_set_basis_of_linear_independent_of_card_eq_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{s : set V}
[nonempty ↥s]
[fintype ↥s]
(lin_ind : linear_independent K coe)
(card_eq : s.to_finset.card = finite_dimensional.finrank K V) :
⇑(set_basis_of_linear_independent_of_card_eq_finrank lin_ind card_eq) = coe
We now give characterisations of finrank K V = 1 and finrank K V ≤ 1.
theorem
finrank_eq_one
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(v : V)
(n : v ≠ 0)
(h : ∀ (w : V), ∃ (c : K), c • v = w) :
finite_dimensional.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}
[field K]
[add_comm_group V]
[module K V]
(v : V)
(h : ∀ (w : V), ∃ (c : K), c • v = w) :
finite_dimensional.finrank K V ≤ 1
If every vector is a multiple of some v : V, then V has dimension at most one.
theorem
finrank_eq_one_iff_of_nonzero
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(v : V)
(nz : v ≠ 0) :
finite_dimensional.finrank K V = 1 ↔ submodule.span K {v} = ⊤
A vector space with a nonzero vector v has dimension 1 iff v spans.
theorem
finrank_eq_one_iff_of_nonzero'
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(v : V)
(nz : v ≠ 0) :
finite_dimensional.finrank K V = 1 ↔ ∀ (w : V), ∃ (c : K), c • v = w
A module with a nonzero vector v has dimension 1 iff every vector is a multiple of v.
theorem
finrank_eq_one_iff
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(ι : Type u_1)
[unique ι] :
finite_dimensional.finrank K V = 1 ↔ nonempty (basis ι K V)
A module has dimension 1 iff there is some v : V so {v} is a basis.
A module has dimension 1 iff there is some nonzero v : V so every vector is a multiple of v.
theorem
finrank_le_one_iff
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
finite_dimensional.finrank K V ≤ 1 ↔ ∃ (v : V), ∀ (w : V), ∃ (c : K), c • v = w
A finite dimensional module has dimension at most 1 iff
there is some v : V so every vector is a multiple of v.
theorem
subalgebra.dim_eq_one_of_eq_bot
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E]
{S : subalgebra F E}
(h : S = ⊥) :
module.rank F ↥S = 1
@[simp]
theorem
subalgebra.dim_bot
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E] :
module.rank F ↥⊥ = 1
theorem
subalgebra_top_dim_eq_submodule_top_dim
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E] :
module.rank F ↥⊤ = module.rank F ↥⊤
theorem
subalgebra_top_finrank_eq_submodule_top_finrank
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E] :
theorem
subalgebra.dim_top
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E] :
module.rank F ↥⊤ = module.rank F E
@[protected, instance]
def
subalgebra.finite_dimensional_bot
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E] :
@[simp]
theorem
subalgebra.finrank_eq_one_of_eq_bot
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E]
{S : subalgebra F E}
(h : S = ⊥) :
finite_dimensional.finrank F ↥S = 1
theorem
subalgebra.eq_bot_of_finrank_one
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E]
{S : subalgebra F E}
(h : finite_dimensional.finrank F ↥S = 1) :
theorem
subalgebra.eq_bot_of_dim_one
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E]
{S : subalgebra F E}
(h : module.rank F ↥S = 1) :
@[simp]
theorem
subalgebra.bot_eq_top_of_dim_eq_one
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E]
(h : module.rank F E = 1) :
@[simp]
theorem
subalgebra.bot_eq_top_of_finrank_eq_one
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E]
(h : finite_dimensional.finrank F E = 1) :
@[simp]
theorem
subalgebra.dim_eq_one_iff
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E]
{S : subalgebra F E} :
@[simp]
theorem
subalgebra.finrank_eq_one_iff
{F : Type u_1}
{E : Type u_2}
[field F]
[field E]
[algebra F E]
{S : subalgebra F E} :
theorem
module.End.exists_ker_pow_eq_ker_pow_succ
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(f : module.End K V) :
∃ (k : ℕ), k ≤ finite_dimensional.finrank K V ∧ linear_map.ker (f ^ k) = linear_map.ker (f ^ k.succ)
theorem
module.End.ker_pow_constant
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
{f : module.End K V}
{k : ℕ}
(h : linear_map.ker (f ^ k) = linear_map.ker (f ^ k.succ))
(m : ℕ) :
linear_map.ker (f ^ k) = linear_map.ker (f ^ (k + m))
theorem
module.End.ker_pow_eq_ker_pow_finrank_of_le
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{f : module.End K V}
{m : ℕ}
(hm : finite_dimensional.finrank K V ≤ m) :
linear_map.ker (f ^ m) = linear_map.ker (f ^ finite_dimensional.finrank K V)
theorem
module.End.ker_pow_le_ker_pow_finrank
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(f : module.End K V)
(m : ℕ) :
linear_map.ker (f ^ m) ≤ linear_map.ker (f ^ finite_dimensional.finrank K V)