Library quotient

 This file contains the definitions of:                              

   coset_of H           == right cosets by the group H (see below)   
   coset_groupType H    == the groupType induced by 'N(H) / H        
   coset H              == the canonical projection induced by H     
   A / B                == the quotient of A by B,                   
                               made to coincide w/ (A :&: 'N(B)) / B 
   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]. 

 Lemmas for these notions, plus the three isomorphism theorems, and  
 counting lemmas for morphisms.                                      


Import GroupScope.

       Cosets are right cosets of elements in the normaliser      

Section Cosets.

Variables (gT : finGroupType) (Q A : {set gT}).

 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, its        
 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 is that            
      1 : coset_of A : set _ = <<A>> rather than A,                
 is covered by the genGid lemma.                                   

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 Structure coset_subType :=
  Eval hnf in [subType for set_of_coset by coset_of_rect].
Definition coset_eqMixin := Eval hnf in [eqMixin of coset_of by <:].
Canonical Structure coset_eqType :=
  Eval hnf in EqType coset_of coset_eqMixin.
Definition coset_choiceMixin := [choiceMixin of coset_of by <:].
Canonical Structure coset_choiceType :=
  Eval hnf in ChoiceType coset_of coset_choiceMixin.
Definition coset_countMixin := [countMixin of coset_of by <:].
Canonical Structure coset_countType :=
  Eval hnf in CountType coset_of coset_countMixin.
Canonical Structure coset_subCountType :=
  Eval hnf in [subCountType of coset_of].
Definition coset_finMixin := [finMixin of coset_of by <:].
Canonical Structure coset_finType :=
  Eval hnf in FinType coset_of coset_finMixin.
Canonical Structure 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.


Lemma coset_range_mul : forall B C : coset_of, coset_range (B * C).

Definition coset_mul B C := Coset (coset_range_mul B C).

Lemma coset_range_inv : forall 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 Structure coset_baseGroupType :=
  Eval hnf in BaseFinGroupType coset_of coset_of_groupMixin.
Canonical Structure 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 : forall x, x \in 'N(A) -> coset x :=: H :* x.

