(Joint Center)Library MathComp.quotient

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice.
Require Import fintype prime finset fingroup morphism automorphism.

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 _ = A rather than A, is covered 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.
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 xbarcoset 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 xbarrepr 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 Acoset 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)) = falsecoset 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.
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 Gcoset H x \in G / H.

Lemma quotientS A B : A \subset BA / 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 Hcoset H (x × y) = coset H y.

Lemma coset_kerr x y : y \in Hcoset 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 yexists2 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 <| Gcoset 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 HG / H = 1.

Lemma sub_cosetpre M : H \subset coset H @*^-1 M.

Lemma quotient_proper G K :
  H <| GH <| 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 GG / H)}.

Lemma quotient_inj G1 G2 :
   H <| G1H <| G2G1 / H = G2 / HG1 :=: 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 Ccoset 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 <| BA / 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 Aabelian (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 Grestrm 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 / Hinv_quotient_spec (fun KK \subset G).

Lemma inv_quotientN : Kbar <| G / Hinv_quotient_spec (fun KK <| 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 Gquotm (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 Gxqisom @* Gx).

End EqIso.

Implicit Arguments qisom_inj [gT G H].
Implicit Arguments morphim_qisom_inj [gT G H].

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 Hg @* (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 Hf @* (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 KA / 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 Gf @* (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 <| KH \char GK / H \char G / HK \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| pcoprime #|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 GG \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 fG \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 GG \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 KK \subset GG \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.