proposition: Lemma transfer_cycle_expansion : transfer g = \sum_(x in X) fmalpha ((g ^+ n_ x) ^ (x^-1)).
proof: Proof. pose Y := \bigcup_(x in X) [set x * g ^+ i | i : 'I_(n_ x)]. pose rY := transversal_repr 1 Y. pose pcyc x := porbit (actperm 'Rs g) (H :* x). pose traj x := traject (actperm 'Rs g) (H :* x) #|pcyc x|. have Hgr_eq x: H_g_rcosets x = pcyc x. by rewrite /H_g_rcosets -orbitRs -porbit_actperm ?inE. have pcyc_eq x: pcyc x =i traj x by apply: porbit_traject. have uniq_traj x: uniq (traj x) by apply: uniq_traject_porbit. have n_eq x: n_ x = #|pcyc x| by rewrite -Hgr_eq. have size_traj x: size (traj x) = n_ x by rewrite n_eq size_traject. have nth_traj x j: j < n_ x -> nth (H :* x) (traj x) j = H :* (x * g ^+ j). move=> lt_j_x; rewrite nth_traject -?n_eq //. by rewrite -permX -morphX ?inE // actpermE //= rcosetE rcosetM. have sYG: Y \subset G. apply/bigcupsP=> x Xx; apply/subsetP=> _ /imsetP[i _ ->]. by rewrite groupM ?groupX // sXG. have trY: is_transversal Y HG G. apply/and3P; split=> //; apply/forall_inP=> Hy. have /and3P[/eqP <- _ _] := partHGg; rewrite -defHgX cover_imset. case/bigcupP=> x Xx; rewrite Hgr_eq pcyc_eq => /trajectP[i]. rewrite -n_eq -permX -morphX ?in_setT // actpermE /= rcosetE -rcosetM => lti. set y := x * _ => ->{Hy}; pose oi := Ordinal lti. have Yy: y \in Y by apply/bigcupP; exists x => //; apply/imsetP; exists oi. apply/cards1P; exists y; apply/esym/eqP. rewrite eqEsubset sub1set inE Yy rcoset_refl. apply/subsetP=> _ /setIP[/bigcupP[x' Xx' /imsetP[j _ ->]] Hy_x'gj]. have eq_xx': x = x'. apply: (pblock_inj trX) => //; have /andP[/and3P[_ tiX _] _] := trX. have HGgHyg: H :* y * <[g]> \in HG :* <[g]>. by rewrite mem_mulg ?set11 // -rcosetE imset_f ?(subsetP sYG). rewrite !(def_pblock tiX HGgHyg) //. by rewrite -[x'](mulgK (g ^+ j)) mem_mulg // groupV mem_cycle. by rewrite -[x](mulgK (g ^+ i)) mem_mulg ?rcoset_refl // groupV mem_cycle. apply/set1P; rewrite /y eq_xx'; congr (_ * _ ^+ _) => //; apply/eqP. rewrite -(@nth_uniq _ (H :* x) (traj x)) ?size_traj // ?eq_xx' //. by rewrite !nth_traj ?(rcoset_eqP Hy_x'gj) // -eq_xx'. have rYE x i : x \in X -> i < n_ x -> rY (H :* x :* g ^+ i) = x * g ^+ i. move=> Xx lt_i_x; rewrite -rcosetM; apply: (canLR_in (pblockK trY 1)). by apply/bigcupP; exists x => //; apply/imsetP; exists (Ordinal lt_i_x). apply/esym/def_pblock; last exact: rcoset_refl; first by case/and3P: partHG. by rewrite -rcosetE imset_f ?groupM ?groupX // sXG. rewrite (transfer_indep trY Gg) /V -/rY (set_partition_big _ partHGg) /=. rewrite -defHgX big_imset /=; last first. apply/imset_injP; rewrite defHgX (card_transversal trX) defHGg. by rewrite (card_in_imset injHGg). apply eq_bigr=> x Xx; rewrite Hgr_eq (eq_bigl _ _ (pcyc_eq x)) -big_uniq //=. have n_gt0: 0 < n_ x by rewrite indexg_gt0. rewrite /traj -n_eq; case def_n: (n_ x) (n_gt0) => // [n] _. rewrite conjgE invgK -{1}[H :* x]rcoset1 -{1}(expg0 g). elim: {1 3}n 0%N (addn0 n) => [|m IHm] i def_i /=. rewrite big_seq1 {i}[i]def_i rYE // ?def_n //. rewrite -(mulgA _ _ g) -rcosetM -expgSr -[(H :* x) :* _]rcosetE. rewrite -actpermE morphX ?inE // permX // -{2}def_n n_eq iter_porbit mulgA. by rewrite -[H :* x]rcoset1 (rYE _ 0) ?mulg1. rewrite big_cons rYE //; last by rewrite def_n -def_i ltnS leq_addl. rewrite permE /= rcosetE -rcosetM -(mulgA _ _ g) -expgSr. rewrite addSnnS in def_i; rewrite IHm //. rewrite rYE //; last by rewrite def_n -def_i ltnS leq_addl. by rewrite mulgV [fmalpha 1]morph1 add0r. 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)