Library mathcomp.solvable.frobenius
- -
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-
-
-- Distributed under the terms of CeCILL-B. *)
- -
-
- 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}.
- -
-
-
--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)|.
-