(Joint Center)Library MathComp.frobenius

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat div fintype bigop prime.
Require Import finset fingroup morphism perm action quotient gproduct.
Require Import cyclic center 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 actually 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 chareacter theory and will only be proved in the vcharacter module. [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.
Definition semiregular K H := {in H^#, x, 'C_K[x] = 1}.

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 Hsemiregular H K.

Lemma semiregularS K1 K2 A1 A2 :
  K1 \subset K2A1 \subset A2semiregular K2 A2semiregular K1 A1.

Lemma semiregular_prime H K : semiregular K Hsemiprime 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 K2A1 \subset A2semiprime K2 A2semiprime K1 A1.

Lemma cent_semiprime H K X :
   semiprime K HX \subset HX :!=: 1 → 'C_K(X) = 'C_K(H).

Lemma stab_semiprime H K X :
   semiprime K HX \subset K'C_H(X) != 1 → 'C_H(X) = H.

Lemma cent_semiregular H K X :
   semiregular K HX \subset HX :!=: 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 Hcoprime #|K| #|H|.

Lemma semiregularJ K H x : semiregular K Hsemiregular (K :^ x) (H :^ x).

Lemma semiprimeJ K H x : semiprime K Hsemiprime (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 != set0trivIset (A :^: G) → partition (A :^: G) (class_support A G).

Lemma partition_normedTI A G L :
  normedTI A G Lpartition (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 != set0L \subset 'N(A)A \subset BnormedTI 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 = GK :!=: 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 KH \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 GK \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 = GN <| Gcoprime #|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)|.