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.

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.