Library smith_complements
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq perm fingroup.
Require Import ssralg path fintype finfun poly polydiv bigop matrix zmodp.
Require Import mxtens similar ssrcomplements mxstructure tuple.
Require Import minor binetcauchy smith.
Require Import dvdring polydvd.
Require Import ssralg path fintype finfun poly polydiv bigop matrix zmodp.
Require Import mxtens similar ssrcomplements mxstructure tuple.
Require Import minor binetcauchy smith.
Require Import dvdring polydvd.
This file is a complement of the file Smith.v of the CoqEAL library.
We prove here the unicity of the Smith normal form of a matrix.
The algorithm described in the file Smith.v takes a matrix M of
type 'M_(m,n) and returns a triple (L,s,R) where s is the
sequence such that diag_mx_seq m n s is the Smith normal
form of M, and L and R are the transition matrices
(i.e diag_mx_seq m n s = L * M * R). In this context we have
the following definitions :
Smith_seq M == The sequence s of the triple (L,s,R).
Smith_form M == diag_mx_seq m n (Smith_seq M).
Set Implicit Arguments.
Section Specification.
Local Open Scope ring_scope.
Import GRing.Theory.
Variable E : euclidRingType.
Definition Smith_seq n m (M: 'M[E]_(n,m)) :=
let: (L,d,R) := (Smith _ M) in
if d is a :: d' then (\det L)^-1 * (\det R)^-1 *a :: d' else nil.
Definition Smith_form n m (M: 'M[E]_(n,m)) :=
diag_mx_seq n m (Smith_seq M).
Lemma equiv_Smith n m (M: 'M[E]_(n,m)) : equivalent M (Smith_form M).
Lemma sorted_Smith n m (M: 'M[E]_(n,m)):
sorted (@dvdr E) (Smith_seq M).
Lemma det_Smith n (M: 'M[E]_n) : \det (Smith_form M) = \det M.
Lemma size_Smith_seq n (M: 'M[E]_n) :
\det M != 0 -> size (take n (Smith_seq M)) = n.
End Specification.
Section Preunicity.
Import GRing.Theory.
Import PolyPriField.
Variable E : euclidRingType.
Variables (s : seq E) (m n k : nat) (A : 'M[E]_(m,n)).
Hypothesis (Hk : k <= minn m n) (Hs: sorted %|%R s).
Hypothesis (HAs : equivalent A (diag_mx_seq m n s)).
Let widen_minl i := widen_ord (geq_minl m n) i.
Let widen_minr i := widen_ord (geq_minr m n) i.
Lemma minor_diag_mx_seq :
let l := minn m n in
forall (f g : 'I_k -> 'I_l),
let f' i := widen_minl (f i) in
let g' i := widen_minr (g i) in
injective f -> injective g -> {subset codom f <= codom g} ->
minor k f' g' (diag_mx_seq m n s) %= \prod_i s`_(f i).
Lemma prod_minor_seq :
\prod_(i < k) s`_i =
minor k [ffun x : 'I_k => widen_minl (widen_ord Hk x)]
[ffun x : 'I_k => widen_minr (widen_ord Hk x)] (diag_mx_seq m n s).
Lemma minor_eq0l (R : comRingType) k1 m1 n1 (s1 : seq R) x :
forall (f : 'I_k1 -> 'I_m1) g, n1 <= f x ->
minor k1 f g (diag_mx_seq m1 n1 s1) = 0.
Lemma minor_eq0r (R : comRingType) k1 m1 n1 (s1 : seq R) x :
forall f (g : 'I_k1 -> 'I_n1) , m1 <= g x ->
minor k1 f g (diag_mx_seq m1 n1 s1) = 0.
Lemma eqd_seq_gcdr :
\prod_(i < k) s`_i %=
\big[(@gcdr E)/0]_(f : {ffun 'I_k -> 'I_m})
(\big[(@gcdr E)/0]_(g : {ffun 'I_k -> 'I_n}) minor k f g (diag_mx_seq m n s)).
Lemma Smith_gcdr_spec :
\prod_(i < k) s`_i %=
\big[(@gcdr E)/0]_(f : {ffun 'I_k -> 'I_m})
(\big[(@gcdr E)/0]_(g : {ffun 'I_k -> 'I_n}) minor k f g A) .
End Preunicity.
Section Unicity.
Import GRing.Theory.
Import PolyPriField.
Variable E : euclidRingType.
Lemma Smith_unicity n (A : 'M[E]_n) (s : seq E) :
sorted %|%R s -> equivalent A (diag_mx_seq n n s) ->
forall i, i < n -> s`_i %= (Smith_seq A)`_i.
End Unicity.
This page has been generated by coqdoc