Library mathcomp.solvable.jordanholder
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ 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. + + +
+
+
+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.
+ +
+
+
++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
+
+
+
+
+ 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.
+ +
+
+
++ +
+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.
+ +
+
+
++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.
+ +
+
+
++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).
+ +
+
+
++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
+
+
+