Library mathcomp.solvable.frobenius
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div.
From mathcomp Require Import fintype bigop prime finset fingroup morphism.
From mathcomp Require Import perm action quotient gproduct cyclic center.
From mathcomp Require Import pgroup nilpotent sylow hall abelian.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div.
From mathcomp Require Import fintype bigop prime finset fingroup morphism.
From mathcomp Require Import perm action quotient gproduct cyclic center.
From mathcomp Require Import pgroup nilpotent sylow hall abelian.
Definition of Frobenius groups, some basic results, and the Frobenius
theorem on the number of solutions of x ^+ n = 1.
semiregular K H <->
the internal action of H on K is semiregular, i.e., no nontrivial
elements of H and K commute; note that this is actually a symmetric
condition.
semiprime K H <->
the internal action of H on K is "prime", i.e., an element of K that
centralises a nontrivial element of H must centralise all of H.
normedTI A G L <=>
A is nonempty, strictly disjoint from its conjugates in G, and has
normaliser L in G.
[Frobenius G = K ><| H] <=>
G is (isomorphic to) a Frobenius group with kernel K and complement
H. This is an effective predicate (in bool), which tests the
equality with the semidirect product, and then the fact that H is a
proper self-normalizing TI-subgroup of G.
[Frobenius G with kernel H] <=>
G is (isomorphic to) a Frobenius group with kernel K; same as above,
but without the semi-direct product.
[Frobenius G with complement H] <=>
G is (isomorphic to) a Frobenius group with complement H; same as
above, but without the semi-direct product. The proof that this form
is equivalent to the above (i.e., the existence of Frobenius
kernels) requires character theory and will only be proved in the
vcharacter.v file.
[Frobenius G] <=> G is a Frobenius group.
Frobenius_action G H S to <->
The action to of G on S defines an isomorphism of G with a
(permutation) Frobenius group, i.e., to is faithful and transitive
on S, no nontrivial element of G fixes more than one point in S, and
H is the stabilizer of some element of S, and non-trivial. Thus,
Frobenius_action G H S 'P
asserts that G is a Frobenius group in the classic sense.
has_Frobenius_action G H <->
Frobenius_action G H S to holds for some sT : finType, S : {set st}
and to : {action gT &-> sT}. This is a predicate in Prop, but is
exactly reflected by [Frobenius G with complement H] : bool.
Set Implicit Arguments.
Import GroupScope.
Section Definitions.
Variable gT : finGroupType.
Implicit Types A G K H L : {set gT}.
Corresponds to "H acts on K in a regular manner" in B & G.
Corresponds to "H acts on K in a prime manner" in B & G.
Definition semiprime K H := {in H^#, ∀ x, 'C_K[x] = 'C_K(H)}.
Definition normedTI A G L := [&& A != set0, trivIset (A :^: G) & 'N_G(A) == L].
Definition Frobenius_group_with_complement G H := (H != G) && normedTI H^# G H.
Definition Frobenius_group G :=
[∃ H : {group gT}, Frobenius_group_with_complement G H].
Definition Frobenius_group_with_kernel_and_complement G K H :=
(K ><| H == G) && Frobenius_group_with_complement G H.
Definition Frobenius_group_with_kernel G K :=
[∃ H : {group gT}, Frobenius_group_with_kernel_and_complement G K H].
Section FrobeniusAction.
Variables G H : {set gT}.
Variables (sT : finType) (S : {set sT}) (to : {action gT &-> sT}).
Definition Frobenius_action :=
[/\ [faithful G, on S | to],
[transitive G, on S | to],
{in G^#, ∀ x, #|'Fix_(S | to)[x]| ≤ 1},
H != 1
& exists2 u, u \in S & H = 'C_G[u | to]].
End FrobeniusAction.
Variant has_Frobenius_action G H : Prop :=
HasFrobeniusAction sT S to of @Frobenius_action G H sT S to.
End Definitions.
Notation "[ 'Frobenius' G 'with' 'complement' H ]" :=
(Frobenius_group_with_complement G H)
(at level 0, G at level 50, H at level 35,
format "[ 'Frobenius' G 'with' 'complement' H ]") : group_scope.
Notation "[ 'Frobenius' G 'with' 'kernel' K ]" :=
(Frobenius_group_with_kernel G K)
(at level 0, G at level 50, K at level 35,
format "[ 'Frobenius' G 'with' 'kernel' K ]") : group_scope.
Notation "[ 'Frobenius' G ]" :=
(Frobenius_group G)
(at level 0, G at level 50,
format "[ 'Frobenius' G ]") : group_scope.
Notation "[ 'Frobenius' G = K ><| H ]" :=
(Frobenius_group_with_kernel_and_complement G K H)
(at level 0, G at level 50, K, H at level 35,
format "[ 'Frobenius' G = K ><| H ]") : group_scope.
Section FrobeniusBasics.
Variable gT : finGroupType.
Implicit Types (A B : {set gT}) (G H K L R X : {group gT}).
Lemma semiregular1l H : semiregular 1 H.
Lemma semiregular1r K : semiregular K 1.
Lemma semiregular_sym H K : semiregular K H → semiregular H K.
Lemma semiregularS K1 K2 A1 A2 :
K1 \subset K2 → A1 \subset A2 → semiregular K2 A2 → semiregular K1 A1.
Lemma semiregular_prime H K : semiregular K H → semiprime K H.
Lemma semiprime_regular H K : semiprime K H → 'C_K(H) = 1 → semiregular K H.
Lemma semiprimeS K1 K2 A1 A2 :
K1 \subset K2 → A1 \subset A2 → semiprime K2 A2 → semiprime K1 A1.
Lemma cent_semiprime H K X :
semiprime K H → X \subset H → X :!=: 1 → 'C_K(X) = 'C_K(H).
Lemma stab_semiprime H K X :
semiprime K H → X \subset K → 'C_H(X) != 1 → 'C_H(X) = H.
Lemma cent_semiregular H K X :
semiregular K H → X \subset H → X :!=: 1 → 'C_K(X) = 1.
Lemma regular_norm_dvd_pred K H :
H \subset 'N(K) → semiregular K H → #|H| %| #|K|.-1.
Lemma regular_norm_coprime K H :
H \subset 'N(K) → semiregular K H → coprime #|K| #|H|.
Lemma semiregularJ K H x : semiregular K H → semiregular (K :^ x) (H :^ x).
Lemma semiprimeJ K H x : semiprime K H → semiprime (K :^ x) (H :^ x).
Lemma normedTI_P A G L :
reflect [/\ A != set0, L \subset 'N_G(A)
& {in G, ∀ g, ~~ [disjoint A & A :^ g] → g \in L}]
(normedTI A G L).
Lemma normedTI_memJ_P A G L :
reflect [/\ A != set0, L \subset G
& {in A & G, ∀ a g, (a ^ g \in A) = (g \in L)}]
(normedTI A G L).
Lemma partition_class_support A G :
A != set0 → trivIset (A :^: G) → partition (A :^: G) (class_support A G).
Lemma partition_normedTI A G L :
normedTI A G L → partition (A :^: G) (class_support A G).
Lemma card_support_normedTI A G L :
normedTI A G L → #|class_support A G| = (#|A| × #|G : L|)%N.
Lemma normedTI_S A B G L :
A != set0 → L \subset 'N(A) → A \subset B → normedTI B G L →
normedTI A G L.
Lemma cent1_normedTI A G L :
normedTI A G L → {in A, ∀ x, 'C_G[x] \subset L}.
Lemma Frobenius_actionP G H :
reflect (has_Frobenius_action G H) [Frobenius G with complement H].
Section FrobeniusProperties.
Variables G H K : {group gT}.
Hypothesis frobG : [Frobenius G = K ><| H].
Lemma FrobeniusWker : [Frobenius G with kernel K].
Lemma FrobeniusWcompl : [Frobenius G with complement H].
Lemma FrobeniusW : [Frobenius G].
Lemma Frobenius_context :
[/\ K ><| H = G, K :!=: 1, H :!=: 1, K \proper G & H \proper G].
Lemma Frobenius_partition : partition (gval K |: (H^# :^: K)) G.
Lemma Frobenius_cent1_ker : {in K^#, ∀ x, 'C_G[x] \subset K}.
Lemma Frobenius_reg_ker : semiregular K H.
Lemma Frobenius_reg_compl : semiregular H K.
Lemma Frobenius_dvd_ker1 : #|H| %| #|K|.-1.
Lemma ltn_odd_Frobenius_ker : odd #|G| → #|H|.*2 < #|K|.
Lemma Frobenius_index_dvd_ker1 : #|G : K| %| #|K|.-1.
Lemma Frobenius_coprime : coprime #|K| #|H|.
Lemma Frobenius_trivg_cent : 'C_K(H) = 1.
Lemma Frobenius_index_coprime : coprime #|K| #|G : K|.
Lemma Frobenius_ker_Hall : Hall G K.
Lemma Frobenius_compl_Hall : Hall G H.
End FrobeniusProperties.
Lemma normedTI_J x A G L : normedTI (A :^ x) (G :^ x) (L :^ x) = normedTI A G L.
Lemma FrobeniusJcompl x G H :
[Frobenius G :^ x with complement H :^ x] = [Frobenius G with complement H].
Lemma FrobeniusJ x G K H :
[Frobenius G :^ x = K :^ x ><| H :^ x] = [Frobenius G = K ><| H].
Lemma FrobeniusJker x G K :
[Frobenius G :^ x with kernel K :^ x] = [Frobenius G with kernel K].
Lemma FrobeniusJgroup x G : [Frobenius G :^ x] = [Frobenius G].
Lemma Frobenius_ker_dvd_ker1 G K :
[Frobenius G with kernel K] → #|G : K| %| #|K|.-1.
Lemma Frobenius_ker_coprime G K :
[Frobenius G with kernel K] → coprime #|K| #|G : K|.
Lemma Frobenius_semiregularP G K H :
K ><| H = G → K :!=: 1 → H :!=: 1 →
reflect (semiregular K H) [Frobenius G = K ><| H].
Lemma prime_FrobeniusP G K H :
K :!=: 1 → prime #|H| →
reflect (K ><| H = G ∧ 'C_K(H) = 1) [Frobenius G = K ><| H].
Lemma Frobenius_subl G K K1 H :
K1 :!=: 1 → K1 \subset K → H \subset 'N(K1) → [Frobenius G = K ><| H] →
[Frobenius K1 <*> H = K1 ><| H].
Lemma Frobenius_subr G K H H1 :
H1 :!=: 1 → H1 \subset H → [Frobenius G = K ><| H] →
[Frobenius K <*> H1 = K ><| H1].
Lemma Frobenius_kerP G K :
reflect [/\ K :!=: 1, K \proper G, K <| G
& {in K^#, ∀ x, 'C_G[x] \subset K}]
[Frobenius G with kernel K].
Lemma set_Frobenius_compl G K H :
K ><| H = G → [Frobenius G with kernel K] → [Frobenius G = K ><| H].
Lemma Frobenius_kerS G K G1 :
G1 \subset G → K \proper G1 →
[Frobenius G with kernel K] → [Frobenius G1 with kernel K].
Lemma Frobenius_action_kernel_def G H K sT S to :
K ><| H = G → @Frobenius_action _ G H sT S to →
K :=: 1 :|: [set x in G | 'Fix_(S | to)[x] == set0].
End FrobeniusBasics.
Lemma Frobenius_coprime_quotient (gT : finGroupType) (G K H N : {group gT}) :
K ><| H = G → N <| G → coprime #|K| #|H| ∧ H :!=: 1%g →
N \proper K ∧ {in H^#, ∀ x, 'C_K[x] \subset N} →
[Frobenius G / N = (K / N) ><| (H / N)]%g.
Section InjmFrobenius.
Variables (gT rT : finGroupType) (D G : {group gT}) (f : {morphism D >-> rT}).
Implicit Types (H K : {group gT}) (sGD : G \subset D) (injf : 'injm f).
Lemma injm_Frobenius_compl H sGD injf :
[Frobenius G with complement H] → [Frobenius f @* G with complement f @* H].
Lemma injm_Frobenius H K sGD injf :
[Frobenius G = K ><| H] → [Frobenius f @* G = f @* K ><| f @* H].
Lemma injm_Frobenius_ker K sGD injf :
[Frobenius G with kernel K] → [Frobenius f @* G with kernel f @* K].
Lemma injm_Frobenius_group sGD injf : [Frobenius G] → [Frobenius f @* G].
End InjmFrobenius.
Theorem Frobenius_Ldiv (gT : finGroupType) (G : {group gT}) n :
n %| #|G| → n %| #|'Ldiv_n(G)|.
Definition normedTI A G L := [&& A != set0, trivIset (A :^: G) & 'N_G(A) == L].
Definition Frobenius_group_with_complement G H := (H != G) && normedTI H^# G H.
Definition Frobenius_group G :=
[∃ H : {group gT}, Frobenius_group_with_complement G H].
Definition Frobenius_group_with_kernel_and_complement G K H :=
(K ><| H == G) && Frobenius_group_with_complement G H.
Definition Frobenius_group_with_kernel G K :=
[∃ H : {group gT}, Frobenius_group_with_kernel_and_complement G K H].
Section FrobeniusAction.
Variables G H : {set gT}.
Variables (sT : finType) (S : {set sT}) (to : {action gT &-> sT}).
Definition Frobenius_action :=
[/\ [faithful G, on S | to],
[transitive G, on S | to],
{in G^#, ∀ x, #|'Fix_(S | to)[x]| ≤ 1},
H != 1
& exists2 u, u \in S & H = 'C_G[u | to]].
End FrobeniusAction.
Variant has_Frobenius_action G H : Prop :=
HasFrobeniusAction sT S to of @Frobenius_action G H sT S to.
End Definitions.
Notation "[ 'Frobenius' G 'with' 'complement' H ]" :=
(Frobenius_group_with_complement G H)
(at level 0, G at level 50, H at level 35,
format "[ 'Frobenius' G 'with' 'complement' H ]") : group_scope.
Notation "[ 'Frobenius' G 'with' 'kernel' K ]" :=
(Frobenius_group_with_kernel G K)
(at level 0, G at level 50, K at level 35,
format "[ 'Frobenius' G 'with' 'kernel' K ]") : group_scope.
Notation "[ 'Frobenius' G ]" :=
(Frobenius_group G)
(at level 0, G at level 50,
format "[ 'Frobenius' G ]") : group_scope.
Notation "[ 'Frobenius' G = K ><| H ]" :=
(Frobenius_group_with_kernel_and_complement G K H)
(at level 0, G at level 50, K, H at level 35,
format "[ 'Frobenius' G = K ><| H ]") : group_scope.
Section FrobeniusBasics.
Variable gT : finGroupType.
Implicit Types (A B : {set gT}) (G H K L R X : {group gT}).
Lemma semiregular1l H : semiregular 1 H.
Lemma semiregular1r K : semiregular K 1.
Lemma semiregular_sym H K : semiregular K H → semiregular H K.
Lemma semiregularS K1 K2 A1 A2 :
K1 \subset K2 → A1 \subset A2 → semiregular K2 A2 → semiregular K1 A1.
Lemma semiregular_prime H K : semiregular K H → semiprime K H.
Lemma semiprime_regular H K : semiprime K H → 'C_K(H) = 1 → semiregular K H.
Lemma semiprimeS K1 K2 A1 A2 :
K1 \subset K2 → A1 \subset A2 → semiprime K2 A2 → semiprime K1 A1.
Lemma cent_semiprime H K X :
semiprime K H → X \subset H → X :!=: 1 → 'C_K(X) = 'C_K(H).
Lemma stab_semiprime H K X :
semiprime K H → X \subset K → 'C_H(X) != 1 → 'C_H(X) = H.
Lemma cent_semiregular H K X :
semiregular K H → X \subset H → X :!=: 1 → 'C_K(X) = 1.
Lemma regular_norm_dvd_pred K H :
H \subset 'N(K) → semiregular K H → #|H| %| #|K|.-1.
Lemma regular_norm_coprime K H :
H \subset 'N(K) → semiregular K H → coprime #|K| #|H|.
Lemma semiregularJ K H x : semiregular K H → semiregular (K :^ x) (H :^ x).
Lemma semiprimeJ K H x : semiprime K H → semiprime (K :^ x) (H :^ x).
Lemma normedTI_P A G L :
reflect [/\ A != set0, L \subset 'N_G(A)
& {in G, ∀ g, ~~ [disjoint A & A :^ g] → g \in L}]
(normedTI A G L).
Lemma normedTI_memJ_P A G L :
reflect [/\ A != set0, L \subset G
& {in A & G, ∀ a g, (a ^ g \in A) = (g \in L)}]
(normedTI A G L).
Lemma partition_class_support A G :
A != set0 → trivIset (A :^: G) → partition (A :^: G) (class_support A G).
Lemma partition_normedTI A G L :
normedTI A G L → partition (A :^: G) (class_support A G).
Lemma card_support_normedTI A G L :
normedTI A G L → #|class_support A G| = (#|A| × #|G : L|)%N.
Lemma normedTI_S A B G L :
A != set0 → L \subset 'N(A) → A \subset B → normedTI B G L →
normedTI A G L.
Lemma cent1_normedTI A G L :
normedTI A G L → {in A, ∀ x, 'C_G[x] \subset L}.
Lemma Frobenius_actionP G H :
reflect (has_Frobenius_action G H) [Frobenius G with complement H].
Section FrobeniusProperties.
Variables G H K : {group gT}.
Hypothesis frobG : [Frobenius G = K ><| H].
Lemma FrobeniusWker : [Frobenius G with kernel K].
Lemma FrobeniusWcompl : [Frobenius G with complement H].
Lemma FrobeniusW : [Frobenius G].
Lemma Frobenius_context :
[/\ K ><| H = G, K :!=: 1, H :!=: 1, K \proper G & H \proper G].
Lemma Frobenius_partition : partition (gval K |: (H^# :^: K)) G.
Lemma Frobenius_cent1_ker : {in K^#, ∀ x, 'C_G[x] \subset K}.
Lemma Frobenius_reg_ker : semiregular K H.
Lemma Frobenius_reg_compl : semiregular H K.
Lemma Frobenius_dvd_ker1 : #|H| %| #|K|.-1.
Lemma ltn_odd_Frobenius_ker : odd #|G| → #|H|.*2 < #|K|.
Lemma Frobenius_index_dvd_ker1 : #|G : K| %| #|K|.-1.
Lemma Frobenius_coprime : coprime #|K| #|H|.
Lemma Frobenius_trivg_cent : 'C_K(H) = 1.
Lemma Frobenius_index_coprime : coprime #|K| #|G : K|.
Lemma Frobenius_ker_Hall : Hall G K.
Lemma Frobenius_compl_Hall : Hall G H.
End FrobeniusProperties.
Lemma normedTI_J x A G L : normedTI (A :^ x) (G :^ x) (L :^ x) = normedTI A G L.
Lemma FrobeniusJcompl x G H :
[Frobenius G :^ x with complement H :^ x] = [Frobenius G with complement H].
Lemma FrobeniusJ x G K H :
[Frobenius G :^ x = K :^ x ><| H :^ x] = [Frobenius G = K ><| H].
Lemma FrobeniusJker x G K :
[Frobenius G :^ x with kernel K :^ x] = [Frobenius G with kernel K].
Lemma FrobeniusJgroup x G : [Frobenius G :^ x] = [Frobenius G].
Lemma Frobenius_ker_dvd_ker1 G K :
[Frobenius G with kernel K] → #|G : K| %| #|K|.-1.
Lemma Frobenius_ker_coprime G K :
[Frobenius G with kernel K] → coprime #|K| #|G : K|.
Lemma Frobenius_semiregularP G K H :
K ><| H = G → K :!=: 1 → H :!=: 1 →
reflect (semiregular K H) [Frobenius G = K ><| H].
Lemma prime_FrobeniusP G K H :
K :!=: 1 → prime #|H| →
reflect (K ><| H = G ∧ 'C_K(H) = 1) [Frobenius G = K ><| H].
Lemma Frobenius_subl G K K1 H :
K1 :!=: 1 → K1 \subset K → H \subset 'N(K1) → [Frobenius G = K ><| H] →
[Frobenius K1 <*> H = K1 ><| H].
Lemma Frobenius_subr G K H H1 :
H1 :!=: 1 → H1 \subset H → [Frobenius G = K ><| H] →
[Frobenius K <*> H1 = K ><| H1].
Lemma Frobenius_kerP G K :
reflect [/\ K :!=: 1, K \proper G, K <| G
& {in K^#, ∀ x, 'C_G[x] \subset K}]
[Frobenius G with kernel K].
Lemma set_Frobenius_compl G K H :
K ><| H = G → [Frobenius G with kernel K] → [Frobenius G = K ><| H].
Lemma Frobenius_kerS G K G1 :
G1 \subset G → K \proper G1 →
[Frobenius G with kernel K] → [Frobenius G1 with kernel K].
Lemma Frobenius_action_kernel_def G H K sT S to :
K ><| H = G → @Frobenius_action _ G H sT S to →
K :=: 1 :|: [set x in G | 'Fix_(S | to)[x] == set0].
End FrobeniusBasics.
Lemma Frobenius_coprime_quotient (gT : finGroupType) (G K H N : {group gT}) :
K ><| H = G → N <| G → coprime #|K| #|H| ∧ H :!=: 1%g →
N \proper K ∧ {in H^#, ∀ x, 'C_K[x] \subset N} →
[Frobenius G / N = (K / N) ><| (H / N)]%g.
Section InjmFrobenius.
Variables (gT rT : finGroupType) (D G : {group gT}) (f : {morphism D >-> rT}).
Implicit Types (H K : {group gT}) (sGD : G \subset D) (injf : 'injm f).
Lemma injm_Frobenius_compl H sGD injf :
[Frobenius G with complement H] → [Frobenius f @* G with complement f @* H].
Lemma injm_Frobenius H K sGD injf :
[Frobenius G = K ><| H] → [Frobenius f @* G = f @* K ><| f @* H].
Lemma injm_Frobenius_ker K sGD injf :
[Frobenius G with kernel K] → [Frobenius f @* G with kernel f @* K].
Lemma injm_Frobenius_group sGD injf : [Frobenius G] → [Frobenius f @* G].
End InjmFrobenius.
Theorem Frobenius_Ldiv (gT : finGroupType) (G : {group gT}) n :
n %| #|G| → n %| #|'Ldiv_n(G)|.