proposition: 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))%N -> p \is monic -> similar (companion_mx p) (diag_block_mx size_seq blocks).
proof: Proof. move=> /= Hp1 Hmp. move: (@coprimep_linear_factor_seq _ p). move: (@monic_linear_factor_seq _ p). move: (@size_linear_factor_leq1 _ p). move: Hmp Hp1 (monic_prod_factor Hmp). elim: (linear_factor_seq p) {1 2 3 14 16}p. move=> p0 Hmp0 Hsp0; rewrite big_nil=> H. by rewrite H size_poly1 in Hsp0. move=> a; case=> [_ p1 _ _ Hp1 _ _ _ | b l IHl p1 Hmp1 Hsp1 Hp1 Hs Hm Hcp] /=. rewrite Hp1 big_cons big_nil mulr1. by apply: similar_refl. have Hicp : forall i j : 'I_(size (b :: l)), i != j -> coprimep (b :: l)`_i (b :: l)`_j. move=> i j H. have Hij: (lift ord0 i) != (lift ord0 j). by apply/val_eqP=> /lift_inj; apply/eqP. by move: (Hcp _ _ Hij); rewrite -!nth_behead. pose p2:= p1 %/ a. have Hma: a \is monic by apply: Hm; rewrite mem_head. have Hsa: (1 < size a)%N by apply: Hs; rewrite mem_head. have Hp2: p2 = \prod_(x <- (b :: l)) x. by rewrite /p2 Hp1 big_cons divr_mulKr // monic_neq0. have Hml: forall x, x \in (b :: l) -> x \is monic. by move=> x Hx; apply: Hm; rewrite mem_behead. have Hsl: forall x, x \in b :: l -> (1 < size x)%N. by move=> x Hx; apply: Hs; rewrite mem_behead. have {Hs} Hsb: (1 < size b)%N by apply: Hsl; rewrite mem_head. have {Hm} Hmb: b \is monic by apply: Hml; rewrite mem_head. have {Hp1} Hp12: p1 = a * p2 by rewrite Hp1 Hp2 big_cons. have Hmp2: p2 \is monic by rewrite -(monicMl _ Hma) -Hp12. have sp1gt0 : (0 < size (1%:P : {poly R}))%N by rewrite size_poly1. have mgt0 (x y : {poly R}) : (0 < size x -> 0 < size y -> 0 < size (x * y)%R)%N. by move=> sx sy; rewrite size_mul -?size_poly_eq0; move: sx sy; case: (size x); case: (size y) => // n1 n2; rewrite ?addnS. have {Hsb Hmb} Hsp2: (1 < size p2)%N. rewrite Hp2 big_cons size_proper_mul. rewrite -subn1 -addnBA ?ltn_addr //. rewrite big_seq. apply: (big_ind (fun (p : {poly R}) => (0 < size p)%N) sp1gt0 mgt0)=> q Hq. have: (1 < size q)%N by apply: Hsl; rewrite mem_behead. by apply: ltn_trans. move/monicP: Hmb => ->; rewrite mul1r lead_coef_eq0 -size_poly_leq0. rewrite -ltnNge big_seq. apply: (big_ind (fun (p : {poly R}) => (0 < size p)%N) sp1gt0 mgt0)=> q Hq. have: (1 < size q)%N by apply: Hsl; rewrite mem_behead. by apply: ltn_trans. move=> {sp1gt0 mgt0}. apply: (@similar_trans _ _ _ _ (block_mx (companion_mx a) 0 0 (companion_mx p2))); last first. by apply: (similar_drblockmx _ (IHl _ Hmp2 Hsp2 Hp2 Hsl Hml Hicp)). have {Hp2 Hml Hsl Hcp Hicp IHl} Hcap: coprimep a p2. have copa1 : coprimep a 1%P by apply: coprimep1. have copaxy (x y : {poly R}) : coprimep a x -> coprimep a y -> coprimep a (x * y)%R. by rewrite coprimepMr=> -> ->. rewrite Hp2 big_seq. apply: (big_ind (fun p => coprimep a p)). + by apply: coprimep1. + by move=> x y; rewrite coprimepMr => -> ->. move=> i iin; move/(nth_index 0): (iin)=> iid. move: (iin); rewrite -index_mem -ltnS=> ii_prf. set j := Ordinal ii_prf. have vi : [:: a, b & l]`_j = i by apply: (nth_index 0 iin). by have := Hcp ord0 j isT; rewrite vi /=. apply/similar_fundamental. apply: (equiv_trans (equiv_Smith _)). apply: (equiv_trans (Smith_companion Hsp1 Hmp1)). rewrite Hp12 char_dblock_mx. apply: (@equiv_trans _ _ _ _ _ _ _ (block_mx (diag_mx_seq (size a).-2.+1 (size a).-2.+1 (rcons (nseq (size a).-2 1) a)) 0 0 (diag_mx_seq (size p2).-2.+1 (size p2).-2.+1 (rcons (nseq (size p2).-2 1) p2)))); last first. apply: equiv_dgblockmx; apply: equiv_sym; set C := char_poly_mx _ . by apply: (equiv_trans (equiv_Smith C)); apply: Smith_companion. by apply: (equiv_trans (equiv_Smith C)); apply: Smith_companion. rewrite -diag_mx_seq_cat ?size_rcons ?size_nseq //. set M := diag_mx_seq _ _ (_ ++ _). set sap := (size (a * p2)).-2.+1. set sa := (size a).-2.+1. set sp := (size p2).-2.+1. have Hcast: sap = (sa + sp)%N. rewrite /sap /sa /sp size_proper_mul. rewrite -!subn1 -addnBA; last by rewrite ltnW. rewrite addnC -addnBA; last by rewrite ltnW. rewrite -addnBA ?subn_gt0 // addSn addnC !subn1 (@prednK (_.-1)) //. by rewrite -subn1 subn_gt0. by move/monicP: Hma; move/monicP: Hmp2=> -> ->; rewrite mulr1 oner_eq0. have HdetM: \det M = p1. rewrite det_diag_mx_seq ?size_cat ?size_rcons ?size_nseq //. rewrite -!cats1 !big_cat /= !big_cons !big_nil. rewrite !big1_seq=> [|i|i]; try by rewrite mem_nseq => /= /andP[] _ /eqP. by rewrite !mul1r !mulr1 -Hp12. have Ho: (sa.-1 < (sa + sp).-1)%N by rewrite prednK // addnS leq_addr. have HM1: row' (Ordinal Ho) (col' (Ordinal Ho) (row' ord_max (col' ord_max M))) = 1%:M. apply/matrixP=> j k; rewrite !mxE !lift_max. rewrite nth_cat size_rcons size_nseq. case: ifP; rewrite nth_rcons size_nseq. rewrite ltnS leq_eqVlt eq_sym (negbTE (neq_bump _ _)) /= => Hb. by rewrite Hb nth_nseq Hb eqn_leq !leq_bump2 -eqn_leq. move/negbT;rewrite -leqNgt=> Hb. have Hb2: (bump (size a).-2 j - (size a).-2.+1 < (size p2).-2)%N. rewrite -(ltn_add2r sa _ _.-2) subnK //. by rewrite (leq_trans (ltn_ord (lift (Ordinal Ho) j))) // addnC addSn. by rewrite Hb2 nth_nseq Hb2 eqn_leq !leq_bump2 -eqn_leq. apply/equiv_sym/(equiv_trans (equiv_Smith M)). rewrite /Smith_form -diag_mx_seq_takel. set s := take _ _. have Hs1: size s = sap by rewrite Hcast size_Smith_seq // HdetM monic_neq0. apply: eqd_equiv=> // [|i]; first by rewrite size_rcons size_nseq. have Hle: (sap.-2 <= sa + sp)%N by rewrite -Hcast -subn2 leq_subr. have Hsort: sorted (@dvdr _) s. by apply/(sorted_take (@dvdr_trans _))/sorted_Smith. have:= (equiv_Smith M). rewrite /Smith_form -diag_mx_seq_takel=> Hequiv. have Hle2: (sap.-2 < minn (sa + sp) (sa + sp))%N by rewrite minnn Hcast addnS addSn. have:= Smith_gcdr_spec Hle2 Hsort Hequiv. set d2 := \big[_/_]_(_<_) _=> H2. have {H2} Hd2: d2 %= 1. apply/(eqd_trans H2); rewrite /eqd !dvdr_dvdp. apply: (coprimepP _ _ Hcap); rewrite -dvdr_dvdp. + apply: big_gcdr_def; rewrite Hcast prednK ?addnS ?addSn //. exists (finfun (lift (@ord_max (sa + sp).-1))). apply: big_gcdr_def. exists (finfun (lift (@ord_max (sa + sp).-1))). rewrite /minor.minor /minor.submatrix /=. rewrite (expand_det_row _ (Ordinal Ho)) (bigD1 (Ordinal Ho)) //=. rewrite !mxE !ffunE big1 ?addr0. rewrite nth_cat size_rcons size_nseq lift_max /=. rewrite ltnS leqnn nth_rcons size_nseq ltnn eqxx. rewrite /cofactor exprD -expr2 sqrr_sign mul1r. set N:= row' _ _. have ->: N = 1%:M. by rewrite -HM1; apply/matrixP=> j k; rewrite !mxE !ffunE !lift_max. by rewrite det1 mulr1. move=> j /negbTE Hj; rewrite !mxE !ffunE. by rewrite (inj_eq (@ord_inj _)) (inj_eq (@lift_inj _ _)) eq_sym Hj mul0r. have Ho2: (sa .-1 < sa + sp)%N by rewrite prednK // leq_addr. apply: big_gcdr_def; rewrite Hcast prednK ?addnS ?addSn //. exists (finfun (lift (Ordinal Ho2))). apply: big_gcdr_def. exists (finfun (lift (Ordinal Ho2))). rewrite /minor.minor /minor.submatrix /=. have Hom: ((size a).-2 + (size p2).-2 < (size a).-2 + sp)%N by rewrite addnS. have Hlom k : lift (Ordinal Hom) k = widen_ord (leq_pred _) k. apply: ord_inj=> /=; rewrite /bump leqNgt. by rewrite (leq_trans (ltn_ord k)) // addnS leqnn. rewrite (expand_det_row _ (Ordinal Hom)). rewrite (bigD1 (Ordinal Hom)) //= big1 ?addr0. rewrite !mxE !ffunE /= -[X in bump X _]addn0 bumpDl /bump leq0n /=. rewrite nth_cat size_rcons size_nseq ltnS add1n {1}addnS. rewrite ltnNge leq_addr /= nth_rcons size_nseq. rewrite {1 3}addnS !subSS !addKn !ltnn !eqxx. rewrite /cofactor exprD -expr2 sqrr_sign mul1r. set N:= row' _ _. have ->: N = 1%:M. rewrite -HM1; apply/matrixP=> j k. by rewrite !mxE !ffunE !lift_max !Hlom /=. by rewrite det1 mulr1. move=> j /negbTE Hj; rewrite !mxE !ffunE (inj_eq (@ord_inj _)). by rewrite (inj_eq (@lift_inj _ _)) eq_sym Hj mul0r. have Hsp: s`_sap.-1 %= p1. rewrite eqd_sym in Hd2. rewrite -(mul1r s`_sap.-1) (eqd_ltrans (eqd_mulr _ Hd2)). rewrite -HdetM -det_Smith /Smith_form -diag_mx_seq_takel det_diag_mx_seq. rewrite (big_nth 0) big_mkord Hs1 big_ord_recr /=. by apply: eqd_mul=> //; rewrite /d2 prednK // Hcast addnS addSn. by rewrite Hs1 Hcast. move/eqd_big_mul1: Hd2=> H. have [Hi|Hi|/eqP Hi] := (ltngtP i sap.-1). + have Hi2: (i < sap.-2.+1)%N by rewrite prednK // Hcast addnS addSn. rewrite nth_rcons size_nseq Hi nth_nseq Hi. exact: (H (Ordinal Hi2)). by rewrite !nth_default // ?Hs1 // size_rcons size_nseq. by rewrite nth_rcons size_nseq Hi (eqP Hi) ltnn -Hp12. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image companion closed_poly smith_complements)