- -

Library mathcomp.fingroup.automorphism

- -

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

- -

- Group automorphisms and characteristic subgroups. - Unlike morphisms on a group G, which are functions of type gT -> rT, with - a canonical structure of dependent type {morphim G >-> rT}, automorphisms - are permutations of type {perm gT} contained in Aut G : {set {perm gT}}. - This lets us use the finGroupType of {perm gT}. Note also that while - morphisms on G are undefined outside G, automorphisms have their support - in G, i.e., they are the identity outside G. - Definitions: - Aut G (or [Aut G]) == the automorphism group of G. - [Aut G]%G == the group structure for Aut G. - autm AutGa == the morphism on G induced by a, given - AutGa : a \in Aut G. - perm_in injf fA == the permutation with support B in induced by f, - given injf : {in A &, injective f} and - fA : f @: A \subset A. - aut injf fG == the automorphism of G induced by the morphism f, - given injf : 'injm f and fG : f @* G \subset G. - Aut_isom injf sDom == the injective homomorphism that maps Aut G to - Aut (f @* G), with f : {morphism D >-> rT} and - given injf: 'injm f and sDom : G \subset D. - conjgm G == the conjugation automorphism on G. - H \char G == H is a characteristic subgroup of G. -

- -
-Set Implicit Arguments.
- -
-Import GroupScope.
- -
-

- -

- A group automorphism, defined as a permutation on a subset of a - finGroupType that respects the morphism law. - Here perm_on is used as a closure rule for the set A. -

- -
-Section Automorphism.
- -
-Variable gT : finGroupType.
-Implicit Type A : {set gT }.
-Implicit Types a b : {perm gT }.
- -
-Definition Aut A := [set a | perm_on A a & morphic A a ].
- -
-Lemma Aut_morphic A a : a \in Aut A → morphic A a.
- -
-Lemma out_Aut A a x : a \in Aut A → x \notin A → a x = x.
- -
-Lemma eq_Aut A : {in Aut A &, ∀ a b, {in A , a =1 b } → a = b }.
- -
-

- -

- The morphism that is represented by a given element of Aut A. -

- -
-Definition autm A a (AutAa : a \in Aut A) := morphm (Aut_morphic AutAa).
-Lemma autmE A a (AutAa : a \in Aut A) : autm AutAa = a.
- -
-Canonical autm_morphism A a aM := Eval hnf in [morphism of @autm A a aM ].
- -
-Section AutGroup.
- -
-Variable G : {group gT }.
- -
-Lemma Aut_group_set : group_set (Aut G).
- -
-Canonical Aut_group := group Aut_group_set.
- -
-Variable (a : {perm gT }) (AutGa : a \in Aut G).
-Notation f := (autm AutGa).
-Notation fE := (autmE AutGa).
- -
-Lemma injm_autm : 'injm f.
- -
-Lemma ker_autm : 'ker f = 1.
- -
-Lemma im_autm : f @* G = G.
- -
-Lemma Aut_closed x : x \in G → a x \in G.
- -
-End AutGroup.
- -
-Lemma Aut1 : Aut 1 = 1.
- -
-End Automorphism.
- -
-Notation "[ 'Aut' G ]" := (Aut_group G)
- (at level 0, format "[ 'Aut' G ]") : Group_scope.
-Notation "[ 'Aut' G ]" := (Aut G)
- (at level 0, only parsing) : group_scope.
- -
- -
-

- -

- The permutation function (total on the underlying groupType) that is the - representant of a given morphism f with domain A in (Aut A). -

- -
-Section PermIn.
- -
-Variables (T : finType) (A : {set T }) (f : T → T).
- -
-Hypotheses (injf : {in A &, injective f }) (sBf : f @: A \subset A).
- -
-Lemma perm_in_inj : injective (fun x ⇒ if x \in A then f x else x).
- -
-Definition perm_in := perm perm_in_inj.
- -
-Lemma perm_in_on : perm_on A perm_in.
- -
-Lemma perm_inE : {in A , perm_in =1 f }.
- -
-End PermIn.
- -
-

- -

- properties of injective endomorphisms -

