proposition: Lemma group_splitting_field_exists gT (G : {group gT}) F : classically {Fs : fieldType & {rmorphism F -> Fs} & group_splitting_field Fs G}.
proof: Proof. move: F => F0 [] // nosplit; pose nG := #|G|; pose aG F := regular_repr F G. pose m := nG.+1; pose F := F0; pose U : seq 'M[F]_nG := [::]. suffices: size U + m <= nG by rewrite ltnn. have: mx_subseries (aG F) U /\ path ltmx 0 U by []. pose f : {rmorphism F0 -> F} := idfun. elim: m F U f => [|m IHm] F U f [modU ltU]. by rewrite addn0 (leq_trans (max_size_mx_series ltU)) ?rank_leq_row. rewrite addnS ltnNge -implybF; apply/implyP=> le_nG_Um; apply: nosplit. exists F => //; case=> [|n] rG irrG; first by case/mx_irrP: irrG. apply/idPn=> nabsG; pose cG := ('C(enveloping_algebra_mx rG))%MS. have{nabsG} [A]: exists2 A, (A \in cG)%MS & ~~ is_scalar_mx A. apply/has_non_scalar_mxP; rewrite ?scalar_mx_cent // ltnNge. by apply: contra nabsG; apply: cent_mx_scalar_abs_irr. rewrite {cG}memmx_cent_envelop -mxminpoly_linear_is_scalar -ltnNge => cGA. move/(non_linear_gen_reducible irrG cGA). set F' := _ irrG cGA; set rG' := @map_repr _ F' _ _ _ _ rG. move: F' (gen _ _ : {rmorphism F -> F'}) => F' f' in rG' * => irrG'. pose U' := [seq map_mx f' Ui | Ui <- U]. have modU': mx_subseries (aG F') U'. apply: etrans modU; rewrite /mx_subseries all_map; apply: eq_all => Ui. rewrite -(mxmodule_map f'); apply: eq_subset_r => x. by rewrite !inE map_regular_repr. case: notF; apply: (mx_Schreier modU ltU) => [[V [compV lastV sUV]]]. have{lastV} [] := rsim_regular_series irrG compV lastV. have{sUV} defV: V = U. apply/eqP; rewrite eq_sym -(geq_leqif (size_subseq_leqif sUV)). rewrite -(leq_add2r m); apply: leq_trans le_nG_Um. by apply: IHm f _; rewrite (mx_series_lt compV); case: compV. rewrite {V}defV in compV * => i rsimVi. apply: (mx_Schreier modU') => [|[V' [compV' _ sUV']]]. rewrite {modU' compV modU i le_nG_Um rsimVi}/U' -(map_mx0 f'). by apply: etrans ltU; elim: U 0 => //= Ui U IHU Ui'; rewrite IHU map_ltmx. have{sUV'} defV': V' = U'; last rewrite {V'}defV' in compV'. apply/eqP; rewrite eq_sym -(geq_leqif (size_subseq_leqif sUV')) size_map. rewrite -(leq_add2r m); apply: leq_trans le_nG_Um. apply: IHm (f' \o f) _. by rewrite (mx_series_lt compV'); case: compV'. suffices{irrG'}: mx_irreducible rG' by case/mxsimpleP=> _ _ []. have ltiU': i < size U' by rewrite size_map. apply: mx_rsim_irr (mx_rsim_sym _ ) (mx_series_repr_irr compV' ltiU'). by apply: mx_rsim_trans (mx_rsim_map f' rsimVi) _; apply: map_regular_subseries. 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)