proposition: Lemma galois_fixedField K E : reflect (fixedField 'Gal(E / K) = K) (galois K E).
proof: Proof. apply: (iffP idP) => [/and3P[sKE /separableP sepKE nKE] | fixedKE]. apply/eqP; rewrite eqEsubv galois_connection_subv ?andbT //. apply/subvP=> a /mem_fixedFieldP[Ea fixEa]; rewrite -adjoin_deg_eq1. have [r /allP Er splitKa] := normalFieldP nKE a Ea. rewrite -eqSS -size_minPoly splitKa size_prod_XsubC eqSS -[1]/(size [:: a]). have Ur: uniq r by rewrite -separable_prod_XsubC -splitKa; apply: sepKE. rewrite -uniq_size_uniq {Ur}// => b; rewrite inE -root_prod_XsubC -splitKa. apply/eqP/idP=> [-> | pKa_b_0]; first exact: root_minPoly. by have [x /fixEa-> ->] := normalField_root_minPoly sKE nKE Ea pKa_b_0. have sKE: (K <= E)%VS by rewrite -fixedKE capvSl. apply/galois_factors=> // a Ea. pose r_pKa := [seq x a | x : gal_of E in 'Gal(E / K)]. have /fin_all_exists2[x_ galEx_ Dx_a] (b : seq_sub r_pKa) := imageP (valP b). exists (codom x_); rewrite -map_comp; set r := map _ _. have r_xa x: x \in 'Gal(E / K) -> x a \in r. move=> galEx; have r_pKa_xa: x a \in r_pKa by apply/imageP; exists x. by rewrite [x a](Dx_a (SeqSub r_pKa_xa)); apply: codom_f. have Ur: uniq r by apply/injectiveP=> b c /=; rewrite -!Dx_a => /val_inj. split=> //; first by apply/subsetP=> _ /codomP[b ->]. apply/eqP; rewrite -eqp_monic ?monic_minPoly ?monic_prod_XsubC //. apply/andP; split; last first. rewrite uniq_roots_dvdp ?uniq_rootsE // all_map. by apply/allP=> b _ /=; rewrite root_minPoly_gal. apply: minPoly_dvdp; last by rewrite root_prod_XsubC -(gal_id E a) r_xa ?group1. rewrite -fixedKE; apply/polyOverP => i; apply/fixedFieldP=> [|x galEx]. rewrite (polyOverP _) // big_map rpred_prod // => b _. by rewrite polyOverXsubC memv_gal. rewrite -coef_map rmorph_prod; congr (_ : {poly _})`_i. symmetry; rewrite (perm_big (map x r)) /= ?(big_map x). by apply: eq_bigr => b _; rewrite rmorphB /= map_polyX map_polyC. have Uxr: uniq (map x r) by rewrite map_inj_uniq //; apply: fmorph_inj. have /uniq_min_size: {subset map x r <= r}. by rewrite -map_comp => _ /codomP[b ->] /=; rewrite -galM // r_xa ?groupM. by rewrite (size_map x) perm_sym; case=> // _ /uniq_perm->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)