+ +

Library mathcomp.fingroup.automorphism

+ +

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

+ +

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