Library morphism

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype finfun finset.
Require Import fingroup.

 This file contains the definitions of:                                     

   {morphism D >-> rT} ==                                                   
     the structure type of functions that are group morphisms mapping a     
     domain set D : {set aT} to a type rT; rT must have a finGroupType      
     structure, and D is usually a group (most of the theory expects this). 
            mfun == the coercion projecting {morphism D >-> rT} to aT -> rT 

 Basic examples:                                                            
            idm D == the identity morphism with domain D, or more precisely 
                     the identity function, but with a canonical            
                     {morphism G -> gT} structure.                          
          trivm D == the trivial morphism with domain D                     
 If f has a {morphism D >-> rT} structure                                   
           'dom f == D                                                      
           f @* A == the image of A by f, where f is defined                
                  := f @: (D :&: A)                                         
        f @*^-1 R == the pre-image of R by f, where f is defined            
                  :=  D :&: f @^-1: R                                       
           'ker f == the kernel of f                                        
                  :=  f @^-1: 1                                             
         'ker_G f == the kernel of f restricted to G                        
                  :=  G :&: 'ker f (this is a pure notation)                
          'injm f <=> f injective on D                                      
                  <-> ker f \subset 1 (this is a pure notation)             
        invm injf == the inverse morphism of f, with domain f @* D, when f  
                     is injective (injf : 'injm f)                          
    restrm f sDom == the restriction of f to a subset A of D, given         
                     (sDom : A \subset D); restrm f sDom is transparently   
                     identical to f; the restrmP and domP lemmas provide    
                     opaque restrictions.                                   
     invm f infj  == the inverse morphism for an injective f, with domain   
                     f @* D, given (injf : 'injm f)                         

      G \isog H  <=> G and H are isomorphic as groups                       
       H \homg G <=> H is a homomorphic image of G                          
      isom G H f <=> f maps G isomorphically to H, provided D contains G    
                 <-> f @: G^# == H^#                                        

 If, moreover, g : {morphism G >-> gT} with G : {group aT},                 
  factm sKer sDom == the (natural) factor morphism mapping f @* G to g @* G 
                     given sDom : G \subset D, sKer : 'ker f \subset 'ker g 
    ifactm injf g == the (natural) factor morphism mapping f @* G to g @* G 
                     when f is injective (injf : 'injm f); here g must      
                     be an actual morphism structure, not its function      
                     projection.                                            

 If g has a {morphism G >-> aT} structure for any G : {group gT}, then      
           f \o g has a canonical {morphism g @*^-1 D >-> rT} structure     

 Finally, for an arbitrary function f : aT -> rT                            
     morphic D f <=> f preserves group multiplication in D, i.e.,           
                     f (x * y) = (f x) * (f y) for all x, y in D            
        morphm fM == a function identical to f, but with a canonical        
                     {morphism D >-> rT} structure, given fM : morphic D f  
      misom D C f <=> f maps D isomorphically to C                          
                  := morphic D f && isom D C f                              


Import GroupScope.

Reserved Notation "x \isog y" (at level 70).

Section MorphismStructure.

Variables aT rT : finGroupType.

Structure morphism (D : {set aT}) : Type := Morphism {
  mfun :> aT -> FinGroup.sort rT;
  _ : {in D &, {morph mfun : x y / x * y}}
}.

 We give the most 'lightweight' possible specification to define morphisms:
 local congruence with the group law of aT. We then provide the properties 
 for the 'textbook' notion of morphism, when the required structures are   
 available (e.g. its domain is a group).                                   

Definition morphism_for D of phant rT := morphism D.

Definition clone_morphism D f :=
  let: Morphism _ fM := f
    return {type of @Morphism D for f} -> morphism_for D (Phant rT)
  in fun k => k fM.

Variables (D A : {set aT}) (R : {set rT}) (x : aT) (y : rT) (f : aT -> rT).

CoInductive morphim_spec : Prop := MorphimSpec z & z \in D & z \in A & y = f z.

Lemma morphimP : reflect morphim_spec (y \in f @: (D :&: A)).

Lemma morphpreP : reflect (x \in D /\ f x \in R) (x \in D :&: f @^-1: R).

End MorphismStructure.

Notation "{ 'morphism' D >-> T }" := (morphism_for D (Phant T))
  (at level 0, format "{ 'morphism' D >-> T }") : group_scope.
Notation "[ 'morphism' D 'of' f ]" :=
     (@clone_morphism _ _ D _ (fun fM => @Morphism _ _ D f fM))
   (at level 0, format "[ 'morphism' D 'of' f ]") : form_scope.
Notation "[ 'morphism' 'of' f ]" := (clone_morphism (@Morphism _ _ _ f))
   (at level 0, format "[ 'morphism' 'of' f ]") : form_scope.

Implicit Arguments morphimP [aT rT D A f y].
Implicit Arguments morphpreP [aT rT D R f x].

 domain, image, preimage, kernel, using phantom types to infer the domain 

Section MorphismOps1.

Variables (aT rT : finGroupType) (D : {set aT}) (f : {morphism D >-> rT}).

Lemma morphM : {in D &, {morph f : x y / x * y}}.

Notation morPhantom := (phantom (aT -> rT)).
Definition MorPhantom := Phantom (aT -> rT).

Definition dom of morPhantom f := D.

Definition morphim of morPhantom f := fun A => f @: (D :&: A).

Definition morphpre of morPhantom f := fun R : {set rT} => D :&: f @^-1: R.

Definition ker mph := morphpre mph 1.

End MorphismOps1.

Notation "''dom' f" := (dom (MorPhantom f))
  (at level 10, f at level 8, format "''dom' f") : group_scope.

Notation "''ker' f" := (ker (MorPhantom f))
  (at level 10, f at level 8, format "''ker' f") : group_scope.

Notation "''ker_' H f" := (H :&: 'ker f)
  (at level 10, H at level 2, f at level 8, format "''ker_' H f")
  : group_scope.

Notation "f @* A" := (morphim (MorPhantom f) A)
  (at level 24, format "f @* A") : group_scope.

Notation "f @*^-1 R" := (morphpre (MorPhantom f) R)
  (at level 24, format "f @*^-1 R") : group_scope.

Notation "''injm' f" := (pred_of_set ('ker f) \subset pred_of_set 1)
  (at level 10, f at level 8, format "''injm' f") : group_scope.

Section MorphismTheory.

Variables aT rT : finGroupType.
Implicit Types A B : {set aT}.
Implicit Types G H : {group aT}.
Implicit Types R S : {set rT}.
Implicit Types M : {group rT}.

 Most properties of morphims hold only when the domain is a group. 
Variables (D : {group aT}) (f : {morphism D >-> rT}).

Lemma morph1 : f 1 = 1.

Lemma morphV : {in D, {morph f : x / x^-1}}.

Lemma morphJ : {in D &, {morph f : x y / x ^ y}}.

Lemma morphX : forall n, {in D, {morph f : x / x ^+ n}}.

Lemma morphR : {in D &, {morph f : x y / [~ x, y]}}.

 morphic image,preimage properties w.r.t. set-theoretic operations 

Lemma morphimE : forall A, f @* A = f @: (D :&: A).

Lemma morphpreE : forall R, f @*^-1 R = D :&: f @^-1: R.

Lemma kerE : 'ker f = f @*^-1 1.

Lemma morphimEsub : forall A, A \subset D -> f @* A = f @: A.

Lemma morphimEdom : f @* D = f @: D.

Lemma morphimIdom : forall A, f @* (D :&: A) = f @* A.

Lemma morphpreIdom : forall R, D :&: f @*^-1 R = f @*^-1 R.

Lemma morphpreIim : forall R, f @*^-1 (f @* D :&: R) = f @*^-1 R.

Lemma morphimIim : forall A, f @* D :&: f @* A = f @* A.

Lemma mem_morphim : forall A x, x \in D -> x \in A -> f x \in f @* A.

Lemma mem_morphpre : forall R x, x \in D -> f x \in R -> x \in f @*^-1 R.

Lemma morphimS : forall A B, A \subset B -> f @* A \subset f @* B.

Lemma morphim_sub : forall A, f @* A \subset f @* D.

Lemma leq_morphim : forall A, #|f @* A| <= #|A|.

Lemma morphpreS : forall R S, R \subset S -> f @*^-1 R \subset f @*^-1 S.

Lemma morphim_setIpre : forall A R, f @* (A :&: f @*^-1 R) = f @* A :&: R.

Lemma morphim0 : f @* set0 = set0.

Lemma morphim_set1 : forall x, x \in D -> f @* [set x] = [set f x].

Lemma morphim1 : f @* 1 = 1.

Lemma morphimV : forall A, f @* A^-1 = (f @* A)^-1.

Lemma morphpreV : forall R, f @*^-1 R^-1 = (f @*^-1 R)^-1.

Lemma morphimMl : forall A B, A \subset D -> f @* (A * B) = f @* A * f @* B.

Lemma morphimMr : forall A B, B \subset D -> f @* (A * B) = f @* A * f @* B.

Lemma morphpreMl : forall R S,
  R \subset f @* D -> f @*^-1 (R * S) = f @*^-1 R * f @*^-1 S.

Lemma morphimJ : forall A x, x \in D -> f @* (A :^ x) = f @* A :^ f x.

Lemma morphpreJ : forall R x, x \in D -> f @*^-1 (R :^ f x) = f @*^-1 R :^ x.

Lemma morphimU : forall A B, f @* (A :|: B) = f @* A :|: f @* B.

Lemma morphimI : forall A B, f @* (A :&: B) \subset f @* A :&: f @* B.

Lemma morphpre0 : f @*^-1 set0 = set0.

Lemma morphpreT : f @*^-1 setT = D.

Lemma morphpreU : forall R S, f @*^-1 (R :|: S) = f @*^-1 R :|: f @*^-1 S.

Lemma morphpreI : forall R S, f @*^-1 (R :&: S) = f @*^-1 R :&: f @*^-1 S.

Lemma morphpreD : forall R S, f @*^-1 (R :\: S) = f @*^-1 R :\: f @*^-1 S.

 kernel, domain properties 

Lemma kerP : forall x, x \in D -> reflect (f x = 1) (x \in 'ker f).

Lemma dom_ker : {subset 'ker f <= D}.

Lemma mker : forall x, x \in 'ker f -> f x = 1.

Lemma mkerl : forall x y, x \in 'ker f -> y \in D -> f (x * y) = f y.

Lemma mkerr : forall x y, x \in D -> y \in 'ker f -> f (x * y) = f x.

Lemma rcoset_kerP : forall x y,
  x \in D -> y \in D -> reflect (f x = f y) (x \in 'ker f :* y).

Lemma ker_rcoset : forall x y,
  x \in D -> y \in D -> f x = f y -> exists2 z, z \in 'ker f & x = z * y.

Lemma ker_norm : D \subset 'N('ker f).

Lemma ker_normal : 'ker f <| D.

Lemma morphimGI : forall G A,
  'ker f \subset G -> f @* (G :&: A) = f @* G :&: f @* A.

Lemma morphimIG : forall A G,
  'ker f \subset G -> f @* (A :&: G) = f @* A :&: f @* G.

Lemma morphimD : forall A B, f @* A :\: f @* B \subset f @* (A :\: B).

Lemma morphimDG : forall A G,
  'ker f \subset G -> f @* (A :\: G) = f @* A :\: f @* G.

 group structure preservation 

Lemma morphpre_groupset : forall M, group_set (f @*^-1 M).

Lemma morphim_groupset : forall G, group_set (f @* G).

Canonical Structure morphpre_group fPh M :=
  @group _ (morphpre fPh M) (morphpre_groupset M).
Canonical Structure morphim_group fPh G :=
  @group _ (morphim fPh G) (morphim_groupset G).
Canonical Structure ker_group fPh : {group aT} :=
  Eval hnf in [group of ker fPh].

Lemma morph_dom_groupset : group_set (f @: D).

Canonical Structure morph_dom_group := group morph_dom_groupset.

Lemma morphpreMr : forall R S,
  S \subset f @* D -> f @*^-1 (R * S) = f @*^-1 R * f @*^-1 S.

 compatibility with inclusion 

Lemma morphimK : forall A, A \subset D -> f @*^-1 (f @* A) = 'ker f * A.

Lemma morphimGK : forall G,
 'ker f \subset G -> G \subset D -> f @*^-1 (f @* G) = G.

Lemma morphpre_set1 : forall x, x \in D -> f @*^-1 [set f x] = 'ker f :* x.

Lemma morphpreK : forall R, R \subset f @* D -> f @* (f @*^-1 R) = R.

Lemma morphim_ker : f @* 'ker f = 1.

Lemma ker_sub_pre : forall M, 'ker f \subset f @*^-1 M.

Lemma ker_normal_pre : forall M, 'ker f <| f @*^-1 M.

Lemma morphpreSK : forall R S,
  R \subset f @* D -> (f @*^-1 R \subset f @*^-1 S) = (R \subset S).

Lemma sub_morphim_pre : forall A R,
  A \subset D -> (f @* A \subset R) = (A \subset f @*^-1 R).

Lemma morphpre_proper : forall R S,
  R \subset f @* D -> S \subset f @* D ->
  (f @*^-1 R \proper f @*^-1 S) = (R \proper S).

Lemma sub_morphpre_im : forall R G,
    'ker f \subset G -> G \subset D -> R \subset f @* D ->
  (f @*^-1 R \subset G) = (R \subset f @* G).

Lemma ker_trivg_morphim : forall A,
  (A \subset 'ker f) = (A \subset D) && (f @* A \subset [1]).

Lemma morphimSK : forall A B,
  A \subset D -> (f @* A \subset f @* B) = (A \subset 'ker f * B).

Lemma morphimSGK : forall A G,
  A \subset D -> 'ker f \subset G -> (f @* A \subset f @* G) = (A \subset G).

Lemma ltn_morphim : forall A, [1] \proper 'ker_A f -> #|f @* A| < #|A|.

 injectivity of image and preimage 

Lemma morphpre_inj :
  {in [pred R : {set rT} | R \subset f @* D] &, injective (fun R => f @*^-1 R)}.

Lemma morphim_injG :
  {in [pred G : {group aT} | ('ker f \subset G) && (G \subset D)] &,
   injective (fun G => f @* G)}.

Lemma morphim_inj : forall G H,
    ('ker f \subset G) && (G \subset D) ->
    ('ker f \subset H) && (H \subset D) ->
  f @* G = f @* H -> G :=: H.

 commutation with generated groups and cycles 

Lemma morphim_gen : forall A, A \subset D -> f @* <<A>> = <<f @* A>>.

Lemma morphim_cycle : forall x, x \in D -> f @* <[x]> = <[f x]>.

Lemma morphimY : forall A B,
  A \subset D -> B \subset D -> f @* (A <*> B) = f @* A <*> f @* B.

Lemma morphpre_gen : forall R,
  1 \in R -> R \subset f @* D -> f @*^-1 <<R>> = <<f @*^-1 R>>.

 commutator, normaliser, normal, center properties

Lemma morphimR : forall A B,
  A \subset D -> B \subset D -> f @* [~: A, B] = [~: f @* A, f @* B].

Lemma morphim_norm : forall A, f @* 'N(A) \subset 'N(f @* A).

Lemma morphim_norms : forall A B,
  A \subset 'N(B) -> f @* A \subset 'N(f @* B).

Lemma morphim_subnorm : forall A B, f @* 'N_A(B) \subset 'N_(f @* A)(f @* B).

Lemma morphim_normal : forall A B, A <| B -> f @* A <| f @* B.

Lemma morphim_cent1 : forall x, x \in D -> f @* 'C[x] \subset 'C[f x].

Lemma morphim_cent1s : forall A x,
  x \in D -> A \subset 'C[x] -> f @* A \subset 'C[f x].

Lemma morphim_subcent1 : forall A x, x \in D ->
   f @* 'C_A[x] \subset 'C_(f @* A)[f x].

Lemma morphim_cent : forall A, f @* 'C(A) \subset 'C(f @* A).

Lemma morphim_cents : forall A B,
  A \subset 'C(B) -> f @* A \subset 'C(f @* B).

Lemma morphim_subcent : forall A B, f @* 'C_A(B) \subset 'C_(f @* A)(f @* B).

Lemma morphim_abelian : forall A, abelian A -> abelian (f @* A).

Lemma morphpre_norm : forall R, f @*^-1 'N(R) \subset 'N(f @*^-1 R).

Lemma morphpre_norms : forall R S,
  R \subset 'N(S) -> f @*^-1 R \subset 'N(f @*^-1 S).

Lemma morphpre_normal : forall R S,
  R \subset f @* D -> S \subset f @* D -> (f @*^-1 R <| f @*^-1 S) = (R <| S).

Lemma morphpre_subnorm : forall R S,
  f @*^-1 'N_R(S) \subset 'N_(f @*^-1 R)(f @*^-1 S).

Lemma morphim_normG : forall G,
  'ker f \subset G -> G \subset D -> f @* 'N(G) = 'N_(f @* D)(f @* G).

Lemma morphim_subnormG : forall A G,
  'ker f \subset G -> G \subset D -> f @* 'N_A(G) = 'N_(f @* A)(f @* G).

Lemma morphpre_cent1 : forall x, x \in D -> 'C_D[x] \subset f @*^-1 'C[f x].

Lemma morphpre_cent1s : forall R x,
  x \in D -> R \subset f @* D -> f @*^-1 R \subset 'C[x] -> R \subset 'C[f x].

Lemma morphpre_subcent1 : forall R x, x \in D ->
  'C_(f @*^-1 R)[x] \subset f @*^-1 'C_R[f x].

Lemma morphpre_cent : forall A, 'C_D(A) \subset f @*^-1 'C(f @* A).

Lemma morphpre_cents : forall A R,
  R \subset f @* D -> f @*^-1 R \subset 'C(A) -> R \subset 'C(f @* A).

Lemma morphpre_subcent : forall R A,
  'C_(f @*^-1 R)(A) \subset f @*^-1 'C_R(f @* A).

 local injectivity properties 

Lemma injmP : reflect {in D &, injective f} ('injm f).

Lemma card_im_injm : (#|f @* D| == #|D|) = 'injm f.

Section Injective.

Hypothesis injf : 'injm f.

Lemma ker_injm : 'ker f = 1.

Lemma injmK : forall A, A \subset D -> f @*^-1 (f @* A) = A.

Lemma injm_morphim_inj : forall A B,
  A \subset D -> B \subset D -> f @* A = f @* B -> A = B.

Lemma card_injm : forall A, A \subset D -> #|f @* A| = #|A|.

Lemma order_injm : forall x, x \in D -> #[f x] = #[x].

Lemma injm1 : forall x, x \in D -> f x = 1 -> x = 1.

Lemma morph_injm_eq1 : forall x, x \in D -> (f x == 1) = (x == 1).

Lemma morphim_injm_eq1 : forall A, A \subset D -> (f @* A == 1) = (A == 1).

Lemma injmSK : forall A B,
  A \subset D -> (f @* A \subset f @* B) = (A \subset B).

Lemma sub_morphpre_injm : forall R A,
    A \subset D -> R \subset f @* D ->
  (f @*^-1 R \subset A) = (R \subset f @* A).

Lemma injmI : forall A B, f @* (A :&: B) = f @* A :&: f @* B.

Lemma injm_norm : forall A, A \subset D -> f @* 'N(A) = 'N_(f @* D)(f @* A).

Lemma injm_subnorm : forall A B,
  B \subset D -> f @* 'N_A(B) = 'N_(f @* A)(f @* B).

Lemma injm_cent1 : forall x, x \in D -> f @* 'C[x] = 'C_(f @* D)[f x].

Lemma injm_subcent1 : forall A x, x \in D -> f @* 'C_A[x] = 'C_(f @* A)[f x].

Lemma injm_cent : forall A, A \subset D -> f @* 'C(A) = 'C_(f @* D)(f @* A).

Lemma injm_subcent : forall A B,
  B \subset D -> f @* 'C_A(B) = 'C_(f @* A)(f @* B).

Lemma injm_abelian : forall A, A \subset D -> abelian (f @* A) = abelian A.

End Injective.

Lemma eq_morphim : forall g : {morphism D >-> rT},
  {in D, f =1 g} -> forall A, f @* A = g @* A.

Lemma eq_in_morphim : forall B A (g : {morphism B >-> rT}),
  D :&: A = B :&: A -> {in A, f =1 g} -> f @* A = g @* A.

End MorphismTheory.

Notation "''ker' f" := (ker_group (MorPhantom f)) : subgroup_scope.
Notation "''ker_' G f" := (G :&: 'ker f)%G : subgroup_scope.
Notation "f @* G" := (morphim_group (MorPhantom f) G) : subgroup_scope.
Notation "f @*^-1 M" := (morphpre_group (MorPhantom f) M) : subgroup_scope.
Notation "f @: D" := (morph_dom_group f D) : subgroup_scope.

Section IdentityMorphism.

Variable gT : finGroupType.
Implicit Types A B : {set gT}.
Implicit Type G : {group gT}.

Definition idm of {set gT} := fun x : gT => x : FinGroup.sort gT.

Lemma idm_morphM : forall A, {in A & , {morph idm A : x y / x * y}}.

Canonical Structure idm_morphism A := Morphism (@idm_morphM A).

Lemma injm_idm : forall G, 'injm (idm G).

Lemma ker_idm : forall G, 'ker (idm G) = 1.

Lemma morphim_idm : forall A B, B \subset A -> idm A @* B = B.

Lemma morphpre_idm : forall A B, idm A @*^-1 B = A :&: B.

Lemma im_idm : forall A, idm A @* A = A.

End IdentityMorphism.


Section RestrictedMorphism.

Variables aT rT : finGroupType.
Variables A D : {set aT}.
Implicit Type B : {set aT}.
Implicit Type R : {set rT}.

Definition restrm of A \subset D := @id (aT -> FinGroup.sort rT).

Section Props.

Hypothesis sAD : A \subset D.
Variable f : {morphism D >-> rT}.
Local Notation fA := (restrm sAD (mfun f)).

Canonical Structure restrm_morphism :=
  @Morphism aT rT A fA (sub_in2 (subsetP sAD) (morphM f)).

Lemma morphim_restrm : forall B, fA @* B = f @* (A :&: B).

Lemma im_restrm : fA @* A = f @* A.

Lemma morphpre_restrm : forall R, fA @*^-1 R = A :&: f @*^-1 R.

Lemma ker_restrm : 'ker fA = 'ker_A f.

Lemma injm_restrm : 'injm f -> 'injm fA.

End Props.

Lemma restrmP : forall f : {morphism D >-> rT}, A \subset 'dom f ->
  {g : {morphism A >-> rT} | [/\ g = f :> (aT -> rT), 'ker g = 'ker_A f,
                                 forall R, g @*^-1 R = A :&: f @*^-1 R
                               & forall B, B \subset A -> g @* B = f @* B]}.

Lemma domP : forall f : {morphism D >-> rT}, 'dom f = A ->
  {g : {morphism A >-> rT} | [/\ g = f :> (aT -> rT), 'ker g = 'ker f,
                                 forall R, g @*^-1 R = f @*^-1 R
                               & forall B, g @* B = f @* B]}.

End RestrictedMorphism.

Implicit Arguments restrmP [aT rT D A].
Implicit Arguments domP [aT rT D A].

Section TrivMorphism.

Variables aT rT : finGroupType.

Definition trivm of {set aT} & aT := 1 : FinGroup.sort rT.

Lemma trivm_morphM : forall A : {set aT},
  {in A & , {morph trivm A : x y / x * y}}.

Canonical Structure triv_morph A := Morphism (@trivm_morphM A).

Lemma morphim_trivm : forall (G H : {group aT}), trivm G @* H = 1.

Lemma ker_trivm : forall G : {group aT}, 'ker (trivm G) = G.

End TrivMorphism.


 Canonical Structure of morphism for the composition of 2 morphisms. 

Section MorphismComposition.

Variables gT hT rT : finGroupType.
Variables (G : {group gT}) (H : {group hT}).

Variable f : {morphism G >-> hT}.
Variable g : {morphism H >-> rT}.

Notation Local gof := (mfun g \o mfun f).

Lemma comp_morphM : {in f @*^-1 H &, {morph gof: x y / x * y}}.

Canonical Structure comp_morphism := Morphism comp_morphM.

Lemma ker_comp : 'ker gof = f @*^-1 'ker g.

Lemma injm_comp : 'injm f -> 'injm g -> 'injm gof.

Lemma morphim_comp : forall A : {set gT}, gof @* A = g @* (f @* A).

Lemma morphpre_comp : forall C : {set rT},
  gof @*^-1 C = f @*^-1 (g @*^-1 C).

End MorphismComposition.

 Canonical structure of morphism for the factor morphism 

Section FactorMorphism.

Variables aT qT rT : finGroupType.

Variables G H : {group aT}.
Variable f : {morphism G >-> rT}.
Variable q : {morphism H >-> qT}.

Definition factm of 'ker q \subset 'ker f & G \subset H :=
  fun x => f (repr (q @*^-1 [set x])).

Hypothesis sKqKf : 'ker q \subset 'ker f.
Hypothesis sGH : G \subset H.

Notation ff := (factm sKqKf sGH).

Lemma factmE : forall x, x \in G -> ff (q x) = f x.

Lemma factm_morphM : {in q @* G &, {morph ff : x y / x * y}}.

Canonical Structure factm_morphism := Morphism factm_morphM.

Lemma morphim_factm : forall A : {set aT}, ff @* (q @* A) = f @* A.

Lemma morphpre_factm : forall C : {set rT}, ff @*^-1 C = q @* (f @*^-1 C).

Lemma ker_factm : 'ker ff = q @* 'ker f.

Lemma injm_factm : 'injm f -> 'injm ff.

Lemma injm_factmP : reflect ('ker f = 'ker q) ('injm ff).

Lemma ker_factm_loc : forall K : {group aT}, 'ker_(q @* K) ff = q @* 'ker_K f.

End FactorMorphism.


Section InverseMorphism.

Variables aT rT : finGroupType.
Implicit Types A B : {set aT}.
Implicit Types C D : {set rT}.
Variables (G : {group aT}) (f : {morphism G >-> rT}).
Hypothesis injf : 'injm f.

Lemma invm_subker : 'ker f \subset 'ker (idm G).

Definition invm := factm invm_subker (subxx _).

Canonical Structure invm_morphism := Eval hnf in [morphism of invm].

Lemma invmE : {in G, cancel f invm}.

Lemma invmK : {in f @* G, cancel invm f}.

Lemma morphpre_invm : forall A, invm @*^-1 A = f @* A.

Lemma morphim_invm : forall A, A \subset G -> invm @* (f @* A) = A.

Lemma morphim_invmE : forall C, invm @* C = f @*^-1 C.

Lemma injm_proper : forall A B,
  A \subset G -> B \subset G -> (f @* A \proper f @* B) = (A \proper B).

Lemma injm_invm : 'injm invm.

Lemma ker_invm : 'ker invm = 1.

Lemma im_invm : invm @* (f @* G) = G.

End InverseMorphism.


Section InjFactm.

Variables (gT aT rT : finGroupType) (D G : {group gT}).
Variables (g : {morphism G >-> rT}) (f : {morphism D >-> aT}) (injf : 'injm f).

Definition ifactm :=
  tag (domP [morphism of g \o invm injf] (morphpre_invm injf G)).

Lemma ifactmE : {in D, forall x, ifactm (f x) = g x}.

Lemma morphim_ifactm : forall A : {set gT},
  A \subset D -> ifactm @* (f @* A) = g @* A.

Lemma im_ifactm : G \subset D -> ifactm @* (f @* G) = g @* G.

Lemma morphpre_ifactm : forall C, ifactm @*^-1 C = f @* (g @*^-1 C).

Lemma ker_ifactm : 'ker ifactm = f @* 'ker g.

Lemma injm_ifactm : 'injm g -> 'injm ifactm.

End InjFactm.

 Reflected (boolean) form of morphism and isomorphism properties 

Section ReflectProp.

Variables aT rT : finGroupType.

Section Defs.

Variables (A : {set aT}) (B : {set rT}).

 morphic is the morphM property of morphisms seen through morphicP 
Definition morphic (f : aT -> rT) :=
  forallb u, (u \in [predX A & A]) ==> (f (u.1 * u.2) == f u.1 * f u.2).

Definition isom f := f @: A^# == B^#.

Definition misom f := morphic f && isom f.

Definition isog := existsb f : {ffun aT -> rT}, misom f.

Section MorphicProps.

Variable f : aT -> rT.

Lemma morphicP : reflect {in A &, {morph f : x y / x * y}} (morphic f).

Definition morphm of morphic f := f : aT -> FinGroup.sort rT.

Lemma morphmE : forall fM, morphm fM = f.

Canonical Structure morphm_morphism fM :=
  @Morphism _ _ A (morphm fM) (morphicP fM).

End MorphicProps.

Lemma misomP : forall f, reflect {fM : morphic f & isom (morphm fM)} (misom f).

Lemma misom_isog : forall f, misom f -> isog.

Lemma isom_isog : forall (D : {group aT}) (f : {morphism D >-> rT}),
  A \subset D -> isom f -> isog.

End Defs.

Implicit Arguments isom_isog [A B D].

Infix "\isog" := isog.

 The real reflection properties only hold for true groups and morphisms. 

Section Main.

Variables (G : {group aT}) (H : {group rT}).
Notation fMT := {morphism G >-> rT}.

Lemma isomP : forall f : fMT, reflect ('injm f /\ f @* G = H) (isom G H f).

Lemma isom_card : forall f : fMT, isom G H f -> #|G| = #|H|.

Lemma isogP : reflect (exists2 f : fMT, 'injm f & f @* G = H) (G \isog H).

End Main.

Variables (G : {group aT}) (f : {morphism G >-> rT}).

Lemma morphim_isom : forall (H : {group aT}) (K : {group rT}),
  H \subset G -> isom H K f -> f @* H = K.

Lemma sub_isom : forall (A : {set aT}) (C : {set rT}),
  A \subset G -> f @* A = C -> 'injm f -> isom A C f.

Lemma sub_isog : forall (A : {set aT}),
  A \subset G -> 'injm f -> isog A (f @* A).

End ReflectProp.

Implicit Arguments morphicP [aT rT A f].
Implicit Arguments misomP [aT rT A B f].
Implicit Arguments isom_isog [aT rT A B D].
Implicit Arguments isomP [aT rT G H f].
Implicit Arguments isogP [aT rT G H].
Notation "x \isog y":= (isog x y).

Section Isomorphisms.

Variables gT hT kT : finGroupType.
Variables (G : {group gT}) (H : {group hT}) (K : {group kT}).

Lemma isog_refl : G \isog G.

Lemma card_isog : G \isog H -> #|G| = #|H|.

Lemma isog_abelian : G \isog H -> abelian G = abelian H.

Lemma trivial_isog : G :=: 1 -> H :=: 1 -> G \isog H.

Lemma isog_eq1 : G \isog H -> (G :==: 1) = (H :==: 1).

Lemma isog_symr : G \isog H -> H \isog G.

Lemma isog_trans : G \isog H -> H \isog K -> G \isog K.

End Isomorphisms.

Section IsoBoolEquiv.

Variables gT hT kT : finGroupType.
Variables (G : {group gT}) (H : {group hT}) (K : {group kT}).

Lemma isog_sym : (G \isog H) = (H \isog G).

Lemma isog_transl : G \isog H -> (G \isog K) = (H \isog K).

Lemma isog_transr : G \isog H -> (K \isog G) = (K \isog H).

End IsoBoolEquiv.

Section Homg.

Implicit Types rT gT aT : finGroupType.

Definition homg rT aT (C : {set rT}) (D : {set aT}) :=
  existsb f : {ffun aT -> rT}, (morphic D f && (f @: D == C)).

Lemma homgP : forall rT aT (C : {set rT}) (D : {set aT}),
  reflect (exists f : {morphism D >-> rT}, f @* D = C) (homg C D).

Lemma morphim_homg : forall aT rT (A D : {set aT}) (f : {morphism D >-> rT}),
  A \subset D -> homg (f @* A) A.

Lemma leq_homg : forall rT aT (C : {set rT}) (G : {group aT}),
  homg C G -> #|C| <= #|G|.

Lemma homg_refl : forall aT (A : {set aT}), homg A A.

Lemma homg_trans : forall aT (B : {set aT}),
                   forall rT (C : {set rT}) gT (G : {group gT}),
  homg C B -> homg B G -> homg C G.

Lemma isogEcard : forall rT aT (G : {group rT}) (H : {group aT}),
  (G \isog H) = (homg G H) && (#|H| <= #|G|).

Lemma isog_hom : forall rT aT (G : {group rT}) (H : {group aT}),
  G \isog H -> homg G H.

Lemma isogEhom : forall rT aT (G : {group rT}) (H : {group aT}),
  (G \isog H) = homg G H && homg H G.

Lemma eq_homgl : forall gT aT rT,
                 forall (G : {group gT}) (H : {group aT}) (K : {group rT}),
  G \isog H -> homg G K = homg H K.

Lemma eq_homgr : forall gT rT aT,
                 forall (G : {group gT}) (H : {group rT}) (K : {group aT}),
  G \isog H -> homg K G = homg K H.

End Homg.

Notation "G \homg H" := (homg G H)
  (at level 70, no associativity) : group_scope.

Implicit Arguments homgP [rT aT C D].

 Isomorphism between a group and its subtype. 

Section SubMorphism.

Variables (gT : finGroupType) (G : {group gT}).

Canonical Structure sgval_morphism := Morphism (@sgvalM _ G).
Canonical Structure subg_morphism := Morphism (@subgM _ G).

Lemma injm_sgval : 'injm sgval.

Lemma injm_subg : 'injm (subg G).
Hint Resolve injm_sgval injm_subg.

Lemma ker_sgval : 'ker sgval = 1.

Lemma ker_subg : 'ker (subg G) = 1.

Lemma im_subg : subg G @* G = [subg G].

Lemma sgval_sub : forall A, sgval @* A \subset G.

Lemma sgvalmK : forall A, subg G @* (sgval @* A) = A.

Lemma subgmK : forall A : {set gT}, A \subset G -> sgval @* (subg G @* A) = A.

Lemma im_sgval : sgval @* [subg G] = G.

Lemma isom_subg : isom G [subg G] (subg G).

Lemma isom_sgval : isom [subg G] G sgval.

Lemma isog_subg : isog G [subg G].

End SubMorphism.