# Library mathcomp.algebra.mxalgebra

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

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import fintype finfun bigop finset fingroup perm.
From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix.

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.

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, _.+1fun 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.

Notation stablemx V f := (V%MS ×m f%R V%MS)%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.
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.

Lemma eq_row_full m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
(A :=: B)%MS row_full A = row_full B.

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 : core.

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 mulmxVp m n (A : 'M[F]_(m, n)) : row_free A A ×m pinvmx A = 1%:M.

Lemma mulmxKp p m n (B : 'M[F]_(m, n)) : row_free B
cancel ((@mulmx _ p _ _)^~ B) (mulmx^~ (pinvmx B)).

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 : core.

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 rowsub_sub m1 m2 n (f : 'I_m2 'I_m1) (A : 'M_(m1, n)) :
(rowsub f A A)%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).

A variant of row_free_inj that exposes mulmxr, an alias for mulmx^~ but which is canonically additive
Definition row_free_injr m n p A : row_free A injective (mulmxr A) :=
@row_free_inj 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 pinvmxE n (A : 'M[F]_n) : A \in unitmx pinvmx A = invmx A.

Lemma mulVpmx m n (A : 'M[F]_(m, n)) : row_full A pinvmx A ×m A = 1%:M.

Lemma pinvmx_free m n (A : 'M[F]_(m, n)) : row_full A row_free (pinvmx A).

Lemma pinvmx_full m n (A : 'M[F]_(m, n)) : row_free A row_full (pinvmx A).

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.

Lemma row_base0 (m n : nat) : row_base (0 : 'M[F]_(m, n)) = 0.

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>> = <<B>>)%MS.

Lemma genmxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
reflect (<<A>> = <<B>>)%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 : core.

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 row_full_castmx m1 m2 n (A : 'M_(m1, n)) e :
row_full (castmx e A : 'M_(m2, n)) = row_full A.

Lemma row_free_castmx m1 m2 n (A : 'M_(m1, n)) e :
row_free (castmx e A : 'M_(m2, n)) = row_free A.

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.

Lemma rowsub_comp_sub (m n p q : nat) f (g : 'I_n 'I_p) (A : 'M_(m, q)) :
(rowsub (f \o g) A rowsub f A)%MS.

Lemma submx_rowsub (m n p q : nat) (h : 'I_n 'I_p) f g (A : 'M_(m, q)) :
f =1 g \o h (rowsub f A rowsub g A)%MS.

Lemma eqmx_rowsub_comp_perm (m1 m2 n : nat) (s : 'S_m2) f (A : 'M_(m1, n)) :
(rowsub (f \o s) A :=: rowsub f A)%MS.

Lemma eqmx_rowsub_comp (m n p q : nat) f (g : 'I_n 'I_p) (A : 'M_(m, q)) :
p n injective g (rowsub (f \o g) A :=: rowsub f A)%MS.

Lemma eqmx_rowsub (m n p q : nat) (h : 'I_n 'I_p) f g (A : 'M_(m, q)) :
injective h p n f =1 g \o h (rowsub f A :=: rowsub g A)%MS.

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.

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.

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.

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>> + <<B>>)%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_sums_genmxP P m n p (A : 'M_(m, p)) (B_ : I 'M_(n, p)) :
reflect ( u_ : I 'M_(m, n), A = \sum_(i | P i) u_ i ×m B_ i)
(A \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 sub_kermx p m n (A : 'M_(m, n)) (B : 'M_(p, m)) :
(B kermx A)%MS = (B ×m A == 0).

Lemma kermx0 m n : (kermx (0 : 'M_(m, n)) :=: 1%:M)%MS.

Lemma mulmx_free_eq0 m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
row_free B (A ×m B == 0) = (A == 0).

Lemma inj_row_free m n (A : 'M_(m, n)) :
( v : 'rV_m, v ×m A = 0 v = 0) row_free A.

Lemma row_freePn m n (M : 'M[F]_(m, n)) :
reflect ( i, (row i M row' i M)%MS) (~~ row_free M).

Lemma negb_row_free m n (M : 'M[F]_(m, n)) :
~~ row_free M = [ i, (row i M row' i M)%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>> :&: <<B>>)%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.
Two matrices with the same shape represent the same subspace iff they differ only by a change of basis.

Lemma eqmxMunitP m n (U V : 'M_(m, n)) :
reflect (exists2 P, P \in unitmx & U = P ×m V) (U == V)%MS.

Mapping between two subspaces with the same dimension.
maximal rank and full rank submatrices

Section MaxRankSubMatrix.
Variables (m n : nat) (A : 'M_(m, n)).

Definition maxrankfun : 'I_m ^ \rank A :=
[arg max_(f > finfun (widen_ord (rank_leq_row A))) \rank (rowsub f A)].

Lemma maxrowsub_free : row_free (rowsub mxf A).

Lemma eq_maxrowsub : (rowsub mxf A :=: A)%MS.

Lemma maxrankfun_inj : injective mxf.

Variable (rkA : row_full A).

Lemma maxrowsub_full : row_full (rowsub mxf A).
Hint Resolve maxrowsub_full : core.

Definition fullrankfun : 'I_m ^ n := finfun (mxf \o cast_ord (esym (eqP rkA))).

Lemma fullrowsub_full : row_full (rowsub frf A).

Lemma fullrowsub_unit : rowsub frf A \in unitmx.

Lemma fullrowsub_free : row_free (rowsub frf A).

Lemma mxrank_fullrowsub : \rank (rowsub frf A) = n.

Lemma eq_fullrowsub : (rowsub frf A :=: A)%MS.

Lemma fullrankfun_inj : injective frf.

End MaxRankSubMatrix.

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<