Library similar

Require Import ssreflect ssrfun ssrbool eqtype fintype finfun ssrnat seq.
Require Import choice ssralg poly polydiv mxpoly matrix bigop.
Require Import mxalgebra perm fingroup tuple.
Require Import mxstructure ssrcomplements dvdring.

Set Implicit Arguments.

Section SimilarDef.

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

Definition similar m n (A : 'M[R]_m) (B : 'M[R]_n) :=
   m = n /\ exists P, P \in unitmx /\ P *m A = (conform_mx P B) *m P.

Lemma similar0 m (A : 'M[R]_0) (B : 'M[R]_m) : (0 = m)%N -> similar A B.

Lemma similar_sym m : forall n (A : 'M[R]_m) (B : 'M[R]_n),
  similar A B -> similar B A.

Lemma similar_trans m n p (B : 'M[R]_n) (A : 'M[R]_m) (C : 'M[R]_p) :
  similar A B -> similar B C -> similar A C.

Lemma similar_refl n (A : 'M[R]_n) : similar A A.

Lemma similar_det m n (A : 'M[R]_m) (B : 'M[R]_n) :
  similar A B -> \det A = \det B.

Lemma similar_cast n m p (eq1 : m = p) (eq2 : m = p)
  (A : 'M[R]_n) (B : 'M[R]_m) :
  similar A (castmx (eq1,eq2) B) <-> similar A B.

Lemma similar_diag_mx_seq m n s1 s2 :
  m = n -> size s1 = m -> perm_eq s1 s2 ->
similar (diag_mx_seq m m s1) (diag_mx_seq n n s2).

Lemma similar_ulblockmx n1 n2 n3 (Aul : 'M[R]_n1) (Adr : 'M[R]_n3)
  (Bul : 'M[R]_n2) :
  similar Aul Bul ->
  similar (block_mx Aul 0 0 Adr) (block_mx Bul 0 0 Adr).

Lemma similar_drblockmx n1 n2 n3(Aul : 'M[R]_n1) (Adr : 'M[R]_n2)
  (Bdr : 'M[R]_n3) :
  similar Adr Bdr ->
  similar (block_mx Aul 0 0 Adr) (block_mx Aul 0 0 Bdr).

Lemma similar_dgblockmx n1 n2 n3 n4 (Aul : 'M[R]_n1) (Adr : 'M[R]_n2)
  (Bul : 'M[R]_n3) (Bdr : 'M[R]_n4) :
  similar Aul Bul -> similar Adr Bdr ->
  similar (block_mx Aul 0 0 Adr) (block_mx Bul 0 0 Bdr).

Lemma similar_exp m n (A : 'M[R]_m.+1) (B : 'M_n.+1) k:
  similar A B -> similar (A ^+ k) (B ^+ k).

Lemma similar_poly m n (A : 'M[R]_m.+1) (B : 'M_n.+1) p:
  similar A B -> similar (horner_mx A p) (horner_mx B p).

Lemma similar_horner n m (A : 'M[R]_n.+1) (B : 'M_m.+1) p :
  similar A B -> horner_mx A p = 0 -> horner_mx B p = 0.

Lemma similar_diag_block : forall l1 l2, size l1 = size l2 ->
   forall (F1 F2 : forall n : nat, nat -> 'M[R]_n.+1),
   (forall i, i < size l1 ->
    similar (F1 (nth 0%N l1 i) i) (F2 (nth 0%N l2 i) i)) ->
   similar (diag_block_mx l1 F1) (diag_block_mx l2 F2).

End SimilarDef.

Section EquivalentDef.

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

Definition equivalent m1 n1 m2 n2 (A : 'M[R]_(m1,n1)) (B : 'M[R]_(m2,n2)) :=
  [/\ m1 = m2, n1 = n2 & exists M, exists N,
  [/\ M \in unitmx , N \in unitmx & M *m A *m N = conform_mx A B]].

Lemma equiv0l n m p (A : 'M[R]_(0,n)) (B : 'M[R]_(m,p)) :
 (0 = m)%N -> (n = p)%N -> equivalent A B.

Lemma equiv0r n m p (A : 'M[R]_(n,0)) (B : 'M[R]_(m,p)) :
 (n = m)%N -> (0 = p)%N -> equivalent A B.

Lemma similar_equiv m n (A : 'M_m) (B : 'M_n) : similar A B -> equivalent A B.

Lemma equiv_refl m n (A : 'M[R]_(m,n)) : equivalent A A.

Lemma equiv_sym m1 n1 m2 n2 (A : 'M[R]_(m1,n1)) (B : 'M[R]_(m2,n2)) :
  equivalent A B -> equivalent B A.

Lemma equiv_trans m1 n1 m2 n2 m3 n3 (B : 'M[R]_(m2,n2))
  (A : 'M[R]_(m1,n1)) (C : 'M[R]_(m3,n3)) :
  equivalent A B -> equivalent B C -> equivalent A C.

Lemma equiv_ulblockmx m1 n1 m2 n2 m3 n3 (Aul : 'M[R]_(m1,n1))
 (Adr : 'M[R]_(m2,n2)) (Bul : 'M[R]_(m3,n3)) :
  equivalent Aul Bul ->
  equivalent (block_mx Aul 0 0 Adr) (block_mx Bul 0 0 Adr).

Lemma equiv_drblockmx m1 n1 m2 n2 m3 n3 (Aul : 'M[R]_(m1,n1))
  (Adr : 'M[R]_(m2,n2)) (Bdr : 'M[R]_(m3,n3)) :
   equivalent Adr Bdr ->
   equivalent (block_mx Aul 0 0 Adr) (block_mx Aul 0 0 Bdr).

Lemma equiv_dgblockmx m1 n1 m2 n2 m3 n3 m4 n4
  (Aul : 'M[R]_(m1,n1)) (Adr : 'M[R]_(m2,n2))
  (Bul : 'M[R]_(m3,n3)) (Bdr : 'M[R]_(m4,n4)) :
  equivalent Aul Bul -> equivalent Adr Bdr ->
  equivalent (block_mx Aul 0 0 Adr) (block_mx Bul 0 0 Bdr).

Lemma equiv_cast m1 n1 m2 n2 m3 n3 (eqm : m2 = m3) (eqn : n2 = n3)
 (A : 'M[R]_(m1,n1)) (B : 'M[R]_(m2,n2)) :
  equivalent A (castmx (eqm,eqn) B) <-> equivalent A B.

Lemma equiv_diag_block : forall l1 l2, size l1 = size l2 ->
   forall (F1 F2 : forall n : nat, nat -> 'M_n.+1),
   (forall i, i < size l1->
    equivalent (F1 (nth 0%N l1 i) i) (F2 (nth 0%N l2 i) i)) ->
   equivalent (diag_block_mx l1 F1) (diag_block_mx l2 F2).

End EquivalentDef.

Section Field.

Import GRing.Theory.
Import polydiv.Pdiv.Ring.
Import RPdiv.
Import polydiv.Pdiv.RingMonic.
Import RPdiv.mon.

Variables R : fieldType.
Variable m n : nat.
Local Open Scope ring_scope.

Theorem similar_fundamental (A: 'M[R]_m) (B : 'M[R]_n) :
  similar A B <-> equivalent (char_poly_mx A) (char_poly_mx B).

Lemma similar_mxminpoly m' n' (A : 'M[R]_m'.+1) (B : 'M[R]_n'.+1) :
   similar A B -> mxminpoly A = mxminpoly B.

Lemma similar_char_poly m' n' (A : 'M[R]_m') (B : 'M[R]_n') :
    similar A B -> char_poly A = char_poly B.

End Field.

Section DvdRing.

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

Lemma eqd_equiv n m n' m' (s1 s2 : seq R) : n = n' -> m = m' ->
   size s1 = size s2 -> (forall i, nth 0 s1 i %= nth 0 s2 i) ->
   equivalent (diag_mx_seq n m s1) (diag_mx_seq n' m' s2).

End DvdRing.