Library automorphism

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


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 : forall A a, a \in Aut A -> morphic A a.

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

Lemma eq_Aut : forall A, {in Aut A &, forall 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 : forall A a (AutAa : a \in Aut A), autm AutAa = a.

Canonical Structure 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 Structure 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 : forall 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 ]") : subgroup_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 : 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].

Section AutIsom.

Variables (gT rT : finGroupType) (G D : {group gT}) (f : {morphism D >-> rT}).

Hypotheses (injf : 'injm f) (sGD : G \subset D).

Lemma Aut_isom_subproof : forall 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 : forall a, Aut_isom a \in Aut (f @* G).

Lemma Aut_isomE : forall a,
   a \in Aut G -> {in G, forall x, Aut_isom a (f x) = f (a x)}.

Lemma Aut_isomM : {in Aut G &, {morph Aut_isom: x y / x * y}}.
Canonical Structure 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).

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 : forall A x y, conjgm A x y = y ^ x.

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 conj_isog : forall x, G :^ x \isog G.

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

Definition conj_aut x :=
  aut (injm_conj _) (im_conjgm_norm (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).

Lemma Aut_conj_aut : forall 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) && (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 char1 : 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.

Section InjmChar.

Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}).

Hypothesis injf : 'injm f.

Lemma injm_char : forall 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 : forall G H : {group aT},
  G \subset D -> H \subset D -> (f @* H \char f @* G) = (H \char G).

End CharInjm.