+ +

Library mathcomp.algebra.mxalgebra

+ +

+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+

+ +

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

+ +
+Set Implicit Arguments.
+ +
+Import GroupScope.
+Import GRing.Theory.
+Local Open Scope ring_scope.
+ +
+Reserved Notation "\rank A" (at level 10, A at level 8, format "\rank A").
+Reserved Notation "A ^C" (at level 8, format "A ^C").
+ +
+Notation "''A_' ( m , n )" := 'M_(m, n ^ 2)
+  (at level 8, format "''A_' ( m , n )") : type_scope.
+ +
+Notation "''A_' ( n )" := 'A_(n ^ 2, n)
+  (at level 8, only parsing) : type_scope.
+ +
+Notation "''A_' n" := 'A_(n)
+  (at level 8, n at next level, format "''A_' n") : type_scope.
+ +
+Notation "''A' [ F ]_ ( m , n )" := 'M [F]_(m, n ^ 2)
+  (at level 8, only parsing) : type_scope.
+ +
+Notation "''A' [ F ]_ ( n )" := 'A [F]_(n ^ 2, n)
+  (at level 8, only parsing) : type_scope.
+ +
+Notation "''A' [ F ]_ n" := 'A [F]_(n)
+  (at level 8, n at level 2, only parsing) : type_scope.
+ +
+Delimit Scope matrix_set_scope with MS.
+ +
+ +
+

+ +

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

+ +
+Section RowSpaceTheory.
+ +
+Variable F : fieldType.
+Implicit Types m n p r : nat.
+ +
+ +
+

+ +

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

