# Library frobenius_form

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.