Library mathcomp.fingroup.quotient

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
From mathcomp Require Import choice fintype prime finset fingroup morphism.
From mathcomp Require Import 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 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 }.

#[hnf] HB.instance Definition _ := [Finite of coset_of by <:].

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.


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.

Arguments coset_of {gT} H%g : rename.
Arguments coset {gT} H%g x%g : rename.
Arguments quotient {gT} A%g H%g : rename.
Arguments coset_reprK {gT H%g} xbar%g : rename.

Bind Scope group_scope with coset_of.

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.
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.

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.
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.

Variant 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.

Arguments qisom_inj {gT G H} eqGH [x1 x2].
Arguments morphim_qisom_inj {gT G H} eqGH [x1 x2].

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.