(Joint Center)Library MathComp.morphism

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun.
Require Import bigop finset 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

Set Implicit Arguments.

Import GroupScope.

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

Section MorphismStructure.

Variables aT rT : finGroupType.

Structure morphism (D : {set aT}) : Type := Morphism {
  mfun :> aTFinGroup.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 kk fM.

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

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 (aTrT)).
Definition MorPhantom := Phantom (aTrT).

Definition dom of morPhantom f := D.

Definition morphim of morPhantom f := fun Af @: (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 morph_prod I r (P : pred I) F :
    ( i, P iF i \in D) →
  f (\prod_(i <- r | P i) F i) = \prod_( i <- r | P i) f (F i).

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

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

Lemma morphX 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 A : f @* A = f @: (D :&: A).
Lemma morphpreE R : f @*^-1 R = D :&: f @^-1: R.
Lemma kerE : 'ker f = f @*^-1 1.

Lemma morphimEsub A : A \subset Df @* A = f @: A.

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

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

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

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

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

Lemma mem_morphim A x : x \in Dx \in Af x \in f @* A.

Lemma mem_morphpre R x : x \in Df x \in Rx \in f @*^-1 R.

Lemma morphimS A B : A \subset Bf @* A \subset f @* B.

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

Lemma leq_morphim A : #|f @* A| #|A|.

Lemma morphpreS R S : R \subset Sf @*^-1 R \subset f @*^-1 S.

Lemma morphpre_sub R : f @*^-1 R \subset D.

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

Lemma morphim0 : f @* set0 = set0.

Lemma morphim_eq0 A : A \subset D(f @* A == set0) = (A == set0).

Lemma morphim_set1 x : x \in Df @* [set x] = [set f x].

Lemma morphim1 : f @* 1 = 1.

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

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

Lemma morphimMl A B : A \subset Df @* (A × B) = f @* A × f @* B.

Lemma morphimMr A B : B \subset Df @* (A × B) = f @* A × f @* B.

Lemma morphpreMl R S :
  R \subset f @* Df @*^-1 (R × S) = f @*^-1 R × f @*^-1 S.

Lemma morphimJ A x : x \in Df @* (A :^ x) = f @* A :^ f x.

Lemma morphpreJ R x : x \in Df @*^-1 (R :^ f x) = f @*^-1 R :^ x.

Lemma morphim_class x A :
  x \in DA \subset Df @* (x ^: A) = f x ^: f @* A.

Lemma classes_morphim A :
  A \subset Dclasses (f @* A) = [set f @* xA | xA in classes A].

Lemma morphimT : f @* setT = f @* D.

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

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

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

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

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

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

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

kernel, domain properties

Lemma kerP x : x \in Dreflect (f x = 1) (x \in 'ker f).

Lemma dom_ker : {subset 'ker f D}.

Lemma mker x : x \in 'ker ff x = 1.

Lemma mkerl x y : x \in 'ker fy \in Df (x × y) = f y.

Lemma mkerr x y : x \in Dy \in 'ker ff (x × y) = f x.

Lemma rcoset_kerP x y :
  x \in Dy \in Dreflect (f x = f y) (x \in 'ker f :* y).

Lemma ker_rcoset x y :
  x \in Dy \in Df x = f yexists2 z, z \in 'ker f & x = z × y.

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

Lemma ker_normal : 'ker f <| D.

Lemma morphimGI G A : 'ker f \subset Gf @* (G :&: A) = f @* G :&: f @* A.

Lemma morphimIG A G : 'ker f \subset Gf @* (A :&: G) = f @* A :&: f @* G.

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

Lemma morphimDG A G : 'ker f \subset Gf @* (A :\: G) = f @* A :\: f @* G.

Lemma morphimD1 A : (f @* A)^# \subset f @* A^#.

group structure preservation

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

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

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

Lemma morph_dom_groupset : group_set (f @: D).

Canonical morph_dom_group := group morph_dom_groupset.

Lemma morphpreMr R S :
  S \subset f @* Df @*^-1 (R × S) = f @*^-1 R × f @*^-1 S.

Lemma morphimK A : A \subset Df @*^-1 (f @* A) = 'ker f × A.

Lemma morphimGK G : 'ker f \subset GG \subset Df @*^-1 (f @* G) = G.

Lemma morphpre_set1 x : x \in Df @*^-1 [set f x] = 'ker f :* x.

Lemma morphpreK R : R \subset f @* Df @* (f @*^-1 R) = R.

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

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

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

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

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

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

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

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

Lemma morphimSK A B :
  A \subset D(f @* A \subset f @* B) = (A \subset 'ker f × B).

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

Lemma ltn_morphim 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 Rf @*^-1 R)}.

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

Lemma morphim_inj G H :
    ('ker f \subset G) && (G \subset D)
    ('ker f \subset H) && (H \subset D)
  f @* G = f @* HG :=: H.

commutation with generated groups and cycles

Lemma morphim_gen A : A \subset Df @* <<A>> = <<f @* A>>.

Lemma morphim_cycle x : x \in Df @* <[x]> = <[f x]>.

Lemma morphimY A B :
  A \subset DB \subset Df @* (A <*> B) = f @* A <*> f @* B.

Lemma morphpre_gen R :
  1 \in RR \subset f @* Df @*^-1 <<R>> = <<f @*^-1 R>>.

commutator, normaliser, normal, center properties

Lemma morphimR A B :
  A \subset DB \subset Df @* [~: A, B] = [~: f @* A, f @* B].

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

Lemma morphim_norms A B : A \subset 'N(B)f @* A \subset 'N(f @* B).

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

Lemma morphim_normal A B : A <| Bf @* A <| f @* B.

Lemma morphim_cent1 x : x \in Df @* 'C[x] \subset 'C[f x].

Lemma morphim_cent1s A x : x \in DA \subset 'C[x]f @* A \subset 'C[f x].

Lemma morphim_subcent1 A x : x \in Df @* 'C_A[x] \subset 'C_(f @* A)[f x].

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

Lemma morphim_cents A B : A \subset 'C(B)f @* A \subset 'C(f @* B).

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

Lemma morphim_abelian A : abelian Aabelian (f @* A).

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

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

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

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

Lemma morphim_normG G :
  'ker f \subset GG \subset Df @* 'N(G) = 'N_(f @* D)(f @* G).

Lemma morphim_subnormG A G :
  'ker f \subset GG \subset Df @* 'N_A(G) = 'N_(f @* A)(f @* G).

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

Lemma morphpre_cent1s R x :
  x \in DR \subset f @* Df @*^-1 R \subset 'C[x]R \subset 'C[f x].

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

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

Lemma morphpre_cents A R :
  R \subset f @* Df @*^-1 R \subset 'C(A)R \subset 'C(f @* A).

Lemma morphpre_subcent 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 A : A \subset Df @*^-1 (f @* A) = A.

Lemma injm_morphim_inj A B :
  A \subset DB \subset Df @* A = f @* BA = B.

Lemma card_injm A : A \subset D#|f @* A| = #|A|.

Lemma order_injm x : x \in D#[f x] = #[x].

Lemma injm1 x : x \in Df x = 1 → x = 1.

Lemma morph_injm_eq1 x : x \in D(f x == 1) = (x == 1).

Lemma injmSK A B :
  A \subset D(f @* A \subset f @* B) = (A \subset B).

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

Lemma injm_eq A B : A \subset DB \subset D(f @* A == f @* B) = (A == B).

Lemma morphim_injm_eq1 A : A \subset D(f @* A == 1) = (A == 1).

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

Lemma injmD1 A : f @* A^# = (f @* A)^#.

Lemma nclasses_injm A : A \subset D#|classes (f @* A)| = #|classes A|.

Lemma injm_norm A : A \subset Df @* 'N(A) = 'N_(f @* D)(f @* A).

Lemma injm_norms A B :
  A \subset DB \subset D(f @* A \subset 'N(f @* B)) = (A \subset 'N(B)).

Lemma injm_normal A B :
  A \subset DB \subset D(f @* A <| f @* B) = (A <| B).

Lemma injm_subnorm A B : B \subset Df @* 'N_A(B) = 'N_(f @* A)(f @* B).

Lemma injm_cent1 x : x \in Df @* 'C[x] = 'C_(f @* D)[f x].

Lemma injm_subcent1 A x : x \in Df @* 'C_A[x] = 'C_(f @* A)[f x].

Lemma injm_cent A : A \subset Df @* 'C(A) = 'C_(f @* D)(f @* A).

Lemma injm_cents A B :
  A \subset DB \subset D(f @* A \subset 'C(f @* B)) = (A \subset 'C(B)).

Lemma injm_subcent A B : B \subset Df @* 'C_A(B) = 'C_(f @* A)(f @* B).

Lemma injm_abelian A : A \subset Dabelian (f @* A) = abelian A.

End Injective.

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

Lemma eq_in_morphim 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)) : Group_scope.
Notation "''ker_' G f" := (G :&: 'ker f)%G : Group_scope.
Notation "f @* G" := (morphim_group (MorPhantom f) G) : Group_scope.
Notation "f @*^-1 M" := (morphpre_group (MorPhantom f) M) : Group_scope.
Notation "f @: D" := (morph_dom_group f D) : Group_scope.

Implicit Arguments injmP [aT rT D f].

Section IdentityMorphism.

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

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

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

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

Lemma injm_idm G : 'injm (idm G).

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

Lemma morphim_idm A B : B \subset Aidm A @* B = B.

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

Lemma im_idm 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 (aTFinGroup.sort rT).

Section Props.

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

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

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

Lemma restrmEsub B : B \subset AfA @* B = f @* B.

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

Lemma morphpre_restrm 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 (f : {morphism D >-> rT}) : A \subset 'dom f
  {g : {morphism A >-> rT} | [/\ g = f :> (aTrT), 'ker g = 'ker_A f,
                                  R, g @*^-1 R = A :&: f @*^-1 R
                               & B, B \subset Ag @* B = f @* B]}.

Lemma domP (f : {morphism D >-> rT}) : 'dom f = A
  {g : {morphism A >-> rT} | [/\ g = f :> (aTrT), 'ker g = 'ker f,
                                  R, g @*^-1 R = f @*^-1 R
                               & 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 (A : {set aT}) : {in A &, {morph trivm A : x y / x × y}}.

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

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

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

End TrivMorphism.

Implicit Arguments trivm [[aT] [rT]].

The composition of two morphisms is a Canonical morphism instance.
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 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 (A : {set gT}) : gof @* A = g @* (f @* A).

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

End MorphismComposition.

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 xf (repr (q @*^-1 [set x])).

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

Notation ff := (factm sKqKf sGH).

Lemma factmE x : x \in Gff (q x) = f x.

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

Canonical factm_morphism := Morphism factm_morphM.

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

Lemma morphpre_factm (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 (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 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 A : invm @*^-1 A = f @* A.

Lemma morphim_invm A : A \subset Ginvm @* (f @* A) = A.

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

Lemma injm_proper A B :
  A \subset GB \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, x, ifactm (f x) = g x}.

Lemma morphim_ifactm (A : {set gT}) :
   A \subset Difactm @* (f @* A) = g @* A.

Lemma im_ifactm : G \subset Difactm @* (f @* G) = g @* G.

Lemma morphpre_ifactm 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 : aTrT) :=
  [ 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 := [ f : {ffun aTrT}, misom f].

Section MorphicProps.

Variable f : aTrT.

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

Definition morphm of morphic f := f : aTFinGroup.sort rT.

Lemma morphmE fM : morphm fM = f.

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

End MorphicProps.

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

Lemma misom_isog f : misom fisog.

Lemma isom_isog (D : {group aT}) (f : {morphism D >-> rT}) :
  A \subset Disom fisog.

Lemma isog_isom : isog{f : {morphism A >-> rT} | isom f}.

End Defs.

Infix "\isog" := isog.

Implicit Arguments isom_isog [A B D].

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

Section Main.

Variables (G : {group aT}) (H : {group rT}).

Lemma isomP (f : {morphism G >-> rT}) :
  reflect ('injm f f @* G = H) (isom G H f).

Lemma isogP :
  reflect (exists2 f : {morphism G >-> rT}, 'injm f & f @* G = H) (G \isog H).

Variable f : {morphism G >-> rT}.
Hypothesis isoGH : isom G H f.

Lemma isom_inj : 'injm f.
Lemma isom_im : f @* G = H.
Lemma isom_card : #|G| = #|H|.
Lemma isom_sub_im : H \subset f @* G.
Definition isom_inv := restrm isom_sub_im (invm isom_inj).

End Main.

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

Lemma morphim_isom (H : {group aT}) (K : {group rT}) :
  H \subset Gisom H K ff @* H = K.

Lemma sub_isom (A : {set aT}) (C : {set rT}) :
  A \subset Gf @* A = C'injm fisom A C f.

Lemma sub_isog (A : {set aT}) : A \subset G'injm fisog A (f @* A).

Lemma restr_isom_to (A : {set aT}) (C R : {group rT}) (sAG : A \subset G) :
   f @* A = Cisom G R fisom A C (restrm sAG f).

Lemma restr_isom (A : {group aT}) (R : {group rT}) (sAG : A \subset G) :
  isom G R fisom A (f @* A) (restrm sAG f).

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 idm_isom : isom G G (idm G).

Lemma isog_refl : G \isog G.

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

Lemma isog_abelian : G \isog Habelian G = abelian H.

Lemma trivial_isog : G :=: 1 → H :=: 1 → G \isog H.

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

Lemma isom_sym (f : {morphism G >-> hT}) (isoGH : isom G H f) :
  isom H G (isom_inv isoGH).

Lemma isog_symr : G \isog HH \isog G.

Lemma isog_trans : G \isog HH \isog KG \isog K.

Lemma nclasses_isog : G \isog H#|classes G| = #|classes H|.

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}) :=
  [ (f : {ffun aTrT} | morphic D f), f @: D == C].

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

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

Lemma leq_homg rT aT (C : {set rT}) (G : {group aT}) :
  homg C G#|C| #|G|.

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

Lemma homg_trans aT (B : {set aT}) rT (C : {set rT}) gT (G : {group gT}) :
  homg C Bhomg B Ghomg C G.

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

Lemma isog_hom rT aT (G : {group rT}) (H : {group aT}) : G \isog Hhomg G H.

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

Lemma eq_homgl gT aT rT (G : {group gT}) (H : {group aT}) (K : {group rT}) :
  G \isog Hhomg G K = homg H K.

Lemma eq_homgr gT rT aT (G : {group gT}) (H : {group rT}) (K : {group aT}) :
  G \isog Hhomg 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 sgval_morphism := Morphism (@sgvalM _ G).
Canonical 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 A : sgval @* A \subset G.

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

Lemma subgmK (A : {set gT}) : A \subset Gsgval @* (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.