proposition: Lemma isog_abelian_type G H : isog G H -> abelian_type G = abelian_type H.
proof: Proof. pose lnO p n gT (A : {set gT}) := logn p #|'Ohm_n.+1(A) : 'Ohm_n(A)|. pose lni i p gT (A : {set gT}) := \max_(e < logn p #|A| | i < lnO p e _ A) e.+1. suffices{G} nth_abty gT (G : {group gT}) i: abelian G -> i < size (abelian_type G) -> nth 1%N (abelian_type G) i = (\prod_(p < #|G|.+1) p ^ lni i p _ G)%N. - move=> isoGH; case cGG: (abelian G); last first. rewrite /abelian_type -(prednK (cardG_gt0 G)) -(prednK (cardG_gt0 H)) /=. by rewrite {1}(genGid G) {1}(genGid H) -(isog_abelian isoGH) cGG. have cHH: abelian H by rewrite -(isog_abelian isoGH). have eq_sz: size (abelian_type G) = size (abelian_type H). by rewrite !size_abelian_type ?(isog_rank isoGH). apply: (@eq_from_nth _ 1%N) => // i lt_i_G; rewrite !nth_abty // -?eq_sz //. rewrite /lni (card_isog isoGH); apply: eq_bigr => p _; congr (p ^ _)%N. apply: eq_bigl => e; rewrite /lnO -!divgS ?(Ohm_leq _ (leqnSn _)) //=. by have:= card_isog (gFisog _ isoGH) => /= eqF; rewrite !eqF. move=> cGG. have (p): path leq 0 (map (logn p) (rev (abelian_type G))). move: (abelian_type_gt1 G) (abelian_type_dvdn_sorted G). case: abelian_type => //= m t; rewrite rev_cons map_rcons. elim: t m => //= n t IHt m /andP[/ltnW m_gt0 nt_gt1]. rewrite -cats1 cat_path rev_cons map_rcons last_rcons /=. by case/andP=> /dvdn_leq_log-> // /IHt->. have{cGG} [b defG <- b_sorted] := abelian_structure cGG. rewrite size_map => ltib; rewrite (nth_map 1 _ _ ltib); set x := nth 1 b i. have Gx: x \in G. have: x \in b by rewrite mem_nth. rewrite -(bigdprodWY defG); case/splitPr=> bl br. by rewrite mem_gen // big_cat big_cons !inE cycle_id orbT. have lexG: #[x] <= #|G| by rewrite dvdn_leq ?order_dvdG. rewrite -[#[x]]partn_pi // (widen_partn _ lexG) big_mkord big_mkcond. apply: eq_bigr => p _; transitivity (p ^ logn p #[x])%N. by rewrite -logn_gt0; case: posnP => // ->. suffices lti_lnO e: (i < lnO p e _ G) = (e < logn p #[x]). congr (p ^ _)%N; apply/eqP; rewrite eqn_leq andbC; apply/andP; split. by apply/bigmax_leqP=> e; rewrite lti_lnO. have [-> //|logx_gt0] := posnP (logn p #[x]). have lexpG: (logn p #[x]).-1 < logn p #|G|. by rewrite prednK // dvdn_leq_log ?order_dvdG. by rewrite (bigmax_sup (Ordinal lexpG)) ?(prednK, lti_lnO). rewrite /lnO -(count_logn_dprod_cycle _ _ defG). case: (ltnP e) (b_sorted p) => [lt_e_x | le_x_e]. rewrite -(cat_take_drop i.+1 b) -map_rev rev_cat !map_cat cat_path. case/andP=> _ ordb; rewrite count_cat ((count _ _ =P i.+1) _) ?leq_addr //. rewrite -{2}(size_takel ltib) -all_count. move: ordb; rewrite (take_nth 1 ltib) -/x rev_rcons all_rcons /= lt_e_x. case/andP=> _ /=; move/(order_path_min leq_trans); apply: contraLR. rewrite -!has_predC !has_map; case/hasP=> y b_y /= le_y_e; apply/hasP. by exists y; rewrite ?mem_rev //=; apply: contra le_y_e; apply: leq_trans. rewrite -(cat_take_drop i b) -map_rev rev_cat !map_cat cat_path. case/andP=> ordb _; rewrite count_cat -{1}(size_takel (ltnW ltib)) ltnNge. rewrite addnC ((count _ _ =P 0) _) ?count_size //. rewrite eqn0Ngt -has_count; apply/hasPn=> y b_y /=; rewrite -leqNgt. apply: leq_trans le_x_e; have ->: x = last x (rev (drop i b)). by rewrite (drop_nth 1 ltib) rev_cons last_rcons. rewrite -mem_rev in b_y; case/splitPr: (rev _) / b_y ordb => b1 b2. rewrite !map_cat cat_path last_cat /=; case/and3P=> _ _. move/(order_path_min leq_trans); case/lastP: b2 => // b3 x'. by move/allP; apply; rewrite ?map_f ?last_rcons ?mem_rcons ?mem_head. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)