- -

Library mathcomp.fingroup.morphism

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

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

- -

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

- -

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

- -

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

- -

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

- -

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

- -

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

- -

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