diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 15 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 106 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 16 |
3 files changed, 132 insertions, 5 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 22229fe..08a16bd 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -206,6 +206,16 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). * application of kernel lemmas `mxdirect_sum_geigenspace`, * new lemmas: `eigenpolyP`, `eigenvalue_poly`, `eigenspace_sub_geigen`, + new `map_mx` lemmas: `map_kermxpoly`, `map_geigenspace`, `eigenpoly_map`. +- in `matrix.v`, added `comm_mx` and `comm_mxb` the propositional and + boolean versions of matrix commutation, `comm_mx A B` is + definitionally equal to `GRing.comm A B` when `A B : 'M_n.+1`, this + is witnessed by the lemma `comm_mxE`. New notation `all_comm_mx` + stands for `allrel comm_mxb`. New lemmas `comm_mx_sym`, `comm_mx_refl`, + `comm_mx0`, `comm0mx`, `comm_mx1`, `comm1mx`, `comm_mxN`, `comm_mxN1`, + `comm_mxD`, `comm_mxB`, `comm_mx_sum`, `comm_mxP`, `all_comm_mxP`, + `all_comm_mx1`, `all_comm_mx2P`, `all_comm_mx_cons`, `comm_mxC`, + `commCmx`, `comm_mx_horner`, and `horner_mxC`. The common arguments + of these lemmas `R` and `n` are maximal implicits. - in `seq.v`, added `in_mask`, `cons_subseq`, `undup_subseq`, `subset_maskP`. - in `fintype.v`, added `mask_enum_ord`. @@ -254,6 +264,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `BLeft x` and `BRight x` respectively mean close and open bounds as left bounds, and they respectively mean open and close bounds as right bounds. This change gives us the canonical "left to right" ordering of interval bounds. +- In `matrix.v`, generalized `diag_mx_comm` and `scalar_mx_comm` to + all `n`, instead of `n'.+1`, thanks to `commmmx`. - in `interval.v`: + Lemmas `mid_in_itv(|oo|cc)` have been generalized from `realFieldType` to @@ -315,6 +327,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). + `itv_intersectionC` (use `meetC` instead) + `itv_intersectionA` (use `meetA` instead) +- in `mxpoly.v`, we deprecate `scalar_mx_comm`, and advise to use + `comm_mxC` instead (with maximal implicit arguments `R` and `n`). + ### Infrastructure ### Misc diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 1cc585e..feb9edd 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -110,6 +110,9 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg. (* A \in unitmx == A is invertible (R must be a comUnitRingType). *) (* invmx A == the inverse matrix of A if A \in unitmx A, otherwise A. *) (* A \is a mxOver S == the matrix A has its coefficients in S. *) +(* comm_mx A B := A *m B = B *m A *) +(* comm_mxb A B := A *m B == B *m A *) +(* all_comm_mx As := allrel comm_mxb *) (* The following operations provide a correspondence between linear functions *) (* and matrices: *) (* lin1_mx f == the m x n matrix that emulates via right product *) @@ -2711,6 +2714,89 @@ Qed. End MapRingMatrix. +Section CommMx. +(***********************************************************************) +(************* Commutation property specialized to 'M[R]_n *************) +(***********************************************************************) +(* GRing.comm is bound to (non trivial) rings, and matrices form a *) +(* (non trivial) ring only when they are square and of manifestly *) +(* positive size. However during proofs in endomorphism reduction, we *) +(* take restrictions, which are matrices of size #|V| (with V a matrix *) +(* space) and it becomes cumbersome to state commutation between *) +(* restrictions, unless we relax the setting, and this relaxation *) +(* corresponds to comm_mx A B := A *m B = B *m A. *) +(* As witnessed by comm_mxE, when A and B have type 'M_n.+1, *) +(* comm_mx A B is convertible to GRing.comm A B. *) +(* The boolean version comm_mxb is designed to be used with seq.allrel *) +(***********************************************************************) + +Context {R : ringType} {n : nat}. +Implicit Types (f g p : 'M[R]_n) (fs : seq 'M[R]_n) (d : 'rV[R]_n) (I : Type). + +Definition comm_mx f g : Prop := f *m g = g *m f. +Definition comm_mxb f g : bool := f *m g == g *m f. + +Lemma comm_mx_sym f g : comm_mx f g -> comm_mx g f. +Proof. by rewrite /comm_mx. Qed. + +Lemma comm_mx_refl f : comm_mx f f. Proof. by []. Qed. + +Lemma comm_mx0 f : comm_mx f 0. Proof. by rewrite /comm_mx mulmx0 mul0mx. Qed. +Lemma comm0mx f : comm_mx 0 f. Proof. by rewrite /comm_mx mulmx0 mul0mx. Qed. + +Lemma comm_mx1 f : comm_mx f 1%:M. +Proof. by rewrite /comm_mx mulmx1 mul1mx. Qed. + +Lemma comm1mx f : comm_mx 1%:M f. +Proof. by rewrite /comm_mx mulmx1 mul1mx. Qed. + +Hint Resolve comm_mx0 comm0mx comm_mx1 comm1mx : core. + +Lemma comm_mxN f g : comm_mx f g -> comm_mx f (- g). +Proof. by rewrite /comm_mx mulmxN mulNmx => ->. Qed. + +Lemma comm_mxN1 f : comm_mx f (- 1%:M). Proof. exact/comm_mxN/comm_mx1. Qed. + +Lemma comm_mxD f g g' : comm_mx f g -> comm_mx f g' -> comm_mx f (g + g'). +Proof. by rewrite /comm_mx mulmxDl mulmxDr => -> ->. Qed. + +Lemma comm_mxB f g g' : comm_mx f g -> comm_mx f g' -> comm_mx f (g - g'). +Proof. by move=> fg fg'; apply/comm_mxD => //; apply/comm_mxN. Qed. + +Lemma comm_mxM f g g' : comm_mx f g -> comm_mx f g' -> comm_mx f (g *m g'). +Proof. by rewrite /comm_mx mulmxA => ->; rewrite -!mulmxA => ->. Qed. + +Lemma comm_mx_sum I (s : seq I) (P : pred I) (F : I -> 'M[R]_n) (f : 'M[R]_n) : + (forall i : I, P i -> comm_mx f (F i)) -> comm_mx f (\sum_(i <- s | P i) F i). +Proof. by move=> comm_mxfF; elim/big_ind: _ => // g h; apply: comm_mxD. Qed. + +Lemma comm_mxP f g : reflect (comm_mx f g) (comm_mxb f g). +Proof. exact: eqP. Qed. + +Notation all_comm_mx := (allrel comm_mxb). + +Lemma all_comm_mxP fs : + reflect {in fs &, forall f g, f *m g = g *m f} (all_comm_mx fs). +Proof. by apply: (iffP allrelP) => fsP ? ? ? ?; apply/eqP/fsP. Qed. + +Lemma all_comm_mx1 f : all_comm_mx [:: f]. +Proof. by rewrite /comm_mxb allrel1. Qed. + +Lemma all_comm_mx2P f g : reflect (f *m g = g *m f) (all_comm_mx [:: f; g]). +Proof. +by rewrite /comm_mxb; apply: (iffP and4P) => [[_/eqP//]|->]; rewrite ?eqxx. +Qed. + +Lemma all_comm_mx_cons f fs : + all_comm_mx (f :: fs) = all (comm_mxb f) fs && all_comm_mx fs. +Proof. by rewrite /comm_mxb [LHS]allrel_cons. Qed. + +End CommMx. +Notation all_comm_mx := (allrel comm_mxb). + +Lemma comm_mxE (R : ringType) (n : nat) : @comm_mx R n.+1 = @GRing.comm _. +Proof. by []. Qed. + Section ComMatrix. (* Lemmas for matrices with coefficients in a commutative ring *) Variable R : comRingType. @@ -2792,7 +2878,7 @@ Proof. by rewrite !mulmx_diag; congr (diag_mx _); apply/rowP=> i; rewrite !mxE mulrC. Qed. -Lemma diag_mx_comm n' (d e : 'rV[R]_n'.+1) : GRing.comm (diag_mx d) (diag_mx e). +Lemma diag_mx_comm n (d e : 'rV[R]_n) : comm_mx (diag_mx d) (diag_mx e). Proof. exact: diag_mxC. Qed. Lemma scalar_mxC m n a (A : 'M[R]_(m, n)) : A *m a%:M = a%:M *m A. @@ -2800,12 +2886,15 @@ Proof. by apply: trmx_inj; rewrite trmx_mul tr_scalar_mx !mul_scalar_mx linearZ. Qed. -Lemma scalar_mx_comm n' a (A : 'M[R]_n'.+1) : GRing.comm A a%:M. -Proof. exact: scalar_mxC. Qed. - Lemma mul_mx_scalar m n a (A : 'M[R]_(m, n)) : A *m a%:M = a *: A. Proof. by rewrite scalar_mxC mul_scalar_mx. Qed. +Lemma comm_mxC n a (A : 'M[R]_n) : comm_mx A a%:M. +Proof. by rewrite /comm_mx mul_mx_scalar mul_scalar_mx. Qed. + +Lemma commCmx n a (A : 'M[R]_n) : comm_mx a%:M A. +Proof. exact/comm_mx_sym/comm_mxC. Qed. + Lemma mxtrace_mulC m n (A : 'M[R]_(m, n)) B : \tr (A *m B) = \tr (B *m A). Proof. @@ -3051,10 +3140,19 @@ End ComMatrix. Arguments lin_mul_row {R m n} u. Arguments lin_mulmx {R m n p} A. +Arguments comm_mxC {R n}. +Arguments commCmx {R n}. +Arguments diag_mx_comm {R n}. Canonical matrix_finAlgType (R : finComRingType) n' := [finAlgType R of 'M[R]_n'.+1]. +Hint Resolve comm_mxC commCmx : core. + +Notation "@ 'scalar_mx_comm'" := (deprecate scalar_mx_comm comm_mxC) + (at level 10, only parsing) : fun_scope. +Notation scalar_mx_comm := (@scalar_mx_comm _ _) (only parsing). + (*****************************************************************************) (********************** Matrix unit ring and inverse matrices ****************) (*****************************************************************************) diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 24de1bc..79a28bf 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -271,7 +271,7 @@ Local Notation n := n'.+1. Variable A : 'M[R]_n. Implicit Types p q : {poly R}. -Definition horner_mx := horner_morph (fun a => scalar_mx_comm a A). +Definition horner_mx := horner_morph (comm_mxC^~ A). Canonical horner_mx_additive := [additive of horner_mx]. Canonical horner_mx_rmorphism := [rmorphism of horner_mx]. @@ -939,6 +939,20 @@ Proof. by rewrite /eigenpoly -map_kermxpoly map_mx_eq0. Qed. End MapKermxPoly. +Section CommmxPoly. + +Lemma comm_mx_horner (R : comRingType) (n' : nat) (A B : 'M[R]_n'.+1) + (p : {poly R}) : comm_mx A B -> comm_mx A (horner_mx B p). +Proof. +by move=> fg; apply: commr_horner => // i; rewrite coef_map; apply/commCmx. +Qed. + +Lemma horner_mxC (R : comRingType) (n' : nat) (A : 'M_n'.+1) (p q : {poly R}) : + GRing.comm (horner_mx A p) (horner_mx A p). +Proof. exact/comm_mx_horner/comm_mx_sym/comm_mx_horner. Qed. + +End CommmxPoly. + Section IntegralOverRing. Definition integralOver (R K : ringType) (RtoK : R -> K) (z : K) := |