-
Definition semiprime K H :=
{in H^#, ∀ x,
'C_K[x] = 'C_K(H)}.
+
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 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_with_complement G H :=
(H != G) && normedTI H^# G H.
Definition Frobenius_group G :=
-
[∃ H : {group gT}, Frobenius_group_with_complement G H].
+
[∃ 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.
+
(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].
+
[∃ 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}).
+
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]].
+
[/\ [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 :=
+
Variant has_Frobenius_action G H :
Prop :=
HasFrobeniusAction sT S to of @
Frobenius_action G H sT S to.
@@ -145,25 +144,25 @@
-
Notation "[ 'Frobenius' G 'with' 'complement' H ]" :=
+
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 ]" :=
+
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 ]" :=
+
Notation "[ 'Frobenius' G ]" :=
(
Frobenius_group G)
(
at level 0,
G at level 50,
format "[ 'Frobenius' G ]") :
group_scope.
-
Notation "[ 'Frobenius' G = K ><| H ]" :=
+
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.
@@ -173,7 +172,7 @@
Variable gT :
finGroupType.
-
Implicit Types (
A B :
{set gT}) (
G H K L R X :
{group gT}).
+
Implicit Types (
A B :
{set gT}) (
G H K L R X :
{group gT}).
Lemma semiregular1l H :
semiregular 1
H.
@@ -182,110 +181,110 @@
Lemma semiregular1r K :
semiregular K 1.
-
Lemma semiregular_sym H K :
semiregular K H → semiregular H K.
+
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.
+
K1 \subset K2 → A1 \subset A2 → semiregular K2 A2 → semiregular K1 A1.
-
Lemma semiregular_prime H K :
semiregular K H → semiprime K H.
+
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 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.
+
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).
+
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.
+
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.
+
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.
+
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|.
+
H \subset 'N(K) → semiregular K H → coprime #|K| #|H|.
-
Lemma semiregularJ K H x :
semiregular K H → semiregular (
K :^ x) (
H :^ x).
+
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 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}]
+
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)}]
+
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).
+
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).
+
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.
+
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 →
+
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}.
+
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].
+
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].
+
Variables G H K :
{group gT}.
+
Hypothesis frobG :
[Frobenius G = K ><| H].
-
Lemma FrobeniusWker :
[Frobenius G with kernel K].
+
Lemma FrobeniusWker :
[Frobenius G with kernel K].
-
Lemma FrobeniusWcompl :
[Frobenius G with complement H].
+
Lemma FrobeniusWcompl :
[Frobenius G with complement H].
-
Lemma FrobeniusW :
[Frobenius G].
+
Lemma FrobeniusW :
[Frobenius G].
Lemma Frobenius_context :
-
[/\ K ><| H = G, K :!=: 1
, H :!=: 1
, K \proper G & H \proper G].
+
[/\ K ><| H = G, K :!=: 1
, H :!=: 1
, K \proper G & H \proper G].
-
Lemma Frobenius_partition :
partition (
gval K |: (H^# :^: K))
G.
+
Lemma Frobenius_partition :
partition (
gval K |: (H^# :^: K))
G.
-
Lemma Frobenius_cent1_ker :
{in K^#, ∀ x,
'C_G[x] \subset K}.
+
Lemma Frobenius_cent1_ker :
{in K^#, ∀ x,
'C_G[x] \subset K}.
Lemma Frobenius_reg_ker :
semiregular K H.
@@ -294,22 +293,22 @@
Lemma Frobenius_reg_compl :
semiregular H K.
-
Lemma Frobenius_dvd_ker1 :
#|H| %| #|K|.-1.
+
Lemma Frobenius_dvd_ker1 :
#|H| %| #|K|.-1.
-
Lemma ltn_odd_Frobenius_ker :
odd #|G| → #|H|.*2 < #|K|.
+
Lemma ltn_odd_Frobenius_ker :
odd #|G| → #|H|.*2 < #|K|.
-
Lemma Frobenius_index_dvd_ker1 :
#|G : K| %| #|K|.-1.
+
Lemma Frobenius_index_dvd_ker1 :
#|G : K| %| #|K|.-1.
-
Lemma Frobenius_coprime :
coprime #|K| #|H|.
+
Lemma Frobenius_coprime :
coprime #|K| #|H|.
-
Lemma Frobenius_trivg_cent :
'C_K(H) = 1.
+
Lemma Frobenius_trivg_cent :
'C_K(H) = 1.
-
Lemma Frobenius_index_coprime :
coprime #|K| #|G : K|.
+
Lemma Frobenius_index_coprime :
coprime #|K| #|G : K|.
Lemma Frobenius_ker_Hall :
Hall G K.
@@ -321,70 +320,70 @@
End FrobeniusProperties.
-
Lemma normedTI_J x A G L :
normedTI (
A :^ x) (
G :^ x) (
L :^ x)
= normedTI A G L.
+
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].
+
[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].
+
[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].
+
[Frobenius G :^ x with kernel K :^ x] = [Frobenius G with kernel K].
-
Lemma FrobeniusJgroup x G :
[Frobenius G :^ x] = [Frobenius G].
+
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.
+
[Frobenius G with kernel K] → #|G : K| %| #|K|.-1.
Lemma Frobenius_ker_coprime G K :
-
[Frobenius G with kernel K] → coprime #|K| #|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].
+
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].
+
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].
+
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].
+
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].
+
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].
+
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].
+
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].
+
K ><| H = G → @
Frobenius_action _ G H sT S to →
+
K :=: 1
:|: [set x in G | 'Fix_(S | to)[x] == set0].
End FrobeniusBasics.
@@ -392,39 +391,39 @@
-
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.
+
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).
+
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].
+
[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].
+
[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].
+
[Frobenius G with kernel K] → [Frobenius f @* G with kernel f @* K].
-
Lemma injm_Frobenius_group sGD injf :
[Frobenius G] → [Frobenius f @* G].
+
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)|.
+
Theorem Frobenius_Ldiv (
gT :
finGroupType) (
G :
{group gT})
n :
+
n %| #|G| → n %| #|'Ldiv_n(G)|.