Library frobenius

  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.                                                                
    [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 complement H] <=>                                     
       G is (isomorphic to) a Frobenius group with complement H; same as    
       above, but without the semi-direct product.                          
    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.        
 Note that at this point we do not have the existence or nilpotence of      
 Frobenius kernels. This is not a problem, because in all the applications  
 we make of Frobenius groups, the kernel and complement are already known.  


Import GroupScope.

Section Definitions.

Variable gT : finGroupType.
Implicit Types G K H : {set gT}.

 Corresponds to "H acts on K in a regular manner" in B & G. 
Definition semiregular K H := {in H^#, forall x, 'C_K[x] = 1}.

 Corresponds to "H acts on K in a prime manner" in B & G. 
Definition semiprime K H := {in H^#, forall x, 'C_K[x] = 'C_K(H)}.

Definition Frobenius_group_with_complement G H :=
  [&& H \proper G, trivIset (H^# :^: G) & 'N_G(H) == H].

Definition Frobenius_group_with_kernel_and_complement G K H :=
  (K ><| H == G) && Frobenius_group_with_complement G 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^#, forall 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 = 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 Type G H K R X : {group gT}.

Lemma semiregular1l : forall H, semiregular 1 H.

Lemma semiregular1r : forall K, semiregular K 1.

Lemma semiregular_sym : forall H K, semiregular K H -> semiregular H K.

Lemma semiregular_prime : forall H K, semiregular K H -> semiprime K H.

Lemma semiprime_regular : forall H K,
  semiprime K H -> 'C_K(H) = 1 -> semiregular K H.

Lemma cent_semiprime : forall H K X,
   semiprime K H -> X \subset H -> X :!=: 1 -> 'C_K(X) = 'C_K(H).

Lemma stab_semiprime : forall H K X,
   semiprime K H -> X \subset K -> 'C_H(X) != 1 -> 'C_H(X) = H.

Lemma cent_semiregular : forall H K X,
   semiregular K H -> X \subset H -> X :!=: 1 -> 'C_K(X) = 1.

Lemma regular_norm_dvd_pred : forall K H,
  H \subset 'N(K) -> semiregular K H -> #|H| %| #|K|.-1.

Lemma regular_norm_coprime : forall K H,
  H \subset 'N(K) -> semiregular K H -> coprime #|K| #|H|.

Lemma TIconjP : forall G H,
  reflect {in G &, forall x y, x * y^-1 \in 'N_G(H) \/ H :^ x :&: H :^ y = 1}
          (trivIset (H^# :^: G)).
Implicit Arguments TIconjP [G H].

Lemma TIconj_SN_P : forall G H,
    H :!=: 1 -> H \subset G ->
  reflect {in G :\: H, forall x, H :&: H :^ x = 1}
          (trivIset (H^# :^: G) && ('N_G(H) == H)).

Lemma Frobenius_actionP : forall G H,
  reflect (has_Frobenius_action G H) [Frobenius G with complement H].

Lemma Frobenius_context : forall G H K,
    [Frobenius G = K ><| H] ->
  [/\ K ><| H = G, K :!=: 1, H :!=: 1, K \proper G & H \proper G].

Lemma Frobenius_partition : forall G H K,
  [Frobenius G = K ><| H] -> partition (gval K |: (H^# :^: K)) G.

Lemma Frobenius_action_kernel_def : forall 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].

Lemma Frobenius_cent1_ker : forall G H K,
  [Frobenius G = K ><| H] -> {in K^#, forall x, 'C_G[x] \subset K}.

Lemma Frobenius_reg_ker : forall G H K,
  [Frobenius G = K ><| H] -> semiregular K H.

Lemma Frobenius_reg_compl : forall K H G,
  [Frobenius G = K ><| H] -> semiregular H K.

Lemma Frobenius_dvd_ker1 : forall G H K,
  [Frobenius G = K ><| H] -> #|H| %| #|K|.-1.

Lemma Frobenius_coprime : forall G H K,
  [Frobenius G = K ><| H] -> coprime #|K| #|H|.

Lemma Frobenius_ker_Hall : forall G H K,
  [Frobenius G = K ><| H] -> Hall G K.

Lemma Frobenius_compl_Hall : forall G H K,
  [Frobenius G = K ><| H] -> Hall G H.


Theorem Frobenius_kernel_exists : forall G H,
  [Frobenius G with complement H] -> group_set (G :\: cover (H^# :^: G)).
Admitted.


End FrobeniusBasics.

Theorem Frobenius_Ldiv : forall (gT : finGroupType) (G : {group gT}) n,
  n %| #|G| -> n %| #|'Ldiv_n(G)|.