proposition: Theorem similar_fundamental (A: 'M[R]_m) (B : 'M[R]_n) : similar A B <-> equivalent (char_poly_mx A) (char_poly_mx B).
proof: Proof. constructor. case: n B=> [B [eq _]|n' B]; first by apply/equiv_sym/equiv0l/esym. case: m A=> [A [eq _]|m' A]; first exact: equiv0l. case=> eq [P HP HPA]; split=> //. move: A P HP HPA; rewrite eq=> A P HP; rewrite !conform_mx_id=> HPA. pose M := map_mx polyC P. pose N := map_mx polyC P^-1. have HM: M \in unitmx by rewrite map_unitmx. exists M, N; split=> //; first by rewrite map_unitmx unitmx_inv. rewrite mulmxBr mulmxBl mul_mx_scalar -scalemxAl /M /N map_mx_inv. rewrite (mulmxV HM) scalemx1 -map_mxM HPA -map_mx_inv -map_mxM. by rewrite -mulmxA (mulmxV HP) mulmx1. case:n B=> [B [eq _ _]|n' B]; first by apply/similar_sym/similar0/esym. case: m A=> [A [eq _ _]|m' A]; first exact: similar0. case=> eq _ [M [N [HM HN HA]]]; split=> //. move: A M N HM HN HA; rewrite eq=> A M N HM HN; rewrite conform_mx_id=> HA. have [phi [phi_bij phiZ phiC phiG]] := mx_poly_ring_isom R n'. have: phi M * phi (char_poly_mx A) * phi N = phi (char_poly_mx B). by rewrite -!rmorphM -mulmxE HA. rewrite !{1}rmorphB phiZ !phiC map_polyX=> H. have HphiM: phi M * ('X - A%:P) = ('X - B%:P) * phi N^-1. by rewrite -H -!mulrA -rmorphM mulrV // rmorph1 mulr1. have HphiN: ('X - A%:P) * phi N = phi M^-1 * ('X - B%:P). by rewrite -H !mulrA -rmorphM -mulmxE (mulVmx HM) rmorph1 mul1r. pose M0 := rmodp_l (phi M) ('X - B%:P). pose N0 := rmodp (phi N) ('X - B%:P). pose M1 := rdivp_l (phi M) ('X - B%:P). pose N1 := rdivp (phi N) ('X - B%:P). pose R1 := M1 * phi M^-1 + phi N^-1 * N1 - M1 * ('X - A%:P) * N1. have {}H: M0 * ('X - A%:P) * N0 = (1 - ('X - B%:P) * R1) * ('X - B%:P). have HM1: ('X - B%:P) * M1 = phi M - M0. by rewrite [phi M](rdivp_l_eq (monicXsubC B)) addrK. have HN1: N1 * ('X - B%:P) = phi N - N0. by rewrite [phi N](rdivp_eq (monicXsubC B)) addrK. rewrite /R1 (mulrBr (_ - B%:P)) (mulrDr (_ - B%:P)) !mulrA HM1 mulrBl 2!mulrDl. rewrite mulNr -![_ * N1 * _]mulrA HN1 2!mulrBl. rewrite ![_ * (phi N - N0)]mulrBr ![(phi M - M0) * _]mulrBl. rewrite -[_ * _ * phi N]mulrA -!rmorphM divrr // mulVr // !rmorph1 !mulr1. rewrite mul1r [_ * phi N]mulrBl [(_ - _) * N0]mulrBl H [X in _ = _ + X]opprD. rewrite [X in _ + (X - _)]opprD [X in _ + ((X - _) - _)]opprD !opprK. rewrite !addrA addrN add0r -{1 3}H. rewrite !mulrA -[_ * _ * phi M]mulrA -[_ * _ * phi N^-1]mulrA -!rmorphM. rewrite divrr // mulVr // !rmorph1 !mulr1 opprB addrA. rewrite -{1}[_ + _ - B%:P]addrA subrK (addrC (M0 * _ * _)) addrK. by rewrite opprD opprK addrA addrN add0r. have HM0: size M0 <= 1. by rewrite -ltnS -[leqRHS](size_XsubC B) ltn_rmodp_l polyXsubC_eq0. have HN0: size N0 <= 1. by rewrite -ltnS -[leqRHS](size_XsubC B) ltn_rmodp polyXsubC_eq0. case: (eqVneq R1 0) => HR1; last first. have: size ((1 - ('X - B%:P) * R1) * ('X - B%:P)) <= 2. rewrite -H; apply:(leq_trans (size_mul_leq _ _)). rewrite (size1_polyC HN0) size_polyC -subn1 leq_subLR addnC. apply/(leq_add (leq_b1 _))/(leq_trans (size_mul_leq _ _)). by rewrite (size1_polyC HM0) size_polyC size_XsubC addnC; exact:leq_b1. have Hsize: size (1 - ('X - B%:P) * R1) = (size R1).+1. rewrite addrC size_addl size_opp (size_monicM (monicXsubC B) HR1). by rewrite {1}size_XsubC. rewrite size_polyC oner_neq0 size_XsubC. by move:(size_poly_eq0 R1); case:(size R1)=> //; rewrite (negbTE HR1). rewrite size_Mmonic. + by rewrite Hsize size_XsubC addnC !ltnS leqn0 size_poly_eq0 (negbTE HR1). + by rewrite -size_poly_eq0 Hsize. exact: monicXsubC. move:H; rewrite HR1 mulr0 subr0 mul1r (size1_polyC HM0). rewrite (size1_polyC HN0)=> /polyP H; move:(H 1%N); move:(H 0%N). rewrite !coefMC !coefCM !coefD !coefN !coefC !coefX !eqxx !sub0r subr0 mulr1. rewrite mulrN mulNr; move/eqP; rewrite eqr_opp=> /eqP HM0N0 HM0N0I. case:(mulmx1_unit HM0N0I)=> HM00 HN00. exists (M0`_0) => //; rewrite conform_mx_id -HM0N0 mulmxE -(divr1 N0`_0). by rewrite -[1]HM0N0I invrM // mulrA divrr // mul1r -!mulrA mulVr // mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype fintype finfun ssrnat seq) mathcomp(choice ssralg poly polydiv mxpoly matrix bigop) mathcomp(mxalgebra perm fingroup tuple) mxstructure dvdring