Finite dimensional vector spaces

vectType R == interface structure for finite dimensional (more precisely, detachable) vector spaces over R, which should be at least a ringType. Vector.axiom n M <-> type M is linearly isomorphic to 'rV_n. := {v2r : M -> 'rV_n| linear v2r & bijective v2r}. VectMixin isoM == packages a proof isoV of Vector.axiom n M as the vectType mixin for an n-dimensional R-space structure on a type M that is an lmodType R. VectType K M mT == packs the vectType mixin mT to into a vectType K instance for T; T should have an lmodType K canonical instance. [vectType R of T for vS] == a copy of the vS : vectType R structure where the sort is replaced by T; vS : lmodType R should be convertible to a canonical lmodType for T. [vectType R of V] == a clone of an existing vectType R structure on V. {vspace vT} == the type of (detachable) subspaces of vT; vT should have a vectType structure over a fieldType. subvs_of U == the subtype of elements of V in the subspace U. This is canonically a vectType. vsval u == linear injection of u : subvs_of U into V. vsproj U v == linear projection of v : V in subvs U. 'Hom(aT, rT) == the type of linear functions (homomorphisms) from aT to rT, where aT and rT ARE vectType structures. Elements of 'Hom(aT, rT) coerce to Coq functions. > Caveat: aT and rT must denote actual vectType structures, not their projections on Type. linfun f == a vector linear function in 'Hom(aT, rT) that coincides with f : aT -> rT when f is linear. 'End(vT) == endomorphisms of vT (:= 'Hom(vT, vT)). > The types subvs_of U, 'Hom(aT, rT), 'End(vT), K^o, 'M[K](m, n), vT * wT, {ffun I -> vT}, vT ^ n all have canonical vectType instances. Functions: < [v]>%VS == the vector space generated by v (a line if v != 0). 0%VS == the trivial vector subspace. fullv, {:vT} == the complete vector subspace (displays as fullv). (U + V)%VS == the join (sum) of two subspaces U and V. (U :&: V)%VS == intersection of vector subspaces U and V. (U^C)%VS == a complement of the vector subspace U. (U :\: V)%VS == a local complement to U :& V in the subspace U. \dim U == dimension of a vector space U. span X, X%VS == the subspace spanned by the vector sequence X. coord X i v == i'th coordinate of v on X, when v \in X%VS and where X : n.-tuple vT and i : 'I_n. Note that coord X i is a scalar function. vpick U == a nonzero element of U if U= 0%VS, or 0 if U = 0. vbasis U == a (\dim U).-tuple that is a basis of U. \1%VF == the identity linear function. (f \o g)%VF == the composite of two linear functions f and g. (f^-1)%VF == a linear function that is a right inverse to the linear function f on the codomain of f. (f @: U)%VS == the image of vs by the linear function f. (f @^-1: U)%VS == the pre-image of vs by the linear function f. lker f == the kernel of the linear function f. limg f == the image of the linear function f. fixedSpace f == the fixed space of a linear endomorphism f daddv_pi U V == projection onto U along V if U and V are disjoint; daddv_pi U V + daddv_pi V U is then a projection onto the direct sum (U + V)%VS. projv U == projection onto U (along U^C, := daddv_pi U U^C). addv_pi1 U V == projection onto the subspace U :\: V of U along V. addv_pi2 U V == projection onto V along U :\: V; note that addv_pi1 U V and addv_pi2 U V are (asymmetrical) complementary projections on (U + V)%VS. sumv_pi_for defV i == for defV : V = (V \sum(j <- r | P j) Vs j)%VS, j ranging over an eqType, this is a projection on a subspace of Vs i, along a complement in V, such that \sum(j <- r | P j) sumv_pi_for defV j is a projection onto V if filter P r is duplicate-free (e.g., when V := \sum(j | P j) Vs j). sumv_pi V i == notation the above when defV == erefl V, and V is convertible to \sum(j <- r | P j) Vs j)%VS. Predicates: v \in U == v belongs to U (:= (< [v]> <= U)%VS). (U <= V)%VS == U is a subspace of V. free B == B is a sequence of nonzero linearly independent vectors. basis_of U b == b is a basis of the subspace U. directv S == S is the expression for a direct sum of subspaces.

Finite dimension vector space

The contents of this module exposes the matrix encodings, and should therefore not be used outside of the vector library implementation.

Vspace membership is defined as line inclusion.

coord and directv are defined in the VectorTheory section.

Empty space.

Full space

Picking a non-zero vector in a subspace.

Sum of subspaces.

Intersection

Complement

Difference

Subspace dimension.

The vector direct sum theory clones the interface types of the matrix direct sum theory (see mxalgebra for the technical details), but nevetheless reuses much of the matrix theory.

Piggyback on mxalgebra theory.

Linear span generated by a list of vectors

Coordinates function; should perhaps be generalized to nat indices.

Free generator sequences.

Subspace bases