Library mathcomp.fingroup.quotient
+ +
+(* (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 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}).
+ +
+
+
++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].
+ +
+
+
++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.
+ +
+
+
++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.
+
+
+
+
+ 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.
+ +
+
+
++ +
+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.
+ +
+
+
++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 / B" := (quotient A B) : 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|.
+ +
+
+
++ +
+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 / B" := (quotient A B) : 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.
+
+
+
+
+ Variant of kerE.
+
+
+
+
+ Variant of morphimEdom; mophimE[sub] covered by imset_coset.
+ morph[im|pre]Iim are also covered by im_quotient.
+
+
+
+
+ Variant of morphimIdom.
+
+
+Lemma quotientInorm A : 'N_A(H) / H = A / H.
+ +
+Lemma quotient_setIpre A D : (A :&: coset H @*^-1 D) / H = A / H :&: D.
+ +
+Lemma mem_quotient x G : x \in G → coset H x \in G / H.
+ +
+Lemma quotientS A B : A \subset B → A / H \subset B / H.
+ +
+Lemma quotient0 : set0 / H = set0.
+ +
+Lemma quotient_set1 x : x \in 'N(H) → [set x] / H = [set coset H x].
+ +
+Lemma quotient1 : 1 / H = 1.
+ +
+Lemma quotientV A : A^-1 / H = (A / H)^-1.
+ +
+Lemma quotientMl A B : A \subset 'N(H) → A × B / H = (A / H) × (B / H).
+ +
+Lemma quotientMr A B : B \subset 'N(H) → A × B / H = (A / H) × (B / H).
+ +
+Lemma cosetpreM C D : coset H @*^-1 (C × D) = coset H @*^-1 C × coset H @*^-1 D.
+ +
+Lemma quotientJ A x : x \in 'N(H) → A :^ x / H = (A / H) :^ coset H x.
+ +
+Lemma quotientU A B : (A :|: B) / H = A / H :|: B / H.
+ +
+Lemma quotientI A B : (A :&: B) / H \subset A / H :&: B / H.
+ +
+Lemma quotientY A B :
+ A \subset 'N(H) → B \subset 'N(H) → (A <*> B) / H = (A / H) <*> (B / H).
+ +
+Lemma quotient_homg A : A \subset 'N(H) → homg (A / H) A.
+ +
+Lemma coset_kerl x y : x \in H → coset H (x × y) = coset H y.
+ +
+Lemma coset_kerr x y : y \in H → coset H (x × y) = coset H x.
+ +
+Lemma rcoset_kercosetP x y :
+ x \in 'N(H) → y \in 'N(H) → reflect (coset H x = coset H y) (x \in H :* y).
+ +
+Lemma kercoset_rcoset x y :
+ x \in 'N(H) → y \in 'N(H) →
+ coset H x = coset H y → exists2 z, z \in H & x = z × y.
+ +
+Lemma quotientGI G A : H \subset G → (G :&: A) / H = G / H :&: A / H.
+ +
+Lemma quotientIG A G : H \subset G → (A :&: G) / H = A / H :&: G / H.
+ +
+Lemma quotientD A B : A / H :\: B / H \subset (A :\: B) / H.
+ +
+Lemma quotientD1 A : (A / H)^# \subset A^# / H.
+ +
+Lemma quotientDG A G : H \subset G → (A :\: G) / H = A / H :\: G / H.
+ +
+Lemma quotientK A : A \subset 'N(H) → coset H @*^-1 (A / H) = H × A.
+ +
+Lemma quotientYK G : G \subset 'N(H) → coset H @*^-1 (G / H) = H <*> G.
+ +
+Lemma quotientGK G : H <| G → coset H @*^-1 (G / H) = G.
+ +
+Lemma quotient_class x A :
+ x \in 'N(H) → A \subset 'N(H) → x ^: A / H = coset H x ^: (A / H).
+ +
+Lemma classes_quotient A :
+ A \subset 'N(H) → classes (A / H) = [set xA / H | xA in classes A].
+ +
+Lemma cosetpre_set1 x :
+ x \in 'N(H) → coset H @*^-1 [set coset H x] = H :* x.
+ +
+Lemma cosetpre_set1_coset xbar : coset H @*^-1 [set xbar] = xbar.
+ +
+Lemma cosetpreK C : coset H @*^-1 C / H = C.
+ +
+
+
++ +
+Lemma quotient_setIpre A D : (A :&: coset H @*^-1 D) / H = A / H :&: D.
+ +
+Lemma mem_quotient x G : x \in G → coset H x \in G / H.
+ +
+Lemma quotientS A B : A \subset B → A / H \subset B / H.
+ +
+Lemma quotient0 : set0 / H = set0.
+ +
+Lemma quotient_set1 x : x \in 'N(H) → [set x] / H = [set coset H x].
+ +
+Lemma quotient1 : 1 / H = 1.
+ +
+Lemma quotientV A : A^-1 / H = (A / H)^-1.
+ +
+Lemma quotientMl A B : A \subset 'N(H) → A × B / H = (A / H) × (B / H).
+ +
+Lemma quotientMr A B : B \subset 'N(H) → A × B / H = (A / H) × (B / H).
+ +
+Lemma cosetpreM C D : coset H @*^-1 (C × D) = coset H @*^-1 C × coset H @*^-1 D.
+ +
+Lemma quotientJ A x : x \in 'N(H) → A :^ x / H = (A / H) :^ coset H x.
+ +
+Lemma quotientU A B : (A :|: B) / H = A / H :|: B / H.
+ +
+Lemma quotientI A B : (A :&: B) / H \subset A / H :&: B / H.
+ +
+Lemma quotientY A B :
+ A \subset 'N(H) → B \subset 'N(H) → (A <*> B) / H = (A / H) <*> (B / H).
+ +
+Lemma quotient_homg A : A \subset 'N(H) → homg (A / H) A.
+ +
+Lemma coset_kerl x y : x \in H → coset H (x × y) = coset H y.
+ +
+Lemma coset_kerr x y : y \in H → coset H (x × y) = coset H x.
+ +
+Lemma rcoset_kercosetP x y :
+ x \in 'N(H) → y \in 'N(H) → reflect (coset H x = coset H y) (x \in H :* y).
+ +
+Lemma kercoset_rcoset x y :
+ x \in 'N(H) → y \in 'N(H) →
+ coset H x = coset H y → exists2 z, z \in H & x = z × y.
+ +
+Lemma quotientGI G A : H \subset G → (G :&: A) / H = G / H :&: A / H.
+ +
+Lemma quotientIG A G : H \subset G → (A :&: G) / H = A / H :&: G / H.
+ +
+Lemma quotientD A B : A / H :\: B / H \subset (A :\: B) / H.
+ +
+Lemma quotientD1 A : (A / H)^# \subset A^# / H.
+ +
+Lemma quotientDG A G : H \subset G → (A :\: G) / H = A / H :\: G / H.
+ +
+Lemma quotientK A : A \subset 'N(H) → coset H @*^-1 (A / H) = H × A.
+ +
+Lemma quotientYK G : G \subset 'N(H) → coset H @*^-1 (G / H) = H <*> G.
+ +
+Lemma quotientGK G : H <| G → coset H @*^-1 (G / H) = G.
+ +
+Lemma quotient_class x A :
+ x \in 'N(H) → A \subset 'N(H) → x ^: A / H = coset H x ^: (A / H).
+ +
+Lemma classes_quotient A :
+ A \subset 'N(H) → classes (A / H) = [set xA / H | xA in classes A].
+ +
+Lemma cosetpre_set1 x :
+ x \in 'N(H) → coset H @*^-1 [set coset H x] = H :* x.
+ +
+Lemma cosetpre_set1_coset xbar : coset H @*^-1 [set xbar] = xbar.
+ +
+Lemma cosetpreK C : coset H @*^-1 C / H = C.
+ +
+
+ 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).
+ +
+
+
++ +
+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.
+
+
+Lemma quotient_sub1 A : A \subset 'N(H) → (A / H \subset [1]) = (A \subset H).
+ +
+Lemma quotientSK A B :
+ A \subset 'N(H) → (A / H \subset B / H) = (A \subset H × B).
+ +
+Lemma quotientSGK A G :
+ A \subset 'N(H) → H \subset G → (A / H \subset G / H) = (A \subset G).
+ +
+Lemma quotient_injG :
+ {in [pred G : {group gT} | H <| G] &, injective (fun G ⇒ G / H)}.
+ +
+Lemma quotient_inj G1 G2 :
+ H <| G1 → H <| G2 → G1 / H = G2 / H → G1 :=: G2.
+ +
+Lemma quotient_neq1 A : H <| A → (A / H != 1) = (H \proper A).
+ +
+Lemma quotient_gen A : A \subset 'N(H) → <<A>> / H = <<A / H>>.
+ +
+Lemma cosetpre_gen C :
+ 1 \in C → coset H @*^-1 <<C>> = <<coset H @*^-1 C>>.
+ +
+Lemma quotientR A B :
+ A \subset 'N(H) → B \subset 'N(H) → [~: A, B] / H = [~: A / H, B / H].
+ +
+Lemma quotient_norm A : 'N(A) / H \subset 'N(A / H).
+ +
+Lemma quotient_norms A B : A \subset 'N(B) → A / H \subset 'N(B / H).
+ +
+Lemma quotient_subnorm A B : 'N_A(B) / H \subset 'N_(A / H)(B / H).
+ +
+Lemma quotient_normal A B : A <| B → A / H <| B / H.
+ +
+Lemma quotient_cent1 x : 'C[x] / H \subset 'C[coset H x].
+ +
+Lemma quotient_cent1s A x : A \subset 'C[x] → A / H \subset 'C[coset H x].
+ +
+Lemma quotient_subcent1 A x : 'C_A[x] / H \subset 'C_(A / H)[coset H x].
+ +
+Lemma quotient_cent A : 'C(A) / H \subset 'C(A / H).
+ +
+Lemma quotient_cents A B : A \subset 'C(B) → A / H \subset 'C(B / H).
+ +
+Lemma quotient_abelian A : abelian A → abelian (A / H).
+ +
+Lemma quotient_subcent A B : 'C_A(B) / H \subset 'C_(A / H)(B / H).
+ +
+Lemma norm_quotient_pre A C :
+ A \subset 'N(H) → A / H \subset 'N(C) → A \subset 'N(coset H @*^-1 C).
+ +
+Lemma cosetpre_normal C D : (coset H @*^-1 C <| coset H @*^-1 D) = (C <| D).
+ +
+Lemma quotient_normG G : H <| G → 'N(G) / H = 'N(G / H).
+ +
+Lemma quotient_subnormG A G : H <| G → 'N_A(G) / H = 'N_(A / H)(G / H).
+ +
+Lemma cosetpre_cent1 x : 'C_('N(H))[x] \subset coset H @*^-1 'C[coset H x].
+ +
+Lemma cosetpre_cent1s C x :
+ coset H @*^-1 C \subset 'C[x] → C \subset 'C[coset H x].
+ +
+Lemma cosetpre_subcent1 C x :
+ 'C_(coset H @*^-1 C)[x] \subset coset H @*^-1 'C_C[coset H x].
+ +
+Lemma cosetpre_cent A : 'C_('N(H))(A) \subset coset H @*^-1 'C(A / H).
+ +
+Lemma cosetpre_cents A C : coset H @*^-1 C \subset 'C(A) → C \subset 'C(A / H).
+ +
+Lemma cosetpre_subcent C A :
+ 'C_(coset H @*^-1 C)(A) \subset coset H @*^-1 'C_C(A / H).
+ +
+Lemma restrm_quotientE G A (nHG : G \subset 'N(H)) :
+ A \subset G → restrm nHG (coset H) @* A = A / H.
+ +
+Section InverseImage.
+ +
+Variables (G : {group gT}) (Kbar : {group coset_of H}).
+ +
+Hypothesis nHG : H <| G.
+ +
+CoInductive inv_quotient_spec (P : pred {group gT}) : Prop :=
+ InvQuotientSpec K of Kbar :=: K / H & H \subset K & P K.
+ +
+Lemma inv_quotientS :
+ Kbar \subset G / H → inv_quotient_spec (fun K ⇒ K \subset G).
+ +
+Lemma inv_quotientN : Kbar <| G / H → inv_quotient_spec (fun K ⇒ K <| G).
+ +
+End InverseImage.
+ +
+Lemma quotientMidr A : A × H / H = A / H.
+ +
+Lemma quotientMidl A : H × A / H = A / H.
+ +
+Lemma quotientYidr G : G \subset 'N(H) → G <*> H / H = G / H.
+ +
+Lemma quotientYidl G : G \subset 'N(H) → H <*> G / H = G / H.
+ +
+Section Injective.
+ +
+Variables (G : {group gT}).
+Hypotheses (nHG : G \subset 'N(H)) (tiHG : H :&: G = 1).
+ +
+Lemma quotient_isom : isom G (G / H) (restrm nHG (coset H)).
+ +
+Lemma quotient_isog : isog G (G / H).
+ +
+End Injective.
+ +
+End CosetOfGroupTheory.
+ +
+Notation "A / H" := (quotient_group A H) : Group_scope.
+ +
+Section Quotient1.
+ +
+Variables (gT : finGroupType) (A : {set gT}).
+ +
+Lemma coset1_injm : 'injm (@coset gT 1).
+ +
+Lemma quotient1_isom : isom A (A / 1) (coset 1).
+ +
+Lemma quotient1_isog : isog A (A / 1).
+ +
+End Quotient1.
+ +
+Section QuotientMorphism.
+ +
+Variable (gT rT : finGroupType) (G H : {group gT}) (f : {morphism G >-> rT}).
+ +
+Implicit Types A : {set gT}.
+Implicit Types B : {set (coset_of H)}.
+Hypotheses (nsHG : H <| G).
+Let sHG : H \subset G := normal_sub nsHG.
+Let nHG : G \subset 'N(H) := normal_norm nsHG.
+Let nfHfG : f @* G \subset 'N(f @* H) := morphim_norms f nHG.
+ +
+Notation fH := (coset (f @* H) \o f).
+ +
+Lemma quotm_dom_proof : G \subset 'dom fH.
+ +
+Notation fH_G := (restrm quotm_dom_proof fH).
+ +
+Lemma quotm_ker_proof : 'ker (coset H) \subset 'ker fH_G.
+ +
+Definition quotm := factm quotm_ker_proof nHG.
+ +
+Canonical quotm_morphism := [morphism G / H of quotm].
+ +
+Lemma quotmE x : x \in G → quotm (coset H x) = coset (f @* H) (f x).
+ +
+Lemma morphim_quotm A : quotm @* (A / H) = f @* A / f @* H.
+ +
+Lemma morphpre_quotm Abar : quotm @*^-1 (Abar / f @* H) = f @*^-1 Abar / H.
+ +
+Lemma ker_quotm : 'ker quotm = 'ker f / H.
+ +
+Lemma injm_quotm : 'injm f → 'injm quotm.
+ +
+End QuotientMorphism.
+ +
+Section EqIso.
+ +
+Variables (gT : finGroupType) (G H : {group gT}).
+ +
+Hypothesis (eqGH : G :=: H).
+ +
+Lemma im_qisom_proof : 'N(H) \subset 'N(G).
+Lemma qisom_ker_proof : 'ker (coset G) \subset 'ker (coset H).
+ Lemma qisom_restr_proof : setT \subset 'N(H) / G.
+ +
+Definition qisom :=
+ restrm qisom_restr_proof (factm qisom_ker_proof im_qisom_proof).
+ +
+Canonical qisom_morphism := Eval hnf in [morphism of qisom].
+ +
+Lemma qisomE x : qisom (coset G x) = coset H x.
+ +
+Lemma val_qisom Gx : val (qisom Gx) = val Gx.
+ +
+Lemma morphim_qisom A : qisom @* (A / G) = A / H.
+ +
+Lemma morphpre_qisom A : qisom @*^-1 (A / H) = A / G.
+ +
+Lemma injm_qisom : 'injm qisom.
+ +
+Lemma im_qisom : qisom @* setT = setT.
+ +
+Lemma qisom_isom : isom setT setT qisom.
+ +
+Lemma qisom_isog : [set: coset_of G] \isog [set: coset_of H].
+ +
+Lemma qisom_inj : injective qisom.
+ +
+Lemma morphim_qisom_inj : injective (fun Gx ⇒ qisom @* Gx).
+ +
+End EqIso.
+ +
+ +
+Section FirstIsomorphism.
+ +
+Variables aT rT : finGroupType.
+ +
+Lemma first_isom (G : {group aT}) (f : {morphism G >-> rT}) :
+ {g : {morphism G / 'ker f >-> rT} | 'injm g &
+ ∀ A : {set aT}, g @* (A / 'ker f) = f @* A}.
+ +
+Variables (G H : {group aT}) (f : {morphism G >-> rT}).
+Hypothesis sHG : H \subset G.
+ +
+Lemma first_isog : (G / 'ker f) \isog (f @* G).
+ +
+Lemma first_isom_loc : {g : {morphism H / 'ker_H f >-> rT} |
+ 'injm g & ∀ A : {set aT}, A \subset H → g @* (A / 'ker_H f) = f @* A}.
+ +
+Lemma first_isog_loc : (H / 'ker_H f) \isog (f @* H).
+ +
+End FirstIsomorphism.
+ +
+Section SecondIsomorphism.
+ +
+Variables (gT : finGroupType) (H K : {group gT}).
+ +
+Hypothesis nKH : H \subset 'N(K).
+ +
+Lemma second_isom : {f : {morphism H / (K :&: H) >-> coset_of K} |
+ 'injm f & ∀ A : {set gT}, A \subset H → f @* (A / (K :&: H)) = A / K}.
+ +
+Lemma second_isog : H / (K :&: H) \isog H / K.
+ +
+Lemma weak_second_isog : H / (K :&: H) \isog H × K / K.
+ +
+End SecondIsomorphism.
+ +
+Section ThirdIsomorphism.
+ +
+Variables (gT : finGroupType) (G H K : {group gT}).
+ +
+Lemma homg_quotientS (A : {set gT}) :
+ A \subset 'N(H) → A \subset 'N(K) → H \subset K → A / K \homg A / H.
+ +
+Hypothesis sHK : H \subset K.
+Hypothesis snHG : H <| G.
+Hypothesis snKG : K <| G.
+ +
+Theorem third_isom : {f : {morphism (G / H) / (K / H) >-> coset_of K} | 'injm f
+ & ∀ A : {set gT}, A \subset G → f @* (A / H / (K / H)) = A / K}.
+ +
+Theorem third_isog : (G / H / (K / H)) \isog (G / K).
+ +
+End ThirdIsomorphism.
+ +
+Lemma char_from_quotient (gT : finGroupType) (G H K : {group gT}) :
+ H <| K → H \char G → K / H \char G / H → K \char G.
+ +
+
+
++ +
+Lemma quotientSK A B :
+ A \subset 'N(H) → (A / H \subset B / H) = (A \subset H × B).
+ +
+Lemma quotientSGK A G :
+ A \subset 'N(H) → H \subset G → (A / H \subset G / H) = (A \subset G).
+ +
+Lemma quotient_injG :
+ {in [pred G : {group gT} | H <| G] &, injective (fun G ⇒ G / H)}.
+ +
+Lemma quotient_inj G1 G2 :
+ H <| G1 → H <| G2 → G1 / H = G2 / H → G1 :=: G2.
+ +
+Lemma quotient_neq1 A : H <| A → (A / H != 1) = (H \proper A).
+ +
+Lemma quotient_gen A : A \subset 'N(H) → <<A>> / H = <<A / H>>.
+ +
+Lemma cosetpre_gen C :
+ 1 \in C → coset H @*^-1 <<C>> = <<coset H @*^-1 C>>.
+ +
+Lemma quotientR A B :
+ A \subset 'N(H) → B \subset 'N(H) → [~: A, B] / H = [~: A / H, B / H].
+ +
+Lemma quotient_norm A : 'N(A) / H \subset 'N(A / H).
+ +
+Lemma quotient_norms A B : A \subset 'N(B) → A / H \subset 'N(B / H).
+ +
+Lemma quotient_subnorm A B : 'N_A(B) / H \subset 'N_(A / H)(B / H).
+ +
+Lemma quotient_normal A B : A <| B → A / H <| B / H.
+ +
+Lemma quotient_cent1 x : 'C[x] / H \subset 'C[coset H x].
+ +
+Lemma quotient_cent1s A x : A \subset 'C[x] → A / H \subset 'C[coset H x].
+ +
+Lemma quotient_subcent1 A x : 'C_A[x] / H \subset 'C_(A / H)[coset H x].
+ +
+Lemma quotient_cent A : 'C(A) / H \subset 'C(A / H).
+ +
+Lemma quotient_cents A B : A \subset 'C(B) → A / H \subset 'C(B / H).
+ +
+Lemma quotient_abelian A : abelian A → abelian (A / H).
+ +
+Lemma quotient_subcent A B : 'C_A(B) / H \subset 'C_(A / H)(B / H).
+ +
+Lemma norm_quotient_pre A C :
+ A \subset 'N(H) → A / H \subset 'N(C) → A \subset 'N(coset H @*^-1 C).
+ +
+Lemma cosetpre_normal C D : (coset H @*^-1 C <| coset H @*^-1 D) = (C <| D).
+ +
+Lemma quotient_normG G : H <| G → 'N(G) / H = 'N(G / H).
+ +
+Lemma quotient_subnormG A G : H <| G → 'N_A(G) / H = 'N_(A / H)(G / H).
+ +
+Lemma cosetpre_cent1 x : 'C_('N(H))[x] \subset coset H @*^-1 'C[coset H x].
+ +
+Lemma cosetpre_cent1s C x :
+ coset H @*^-1 C \subset 'C[x] → C \subset 'C[coset H x].
+ +
+Lemma cosetpre_subcent1 C x :
+ 'C_(coset H @*^-1 C)[x] \subset coset H @*^-1 'C_C[coset H x].
+ +
+Lemma cosetpre_cent A : 'C_('N(H))(A) \subset coset H @*^-1 'C(A / H).
+ +
+Lemma cosetpre_cents A C : coset H @*^-1 C \subset 'C(A) → C \subset 'C(A / H).
+ +
+Lemma cosetpre_subcent C A :
+ 'C_(coset H @*^-1 C)(A) \subset coset H @*^-1 'C_C(A / H).
+ +
+Lemma restrm_quotientE G A (nHG : G \subset 'N(H)) :
+ A \subset G → restrm nHG (coset H) @* A = A / H.
+ +
+Section InverseImage.
+ +
+Variables (G : {group gT}) (Kbar : {group coset_of H}).
+ +
+Hypothesis nHG : H <| G.
+ +
+CoInductive inv_quotient_spec (P : pred {group gT}) : Prop :=
+ InvQuotientSpec K of Kbar :=: K / H & H \subset K & P K.
+ +
+Lemma inv_quotientS :
+ Kbar \subset G / H → inv_quotient_spec (fun K ⇒ K \subset G).
+ +
+Lemma inv_quotientN : Kbar <| G / H → inv_quotient_spec (fun K ⇒ K <| G).
+ +
+End InverseImage.
+ +
+Lemma quotientMidr A : A × H / H = A / H.
+ +
+Lemma quotientMidl A : H × A / H = A / H.
+ +
+Lemma quotientYidr G : G \subset 'N(H) → G <*> H / H = G / H.
+ +
+Lemma quotientYidl G : G \subset 'N(H) → H <*> G / H = G / H.
+ +
+Section Injective.
+ +
+Variables (G : {group gT}).
+Hypotheses (nHG : G \subset 'N(H)) (tiHG : H :&: G = 1).
+ +
+Lemma quotient_isom : isom G (G / H) (restrm nHG (coset H)).
+ +
+Lemma quotient_isog : isog G (G / H).
+ +
+End Injective.
+ +
+End CosetOfGroupTheory.
+ +
+Notation "A / H" := (quotient_group A H) : Group_scope.
+ +
+Section Quotient1.
+ +
+Variables (gT : finGroupType) (A : {set gT}).
+ +
+Lemma coset1_injm : 'injm (@coset gT 1).
+ +
+Lemma quotient1_isom : isom A (A / 1) (coset 1).
+ +
+Lemma quotient1_isog : isog A (A / 1).
+ +
+End Quotient1.
+ +
+Section QuotientMorphism.
+ +
+Variable (gT rT : finGroupType) (G H : {group gT}) (f : {morphism G >-> rT}).
+ +
+Implicit Types A : {set gT}.
+Implicit Types B : {set (coset_of H)}.
+Hypotheses (nsHG : H <| G).
+Let sHG : H \subset G := normal_sub nsHG.
+Let nHG : G \subset 'N(H) := normal_norm nsHG.
+Let nfHfG : f @* G \subset 'N(f @* H) := morphim_norms f nHG.
+ +
+Notation fH := (coset (f @* H) \o f).
+ +
+Lemma quotm_dom_proof : G \subset 'dom fH.
+ +
+Notation fH_G := (restrm quotm_dom_proof fH).
+ +
+Lemma quotm_ker_proof : 'ker (coset H) \subset 'ker fH_G.
+ +
+Definition quotm := factm quotm_ker_proof nHG.
+ +
+Canonical quotm_morphism := [morphism G / H of quotm].
+ +
+Lemma quotmE x : x \in G → quotm (coset H x) = coset (f @* H) (f x).
+ +
+Lemma morphim_quotm A : quotm @* (A / H) = f @* A / f @* H.
+ +
+Lemma morphpre_quotm Abar : quotm @*^-1 (Abar / f @* H) = f @*^-1 Abar / H.
+ +
+Lemma ker_quotm : 'ker quotm = 'ker f / H.
+ +
+Lemma injm_quotm : 'injm f → 'injm quotm.
+ +
+End QuotientMorphism.
+ +
+Section EqIso.
+ +
+Variables (gT : finGroupType) (G H : {group gT}).
+ +
+Hypothesis (eqGH : G :=: H).
+ +
+Lemma im_qisom_proof : 'N(H) \subset 'N(G).
+Lemma qisom_ker_proof : 'ker (coset G) \subset 'ker (coset H).
+ Lemma qisom_restr_proof : setT \subset 'N(H) / G.
+ +
+Definition qisom :=
+ restrm qisom_restr_proof (factm qisom_ker_proof im_qisom_proof).
+ +
+Canonical qisom_morphism := Eval hnf in [morphism of qisom].
+ +
+Lemma qisomE x : qisom (coset G x) = coset H x.
+ +
+Lemma val_qisom Gx : val (qisom Gx) = val Gx.
+ +
+Lemma morphim_qisom A : qisom @* (A / G) = A / H.
+ +
+Lemma morphpre_qisom A : qisom @*^-1 (A / H) = A / G.
+ +
+Lemma injm_qisom : 'injm qisom.
+ +
+Lemma im_qisom : qisom @* setT = setT.
+ +
+Lemma qisom_isom : isom setT setT qisom.
+ +
+Lemma qisom_isog : [set: coset_of G] \isog [set: coset_of H].
+ +
+Lemma qisom_inj : injective qisom.
+ +
+Lemma morphim_qisom_inj : injective (fun Gx ⇒ qisom @* Gx).
+ +
+End EqIso.
+ +
+ +
+Section FirstIsomorphism.
+ +
+Variables aT rT : finGroupType.
+ +
+Lemma first_isom (G : {group aT}) (f : {morphism G >-> rT}) :
+ {g : {morphism G / 'ker f >-> rT} | 'injm g &
+ ∀ A : {set aT}, g @* (A / 'ker f) = f @* A}.
+ +
+Variables (G H : {group aT}) (f : {morphism G >-> rT}).
+Hypothesis sHG : H \subset G.
+ +
+Lemma first_isog : (G / 'ker f) \isog (f @* G).
+ +
+Lemma first_isom_loc : {g : {morphism H / 'ker_H f >-> rT} |
+ 'injm g & ∀ A : {set aT}, A \subset H → g @* (A / 'ker_H f) = f @* A}.
+ +
+Lemma first_isog_loc : (H / 'ker_H f) \isog (f @* H).
+ +
+End FirstIsomorphism.
+ +
+Section SecondIsomorphism.
+ +
+Variables (gT : finGroupType) (H K : {group gT}).
+ +
+Hypothesis nKH : H \subset 'N(K).
+ +
+Lemma second_isom : {f : {morphism H / (K :&: H) >-> coset_of K} |
+ 'injm f & ∀ A : {set gT}, A \subset H → f @* (A / (K :&: H)) = A / K}.
+ +
+Lemma second_isog : H / (K :&: H) \isog H / K.
+ +
+Lemma weak_second_isog : H / (K :&: H) \isog H × K / K.
+ +
+End SecondIsomorphism.
+ +
+Section ThirdIsomorphism.
+ +
+Variables (gT : finGroupType) (G H K : {group gT}).
+ +
+Lemma homg_quotientS (A : {set gT}) :
+ A \subset 'N(H) → A \subset 'N(K) → H \subset K → A / K \homg A / H.
+ +
+Hypothesis sHK : H \subset K.
+Hypothesis snHG : H <| G.
+Hypothesis snKG : K <| G.
+ +
+Theorem third_isom : {f : {morphism (G / H) / (K / H) >-> coset_of K} | 'injm f
+ & ∀ A : {set gT}, A \subset G → f @* (A / H / (K / H)) = A / K}.
+ +
+Theorem third_isog : (G / H / (K / H)) \isog (G / K).
+ +
+End ThirdIsomorphism.
+ +
+Lemma char_from_quotient (gT : finGroupType) (G H K : {group gT}) :
+ H <| K → H \char G → K / H \char G / H → K \char G.
+ +
+
+ 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.
+
++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.
+