proposition: Theorem Gaschutz_split : [splits G, over H] = [splits P, over H].
proof: Proof. apply/splitsP/splitsP=> [[K /complP[tiHK eqHK]] | [Q /complP[tiHQ eqHQ]]]. exists (K :&: P)%G; rewrite inE setICA (setIidPl sHP) setIC tiHK eqxx. by rewrite group_modl // eqHK (sameP eqP setIidPr). have sQP: Q \subset P by rewrite -eqHQ mulG_subr. pose rP x := repr (P :* x); pose pP x := x * (rP x)^-1. have PpP x: pP x \in P by rewrite -mem_rcoset rcoset_repr rcoset_refl. have rPmul x y: x \in P -> rP (x * y) = rP y. by move=> Px; rewrite /rP rcosetM rcoset_id. pose pQ x := remgr H Q x; pose rH x := pQ (pP x) * rP x. have pQhq: {in H & Q, forall h q, pQ (h * q) = q} by apply: remgrMid. have pQmul: {in P &, {morph pQ : x y / x * y}}. by apply: remgrM; [apply/complP | apply: normalS (nsHG)]. have HrH x: rH x \in H :* x. by rewrite rcoset_sym mem_rcoset invMg mulgA mem_divgr // eqHQ PpP. have GrH x: x \in G -> rH x \in G. move=> Gx; case/rcosetP: (HrH x) => y Hy ->. by rewrite groupM // (subsetP sHG). have rH_Pmul x y: x \in P -> rH (x * y) = pQ x * rH y. by move=> Px; rewrite /rH mulgA -pQmul; first by rewrite /pP rPmul ?mulgA. have rH_Hmul h y: h \in H -> rH (h * y) = rH y. by move=> Hh; rewrite rH_Pmul ?(subsetP sHP) // -(mulg1 h) pQhq ?mul1g. pose mu x y := fmod ((rH x * rH y)^-1 * rH (x * y)). pose nu y := (\sum_(Px in rcosets P G) mu (repr Px) y)%R. have rHmul: {in G &, forall x y, rH (x * y) = rH x * rH y * val (mu x y)}. move=> x y Gx Gy; rewrite /= fmodK ?mulKVg // -mem_lcoset lcoset_sym. rewrite -norm_rlcoset; last by rewrite nHG ?GrH ?groupM. by rewrite (rcoset_eqP (HrH _)) -rcoset_mul ?nHG ?GrH // mem_mulg. have actrH a x: x \in G -> (a ^@ rH x = a ^@ x)%R. move=> Gx; apply: val_inj; rewrite /= !fmvalJ ?nHG ?GrH //. case/rcosetP: (HrH x) => b /(fmodK abelH) <- ->; rewrite conjgM. by congr (_ ^ _); rewrite conjgE -fmvalN -!fmvalA (addrC a) addKr. have mu_Pmul x y z: x \in P -> mu (x * y) z = mu y z. move=> Px; congr fmod; rewrite -mulgA !(rH_Pmul x) ?rPmul //. by rewrite -mulgA invMg -mulgA mulKg. have mu_Hmul x y z: x \in G -> y \in H -> mu x (y * z) = mu x z. move=> Gx Hy; congr fmod; rewrite (mulgA x) (conjgCV x) -mulgA 2?rH_Hmul //. by rewrite -mem_conjg (normP _) ?nHG. have{mu_Hmul} nu_Hmul y z: y \in H -> nu (y * z) = nu z. move=> Hy; apply: eq_bigr => _ /rcosetsP[x Gx ->]; apply: mu_Hmul y z _ Hy. by rewrite -(groupMl _ (subsetP sPG _ (PpP x))) mulgKV. have cocycle_mu: {in G & &, forall x y z, mu (x * y)%g z + mu x y ^@ z = mu y z + mu x (y * z)%g}%R. - move=> x y z Gx Gy Gz; apply: val_inj. apply: (mulgI (rH x * rH y * rH z)). rewrite -(actrH _ _ Gz) addrC fmvalA fmvalJ ?nHG ?GrH //. rewrite mulgA -(mulgA _ (rH z)) -conjgC mulgA -!rHmul ?groupM //. by rewrite mulgA -mulgA -2!(mulgA (rH x)) -!rHmul ?groupM. move: mu => mu in rHmul mu_Pmul cocycle_mu nu nu_Hmul. have{cocycle_mu} cocycle_nu: {in G &, forall y z, nu z + nu y ^@ z = mu y z *+ #|G : P| + nu (y * z)%g}%R. - move=> y z Gy Gz; rewrite /= (actr_sum z) /=. have ->: (nu z = \sum_(Px in rcosets P G) mu (repr Px * y)%g z)%R. rewrite /nu (reindex_acts _ (actsRs_rcosets P G) Gy) /=. apply: eq_bigr => _ /rcosetsP[x Gx /= ->]. rewrite rcosetE -rcosetM. case: repr_rcosetP=> p1 Pp1; case: repr_rcosetP=> p2 Pp2. by rewrite -mulgA [x * y]lock !mu_Pmul. rewrite -sumr_const -!big_split /=; apply: eq_bigr => _ /rcosetsP[x Gx ->]. rewrite -cocycle_mu //; case: repr_rcosetP => p1 Pp1. by rewrite groupMr // (subsetP sPG). move: nu => nu in nu_Hmul cocycle_nu. pose f x := rH x * val (nu x *+ m)%R. have{cocycle_nu} fM: {in G &, {morph f : x y / x * y}}. move=> x y Gx Gy; rewrite /f ?rHmul // -3!mulgA; congr (_ * _). rewrite (mulgA _ (rH y)) (conjgC _ (rH y)) -mulgA; congr (_ * _). rewrite -fmvalJ ?actrH ?nHG ?GrH // -!fmvalA actZr -mulrnDl. rewrite -(addrC (nu y)) cocycle_nu // mulrnDl !fmvalA; congr (_ * _). by rewrite !fmvalZ expgK ?fmodP. exists (Morphism fM @* G)%G; apply/complP; split. apply/trivgP/subsetP=> x /setIP[Hx /morphimP[y _ Gy eq_x]]. apply/set1P; move: Hx; rewrite {x}eq_x /= groupMr ?subgP //. rewrite -{1}(mulgKV y (rH y)) groupMl -?mem_rcoset // => Hy. by rewrite -(mulg1 y) /f nu_Hmul // rH_Hmul //; apply: (morph1 (Morphism fM)). apply/setP=> x; apply/mulsgP/idP=> [[h y Hh fy ->{x}] | Gx]. rewrite groupMl; last exact: (subsetP sHG). case/morphimP: fy => z _ Gz ->{h Hh y}. by rewrite /= /f groupMl ?GrH // (subsetP sHG) ?fmodP. exists (x * (f x)^-1) (f x); last first; first by rewrite mulgKV. by apply/morphimP; exists x. rewrite -groupV invMg invgK -mulgA (conjgC (val _)) mulgA. by rewrite groupMl -(mem_rcoset, mem_conjg) // (normP _) ?nHG ?fmodP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype bigop ssralg finset fingroup) mathcomp(morphism perm finalg action gproduct commutator) mathcomp(cyclic)