proposition: Lemma minor_diag_mx_seq : forall (f g : 'I_k -> 'I_(minn m n)), injective f -> injective g -> {subset codom f <= codom g} -> minor (widen_minl \o f) (widen_minr \o g) (diag_mx_seq m n s) %= \prod_i s`_(f i).
proof: Proof. elim: k=>[f g|j IHj f g Hf Hg Hfg]; first by rewrite /minor det_mx00 big_ord0. have: perm_eq [seq f x | x in 'I_j.+1] [seq g x | x in 'I_j.+1]. have [||_ e] := uniq_min_size _ Hfg; first by rewrite map_inj_uniq ?enum_uniq. by rewrite !size_map. by rewrite uniq_perm // map_inj_uniq // enum_uniq. have Ht : size (codom g) == j.+1 by rewrite size_codom card_ord. have -> : image g 'I_j.+1 = Tuple Ht by []. case/tuple_permP=> p Hp . have Hfg0 i : g (p i) = f i. have He : i < #|'I_j.+1| by rewrite card_ord. have {2}-> : i = enum_val (Ordinal He) by rewrite enum_val_ord; apply: ord_inj. rewrite -(nth_image (f ord0)) Hp -tnth_nth tnth_mktuple (tnth_nth (f ord0)). by rewrite /= codomE (nth_map ord0) ?nth_ord_enum // size_enum_ord. rewrite /minor (expand_det_row _ ((p^-1)%g ord0)) big_ord_recl big1=>[|i _]; last first. rewrite !mxE /= (inj_eq (@ord_inj _)) -Hfg0 (inj_eq Hg) permKV. by rewrite (negbTE (neq_lift _ _)) mul0r. rewrite /cofactor !mxE /=; set B := diag_mx_seq _ _ _; set M := row' _ _. set p0 := ((p^-1)%g ord0). pose f2 x := f (lift p0 x); pose g2 x := g (lift ord0 x). have Hf2 : injective f2 by apply/(inj_comp Hf)/lift_inj. have Hg2 : injective g2 by apply/(inj_comp Hg)/lift_inj. pose f' i := widen_ord (geq_minl m n) (f2 i). pose g' i := widen_ord (geq_minr m n) (g2 i). have -> : M = submatrix f' g' B by apply/matrixP=> r t; rewrite !mxE. have Hfg2 : {subset codom f2 <= codom g2}. move=> x /codomP [y ->]. rewrite codomE /f2 /g2 -Hfg0 map_comp (mem_map Hg). have: p (lift p0 y) \in enum 'I_j.+1 by rewrite mem_enum. rewrite enum_ordSl in_cons -(permKV p ord0). by rewrite (inj_eq (@perm_inj _ _)) eq_sym (negbTE (neq_lift _ _)). rewrite addr0 (bigD1 ((p^-1)%g ord0)) //= -Hfg0 permKV eqxx eqd_mull //. rewrite -[X in _ %= X]mul1r eqd_mul ?eqd1 ?unitrX ?unitrN ?unitr1 //. rewrite (eq_bigl (fun i => p0 != i)); last by move=> i /=; rewrite eq_sym. apply: (eqd_trans (IHj _ _ Hf2 Hg2 Hfg2)); apply: eq_eqd; rewrite /f2. case: (pickP 'I_j) => [k0 _ | n0]; last first. by rewrite !big1 // => [k' /unlift_some[i] | i _]; have:= n0 i. rewrite (reindex (lift p0)); first by apply: eq_bigl=> k'; rewrite neq_lift. exists (fun k => odflt k0 (unlift p0 k)) => k'; first by rewrite liftK. by case/unlift_some=> k'' -> ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path tuple) mathcomp(perm fingroup choice ssralg fintype finfun poly polydiv) mathcomp(bigop matrix zmodp mxalgebra) ssrcomplements dvdring mxstructure similar minor binetcauchy stronglydiscrete coherent