Library jordanholder

 This files establishes Jordan-Hölder theorems for finite groups. These     
 theorems state the uniqueness up to permutation and isomorphism for the    
 series of quotient built from the successive elements of any composition   
 series of the same group. These quotients are also called factors of the   
 composition series. To avoid the heavy use of highly polymorphic lists     
 describing these quotient series, we introduce sections.                   
 This library defines:                                                      
         (G1 / G2)%sec == alias for the pair (G1, G2) of groups in the same 
                          finGroupType, coerced to the actual quotient group
                          G1 / G2. We call this pseudo-quotient a section of
                          G1 and G2.                                        
    section_isog s1 s2 == s1 and s2 respectively coerce to isomorphic       
                          quotient groups.                                  
        section_repr s == canonical representative of the isomorphism class 
                          of the section s.                                 
         mksrepr G1 G2 == canonical representative of the isomorphism class 
                          of (G1 / G2)%sec.                                 
         mkfactors G s == if s is [:: s1, s2, ..., sn], constructs the list 
                      [:: mksrepr G s1, mksrepr s1 s2, ..., mksrepr sn-1 sn]
             comps G s == s is a composition series for G i.e. s is a       
                          decreasing sequence of subgroups of G             
                          in which two adjacent elements are maxnormal one  
                          in the other and the last element of s is 1.      
 Given aT and rT two finGroupTypes, (D : {group rT}), (A : {group aT}) and  
 (to : groupAction A D) an external action.                                 
        maxainv to B C == C is a maximal proper normal subgroup of B        
                          invariant by (the external action of A via) to.   
          asimple to B == the maximal proper normal subgroup of B invariant 
                          by the external action to is trivial.             
         acomps to G s == s is a composition series for G invariant by to,  
                          i.e. s is a decreasing sequence of subgroups of G 
                          in which two adjacent elements are maximally      
                          invariant by to one in the other and the          
                          last element of s is 1.                           
 We prove two versions of the result:                                       
    - JordanHolderUniqueness establishes the uniqueness up to permutation   
       and isomorphism of the lists of factors in composition series of a   
       given group.                                                         
    - StrongJordanHolderUniqueness extends the result to composition series 
       invariant by an external group action.                               

Import GroupScope.


Inductive section (gT : finGroupType) : Type := Sec of {group gT} * {group gT}.

Delimit Scope section_scope with sec.

Definition mkSec (gT : finGroupType)(G1 G2 : {group gT}) := Sec (G1, G2).

Infix "/" := mkSec : section_scope.

Coercion pair_of_section gT (s : section gT) := let: Sec u := s in u.

Coercion quotient_of_section gT (s : section gT) : GroupSet.sort _ :=
  s.1 / s.2.

Coercion section_group gT (s : section gT) : {group (coset_of s.2)} :=
  Eval hnf in [group of s].

Section Sections.

Variables (gT : finGroupType).

Implicit Types G : {group gT}.
Implicit Types s : section gT.

Canonical Structure section_subType :=
  Eval hnf in [newType for (@pair_of_section _) by (@section_rect gT)].
Definition section_eqMixin := Eval hnf in [eqMixin of (section _) by <:].
Canonical Structure section_eqType :=
  Eval hnf in EqType (section _) section_eqMixin.
Definition section_choiceMixin := [choiceMixin of (section _) by <:].
Canonical Structure section_choiceType :=
  Eval hnf in ChoiceType (section _) section_choiceMixin.
Definition section_countMixin := [countMixin of (section _) by <:].
Canonical Structure section_countType :=
   Eval hnf in CountType (section _) section_countMixin.
Canonical Structure section_subCountType :=
  Eval hnf in [subCountType of (section _)].
Definition section_finMixin := [finMixin of (section _) by <:].
Canonical Structure section_finType :=
  Eval hnf in FinType (section _) section_finMixin.
Canonical Structure section_subFinType :=
  Eval hnf in [subFinType of (section _)].
Canonical Structure section_group.

 Isomorphic sections 

Definition section_isog := [rel x y : section gT | x \isog y].

 A witness of the isomorphism class of a section 
Definition section_repr s :=
  if (pick (section_isog ^~ s)) is Some s then s else (mkSec 1 1)%sec.

Definition mksrepr G1 G2 := section_repr (mkSec G1 G2).

Lemma section_reprP : forall s, (section_repr s) \isog s.

Lemma section_repr_isog : forall s1 s2,
  s1 \isog s2 -> section_repr s1 = section_repr s2.

Definition mkfactors (G : {group gT}) (s : seq {group gT}) :=
  map section_repr (pairmap (@mkSec _) G s).

End Sections.

Section CompositionSeries.

Variables (gT : finGroupType).
Local Notation gTg := {group gT}.

Implicit Type G : gTg.
Implicit Type s : seq gTg.

Local Notation compo := [rel x y : {set gT} | maxnormal y x x].

Definition comps G s := ((last G s) == 1%G) && compo.-series G s.

Lemma compsP : forall G s, reflect
  (last G s = 1%G /\ path [rel x y : gTg | maxnormal y x x] G s) (comps G s).

Lemma trivg_comps : forall G s, comps G s -> (G :==: 1) = (s == [::]).

Lemma comps_cons : forall G H s, comps G (H :: s) -> comps H s.

Lemma simple_compsP : forall G s, comps G s ->
  reflect (s = [:: (1%G : gTg) ]) (simple G).

Lemma exists_comps : forall G : gTg, exists s, comps G s.

 The factors associated to two composition series of the same group are     
 the same up to isomorphism and permutation                                 

