# Library mathcomp.algebra.mxred

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
From mathcomp Require Import choice fintype finfun bigop fingroup perm order.
From mathcomp Require Import ssralg zmodp matrix mxalgebra poly polydiv mxpoly.
In this file, we prove diagonalization theorems. For this purpose, we define conjugation, similarity and diagonalizability. conjmx V f := V *m f *m pinvmx V == the conjugation of f by V, i.e. "the" matrix of f in the basis of row vectors of V. Although this makes sense only when f stabilizes V, the definition can be stated more generally. similar_to P A C == where P is a base change matrix, A is a matrix, and C is a class of matrices, this states that conjmx P A is in C, which means A is similar to a matrix in C. From the latter, we derive serveral related notions: similar P A B := similar_to P A (pred1 B) == A is similar to B, with base change matrix P similar_in D A B == A is similar to B, with a base change matrix in D similar_in_to D A C == A is similar to a matrix in the class C, with a base change matrix in D all_similar_to D As C == all the matrices in the sequence As are similar to some matrix in the class C, with a base change matrix in D. We also specialize the class C, to diagonalizability: similar_diag P A := (similar_to P A is_diag_mx). diagonalizable_in D A := (similar_in_to D A is_diag_mx). diagonalizable A := (diagonalizable_in unitmx A). codiagonalizable_in D As := (all_similar_to D As is_diag_mx). codiagonalizable As := (codiagonalizable_in unitmx As). The main results of this file are: diagonalizablePeigen: a matrix is diagonalizable iff there is a sequence of scalars r, such that the sum of the associated eigenspaces is full. diagonalizableP: a matrix is diagonalizable iff its minimal polynomial divides a split polynomial with simple roots. codiagonalizableP: a sequence of matrices are diagonalizable in the same basis iff they are all diagonalizable and commute pairwize. We also specialize the class C, to trigonalizablility: similar_trig P A := (similar_to P A is_trig_mx). trigonalizable_in D A := (similar_in_to D A is_trig_mx). trigonalizable A := (trigonalizable_in unitmx A). cotrigonalizable_in D As := (all_similar_to D As is_trig_mx). cotrigonalizable As := (cotrigonalizable_in unitmx As). The theory of trigonalization is however not developed in this file.
Set Implicit Arguments.
Import GRing.Theory.
Import Monoid.Theory.
Local Open Scope ring_scope.
Section ConjMx.
Context {F : fieldType}.
Definition conjmx (m n : nat)
(V : 'M_(m, n)) (f : 'M[F]_n) : 'M_m := V ×m f ×m pinvmx V.
Notation restrictmx V := (conjmx (row_base V)).
Lemma stablemx_comp (m n p : nat) (V : 'M[F]_(m, n)) (W : 'M_(n, p)) (f : 'M_p) :
stablemx W f → stablemx V (conjmx W f) → stablemx (V ×m W) f.
Lemma stablemx_restrict m n (A : 'M[F]_n) (V : 'M_n) (W : 'M_(m, \rank V)):
stablemx V A → stablemx W (restrictmx V A) = stablemx (W ×m row_base V) A.
Lemma conjmxM (m n : nat) (V : 'M[F]_(m, n)) :
{in [pred f | stablemx V f] &, {morph conjmx V : f g / f ×m g}}.
Lemma conjMmx (m n p : nat) (V : 'M[F]_(m, n)) (W : 'M_(n, p)) (f : 'M_p) :
row_free (V ×m W) → stablemx W f → stablemx V (conjmx W f) →
conjmx (V ×m W) f = conjmx V (conjmx W f).
Lemma conjuMmx (m n : nat) (V : 'M[F]_m) (W : 'M_(m, n)) (f : 'M_n) :
V \in unitmx → row_free W → stablemx W f →
conjmx (V ×m W) f = conjmx V (conjmx W f).
Lemma conjMumx (m n : nat) (V : 'M[F]_(m, n)) (W f : 'M_n) :
W \in unitmx → row_free V → stablemx V (conjmx W f) →
conjmx (V ×m W) f = conjmx V (conjmx W f).
Lemma conjuMumx (n : nat) (V W f : 'M[F]_n) :
V \in unitmx → W \in unitmx →
conjmx (V ×m W) f = conjmx V (conjmx W f).
Lemma conjmx_scalar (m n : nat) (V : 'M[F]_(m, n)) (a : F) :
row_free V → conjmx V a%:M = a%:M.
Lemma conj0mx (m n : nat) f : conjmx (0 : 'M[F]_(m, n)) f = 0.
Lemma conjmx0 (m n : nat) (V : 'M[F]_(m, n)) : conjmx V 0 = 0.
Lemma conjumx (n : nat) (V : 'M_n) (f : 'M[F]_n) : V \in unitmx →
conjmx V f = V ×m f ×m invmx V.
Lemma conj1mx (n : nat) (f : 'M[F]_n) : conjmx 1%:M f = f.
Lemma conjVmx (n : nat) (V : 'M_n) (f : 'M[F]_n) : V \in unitmx →
conjmx (invmx V) f = invmx V ×m f ×m V.
Lemma conjmxK (n : nat) (V f : 'M[F]_n) :
V \in unitmx → conjmx (invmx V) (conjmx V f) = f.
Lemma conjmxVK (n : nat) (V f : 'M[F]_n) :
V \in unitmx → conjmx V (conjmx (invmx V) f) = f.
Lemma horner_mx_conj m n p (B : 'M[F]_(n.+1, m.+1)) (f : 'M_m.+1) :
row_free B → stablemx B f →
horner_mx (conjmx B f) p = conjmx B (horner_mx f p).
Lemma horner_mx_uconj n p (B : 'M[F]_(n.+1)) (f : 'M_n.+1) :
B \is a GRing.unit →
horner_mx (B ×m f ×m invmx B) p = B ×m horner_mx f p ×m invmx B.
Lemma horner_mx_uconjC n p (B : 'M[F]_(n.+1)) (f : 'M_n.+1) :
B \is a GRing.unit →
horner_mx (invmx B ×m f ×m B) p = invmx B ×m horner_mx f p ×m B.
Lemma mxminpoly_conj m n (V : 'M[F]_(m.+1, n.+1)) (f : 'M_n.+1) :
row_free V → stablemx V f → mxminpoly (conjmx V f) %| mxminpoly f.
Lemma mxminpoly_uconj n (V : 'M[F]_(n.+1)) (f : 'M_n.+1) :
V \in unitmx → mxminpoly (conjmx V f) = mxminpoly f.
Section fixed_stablemx_space.
Variables (m n : nat).
Implicit Types (V : 'M[F]_(m, n)) (f : 'M[F]_n).
Implicit Types (a : F) (p : {poly F}).
Section Sub.
Variable (k : nat).
Implicit Types (W : 'M[F]_(k, m)).
Lemma sub_kermxpoly_conjmx V f p W : stablemx V f → row_free V →
(W ≤ kermxpoly (conjmx V f) p)%MS = (W ×m V ≤ kermxpoly f p)%MS.
Lemma sub_eigenspace_conjmx V f a W : stablemx V f → row_free V →
(W ≤ eigenspace (conjmx V f) a)%MS = (W ×m V ≤ eigenspace f a)%MS.
End Sub.
Lemma eigenpoly_conjmx V f : stablemx V f → row_free V →
{subset eigenpoly (conjmx V f) ≤ eigenpoly f}.
Lemma eigenvalue_conjmx V f : stablemx V f → row_free V →
{subset eigenvalue (conjmx V f) ≤ eigenvalue f}.
Lemma conjmx_eigenvalue a V f : (V ≤ eigenspace f a)%MS → row_free V →
conjmx V f = a%:M.
End fixed_stablemx_space.
End ConjMx.
Notation restrictmx V := (conjmx (row_base V)).
Definition similar_to {F : fieldType} {m n} (P : 'M_(m, n)) A
(C : {pred 'M[F]_m}) := C (conjmx P A).
Notation similar P A B := (similar_to P A (PredOfSimpl.coerce (pred1 B))).
Notation similar_in D A B := (exists2 P, P \in D & similar P A B).
Notation similar_in_to D A C := (exists2 P, P \in D & similar_to P A C).
Notation all_similar_to D As C := (exists2 P, P \in D & all [pred A | similar_to P A C] As).
Notation similar_diag P A := (similar_to P A is_diag_mx).
Notation diagonalizable_in D A := (similar_in_to D A is_diag_mx).
Notation diagonalizable A := (diagonalizable_in unitmx A).
Notation codiagonalizable_in D As := (all_similar_to D As is_diag_mx).
Notation codiagonalizable As := (codiagonalizable_in unitmx As).
Notation similar_trig P A := (similar_to P A is_trig_mx).
Notation trigonalizable_in D A := (similar_in_to D A is_trig_mx).
Notation trigonalizable A := (trigonalizable_in unitmx A).
Notation cotrigonalizable_in D As := (all_similar_to D As is_trig_mx).
Notation cotrigonalizable As := (cotrigonalizable_in unitmx As).
Section Similarity.
Context {F : fieldType}.
Lemma similarPp m n {P : 'M[F]_(m, n)} {A B} :
stablemx P A → similar P A B → P ×m A = B ×m P.
Lemma similarW m n {P : 'M[F]_(m, n)} {A B} : row_free P →
P ×m A = B ×m P → similar P A B.
Section Similar.
Context {n : nat}.
Implicit Types (f g p : 'M[F]_n) (fs : seq 'M[F]_n) (d : 'rV[F]_n).
Lemma similarP {p f g} : p \in unitmx →
reflect (p ×m f = g ×m p) (similar p f g).
Lemma similarRL {p f g} : p \in unitmx →
reflect (g = p ×m f ×m invmx p) (similar p f g).
Lemma similarLR {p f g} : p \in unitmx →
reflect (f = conjmx (invmx p) g) (similar p f g).
End Similar.
Lemma similar_mxminpoly {n} {p f g : 'M[F]_n.+1} : p \in unitmx →
similar p f g → mxminpoly f = mxminpoly g.
Lemma similar_diag_row_base m n (P : 'M[F]_(m, n)) (A : 'M_n) :
similar_diag (row_base P) A = is_diag_mx (restrictmx P A).
Lemma similar_diagPp m n (P : 'M[F]_(m, n)) A :
reflect (∀ i j : 'I__, i != j :> nat → conjmx P A i j = 0)
(similar_diag P A).
Lemma similar_diagP n (P : 'M[F]_n) A : P \in unitmx →
reflect (∀ i j : 'I__, i != j :> nat → (P ×m A ×m invmx P) i j = 0)
(similar_diag P A).
Lemma similar_diagPex {m} {n} {P : 'M[F]_(m, n)} {A} :
reflect (∃ D, similar P A (diag_mx D)) (similar_diag P A).
Lemma similar_diagLR n {P : 'M[F]_n} {A} : P \in unitmx →
reflect (∃ D, A = conjmx (invmx P) (diag_mx D)) (similar_diag P A).
Lemma similar_diag_mxminpoly {n} {p f : 'M[F]_n.+1}
(rs := undup [seq conjmx p f i i | i <- enum 'I_n.+1]) :
p \in unitmx → similar_diag p f →
mxminpoly f = \prod_(r <- rs) ('X - r%:P).
End Similarity.
Lemma similar_diag_sum (F : fieldType) (m n : nat) (p_ : 'I_n → nat)
(V_ : ∀ i, 'M[F]_(p_ i, m)) (f : 'M[F]_m) :
mxdirect (\sum_i <<V_ i>>) →
(∀ i, stablemx (V_ i) f) →
(∀ i, row_free (V_ i)) →
similar_diag (\mxcol_i V_ i) f = [∀ i, similar_diag (V_ i) f].
Section Diag.
Variable (F : fieldType).
Lemma codiagonalizable1 n (A : 'M[F]_n) :
codiagonalizable [:: A] ↔ diagonalizable A.
Lemma codiagonalizablePfull n (As : seq 'M[F]_n) :
codiagonalizable As ↔ ∃ m,
exists2 P : 'M_(m, n), row_full P & all [pred A | similar_diag P A] As.
Lemma codiagonalizable_on m n (V_ : 'I_n → 'M[F]_m) (As : seq 'M[F]_m) :
(\sum_i V_ i :=: 1%:M)%MS → mxdirect (\sum_i V_ i) →
(∀ i, all (fun A ⇒ stablemx (V_ i) A) As) →
(∀ i, codiagonalizable (map (restrictmx (V_ i)) As)) → codiagonalizable As.
Lemma diagonalizable_diag {n} (d : 'rV[F]_n) : diagonalizable (diag_mx d).
Hint Resolve diagonalizable_diag : core.
Lemma diagonalizable_scalar {n} (a : F) : diagonalizable (a%:M : 'M_n).
Hint Resolve diagonalizable_scalar : core.
Lemma diagonalizable0 {n} : diagonalizable (0 : 'M[F]_n).
Hint Resolve diagonalizable0 : core.
Lemma diagonalizablePeigen {n} {f : 'M[F]_n} :
diagonalizable f ↔
exists2 rs, uniq rs & (\sum_(r <- rs) eigenspace f r :=: 1%:M)%MS.
Lemma diagonalizableP n' (n := n'.+1) (f : 'M[F]_n) :
diagonalizable f ↔
exists2 rs, uniq rs & mxminpoly f %| \prod_(x <- rs) ('X - x%:P).
Lemma diagonalizable_conj_diag m n (V : 'M[F]_(m, n)) (d : 'rV[F]_n) :
stablemx V (diag_mx d) → row_free V → diagonalizable (conjmx V (diag_mx d)).
Lemma codiagonalizableP n (fs : seq 'M[F]_n) :
{in fs &, ∀ f g, comm_mx f g} ∧ (∀ f, f \in fs → diagonalizable f)
↔ codiagonalizable fs.
End Diag.