Library mathcomp.algebra.mxalgebra

In this file we develop the rank and row space theory of matrices, based on an extended Gaussian elimination procedure similar to LUP decomposition. This provides us with a concrete but generic model of finite dimensional vector spaces and F-algebras, in which vectors, linear functions, families, bases, subspaces, ideals and subrings are all represented using matrices. This model can be used as a foundation for the usual theory of abstract linear algebra, but it can also be used to develop directly substantial theories, such as the theory of finite group linear representation. Here we define the following concepts and notations: Gaussian_elimination A == a permuted triangular decomposition (L, U, r) of A, with L a column permutation of a lower triangular invertible matrix, U a row permutation of an upper triangular invertible matrix, and r the rank of A, all satisfying the identity L *m pid_mx r *m U = A. \rank A == the rank of A. row_free A <=> the rows of A are linearly free (i.e., the rank and height of A are equal). row_full A <=> the row-space of A spans all row-vectors (i.e., the rank and width of A are equal). col_ebase A == the extended column basis of A (the first matrix L returned by Gaussian_elimination A). row_ebase A == the extended row base of A (the second matrix U returned by Gaussian_elimination A). col_base A == a basis for the columns of A: a row-full matrix consisting of the first \rank A columns of col_ebase A. row_base A == a basis for the rows of A: a row-free matrix consisting of the first \rank A rows of row_ebase A. pinvmx A == a partial inverse for A in its row space (or on its column space, equivalently). In particular, if u is a row vector in the row_space of A, then u *m pinvmx A is the row vector of the coefficients of a decomposition of u as a sub of rows of A. kermx A == the row kernel of A : a square matrix whose row space consists of all u such that u *m A = 0 (it consists of the inverse of col_ebase A, with the top \rank A rows zeroed out). Also, kermx A is a partial right inverse to col_ebase A, in the row space anihilated by A. cokermx A == the cokernel of A : a square matrix whose column space consists of all v such that A *m v = 0 (it consists of the inverse of row_ebase A, with the leftmost \rank A columns zeroed out). maxrankfun A == injective function f so that rowsub f A is a submatrix of A with the same rank as A. fullrankfun fA == injective function f so that rowsub f A is row full, where fA is a proof of row_full A eigenvalue g a <=> a is an eigenvalue of the square matrix g. eigenspace g a == a square matrix whose row space is the eigenspace of the eigenvalue a of g (or 0 if a is not an eigenvalue). We use a different scope %MS for matrix row-space set-like operations; to avoid confusion, this scope should not be opened globally. Note that the the arguments of \rank _ and the operations below have default scope %MS. (A <= B)%MS <=> the row-space of A is included in the row-space of B. We test for this by testing if cokermx B anihilates A. (A < B)%MS <=> the row-space of A is properly included in the row-space of B. (A <= B <= C)%MS == (A <= B)%MS && (B <= C)%MS, and similarly for (A < B <= C)%MS, (A < B <= C)%MS and (A < B < C)%MS. (A == B)%MS == (A <= B <= A)%MS (A and B have the same row-space). (A :=: B)%MS == A and B behave identically wrt. \rank and <=. This triple rewrite rule is the Prop version of (A == B)%MS. Note that :=: cannot be treated as a setoid-style Equivalence because its arguments can have different types: A and B need not have the same number of rows, and often don't (e.g., in row_base A :=: A). A%MS == a square matrix with the same row-space as A; A%MS is a canonical representation of the subspace generated by A, viewed as a list of row-vectors: if (A == B)%MS, then A%MS = B%MS. (A + B)%MS == a square matrix whose row-space is the sum of the row-spaces of A and B; thus (A + B == col_mx A B)%MS. (\sum_i <expr i>)%MS == the "big" version of (_ + _)%MS; as the latter has a canonical abelian monoid structure, most generic bigop lemmas apply (the other bigop indexing notations are also defined). (A :&: B)%MS == a square matrix whose row-space is the intersection of the row-spaces of A and B. (\bigcap_i <expr i>)%MS == the "big" version of (_ :&: _)%MS, which also has a canonical abelian monoid structure. A^C%MS == a square matrix whose row-space is a complement to the the row-space of A (it consists of row_ebase A with the top \rank A rows zeroed out). (A :\: B)%MS == a square matrix whose row-space is a complement of the the row-space of (A :&: B)%MS in the row-space of A. We have (A :\: B := A :&: (capmx_gen A B)^C)%MS, where capmx_gen A B is a rectangular matrix equivalent to (A :&: B)%MS, i.e., (capmx_gen A B == A :&: B)%MS. proj_mx A B == a square matrix that projects (A + B)%MS onto A parallel to B, when (A :&: B)%MS = 0 (A and B must also be square). mxdirect S == the sum expression S is a direct sum. This is a NON EXTENSIONAL notation: the exact boolean expression is inferred from the syntactic form of S (expanding definitions, however); both (\sum(i | _) _)%MS and (_ + _)%MS sums are recognized. This construct uses a variant of the reflexive ("quote") canonical structure, mxsum_expr. The structure also recognizes sums of matrix ranks, so that lemmas concerning the rank of direct sums can be used bidirectionally. stablemx V f <=> the matrix f represents an endomorphism that preserves V := (V *m f <= V)%MS The next set of definitions let us represent F-algebras using matrices: 'A[F](m, n) == the type of matrices encoding (sub)algebras of square n x n matrices, via mxvec; as in the matrix type notation, m and F can be omitted (m defaults to n ^ 2). := 'M[F](m, n ^ 2). (A \in R)%MS <=> the square matrix A belongs to the linear set of matrices (most often, a sub-algebra) encoded by the row space of R. This is simply notation, so all the lemmas and rewrite rules for (_ <= _)%MS can apply. := (mxvec A <= R)%MS. (R * S)%MS == a square n^2 x n^2 matrix whose row-space encodes the linear set of n x n matrices generated by the pointwise product of the sets of matrices encoded by R and S. 'C(R)%MS == a square matric encoding the centraliser of the set of square matrices encoded by R. 'C_S(R)%MS := (S :&: 'C(R))%MS (the centraliser of R in S). 'Z(R)%MS == the center of R (i.e., 'C_R(R)%MS). left_mx_ideal R S <=> S is a left ideal for R (R * S <= S)%MS. right_mx_ideal R S <=> S is a right ideal for R (S * R <= S)%MS. mx_ideal R S <=> S is a bilateral ideal for R. mxring_id R e <-> e is an identity element for R (Prop predicate). has_mxring_id R <=> R has a nonzero identity element (bool predicate). mxring R <=> R encodes a nontrivial subring.