- -
-Section MakeAut.
- -
-Variables (gT : finGroupType) (G : {group gT }) (f : {morphism G >-> gT }).
-Implicit Type A : {set gT }.
- -
-Hypothesis injf : 'injm f.
- -
-Lemma morphim_fixP A : A \subset G → reflect (f @* A = A) (f @* A \subset A).
- -
-Hypothesis Gf : f @* G = G.
- -
-Lemma aut_closed : f @: G \subset G.
- -
-Definition aut := perm_in (injmP injf) aut_closed.
- -
-Lemma autE : {in G , aut =1 f }.
- -
-Lemma morphic_aut : morphic G aut.
- -
-Lemma Aut_aut : aut \in Aut G.
- -
-Lemma imset_autE A : A \subset G → aut @: A = f @* A.
- -
-Lemma preim_autE A : A \subset G → aut @^-1: A = f @*^-1 A.
- -
-End MakeAut.
- -
- -
-Section AutIsom.
- -
-Variables (gT rT : finGroupType) (G D : {group gT }) (f : {morphism D >-> rT }).
- -
-Hypotheses (injf : 'injm f) (sGD : G \subset D).
-Let domG := subsetP sGD.
- -
-Lemma Aut_isom_subproof a :
- {a' | a' \in Aut (f @* G) & a \in Aut G → {in G , a' \o f =1 f \o a }}.
- -
-Definition Aut_isom a := s2val (Aut_isom_subproof a).
- -
-Lemma Aut_Aut_isom a : Aut_isom a \in Aut (f @* G).
- -
-Lemma Aut_isomE a : a \in Aut G → {in G , ∀ x, Aut_isom a (f x) = f (a x)}.
- -
-Lemma Aut_isomM : {in Aut G &, {morph Aut_isom : x y / x × y }}.
-Canonical Aut_isom_morphism := Morphism Aut_isomM.
- -
-Lemma injm_Aut_isom : 'injm Aut_isom.
- -
-End AutIsom.
- -
-Section InjmAut.
- -
-Variables (gT rT : finGroupType) (G D : {group gT }) (f : {morphism D >-> rT }).
- -
-Hypotheses (injf : 'injm f) (sGD : G \subset D).
-Let domG := subsetP sGD.
- -
-Lemma im_Aut_isom : Aut_isom injf sGD @* Aut G = Aut (f @* G).
- -
-Lemma Aut_isomP : isom (Aut G) (Aut (f @* G)) (Aut_isom injf sGD).
- -
-Lemma injm_Aut : Aut (f @* G) \isog Aut G.
- -
-End InjmAut.
- -
-

- -

- conjugation automorphism -

- -
-Section ConjugationMorphism.
- -
-Variable gT : finGroupType.
-Implicit Type A : {set gT }.
- -
-Definition conjgm of {set gT } := fun x y : gT ⇒ y ^ x.
- -
-Lemma conjgmE A x y : conjgm A x y = y ^ x.
- -
-Canonical conjgm_morphism A x :=
- @Morphism _ _ A (conjgm A x) (in2W (fun y z ⇒ conjMg y z x)).
- -
-Lemma morphim_conj A x B : conjgm A x @* B = (A :&: B ) :^ x.
- -
-Variable G : {group gT }.
- -
-Lemma injm_conj x : 'injm (conjgm G x ).
- -
-Lemma conj_isom x : isom G (G :^ x) (conjgm G x).
- -
-Lemma conj_isog x : G \isog G :^ x.
- -
-Lemma norm_conjg_im x : x \in 'N (G ) → conjgm G x @* G = G.
- -
-Lemma norm_conj_isom x : x \in 'N (G ) → isom G G (conjgm G x).
- -
-Definition conj_aut x := aut (injm_conj _) (norm_conjg_im (subgP (subg _ x))).
- -
-Lemma norm_conj_autE : {in 'N (G ) & G , ∀ x y, conj_aut x y = y ^ x }.
- -
-Lemma conj_autE : {in G &, ∀ x y, conj_aut x y = y ^ x }.
- -
-Lemma conj_aut_morphM : {in 'N (G ) &, {morph conj_aut : x y / x × y }}.
- -
-Canonical conj_aut_morphism := Morphism conj_aut_morphM.
- -
-Lemma ker_conj_aut : 'ker conj_aut = 'C (G ).
- -
-Lemma Aut_conj_aut A : conj_aut @* A \subset Aut G.
- -
-End ConjugationMorphism.
- -
- -
-Reserved Notation "G \char H" (at level 70).
- -
-

- -

- Characteristic subgroup -

- -
-Section Characteristicity.
- -
-Variable gT : finGroupType.
-Implicit Types A B : {set gT }.
-Implicit Types G H K L : {group gT }.
- -
-Definition characteristic A B :=
-  (A \subset B ) && [∀ f in Aut B , f @: A \subset A ].
- -
-Infix "\char" := characteristic.
- -
-Lemma charP H G :
-  let fixH (f : {morphism G >-> gT }) := 'injm f → f @* G = G → f @* H = H in
-  reflect [/\ H \subset G & ∀ f, fixH f ] (H \char G).
- -
-

- -

- Characteristic subgroup properties : composition, relational properties -

- -
-Lemma char1 G : 1 \char G.
- -
-Lemma char_refl G : G \char G.
- -
-Lemma char_trans H G K : K \char H → H \char G → K \char G.
- -
-Lemma char_norms H G : H \char G → 'N (G ) \subset 'N (H ).
- -
-Lemma char_sub A B : A \char B → A \subset B.
- -
-Lemma char_norm_trans H G A : H \char G → A \subset 'N (G ) → A \subset 'N (H ).
- -
-Lemma char_normal_trans H G K : K \char H → H <| G → K <| G.
- -
-Lemma char_normal H G : H \char G → H <| G.
- -
-Lemma char_norm H G : H \char G → G \subset 'N (H ).
- -
-Lemma charI G H K : H \char G → K \char G → H :&: K \char G.
- -
-Lemma charY G H K : H \char G → K \char G → H <*> K \char G.
- -
-Lemma charM G H K : H \char G → K \char G → H × K \char G.
- -
-Lemma lone_subgroup_char G H :
-  H \subset G → (∀ K, K \subset G → K \isog H → K \subset H ) →
-  H \char G.
- -
-End Characteristicity.
- -
-Notation "H \char G" := (characteristic H G) : group_scope.
-Hint Resolve char_refl : core.
- -
-Section InjmChar.
- -
-Variables (aT rT : finGroupType) (D : {group aT }) (f : {morphism D >-> rT }).
- -
-Hypothesis injf : 'injm f.
- -
-Lemma injm_char (G H : {group aT }) :
-  G \subset D → H \char G → f @* H \char f @* G.
- -
-End InjmChar.
- -
-Section CharInjm.
- -
-Variables (aT rT : finGroupType) (D : {group aT }) (f : {morphism D >-> rT }).
-Hypothesis injf : 'injm f.
- -
-Lemma char_injm (G H : {group aT }) :
-  G \subset D → H \subset D → (f @* H \char f @* G ) = (H \char G ).
- -
-End CharInjm.
- -
-Unset Implicit Arguments.
-