Library mathcomp.solvable.jordanholder
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
From mathcomp Require Import choice fintype bigop finset fingroup morphism.
From mathcomp Require Import automorphism quotient action gseries.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
From mathcomp Require Import choice fintype bigop finset fingroup morphism.
From mathcomp Require Import automorphism quotient action gseries.
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.
Set Implicit Arguments.
Import GroupScope.
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.
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