proposition: Lemma galois_misom (k K F : {subfield L}) (H := 'Gal((K * F) / F)%g) (H' := 'Gal (K / (K :&: F))%g) : galois k K -> (k <= F)%VS -> misom H H' (normalField_cast K).
proof: Proof. move=> gal_kK kF; have kK := galois_subW gal_kK. have normal_kK := galois_normalW gal_kK. have KF u : u \in H -> (u @: K <= K)%VS. move=> Hu; suff : kHom k K u by rewrite -kAutEnormal// kAutE => /andP[]. by apply/kAHomP => x kx; rewrite (fixed_gal _ Hu) ?field_subvMl ?(subvP kF). have r_H_morphic : morphic H (normalField_cast K). apply/morphicP => u v uH vH; apply/eqP/gal_eqP => x Kx. rewrite galM// [LHS]galK ?KF ?groupM//. rewrite 2?galK ?KF//; last by apply/(subvP (KF u uH)); rewrite memv_img. by rewrite galM//; apply: subvP Kx; apply: field_subvMr. apply/misomP; exists r_H_morphic; apply/isomP; split. apply/subsetP => /= u ker_u; have Hu := dom_ker ker_u. apply/set1gP/eqP/gal_eqP => _ /memv_mulP[n [xs [ys [xsP ysP ->]]]]. rewrite rmorph_sum/= gal_id; apply: eq_bigr => i _; rewrite rmorphM/=. have [xiK yiK] := (allP xsP _ (mem_tnth i _), allP ysP _ (mem_tnth i _)). have /eqP/gal_eqP/(_ _ xiK) := mker ker_u. rewrite /normalField_cast galK ?KF// => ->; rewrite gal_id. by rewrite (fixed_gal _ Hu)// field_subvMl. apply/eqP; rewrite eq_sym galois_eq ?(capv_galois kF gal_kK)//. rewrite eqEsubv; apply/andP; split; apply/subvP => x; last first. rewrite memv_cap => /andP[Kx Fx]. apply/fixedFieldP => // _ /morphimP[/= v Hv _ ->]. rewrite morphmE /normalField_cast galK// ?KF//. by rewrite (fixed_gal _ Hv)// field_subvMl. move=> /mem_fixedFieldP[Kx xP]; rewrite memv_cap Kx/=. rewrite -(galois_fixedField (galois_prodvr kF gal_kK)). apply/fixedFieldP; first by rewrite -[x]mulr1 memv_mul// rpred1. move=> u Hu; have := xP (normalField_cast _ u). by rewrite /normalField_cast galK ?KF//; apply; apply/morphimP; exists u. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)