Lemma coset_morphM : {in 'N(A) &, {morph coset : x y / x * y}}.

Canonical Structure coset_morphism := Morphism coset_morphM.

Lemma ker_coset_prim : 'ker coset = 'N_H(A).

Implicit Type xbar : coset_of.

Lemma coset_mem : forall y xbar, y \in xbar -> coset y = xbar.

 coset is an inverse to repr 

Lemma mem_repr_coset : forall 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 : forall xbar, {x | x \in 'N(A) & xbar = coset x}.

Lemma coset_id : forall x, x \in A -> coset x = 1.

Lemma im_coset : coset @* 'N(A) = setT.

Lemma sub_im_coset : forall C : {set coset_of}, C \subset coset @* 'N(A).

Lemma cosetpre_proper : forall 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}.
Implicit Types G K : {group gT}.
Implicit Types xbar yb : coset_of H.
Implicit Types C D : {set coset_of H}.
Implicit Types L M : {group coset_of H}.

Canonical Structure quotient_group G A : {group coset_of A} :=
  Eval hnf in [group of G / A].

Infix "/" := quotient_group : subgroup_scope.

Lemma val_coset : forall x, x \in 'N(H) -> coset H x :=: H :* x.

Lemma coset_default : forall x, (x \in 'N(H)) = false -> coset H x = 1.

Lemma coset_norm : forall xbar, xbar \subset 'N(H).

Lemma ker_coset : 'ker (coset H) = H.

Lemma coset_idr : forall x, x \in 'N(H) -> coset H x = 1 -> x \in H.

Lemma repr_coset_norm : forall xbar, repr xbar \in 'N(H).

Lemma imset_coset : forall G, coset H @: G = G / H.

Lemma val_quotient : forall A, val @: (A / H) = rcosets H 'N_A(H).

Lemma card_quotient_subnorm : forall A, #|A / H| = #|'N_A(H) : H|.

Lemma leq_quotient : forall A, #|A / H| <= #|A|.

Lemma ltn_quotient : forall A,
  H :!=: 1 -> H \subset A -> #|A / H| < #|A|.

Lemma card_quotient : forall A, A \subset 'N(H) -> #|A / H| = #|A : H|.

Lemma divg_normal : forall 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 quotientT.              
Lemma quotientT : 'N(H) / H = setT.

 Variant of morphimIdom. 
Lemma quotientInorm : forall A, 'N_A(H) / H = A / H.

Lemma mem_quotient : forall x G, x \in G -> coset H x \in G / H.

Lemma quotientS : forall A B, A \subset B -> A / H \subset B / H.

Lemma quotient0 : set0 / H = set0.

Lemma quotient_set1 : forall x, x \in 'N(H) -> [set x] / H = [set coset H x].

Lemma quotient1 : 1 / H = 1.

Lemma quotientV : forall A, A^-1 / H = (A / H)^-1.

Lemma quotientMl : forall A B,
  A \subset 'N(H) -> A * B / H = (A / H) * (B / H).

Lemma quotientMr : forall A B,
  B \subset 'N(H) -> A * B / H = (A / H) * (B / H).

Lemma cosetpreM : forall C D,
  coset H @*^-1 (C * D) = coset H @*^-1 C * coset H @*^-1 D.

Lemma quotientJ : forall A x, x \in 'N(H) -> A :^ x / H = (A / H) :^ coset H x.

Lemma quotientU : forall A B, (A :|: B) / H = A / H :|: B / H.

Lemma quotientI : forall A B, (A :&: B) / H \subset A / H :&: B / H.

Lemma quotientY : forall A B,
  A \subset 'N(H) -> B \subset 'N(H) -> (A <*> B) / H = (A / H) <*> (B / H).

Lemma quotient_homg : forall A, A \subset 'N(H) -> homg (A / H) A.

Lemma coset_kerl : forall x y, x \in H -> coset H (x * y) = coset H y.

Lemma coset_kerr : forall x y, y \in H -> coset H (x * y) = coset H x.

Lemma rcoset_kercosetP : forall x y,
  x \in 'N(H) -> y \in 'N(H) -> reflect (coset H x = coset H y) (x \in H :* y).

Lemma kercoset_rcoset : forall 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 : forall G A, H \subset G -> (G :&: A) / H = G / H :&: A / H.

Lemma quotientIG : forall A G, H \subset G -> (A :&: G) / H = A / H :&: G / H.

Lemma quotientD : forall A B, A / H :\: B / H \subset (A :\: B) / H.

Lemma quotientDG : forall A G, H \subset G -> (A :\: G) / H = A / H :\: G / H.

Lemma quotientK : forall A, A \subset 'N(H) -> coset H @*^-1 (A / H) = H * A.

Lemma quotientYK : forall G, G \subset 'N(H) -> coset H @*^-1 (G / H) = H <*> G.

Lemma quotientGK : forall G, H <| G -> coset H @*^-1 (G / H) = G.

Lemma cosetpre_set1 : forall x,
  x \in 'N(H) -> coset H @*^-1 [set coset H x] = H :* x.

Lemma cosetpre_set1_coset : forall xbar, coset H @*^-1 [set xbar] = xbar.

Lemma cosetpreK : forall C, coset H @*^-1 C / H = C.

 Variant of morhphim_ker 
Lemma trivg_quotient : H / H = 1.

Lemma quotientS1 : forall G, G \subset H -> G / H = 1.

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

Lemma quotient_proper : forall G K,
  H <| G -> H <| K -> (G / H \proper K / H) = (G \proper K).

Lemma normal_cosetpre : forall M, H <| coset H @*^-1 M.

Lemma cosetpreSK : forall C D,
  (coset H @*^-1 C \subset coset H @*^-1 D) = (C \subset D).

Lemma sub_quotient_pre : forall A C,
  A \subset 'N(H) -> (A / H \subset C) = (A \subset coset H @*^-1 C).

Lemma sub_cosetpre_quo : forall C G,
  H <| G -> (coset H @*^-1 C \subset G) = (C \subset G / H).

 Variant of ker_trivg_morphim. 
Lemma quotient_sub1 : forall A,
  A \subset 'N(H) -> (A / H \subset [1]) = (A \subset H).

Lemma quotientSK : forall A B,
  A \subset 'N(H) -> (A / H \subset B / H) = (A \subset H * B).

Lemma quotientSGK : forall 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 : forall G1 G2,
   H <| G1 -> H <| G2 -> G1 / H = G2 / H -> G1 :=: G2.

Lemma quotient_gen : forall A, A \subset 'N(H) -> <<A>> / H = <<A / H>>.

Lemma cosetpre_gen : forall C,
  1 \in C -> coset H @*^-1 <<C>> = <<coset H @*^-1 C>>.

Lemma quotientR : forall A B,
  A \subset 'N(H) -> B \subset 'N(H) -> [~: A, B] / H = [~: A / H, B / H].

Lemma quotient_norm : forall A, 'N(A) / H \subset 'N(A / H).

Lemma quotient_norms : forall A B, A \subset 'N(B) -> A / H \subset 'N(B / H).

Lemma quotient_subnorm : forall A B, 'N_A(B) / H \subset 'N_(A / H)(B / H).

Lemma quotient_normal : forall A B, A <| B -> A / H <| B / H.

Lemma quotient_cent1 : forall x, 'C[x] / H \subset 'C[coset H x].

Lemma quotient_cent1s : forall A x,
  A \subset 'C[x] -> A / H \subset 'C[coset H x].

Lemma quotient_subcent1 : forall A x,
  'C_A[x] / H \subset 'C_(A / H)[coset H x].

Lemma quotient_cent : forall A, 'C(A) / H \subset 'C(A / H).

Lemma quotient_cents : forall A B,
  A \subset 'C(B) -> A / H \subset 'C(B / H).

Lemma quotient_abelian : forall A, abelian A -> abelian (A / H).

Lemma quotient_subcent : forall A B, 'C_A(B) / H \subset 'C_(A / H)(B / H).

Lemma cosetpre_normal : forall C D,
  (coset H @*^-1 C <| coset H @*^-1 D) = (C <| D).

Lemma quotient_normG : forall G, H <| G -> 'N(G) / H = 'N(G / H).

Lemma quotient_subnormG : forall A G,
   H <| G -> 'N_A(G) / H = 'N_(A / H)(G / H).

Lemma cosetpre_cent1 : forall x,
  'C_('N(H))[x] \subset coset H @*^-1 'C[coset H x].

Lemma cosetpre_cent1s : forall C x,
  coset H @*^-1 C \subset 'C[x] -> C \subset 'C[coset H x].

Lemma cosetpre_subcent1 : forall C x,
  'C_(coset H @*^-1 C)[x] \subset coset H @*^-1 'C_C[coset H x].

Lemma cosetpre_cent : forall A, 'C_('N(H))(A) \subset coset H @*^-1 'C(A / H).

