Library mathcomp.solvable.frobenius
(* (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.
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.
CoInductive 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).
Implicit Arguments normedTI_P [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.
Implicit Arguments normedTI_P [gT A G L].
Implicit Arguments normedTI_memJ_P [gT A G L].
Implicit Arguments Frobenius_kerP [gT G K].
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.
CoInductive 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).
Implicit Arguments normedTI_P [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.
Implicit Arguments normedTI_P [gT A G L].
Implicit Arguments normedTI_memJ_P [gT A G L].
Implicit Arguments Frobenius_kerP [gT G K].
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)|.