Library mathcomp.solvable.gfunctor

(* (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 bigop finset fingroup morphism automorphism.
From mathcomp Require Import quotient gproduct.

This file provides basic interfaces for the notion of "generic" characteristic subgroups; these amount to subfunctors of the identity functor in some category of groups. See "Generic Proof Tools And Finite Group Theory", Francois Garillot, PhD, 2011, Chapter 3. The implementation proposed here is fairly basic, relying on first order function matching and on structure telescopes, both of which are somewhat limited and fragile. It should switch in the future to more general and more robust quotation matching. The definitions in this file (types, properties and structures) are all packaged under the GFunctor submodule, i.e., client code should refer to GFunctor.continuous, GFunctor.map, etc. Notations, Coercions and Lemmas are exported and thus directly available, however. We provide the following: object_map == the type of the (polymorphic) object map of a group functor; the %gF scope is bound to object_map. := forall gT : finGroupType, {set gT} -> {set gT}. We define two operations on object_map (with notations in the %gF scope): F1 \o F2 == the composite map; (F1 \o F2) G expands to F1 (F2 G). F1 %% F2 == F1 computed modulo F2; we have (F1 %% F2) G / F2 G = F1 (G / F2 G) We define the following (type-polymorphic) properties of an object_map F: group_valued F <-> F G is a group when G is a group closed F <-> F G is a subgroup o fG when G is a group continuous F <-> F is continuous with respect to morphism image: for any f : {morphism G >-> ..}, f @* (F G) is a a subgroup of F (f @* G); equivalently, F is functorial in the category Grp of groups. Most common "characteristic subgroup" are produced continuous object maps. iso_continuous F <-> F is continuous with respect to isomorphism image; equivalently, F is functorial in the Grp groupoid. The Puig and the Thompson J subgroups are examples of iso_continuous maps that are not continuous. pcontinuous F <-> F is continuous with respect to partial morphism image, i.e., functorial in the category of groups and partial morphisms. The center and p-core are examples of pcontinuous maps. hereditary F <-> inclusion in the image of F is hereditary, i.e., for any subgroup H of G, the intersection of H with F G is included in H. Note that F is pcontinuous iff it is continuous and hereditary; indeed proofs of pcontinuous F coerce to proofs of hereditary F and continuous F. monotonic F <-> F is monotonic with respect to inclusion: for any subgroup H of G, F H is a subgroup of F G. The derived and lower central series are examples of monotonic maps. Four structures provide interfaces to these properties: GFunctor.iso_map == structure for object maps that are group_valued, closed, and iso_continuous. [igFun by Fsub & !Fcont] == the iso_map structure for an object map F such that F G is canonically a group when G is, and given Fsub : closed F and Fcont : iso_continuous F. [igFun by Fsub & Fcont] == as above, but expecting Fcont : continuous F. [igFun of F] == clone an existing GFunctor.iso_map structure for F. GFunctor.map == structure for continuous object maps, inheriting from the GFunctor.iso_map structure. [gFun by Fcont] == the map structure for an F with a canonical iso_map structure, given Fcont : continuous F. [gFun of F] == clone an existing GFunctor.map structure for F. GFunctor.pmap == structure for pcontinuous object maps, inheriting from the GFunctor.map structure. [pgFun by Fher] == the pmap structure for an F with a canonical map structure, given Fher : hereditary F. [pgFun of F] == clone an existing GFunctor.pmap structure for F. GFunctor.mono_map == structure for monotonic, continuous object maps inheriting from the GFunctor.map structure. [mgFun by Fmon] == the mono_map structure for an F with a canonical map structure, given Fmon : monotonic F. [mgFun of F] == clone an existing GFunctor.mono_map structure for F Lemmas for these group functors use either a 'gF' prefix or an 'F' suffix. The (F1 \o F2) and (F1 %% F2) operations have canonical GFunctor.map structures when F1 is monotonic or hereditary, respectively.

Import GroupScope.

Set Implicit Arguments.

Delimit Scope gFun_scope with gF.

Module GFunctor.

Definition object_map := gT : finGroupType, {set gT} {set gT}.


Section Definitions.

Implicit Types gT hT : finGroupType.

Variable F : object_map.

Group closure.
Definition group_valued := gT (G : {group gT}), group_set (F G).

Subgroup closure.
Definition closed := gT (G : {group gT}), F G \subset G.

General functoriality, i.e., continuity of the object map
Definition continuous :=
   gT hT (G : {group gT}) (phi : {morphism G >-> hT}),
    phi @* F G \subset F (phi @* G).

Functoriality on the Grp groupoid (arrows are restricted to isos).
Definition iso_continuous :=
   gT hT (G : {group gT}) (phi : {morphism G >-> hT}),
   'injm phi phi @* F G \subset F (phi @* G).

Lemma continuous_is_iso_continuous : continuous iso_continuous.

Functoriality on Grp with partial morphisms.
Definition pcontinuous :=
   gT hT (G D : {group gT}) (phi : {morphism D >-> hT}),
    phi @* F G \subset F (phi @* G).

Lemma pcontinuous_is_continuous : pcontinuous continuous.

Heredity with respect to inclusion
Monotonicity with respect to inclusion
Definition monotonic :=
   gT (H G : {group gT}), H \subset G F H \subset F G.

Self-expanding composition, and modulo

Variables (k : unit) (F1 F2 : object_map).

Definition comp_head : object_map := fun gT Alet: tt := k in F1 (F2 A).

Definition modulo : object_map :=
  fun gT Acoset (F2 A) @*^-1 (F1 (A / (F2 A))).

End Definitions.

Section ClassDefinitions.

Structure iso_map := IsoMap {
  apply : object_map;
  _ : group_valued apply;
  _ : closed apply;
  _ : iso_continuous apply
}.

Structure map := Map { iso_of_map : iso_map; _ : continuous iso_of_map }.

Structure pmap := Pmap { map_of_pmap : map; _ : hereditary map_of_pmap }.

Structure mono_map := MonoMap { map_of_mono : map; _ : monotonic map_of_mono }.

Definition pack_iso F Fcont Fgrp Fsub := @IsoMap F Fgrp Fsub Fcont.

Definition clone_iso (F : object_map) :=
  fun Fgrp Fsub Fcont (isoF := @IsoMap F Fgrp Fsub Fcont) ⇒
  fun isoF0 & phant_id (apply isoF0) F & phant_id isoF isoF0isoF.

Definition clone (F : object_map) :=
  fun isoF & phant_id (apply isoF) F
  fun (funF0 : map) & phant_id (apply funF0) F
  fun Fcont (funF := @Map isoF Fcont) & phant_id funF0 funFfunF.

Definition clone_pmap (F : object_map) :=
  fun (funF : map) & phant_id (apply funF) F
  fun (pfunF0 : pmap) & phant_id (apply pfunF0) F
  fun Fher (pfunF := @Pmap funF Fher) & phant_id pfunF0 pfunFpfunF.

Definition clone_mono (F : object_map) :=
  fun (funF : map) & phant_id (apply funF) F
  fun (mfunF0 : mono_map) & phant_id (apply mfunF0) F
  fun Fmon (mfunF := @MonoMap funF Fmon) & phant_id mfunF0 mfunFmfunF.

End ClassDefinitions.

Module Exports.

Identity Coercion fun_of_object_map : object_map >-> Funclass.
Coercion apply : iso_map >-> object_map.
Coercion iso_of_map : map >-> iso_map.
Coercion map_of_pmap : pmap >-> map.
Coercion map_of_mono : mono_map >-> map.
Coercion continuous_is_iso_continuous : continuous >-> iso_continuous.
Coercion pcontinuous_is_continuous : pcontinuous >-> continuous.
Coercion pcontinuous_is_hereditary : pcontinuous >-> hereditary.

Notation "[ 'igFun' 'by' Fsub & Fcont ]" :=
    (pack_iso (continuous_is_iso_continuous Fcont) (fun gT GgroupP _) Fsub)
  (at level 0, format "[ 'igFun' 'by' Fsub & Fcont ]") : form_scope.

Notation "[ 'igFun' 'by' Fsub & ! Fcont ]" :=
    (pack_iso Fcont (fun gT GgroupP _) Fsub)
  (at level 0, format "[ 'igFun' 'by' Fsub & ! Fcont ]") : form_scope.

Notation "[ 'igFun' 'of' F ]" := (@clone_iso F _ _ _ _ id id)
  (at level 0, format "[ 'igFun' 'of' F ]") : form_scope.

Notation "[ 'gFun' 'by' Fcont ]" := (Map Fcont)
  (at level 0, format "[ 'gFun' 'by' Fcont ]") : form_scope.

Notation "[ 'gFun' 'of' F ]" := (@clone F _ id _ id _ id)
  (at level 0, format "[ 'gFun' 'of' F ]") : form_scope.

Notation "[ 'pgFun' 'by' Fher ]" := (Pmap Fher)
  (at level 0, format "[ 'pgFun' 'by' Fher ]") : form_scope.

Notation "[ 'pgFun' 'of' F ]" := (@clone_pmap F _ id _ id _ id)
  (at level 0, format "[ 'pgFun' 'of' F ]") : form_scope.

Notation "[ 'mgFun' 'by' Fmon ]" := (MonoMap Fmon)
  (at level 0, format "[ 'mgFun' 'by' Fmon ]") : form_scope.

Notation "[ 'mgFun' 'of' F ]" := (@clone_mono F _ id _ id _ id)
  (at level 0, format "[ 'mgFun' 'of' F ]") : form_scope.

End Exports.

End GFunctor.
Export GFunctor.Exports.


Notation "F1 \o F2" := (GFunctor.comp_head tt F1 F2) : gFun_scope.
Notation "F1 %% F2" := (GFunctor.modulo F1 F2) : gFun_scope.

Section FunctorGroup.

Variables (F : GFunctor.iso_map) (gT : finGroupType) (G : {group gT}).
Lemma gFgroupset : group_set (F gT G).
Canonical gFgroup := Group gFgroupset.

End FunctorGroup.

Canonical gFmod_group
    (F1 : GFunctor.iso_map) (F2 : GFunctor.object_map)
    (gT : finGroupType) (G : {group gT}) :=
  [group of (F1 %% F2)%gF gT G].

Section IsoFunctorTheory.

Implicit Types gT rT : finGroupType.
Variable F : GFunctor.iso_map.

Lemma gFsub gT (G : {group gT}) : F gT G \subset G.

Lemma gFsub_trans gT (G : {group gT}) (A : {pred gT}) :
  G \subset A F gT G \subset A.

Lemma gF1 gT : F gT 1 = 1.

Lemma gFiso_cont : GFunctor.iso_continuous F.

Lemma gFchar gT (G : {group gT}) : F gT G \char G.

Lemma gFnorm gT (G : {group gT}) : G \subset 'N(F gT G).

Lemma gFnorms gT (G : {group gT}) : 'N(G) \subset 'N(F gT G).

Lemma gFnormal gT (G : {group gT}) : F gT G <| G.

Lemma gFchar_trans gT (G H : {group gT}) : H \char G F gT H \char G.

Lemma gFnormal_trans gT (G H : {group gT}) : H <| G F gT H <| G.

Lemma gFnorm_trans gT (A : {pred gT}) (G : {group gT}) :
  A \subset 'N(G) A \subset 'N(F gT G).

Lemma injmF_sub gT rT (G D : {group gT}) (f : {morphism D >-> rT}) :
  'injm f G \subset D f @* (F gT G) \subset F rT (f @* G).

Lemma injmF gT rT (G D : {group gT}) (f : {morphism D >-> rT}) :
  'injm f G \subset D f @* (F gT G) = F rT (f @* G).

Lemma gFisom gT rT (G D : {group gT}) R (f : {morphism D >-> rT}) :
  G \subset D isom G (gval R) f isom (F gT G) (F rT R) f.

Lemma gFisog gT rT (G : {group gT}) (R : {group rT}) :
  G \isog R F gT G \isog F rT R.

End IsoFunctorTheory.

Section FunctorTheory.

Implicit Types gT rT : finGroupType.
Variable F : GFunctor.map.

Lemma gFcont : GFunctor.continuous F.

Lemma morphimF gT rT (G D : {group gT}) (f : {morphism D >-> rT}) :
  G \subset D f @* (F gT G) \subset F rT (f @* G).

End FunctorTheory.

Section PartialFunctorTheory.

Implicit Types gT rT : finGroupType.

Section BasicTheory.

Variable F : GFunctor.pmap.

Lemma gFhereditary : GFunctor.hereditary F.

Lemma gFunctorI gT (G H : {group gT}) :
  F gT G :&: H = F gT G :&: F gT (G :&: H).

Lemma pmorphimF : GFunctor.pcontinuous F.

Lemma gFid gT (G : {group gT}) : F gT (F gT G) = F gT G.

End BasicTheory.

Section Modulo.

Variables (F1 : GFunctor.pmap) (F2 : GFunctor.map).

Lemma gFmod_closed : GFunctor.closed (F1 %% F2).

Lemma gFmod_cont : GFunctor.continuous (F1 %% F2).

Canonical gFmod_igFun := [igFun by gFmod_closed & gFmod_cont].
Canonical gFmod_gFun := [gFun by gFmod_cont].

End Modulo.

Variables F1 F2 : GFunctor.pmap.

Lemma gFmod_hereditary : GFunctor.hereditary (F1 %% F2).

Canonical gFmod_pgFun := [pgFun by gFmod_hereditary].

End PartialFunctorTheory.

Section MonotonicFunctorTheory.

Implicit Types gT rT : finGroupType.

Lemma gFunctorS (F : GFunctor.mono_map) : GFunctor.monotonic F.

Section Composition.

Variables (F1 : GFunctor.mono_map) (F2 : GFunctor.map).

Lemma gFcomp_closed : GFunctor.closed (F1 \o F2).

Lemma gFcomp_cont : GFunctor.continuous (F1 \o F2).

Canonical gFcomp_igFun := [igFun by gFcomp_closed & gFcomp_cont].
Canonical gFcomp_gFun :=[gFun by gFcomp_cont].

End Composition.

Variables F1 F2 : GFunctor.mono_map.

Lemma gFcompS : GFunctor.monotonic (F1 \o F2).

Canonical gFcomp_mgFun := [mgFun by gFcompS].

End MonotonicFunctorTheory.

Section GFunctorExamples.

Implicit Types gT : finGroupType.

Definition idGfun gT := @id {set gT}.

Lemma idGfun_closed : GFunctor.closed idGfun.
Lemma idGfun_cont : GFunctor.continuous idGfun.
Lemma idGfun_monotonic : GFunctor.monotonic idGfun.

Canonical bgFunc_id := [igFun by idGfun_closed & idGfun_cont].
Canonical gFunc_id := [gFun by idGfun_cont].
Canonical mgFunc_id := [mgFun by idGfun_monotonic].

Definition trivGfun gT of {set gT} := [1 gT].

Lemma trivGfun_cont : GFunctor.pcontinuous trivGfun.

Canonical trivGfun_igFun := [igFun by sub1G & trivGfun_cont].
Canonical trivGfun_gFun := [gFun by trivGfun_cont].
Canonical trivGfun_pgFun := [pgFun by trivGfun_cont].

End GFunctorExamples.