Library automorphism

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
Group automorphisms and characteristic subgroups.                      
In this file:                                                          
 Aut A                == the automorphism group of A.                  
 autm (Af:f\in Aut A) == the morphism induced by an element of (Aut A) 
 perm_in (H1: {in B, injective f}) (H2: f @:B \subset B)               
                      == the permutation induced by a                  
                            bijective endofunction                     
 aut (H1: 'injm f) {H2: f @:G \subset G)                               
                      == the element of Aut A induced by a             
                            bijective endomorphism of domain G         
 conjgm A             == the conjugation automorphism on A             
 H \char G            == H is a characteristic subgroup of G           

Import Prenex Implicits.

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 f g : {perm gT}.

Definition Aut A := [set f | perm_on A f && morphic A f].

Lemma Aut_morphic : forall A f, f \in Aut A -> morphic A f.

Lemma out_Aut : forall A f x, f \in Aut A -> x \notin A -> f x = x.

Lemma eq_Aut : forall A, {in Aut A &, forall f g, {in A, f =1 g} -> f = g}.

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

Definition autm A f Af := morphm (@Aut_morphic A f Af).
Lemma autmE : forall A f Af, @autm A f Af = f.

Canonical Structure autm_morphism A f fM :=
  Eval hnf in [morphism of @autm A f fM].

Section AutGroup.

Variable G : {group gT}.

Lemma Aut_group_set : group_set (Aut G).

Canonical Structure Aut_group := group Aut_group_set.

Variable (f : {perm gT}) (Af : f \in Aut G).
Notation fm := (autm Af).
Notation fmE := (autmE Af).

Lemma injm_autm : 'injm fm.

Lemma ker_autm : 'ker fm = 1.

Lemma autm_dom : fm @* G = G.
End AutGroup.

Lemma Aut1 : Aut 1 = 1.

End Automorphism.

Notation "[ 'Aut' G ]" := (Aut_group G)
  (at level 0, format "[ 'Aut' G ]") : subgroup_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) (B : {set T}) (f : T -> T).

Hypotheses (injf : {in B &, injective f}) (sBf : f @: B \subset B).

Lemma perm_in_inj : injective (fun x => if x \in B then f x else x).

Definition perm_in := perm perm_in_inj.

Lemma perm_in_on : perm_on B perm_in.

Lemma perm_inE : {in B, 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 : forall 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 : forall A, A \subset G -> aut @: A = f @* A.

Lemma preim_autE : forall A, A \subset G -> aut @^-1: A = f @*^-1 A.

End MakeAut.

Implicit Arguments morphim_fixP [gT G f].

conjugation automorphism 

Section ConjugationMorphism.

Variable gT : finGroupType.

Definition conjgm of {set gT} := fun x y : gT => y ^ x.

Lemma conjgmE : forall A x y, conjgm A x y = y ^ x. Qed.

Canonical Structure conjgm_morphism A x :=
  @Morphism _ _ A (conjgm A x) (in2W (fun y z => conjMg y z x)).

Lemma morphim_conj : forall A x B, conjgm A x @* B = (A :&: B) :^ x.

Variable G : {group gT}.

Lemma injm_conj : forall x, 'injm (conjgm G x).

Lemma norm_conj_dom : forall x, x \in 'N(G) -> conjgm G x @* G = G.

Definition conj_aut x :=
  aut (injm_conj _) (norm_conj_dom (valP (insigd (group1 _) x))).

Lemma norm_conj_autE : {in 'N(G) & G, forall x y, conj_aut x y = y ^ x}.

Lemma conj_autE : {in G &, forall x y, conj_aut x y = y ^ x}.

Lemma conj_aut_morphM : {in 'N(G) &, {morph conj_aut : x y / x * y}}.

Canonical Structure conj_aut_morphism := Morphism conj_aut_morphM.

Lemma ker_conj_aut : 'ker conj_aut = 'C(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) && (forallb f, (f \in Aut B) ==> (f @: A \subset A)).

Infix "\char" := characteristic.

Lemma charP : forall H G,
  reflect [/\ H \subset G & forall f : {morphism G >-> gT},
                            'injm f -> f @* G = G -> f @* H = H]
          (H \char G).

Characteristic subgroup properties : composition, relational properties 

Lemma trivg_char : forall G, 1 \char G.

Lemma char_refl : forall G, G \char G.

Lemma char_trans : forall H G K, K \char H -> H \char G -> K \char G.

Lemma char_norms : forall H G, H \char G -> 'N(G) \subset 'N(H).

Lemma char_sub : forall A B, A \char B -> A \subset B.

Lemma char_norm_trans : forall H G A,
  H \char G -> A \subset 'N(G) -> A \subset 'N(H).

Lemma char_normal_trans : forall H G K, K \char H -> H <| G -> K <| G.

Lemma char_normal : forall H G, H \char G -> H <| G.

Lemma char_norm : forall H G, H \char G -> G \subset 'N(H).

Lemma charI : forall G H K, H \char G -> K \char G -> H :&: K \char G.

Lemma charMgen : forall G H K, H \char G -> K \char G -> H <*> K \char G.

Lemma charM : forall G H K, H \char G -> K \char G -> H * K \char G.

Lemma lone_subgroup_char : forall G H,
  H \subset G -> (forall K, K \subset G -> K \isog H -> K \subset H) ->
  H \char G.

End Characteristicity.

Notation "H \char G" := (characteristic H G) : group_scope.