Lemma cosetpre_cents : forall A C,
  coset H @*^-1 C \subset 'C(A) -> C \subset 'C(A / H).

Lemma cosetpre_subcent : forall C A,
  'C_(coset H @*^-1 C)(A) \subset coset H @*^-1 'C_C(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 : forall A, A * H / H = A / H.

Lemma quotientMidl : forall A, H * A / H = A / H.

Lemma quotientYidr : forall G, G \subset 'N(H) -> G <*> H / H = G / H.

Lemma quotientYidl : forall 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) : subgroup_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.
 (nGf : f @* G = G) (nHf : f @* H = H). 

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 Structure quotm_morphism := [morphism G / H of quotm].

Lemma quotmE : forall x, x \in G -> quotm (coset H x) = coset (f @* H) (f x).

Lemma morphim_quotm : forall A, quotm @* (A / H) = f @* A / f @* H.

Lemma morphpre_quotm : forall 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 Structure qisom_morphism := Eval hnf in [morphism of qisom].

Lemma qisomE : forall x, qisom (coset G x) = coset H x.

Lemma val_qisom : forall Gx, val (qisom Gx) = val Gx.

Lemma morphim_qisom : forall A, qisom @* (A / G) = A / H.

Lemma morphpre_qisom : forall 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.

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

Section FirstIsomorphism.

Variables aT rT : finGroupType.

Lemma first_isom : forall (G : {group aT}) (f : {morphism G >-> rT}),
  {g : {morphism G / 'ker f >-> rT} | 'injm g &
      forall 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 & forall 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 & forall 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 : forall 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
   & forall 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 : forall (gT : finGroupType) (G H K : {group gT}),
  H <| K -> H \char G -> K / H \char G / H -> K \char G.

 slightly longer alternative for the last 3 lines of the last proof,
   using qisom to avoid some dependent rewriting.
rewrite -(morphim_qisom Hf) /= -(morphim_quotm f nsHG) -morphim_comp.
set q := _ \o _; have dq: 'dom q = G / H := morphpreT _.
rewrite -dq in chKG; rewrite chKG // ?injm_comp ?injm_qisom ?injm_quotm //.
by rewrite morphim_comp dq morphim_quotm morphim_qisom Gf.


 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 : forall G, #|f @* G| = #|D :&: G : 'ker f|.

Lemma dvdn_morphim : forall G, #|f @* G| %| #|G|.

Lemma logn_morphim : forall p G, logn p #|f @* G| <= logn p #|G|.

Lemma coprime_morphl : forall G p, coprime #|G| p -> coprime #|f @* G| p.

Lemma coprime_morphr : forall G p, coprime p #|G| -> coprime p #|f @* G|.

Lemma coprime_morph : forall G H,
 coprime #|G| #|H| -> coprime #|f @* G| #|f @* H|.

Lemma index_morphim_ker : forall G H,
    H \subset G -> G \subset D ->
  (#|f @* G : f @* H| * #|'ker_G f : H|)%N = #|G : H|.

Lemma index_morphim : forall G H,
  G :&: H \subset D -> #|f @* G : f @* H| %| #|G : H|.

Lemma index_injm : forall G H,
  'injm f -> G \subset D -> #|f @* G : f @* H| = #|G : H|.

Lemma card_morphpre : forall L,
  L \subset f @* D -> #|f @*^-1 L| = (#|'ker f| * #|L|)%N.

Lemma index_morphpre : forall L M,
  L \subset f @* D -> #|f @*^-1 L : f @*^-1 M| = #|L : M|.

End CardMorphism.

Lemma card_homg : forall (aT rT : finGroupType),
                  forall (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.