- -

Library mathcomp.algebra.mxalgebra

- -

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

- -

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

- -

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

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