Bases #
This file defines bases in a module or vector space.
It is inspired by Isabelle/HOL's linear algebra, and hence indirectly by HOL Light.
Main definitions #
All definitions are given for families of vectors, i.e. v : ι → M
where M
is the module or
vector space and ι : Type*
is an arbitrary indexing type.
-
basis ι R M
is the type ofι
-indexedR
-bases for a moduleM
, represented by a linear equivM ≃ₗ[R] ι →₀ R
. -
the basis vectors of a basis
b : basis ι R M
are available asb i
, wherei : ι
-
basis.repr
is the isomorphism sendingx : M
to its coordinatesbasis.repr x : ι →₀ R
. The converse, turning this isomorphism into a basis, is calledbasis.of_repr
. -
If
ι
is finite, there is a variant ofrepr
calledbasis.equiv_fun b : M ≃ₗ[R] ι → R
(saving you from having to work withfinsupp
). The converse, turning this isomorphism into a basis, is calledbasis.of_equiv_fun
. -
basis.constr hv f
constructs a linear mapM₁ →ₗ[R] M₂
given the valuesf : ι → M₂
at the basis elements⇑b : ι → M₁
. -
basis.reindex
uses an equiv to map a basis to a different indexing set. -
basis.map
uses a linear equiv to map a basis to a different module.
Main statements #
-
basis.mk
: a linear independent set of vectors spanning the whole module determines a basis -
basis.ext
states that two linear maps are equal if they coincide on a basis. Similar results are available for linear equivs (if they coincide on the basis vectors), elements (if their coordinates coincide) and the functionsb.repr
and⇑b
. -
basis.of_vector_space
states that every vector space has a basis.
Implementation notes #
We use families instead of sets because it allows us to say that two identical vectors are linearly
dependent. For bases, this is useful as well because we can easily derive ordered bases by using an
ordered index type ι
.
Tags #
basis, bases
A basis ι R M
for a module M
is the type of ι
-indexed R
-bases of M
.
The basis vectors are available as coe_fn (b : basis ι R M) : ι → M
.
To turn a linear independent family of vectors spanning M
into a basis, use basis.mk
.
They are internally represented as linear equivs M ≃ₗ[R] (ι →₀ R)
,
available as basis.repr
.
Instances for basis
- basis.has_sizeof_inst
- basis.inhabited
- basis.has_coe_to_fun
- basis.empty_unique
Equations
- basis.inhabited = {default := {repr := linear_equiv.refl R (ι →₀ R) (finsupp.module ι R)}}
b i
is the i
th basis vector.
Equations
- basis.has_coe_to_fun = {coe := λ (b : basis ι R M) (i : ι), ⇑(b.repr.symm) (finsupp.single i 1)}
b.coord i
is the linear function giving the i
'th coordinate of a vector
with respect to the basis b
.
b.coord i
is an element of the dual space. In particular, for
finite-dimensional spaces it is the ι
th basis vector of the dual space.
The sum of the coordinates of an element m : M
with respect to a basis.
Equations
- b.sum_coords = (⇑(finsupp.lsum ℕ) (λ (i : ι), linear_map.id)).comp ↑(b.repr)
Two linear maps are equal if they are equal on basis vectors.
Two linear equivs are equal if they are equal on basis vectors.
An unbundled version of repr_eq_iff
Two bases are equal if their basis vectors are the same.
Apply the linear equivalence f
to the basis vectors.
If R
and R'
are isomorphic rings that act identically on a module M
,
then a basis for M
as R
-module is also a basis for M
as R'
-module.
See also basis.algebra_map_coeffs
for the case where f
is equal to algebra_map
.
Equations
- b.map_coeffs f h = let _inst : module R' R := module.comp_hom R ↑(f.symm) in {repr := (linear_equiv.restrict_scalars R' b.repr).trans (finsupp.map_range.linear_equiv (module.comp_hom.to_linear_equiv f.symm).symm)}
b.reindex (e : ι ≃ ι')
is a basis indexed by ι'
b.reindex_range
is a basis indexed by range b
, the basis vectors themselves.
Equations
- b.reindex_range = dite (nontrivial R) (λ (h : nontrivial R), let _inst : nontrivial R := h in b.reindex (equiv.of_injective ⇑b _)) (λ (h : ¬nontrivial R), let _inst : subsingleton R := _ in {repr := module.subsingleton_equiv R M ↥(set.range ⇑b) _inst_3})
b.reindex_finset_range
is a basis indexed by finset.univ.image b
,
the finite set of basis vectors themselves.
Equations
- b.reindex_finset_range = b.reindex_range.reindex ((equiv.refl M).subtype_equiv _)
Construct a linear map given the value at the basis.
This definition is parameterized over an extra semiring S
,
such that smul_comm_class R S M'
holds.
If R
is commutative, you can set S := R
; if R
is not commutative,
you can recover an add_equiv
by setting S := ℕ
.
See library note [bundled maps over different rings].
If b
is a basis for M
and b'
a basis for M'
, and the index types are equivalent,
b.equiv b' e
is a linear equivalence M ≃ₗ[R] M'
, mapping b i
to b' (e i)
.
basis.prod
maps a ι
-indexed basis for M
and a ι'
-indexed basis for M'
to a ι ⊕ ι'
-index basis for M × M'
.
For the specific case of R × R
, see also basis.fin_two_prod
.
basis.singleton ι R
is the basis sending the unique element of ι
to 1 : R
.
Equations
- basis.singleton ι R = {repr := {to_fun := λ (x : R), finsupp.single inhabited.default x, map_add' := _, map_smul' := _, inv_fun := λ (f : ι →₀ R), ⇑f inhabited.default, left_inv := _, right_inv := _}}
If M
is a subsingleton and ι
is empty, this is the unique ι
-indexed basis for M
.
Equations
- basis.empty M = {repr := 0}
Equations
- basis.empty_unique M = {to_inhabited := {default := basis.empty M _inst_7}, uniq := _}
A module over R
with a finite basis is linearly equivalent to functions from its basis to R
.
A module over a finite ring that admits a finite basis is finite.
Equations
- module.fintype_of_fintype b = fintype.of_equiv (ι → R) b.equiv_fun.to_equiv.symm
Given a basis v
indexed by ι
, the canonical linear equivalence between ι → R
and M
maps
a function x : ι → R
to the linear combination ∑_i x i • v i
.
Define a basis by mapping each vector x : M
to its coordinates e x : ι → R
,
as long as ι
is finite.
Equations
- basis.of_equiv_fun e = {repr := e.trans (finsupp.linear_equiv_fun_on_fintype R R ι).symm}
If b
is a basis for M
and b'
a basis for M'
,
and f
, g
form a bijection between the basis vectors,
b.equiv' b' f g hf hg hgf hfg
is a linear equivalence M ≃ₗ[R] M'
, mapping b i
to f (b i)
.
Any basis is a maximal linear independent set.
A linear independent family of vectors spanning the whole module is a basis.
Equations
- basis.mk hli hsp = {repr := {to_fun := (hli.repr.comp (linear_map.cod_restrict (submodule.span R (set.range v)) linear_map.id _)).to_fun, map_add' := _, map_smul' := _, inv_fun := ⇑(finsupp.total ι M R v), left_inv := _, right_inv := _}}
Given a basis, the i
th element of the dual basis evaluates to 1 on the i
th element of the
basis.
Given a basis, the i
th element of the dual basis evaluates to 0 on the j
th element of the
basis if j ≠ i
.
Given a basis, the i
th element of the dual basis evaluates to the Kronecker delta on the
j
th element of the basis.
A linear independent family of vectors is a basis for their span.
Equations
- basis.span hli = basis.mk _ basis.span._proof_3
Given a basis v
and a map w
such that for all i
, w i
are elements of a group,
group_smul
provides the basis corresponding to w • v
.
Equations
- v.group_smul w = basis.mk _ _
Given a basis v
and a map w
such that for all i
, w i
is a unit, smul_of_is_unit
provides the basis corresponding to w • v
.
Equations
- v.units_smul w = basis.mk _ _
A version of smul_of_units
that uses is_unit
.
Equations
- v.is_unit_smul hw = v.units_smul (λ (i : ι), _.unit)
Let b
be a basis for a submodule N
of M
. If y : M
is linear independent of N
and y
and N
together span the whole of M
, then there is a basis for M
whose basis vectors are given by fin.cons y b
.
Equations
- basis.mk_fin_cons y b hli hsp = have span_b : submodule.span R (set.range (⇑(N.subtype) ∘ ⇑b)) = N, from _, basis.mk _ _
Let b
be a basis for a submodule N ≤ O
. If y ∈ O
is linear independent of N
and y
and N
together span the whole of O
, then there is a basis for O
whose basis vectors are given by fin.cons y b
.
Equations
- basis.mk_fin_cons_of_le y yO b hNO hli hsp = basis.mk_fin_cons ⟨y, yO⟩ (b.map (submodule.comap_subtype_equiv_of_le hNO).symm) _ _
The basis of R × R
given by the two vectors (1, 0)
and (0, 1)
.
Equations
If N
is a submodule with finite rank, do induction on adjoining a linear independent
element to a submodule.
Equations
- submodule.induction_on_rank_aux b P ih n N rank_le = nat.rec (λ (N : submodule R M) (rank_le : ∀ {m : ℕ} (v : fin m → ↥N), linear_independent R (coe ∘ v) → m ≤ 0), _.mpr (ih ⊥ (λ (N : submodule R M) (N_le : N ≤ ⊥) (x : M) (x_mem : x ∈ ⊥) (x_ortho : ∀ (c : R) (y : M), y ∈ N → c • x + y = 0 → c = 0), false.rec (P N) _))) (λ (n : ℕ) (rank_ih : Π (N : submodule R M), (∀ {m : ℕ} (v : fin m → ↥N), linear_independent R (coe ∘ v) → m ≤ n) → P N) (N : submodule R M) (rank_le : ∀ {m : ℕ} (v : fin m → ↥N), linear_independent R (coe ∘ v) → m ≤ n.succ), ih N (λ (N' : submodule R M) (N'_le : N' ≤ N) (x : M) (x_mem : x ∈ N) (x_ortho : ∀ (c : R) (y : M), y ∈ N' → c • x + y = 0 → c = 0), rank_ih N' _)) n N rank_le
If s
is a linear independent set of vectors, we can extend it to a basis.
Equations
- basis.extend hs = basis.mk _ _
If v
is a linear independent family of vectors, extend it to a basis indexed by a sum type.
Equations
- basis.sum_extend hs = let s : set V := set.range v, e : ι ≃ ↥s := equiv.of_injective v _, b : set V := _.extend basis.sum_extend._proof_5 in (basis.extend _).reindex ((e.sum_congr (equiv.refl ↥(b \ s))).trans (equiv.set.sum_diff_subset _ (λ (a : V), classical.prop_decidable ((λ (_x : V), _x ∈ s) a)))).symm
A set used to index basis.of_vector_space
.
Equations
- basis.of_vector_space_index K V = _.extend _
Instances for ↥basis.of_vector_space_index
Each vector space has a basis.
Equations
For a module over a division ring, the span of a nonzero element is an atom of the lattice of submodules.
The atoms of the lattice of submodules of a module over a division ring are the submodules equal to the span of a nonzero element of the module.
The lattice of submodules of a module over a division ring is atomistic.
Any linear map f : p →ₗ[K] V'
defined on a subspace p
can be extended to the whole
space.
If p < ⊤
is a subspace of a vector space V
, then there exists a nonzero linear map
f : V →ₗ[K] K
such that p ≤ ker f
.