proposition: Lemma mx_poly_ring_isom (R : ringType) n' (n := n'.+1) : exists phi : {rmorphism 'M[{poly R}]_n -> {poly 'M[R]_n}}, [/\ bijective phi, forall p, phi p%:M = map_poly scalar_mx p, forall A, phi (map_mx polyC A) = A%:P & forall A i j k, (phi A)`_k i j = (A i j)`_k].
proof: Proof. set M_RX := 'M[{poly R}]_n; set MR_X := ({poly 'M[R]_n}). pose Msize (A : M_RX) := \max_i \max_j size (A i j). pose phi (A : M_RX) := \poly_(k < Msize A) \matrix_(i, j) (A i j)`_k. have coef_phi A i j k: (phi A)`_k i j = (A i j)`_k. rewrite coef_poly; case: (ltnP k _) => le_m_k; rewrite mxE // nth_default //. by apply: leq_trans (leq_trans (leq_bigmax i) le_m_k); apply: (leq_bigmax j). have phi_is_additive : additive phi. move=> A B; apply/polyP => k; apply/matrixP => i j. by rewrite !(coef_phi, mxE, coefD, coefN). have phi_is_multiplicative : multiplicative phi. split=> [A B|]; apply/polyP => k; apply/matrixP => i j; last first. by rewrite coef_phi mxE coefMn !coefC; case: (k == _); rewrite ?mxE ?mul0rn. rewrite !coef_phi !mxE !coefM summxE coef_sum. pose F k1 k2 := (A i k1)`_k2 * (B k1 j)`_(k - k2). transitivity (\sum_k1 \sum_(k2 < k.+1) F k1 k2); rewrite {}/F. by apply: eq_bigr=> k1 _; rewrite coefM. rewrite exchange_big /=; apply: eq_bigr => k2 _. by rewrite mxE; apply: eq_bigr => k1 _; rewrite !coef_phi. have bij_phi: bijective phi. exists (fun P : MR_X => \matrix_(i, j) \poly_(k < size P) P`_k i j) => [A|P]. apply/matrixP=> i j; rewrite mxE; apply/polyP=> k. rewrite coef_poly -coef_phi. by case: leqP => // P_le_k; rewrite nth_default ?mxE. apply/polyP=> k; apply/matrixP=> i j; rewrite coef_phi mxE coef_poly. by case: leqP => // P_le_k; rewrite nth_default ?mxE. pose phiaM := GRing.isAdditive.Build _ _ phi phi_is_additive. pose phimM := GRing.isMultiplicative.Build _ _ phi phi_is_multiplicative. pose phiRM : GRing.RMorphism.type _ _ := HB.pack phi phiaM phimM. exists phiRM; split=> // [p | A]; apply/polyP=> k; apply/matrixP=> i j. by rewrite coef_phi coef_map !mxE coefMn. by rewrite coef_phi !mxE !coefC; case k; last rewrite /= mxE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)