Library mathcomp.fingroup.morphism

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import fintype finfun 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, the domain of f. 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. 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 with 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 denote 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 is a morphism that 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 :> aT → FinGroup.sort rT;
_ : {in D &, {morph mfun : x y / x × y }}
}.

We give the 'lightest' possible specification to define morphisms: local congruence, in D, 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).

Variant 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 }") : type_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.

Arguments morphimP {aT rT D A y f}.
Arguments morphpreP {aT rT D R x f}.

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.

Arguments morphim _ _ _%g _ _ _%g.
Arguments morphpre _ _ _%g _ _ _%g.

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 i → F 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 D → f @* 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 D → x \in A → f x \in f @* A.

Lemma mem_morphpre R x : x \in D → f x \in R → x \in f @*^-1 R.

Lemma morphimS A B : A \subset B → f @* 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 S → f @*^-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 D → f @* [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 D → f @* (A × B ) = f @* A × f @* B.

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

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

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

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

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

Lemma classes_morphim A :
  A \subset D → classes (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 D → reflect (f x = 1) (x \in 'ker f).

Lemma dom_ker : {subset 'ker f ≤ D }.

Lemma mker x : x \in 'ker f → f x = 1.

Lemma mkerl x y : x \in 'ker f → y \in D → f (x × y) = f y.

Lemma mkerr x y : x \in D → y \in 'ker f → f (x × y) = f x.

Lemma rcoset_kerP x y :
x \in D → y \in D → reflect (f x = f y) (x \in 'ker f :* y).

Lemma ker_rcoset 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 G A : 'ker f \subset G → f @* (G :&: A ) = f @* G :&: f @* A.

Lemma morphimIG A G : 'ker f \subset G → f @* (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 G → f @* (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 @* D → f @*^-1 (R × S ) = f @*^-1 R × f @*^-1 S.

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

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

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

Lemma morphpreK R : R \subset f @* D → f @* (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 @* D → S \subset f @* D →
  (f @*^-1 R \proper f @*^-1 S ) = (R \proper S ).

Lemma sub_morphpre_im 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 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 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 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 A : A \subset D → f @* <<A >> = <<f @* A >>.

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

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

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

commutator, normaliser, normal, center properties

Lemma morphimR A B :
  A \subset D → B \subset D → f @* [~: 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 <| B → f @* A <| f @* B.

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

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

Lemma morphim_subcent1 A x : x \in D → f @* '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 A → abelian (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 @* D → S \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 G → G \subset D → f @* 'N (G ) = 'N_(f @* D )(f @* G ).

Lemma morphim_subnormG A G :
  'ker f \subset G → G \subset D → f @* '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 D → R \subset f @* D → f @*^-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 @* D → f @*^-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 D → f @*^-1 (f @* A ) = A.

Lemma injm_morphim_inj A B :
  A \subset D → B \subset D → f @* A = f @* B → A = 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 D → f 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 D → R \subset f @* D →
  (f @*^-1 R \subset A ) = (R \subset f @* A ).

Lemma injm_eq A B : A \subset D → B \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 D → f @* 'N (A ) = 'N_(f @* D )(f @* A ).

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

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

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

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

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

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

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

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

Lemma injm_abelian A : A \subset D → abelian (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.

Arguments injmP {aT rT D f}.
Arguments morphpreK {aT rT D f} [R] sRf.

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 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 A → idm A @* B = B.

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

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

End IdentityMorphism.

Arguments idm {_} _%g _%g.

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 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 A → fA @* 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 :> (aT → rT ), 'ker g = 'ker_A f ,
                                 ∀ R, g @*^-1 R = A :&: f @*^-1 R
                               & ∀ B, B \subset A → g @* B = f @* B ]}.

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

End RestrictedMorphism.

Arguments restrm {_ _ _%g _%g} _ _%g.
Arguments restrmP {aT rT A D}.
Arguments domP {aT rT A D}.

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.

Arguments trivm {aT rT} _%g _%g.

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

Local Notation 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 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 x : x \in G → ff (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 G → invm @* (f @* A ) = A.

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

Lemma injm_proper 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 , ∀ x, ifactm (f x) = g x }.

Lemma morphim_ifactm (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 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) :=
[∀ 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 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 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 f → isog.

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

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

End Defs.

Infix "\isog" := isog.

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 G → isom H K f → f @* H = K.

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

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

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

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

End ReflectProp.

Arguments isom {_ _} _%g _%g _.
Arguments morphic {_ _} _%g _.
Arguments misom _ _ _%g _%g _.
Arguments isog {_ _} _%g _%g.

Arguments morphicP {aT rT A f}.
Arguments misomP {aT rT A B f}.
Arguments isom_isog [aT rT A B D].
Arguments isomP {aT rT G H f}.
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 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 isom_sym (f : {morphism G >-> hT }) (isoGH : isom G H f) :
  isom H G (isom_inv isoGH).

Lemma isog_symr : G \isog H → H \isog G.

Lemma isog_trans : G \isog H → H \isog K → G \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 aT → rT } | 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 D → homg (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 B → homg B G → homg 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 H → homg 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 H → homg G K = homg H K.

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

End Homg.

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

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

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

Arguments sgvalmK {gT G} A.
Arguments subgmK {gT G} [A] sAG.