Lemma JordanHolderUniqueness : forall (G : gTg) (s1 s2 : seq gTg),
  comps G s1 -> comps G s2 -> perm_eq (mkfactors G s1) (mkfactors G s2).

End CompositionSeries.

 Helper lemmas for group actions.                                           

Section MoreGroupAction.

Variables (aT rT : finGroupType).
Variables (A : {group aT})(D : {group rT}).
Variable to : groupAction A D.

Lemma gactsP : forall G : {set rT},
  reflect {acts A, on G | to} [acts A, on G | to].

Lemma gactsM : forall N1 N2 : {set rT},
  N1 \subset D -> N2 \subset D ->
  [acts A, on N1 | to] -> [acts A, on N2 | to] -> [acts A, on N1 * N2 | to].

Lemma gactsI : forall N1 N2 : {set rT},
  [acts A, on N1 | to] -> [acts A, on N2 | to] -> [acts A, on N1 :&: N2 | to].

Lemma gastabsP : forall (S : {set rT}) (a : aT), a \in A ->
       reflect (forall x : rT, (to x a \in S) = (x \in S)) (a \in 'N(S | to)).

End MoreGroupAction.

 Helper lemmas for quotient actions.                                        

Section MoreQuotientAction.

Variables (aT rT : finGroupType).
Variables (A : {group aT})(D : {group rT}).
Variable to : groupAction A D.

Lemma qact_dom_doms : forall H : {group rT},
  H \subset D -> qact_dom to H \subset A.

Lemma acts_qact_doms : forall H : {group rT}, H \subset D ->
  [acts A, on H | to] -> qact_dom to H :=: A.

Lemma qacts_cosetpre : forall (H : {group rT})(K' : {group coset_groupType H}),
  H \subset D -> [acts A, on H | to] -> [acts qact_dom to H, on K' | to / H] ->
  [acts A, on (coset H @*^-1 K') | to].

Lemma qacts_coset : forall (H K : {group rT}),
 H \subset D -> [acts A, on K | to] ->
 [acts qact_dom to H, on (coset H) @* K | to / H].

End MoreQuotientAction.

Section StableCompositionSeries.

Variables (aT rT : finGroupType).
Variables (D : {group rT})(A : {group aT}).
Variable to : groupAction A D.

Definition maxainv (B C : {set rT}) :=
  [max C of H |
    [&& (H <| B), ~~ (B \subset H) & [acts A, on H | to]]].

Section MaxAinvProps.

Variables K N : {group rT}.

Lemma maxainv_norm : maxainv K N -> N <| K.

Lemma maxainv_proper : maxainv K N -> N \proper K.

Lemma maxainv_sub : maxainv K N -> N \subset K.

Lemma maxainv_ainvar : maxainv K N -> A \subset 'N(N | to).

Lemma maxainvS : maxainv K N -> N \subset K.

Lemma maxainv_exists : K :!=: 1 -> {N : {group rT} | maxainv K N}.

End MaxAinvProps.

Lemma maxainvM : forall G H K : {group rT},
  H \subset D -> K \subset D -> maxainv G H -> maxainv G K ->
  H :<>: K -> H * K = G.

Definition asimple (K : {set rT}) := maxainv K 1.

Lemma asimpleP : forall K : {group rT},
  reflect (K :!=: 1 /\ (forall H : {group rT},
    H <| K -> [acts A, on H | to] -> H :=: 1 \/ H :=: K))
  (asimple K).

Implicit Type K : {group rT}.
Implicit Type s : seq {group rT}.

Definition acomps K s :=
  ((last K s) == 1%G) &&
  path [rel x y : {group rT} | maxainv x y] K s.

Lemma acompsP : forall K s, reflect
  (last K s = 1%G /\ path [rel x y : {group rT} | maxainv x y] K s) (acomps K s).

Lemma trivg_acomps : forall K s, acomps K s -> (K :==: 1) = (s == [::]).

Lemma acomps_cons : forall K H s, acomps K (H :: s) -> acomps H s.

Lemma asimple_acompsP : forall K s,
  acomps K s -> reflect (s = [:: 1%G]) (asimple K).

Lemma exists_acomps : forall K : {group rT}, exists s, acomps K s.

End StableCompositionSeries.

Section StrongJordanHolder.

Section AuxiliaryLemmas.

Variables (aT rT : finGroupType).
Variables (A : {group aT})(D : {group rT}).
Variable to : groupAction A D.

Lemma maxainv_asimple_quo : forall G H : {group rT},
   H \subset D -> maxainv to G H -> asimple (to / H) (G / H).

Lemma asimple_quo_maxainv : forall G H : {group rT},
  H \subset D -> G \subset D -> [acts A, on G | to] -> [acts A, on H | to] ->
  H <| G -> asimple (to / H) (G / H) ->
    maxainv to G H.

Lemma asimpleI : forall N1 N2: {group rT},
  N2 \subset 'N(N1) -> N1 \subset D ->
  [acts A, on N1 | to] -> [acts A, on N2 | to] ->
  asimple (to / N1) (N2 / N1) -> asimple (to / (N2 :&: N1)) (N2 / (N2 :&: N1)).

End AuxiliaryLemmas.

Variables (aT rT : finGroupType).
Variables (A : {group aT})(D : {group rT}).
Variable to : groupAction A D.

 The factors associated to two A-stable composition series of the same      
 group are the same up to isomorphism and permutation                       

Lemma StrongJordanHolderUniqueness :
  forall (G : {group rT}) (s1 s2 : seq {group rT}),
  G \subset D -> acomps to G s1 -> acomps to G s2 ->
  perm_eq (mkfactors G s1) (mkfactors G s2).

End StrongJordanHolder.