Library mathcomp.solvable.abelian
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
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.
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.
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.
Implicit 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).
Implicit 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.
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)).
Implicit 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)).
Implicit 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)).
Implicit 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.
Implicit Arguments LdivP [gT A n x].
Implicit Arguments exponentP [gT A n].
Implicit Arguments abelemP [gT p G].
Implicit Arguments is_abelemP [gT G].
Implicit Arguments pElemP [gT p A E].
Implicit Arguments pnElemP [gT p n A E].
Implicit Arguments nElemP [gT n G E].
Implicit Arguments nElem1P [gT G E].
Implicit Arguments pmaxElemP [gT p A E].
Implicit Arguments pmaxElem_LdivP [gT p G E].
Implicit Arguments p_rank_geP [gT p n G].
Implicit 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 perm_eq_abelian_type p b G :
p.-group G → \big[dprod/1]_(x <- b) <[x]> = G → 1 \notin b →
perm_eq (map order b) (abelian_type G).
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.
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.