Library mathcomp.solvable.abelian

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div fintype finfun bigop finset prime binomial.
From mathcomp Require Import fingroup morphism perm automorphism action.
From mathcomp Require Import quotient gfunctor gproduct ssralg finalg zmodp.
From mathcomp Require Import cyclic pgroup gseries nilpotent sylow.

Constructions based on abelian groups and their structure, with some emphasis on elementary abelian p-groups. 'Ldiv_n == the set of all x that satisfy x ^+ n = 1, or, equivalently the set of x whose order divides n. 'Ldiv_n(G) == the set of x in G that satisfy x ^+ n = 1. := G :&: 'Ldiv_n (pure Notation) exponent G == the exponent of G: the least e such that x ^+ e = 1 for all x in G (the LCM of the orders of x \in G). If G is nilpotent its exponent is reached. Note that `exponent G %| m' reads as `G has exponent m'. 'm(G) == the generator rank of G: the size of a smallest generating set for G (this is a basis for G if G abelian). abelian_type G == the abelian type of G : if G is abelian, a lexico- graphically maximal sequence of the orders of the elements of a minimal basis of G (if G is a p-group this is the sequence of orders for any basis of G, sorted in decending order). homocyclic G == G is the direct product of cycles of equal order, i.e., G is abelian with constant abelian type. p.-abelem G == G is an elementary abelian p-group, i.e., it is an abelian p-group of exponent p, and thus of order p ^ 'm(G) and rank (logn p #|G|). is_abelem G == G is an elementary abelian p-group for some prime p. 'E_p(G) == the set of elementary abelian p-subgroups of G. := [set E : {group _} | p.-abelem E & E \subset G] 'E_p^n(G) == the set of elementary abelian p-subgroups of G of order p ^ n (or, equivalently, of rank n). := [set E in 'E_p(G) | logn p #|E| == n] := [set E in 'E_p(G) | #|E| == p ^ n]%N if p is prime 'E*p(G) == the set of maximal elementary abelian p-subgroups of G. := [set E | [max E | E \in 'E_p(G) ]#] 'E^n(G) == the set of elementary abelian subgroups of G that have gerank n (i.e., p-rank n for some prime p). := \bigcup(0 <= p < #|G|.+1) 'E_p^n(G) 'r_p(G) == the p-rank of G: the maximal rank of an elementary subgroup of G. := \max(E in 'E_p(G)) logn p #|E|. 'r(G) == the rank of G. := \max(0 <= p < #|G|.+1) 'm_p(G). Note that 'r(G) coincides with 'r_p(G) if G is a p-group, and with 'm(G) if G is abelian, but is much more useful than 'm(G) in the proof of the Odd Order Theorem. 'Ohm_n(G) == the group generated by the x in G with order p ^ m for some prime p and some m <= n. Usually, G will be a p-group, so 'Ohm_n(G) will be generated by 'Ldiv(p ^ n)(G), set of elements of G of order at most p ^ n. If G is also abelian then 'Ohm_n(G) consists exactly of those element, and the abelian type of G can be computed from the orders of the 'Ohm_n(G) subgroups. 'Mho^n(G) == the group generated by the x ^+ (p ^ n) for x a p-element of G for some prime p. Usually G is a p-group, and 'Mho^n(G) is generated by all such x ^+ (p ^ n); it consists of exactly these if G is also abelian.

Set Implicit Arguments.

Import GroupScope.

Section AbelianDefs.

We defer the definition of the functors ('Omh_n(G), 'Mho^n(G)) because they must quantify over the finGroupType explicitly.

Variable gT : finGroupType.
Implicit Types (x : gT) (A B : {set gT }) (pi : nat_pred) (p n : nat).

Definition Ldiv n := [set x : gT | x ^+ n == 1].

Definition exponent A := \big [lcmn /1%N]_(x in A ) #[x ].

Definition abelem p A := [&& p .-group A , abelian A & exponent A %| p ].

Definition is_abelem A := abelem (pdiv #|A |) A.

Definition pElem p A := [set E : {group gT } | E \subset A & abelem p E ].

Definition pnElem p n A := [set E in pElem p A | logn p #|E | == n ].

Definition nElem n A := \bigcup_(0 ≤ p < #|A |.+1 ) pnElem p n A.

Definition pmaxElem p A := [set E | [max E | E \in pElem p A ]].

Definition p_rank p A := \max_(E in pElem p A ) logn p #|E |.

Definition rank A := \max_(0 ≤ p < #|A |.+1 ) p_rank p A.

Definition gen_rank A := #|[arg min_(B < A | <<B >> == A ) #|B |]|.

The definition of abelian_type depends on an existence lemma. The definition of homocyclic depends on abelian_type.

End AbelianDefs.

Arguments exponent {gT} A%g.
Arguments abelem {gT} p%N A%g.
Arguments is_abelem {gT} A%g.
Arguments pElem {gT} p%N A%g.
Arguments pnElem {gT} p%N n%N A%g.
Arguments nElem {gT} n%N A%g.
Arguments pmaxElem {gT} p%N A%g.
Arguments p_rank {gT} p%N A%g.
Arguments rank {gT} A%g.
Arguments gen_rank {gT} A%g.

Notation "''Ldiv_' n " := (Ldiv _ n)
  (at level 8, n at level 2, format "''Ldiv_' n ") : group_scope.

Notation "''Ldiv_' n ( G )" := (G :&: 'Ldiv_n)
  (at level 8, n at level 2, format "''Ldiv_' n ( G )") : group_scope.

Notation "p .-abelem" := (abelem p)
  (at level 2, format "p .-abelem") : group_scope.

Notation "''E_' p ( G )" := (pElem p G)
  (at level 8, p at level 2, format "''E_' p ( G )") : group_scope.

Notation "''E_' p ^ n ( G )" := (pnElem p n G)
  (at level 8, p, n at level 2, format "''E_' p ^ n ( G )") : group_scope.

Notation "''E' ^ n ( G )" := (nElem n G)
  (at level 8, n at level 2, format "''E' ^ n ( G )") : group_scope.

Notation "''E*_' p ( G )" := (pmaxElem p G)
  (at level 8, p at level 2, format "''E*_' p ( G )") : group_scope.

Notation "''m' ( A )" := (gen_rank A)
  (at level 8, format "''m' ( A )") : group_scope.

Notation "''r' ( A )" := (rank A)
  (at level 8, format "''r' ( A )") : group_scope.

Notation "''r_' p ( A )" := (p_rank p A)
  (at level 8, p at level 2, format "''r_' p ( A )") : group_scope.

Section Functors.

A functor needs to quantify over the finGroupType just beore the set.

Variables (n : nat) (gT : finGroupType) (A : {set gT }).

Definition Ohm := <<[set x in A | x ^+ (pdiv #[x ] ^ n ) == 1]>>.

Definition Mho := <<[set x ^+ (pdiv #[x ] ^ n ) | x in A & (pdiv #[x ]).-elt x ]>>.

Canonical Ohm_group : {group gT } := Eval hnf in [group of Ohm ].
Canonical Mho_group : {group gT } := Eval hnf in [group of Mho ].

Lemma pdiv_p_elt (p : nat) (x : gT) : p .-elt x → x != 1 → pdiv #[x ] = p.

Lemma OhmPredP (x : gT) :
  reflect (exists2 p , prime p & x ^+ (p ^ n ) = 1) (x ^+ (pdiv #[x ] ^ n ) == 1).

Lemma Mho_p_elt (p : nat) x : x \in A → p .-elt x → x ^+ (p ^ n ) \in Mho.

End Functors.

Arguments Ohm n%N {gT} A%g.
Arguments Ohm_group n%N {gT} A%g.
Arguments Mho n%N {gT} A%g.
Arguments Mho_group n%N {gT} A%g.
Arguments OhmPredP {n gT x}.

Notation "''Ohm_' n ( G )" := (Ohm n G)
  (at level 8, n at level 2, format "''Ohm_' n ( G )") : group_scope.
Notation "''Ohm_' n ( G )" := (Ohm_group n G) : Group_scope.

Notation "''Mho^' n ( G )" := (Mho n G)
  (at level 8, n at level 2, format "''Mho^' n ( G )") : group_scope.
Notation "''Mho^' n ( G )" := (Mho_group n G) : Group_scope.

Section ExponentAbelem.

Variable gT : finGroupType.
Implicit Types (p n : nat) (pi : nat_pred) (x : gT) (A B C : {set gT }).
Implicit Types E G H K P X Y : {group gT }.

Lemma LdivP A n x : reflect (x \in A ∧ x ^+ n = 1) (x \in 'Ldiv_n (A )).

Lemma dvdn_exponent x A : x \in A → #[x ] %| exponent A.

Lemma expg_exponent x A : x \in A → x ^+ exponent A = 1.

Lemma exponentS A B : A \subset B → exponent A %| exponent B.

Lemma exponentP A n :
  reflect (∀ x, x \in A → x ^+ n = 1) (exponent A %| n).
Arguments exponentP {A n}.

Lemma trivg_exponent G : (G :==: 1) = (exponent G %| 1).

Lemma exponent1 : exponent [1 gT ] = 1%N.

Lemma exponent_dvdn G : exponent G %| #|G |.

Lemma exponent_gt0 G : 0 < exponent G.
Hint Resolve exponent_gt0 : core.

Lemma pnat_exponent pi G : pi .-nat (exponent G ) = pi .-group G.

Lemma exponentJ A x : exponent (A :^ x) = exponent A.

Lemma exponent_witness G : nilpotent G → {x | x \in G & exponent G = #[x ]}.

Lemma exponent_cycle x : exponent <[x ]> = #[x ].

Lemma exponent_cyclic X : cyclic X → exponent X = #|X |.

Lemma primes_exponent G : primes (exponent G) = primes (#|G |).

Lemma pi_of_exponent G : \pi (exponent G ) = \pi (G ).

Lemma partn_exponentS pi H G :
  H \subset G → #|G |`_pi %| #|H | → (exponent H )`_pi = (exponent G )`_pi.

