Library mathcomp.fingroup.morphism
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ 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.
+ 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
+ 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}}
+}.
+ +
+
+
++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).
+ +
+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.
+ +
+ +
+
+
++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.
+ +
+ +
+
+ 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}.
+ +
+
+
++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 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]}}.
+ +
+
+
++ +
+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.
+ +
+
+
++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^#.
+ +
+
+
++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|.
+ +
+
+
++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.
+ +
+
+
++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>>.
+ +
+
+
++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).
+ +
+
+
++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.
+ +
+ +
+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.
+ +
+ +
+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}.
+ +
+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.
+ +
+ +
+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.
+ +
+ +
+
+
++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.
+ +
+ +
+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.
+ +
+ +
+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}.
+ +
+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.
+ +
+ +
+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.
+ +
+ +
+
+ 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}.
+ +
+ +
+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.
+ +
+
+
++ +
+Variables gT hT rT : finGroupType.
+Variables (G : {group gT}) (H : {group hT}).
+ +
+Variable f : {morphism G >-> hT}.
+Variable g : {morphism H >-> rT}.
+ +
+ +
+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.
+ +
+
+
++ +
+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}).
+ +
+
+
++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.
+ +
+ +
+
+
++ [∀ 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.
+ +
+ +
+
+ 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.
+ +
+ +
+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.
+ +
+Notation "G \homg H" := (homg G H)
+ (at level 70, no associativity) : group_scope.
+ +
+ +
+
+
++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.
+ +
+ +
+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.
+ +
+Notation "G \homg H" := (homg G H)
+ (at level 70, no associativity) : group_scope.
+ +
+ +
+
+ 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 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.
+ +
+
++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 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.
+ +
+