# Library jordan

The main result of this file is the theorem of Jordan decomposition. A direct consequence of this theorem is the diagonalization theorem. Jordan_block lam n == The Jordan block of dimension n with the value lam on the diagonal. Jordan_form M == The block diagonal matrix formed by the Jordan blocks of roots of invariant factors of M, and of dimension their multiplicity.

Set Implicit Arguments.

Section def.

Variable R : ringType.
Import GRing.Theory.
Local Open Scope ring_scope.

Definition Jordan_block lam n : 'M[R]_n :=
\matrix_(i,j) (lam *+ (i == j :> nat) + (i.+1 == j)%:R).

Lemma Jordan_block0 : Jordan_block 0 1 = 0.

Lemma upt_Jordan_block lam n : upper_triangular_mx (Jordan_block lam n).

End def.

Section trigonal.

Variable R : comRingType.
Import GRing.Theory.
Local Open Scope ring_scope.

Lemma det_Jordan_block (lam : R) n : \det (Jordan_block lam n) = lam ^+ n.

Lemma Jordan_expn (lam : R) n k :
(Jordan_block lam n.+1)^+ k =
\matrix_(i,j) (('C(k,j - i)%:R * (lam^+ (k - (j - i)))) *+ (i <= j)).

Lemma char_poly_Jordan_block (lam : R) n :
char_poly (Jordan_block lam n) = ('X - lam%:P) ^+n.

End trigonal.

Section similar.

Variable R : fieldType.
Import GRing.Theory.
Import PolyPriField.
Local Open Scope ring_scope.

Lemma similar_cj n (lam : R) :
similar (companion_mx (('X - lam%:P)^+ n.+1)) (Jordan_block lam n.+1).

End similar.

Section jordan.

Variable R : closedFieldType.
Import GRing.Theory.
Import PolyPriField.
Local Open Scope ring_scope.

Definition Jordan_form m (A : 'M[R]_m.+1) :=
let sp := root_seq_poly (invariant_factors A) in
let sizes := [seq (x.2).-1 | x <- sp] in
let blocks n i := Jordan_block (nth (0,0%N) sp i).1 n.+1 in
diag_block_mx sizes blocks.

Lemma upt_Jordan n (A : 'M[R]_n.+1) :
upper_triangular_mx (Jordan_form A).

Lemma Jordan n (A : 'M[R]_n.+1) : similar A (Jordan_form A).

Lemma Jordan_char_poly n (A : 'M_n.+1) :
char_poly A = \prod_i ('X - ((Jordan_form A) i i)%:P).

Lemma eigen_diag n (A : 'M_n.+1) :
let sp := root_seq_poly (invariant_factors A) in
let sizes := [seq (x.2).-1 | x <- sp] in
perm_eq [seq (Jordan_form A) i i | i <- enum 'I_(size_sum sizes).+1]
(root_seq (char_poly A)).

Lemma diagonalization n (A : 'M[R]_n.+1) : uniq (root_seq (mxminpoly A)) ->
similar A (diag_mx_seq n.+1 n.+1 (root_seq (char_poly A))).

Lemma ex_diagonalization n (A : 'M[R]_n.+1) : uniq (root_seq (mxminpoly A)) ->
{s | similar A (diag_mx_seq n.+1 n.+1 s)}.

End jordan.