Library frobenius_form
Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq finfun.
Require Import ssralg path fintype perm poly fingroup mxpoly polydiv.
Require Import tuple matrix bigop zmodp mxtens polyorder dvdring.
Require Import companion similar mxstructure closed_poly.
Require Import ssrcomplements polydvd smith smith_complements.
Require Import ssralg path fintype perm poly fingroup mxpoly polydiv.
Require Import tuple matrix bigop zmodp mxtens polyorder dvdring.
Require Import companion similar mxstructure closed_poly.
Require Import ssrcomplements polydvd smith smith_complements.
This file provides a theory of invariant factors. The main result
proved here is the similarity between a matrix and its Frobenius
normal form.
Frobenius_seq M == The same as the sequence Smith_seq (XI - M) where
each polynomial has been divded by their
lead coefficient (Hence each polynomial is monic).
invariant_factors M == The sequence of non-constant polynomials of
Frobenius_seq M.
Frobenius_form M == The block diagonal matrix formed by the
companion matrices of the invariant factors of M.
Frobenius_form_CF M == The block diagonal matrix defined over a closed
field formed by the companion matrices of
the linear factors of the invariant factors of M.
Set Implicit Arguments.
Section Frobenius.
Variable F : fieldType.
Local Notation E := {poly F}.
Import GRing.Theory.
Import PolyPriField.
Local Open Scope ring_scope.
Definition Frobenius_seq n (A : 'M[F]_n) :=
[seq (lead_coef p)^-1 *: p | p : E <- take n (Smith_seq (char_poly_mx A))].
Lemma sorted_Frobenius_seq n (A : 'M[F]_n) :
sorted (@dvdp _) (Frobenius_seq A).
Lemma size_Frobenius_seq n (A : 'M[F]_n) : size (Frobenius_seq A) = n.
Lemma Frobenius_seq_char_poly n (A : 'M[F]_n) :
\prod_(p <- Frobenius_seq A) p = char_poly A.
Lemma Frobenius_seq_neq0 n (A : 'M[F]_n) p :
p \in Frobenius_seq A -> p != 0.
Lemma monic_Frobenius_seq n (A : 'M[F]_n) p:
p \in Frobenius_seq A -> p \is monic.
Lemma equiv_Frobenius_seq n (A : 'M[F]_n) :
equivalent (diag_mx_seq n n (Smith_seq (char_poly_mx A)))
(diag_mx_seq n n (Frobenius_seq A)).
Definition invariant_factors n (A : 'M[F]_n) :=
filter (fun p : E => 1 < size p) (Frobenius_seq A).
Lemma invariant_factor_neq0 n (A : 'M[F]_n) :
forall p, p \in invariant_factors A -> p != 0.
Lemma monic_invariant_factors n (A : 'M[F]_n) :
forall p, p \in invariant_factors A -> p \is monic.
Section dvdp_monic.
Local Open Scope ring_scope.
Import GRing.Theory.
Import PolyPriField.
Variable T : fieldType.
Definition dvdpm (p q : {poly T}) :=
(p \is monic) && (q \is monic) && (dvdp p q).
Lemma dvdpm_trans : transitive dvdpm.
Lemma dvdpm_asym : antisymmetric dvdpm.
Lemma dvd1pm (p : {poly T}) : p \is monic -> dvdpm 1 p.
End dvdp_monic.
Lemma Frobenius_seqE n (A : 'M[F]_n) : Frobenius_seq A =
nseq (n - size (invariant_factors A)) 1 ++ invariant_factors A.
Lemma invf_char_poly n (A : 'M[F]_n) :
\prod_(p <- invariant_factors A) p = char_poly A.
Lemma dvdp_invf_char_poly m (A : 'M[F]_m) (p : {poly F}) :
p \in (invariant_factors A) -> dvdp p (char_poly A).
Lemma sorted_invf n (A : 'M[F]_n) : sorted (@dvdp _) (invariant_factors A).
Lemma sum_size_inv_factors n (A : 'M[F]_n) :
(\sum_(p <- invariant_factors A) (size p).-1 = n)%N.
Lemma nnil_inv_factors n (A : 'M_n.+1) : invariant_factors A != [::].
Let Smith_block_cpmx n (A : 'M[F]_n) :=
let sp := invariant_factors A in
let size := [seq (size p).-2 | p : E <- sp] in
let blocks m i := diag_mx_seq m.+1 m.+1 (rcons (nseq m 1) sp`_i) in
diag_block_mx size blocks.
Let Smith_seq_cpmx n (A : 'M[F]_n) :=
let sp := invariant_factors A in
let m := size_sum [seq (size p).-2 | p : E <- sp] in
diag_mx_seq m.+1 m.+1 (Frobenius_seq A).
Lemma cast_inv n (A : 'M[F]_n.+1) : size (Frobenius_seq A) =
(size_sum [seq (size p).-2 | p : E <- (invariant_factors A)]).+1.
Lemma equiv_sbc_ssc n (A : 'M[F]_n) :
equivalent (Smith_block_cpmx A) (Smith_seq_cpmx A).
Lemma Smith_companion (p : E) : 1 < size p -> p \is monic ->
equivalent (Smith_form (char_poly_mx (companion_mx p)))
(diag_mx_seq (size p).-2.+1 (size p).-2.+1 (rcons (nseq (size p).-2 1) p)).
Definition Frobenius_form n (A : 'M[F]_n) :=
let sp := invariant_factors A in
let size := [seq (size p).-2 | p : E <- sp] in
let blocks n i := [seq companion_mxn n.+1 p | p <- sp]`_i in
diag_block_mx size blocks.
Lemma Frobenius n (A : 'M[F]_n.+1) :
similar A (Frobenius_form A).
Lemma Frobenius_unicity n m (A : 'M[F]_n) (B : 'M_m) : similar A B <->
invariant_factors A = invariant_factors B.
Lemma mxminpoly_inv_factors n (A : 'M[F]_n.+1) :
last 0 (Frobenius_seq A) = mxminpoly A.
End Frobenius.
Section Polynomial.
Local Open Scope ring_scope.
Import GRing.Theory.
Import PolyPriField.
Variable R : closedFieldType.
Lemma similar_poly_inv (p : {poly R}) :
let sp := linear_factor_seq p in
let size_seq := [seq (size p).-2 | p : {poly R} <- sp] in
let blocks n i := companion_mxn n.+1 sp`_i in
1 < (size p) -> p \is monic ->
similar (companion_mx p) (diag_block_mx size_seq blocks).
Definition Frobenius_form_CF n (A : 'M[R]_n) :=
let fm f s := flatten (map f s) in
let sp := invariant_factors A in
let l p := linear_factor_seq p in
let sc p := [seq (size q).-2 | q : {poly R} <- l p] in
let size := flatten (map sc sp) in
let blocks m i := companion_mxn m.+1 (fm l sp)`_i in
diag_block_mx size blocks.
Lemma similar_Frobenius n (A : 'M[R]_n.+1) :
similar (Frobenius_form A) (Frobenius_form_CF A).
End Polynomial.
This page has been generated by coqdoc