Library normal

version 2 License, as specified in the README file.                 
                                                                    
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 (nHG: H <| G) (nGf : f@* G = G) (nHf : f@*H = H)            
                       == the quotient morphism induced by f and H  
Lemmas for these notions, plus the three isomorphism theorems, and  
counting lemmas for morphisms.                                      

Import Prenex Implicits.

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_of 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_eqMixin.
Definition coset_choiceMixin := [choiceMixin of coset_of by <:].
Canonical Structure coset_choiceType :=
  Eval hnf in ChoiceType coset_choiceMixin.
Definition coset_countMixin := [countMixin of coset_of by <:].
Canonical Structure coset_countType := Eval hnf in CountType 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_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.

Let nNH := subsetP (norm_gen A).

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_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 coset_imT : coset @* 'N(A) = setT.

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

Definition quotient : {set coset_of} := coset @* Q.

Lemma quotientE : quotient = coset @* Q. Qed.

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 card_quotient : forall A, A \subset 'N(H) -> #|A / H| = #|A : 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 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 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 sub_cosetpre : forall M, H \subset coset H @*^-1 M.

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 quotient_mulg : forall A, A * H / H = A / H.

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

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

Section Injective.

Variables (G : {group gT}).
Hypotheses (nHG : G \subset 'N(H)) (trGH : G :&: H = 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 : finGroupType) (G H : {group gT}) (f : {morphism G >-> gT}).

Implicit Types A : {set gT}.
Implicit Types B : {set (coset_groupType H)}.
Hypotheses (nHG : H <| G) (nGf : f @* G = G) (nHf : f @* H = H).

Notation fH := (coset H \o f).

Lemma quotm_restr_proof : G \subset 'dom fH.

Notation fH_G := (restrm quotm_restr_proof fH).

Lemma quotm_fact_proof1 : G \subset 'N(H).

Lemma quotm_fact_proof2 : 'ker (coset H) \subset 'ker fH_G.

Definition quotm := factm quotm_fact_proof1 quotm_fact_proof2.
Canonical Structure quotm_morphism := Eval hnf in [morphism of quotm].

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

Lemma cosetpre_quotm : forall A,
  quotm @*^-1 (A / H) = f @*^-1 A / H.

Lemma ker_quotm : 'ker quotm = 'ker f / H.

Lemma injm_quotm : 'injm f -> 'injm quotm.

End QuotientMorphism.

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

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.

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

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.