proposition: Lemma map_section_repr n (rG : mx_representation aF G n) rGf U V (modU : mxmodule rG U) (modV : mxmodule rG V) (modUf : mxmodule rGf U^f) (modVf : mxmodule rGf V^f) : map_repr f rG =1 rGf -> mx_rsim (map_repr f (section_repr modU modV)) (section_repr modUf modVf).
proof: Proof. move=> def_rGf; set VU := <<_>>%MS. pose valUV := val_factmod (val_submod (1%:M : 'M[aF]_(\rank VU))). have sUV_Uf: (valUV^f <= U^f + V^f)%MS. rewrite -map_addsmx map_submx; apply: submx_trans (proj_factmodS _ _). by rewrite val_factmodS val_submod1 genmxE. exists (in_submod _ (in_factmod U^f valUV^f)) => [||x Gx]. - rewrite !genmxE -(mxrank_map f) map_mxM map_col_base. by case: (\rank (cokermx U)) / (mxrank_map _ _); rewrite map_cokermx. - rewrite -kermx_eq0 -submx0; apply/rV_subP=> u. rewrite (sameP sub_kermxP eqP) submx0 -val_submod_eq0. rewrite val_submodE -mulmxA -val_submodE in_submodK; last first. by rewrite genmxE -(in_factmod_addsK _ V^f) submxMr. rewrite in_factmodE mulmxA -in_factmodE in_factmod_eq0. move/(submxMr (in_factmod U 1%:M *m in_submod VU 1%:M)^f). rewrite -mulmxA -!map_mxM //; do 2!rewrite mulmxA -in_factmodE -in_submodE. rewrite val_factmodK val_submodK map_mx1 mulmx1. have ->: in_factmod U U = 0 by apply/eqP; rewrite in_factmod_eq0. by rewrite linear0 map_mx0 eqmx0 submx0. rewrite {1}in_submodE mulmxA -in_submodE -in_submodJ; last first. by rewrite genmxE -(in_factmod_addsK _ V^f) submxMr. congr (in_submod _ _); rewrite -in_factmodJ // in_factmodE mulmxA -in_factmodE. apply/eqP; rewrite -subr_eq0 -def_rGf -!map_mxM -linearB in_factmod_eq0. rewrite -map_mxB map_submx -in_factmod_eq0 linearB. rewrite /= (in_factmodJ modU) // val_factmodK. rewrite [valUV]val_factmodE mulmxA -val_factmodE val_factmodK. rewrite -val_submodE in_submodK ?subrr //. by rewrite mxmodule_trans ?section_module // val_submod1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)