Lemma exponent_Hall pi G H : pi .-Hall (G ) H → exponent H = (exponent G )`_pi.

Lemma exponent_Zgroup G : Zgroup G → exponent G = #|G |.

Lemma cprod_exponent A B G :
  A \* B = G → lcmn (exponent A) (exponent B) = (exponent G ).

Lemma dprod_exponent A B G :
  A \x B = G → lcmn (exponent A) (exponent B) = (exponent G ).

Lemma sub_LdivT A n : (A \subset 'Ldiv_n ) = (exponent A %| n ).

Lemma LdivT_J n x : 'Ldiv_n :^ x = 'Ldiv_n.

Lemma LdivJ n A x : 'Ldiv_n (A :^ x ) = 'Ldiv_n (A ) :^ x.

Lemma sub_Ldiv A n : (A \subset 'Ldiv_n (A )) = (exponent A %| n ).

Lemma group_Ldiv G n : abelian G → group_set 'Ldiv_n (G ).

Lemma abelian_exponent_gen A : abelian A → exponent <<A >> = exponent A.

Lemma abelem_pgroup p A : p .-abelem A → p .-group A.

Lemma abelem_abelian p A : p .-abelem A → abelian A.

Lemma abelem1 p : p .-abelem [1 gT ].

Lemma abelemE p G : prime p → p .-abelem G = abelian G && (exponent G %| p ).

Lemma abelemP p G :
    prime p →
  reflect (abelian G ∧ ∀ x, x \in G → x ^+ p = 1) (p .-abelem G).

Lemma abelem_order_p p G x : p .-abelem G → x \in G → x != 1 → #[x ] = p.

Lemma cyclic_abelem_prime p X : p .-abelem X → cyclic X → X :!=: 1 → #|X | = p.

Lemma cycle_abelem p x : p .-elt x || prime p → p .-abelem <[x ]> = (#[x ] %| p ).

Lemma exponent2_abelem G : exponent G %| 2 → 2.-abelem G.

Lemma prime_abelem p G : prime p → #|G | = p → p .-abelem G.

Lemma abelem_cyclic p G : p .-abelem G → cyclic G = (logn p #|G | ≤ 1).

Lemma abelemS p H G : H \subset G → p .-abelem G → p .-abelem H.

Lemma abelemJ p G x : p .-abelem (G :^ x ) = p .-abelem G.

Lemma cprod_abelem p A B G :
  A \* B = G → p .-abelem G = p .-abelem A && p .-abelem B.

Lemma dprod_abelem p A B G :
  A \x B = G → p .-abelem G = p .-abelem A && p .-abelem B.

Lemma is_abelem_pgroup p G : p .-group G → is_abelem G = p .-abelem G.

Lemma is_abelemP G : reflect (exists2 p , prime p & p .-abelem G) (is_abelem G).

Lemma pElemP p A E : reflect (E \subset A ∧ p .-abelem E) (E \in 'E_p (A )).
Arguments pElemP {p A E}.

Lemma pElemS p A B : A \subset B → 'E_p (A ) \subset 'E_p (B ).

Lemma pElemI p A B : 'E_p (A :&: B ) = 'E_p (A ) :&: subgroups B.

Lemma pElemJ x p A E : ((E :^ x)%G \in 'E_p (A :^ x )) = (E \in 'E_p (A )).

Lemma pnElemP p n A E :
  reflect [/\ E \subset A , p .-abelem E & logn p #|E | = n ] (E \in 'E_p ^n (A )).
Arguments pnElemP {p n A E}.

Lemma pnElemPcard p n A E :
  E \in 'E_p ^n (A ) → [/\ E \subset A , p .-abelem E & #|E | = p ^ n ]%N.

Lemma card_pnElem p n A E : E \in 'E_p ^n (A ) → #|E | = (p ^ n)%N.

Lemma pnElem0 p G : 'E_p ^0(G ) = [set 1%G].

Lemma pnElem_prime p n A E : E \in 'E_p ^n .+1 (A ) → prime p.

Lemma pnElemE p n A :
  prime p → 'E_p ^n (A ) = [set E in 'E_p (A ) | #|E | == (p ^ n)%N].

Lemma pnElemS p n A B : A \subset B → 'E_p ^n (A ) \subset 'E_p ^n (B ).

Lemma pnElemI p n A B : 'E_p ^n (A :&: B ) = 'E_p ^n (A ) :&: subgroups B.

Lemma pnElemJ x p n A E : ((E :^ x)%G \in 'E_p ^n (A :^ x )) = (E \in 'E_p ^n (A )).

Lemma abelem_pnElem p n G :
  p .-abelem G → n ≤ logn p #|G | → ∃ E , E \in 'E_p ^n (G ).

Lemma card_p1Elem p A X : X \in 'E_p ^1(A ) → #|X | = p.

Lemma p1ElemE p A : prime p → 'E_p ^1(A ) = [set X in subgroups A | #|X | == p ].

Lemma TIp1ElemP p A X Y :
  X \in 'E_p ^1(A ) → Y \in 'E_p ^1(A ) → reflect (X :&: Y = 1) (X :!=: Y).

Lemma card_p1Elem_pnElem p n A E :
  E \in 'E_p ^n (A ) → #|'E_p ^1(E )| = (\sum_(i < n ) p ^ i)%N.

Lemma card_p1Elem_p2Elem p A E : E \in 'E_p ^2(A ) → #|'E_p ^1(E )| = p .+1.

Lemma p2Elem_dprodP p A E X Y :
    E \in 'E_p ^2(A ) → X \in 'E_p ^1(E ) → Y \in 'E_p ^1(E ) →
  reflect (X \x Y = E) (X :!=: Y).

Lemma nElemP n G E : reflect (∃ p , E \in 'E_p ^n (G )) (E \in 'E ^n (G )).
Arguments nElemP {n G E}.

Lemma nElem0 G : 'E ^0(G ) = [set 1%G].

Lemma nElem1P G E :
  reflect (E \subset G ∧ exists2 p , prime p & #|E | = p) (E \in 'E ^1(G )).

Lemma nElemS n G H : G \subset H → 'E ^n (G ) \subset 'E ^n (H ).

Lemma nElemI n G H : 'E ^n (G :&: H ) = 'E ^n (G ) :&: subgroups H.

Lemma def_pnElem p n G : 'E_p ^n (G ) = 'E_p (G ) :&: 'E ^n (G ).

Lemma pmaxElemP p A E :
  reflect (E \in 'E_p (A ) ∧ ∀ H, H \in 'E_p (A ) → E \subset H → H :=: E)
          (E \in 'E ×_p (A )).

Lemma pmaxElem_exists p A D :
  D \in 'E_p (A ) → {E | E \in 'E ×_p (A ) & D \subset E }.

Lemma pmaxElem_LdivP p G E :
  prime p → reflect ('Ldiv_p ('C_G (E )) = E) (E \in 'E ×_p (G )).

Lemma pmaxElemS p A B :
  A \subset B → 'E ×_p (B ) :&: subgroups A \subset 'E ×_p (A ).

Lemma pmaxElemJ p A E x : ((E :^ x)%G \in 'E ×_p (A :^ x )) = (E \in 'E ×_p (A )).

Lemma grank_min B : 'm (<<B >>) ≤ #|B |.

Lemma grank_witness G : {B | <<B >> = G & #|B | = 'm (G )}.

Lemma p_rank_witness p G : {E | E \in 'E_p ^('r_p (G ))(G )}.

Lemma p_rank_geP p n G : reflect (∃ E , E \in 'E_p ^n (G )) (n ≤ 'r_p (G )).

Lemma p_rank_gt0 p H : ('r_p (H ) > 0) = (p \in \pi (H )).

Lemma p_rank1 p : 'r_p ([1 gT ]) = 0.

Lemma logn_le_p_rank p A E : E \in 'E_p (A ) → logn p #|E | ≤ 'r_p (A ).

Lemma p_rank_le_logn p G : 'r_p (G ) ≤ logn p #|G |.

Lemma p_rank_abelem p G : p .-abelem G → 'r_p (G ) = logn p #|G |.

Lemma p_rankS p A B : A \subset B → 'r_p (A ) ≤ 'r_p (B ).

Lemma p_rankElem_max p A : 'E_p ^('r_p (A ))(A ) \subset 'E ×_p (A ).

Lemma p_rankJ p A x : 'r_p (A :^ x ) = 'r_p (A ).

Lemma p_rank_Sylow p G H : p .-Sylow (G ) H → 'r_p (H ) = 'r_p (G ).

Lemma p_rank_Hall pi p G H : pi .-Hall (G ) H → p \in pi → 'r_p (H ) = 'r_p (G ).

Lemma p_rank_pmaxElem_exists p r G :
  'r_p (G ) ≥ r → exists2 E , E \in 'E ×_p (G ) & 'r_p (E ) ≥ r.

Lemma rank1 : 'r ([1 gT ]) = 0.

Lemma p_rank_le_rank p G : 'r_p (G ) ≤ 'r (G ).

Lemma rank_gt0 G : ('r (G ) > 0) = (G :!=: 1).

Lemma rank_witness G : {p | prime p & 'r (G ) = 'r_p (G )}.

Lemma rank_pgroup p G : p .-group G → 'r (G ) = 'r_p (G ).

Lemma rank_Sylow p G P : p .-Sylow (G ) P → 'r (P ) = 'r_p (G ).

Lemma rank_abelem p G : p .-abelem G → 'r (G ) = logn p #|G |.

Lemma nt_pnElem p n E A : E \in 'E_p ^n (A ) → n > 0 → E :!=: 1.

Lemma rankJ A x : 'r (A :^ x ) = 'r (A ).

Lemma rankS A B : A \subset B → 'r (A ) ≤ 'r (B ).

Lemma rank_geP n G : reflect (∃ E , E \in 'E ^n (G )) (n ≤ 'r (G )).

End ExponentAbelem.

Arguments LdivP {gT A n x}.
Arguments exponentP {gT A n}.
Arguments abelemP {gT p G}.
Arguments is_abelemP {gT G}.
Arguments pElemP {gT p A E}.
Arguments pnElemP {gT p n A E}.
Arguments nElemP {gT n G E}.
Arguments nElem1P {gT G E}.
Arguments pmaxElemP {gT p A E}.
Arguments pmaxElem_LdivP {gT p G E}.
Arguments p_rank_geP {gT p n G}.
Arguments rank_geP {gT n G}.

Section MorphAbelem.

Variables (aT rT : finGroupType) (D : {group aT }) (f : {morphism D >-> rT }).
Implicit Types (G H E : {group aT }) (A B : {set aT }).

Lemma exponent_morphim G : exponent (f @* G) %| exponent G.

Lemma morphim_LdivT n : f @* 'Ldiv_n \subset 'Ldiv_n.

Lemma morphim_Ldiv n A : f @* 'Ldiv_n (A ) \subset 'Ldiv_n (f @* A ).

Lemma morphim_abelem p G : p .-abelem G → p .-abelem (f @* G ).

Lemma morphim_pElem p G E : E \in 'E_p (G ) → (f @* E)%G \in 'E_p (f @* G ).

Lemma morphim_pnElem p n G E :
  E \in 'E_p ^n (G ) → {m | m ≤ n & (f @* E)%G \in 'E_p ^m (f @* G )}.

Lemma morphim_grank G : G \subset D → 'm (f @* G ) ≤ 'm (G ).

There are no general morphism relations for the p-rank. We later prove some relations for the p-rank of a quotient in the QuotientAbelem section.

End MorphAbelem.

Section InjmAbelem.

Variables (aT rT : finGroupType) (D G : {group aT }) (f : {morphism D >-> rT }).
Hypotheses (injf : 'injm f) (sGD : G \subset D).
Let defG : invm injf @* (f @* G ) = G := morphim_invm injf sGD.

Lemma exponent_injm : exponent (f @* G) = exponent G.

Lemma injm_Ldiv n A : f @* 'Ldiv_n (A ) = 'Ldiv_n (f @* A ).

Lemma injm_abelem p : p .-abelem (f @* G ) = p .-abelem G.

Lemma injm_pElem p (E : {group aT }) :
  E \subset D → ((f @* E)%G \in 'E_p (f @* G )) = (E \in 'E_p (G )).

Lemma injm_pnElem p n (E : {group aT }) :
  E \subset D → ((f @* E)%G \in 'E_p ^n (f @* G )) = (E \in 'E_p ^n (G )).

Lemma injm_nElem n (E : {group aT }) :
  E \subset D → ((f @* E)%G \in 'E ^n (f @* G )) = (E \in 'E ^n (G )).

Lemma injm_pmaxElem p (E : {group aT }) :
  E \subset D → ((f @* E)%G \in 'E ×_p (f @* G )) = (E \in 'E ×_p (G )).

Lemma injm_grank : 'm (f @* G ) = 'm (G ).

Lemma injm_p_rank p : 'r_p (f @* G ) = 'r_p (G ).

Lemma injm_rank : 'r (f @* G ) = 'r (G ).

End InjmAbelem.

Section IsogAbelem.

Variables (aT rT : finGroupType) (G : {group aT }) (H : {group rT }).
Hypothesis isoGH : G \isog H.

Lemma exponent_isog : exponent G = exponent H.

Lemma isog_abelem p : p .-abelem G = p .-abelem H.

Lemma isog_grank : 'm (G ) = 'm (H ).

Lemma isog_p_rank p : 'r_p (G ) = 'r_p (H ).

Lemma isog_rank : 'r (G ) = 'r (H ).

End IsogAbelem.

Section QuotientAbelem.

Variables (gT : finGroupType) (p : nat).
Implicit Types E G K H : {group gT }.

Lemma exponent_quotient G H : exponent (G / H) %| exponent G.

Lemma quotient_LdivT n H : 'Ldiv_n / H \subset 'Ldiv_n.

Lemma quotient_Ldiv n A H : 'Ldiv_n (A ) / H \subset 'Ldiv_n (A / H ).

Lemma quotient_abelem G H : p .-abelem G → p .-abelem (G / H ).

Lemma quotient_pElem G H E : E \in 'E_p (G ) → (E / H)%G \in 'E_p (G / H ).

Lemma logn_quotient G H : logn p #|G / H | ≤ logn p #|G |.

Lemma quotient_pnElem G H n E :
  E \in 'E_p ^n (G ) → {m | m ≤ n & (E / H)%G \in 'E_p ^m (G / H )}.

Lemma quotient_grank G H : G \subset 'N (H ) → 'm (G / H ) ≤ 'm (G ).

Lemma p_rank_quotient G H : G \subset 'N (H ) → 'r_p (G ) - 'r_p (H ) ≤ 'r_p (G / H ).

Lemma p_rank_dprod K H G : K \x H = G → 'r_p (K ) + 'r_p (H ) = 'r_p (G ).

Lemma p_rank_p'quotient G H :
  (p : nat )^'.-group H → G \subset 'N (H ) → 'r_p (G / H ) = 'r_p (G ).

End QuotientAbelem.

Section OhmProps.

Section Generic.

Variables (n : nat) (gT : finGroupType).
Implicit Types (p : nat) (x : gT) (rT : finGroupType).
Implicit Types (A B : {set gT }) (D G H : {group gT }).

Lemma Ohm_sub G : 'Ohm_n (G ) \subset G.

Lemma Ohm1 : 'Ohm_n ([1 gT ]) = 1.

Lemma Ohm_id G : 'Ohm_n ('Ohm_n (G )) = 'Ohm_n (G ).

Lemma Ohm_cont rT G (f : {morphism G >-> rT }) :
  f @* 'Ohm_n (G ) \subset 'Ohm_n (f @* G ).

Lemma OhmS H G : H \subset G → 'Ohm_n (H ) \subset 'Ohm_n (G ).

Lemma OhmE p G : p .-group G → 'Ohm_n (G ) = <<'Ldiv_(p ^ n )(G )>>.

Lemma OhmEabelian p G :
  p .-group G → abelian 'Ohm_n (G ) → 'Ohm_n (G ) = 'Ldiv_(p ^ n )(G ).

Lemma Ohm_p_cycle p x :
  p .-elt x → 'Ohm_n (<[x ]>) = <[x ^+ (p ^ (logn p #[x ] - n ))]>.

Lemma Ohm_dprod A B G : A \x B = G → 'Ohm_n (A ) \x 'Ohm_n (B ) = 'Ohm_n (G ).

Lemma Mho_sub G : 'Mho ^n (G ) \subset G.

Lemma Mho1 : 'Mho ^n ([1 gT ]) = 1.

Lemma morphim_Mho rT D G (f : {morphism D >-> rT }) :
  G \subset D → f @* 'Mho ^n (G ) = 'Mho ^n (f @* G ).

Lemma Mho_cont rT G (f : {morphism G >-> rT }) :
  f @* 'Mho ^n (G ) \subset 'Mho ^n (f @* G ).

Lemma MhoS H G : H \subset G → 'Mho ^n (H ) \subset 'Mho ^n (G ).

Lemma MhoE p G : p .-group G → 'Mho ^n (G ) = <<[set x ^+ (p ^ n ) | x in G ]>>.

Lemma MhoEabelian p G :
  p .-group G → abelian G → 'Mho ^n (G ) = [set x ^+ (p ^ n ) | x in G ].

Lemma trivg_Mho G : 'Mho ^n (G ) == 1 → 'Ohm_n (G ) == G.

Lemma Mho_p_cycle p x : p .-elt x → 'Mho ^n (<[x ]>) = <[x ^+ (p ^ n )]>.

Lemma Mho_cprod A B G : A \* B = G → 'Mho ^n (A ) \* 'Mho ^n (B ) = 'Mho ^n (G ).

Lemma Mho_dprod A B G : A \x B = G → 'Mho ^n (A ) \x 'Mho ^n (B ) = 'Mho ^n (G ).

End Generic.

Canonical Ohm_igFun i := [igFun by Ohm_sub i & Ohm_cont i ].
Canonical Ohm_gFun i := [gFun by Ohm_cont i ].
Canonical Ohm_mgFun i := [mgFun by OhmS i ].

Canonical Mho_igFun i := [igFun by Mho_sub i & Mho_cont i ].
Canonical Mho_gFun i := [gFun by Mho_cont i ].
Canonical Mho_mgFun i := [mgFun by MhoS i ].

Section char.

Variables (n : nat) (gT rT : finGroupType) (D G : {group gT }).

Lemma Ohm_char : 'Ohm_n (G ) \char G.
Lemma Ohm_normal : 'Ohm_n (G ) <| G.

Lemma Mho_char : 'Mho ^n (G ) \char G.
Lemma Mho_normal : 'Mho ^n (G ) <| G.

Lemma morphim_Ohm (f : {morphism D >-> rT }) :
  G \subset D → f @* 'Ohm_n (G ) \subset 'Ohm_n (f @* G ).

Lemma injm_Ohm (f : {morphism D >-> rT }) :
  'injm f → G \subset D → f @* 'Ohm_n (G ) = 'Ohm_n (f @* G ).

Lemma isog_Ohm (H : {group rT }) : G \isog H → 'Ohm_n (G ) \isog 'Ohm_n (H ).

Lemma isog_Mho (H : {group rT }) : G \isog H → 'Mho ^n (G ) \isog 'Mho ^n (H ).

End char.

Variable gT : finGroupType.
Implicit Types (pi : nat_pred) (p : nat).
Implicit Types (A B C : {set gT }) (D G H E : {group gT }).

Lemma Ohm0 G : 'Ohm_0 (G ) = 1.

Lemma Ohm_leq m n G : m ≤ n → 'Ohm_m (G ) \subset 'Ohm_n (G ).

Lemma OhmJ n G x : 'Ohm_n (G :^ x ) = 'Ohm_n (G ) :^ x.

Lemma Mho0 G : 'Mho ^0(G ) = G.

Lemma Mho_leq m n G : m ≤ n → 'Mho ^n (G ) \subset 'Mho ^m (G ).

Lemma MhoJ n G x : 'Mho ^n (G :^ x ) = 'Mho ^n (G ) :^ x.

Lemma extend_cyclic_Mho G p x :
    p .-group G → x \in G → 'Mho ^1(G ) = <[x ^+ p ]> →
  ∀ k, k > 0 → 'Mho ^k (G ) = <[x ^+ (p ^ k )]>.

Lemma Ohm1Eprime G : 'Ohm_1 (G ) = <<[set x in G | prime #[x ]]>>.

Lemma abelem_Ohm1 p G : p .-group G → p .-abelem 'Ohm_1 (G ) = abelian 'Ohm_1 (G ).

Lemma Ohm1_abelem p G : p .-group G → abelian G → p .-abelem ('Ohm_1 (G )).

Lemma Ohm1_id p G : p .-abelem G → 'Ohm_1 (G ) = G.

Lemma abelem_Ohm1P p G :
  abelian G → p .-group G → reflect ('Ohm_1 (G ) = G) (p .-abelem G).

Lemma TI_Ohm1 G H : H :&: 'Ohm_1 (G ) = 1 → H :&: G = 1.

Lemma Ohm1_eq1 G : ('Ohm_1 (G ) == 1) = (G :==: 1).

Lemma meet_Ohm1 G H : G :&: H != 1 → G :&: 'Ohm_1 (H ) != 1.

Lemma Ohm1_cent_max G E p : E \in 'E ×_p (G ) → p .-group G → 'Ohm_1 ('C_G (E )) = E.

Lemma Ohm1_cyclic_pgroup_prime p G :
  cyclic G → p .-group G → G :!=: 1 → #|'Ohm_1 (G )| = p.

Lemma cyclic_pgroup_dprod_trivg p A B C :
    p .-group C → cyclic C → A \x B = C →
  A = 1 ∧ B = C ∨ B = 1 ∧ A = C.

Lemma piOhm1 G : \pi ('Ohm_1 (G )) = \pi (G ).

Lemma Ohm1Eexponent p G :
  prime p → exponent 'Ohm_1 (G ) %| p → 'Ohm_1 (G ) = 'Ldiv_p (G ).

Lemma p_rank_Ohm1 p G : 'r_p ('Ohm_1 (G )) = 'r_p (G ).

Lemma rank_Ohm1 G : 'r ('Ohm_1 (G )) = 'r (G ).

Lemma p_rank_abelian p G : abelian G → 'r_p (G ) = logn p #|'Ohm_1 (G )|.

Lemma rank_abelian_pgroup p G :
  p .-group G → abelian G → 'r (G ) = logn p #|'Ohm_1 (G )|.

End OhmProps.

Section AbelianStructure.

Variable gT : finGroupType.
Implicit Types (p : nat) (G H K E : {group gT }).

Lemma abelian_splits x G :
  x \in G → #[x ] = exponent G → abelian G → [splits G , over <[x ]>].

Lemma abelem_splits p G H : p .-abelem G → H \subset G → [splits G , over H ].

Fact abelian_type_subproof G :
  {H : {group gT } & abelian G → {x | #[x ] = exponent G & <[x ]> \x H = G }}.

Fixpoint abelian_type_rec n G :=
  if n is n'.+1 then if abelian G && (G :!=: 1) then
    exponent G :: abelian_type_rec n' (tag (abelian_type_subproof G))
  else [::] else [::].

Definition abelian_type (A : {set gT }) := abelian_type_rec #|A | <<A >>.

Lemma abelian_type_dvdn_sorted A : sorted [rel m n | n %| m ] (abelian_type A).

Lemma abelian_type_gt1 A : all [pred m | m > 1] (abelian_type A).

Lemma abelian_type_sorted A : sorted geq (abelian_type A).

Theorem abelian_structure G :
    abelian G →
  {b | \big [dprod /1]_(x <- b ) <[x ]> = G & map order b = abelian_type G }.

Lemma count_logn_dprod_cycle p n b G :
    \big [dprod /1]_(x <- b ) <[x ]> = G →
  count [pred x | logn p #[x ] > n ] b = logn p #|'Ohm_n .+1 (G ) : 'Ohm_n (G )|.

Lemma abelian_type_pgroup p b G :
    p .-group G → \big [dprod /1]_(x <- b ) <[x ]> = G → 1 \notin b →
  perm_eq (abelian_type G) (map order b).

Lemma size_abelian_type G : abelian G → size (abelian_type G) = 'r (G ).

Lemma mul_card_Ohm_Mho_abelian n G :
  abelian G → (#|'Ohm_n (G )| × #|'Mho ^n (G )|)%N = #|G |.

Lemma grank_abelian G : abelian G → 'm (G ) = 'r (G ).

Lemma rank_cycle (x : gT) : 'r (<[x ]>) = (x != 1).

Lemma abelian_rank1_cyclic G : abelian G → cyclic G = ('r (G ) ≤ 1).

Definition homocyclic A := abelian A && constant (abelian_type A).

Lemma homocyclic_Ohm_Mho n p G :
  p .-group G → homocyclic G → 'Ohm_n (G ) = 'Mho ^(logn p (exponent G) - n )(G ).

Lemma Ohm_Mho_homocyclic (n p : nat) G :
    abelian G → p .-group G → 0 < n < logn p (exponent G) →
  'Ohm_n (G ) = 'Mho ^(logn p (exponent G) - n )(G ) → homocyclic G.

Lemma abelem_homocyclic p G : p .-abelem G → homocyclic G.

Lemma homocyclic1 : homocyclic [1 gT ].

Lemma Ohm1_homocyclicP p G : p .-group G → abelian G →
  reflect ('Ohm_1 (G ) = 'Mho ^(logn p (exponent G)).-1 (G )) (homocyclic G).

Lemma abelian_type_homocyclic G :
  homocyclic G → abelian_type G = nseq 'r (G ) (exponent G).

Lemma abelian_type_abelem p G : p .-abelem G → abelian_type G = nseq 'r (G ) p.

Lemma max_card_abelian G :
  abelian G → #|G | ≤ exponent G ^ 'r (G ) ?= iff homocyclic G.

Lemma card_homocyclic G : homocyclic G → #|G | = (exponent G ^ 'r (G ))%N.

Lemma abelian_type_dprod_homocyclic p K H G :
    K \x H = G → p .-group G → homocyclic G →
     abelian_type K = nseq 'r (K ) (exponent G)
  ∧ abelian_type H = nseq 'r (H ) (exponent G).

Lemma dprod_homocyclic p K H G :
  K \x H = G → p .-group G → homocyclic G → homocyclic K ∧ homocyclic H.

Lemma exponent_dprod_homocyclic p K H G :
    K \x H = G → p .-group G → homocyclic G → K :!=: 1 →
  exponent K = exponent G.

End AbelianStructure.

Arguments abelian_type {gT} A%g.
Arguments homocyclic {gT} A%g.

Section IsogAbelian.

Variables aT rT : finGroupType.
Implicit Type (gT : finGroupType) (D G : {group aT }) (H : {group rT }).

Lemma isog_abelian_type G H : isog G H → abelian_type G = abelian_type H.

Lemma eq_abelian_type_isog G H :
  abelian G → abelian H → isog G H = (abelian_type G == abelian_type H ).

Lemma isog_abelem_card p G H :
  p .-abelem G → isog G H = p .-abelem H && (#|H | == #|G |).

Variables (D : {group aT }) (f : {morphism D >-> rT }).

Lemma morphim_rank_abelian G : abelian G → 'r (f @* G ) ≤ 'r (G ).

Lemma morphim_p_rank_abelian p G : abelian G → 'r_p (f @* G ) ≤ 'r_p (G ).

Lemma isog_homocyclic G H : G \isog H → homocyclic G = homocyclic H.

End IsogAbelian.

Section QuotientRank.

Variables (gT : finGroupType) (p : nat) (G H : {group gT }).
Hypothesis cGG : abelian G.

Lemma quotient_rank_abelian : 'r (G / H ) ≤ 'r (G ).

Lemma quotient_p_rank_abelian : 'r_p (G / H ) ≤ 'r_p (G ).

End QuotientRank.

Section FimModAbelem.

Import GRing.Theory FinRing.Theory.

Lemma fin_lmod_char_abelem p (R : ringType) (V : finLmodType R):
  p \in [char R ]%R → p .-abelem [set : V ].

Lemma fin_Fp_lmod_abelem p (V : finLmodType 'F_p) :
  prime p → p .-abelem [set : V ].

Lemma fin_ring_char_abelem p (R : finRingType) :
  p \in [char R ]%R → p .-abelem [set : R ].

End FimModAbelem.