- -

Library mathcomp.solvable.jordanholder

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- This files establishes Jordan-Holder 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 - 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. - -

- See also "The Rooster and the Butterflies", proceedings of Calculemus 2013, - by Assia Mahboubi. -

- -
-Import GroupScope.
- -
-Set Implicit Arguments.
- -
-Inductive section (gT : finGroupType) := GSection of {group gT } × {group gT }.
- -
-Delimit Scope section_scope with sec.
- -
-Definition mkSec (gT : finGroupType) (G1 G2 : {group gT }) := GSection (G1 , G2 ).
- -
-Infix "/" := mkSec : section_scope.
- -
-Coercion pair_of_section gT (s : section gT) := let: GSection 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 }) (s : section gT).
- -
-Canonical section_subType := Eval hnf in [newType for @pair_of_section gT ].
-Definition section_eqMixin := Eval hnf in [eqMixin of section gT by <:].
-Canonical section_eqType := Eval hnf in EqType (section gT) section_eqMixin.
-Definition section_choiceMixin := [choiceMixin of section gT by <:].
-Canonical section_choiceType :=
-  Eval hnf in ChoiceType (section gT) section_choiceMixin.
-Definition section_countMixin := [countMixin of section gT by <:].
-Canonical section_countType :=
-  Eval hnf in CountType (section gT) section_countMixin.
-Canonical section_subCountType := Eval hnf in [subCountType of section gT ].
-Definition section_finMixin := [finMixin of section gT by <:].
-Canonical section_finType := Eval hnf in FinType (section gT) section_finMixin.
-Canonical section_subFinType := Eval hnf in [subFinType of section gT ].
-Canonical 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 := odflt (1 / 1)%sec (pick (section_isog ^~ s)).
- -
-Definition mksrepr G1 G2 := section_repr (mkSec G1 G2).
- -
-Lemma section_reprP s : section_repr s \isog s.
- -
-Lemma section_repr_isog 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.
- -
-Variable gT : finGroupType.
-Implicit Types (G : gTg) (s : seq gTg).
- -
- -
-Definition comps G s := ((last G s ) == 1%G) && compo .-series G s.
- -
-Lemma compsP 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 G s : comps G s → (G :==: 1) = (s == [::]).
- -
-Lemma comps_cons G H s : comps G (H :: s) → comps H s.
- -
-Lemma simple_compsP G s : comps G s → reflect (s = [:: 1%G]) (simple G).
- -
-Lemma exists_comps (G : gTg) : ∃ 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 (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 (G : {set rT }) : reflect {acts A , on G | to } [acts A , on G | to ].
- -
-Lemma gactsM (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 (N1 N2 : {set rT }) :
-  [acts A , on N1 | to ] → [acts A , on N2 | to ] → [acts A , on N1 :&: N2 | to ].
- -
-Lemma gastabsP (S : {set rT }) (a : aT) :
-  a \in A → reflect (∀ x, (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 (H : {group rT }) : H \subset D → qact_dom to H \subset A.
- -
-Lemma acts_qact_doms (H : {group rT }) :
-  H \subset D → [acts A , on H | to ] → qact_dom to H :=: A.
- -
-Lemma qacts_cosetpre (H : {group rT }) (K' : {group coset_of 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 (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 (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.
- -
-Implicit Types (H K : {group rT }) (s : seq {group rT }).
- -
-Lemma asimpleP K :
-  reflect [/\ K :!=: 1
-            & ∀ H, H <| K → [acts A , on H | to ] → H :=: 1 ∨ H :=: K ]
-          (asimple K).
- -
-Definition acomps K s :=
-  ((last K s ) == 1%G) && path [rel x y : {group rT } | maxainv x y ] K s.
- -
-Lemma acompsP 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 K s : acomps K s → (K :==: 1) = (s == [::]).
- -
-Lemma acomps_cons K H s : acomps K (H :: s) → acomps H s.
- -
-Lemma asimple_acompsP K s : acomps K s → reflect (s = [:: 1%G]) (asimple K).
- -
-Lemma exists_acomps K : ∃ s, acomps K s.
- -
-End StableCompositionSeries.
- -
- -
-Section StrongJordanHolder.
- -
-Section AuxiliaryLemmas.
- -
-Variables aT rT : finGroupType.
-Variables (A : {group aT }) (D : {group rT }) (to : groupAction A D).
- -
-Lemma maxainv_asimple_quo (G H : {group rT }) :
-   H \subset D → maxainv to G H → asimple (to / H) (G / H).
- -
-Lemma asimple_quo_maxainv (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 (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 }) (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 (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.
- -
-