Library morphisms

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype finfun finset.
Require Import groups.

This file contains the definitions of:                                    
                                                                          
  {morphism A >-> gT} == the type of morphisms from domain set A of       
                         elements of a groupType, to groupType gT         
                                                                          
if p is a morphism of domain A:                                           
  dom p                      == A                                         
  p @* B                     == the image of B, where defined             
                             := f @: (A :&: B)                            
  p @*^-1 C                  == the pre-image of C, where defined         
                             :=  A :&: f @^-1: B                          
  'ker p                     == the kernel of p                           
                             :=  p @*^-1: 1                               
  'ker_H p                   ==  (p @*^-1: 1), intersected with H         
  'injm p                    <=> p injective                              
                             <-> ker p \subset 1)                         
  invm p (H :'injm f)        == the inverse morphism for an injective p   
  idm B                      == the identity morphism on B                
  restrm p (H : A \subset B) == the morphism that coincides with p on its 
                                domain A                                  
  trivm B                    == the trivial morphism on B                 
                                                                          
if, moreover, q is a morphism of domain B:                                
  factm (H1 : A \subset B) (H2 : 'ker q \subset 'ker p) == the natural    
                                 surjection between the ranges of q and p 
                                                                          
for any function f between groupTypes :                                   
  morphic A f              <=> forall x,y in A, f(x * y) = (f x) * (f y)  
  isom A B f               <=> f @: (A  \: 1) = (B \: 1)                  
  misom A B f              <=> morphic A f && isom A B f                  
  A \isog B                <=> exists f, misom A B f                      
  morphm (H : morphic B f) == f with a canonical structure of morphism    
                              with domain B                               

Import Prenex Implicits.

Import GroupScope.

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

Section MorphismStructure.

Variables aT rT : finGroupType.

Structure morphism (A : {set aT}) : Type := Morphism {
  mfun :> aT -> FinGroup.sort rT;
  _ : {in A &, {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 A of phant rT := morphism A.

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

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

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

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

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

End MorphismStructure.

Notation "{ 'morphism' A >-> T }" := (morphism_for A (Phant T))
  (at level 0, format "{ 'morphism' A >-> T }") : group_scope.

Notation "[ 'morphism' 'of' f ]" :=
     (repack_morphism (fun fM => @Morphism _ _ _ f fM))
   (at level 0, format "[ 'morphism' 'of' f ]") : form_scope.

Implicit Arguments morphimP [aT rT A B f y].
Implicit Arguments morphpreP [aT rT A C f x].

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

Section MorphismOps1.

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

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

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

Definition dom of morphantom f := A.

Definition morphim of morphantom f := fun B => f @: (A :&: B).

Definition morphpre of morphantom f := fun C : {set rT} => A :&: f @^-1: C.

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 @* H" := (morphim (MorPhantom f) H)
  (at level 24, format "f @* H") : group_scope.

Notation "f @*^-1 L" := (morphpre (MorPhantom f) L)
  (at level 24, format "f @*^-1 L") : 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 K : {group aT}.
Implicit Types C D : {set rT}.
Implicit Types L M : {group rT}.

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

the usual properties occur when the domain is a group. 

Lemma morph1 : f 1 = 1.

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

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

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

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

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

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

Lemma morphpreE : forall C, f @*^-1 C = G :&: f @^-1: C. Qed.

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

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

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

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

Lemma morphpreIdom : forall C, G :&: f @*^-1 C = f @*^-1 C.

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

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

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

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

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

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

Lemma morphpreS : forall C D, C \subset D -> f @*^-1 C \subset f @*^-1 D.

Lemma morphim0 : f @* set0 = set0.

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

Lemma morphim1 : f @* 1 = 1.

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

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

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

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

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

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

Lemma morphpreJ : forall C x, x \in G -> f @*^-1 (C :^ f x) = f @*^-1 C :^ 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 = G.

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

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

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

kernel, domain properties 

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

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

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

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

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

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

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

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

Lemma ker_normal : 'ker f <| G.

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

Lemma morphimIG : forall (A : {set aT}) (H : {group aT}),
  'ker f \subset H -> f @* (A :&: H) = f @* A :&: f @* H.

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

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

group structure preservation 

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

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

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

Lemma morph_dom_groupset : group_set (f @: G).

Canonical Structure morph_dom_group := group morph_dom_groupset.

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

compatibility with inclusion 

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

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

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

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

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 C D,
  C \subset f @* G -> (f @*^-1 C \subset f @*^-1 D) = (C \subset D).

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

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

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

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

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

injectivity of image and preimage 

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

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

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

commutation with the generated group 

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

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

commutator, normaliser, normal, center properties

Lemma morphimR : forall A B,
  A \subset G -> B \subset G -> 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 G -> f @* 'C[x] \subset 'C[f x].

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

Lemma morphim_subcent1 : forall A x, x \in G ->
   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 C, f @*^-1 'N(C) \subset 'N(f @*^-1 C).

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

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

Lemma morphpre_subnorm : forall C D,
  f @*^-1 'N_C(D) \subset 'N_(f @*^-1 C)(f @*^-1 D).

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

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

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

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

Lemma morphpre_subcent1 : forall C x, x \in G ->
  'C_(f @*^-1 C)[x] \subset f @*^-1 'C_C[f x].

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

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

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

local injectivity properties 

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

Section Injective.

Hypothesis injf : 'injm f.

Lemma ker_injm : 'ker f = 1.

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

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

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

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

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

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

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

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

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

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

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

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

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

End Injective.

Variable g : {morphism G >-> rT}.

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

End MorphismTheory.

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

Section IdentityMorphism.

Variable gT : finGroupType.

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

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

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

Lemma injm_idm : forall G : {group gT}, 'injm (idm G).

Lemma ker_idm : forall G : {group gT}, 'ker (idm G) = 1.

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

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

End IdentityMorphism.


Module AfterMorph. End AfterMorph.

Section RestrictedMorphism.

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

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

Section Props.

Hypothesis sAB : A \subset B.
Variable f : {morphism B >-> rT}.
Notation fB := (restrm sAB (mfun f)).

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

Lemma morphim_restrm : forall C, fB @* C = f @* (A :&: C).

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

Lemma ker_restrm : 'ker (restrm sAB f) = 'ker_A f.

Lemma injm_restrm : 'injm f -> 'injm (restrm sAB f).

End Props.

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

End RestrictedMorphism.

Implicit Arguments restrmP [aT rT A B].

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 G \subset H & 'ker q \subset 'ker f :=
  fun x => f (repr (q @*^-1 [set x])).

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

Notation ff := (factm sGH sKqKf).

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 (subxx _) invm_subker.

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_invm : 'injm invm.

Lemma ker_invm : 'ker invm = 1.

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

End InverseMorphism.


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

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 isog_card : G \isog H -> #|G| = #|H|.

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

Lemma isog_triv : 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).

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

End IsoBoolEquiv.

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

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

Lemma subgEdom : 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 sgvalEdom : 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.