# Library mathcomp.fingroup.automorphism

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype.
From mathcomp Require Import finset fingroup perm morphism.
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.
Arguments Aut _ _%g.
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.
Arguments morphim_fixP {gT G f}.
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.
Arguments conjgm _ _%g.
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.
Arguments characteristic _ _%g _%g.
Notation "H \char G" := (characteristic H G) : group_scope.
#[global] 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.