+ +
+Fixpoint Gaussian_elimination {m n} : 'M_(m , n ) → 'M_m × 'M_n × nat :=
+ match m, n with
+ | _.+1, _.+1 ⇒ fun A : 'M_(1 + _, 1 + _) ⇒
+ if [pick ij | A ij .1 ij .2 != 0] is Some (i, j) then
+ let a := A i j in let A1 := xrow i 0 (xcol j 0 A) in
+ let u := ursubmx A1 in let v := a ^-1 *: dlsubmx A1 in
+ let: (L, U, r) := Gaussian_elimination (drsubmx A1 - v ×m u) in
+ (xrow i 0 (block_mx 1 0 v L), xcol j 0 (block_mx a %:M u 0 U), r.+1 )
+ else (1%:M , 1%:M , 0%N)
+ | _, _ ⇒ fun _ ⇒ (1%:M , 1%:M , 0%N)
+ end.
+ +
+Section Defs.
+ +
+Variables (m n : nat) (A : 'M_(m , n )).
+ +
+Fact Gaussian_elimination_key : unit.
+ +
+Let LUr := locked_with Gaussian_elimination_key (@Gaussian_elimination) m n A.
+ +
+Definition col_ebase := LUr .1.1.
+Definition row_ebase := LUr .1 .2.
+Definition mxrank := if [|| m == 0 | n == 0]%N then 0%N else LUr .2.
+ +
+Definition row_free := mxrank == m.
+Definition row_full := mxrank == n.
+ +
+Definition row_base : 'M_(mxrank , n ) := pid_mx mxrank ×m row_ebase.
+Definition col_base : 'M_(m , mxrank ) := col_ebase ×m pid_mx mxrank.
+ +
+Definition complmx : 'M_n := copid_mx mxrank ×m row_ebase.
+Definition kermx : 'M_m := copid_mx mxrank ×m invmx col_ebase.
+Definition cokermx : 'M_n := invmx row_ebase ×m copid_mx mxrank.
+ +
+Definition pinvmx : 'M_(n , m ) :=
+ invmx row_ebase ×m pid_mx mxrank ×m invmx col_ebase.
+ +
+End Defs.
+ +
+ +
+Definition submx_def := idfun (fun m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) ⇒
+ A ×m cokermx B == 0).
+Fact submx_key : unit.
+Definition submx := locked_with submx_key submx_def.
+Canonical submx_unlockable := [unlockable fun submx ].
+ +
+ +
+Definition ltmx m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :=
+ (A ≤ B)%MS && ~~ (B ≤ A)%MS.
+ +
+Definition eqmx m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :=
+ prod (\rank A = \rank B)
+ (∀ m3 (C : 'M_(m3 , n )),
+ ((A ≤ C ) = (B ≤ C )) × ((C ≤ A ) = (C ≤ B )))%MS.
+ +
+Section LtmxIdentities.
+ +
+Variables (m1 m2 n : nat) (A : 'M_(m1 , n )) (B : 'M_(m2 , n )).
+ +
+Lemma ltmxE : (A < B)%MS = ((A ≤ B)%MS && ~~ (B ≤ A)%MS).
+ +
+Lemma ltmxW : (A < B)%MS → (A ≤ B)%MS.
+ +
+Lemma ltmxEneq : (A < B)%MS = (A ≤ B)%MS && ~~ (A == B)%MS.
+ +
+Lemma submxElt : (A ≤ B)%MS = (A == B)%MS || (A < B)%MS.
+ +
+End LtmxIdentities.
+ +
+

+ +

+ 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. +

+Let qidmx m n (A : 'M_(m , n )) :=
+  if m == n then A == pid_mx n else row_full A.
+Let equivmx m n (A : 'M_(m , n )) idA (B : 'M_n) :=
+  (B == A)%MS && (qidmx B == idA ).
+Let equivmx_spec m n (A : 'M_(m , n )) idA (B : 'M_n) :=
+  prod (B :=: A)%MS (qidmx B = idA).
+Definition genmx_witness m n (A : 'M_(m , n )) : 'M_n :=
+  if row_full A then 1%:M else pid_mx (\rank A) ×m row_ebase A.
+Definition genmx_def := idfun (fun m n (A : 'M_(m , n )) ⇒
+   choose (equivmx A (row_full A)) (genmx_witness A) : 'M_n).
+Fact genmx_key : unit.
+Definition genmx := locked_with genmx_key genmx_def.
+Canonical genmx_unlockable := [unlockable fun genmx ].
+ +
+

+ +

+ 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. +

+Let addsmx_nop m n (A : 'M_(m , n )) := conform_mx <<A >>%MS A.
+Definition addsmx_def := idfun (fun m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) ⇒
+ if A == 0 then addsmx_nop B else if B == 0 then addsmx_nop A else
+ <<col_mx A B >>%MS : 'M_n).
+Fact addsmx_key : unit.
+Definition addsmx := locked_with addsmx_key addsmx_def.
+Canonical addsmx_unlockable := [unlockable fun addsmx ].
+ +
+

+ +

+ 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. +

+Let capmx_witness m n (A : 'M_(m , n )) :=
+ if row_full A then conform_mx 1%:M A else <<A >>%MS.
+Let capmx_norm m n (A : 'M_(m , n )) :=
+ choose (equivmx A (qidmx A)) (capmx_witness A).
+Let capmx_nop m n (A : 'M_(m , n )) := conform_mx (capmx_norm A) A.
+Definition capmx_gen m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :=
+ lsubmx (kermx (col_mx A B)) ×m A.
+Definition capmx_def := idfun (fun m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) ⇒
+ if qidmx A then capmx_nop B else
+ if qidmx B then capmx_nop A else
+ if row_full B then capmx_norm A else capmx_norm (capmx_gen A B) : 'M_n).
+Fact capmx_key : unit.
+Definition capmx := locked_with capmx_key capmx_def.
+Canonical capmx_unlockable := [unlockable fun capmx ].
+ +
+Definition diffmx_def := idfun (fun m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) ⇒
+ <<capmx_gen A (capmx_gen A B )^C >>%MS : 'M_n).
+Fact diffmx_key : unit.
+Definition diffmx := locked_with diffmx_key diffmx_def.
+Canonical diffmx_unlockable := [unlockable fun diffmx ].
+ +
+Definition proj_mx n (U V : 'M_n) : 'M_n := pinvmx (col_mx U V) ×m col_mx U 0.
+ +
+ +
+Fact mxrankE m n (A : 'M_(m , n )) : \rank A = (GaussE A ).2.
+ +
+Lemma rank_leq_row m n (A : 'M_(m , n )) : \rank A ≤ m.
+ +
+Lemma row_leq_rank m n (A : 'M_(m , n )) : (m ≤ \rank A ) = row_free A.
+ +
+Lemma rank_leq_col m n (A : 'M_(m , n )) : \rank A ≤ n.
+ +
+Lemma col_leq_rank m n (A : 'M_(m , n )) : (n ≤ \rank A ) = row_full A.
+ +
+Let unitmx1F := @unitmx1 F.
+Lemma row_ebase_unit m n (A : 'M_(m , n )) : row_ebase A \in unitmx.
+ +
+Lemma col_ebase_unit m n (A : 'M_(m , n )) : col_ebase A \in unitmx.
+Hint Resolve rank_leq_row rank_leq_col row_ebase_unit col_ebase_unit.
+ +
+Lemma mulmx_ebase m n (A : 'M_(m , n )) :
+ col_ebase A ×m pid_mx (\rank A) ×m row_ebase A = A.
+ +
+Lemma mulmx_base m n (A : 'M_(m , n )) : col_base A ×m row_base A = A.
+ +
+Lemma mulmx1_min_rank r m n (A : 'M_(m , n )) M N :
+ M ×m A ×m N = 1%:M :> 'M_r → r ≤ \rank A.
+ +
+Lemma mulmx_max_rank r m n (M : 'M_(m , r )) (N : 'M_(r , n )) :
+ \rank (M ×m N ) ≤ r.
+ +
+Lemma mxrank_tr m n (A : 'M_(m , n )) : \rank A ^T = \rank A.
+ +
+Lemma mxrank_add m n (A B : 'M_(m , n )) : \rank (A + B)%R ≤ \rank A + \rank B.
+ +
+Lemma mxrankM_maxl m n p (A : 'M_(m , n )) (B : 'M_(n , p )) :
+ \rank (A ×m B ) ≤ \rank A.
+ +
+Lemma mxrankM_maxr m n p (A : 'M_(m , n )) (B : 'M_(n , p )) :
+ \rank (A ×m B ) ≤ \rank B.
+ +
+Lemma mxrank_scale m n a (A : 'M_(m , n )) : \rank (a *: A ) ≤ \rank A.
+ +
+Lemma mxrank_scale_nz m n a (A : 'M_(m , n )) :
+ a != 0 → \rank (a *: A ) = \rank A.
+ +
+Lemma mxrank_opp m n (A : 'M_(m , n )) : \rank (- A ) = \rank A.
+ +
+Lemma mxrank0 m n : \rank (0 : 'M_(m , n )) = 0%N.
+ +
+Lemma mxrank_eq0 m n (A : 'M_(m , n )) : (\rank A == 0%N) = (A == 0).
+ +
+Lemma mulmx_coker m n (A : 'M_(m , n )) : A ×m cokermx A = 0.
+ +
+Lemma submxE m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A ≤ B)%MS = (A ×m cokermx B == 0).
+ +
+Lemma mulmxKpV m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A ≤ B)%MS → A ×m pinvmx B ×m B = A.
+ +
+Lemma submxP m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ reflect (∃ D, A = D ×m B) (A ≤ B)%MS.
+ +
+Lemma submx_refl m n (A : 'M_(m , n )) : (A ≤ A)%MS.
+ Hint Resolve submx_refl.
+ +
+Lemma submxMl m n p (D : 'M_(m , n )) (A : 'M_(n , p )) : (D ×m A ≤ A)%MS.
+ +
+Lemma submxMr m1 m2 n p (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(n , p )) :
+ (A ≤ B)%MS → (A ×m C ≤ B ×m C)%MS.
+ +
+Lemma mulmx_sub m n1 n2 p (C : 'M_(m , n1 )) A (B : 'M_(n2 , p )) :
+ (A ≤ B → C ×m A ≤ B)%MS.
+ +
+Lemma submx_trans m1 m2 m3 n
+ (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(m3 , n )) :
+ (A ≤ B → B ≤ C → A ≤ C)%MS.
+ +
+Lemma ltmx_sub_trans m1 m2 m3 n
+ (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(m3 , n )) :
+ (A < B)%MS → (B ≤ C)%MS → (A < C)%MS.
+ +
+Lemma sub_ltmx_trans m1 m2 m3 n
+ (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(m3 , n )) :
+ (A ≤ B)%MS → (B < C)%MS → (A < C)%MS.
+ +
+Lemma ltmx_trans m n : transitive (@ltmx m m n).
+ +
+Lemma ltmx_irrefl m n : irreflexive (@ltmx m m n).
+ +
+Lemma sub0mx m1 m2 n (A : 'M_(m2 , n )) : ((0 : 'M_(m1 , n )) ≤ A)%MS.
+ +
+Lemma submx0null m1 m2 n (A : 'M [F ]_(m1 , n )) :
+ (A ≤ (0 : 'M_(m2 , n )))%MS → A = 0.
+ +
+Lemma submx0 m n (A : 'M_(m , n )) : (A ≤ (0 : 'M_n ))%MS = (A == 0).
+ +
+Lemma lt0mx m n (A : 'M_(m , n )) : ((0 : 'M_n ) < A)%MS = (A != 0).
+ +
+Lemma ltmx0 m n (A : 'M [F ]_(m , n )) : (A < (0 : 'M_n ))%MS = false.
+ +
+Lemma eqmx0P m n (A : 'M_(m , n )) : reflect (A = 0) (A == (0 : 'M_n ))%MS.
+ +
+Lemma eqmx_eq0 m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A :=: B)%MS → (A == 0) = (B == 0).
+ +
+Lemma addmx_sub m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m1 , n )) (C : 'M_(m2 , n )) :
+ (A ≤ C)%MS → (B ≤ C)%MS → ((A + B)%R ≤ C)%MS.
+ +
+Lemma summx_sub m1 m2 n (B : 'M_(m2 , n ))
+ I (r : seq I) (P : pred I) (A_ : I → 'M_(m1 , n )) :
+ (∀ i, P i → A_ i ≤ B)%MS → ((\sum_(i <- r | P i ) A_ i)%R ≤ B)%MS.
+ +
+Lemma scalemx_sub m1 m2 n a (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A ≤ B)%MS → (a *: A ≤ B)%MS.
+ +
+Lemma row_sub m n i (A : 'M_(m , n )) : (row i A ≤ A)%MS.
+ +
+Lemma eq_row_sub m n v (A : 'M_(m , n )) i : row i A = v → (v ≤ A)%MS.
+ +
+Lemma nz_row_sub m n (A : 'M_(m , n )) : (nz_row A ≤ A)%MS.
+ +
+Lemma row_subP m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ reflect (∀ i, row i A ≤ B)%MS (A ≤ B)%MS.
+ +
+Lemma rV_subP m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ reflect (∀ v : 'rV_n, v ≤ A → v ≤ B)%MS (A ≤ B)%MS.
+ +
+Lemma row_subPn m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ reflect (∃ i, ~~ (row i A ≤ B)%MS) (~~ (A ≤ B)%MS).
+ +
+Lemma sub_rVP n (u v : 'rV_n) : reflect (∃ a, u = a *: v) (u ≤ v)%MS.
+ +
+Lemma rank_rV n (v : 'rV_n) : \rank v = (v != 0).
+ +
+Lemma rowV0Pn m n (A : 'M_(m , n )) :
+ reflect (exists2 v : 'rV_n , v ≤ A & v != 0)%MS (A != 0).
+ +
+Lemma rowV0P m n (A : 'M_(m , n )) :
+ reflect (∀ v : 'rV_n, v ≤ A → v = 0)%MS (A == 0).
+ +
+Lemma submx_full m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ row_full B → (A ≤ B)%MS.
+ +
+Lemma row_fullP m n (A : 'M_(m , n )) :
+ reflect (∃ B, B ×m A = 1%:M) (row_full A).
+ +
+Lemma row_full_inj m n p A : row_full A → injective (@mulmx _ m n p A).
+ +
+Lemma row_freeP m n (A : 'M_(m , n )) :
+ reflect (∃ B, A ×m B = 1%:M) (row_free A).
+ +
+Lemma row_free_inj m n p A : row_free A → injective ((@mulmx _ m n p )^~ A).
+ +
+Lemma row_free_unit n (A : 'M_n) : row_free A = (A \in unitmx ).
+ +
+Lemma row_full_unit n (A : 'M_n) : row_full A = (A \in unitmx ).
+ +
+Lemma mxrank_unit n (A : 'M_n) : A \in unitmx → \rank A = n.
+ +
+Lemma mxrank1 n : \rank (1%:M : 'M_n ) = n.
+ +
+Lemma mxrank_delta m n i j : \rank (delta_mx i j : 'M_(m , n )) = 1%N.
+ +
+Lemma mxrankS m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A ≤ B)%MS → \rank A ≤ \rank B.
+ +
+Lemma submx1 m n (A : 'M_(m , n )) : (A ≤ 1%:M)%MS.
+ +
+Lemma sub1mx m n (A : 'M_(m , n )) : (1%:M ≤ A)%MS = row_full A.
+ +
+Lemma ltmx1 m n (A : 'M_(m , n )) : (A < 1%:M)%MS = ~~ row_full A.
+ +
+Lemma lt1mx m n (A : 'M_(m , n )) : (1%:M < A)%MS = false.
+ +
+Lemma eqmxP m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ reflect (A :=: B)%MS (A == B)%MS.
+ +
+Lemma rV_eqP m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ reflect (∀ u : 'rV_n, (u ≤ A ) = (u ≤ B ))%MS (A == B)%MS.
+ +
+Lemma eqmx_refl m1 n (A : 'M_(m1 , n )) : (A :=: A)%MS.
+ +
+Lemma eqmx_sym m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A :=: B)%MS → (B :=: A)%MS.
+ +
+Lemma eqmx_trans m1 m2 m3 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(m3 , n )) :
+ (A :=: B)%MS → (B :=: C)%MS → (A :=: C)%MS.
+ +
+Lemma eqmx_rank m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A == B)%MS → \rank A = \rank B.
+ +
+Lemma lt_eqmx m1 m2 m3 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A :=: B)%MS →
+ ∀ C : 'M_(m3 , n ), (((A < C ) = (B < C ))%MS × ((C < A ) = (C < B ))%MS)%type.
+ +
+Lemma eqmxMr m1 m2 n p (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(n , p )) :
+ (A :=: B)%MS → (A ×m C :=: B ×m C)%MS.
+ +
+Lemma eqmxMfull m n p (A : 'M_(m , n )) (B : 'M_(n , p )) :
+ row_full A → (A ×m B :=: B)%MS.
+ +
+Lemma eqmx0 m n : ((0 : 'M [F ]_(m , n )) :=: (0 : 'M_n ))%MS.
+ +
+Lemma eqmx_scale m n a (A : 'M_(m , n )) : a != 0 → (a *: A :=: A)%MS.
+ +
+Lemma eqmx_opp m n (A : 'M_(m , n )) : (- A :=: A)%MS.
+ +
+Lemma submxMfree m1 m2 n p (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(n , p )) :
+ row_free C → (A ×m C ≤ B ×m C)%MS = (A ≤ B)%MS.
+ +
+Lemma eqmxMfree m1 m2 n p (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(n , p )) :
+ row_free C → (A ×m C :=: B ×m C)%MS → (A :=: B)%MS.
+ +
+Lemma mxrankMfree m n p (A : 'M_(m , n )) (B : 'M_(n , p )) :
+ row_free B → \rank (A ×m B ) = \rank A.
+ +
+Lemma eq_row_base m n (A : 'M_(m , n )) : (row_base A :=: A)%MS.
+ +
+Let qidmx_eq1 n (A : 'M_n) : qidmx A = (A == 1%:M ).
+ +
+Let genmx_witnessP m n (A : 'M_(m , n )) :
+ equivmx A (row_full A) (genmx_witness A).
+ +
+Lemma genmxE m n (A : 'M_(m , n )) : (<<A >> :=: A)%MS.
+ +
+Lemma eq_genmx m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A :=: B → <<A >> = <>)%MS.
+ +
+Lemma genmxP m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ reflect (<<A >> = <>)%MS (A == B)%MS.
+ +
+Lemma genmx0 m n : <<0 : 'M_(m , n )>>%MS = 0.
+ +
+Lemma genmx1 n : <<1%:M : 'M_n >>%MS = 1%:M.
+ +
+Lemma genmx_id m n (A : 'M_(m , n )) : (<<<<A >>>> = <<A >>)%MS.
+ +
+Lemma row_base_free m n (A : 'M_(m , n )) : row_free (row_base A).
+ +
+Lemma mxrank_gen m n (A : 'M_(m , n )) : \rank <<A >> = \rank A.
+ +
+Lemma col_base_full m n (A : 'M_(m , n )) : row_full (col_base A).
+Hint Resolve row_base_free col_base_full.
+ +
+Lemma mxrank_leqif_sup m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A ≤ B)%MS → \rank A ≤ \rank B ?= iff (B ≤ A)%MS.
+ +
+Lemma mxrank_leqif_eq m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A ≤ B)%MS → \rank A ≤ \rank B ?= iff (A == B)%MS.
+ +
+Lemma ltmxErank m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A < B)%MS = (A ≤ B)%MS && (\rank A < \rank B ).
+ +
+Lemma rank_ltmx m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A < B)%MS → \rank A < \rank B.
+ +
+Lemma eqmx_cast m1 m2 n (A : 'M_(m1 , n )) e :
+ ((castmx e A : 'M_(m2 , n )) :=: A)%MS.
+ +
+Lemma eqmx_conform m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (conform_mx A B :=: A ∨ conform_mx A B :=: B)%MS.
+ +
+Let eqmx_sum_nop m n (A : 'M_(m , n )) : (addsmx_nop A :=: A)%MS.
+ +
+Section AddsmxSub.
+ +
+Variable (m1 m2 n : nat) (A : 'M [F ]_(m1 , n )) (B : 'M [F ]_(m2 , n )).
+ +
+Lemma col_mx_sub m3 (C : 'M_(m3 , n )) :
+ (col_mx A B ≤ C)%MS = (A ≤ C)%MS && (B ≤ C)%MS.
+ +
+Lemma addsmxE : (A + B :=: col_mx A B)%MS.
+ +
+Lemma addsmx_sub m3 (C : 'M_(m3 , n )) :
+ (A + B ≤ C)%MS = (A ≤ C)%MS && (B ≤ C)%MS.
+ +
+Lemma addsmxSl : (A ≤ A + B)%MS.
+ +
+Lemma addsmxSr : (B ≤ A + B)%MS.
+ +
+Lemma addsmx_idPr : reflect (A + B :=: B)%MS (A ≤ B)%MS.
+ +
+Lemma addsmx_idPl : reflect (A + B :=: A)%MS (B ≤ A)%MS.
+ +
+End AddsmxSub.
+ +
+Lemma adds0mx m1 m2 n (B : 'M_(m2 , n )) : ((0 : 'M_(m1 , n )) + B :=: B)%MS.
+ +
+Lemma addsmx0 m1 m2 n (A : 'M_(m1 , n )) : (A + (0 : 'M_(m2 , n )) :=: A)%MS.
+ +
+Let addsmx_nop_eq0 m n (A : 'M_(m , n )) : (addsmx_nop A == 0) = (A == 0).
+ +
+Let addsmx_nop0 m n : addsmx_nop (0 : 'M_(m , n )) = 0.
+ +
+Let addsmx_nop_id n (A : 'M_n) : addsmx_nop A = A.
+ +
+Lemma addsmxC m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) : (A + B = B + A)%MS.
+ +
+Lemma adds0mx_id m1 n (B : 'M_n) : ((0 : 'M_(m1 , n )) + B)%MS = B.
+ +
+Lemma addsmx0_id m2 n (A : 'M_n) : (A + (0 : 'M_(m2 , n )))%MS = A.
+ +
+Lemma addsmxA m1 m2 m3 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(m3 , n )) :
+ (A + (B + C ) = A + B + C)%MS.
+ +
+Canonical addsmx_monoid n :=
+ Monoid.Law (@addsmxA n n n n) (@adds0mx_id n n) (@addsmx0_id n n).
+Canonical addsmx_comoid n := Monoid.ComLaw (@addsmxC n n n).
+ +
+Lemma addsmxMr m1 m2 n p (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(n , p )) :
+ ((A + B)%MS ×m C :=: A ×m C + B ×m C)%MS.
+ +
+Lemma addsmxS m1 m2 m3 m4 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n ))
+ (C : 'M_(m3 , n )) (D : 'M_(m4 , n )) :
+ (A ≤ C → B ≤ D → A + B ≤ C + D)%MS.
+ +
+Lemma addmx_sub_adds m m1 m2 n (A : 'M_(m , n )) (B : 'M_(m , n ))
+ (C : 'M_(m1 , n )) (D : 'M_(m2 , n )) :
+ (A ≤ C → B ≤ D → (A + B)%R ≤ C + D)%MS.
+ +
+Lemma addsmx_addKl n m1 m2 (A : 'M_(m1 , n )) (B C : 'M_(m2 , n )) :
+ (B ≤ A)%MS → (A + (B + C)%R :=: A + C)%MS.
+ +
+Lemma addsmx_addKr n m1 m2 (A B : 'M_(m1 , n )) (C : 'M_(m2 , n )) :
+ (B ≤ C)%MS → ((A + B)%R + C :=: A + C)%MS.
+ +
+Lemma adds_eqmx m1 m2 m3 m4 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n ))
+ (C : 'M_(m3 , n )) (D : 'M_(m4 , n )) :
+ (A :=: C → B :=: D → A + B :=: C + D)%MS.
+ +
+Lemma genmx_adds m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (<<(A + B)%MS>> = <<A >> + <>)%MS.
+ +
+Lemma sub_addsmxP m1 m2 m3 n
+ (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(m3 , n )) :
+ reflect (∃ u, A = u .1 ×m B + u .2 ×m C) (A ≤ B + C)%MS.
+ +
+Variable I : finType.
+Implicit Type P : pred I.
+ +
+Lemma genmx_sums P n (B_ : I → 'M_n) :
+ <<(\sum_(i | P i ) B_ i)%MS>>%MS = (\sum_(i | P i ) <<B_ i >>)%MS.
+ +
+Lemma sumsmx_sup i0 P m n (A : 'M_(m , n )) (B_ : I → 'M_n) :
+ P i0 → (A ≤ B_ i0)%MS → (A ≤ \sum_(i | P i ) B_ i)%MS.
+ +
+Lemma sumsmx_subP P m n (A_ : I → 'M_n) (B : 'M_(m , n )) :
+ reflect (∀ i, P i → A_ i ≤ B)%MS (\sum_(i | P i ) A_ i ≤ B)%MS.
+ +
+Lemma summx_sub_sums P m n (A : I → 'M [F ]_(m , n )) B :
+ (∀ i, P i → A i ≤ B i)%MS →
+ ((\sum_(i | P i ) A i)%R ≤ \sum_(i | P i ) B i)%MS.
+ +
+Lemma sumsmxS P n (A B : I → 'M [F ]_n) :
+ (∀ i, P i → A i ≤ B i)%MS →
+ (\sum_(i | P i ) A i ≤ \sum_(i | P i ) B i)%MS.
+ +
+Lemma eqmx_sums P n (A B : I → 'M [F ]_n) :
+ (∀ i, P i → A i :=: B i)%MS →
+ (\sum_(i | P i ) A i :=: \sum_(i | P i ) B i)%MS.
+ +
+Lemma sub_sumsmxP P m n (A : 'M_(m , n )) (B_ : I → 'M_n) :
+ reflect (∃ u_, A = \sum_(i | P i ) u_ i ×m B_ i)
+ (A ≤ \sum_(i | P i ) B_ i)%MS.
+ +
+Lemma sumsmxMr_gen P m n A (B : 'M [F ]_(m , n )) :
+ ((\sum_(i | P i ) A i)%MS ×m B :=: \sum_(i | P i ) <<A i ×m B >>)%MS.
+ +
+Lemma sumsmxMr P n (A_ : I → 'M [F ]_n) (B : 'M_n) :
+ ((\sum_(i | P i ) A_ i)%MS ×m B :=: \sum_(i | P i ) (A_ i ×m B ))%MS.
+ +
+Lemma rank_pid_mx m n r : r ≤ m → r ≤ n → \rank (pid_mx r : 'M_(m , n )) = r.
+ +
+Lemma rank_copid_mx n r : r ≤ n → \rank (copid_mx r : 'M_n ) = (n - r)%N.
+ +
+Lemma mxrank_compl m n (A : 'M_(m , n )) : \rank A ^C = (n - \rank A)%N.
+ +
+Lemma mxrank_ker m n (A : 'M_(m , n )) : \rank (kermx A ) = (m - \rank A)%N.
+ +
+Lemma kermx_eq0 n m (A : 'M_(m , n )) : (kermx A == 0) = row_free A.
+ +
+Lemma mxrank_coker m n (A : 'M_(m , n )) : \rank (cokermx A ) = (n - \rank A)%N.
+ +
+Lemma cokermx_eq0 n m (A : 'M_(m , n )) : (cokermx A == 0) = row_full A.
+ +
+Lemma mulmx_ker m n (A : 'M_(m , n )) : kermx A ×m A = 0.
+ +
+Lemma mulmxKV_ker m n p (A : 'M_(n , p )) (B : 'M_(m , n )) :
+ B ×m A = 0 → B ×m col_ebase A ×m kermx A = B.
+ +
+Lemma sub_kermxP p m n (A : 'M_(m , n )) (B : 'M_(p , m )) :
+ reflect (B ×m A = 0) (B ≤ kermx A)%MS.
+ +
+Lemma mulmx0_rank_max m n p (A : 'M_(m , n )) (B : 'M_(n , p )) :
+ A ×m B = 0 → \rank A + \rank B ≤ n.
+ +
+Lemma mxrank_Frobenius m n p q (A : 'M_(m , n )) B (C : 'M_(p , q )) :
+ \rank (A ×m B ) + \rank (B ×m C ) ≤ \rank B + \rank (A ×m B ×m C ).
+ +
+Lemma mxrank_mul_min m n p (A : 'M_(m , n )) (B : 'M_(n , p )) :
+ \rank A + \rank B - n ≤ \rank (A ×m B ).
+ +
+Lemma addsmx_compl_full m n (A : 'M_(m , n )) : row_full (A + A ^C)%MS.
+ +
+Lemma sub_capmx_gen m1 m2 m3 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(m3 , n )) :
+ (A ≤ capmx_gen B C)%MS = (A ≤ B)%MS && (A ≤ C)%MS.
+ +
+Let capmx_witnessP m n (A : 'M_(m , n )) : equivmx A (qidmx A) (capmx_witness A).
+ +
+Let capmx_normP m n (A : 'M_(m , n )) : equivmx_spec A (qidmx A) (capmx_norm A).
+ +
+Let capmx_norm_eq m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ qidmx A = qidmx B → (A == B)%MS → capmx_norm A = capmx_norm B.
+ +
+Let capmx_nopP m n (A : 'M_(m , n )) : equivmx_spec A (qidmx A) (capmx_nop A).
+ +
+Let sub_qidmx m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ qidmx B → (A ≤ B)%MS.
+ +
+Let qidmx_cap m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ qidmx (A :&: B)%MS = qidmx A && qidmx B.
+ +
+Let capmx_eq_norm m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ qidmx A = qidmx B → (A :&: B)%MS = capmx_norm (A :&: B)%MS.
+ +
+Lemma capmxE m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A :&: B :=: capmx_gen A B)%MS.
+ +
+Lemma capmxSl m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) : (A :&: B ≤ A)%MS.
+ +
+Lemma sub_capmx m m1 m2 n (A : 'M_(m , n )) (B : 'M_(m1 , n )) (C : 'M_(m2 , n )) :
+ (A ≤ B :&: C)%MS = (A ≤ B)%MS && (A ≤ C)%MS.
+ +
+Lemma capmxC m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) : (A :&: B = B :&: A)%MS.
+ +
+Lemma capmxSr m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) : (A :&: B ≤ B)%MS.
+ +
+Lemma capmx_idPr n m1 m2 (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ reflect (A :&: B :=: B)%MS (B ≤ A)%MS.
+ +
+Lemma capmx_idPl n m1 m2 (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ reflect (A :&: B :=: A)%MS (A ≤ B)%MS.
+ +
+Lemma capmxS m1 m2 m3 m4 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n ))
+ (C : 'M_(m3 , n )) (D : 'M_(m4 , n )) :
+ (A ≤ C → B ≤ D → A :&: B ≤ C :&: D)%MS.
+ +
+Lemma cap_eqmx m1 m2 m3 m4 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n ))
+ (C : 'M_(m3 , n )) (D : 'M_(m4 , n )) :
+ (A :=: C → B :=: D → A :&: B :=: C :&: D)%MS.
+ +
+Lemma capmxMr m1 m2 n p (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(n , p )) :
+ ((A :&: B ) ×m C ≤ A ×m C :&: B ×m C)%MS.
+ +
+Lemma cap0mx m1 m2 n (A : 'M_(m2 , n )) : ((0 : 'M_(m1 , n )) :&: A)%MS = 0.
+ +
+Lemma capmx0 m1 m2 n (A : 'M_(m1 , n )) : (A :&: (0 : 'M_(m2 , n )))%MS = 0.
+ +
+Lemma capmxT m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ row_full B → (A :&: B :=: A)%MS.
+ +
+Lemma capTmx m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ row_full A → (A :&: B :=: B)%MS.
+ +
+Let capmx_nop_id n (A : 'M_n) : capmx_nop A = A.
+ +
+Lemma cap1mx n (A : 'M_n) : (1%:M :&: A = A)%MS.
+ +
+Lemma capmx1 n (A : 'M_n) : (A :&: 1%:M = A)%MS.
+ +
+Lemma genmx_cap m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ <<A :&: B >>%MS = (<<A >> :&: <>)%MS.
+ +
+Lemma capmxA m1 m2 m3 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(m3 , n )) :
+ (A :&: (B :&: C ) = A :&: B :&: C)%MS.
+ +
+Canonical capmx_monoid n :=
+ Monoid.Law (@capmxA n n n n) (@cap1mx n) (@capmx1 n).
+Canonical capmx_comoid n := Monoid.ComLaw (@capmxC n n n).
+ +
+Lemma bigcapmx_inf i0 P m n (A_ : I → 'M_n) (B : 'M_(m , n )) :
+ P i0 → (A_ i0 ≤ B → \bigcap_(i | P i ) A_ i ≤ B)%MS.
+ +
+Lemma sub_bigcapmxP P m n (A : 'M_(m , n )) (B_ : I → 'M_n) :
+ reflect (∀ i, P i → A ≤ B_ i)%MS (A ≤ \bigcap_(i | P i ) B_ i)%MS.
+ +
+Lemma genmx_bigcap P n (A_ : I → 'M_n) :
+ (<<\bigcap_(i | P i ) A_ i >> = \bigcap_(i | P i ) <<A_ i >>)%MS.
+ +
+Lemma matrix_modl m1 m2 m3 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(m3 , n )) :
+ (A ≤ C → A + (B :&: C ) :=: (A + B ) :&: C)%MS.
+ +
+Lemma matrix_modr m1 m2 m3 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) (C : 'M_(m3 , n )) :
+ (C ≤ A → (A :&: B ) + C :=: A :&: (B + C ))%MS.
+ +
+Lemma capmx_compl m n (A : 'M_(m , n )) : (A :&: A ^C)%MS = 0.
+ +
+Lemma mxrank_mul_ker m n p (A : 'M_(m , n )) (B : 'M_(n , p )) :
+ (\rank (A ×m B ) + \rank (A :&: kermx B ))%N = \rank A.
+ +
+Lemma mxrank_injP m n p (A : 'M_(m , n )) (f : 'M_(n , p )) :
+ reflect (\rank (A ×m f ) = \rank A) ((A :&: kermx f)%MS == 0).
+ +
+Lemma mxrank_disjoint_sum m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A :&: B)%MS = 0 → \rank (A + B)%MS = (\rank A + \rank B)%N.
+ +
+Lemma diffmxE m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A :\: B :=: A :&: (capmx_gen A B )^C)%MS.
+ +
+Lemma genmx_diff m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (<<A :\: B >> = A :\: B)%MS.
+ +
+Lemma diffmxSl m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) : (A :\: B ≤ A)%MS.
+ +
+Lemma capmx_diff m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ ((A :\: B ) :&: B)%MS = 0.
+ +
+Lemma addsmx_diff_cap_eq m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A :\: B + A :&: B :=: A)%MS.
+ +
+Lemma mxrank_cap_compl m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (\rank (A :&: B ) + \rank (A :\: B ))%N = \rank A.
+ +
+Lemma mxrank_sum_cap m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (\rank (A + B ) + \rank (A :&: B ) = \rank A + \rank B)%N.
+ +
+Lemma mxrank_adds_leqif m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ \rank (A + B ) ≤ \rank A + \rank B ?= iff (A :&: B ≤ (0 : 'M_n ))%MS.
+ +
+

+ +

+ Subspace projection matrix +

+ +
+Lemma proj_mx_sub m n U V (W : 'M_(m , n )) : (W ×m proj_mx U V ≤ U)%MS.
+ +
+Lemma proj_mx_compl_sub m n U V (W : 'M_(m , n )) :
+  (W ≤ U + V → W - W ×m proj_mx U V ≤ V)%MS.
+ +
+Lemma proj_mx_id m n U V (W : 'M_(m , n )) :
+  (U :&: V = 0)%MS → (W ≤ U)%MS → W ×m proj_mx U V = W.
+ +
+Lemma proj_mx_0 m n U V (W : 'M_(m , n )) :
+  (U :&: V = 0)%MS → (W ≤ V)%MS → W ×m proj_mx U V = 0.
+ +
+Lemma add_proj_mx m n U V (W : 'M_(m , n )) :
+    (U :&: V = 0)%MS → (W ≤ U + V)%MS →
+  W ×m proj_mx U V + W ×m proj_mx V U = W.
+ +
+Lemma proj_mx_proj n (U V : 'M_n) :
+  let P := proj_mx U V in (U :&: V = 0)%MS → P ×m P = P.
+ +
+

+ +

+ Completing a partially injective matrix to get a unit matrix. +

+ +
+Lemma complete_unitmx m n (U : 'M_(m , n )) (f : 'M_n) :
+ \rank (U ×m f ) = \rank U → {g : 'M_n | g \in unitmx & U ×m f = U ×m g }.
+ +
+

+ +

+ Mapping between two subspaces with the same dimension. +

+ +
+Lemma eq_rank_unitmx m1 m2 n (U : 'M_(m1 , n )) (V : 'M_(m2 , n )) :
+ \rank U = \rank V → {f : 'M_n | f \in unitmx & V :=: U ×m f }%MS.
+ +
+Section SumExpr.
+ +
+

+ +

+ This is the infrastructure to support the mxdirect predicate. We use a + bespoke canonical structure to decompose a matrix expression into binary + and n-ary products, using some of the "quote" technology. This lets us + characterize direct sums as set sums whose rank is equal to the sum of the + ranks of the individual terms. The mxsum_expr/proper_mxsum_expr structures + below supply both the decomposition and the calculation of the rank sum. + The mxsum_spec dependent predicate family expresses the consistency of + these two decompositions. + The main technical difficulty we need to overcome is the fact that + the "catch-all" case of canonical structures has a priority lower than + constant expansion. However, it is undesireable that local abbreviations + be opaque for the direct-sum predicate, e.g., not be able to handle + let S := (\sum(i | P i) LargeExpression i)%MS in mxdirect S -> ...). + As in "quote", we use the interleaving of constant expansion and + canonical projection matching to achieve our goal: we use a "wrapper" type + (indeed, the wrapped T type defined in ssrfun.v) with a self-inserting + non-primitive constructor to gain finer control over the type and + structure inference process. The innermost, primitive, constructor flags + trivial sums; it is initially hidden by an eta-expansion, which has been + made into a (default) canonical structure -- this lets type inference + automatically insert this outer tag. + In detail, we define three types + mxsum_spec S r <-> There exists a finite list of matrices A1, ..., Ak + such that S is the set sum of the Ai, and r is the sum + of the ranks of the Ai, i.e., S = (A1 + ... + Ak)%MS + and r = \rank A1 + ... + \rank Ak. Note that + mxsum_spec is a recursive dependent predicate family + whose elimination rewrites simultaneaously S, r and + the height of S. + proper_mxsum_expr n == The interface for proper sum expressions; this is + a double-entry interface, keyed on both the matrix sum + value and the rank sum. The matrix value is restricted + to square matrices, as the "+"%MS operator always + returns a square matrix. This interface has two + canonical insances, for binary and n-ary sums. + mxsum_expr m n == The interface for general sum expressions, comprising + both proper sums and trivial sums consisting of a + single matrix. The key values are WRAPPED as this lets + us give priority to the "proper sum" interpretation + (see below). To allow for trivial sums, the matrix key + can have any dimension. The mxsum_expr interface has + two canonical instances, for trivial and proper sums, + keyed to the Wrap and wrap constructors, respectively. + The projections for the two interfaces above are + proper_mxsum_val, mxsum_val : these are respectively coercions to 'M_n + and wrapped 'M(m, n); thus, the matrix sum for an + S : mxsum_expr m n can be written unwrap S. + proper_mxsum_rank, mxsum_rank : projections to the nat and wrapped nat, + respectively; the rank sum for S : mxsum_expr m n is + thus written unwrap (mxsum_rank S). + The mxdirect A predicate actually gets A in a phantom argument, which is + used to infer an (implicit) S : mxsum_expr such that unwrap S = A; the + actual definition is \rank (unwrap S) == unwrap (mxsum_rank S). + Note that the inference of S is inherently ambiguous: ANY matrix can be + viewed as a trivial sum, including one whose description is manifestly a + proper sum. We use the wrapped type and the interaction between delta + reduction and canonical structure inference to resolve this ambiguity in + favor of proper sums, as follows: +

The phantom type sets up a unification problem of the form + unwrap (mxsum_val ?S) = A + with unknown evar ?S : mxsum_expr m n. + +
As the constructor wrap is also a default Canonical instance for the + wrapped type, so A is immediately replaced with unwrap (wrap A) and + we get the residual unification problem + mxsum_val ?S = wrap A + +
Now Coq tries to apply the proper sum Canonical instance, which has + key projection wrap (proper_mxsum_val ?PS) where ?PS is a fresh evar + (of type proper_mxsum_expr n). This can only succeed if m = n, and if + a solution can be found to the recursive unification problem + proper_mxsum_val ?PS = A + This causes Coq to look for one of the two canonical constants for + proper_mxsum_val (addsmx or bigop) at the head of A, delta-expanding + A as needed, and then inferring recursively mxsum_expr structures for + the last argument(s) of that constant. + +
If the above step fails then the wrap constant is expanded, revealing + the primitive Wrap constructor; the unification problem now becomes + mxsum_val ?S = Wrap A + which fits perfectly the trivial sum canonical structure, whose key + projection is Wrap ?B where ?B is a fresh evar. Thus the inference + succeeds, and returns the trivial sum. + +

+ Note that the rank projections also register canonical values, so that the + same process can be used to infer a sum structure from the rank sum. In + that case, however, there is no ambiguity and the inference can fail, + because the rank sum for a trivial sum is not an arbitrary integer -- it + must be of the form \rank ?B. It is nevertheless necessary to use the + wrapped nat type for the rank sums, because in the non-trivial case the + head constant of the nat expression is determined by the proper_mxsum_expr + canonical structure, so the mxsum_expr structure must use a generic + constant, namely wrap. +

+ +
+Inductive mxsum_spec n : ∀ m, 'M [F ]_(m , n) → nat → Prop :=
+ | TrivialMxsum m A
+ : @mxsum_spec n m A (\rank A)
+ | ProperMxsum m1 m2 T1 T2 r1 r2 of
+ @mxsum_spec n m1 T1 r1 & @mxsum_spec n m2 T2 r2
+ : mxsum_spec (T1 + T2)%MS (r1 + r2)%N.
+ +
+Structure mxsum_expr m n := Mxsum {
+ mxsum_val :> wrapped 'M_(m , n );
+ mxsum_rank : wrapped nat;
+ _ : mxsum_spec (unwrap mxsum_val) (unwrap mxsum_rank)
+}.
+ +
+Canonical trivial_mxsum m n A :=
+ @Mxsum m n (Wrap A) (Wrap (\rank A)) (TrivialMxsum A).
+ +
+Structure proper_mxsum_expr n := ProperMxsumExpr {
+ proper_mxsum_val :> 'M_n;
+ proper_mxsum_rank : nat;
+ _ : mxsum_spec proper_mxsum_val proper_mxsum_rank
+}.
+ +
+Definition proper_mxsumP n (S : proper_mxsum_expr n) :=
+ let: ProperMxsumExpr _ _ termS := S return mxsum_spec S (proper_mxsum_rank S)
+ in termS.
+ +
+Canonical sum_mxsum n (S : proper_mxsum_expr n) :=
+ @Mxsum n n (wrap (S : 'M_n)) (wrap (proper_mxsum_rank S)) (proper_mxsumP S).
+ +
+Section Binary.
+Variable (m1 m2 n : nat) (S1 : mxsum_expr m1 n) (S2 : mxsum_expr m2 n).
+Fact binary_mxsum_proof :
+ mxsum_spec (unwrap S1 + unwrap S2)
+ (unwrap (mxsum_rank S1) + unwrap (mxsum_rank S2)).
+ Canonical binary_mxsum_expr := ProperMxsumExpr binary_mxsum_proof.
+End Binary.
+ +
+Section Nary.
+Context J (r : seq J) (P : pred J) n (S_ : J → mxsum_expr n n).
+Fact nary_mxsum_proof :
+ mxsum_spec (\sum_(j <- r | P j ) unwrap (S_ j))
+ (\sum_(j <- r | P j ) unwrap (mxsum_rank (S_ j))).
+Canonical nary_mxsum_expr := ProperMxsumExpr nary_mxsum_proof.
+End Nary.
+ +
+Definition mxdirect_def m n T of phantom 'M_(m , n ) (unwrap (mxsum_val T)) :=
+ \rank (unwrap T ) == unwrap (mxsum_rank T).
+ +
+End SumExpr.
+ +
+Notation mxdirect A := (mxdirect_def (Phantom 'M_(_,_) A%MS)).
+ +
+Lemma mxdirectP n (S : proper_mxsum_expr n) :
+ reflect (\rank S = proper_mxsum_rank S) (mxdirect S).
+ +
+Lemma mxdirect_trivial m n A : mxdirect (unwrap (@trivial_mxsum m n A)).
+ +
+Lemma mxrank_sum_leqif m n (S : mxsum_expr m n) :
+ \rank (unwrap S ) ≤ unwrap (mxsum_rank S) ?= iff mxdirect (unwrap S).
+ +
+Lemma mxdirectE m n (S : mxsum_expr m n) :
+ mxdirect (unwrap S) = (\rank (unwrap S ) == unwrap (mxsum_rank S)).
+ +
+Lemma mxdirectEgeq m n (S : mxsum_expr m n) :
+ mxdirect (unwrap S) = (\rank (unwrap S ) ≥ unwrap (mxsum_rank S)).
+ +
+Section BinaryDirect.
+ +
+Variables m1 m2 n : nat.
+ +
+Lemma mxdirect_addsE (S1 : mxsum_expr m1 n) (S2 : mxsum_expr m2 n) :
+ mxdirect (unwrap S1 + unwrap S2)
+ = [&& mxdirect (unwrap S1), mxdirect (unwrap S2)
+ & unwrap S1 :&: unwrap S2 == 0]%MS.
+ +
+Lemma mxdirect_addsP (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ reflect (A :&: B = 0)%MS (mxdirect (A + B)).
+ +
+End BinaryDirect.
+ +
+Section NaryDirect.
+ +
+Variables (P : pred I) (n : nat).
+ +
+Let TIsum A_ i := (A_ i :&: (\sum_(j | P j && (j != i )) A_ j ) = 0 :> 'M_n)%MS.
+ +
+Let mxdirect_sums_recP (S_ : I → mxsum_expr n n) :
+ reflect (∀ i, P i → mxdirect (unwrap (S_ i)) ∧ TIsum (unwrap \o S_) i)
+ (mxdirect (\sum_(i | P i ) (unwrap (S_ i)))).
+ +
+Lemma mxdirect_sumsP (A_ : I → 'M_n) :
+ reflect (∀ i, P i → A_ i :&: (\sum_(j | P j && (j != i )) A_ j ) = 0)%MS
+ (mxdirect (\sum_(i | P i ) A_ i)).
+ +
+Lemma mxdirect_sumsE (S_ : I → mxsum_expr n n) (xunwrap := unwrap) :
+ reflect (and (∀ i, P i → mxdirect (unwrap (S_ i)))
+ (mxdirect (\sum_(i | P i ) (xunwrap (S_ i)))))
+ (mxdirect (\sum_(i | P i ) (unwrap (S_ i)))).
+ +
+End NaryDirect.
+ +
+Section SubDaddsmx.
+ +
+Variables m m1 m2 n : nat.
+Variables (A : 'M [F ]_(m , n )) (B1 : 'M [F ]_(m1 , n )) (B2 : 'M [F ]_(m2 , n )).
+ +
+CoInductive sub_daddsmx_spec : Prop :=
+ SubDaddsmxSpec A1 A2 of (A1 ≤ B1)%MS & (A2 ≤ B2)%MS & A = A1 + A2
+ & ∀ C1 C2, (C1 ≤ B1)%MS → (C2 ≤ B2)%MS →
+ A = C1 + C2 → C1 = A1 ∧ C2 = A2.
+ +
+Lemma sub_daddsmx : (B1 :&: B2 = 0)%MS → (A ≤ B1 + B2)%MS → sub_daddsmx_spec.
+ +
+End SubDaddsmx.
+ +
+Section SubDsumsmx.
+ +
+Variables (P : pred I) (m n : nat) (A : 'M [F ]_(m , n )) (B : I → 'M [F ]_n).
+ +
+CoInductive sub_dsumsmx_spec : Prop :=
+ SubDsumsmxSpec A_ of ∀ i, P i → (A_ i ≤ B i)%MS
+ & A = \sum_(i | P i ) A_ i
+ & ∀ C, (∀ i, P i → C i ≤ B i)%MS →
+ A = \sum_(i | P i ) C i → {in SimplPred P , C =1 A_}.
+ +
+Lemma sub_dsumsmx :
+ mxdirect (\sum_(i | P i ) B i) → (A ≤ \sum_(i | P i ) B i)%MS →
+ sub_dsumsmx_spec.
+ +
+End SubDsumsmx.
+ +
+Section Eigenspace.
+ +
+Variables (n : nat) (g : 'M_n).
+ +
+Definition eigenspace a := kermx (g - a %:M).
+Definition eigenvalue : pred F := fun a ⇒ eigenspace a != 0.
+ +
+Lemma eigenspaceP a m (W : 'M_(m , n )) :
+ reflect (W ×m g = a *: W) (W ≤ eigenspace a)%MS.
+ +
+Lemma eigenvalueP a :
+ reflect (exists2 v : 'rV_n , v ×m g = a *: v & v != 0) (eigenvalue a).
+ +
+Lemma mxdirect_sum_eigenspace (P : pred I) a_ :
+ {in P &, injective a_} → mxdirect (\sum_(i | P i ) eigenspace (a_ i)).
+ +
+End Eigenspace.
+ +
+End RowSpaceTheory.
+ +
+Hint Resolve submx_refl.
+ +
+Notation "\rank A" := (mxrank A) : nat_scope.
+Notation "<< A >>" := (genmx A) : matrix_set_scope.
+Notation "A ^C" := (complmx A) : matrix_set_scope.
+Notation "A <= B" := (submx A B) : matrix_set_scope.
+Notation "A < B" := (ltmx A B) : matrix_set_scope.
+Notation "A <= B <= C" := ((submx A B) && (submx B C)) : matrix_set_scope.
+Notation "A < B <= C" := (ltmx A B && submx B C) : matrix_set_scope.
+Notation "A <= B < C" := (submx A B && ltmx B C) : matrix_set_scope.
+Notation "A < B < C" := (ltmx A B && ltmx B C) : matrix_set_scope.
+Notation "A == B" := ((submx A B) && (submx B A)) : matrix_set_scope.
+Notation "A :=: B" := (eqmx A B) : matrix_set_scope.
+Notation "A + B" := (addsmx A B) : matrix_set_scope.
+Notation "A :&: B" := (capmx A B) : matrix_set_scope.
+Notation "A :\: B" := (diffmx A B) : matrix_set_scope.
+Notation mxdirect S := (mxdirect_def (Phantom 'M_(_,_) S%MS)).
+ +
+Notation "\sum_ ( i <- r | P ) B" :=
+ (\big [addsmx /0%R]_(i <- r | P%B) B%MS) : matrix_set_scope.
+Notation "\sum_ ( i <- r ) B" :=
+ (\big [addsmx /0%R]_(i <- r) B%MS) : matrix_set_scope.
+Notation "\sum_ ( m <= i < n | P ) B" :=
+ (\big [addsmx /0%R]_(m ≤ i < n | P%B) B%MS) : matrix_set_scope.
+Notation "\sum_ ( m <= i < n ) B" :=
+ (\big [addsmx /0%R]_(m ≤ i < n) B%MS) : matrix_set_scope.
+Notation "\sum_ ( i | P ) B" :=
+ (\big [addsmx /0%R]_(i | P%B) B%MS) : matrix_set_scope.
+Notation "\sum_ i B" :=
+ (\big [addsmx /0%R]_i B%MS) : matrix_set_scope.
+Notation "\sum_ ( i : t | P ) B" :=
+ (\big [addsmx /0%R]_(i : t | P%B) B%MS) (only parsing) : matrix_set_scope.
+Notation "\sum_ ( i : t ) B" :=
+ (\big [addsmx /0%R]_(i : t) B%MS) (only parsing) : matrix_set_scope.
+Notation "\sum_ ( i < n | P ) B" :=
+ (\big [addsmx /0%R]_(i < n | P%B) B%MS) : matrix_set_scope.
+Notation "\sum_ ( i < n ) B" :=
+ (\big [addsmx /0%R]_(i < n) B%MS) : matrix_set_scope.
+Notation "\sum_ ( i 'in' A | P ) B" :=
+ (\big [addsmx /0%R]_(i in A | P%B) B%MS) : matrix_set_scope.
+Notation "\sum_ ( i 'in' A ) B" :=
+ (\big [addsmx /0%R]_(i in A) B%MS) : matrix_set_scope.
+ +
+Notation "\bigcap_ ( i <- r | P ) B" :=
+ (\big [capmx /1%:M ]_(i <- r | P%B) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( i <- r ) B" :=
+ (\big [capmx /1%:M ]_(i <- r) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( m <= i < n | P ) B" :=
+ (\big [capmx /1%:M ]_(m ≤ i < n | P%B) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( m <= i < n ) B" :=
+ (\big [capmx /1%:M ]_(m ≤ i < n) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( i | P ) B" :=
+ (\big [capmx /1%:M ]_(i | P%B) B%MS) : matrix_set_scope.
+Notation "\bigcap_ i B" :=
+ (\big [capmx /1%:M ]_i B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( i : t | P ) B" :=
+ (\big [capmx /1%:M ]_(i : t | P%B) B%MS) (only parsing) : matrix_set_scope.
+Notation "\bigcap_ ( i : t ) B" :=
+ (\big [capmx /1%:M ]_(i : t) B%MS) (only parsing) : matrix_set_scope.
+Notation "\bigcap_ ( i < n | P ) B" :=
+ (\big [capmx /1%:M ]_(i < n | P%B) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( i < n ) B" :=
+ (\big [capmx /1%:M ]_(i < n) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( i 'in' A | P ) B" :=
+ (\big [capmx /1%:M ]_(i in A | P%B) B%MS) : matrix_set_scope.
+Notation "\bigcap_ ( i 'in' A ) B" :=
+ (\big [capmx /1%:M ]_(i in A) B%MS) : matrix_set_scope.
+ +
+Section DirectSums.
+Variables (F : fieldType) (I : finType) (P : pred I).
+ +
+Lemma mxdirect_delta n f : {in P &, injective f } →
+ mxdirect (\sum_(i | P i ) <<delta_mx 0 (f i) : 'rV [F ]_n >>).
+ +
+End DirectSums.
+ +
+Section CardGL.
+ +
+Variable F : finFieldType.
+ +
+Lemma card_GL n : n > 0 →
+ #|'GL_n [F ]| = (#|F | ^ 'C (n , 2) × \prod_(1 ≤ i < n .+1 ) (#|F | ^ i - 1))%N.
+ +
+

+ +

+ An alternate, somewhat more elementary proof, that does not rely on the + row-space theory, but directly performs the LUP decomposition. +

+Lemma LUP_card_GL n : n > 0 →
+ #|'GL_n [F ]| = (#|F | ^ 'C (n , 2) × \prod_(1 ≤ i < n .+1 ) (#|F | ^ i - 1))%N.
+ +
+Lemma card_GL_1 : #|'GL_1 [F ]| = #|F |.-1.
+ +
+Lemma card_GL_2 : #|'GL_2 [F ]| = (#|F | × #|F |.-1 ^ 2 × #|F |.+1)%N.
+ +
+End CardGL.
+ +
+Lemma logn_card_GL_p n p : prime p → logn p #|'GL_n (p )| = 'C (n , 2).
+ +
+Section MatrixAlgebra.
+ +
+Variables F : fieldType.
+ +
+ +
+Lemma mem0mx m n (R : 'A_(m , n )) : 0 \in R.
+ +
+Lemma memmx0 n A : (A \in (0 : 'A_n )) → A = 0.
+ +
+Lemma memmx1 n (A : 'M_n) : (A \in mxvec 1%:M ) = is_scalar_mx A.
+ +
+Lemma memmx_subP m1 m2 n (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) :
+ reflect (∀ A, A \in R1 → A \in R2) (R1 ≤ R2)%MS.
+ +
+Lemma memmx_eqP m1 m2 n (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) :
+ reflect (∀ A, (A \in R1 ) = (A \in R2 )) (R1 == R2)%MS.
+ +
+Lemma memmx_addsP m1 m2 n A (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) :
+ reflect (∃ D, [/\ D .1 \in R1 , D .2 \in R2 & A = D .1 + D .2 ])
+ (A \in R1 + R2)%MS.
+ +
+Lemma memmx_sumsP (I : finType) (P : pred I) n (A : 'M_n) R_ :
+ reflect (exists2 A_, A = \sum_(i | P i ) A_ i & ∀ i, A_ i \in R_ i)
+ (A \in \sum_(i | P i ) R_ i)%MS.
+ +
+Lemma has_non_scalar_mxP m n (R : 'A_(m , n )) :
+ (1%:M \in R)%MS →
+ reflect (exists2 A, A \in R & ~~ is_scalar_mx A)%MS (1 < \rank R).
+ +
+Definition mulsmx m1 m2 n (R1 : 'A [F ]_(m1 , n )) (R2 : 'A_(m2 , n )) :=
+ (\sum_i <<R1 ×m lin_mx (mulmxr (vec_mx (row i R2)))>>)%MS.
+ +
+ +
+ +
+Lemma genmx_muls m1 m2 n (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) :
+ <<(R1 × R2)%MS>>%MS = (R1 × R2)%MS.
+ +
+Lemma mem_mulsmx m1 m2 n (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) A1 A2 :
+ (A1 \in R1 → A2 \in R2 → A1 ×m A2 \in R1 × R2)%MS.
+ +
+Lemma mulsmx_subP m1 m2 m n
+ (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) (R : 'A_(m , n )) :
+ reflect (∀ A1 A2, A1 \in R1 → A2 \in R2 → A1 ×m A2 \in R)
+ (R1 × R2 ≤ R)%MS.
+ +
+Lemma mulsmxS m1 m2 m3 m4 n (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n ))
+ (R3 : 'A_(m3 , n )) (R4 : 'A_(m4 , n )) :
+ (R1 ≤ R3 → R2 ≤ R4 → R1 × R2 ≤ R3 × R4)%MS.
+ +
+Lemma muls_eqmx m1 m2 m3 m4 n (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n ))
+ (R3 : 'A_(m3 , n )) (R4 : 'A_(m4 , n )) :
+ (R1 :=: R3 → R2 :=: R4 → R1 × R2 = R3 × R4)%MS.
+ +
+Lemma mulsmxP m1 m2 n A (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) :
+ reflect (exists2 A1, ∀ i, A1 i \in R1
+ & exists2 A2, ∀ i, A2 i \in R2
+ & A = \sum_(i < n ^ 2) A1 i ×m A2 i)
+ (A \in R1 × R2)%MS.
+ +
+Lemma mulsmxA m1 m2 m3 n (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) (R3 : 'A_(m3 , n )) :
+ (R1 × (R2 × R3 ) = R1 × R2 × R3)%MS.
+ +
+Lemma mulsmx_addl m1 m2 m3 n
+ (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) (R3 : 'A_(m3 , n )) :
+ ((R1 + R2 ) × R3 = R1 × R3 + R2 × R3)%MS.
+ +
+Lemma mulsmx_addr m1 m2 m3 n
+ (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) (R3 : 'A_(m3 , n )) :
+ (R1 × (R2 + R3 ) = R1 × R2 + R1 × R3)%MS.
+ +
+Lemma mulsmx0 m1 m2 n (R1 : 'A_(m1 , n )) : (R1 × (0 : 'A_(m2 , n )) = 0)%MS.
+ +
+Lemma muls0mx m1 m2 n (R2 : 'A_(m2 , n )) : ((0 : 'A_(m1 , n )) × R2 = 0)%MS.
+ +
+Definition left_mx_ideal m1 m2 n (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) :=
+ (R1 × R2 ≤ R2)%MS.
+ +
+Definition right_mx_ideal m1 m2 n (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) :=
+ (R2 × R1 ≤ R2)%MS.
+ +
+Definition mx_ideal m1 m2 n (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) :=
+ left_mx_ideal R1 R2 && right_mx_ideal R1 R2.
+ +
+Definition mxring_id m n (R : 'A_(m , n )) e :=
+ [/\ e != 0,
+ e \in R ,
+ ∀ A, A \in R → e ×m A = A
+ & ∀ A, A \in R → A ×m e = A ]%MS.
+ +
+Definition has_mxring_id m n (R : 'A [F ]_(m , n )) :=
+ (R != 0) &&
+ (row_mx 0 (row_mx (mxvec R) (mxvec R))
+ ≤ row_mx (cokermx R) (row_mx (lin_mx (mulmx R \o lin_mulmx))
+ (lin_mx (mulmx R \o lin_mulmxr))))%MS.
+ +
+Definition mxring m n (R : 'A_(m , n )) :=
+ left_mx_ideal R R && has_mxring_id R.
+ +
+Lemma mxring_idP m n (R : 'A_(m , n )) :
+ reflect (∃ e, mxring_id R e) (has_mxring_id R).
+ +
+Section CentMxDef.
+ +
+Variables (m n : nat) (R : 'A [F ]_(m , n )).
+ +
+Definition cent_mx_fun (B : 'M [F ]_n) := R ×m lin_mx (mulmxr B \- mulmx B).
+ +
+Lemma cent_mx_fun_is_linear : linear cent_mx_fun.
+Canonical cent_mx_fun_additive := Additive cent_mx_fun_is_linear.
+Canonical cent_mx_fun_linear := Linear cent_mx_fun_is_linear.
+ +
+Definition cent_mx := kermx (lin_mx cent_mx_fun).
+ +
+Definition center_mx := (R :&: cent_mx)%MS.
+ +
+End CentMxDef.
+ +
+ +
+Lemma cent_rowP m n B (R : 'A_(m , n )) :
+ reflect (∀ i (A := vec_mx (row i R)), A ×m B = B ×m A) (B \in 'C (R ))%MS.
+ +
+Lemma cent_mxP m n B (R : 'A_(m , n )) :
+ reflect (∀ A, A \in R → A ×m B = B ×m A) (B \in 'C (R ))%MS.
+ +
+Lemma scalar_mx_cent m n a (R : 'A_(m , n )) : (a %:M \in 'C (R ))%MS.
+ +
+Lemma center_mx_sub m n (R : 'A_(m , n )) : ('Z (R ) ≤ R)%MS.
+ +
+Lemma center_mxP m n A (R : 'A_(m , n )) :
+ reflect (A \in R ∧ ∀ B, B \in R → B ×m A = A ×m B)
+ (A \in 'Z (R ))%MS.
+ +
+Lemma mxring_id_uniq m n (R : 'A_(m , n )) e1 e2 :
+ mxring_id R e1 → mxring_id R e2 → e1 = e2.
+ +
+Lemma cent_mx_ideal m n (R : 'A_(m , n )) : left_mx_ideal 'C (R )%MS 'C (R )%MS.
+ +
+Lemma cent_mx_ring m n (R : 'A_(m , n )) : n > 0 → mxring 'C (R )%MS.
+ +
+Lemma mxdirect_adds_center m1 m2 n (R1 : 'A_(m1 , n )) (R2 : 'A_(m2 , n )) :
+ mx_ideal (R1 + R2)%MS R1 → mx_ideal (R1 + R2)%MS R2 →
+ mxdirect (R1 + R2) →
+ ('Z ((R1 + R2)%MS) :=: 'Z (R1 ) + 'Z (R2 ))%MS.
+ +
+Lemma mxdirect_sums_center (I : finType) m n (R : 'A_(m , n )) R_ :
+ (\sum_i R_ i :=: R)%MS → mxdirect (\sum_i R_ i) →
+ (∀ i : I, mx_ideal R (R_ i)) →
+ ('Z (R ) :=: \sum_i 'Z (R_ i ))%MS.
+ +
+End MatrixAlgebra.
+ +
+ +
+ +
+Notation "A \in R" := (submx (mxvec A) R) : matrix_set_scope.
+Notation "R * S" := (mulsmx R S) : matrix_set_scope.
+Notation "''C' ( R )" := (cent_mx R) : matrix_set_scope.
+Notation "''C_' R ( S )" := (R :&: 'C (S))%MS : matrix_set_scope.
+Notation "''C_' ( R ) ( S )" := ('C_R (S))%MS (only parsing) : matrix_set_scope.
+Notation "''Z' ( R )" := (center_mx R) : matrix_set_scope.
+ +
+ +
+

+ +

+ Parametricity for the row-space/F-algebra theory. +

+Section MapMatrixSpaces.
+ +
+Variables (aF rF : fieldType) (f : {rmorphism aF → rF }).
+ +
+Lemma Gaussian_elimination_map m n (A : 'M_(m , n )) :
+ Gaussian_elimination A ^f = ((col_ebase A )^f , (row_ebase A )^f , \rank A ).
+ +
+Lemma mxrank_map m n (A : 'M_(m , n )) : \rank A ^f = \rank A.
+ +
+Lemma row_free_map m n (A : 'M_(m , n )) : row_free A ^f = row_free A.
+ +
+Lemma row_full_map m n (A : 'M_(m , n )) : row_full A ^f = row_full A.
+ +
+Lemma map_row_ebase m n (A : 'M_(m , n )) : (row_ebase A )^f = row_ebase A ^f.
+ +
+Lemma map_col_ebase m n (A : 'M_(m , n )) : (col_ebase A )^f = col_ebase A ^f.
+ +
+Lemma map_row_base m n (A : 'M_(m , n )) :
+ (row_base A )^f = castmx (mxrank_map A , erefl n ) (row_base A ^f).
+ +
+Lemma map_col_base m n (A : 'M_(m , n )) :
+ (col_base A )^f = castmx (erefl m , mxrank_map A ) (col_base A ^f).
+ +
+Lemma map_pinvmx m n (A : 'M_(m , n )) : (pinvmx A )^f = pinvmx A ^f.
+ +
+Lemma map_kermx m n (A : 'M_(m , n )) : (kermx A )^f = kermx A ^f.
+ +
+Lemma map_cokermx m n (A : 'M_(m , n )) : (cokermx A )^f = cokermx A ^f.
+ +
+Lemma map_submx m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A ^f ≤ B ^f)%MS = (A ≤ B)%MS.
+ +
+Lemma map_ltmx m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (A ^f >^f :=: <<A ^f >>)%MS.
+ +
+Lemma map_addsmx m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (((A + B)%MS)^f :=: A ^f + B ^f)%MS.
+ +
+Lemma map_capmx_gen m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ (capmx_gen A B )^f = capmx_gen A ^f B ^f.
+ +
+Lemma map_capmx m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ ((A :&: B )^f :=: A ^f :&: B ^f)%MS.
+ +
+Lemma map_complmx m n (A : 'M_(m , n )) : (A ^C ^f = A ^f ^C)%MS.
+ +
+Lemma map_diffmx m1 m2 n (A : 'M_(m1 , n )) (B : 'M_(m2 , n )) :
+ ((A :\: B )^f :=: A ^f :\: B ^f)%MS.
+ +
+Lemma map_eigenspace n (g : 'M_n) a : (eigenspace g a )^f = eigenspace g ^f (f a).
+ +
+Lemma eigenvalue_map n (g : 'M_n) a : eigenvalue g ^f (f a) = eigenvalue g a.
+ +
+Lemma memmx_map m n A (E : 'A_(m , n )) : (A ^f \in E ^f)%MS = (A \in E)%MS.
+ +
+Lemma map_mulsmx m1 m2 n (E1 : 'A_(m1 , n )) (E2 : 'A_(m2 , n )) :
+ ((E1 × E2)%MS^f :=: E1 ^f × E2 ^f)%MS.
+ +
+Lemma map_cent_mx m n (E : 'A_(m , n )) : ('C (E )%MS)^f = 'C (E ^f )%MS.
+ +
+Lemma map_center_mx m n (E : 'A_(m , n )) : (('Z (E ))^f :=: 'Z (E ^f ))%MS.
+ +
+End MapMatrixSpaces.
+ +
+