Rank and row-space theory *****************************

Decomposition with double pivoting; computes the rank, row and column images, kernels, and complements of a matrix.

The definition of the row-space operator is rigged to return the identity matrix for full matrices. To allow for further tweaks that will make the row-space intersection operator strictly commutative and monoidal, we slightly generalize some auxiliary definitions: we parametrize the "equivalent subspace and identity" choice predicate equivmx by a boolean determining whether the matrix should be the identity (so for genmx A its value is row_full A), and introduce a "quasi-identity" predicate qidmx that selects non-square full matrices along with the identity matrix 1%:M (this does not affect genmx, which chooses a square matrix). The choice witness for genmx A is either 1%:M for a row-full A, or else row_base A padded with null rows.

The setwise sum is tweaked so that 0 is a strict identity element for square matrices, because this lets us use the bigop component. As a result setwise sum is not quite strictly extensional.

The set intersection is similarly biased so that the identity matrix is a strict identity. This is somewhat more delicate than for the sum, because the test for the identity is non-extensional. This forces us to actually bias the choice operator so that it does not accidentally map an intersection of non-identity matrices to 1%:M; this would spoil associativity: if B :&: C = 1%:M but B and C are not identity, then for a square matrix A we have A :&: (B :&: C) = A != (A :&: B) :&: C in general. To complicate matters there may not be a square non-singular matrix different than 1%:M, since we could be dealing with 'M['F_2]_1. We sidestep the issue by making all non-square row-full matrices identities, and choosing a normal representative that preserves the qidmx property. Thus A :&: B = 1%:M iff A and B are both identities, and this suffices for showing that associativity is strict.

A variant of row_free_inj that exposes mulmxr, an alias for mulmx^~ but which is canonically additive