- -

Library mathcomp.fingroup.quotient

- -

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

- -

- This file contains the definitions of: - coset_of H == the (sub)type of bilateral cosets of H (see below). - coset H == the canonical projection into coset_of H. - A / H == the quotient of A by H, that is, the morphic image - of A by coset H. We do not require H <| A, so in a - textbook A / H would be written 'N_A(H) * H / H. - quotm f (nHG : H <| G) == the quotient morphism induced by f, - mapping G / H onto f @* G / f @* H. - qisom f (eqHG : H = G) == the identity isomorphism between - [set: coset_of G] and [set: coset_of H]. - We also prove the three isomorphism theorems, and counting lemmas for - morphisms. -

- -
-Set Implicit Arguments.
- -
-Import GroupScope.
- -
-Section Cosets.
- -
-Variables (gT : finGroupType) (Q A : {set gT }).
- -
-

- -

- Cosets are right cosets of elements in the normaliser. - We let cosets coerce to GroupSet.sort, so they inherit the group subset - base group structure. Later we will define a proper group structure on - cosets, which will then hide the inherited structure once coset_of unifies - with FinGroup.sort; the coercion to GroupSet.sort will no longer be used. - Note that for Hx Hy : coset_of H, Hx * Hy : {set gT} can mean either - set_of_coset (mulg Hx Hy) OR mulg (set_of_coset Hx) (set_of_coset Hy). - However, since the two terms are actually convertible, we can live with - this ambiguity. - We take great care that neither the type coset_of H, nor its Canonical - finGroupType structure, nor the coset H morphism depend on the actual - group structure of H. Otherwise, rewriting would be extremely awkward - because all our equalities are stated at the set level. - The trick we use is to interpret coset_of A, when A is any set, as the - type of cosets of the group A generated by A, in the group A <*> N(A) - generated by A and its normaliser. This coincides with the type of - bilateral cosets of A when A is a group. We restrict the domain of coset A - to 'N(A), so that we get almost all the same conversion equalities as if - we had forced A to be a group in the first place; the only exception, that - 1 : coset_of A : {set gT} = A rather than A, can be handled by genGid. -

