diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 83 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 61 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 11 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 6 |
4 files changed, 111 insertions, 50 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 1d4f6d2..a0ac28f 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -574,8 +574,7 @@ Proof. by apply/matrixP=> i j; rewrite mxE row_mxEr. Qed. Lemma hsubmxK A : row_mx (lsubmx A) (rsubmx A) = A. Proof. -apply/matrixP=> i j; rewrite !mxE. -by case: splitP => k Dk //=; rewrite !mxE //=; congr (A _ _); apply: val_inj. +by apply/matrixP=> i j; rewrite !mxE; case: split_ordP => k ->; rewrite !mxE. Qed. Lemma col_mxEu A1 A2 i j : col_mx A1 A2 (lshift m2 i) j = A1 i j. @@ -707,12 +706,10 @@ Proof. by apply/matrixP=> i j; rewrite !(col_mxEd, mxE). Qed. Lemma col'Kl m n1 n2 j1 (A1 : 'M_(m, n1.+1)) (A2 : 'M_(m, n2)) : col' (lshift n2 j1) (row_mx A1 A2) = row_mx (col' j1 A1) A2. Proof. -apply/matrixP=> i /= j; symmetry; rewrite 2!mxE. -case: splitP => j' def_j'. - rewrite mxE -(row_mxEl _ A2); congr (row_mx _ _ _); apply: ord_inj. - by rewrite /= def_j'. +apply/matrixP=> i /= j; symmetry; rewrite 2!mxE; case: split_ordP => j' ->. + by rewrite mxE -(row_mxEl _ A2); congr (row_mx _ _ _); apply: ord_inj. rewrite -(row_mxEr A1); congr (row_mx _ _ _); apply: ord_inj => /=. -by rewrite /bump def_j' -ltnS -addSn ltn_addr. +by rewrite /bump -ltnS -addSn ltn_addr. Qed. Lemma row'Ku m1 m2 n i1 (A1 : 'M_(m1.+1, n)) (A2 : 'M_(m2, n)) : @@ -1192,6 +1189,30 @@ Lemma block_mx_eq0 m1 m2 n1 n2 (Aul : 'M_(m1, n1)) Aur Adl (Adr : 'M_(m2, n2)) : [&& Aul == 0, Aur == 0, Adl == 0 & Adr == 0]. Proof. by rewrite col_mx_eq0 !row_mx_eq0 !andbA. Qed. +Lemma matrix_eq0 m n (A : 'M_(m, n)) : + (A == 0) = [forall i, forall j, A i j == 0]. +Proof. +apply/eqP/'forall_'forall_eqP => [-> i j|A_eq0]; first by rewrite !mxE. +by apply/matrixP => i j; rewrite A_eq0 !mxE. +Qed. + +Lemma matrix0Pn m n (A : 'M_(m, n)) : reflect (exists i j, A i j != 0) (A != 0). +Proof. +by rewrite matrix_eq0; apply/(iffP forallPn) => -[i /forallPn]; exists i. +Qed. + +Lemma rV0Pn n (v : 'rV_n) : reflect (exists i, v 0 i != 0) (v != 0). +Proof. +apply: (iffP (matrix0Pn _)) => [[i [j]]|[j]]; last by exists 0, j. +by rewrite ord1; exists j. +Qed. + +Lemma cV0Pn n (v : 'cV_n) : reflect (exists i, v i 0 != 0) (v != 0). +Proof. +apply: (iffP (matrix0Pn _)) => [[i] [j]|[i]]; last by exists i, 0. +by rewrite ord1; exists i. +Qed. + Definition nz_row m n (A : 'M_(m, n)) := oapp (fun i => row i A) 0 [pick i | row i A != 0]. @@ -1289,10 +1310,10 @@ Lemma matrix_sum_delta A : A = \sum_(i < m) \sum_(j < n) A i j *: delta_mx i j. Proof. apply/matrixP=> i j. -rewrite summxE (bigD1 i) // summxE (bigD1 j) //= !mxE !eqxx mulr1. -rewrite !big1 ?addr0 //= => [i' | j']; rewrite eq_sym => /negPf diff. - by rewrite summxE big1 // => j' _; rewrite !mxE diff mulr0. -by rewrite !mxE eqxx diff mulr0. +rewrite summxE (bigD1_ord i) // summxE (bigD1_ord j) //= !mxE !eqxx mulr1. +rewrite !big1 ?addr0 //= => [i' | j'] _. + by rewrite summxE big1// => j' _; rewrite !mxE eq_liftF mulr0. +by rewrite !mxE eqxx eq_liftF mulr0. Qed. End RingModule. @@ -1405,9 +1426,8 @@ Canonical diag_mx_linear n := Linear (@diag_mx_is_linear n). Lemma diag_mx_sum_delta n (d : 'rV_n) : diag_mx d = \sum_i d 0 i *: delta_mx i i. Proof. -apply/matrixP=> i j; rewrite summxE (bigD1 i) //= !mxE eqxx /=. -rewrite eq_sym mulr_natr big1 ?addr0 // => i' ne_i'i. -by rewrite !mxE eq_sym (negPf ne_i'i) mulr0. +apply/matrixP=> i j; rewrite summxE (bigD1_ord i) //= !mxE eqxx /=. +by rewrite eq_sym mulr_natr big1 ?addr0 // => i'; rewrite !mxE eq_liftF mulr0. Qed. Lemma row_diag_mx n (d : 'rV_n) i : @@ -1531,9 +1551,8 @@ Proof. by apply/rowP=> j; rewrite ord1 mxE. Qed. Lemma scalar_mx_block n1 n2 a : a%:M = block_mx a%:M 0 0 a%:M :> 'M_(n1 + n2). Proof. -apply/matrixP=> i j; rewrite !mxE -val_eqE /=. -by do 2![case: splitP => ? ->; rewrite !mxE]; - rewrite ?eqn_add2l // -?(eq_sym (n1 + _)%N) eqn_leq leqNgt lshift_subproof. +apply/matrixP=> i j; rewrite !mxE. +by do 2![case: split_ordP => ? ->; rewrite !mxE]; rewrite ?eq_shift. Qed. (* Matrix multiplication using bigops. *) @@ -1619,8 +1638,8 @@ Qed. Lemma rowE m n i (A : 'M_(m, n)) : row i A = delta_mx 0 i *m A. Proof. -apply/rowP=> j; rewrite !mxE (bigD1 i) //= mxE !eqxx mul1r. -by rewrite big1 ?addr0 // => i' ne_i'i; rewrite mxE /= (negPf ne_i'i) mul0r. +apply/rowP=> j; rewrite !mxE (bigD1_ord i) //= mxE !eqxx mul1r. +by rewrite big1 ?addr0 // => i'; rewrite mxE /= lift_eqF mul0r. Qed. Lemma row_mul m n p (i : 'I_m) A (B : 'M_(n, p)) : @@ -1636,9 +1655,9 @@ Qed. Lemma mul_delta_mx_cond m n p (j1 j2 : 'I_n) (i1 : 'I_m) (k2 : 'I_p) : delta_mx i1 j1 *m delta_mx j2 k2 = delta_mx i1 k2 *+ (j1 == j2). Proof. -apply/matrixP => i k; rewrite !mxE (bigD1 j1) //=. +apply/matrixP => i k; rewrite !mxE (bigD1_ord j1) //=. rewrite mulmxnE !mxE !eqxx andbT -natrM -mulrnA !mulnb !andbA andbAC. -by rewrite big1 ?addr0 // => j; rewrite !mxE andbC -natrM; move/negPf->. +by rewrite big1 ?addr0 // => j; rewrite !mxE andbC -natrM lift_eqF. Qed. Lemma mul_delta_mx m n p (j : 'I_n) (i : 'I_m) (k : 'I_p) : @@ -1783,21 +1802,20 @@ Proof. by apply/matrixP=> i j; rewrite !mxE ltn_ord andbT. Qed. Lemma pid_mx_row n r : pid_mx r = row_mx 1%:M 0 :> 'M_(r, r + n). Proof. apply/matrixP=> i j; rewrite !mxE ltn_ord andbT. -case: splitP => j' ->; rewrite !mxE // . -by rewrite eqn_leq andbC leqNgt lshift_subproof. +by case: split_ordP => j' ->; rewrite !mxE// (val_eqE (lshift n i)) eq_shift. Qed. Lemma pid_mx_col m r : pid_mx r = col_mx 1%:M 0 :> 'M_(r + m, r). Proof. apply/matrixP=> i j; rewrite !mxE andbC. -by case: splitP => i' ->; rewrite !mxE // eq_sym. +by case: split_ordP => ? ->; rewrite !mxE//. Qed. Lemma pid_mx_block m n r : pid_mx r = block_mx 1%:M 0 0 0 :> 'M_(r + m, r + n). Proof. apply/matrixP=> i j; rewrite !mxE row_mx0 andbC. -case: splitP => i' ->; rewrite !mxE //; case: splitP => j' ->; rewrite !mxE //=. -by rewrite eqn_leq andbC leqNgt lshift_subproof. +do ![case: split_ordP => ? ->; rewrite !mxE//]. +by rewrite (val_eqE (lshift n _)) eq_shift. Qed. Lemma tr_pid_mx m n r : (pid_mx r)^T = pid_mx r :> 'M_(n, m). @@ -2818,8 +2836,7 @@ have [{detA0}A'0 | nzA'] := eqVneq (row 0 (\adj A)) 0; last first. pose A' := col' 0 A; pose vA := col 0 A. have defA: A = row_mx vA A'. apply/matrixP=> i j; rewrite !mxE. - case: splitP => j' def_j; rewrite mxE; congr (A i _); apply: val_inj => //=. - by rewrite def_j [j']ord1. + by case: split_ordP => j' ->; rewrite !mxE ?ord1; congr (A i _); apply: val_inj. have{IHn} w_ j : exists w : 'rV_n.+1, [/\ w != 0, w 0 j = 0 & w *m A' = 0]. have [|wj nzwj wjA'0] := IHn (row' j A'). by apply/eqP; move/rowP/(_ j)/eqP: A'0; rewrite !mxE mulf_eq0 signr_eq0. @@ -2827,13 +2844,9 @@ have{IHn} w_ j : exists w : 'rV_n.+1, [/\ w != 0, w 0 j = 0 & w *m A' = 0]. rewrite !mxE unlift_none -wjA'0; split=> //. apply: contraNneq nzwj => w0; apply/eqP/rowP=> k'. by move/rowP/(_ (lift j k')): w0; rewrite !mxE liftK. - apply/rowP=> k; rewrite !mxE (bigD1 j) //= mxE unlift_none mul0r add0r. - rewrite (reindex_onto (lift j) (odflt k \o unlift j)) /= => [|k']. - by apply: eq_big => k'; rewrite ?mxE liftK eq_sym neq_lift eqxx. - by rewrite eq_sym; case/unlift_some=> ? ? ->. -have [w0 [nz_w0 w00_0 w0A']] := w_ 0; pose a0 := (w0 *m vA) 0 0. -have [j {nz_w0}/= nz_w0j | w00] := pickP [pred j | w0 0 j != 0]; last first. - by case/eqP: nz_w0; apply/rowP=> j; rewrite mxE; move/eqP: (w00 j). + apply/rowP=> k; rewrite !mxE (bigD1_ord j) //= mxE unlift_none mul0r add0r. + by apply: eq_big => //= k'; rewrite !mxE/= liftK. +have [w0 [/rV0Pn[j nz_w0j] w00_0 w0A']] := w_ 0; pose a0 := (w0 *m vA) 0 0. have{w_} [wj [nz_wj wj0_0 wjA']] := w_ j; pose aj := (wj *m vA) 0 0. have [aj0 | nz_aj] := eqVneq aj 0. exists wj => //; rewrite defA (@mul_mx_row _ _ _ 1) [_ *m _]mx11_scalar -/aj. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 9a0034d..c0c4577 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -490,6 +490,17 @@ rewrite -{4}[B]mulmx_ebase -!mulmxA mulKmx //. by rewrite (mulmxA (pid_mx _)) pid_mx_id // !mulmxA -{}defA mulmxKV. Qed. +Lemma mulmxVp m n (A : 'M[F]_(m, n)) : row_free A -> A *m pinvmx A = 1%:M. +Proof. +move=> fA; rewrite -[X in X *m _]mulmx_ebase !mulmxA mulmxK ?row_ebase_unit//. +rewrite -[X in X *m _]mulmxA mul_pid_mx !minnn (minn_idPr _) ?rank_leq_col//. +by rewrite (eqP fA) pid_mx_1 mulmx1 mulmxV ?col_ebase_unit. +Qed. + +Lemma mulmxKp p m n (B : 'M[F]_(m, n)) : row_free B -> + cancel ((@mulmx _ p _ _)^~ B) (mulmx^~ (pinvmx B)). +Proof. by move=> ? A; rewrite -mulmxA mulmxVp ?mulmx1. Qed. + Lemma submxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (exists D, A = D *m B) (A <= B)%MS. Proof. @@ -715,6 +726,21 @@ Proof. by rewrite /ltmx sub1mx submx1. Qed. Lemma lt1mx m n (A : 'M_(m, n)) : (1%:M < A)%MS = false. Proof. by rewrite /ltmx submx1 andbF. Qed. +Lemma pinvmxE n (A : 'M[F]_n) : A \in unitmx -> pinvmx A = invmx A. +Proof. +move=> A_unit; apply: (@row_free_inj _ _ _ A); rewrite ?row_free_unit//. +by rewrite -[pinvmx _]mul1mx mulmxKpV ?sub1mx ?row_full_unit// mulVmx. +Qed. + +Lemma mulVpmx m n (A : 'M[F]_(m, n)) : row_full A -> pinvmx A *m A = 1%:M. +Proof. by move=> fA; rewrite -[pinvmx _]mul1mx mulmxKpV// sub1mx. Qed. + +Lemma pinvmx_free m n (A : 'M[F]_(m, n)) : row_full A -> row_free (pinvmx A). +Proof. by move=> /mulVpmx pAA1; apply/row_freeP; exists A. Qed. + +Lemma pinvmx_full m n (A : 'M[F]_(m, n)) : row_free A -> row_full (pinvmx A). +Proof. by move=> /mulmxVp ApA1; apply/row_fullP; exists A. Qed. + Lemma eqmxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (A :=: B)%MS (A == B)%MS. Proof. @@ -805,6 +831,9 @@ exists (col_ebase A *m pid_mx (\rank A)). by rewrite mulmxA -(mulmxA _ _ (pid_mx _)) pid_mx_id // mulmx_ebase. Qed. +Lemma row_base0 (m n : nat) : row_base (0 : 'M[F]_(m, n)) = 0. +Proof. by apply/eqmx0P; rewrite !eq_row_base !sub0mx. Qed. + Let qidmx_eq1 n (A : 'M_n) : qidmx A = (A == 1%:M). Proof. by rewrite /qidmx eqxx pid_mx_1. Qed. @@ -1174,11 +1203,22 @@ apply: (iffP submxP) => [[D ->]|]; first by rewrite -mulmxA mulmx_ker mulmx0. by move/mulmxKV_ker; exists (B *m col_ebase A). Qed. +Lemma sub_kermx p m n (A : 'M_(m, n)) (B : 'M_(p, m)) : + (B <= kermx A)%MS = (B *m A == 0). +Proof. exact/sub_kermxP/eqP. Qed. + +Lemma kermx0 m n : (kermx (0 : 'M_(m, n)) :=: 1%:M)%MS. +Proof. by apply/eqmxP; rewrite submx1/= sub_kermx mulmx0. Qed. + +Lemma mulmx_free_eq0 m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : + row_free B -> (A *m B == 0) = (A == 0). +Proof. by rewrite -sub_kermx -kermx_eq0 => /eqP->; rewrite submx0. Qed. + Lemma mulmx0_rank_max m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : A *m B = 0 -> \rank A + \rank B <= n. Proof. move=> AB0; rewrite -{3}(subnK (rank_leq_row B)) leq_add2r. -by rewrite -mxrank_ker mxrankS //; apply/sub_kermxP. +by rewrite -mxrank_ker mxrankS // sub_kermx AB0. Qed. Lemma mxrank_Frobenius m n p q (A : 'M_(m, n)) B (C : 'M_(p, q)) : @@ -1192,7 +1232,7 @@ set C1 := _ *m C; rewrite -{2}(subnKC (rank_leq_row C1)) leq_add2l -mxrank_ker. rewrite -(mxrankMfree _ (row_base_free (A *m B))). have: (row_base (A *m B) <= row_base B)%MS by rewrite !eq_row_base submxMl. case/submxP=> D defD; rewrite defD mulmxA mxrankMfree ?mxrankS //. -by apply/sub_kermxP; rewrite -mulmxA (mulmxA D) -defD -/C2 mulmx_ker. +by rewrite sub_kermx -mulmxA (mulmxA D) -defD -/C2 mulmx_ker. Qed. Lemma mxrank_mul_min m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : @@ -1218,7 +1258,7 @@ apply/idP/andP=> [sAI | [/submxP[B' ->{A}] /submxP[C' eqBC']]]. rewrite -{1}[K]hsubmxK mul_row_col; move/(canRL (addrK _))->. by rewrite add0r -mulNmx submxMl. have: (row_mx B' (- C') <= kermx (col_mx B C))%MS. - by apply/sub_kermxP; rewrite mul_row_col eqBC' mulNmx subrr. + by rewrite sub_kermx mul_row_col eqBC' mulNmx subrr. case/submxP=> D; rewrite -[kermx _]hsubmxK mul_mx_row. by case/eq_row_mx=> -> _; rewrite -mulmxA submxMl. Qed. @@ -1450,11 +1490,9 @@ apply/eqP; set K := kermx B; set C := (A :&: K)%MS. rewrite -(eqmxMr B (eq_row_base A)); set K' := _ *m B. rewrite -{2}(subnKC (rank_leq_row K')) -mxrank_ker eqn_add2l. rewrite -(mxrankMfree _ (row_base_free A)) mxrank_leqif_sup. - rewrite sub_capmx -(eq_row_base A) submxMl. - by apply/sub_kermxP; rewrite -mulmxA mulmx_ker. + by rewrite sub_capmx -(eq_row_base A) submxMl sub_kermx -mulmxA mulmx_ker/=. have /submxP[C' defC]: (C <= row_base A)%MS by rewrite eq_row_base capmxSl. -rewrite defC submxMr //; apply/sub_kermxP. -by rewrite mulmxA -defC; apply/sub_kermxP; rewrite capmxSr. +by rewrite defC submxMr // sub_kermx mulmxA -defC -sub_kermx capmxSr. Qed. Lemma mxrank_injP m n p (A : 'M_(m, n)) (f : 'M_(n, p)) : @@ -1936,10 +1974,7 @@ 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. -Proof. -rewrite (sameP (sub_kermxP _ _) eqP). -by rewrite mulmxBr subr_eq0 mul_mx_scalar; apply: eqP. -Qed. +Proof. by rewrite sub_kermx mulmxBr subr_eq0 mul_mx_scalar; apply/eqP. Qed. Lemma eigenvalueP a : reflect (exists2 v : 'rV_n, v *m g = a *: v & v != 0) (eigenvalue a). @@ -2155,9 +2190,7 @@ rewrite -sum1_card (partition_big lsubmx nzC) => [|A]; last first. rewrite -[A]hsubmxK v0 -[n.+1]/(1 + n)%N -col_mx0. rewrite -[rsubmx _]vsubmxK -det_tr tr_row_mx !tr_col_mx !trmx0. by rewrite det_lblock [0]mx11_scalar det_scalar1 mxE mul0r. -rewrite -sum_nat_const; apply: eq_bigr; rewrite /= -[n.+1]/(1 + n)%N => v nzv. -case: (pickP (fun i => v i 0 != 0)) => [k nza | v0]; last first. - by case/eqP: nzv; apply/colP=> i; move/eqP: (v0 i); rewrite mxE. +rewrite -sum_nat_const; apply: eq_bigr => /= v /cV0Pn[k nza]. have xrkK: involutive (@xrow F _ _ 0 k). by move=> m A /=; rewrite /xrow -row_permM tperm2 row_perm1. rewrite (reindex_inj (inv_inj (xrkK (1 + n)%N))) /= -[n.+1]/(1 + n)%N. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index a8cf94b..f33e291 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -188,7 +188,7 @@ have: rj0T (Ss_ dj.+1) = 'X^dj *: rj0T (S_ j1) + 1 *: rj0T (Ss_ dj). rewrite Sylvester_mxE insubdK; last exact: leq_ltn_trans (ltjS). by have [->|] := eqP; rewrite (addr0, add0r). rewrite -det_tr => /determinant_multilinear->; - try by apply/matrixP=> i j; rewrite !mxE eq_sym (negPf (neq_lift _ _)). + try by apply/matrixP=> i j; rewrite !mxE lift_eqF. have [dj0 | dj_gt0] := posnP dj; rewrite ?dj0 !mul1r. rewrite !det_tr det_map_mx addrC (expand_det_col _ j0) big1 => [|i _]. rewrite add0r; congr (\det _)%:P. @@ -598,6 +598,15 @@ Qed. Lemma mxminpoly_min p : horner_mx A p = 0 -> p_A %| p. Proof. by move=> pA0; rewrite /dvdp -horner_mxK pA0 mx_inv_horner0. Qed. +Lemma mxminpoly_minP p : reflect (horner_mx A p = 0) (p_A %| p). +Proof. +apply: (iffP idP); last exact: mxminpoly_min. +by move=> /Pdiv.Field.dvdpP[q ->]; rewrite rmorphM/= mx_root_minpoly mulr0. +Qed. + +Lemma dvd_mxminpoly p : (p_A %| p) = (horner_mx A p == 0). +Proof. exact/mxminpoly_minP/eqP. Qed. + Lemma horner_rVpoly_inj : injective (horner_mx A \o rVpoly : 'rV_d -> 'M_n). Proof. apply: can_inj (poly_rV \o mx_inv_horner) _ => u /=. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index e83bc09..a33788d 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1093,6 +1093,12 @@ Proof. by rewrite /comm_poly !hornerC !simp. Qed. Lemma comm_polyX x : comm_poly 'X x. Proof. by rewrite /comm_poly !hornerX. Qed. +Lemma commr_horner a b p : GRing.comm a b -> comm_coef p a -> GRing.comm a p.[b]. +Proof. +move=> cab cpa; rewrite horner_coef; apply: commr_sum => i _. +by apply: commrM => //; apply: commrX. +Qed. + Lemma hornerM_comm p q x : comm_poly q x -> (p * q).[x] = p.[x] * q.[x]. Proof. move=> comm_qx. |