- -
-Notation H := <<A >>.
-Definition coset_range := [pred B in rcosets H 'N (A )].
- -
-Record coset_of : Type :=
- Coset { set_of_coset :> GroupSet.sort gT; _ : coset_range set_of_coset }.
- -
-Canonical coset_subType := Eval hnf in [subType for set_of_coset ].
-Definition coset_eqMixin := Eval hnf in [eqMixin of coset_of by <:].
-Canonical coset_eqType := Eval hnf in EqType coset_of coset_eqMixin.
-Definition coset_choiceMixin := [choiceMixin of coset_of by <:].
-Canonical coset_choiceType := Eval hnf in ChoiceType coset_of coset_choiceMixin.
-Definition coset_countMixin := [countMixin of coset_of by <:].
-Canonical coset_countType := Eval hnf in CountType coset_of coset_countMixin.
-Canonical coset_subCountType := Eval hnf in [subCountType of coset_of ].
-Definition coset_finMixin := [finMixin of coset_of by <:].
-Canonical coset_finType := Eval hnf in FinType coset_of coset_finMixin.
-Canonical coset_subFinType := Eval hnf in [subFinType of coset_of ].
- -
-

- -

- We build a new (canonical) structure of groupType for cosets. - When A is a group, this is the largest possible quotient 'N(A) / A. -

- -
-Lemma coset_one_proof : coset_range H.
- Definition coset_one := Coset coset_one_proof.
- -
-Let nNH := subsetP (norm_gen A).
- -
-Lemma coset_range_mul (B C : coset_of) : coset_range (B × C).
- -
-Definition coset_mul B C := Coset (coset_range_mul B C).
- -
-Lemma coset_range_inv (B : coset_of) : coset_range B ^-1.
- -
-Definition coset_inv B := Coset (coset_range_inv B).
- -
-Lemma coset_mulP : associative coset_mul.
- -
-Lemma coset_oneP : left_id coset_one coset_mul.
- -
-Lemma coset_invP : left_inverse coset_one coset_inv coset_mul.
- -
-Definition coset_of_groupMixin :=
- FinGroup.Mixin coset_mulP coset_oneP coset_invP.
- -
-Canonical coset_baseGroupType :=
- Eval hnf in BaseFinGroupType coset_of coset_of_groupMixin.
-Canonical coset_groupType := FinGroupType coset_invP.
- -
-

- -

- Projection of the initial group type over the cosets groupType. -

- -
-Definition coset x : coset_of := insubd (1 : coset_of) (H :* x).
- -
-

- -

- This is a primitive lemma -- we'll need to restate it for - the case where A is a group. -

-Lemma val_coset_prim x : x \in 'N (A ) → coset x :=: H :* x.
- -
-Lemma coset_morphM : {in 'N (A ) &, {morph coset : x y / x × y }}.
- -
-Canonical coset_morphism := Morphism coset_morphM.
- -
-Lemma ker_coset_prim : 'ker coset = 'N_H (A ).
- -
-Implicit Type xbar : coset_of.
- -
-Lemma coset_mem y xbar : y \in xbar → coset y = xbar.
- -
-

- -

- coset is an inverse to repr -

- -
-Lemma mem_repr_coset xbar : repr xbar \in xbar.
- -
-Lemma repr_coset1 : repr (1 : coset_of) = 1.
- -
-Lemma coset_reprK : cancel (fun xbar ⇒ repr xbar) coset.
- -
-

- -

- cosetP is slightly stronger than using repr because we only - guarantee repr xbar \in 'N(A) when A is a group. -

-Lemma cosetP xbar : {x | x \in 'N (A ) & xbar = coset x }.
- -
-Lemma coset_id x : x \in A → coset x = 1.
- -
-Lemma im_coset : coset @* 'N (A ) = setT.
- -
-Lemma sub_im_coset (C : {set coset_of }) : C \subset coset @* 'N (A ).
- -
-Lemma cosetpre_proper C D :
- (coset @*^-1 C \proper coset @*^-1 D ) = (C \proper D ).
- -
-Definition quotient : {set coset_of } := coset @* Q.
- -
-Lemma quotientE : quotient = coset @* Q.
- -
-End Cosets.
- -
- -
- -
-Notation "A / H" := (quotient A H) : group_scope.
- -
-Section CosetOfGroupTheory.
- -
-Variables (gT : finGroupType) (H : {group gT }).
-Implicit Types (A B : {set gT }) (G K : {group gT }) (xbar yb : coset_of H).
-Implicit Types (C D : {set coset_of H }) (L M : {group coset_of H }).
- -
-Canonical quotient_group G A : {group coset_of A } :=
- Eval hnf in [group of G / A ].
- -
-Infix "/" := quotient_group : Group_scope.
- -
-Lemma val_coset x : x \in 'N (H ) → coset H x :=: H :* x.
- -
-Lemma coset_default x : (x \in 'N (H )) = false → coset H x = 1.
- -
-Lemma coset_norm xbar : xbar \subset 'N (H ).
- -
-Lemma ker_coset : 'ker (coset H ) = H.
- -
-Lemma coset_idr x : x \in 'N (H ) → coset H x = 1 → x \in H.
- -
-Lemma repr_coset_norm xbar : repr xbar \in 'N (H ).
- -
-Lemma imset_coset G : coset H @: G = G / H.
- -
-Lemma val_quotient A : val @: (A / H ) = rcosets H 'N_A (H ).
- -
-Lemma card_quotient_subnorm A : #|A / H | = #|'N_A (H ) : H |.
- -
-Lemma leq_quotient A : #|A / H | ≤ #|A |.
- -
-Lemma ltn_quotient A : H :!=: 1 → H \subset A → #|A / H | < #|A |.
- -
-Lemma card_quotient A : A \subset 'N (H ) → #|A / H | = #|A : H |.
- -
-Lemma divg_normal G : H <| G → #|G | %/ #|H | = #|G / H |.
- -
-

- -

- Specializing all the morphisms lemmas that have different assumptions - (e.g., because 'ker (coset H) = H), or conclusions (e.g., because we use - A / H rather than coset H @* A). We may want to reevaluate later, and - eliminate variants that aren't used . -

- - Variant of morph1; no specialization for other morph lemmas. -

-Lemma coset1 : coset H 1 :=: H.
- -
-

- -

- Variant of kerE. -

-Lemma cosetpre1 : coset H @*^-1 1 = H.
- -
-

- -

- Variant of morphimEdom; mophimE[sub] covered by imset_coset. - morph[im|pre]Iim are also covered by im_quotient. -

-Lemma im_quotient : 'N (H ) / H = setT.
- -
-Lemma quotientT : setT / H = setT.
- -
-

- -

- Variant of morphimIdom. -

- -

- Variant of morhphim_ker -

-Lemma trivg_quotient : H / H = 1.
- -
-Lemma quotientS1 G : G \subset H → G / H = 1.
- -
-Lemma sub_cosetpre M : H \subset coset H @*^-1 M.
- -
-Lemma quotient_proper G K :
-  H <| G → H <| K → (G / H \proper K / H ) = (G \proper K ).
- -
-Lemma normal_cosetpre M : H <| coset H @*^-1 M.
- -
-Lemma cosetpreSK C D :
-  (coset H @*^-1 C \subset coset H @*^-1 D ) = (C \subset D ).
- -
-Lemma sub_quotient_pre A C :
-  A \subset 'N (H ) → (A / H \subset C ) = (A \subset coset H @*^-1 C ).
- -
-Lemma sub_cosetpre_quo C G :
-  H <| G → (coset H @*^-1 C \subset G ) = (C \subset G / H ).
- -
-

- -

- Variant of ker_trivg_morphim. -

- -

- Counting lemmas for morphisms. -

- -
-Section CardMorphism.
- -
-Variables (aT rT : finGroupType) (D : {group aT }) (f : {morphism D >-> rT }).
-Implicit Types G H : {group aT }.
-Implicit Types L M : {group rT }.
- -
-Lemma card_morphim G : #|f @* G | = #|D :&: G : 'ker f |.
- -
-Lemma dvdn_morphim G : #|f @* G | %| #|G |.
- -
-Lemma logn_morphim p G : logn p #|f @* G | ≤ logn p #|G |.
- -
-Lemma coprime_morphl G p : coprime #|G | p → coprime #|f @* G | p.
- -
-Lemma coprime_morphr G p : coprime p #|G | → coprime p #|f @* G |.
- -
-Lemma coprime_morph G H : coprime #|G | #|H | → coprime #|f @* G | #|f @* H |.
- -
-Lemma index_morphim_ker G H :
-    H \subset G → G \subset D →
-  (#|f @* G : f @* H | × #|'ker_G f : H |)%N = #|G : H |.
- -
-Lemma index_morphim G H : G :&: H \subset D → #|f @* G : f @* H | %| #|G : H |.
- -
-Lemma index_injm G H : 'injm f → G \subset D → #|f @* G : f @* H | = #|G : H |.
- -
-Lemma card_morphpre L : L \subset f @* D → #|f @*^-1 L | = (#|'ker f | × #|L |)%N.
- -
-Lemma index_morphpre L M :
-  L \subset f @* D → #|f @*^-1 L : f @*^-1 M | = #|L : M |.
- -
-End CardMorphism.
- -
-Lemma card_homg (aT rT : finGroupType) (G : {group aT }) (R : {group rT }) :
-  G \homg R → #|G | %| #|R |.
- -
-Section CardCosetpre.
- -
-Variables (gT : finGroupType) (G H K : {group gT }) (L M : {group coset_of H }).
- -
-Lemma dvdn_quotient : #|G / H | %| #|G |.
- -
-Lemma index_quotient_ker :
-     K \subset G → G \subset 'N (H ) →
-  (#|G / H : K / H | × #|G :&: H : K |)%N = #|G : K |.
- -
-Lemma index_quotient : G :&: K \subset 'N (H ) → #|G / H : K / H | %| #|G : K |.
- -
-Lemma index_quotient_eq :
-    G :&: H \subset K → K \subset G → G \subset 'N (H ) →
-  #|G / H : K / H | = #|G : K |.
- -
-Lemma card_cosetpre : #|coset H @*^-1 L | = (#|H | × #|L |)%N.
- -
-Lemma index_cosetpre : #|coset H @*^-1 L : coset H @*^-1 M | = #|L : M |.
- -
-End CardCosetpre.
-