# Library gfunctor

Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop finset.

Require Import fingroup morphism automorphism quotient gproduct.

Require Import fingroup morphism automorphism 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. 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.

Delimit Scope gFun_scope with gF.

Module GFunctor.

Definition object_map := forall gT : finGroupType, {set gT} -> {set gT}.

Section Definitions.

Implicit Types gT hT : finGroupType.

Variable F : object_map.

Group closure.

Subgroup closure.

General functoriality, i.e., continuity of the object map

Definition continuous :=

forall gT hT (G : {group gT}) (phi : {morphism G >-> hT}),

phi @* F G \subset F (phi @* G).

forall 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 :=

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

forall 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 :=

forall gT hT (G D : {group gT}) (phi : {morphism D >-> hT}),

phi @* F G \subset F (phi @* G).

Lemma pcontinuous_is_continuous : pcontinuous -> continuous.

forall 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

Definition hereditary :=

forall gT (H G : {group gT}), H \subset G -> F G :&: H \subset F H.

Lemma pcontinuous_is_hereditary : pcontinuous -> hereditary.

forall gT (H G : {group gT}), H \subset G -> F G :&: H \subset F H.

Lemma pcontinuous_is_hereditary : pcontinuous -> hereditary.

Monotonicity with respect to inclusion

Self-expanding composition, and modulo

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

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

Definition modulo : object_map :=

fun gT A => coset (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

}.

Local Coercion apply : iso_map >-> object_map.

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

Local Coercion iso_of_map : map >-> iso_map.

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

Local Coercion map_of_pmap : pmap >-> map.

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

Local Coercion map_of_mono : mono_map >-> map.

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 isoF0 => isoF.

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 funF => funF.

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 pfunF => pfunF.

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 mfunF => mfunF.

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 G => groupP _) Fsub)

(at level 0, format "[ 'igFun' 'by' Fsub & Fcont ]") : form_scope.

Notation "[ 'igFun' 'by' Fsub & ! Fcont ]" :=

(pack_iso Fcont (fun gT G => groupP _) 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 Structure gFgroup := Group gFgroupset.

End FunctorGroup.

Canonical Structure 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 : forall gT (G : {group gT}), F gT G \subset G.

Lemma gFiso_cont : GFunctor.iso_continuous F.

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

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

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

Lemma injmF_sub : forall 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 : forall 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 :

forall gT rT (G D : {group gT}) (R : {group rT}) (f : {morphism D >-> rT}),

G \subset D -> isom G R f -> isom (F gT G) (F rT R) f.

Lemma gFisog : forall 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 : forall 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 : forall gT (G H : {group gT}),

F gT G :&: H = F gT G :&: F gT (G :&: H).

Lemma pmorphimF : GFunctor.pcontinuous F.

Lemma gFid : forall 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 Structure gFmod_igFun := [igFun by gFmod_closed & gFmod_cont].

Canonical Structure gFmod_gFun := [gFun by gFmod_cont].

End Modulo.

Variables F1 F2 : GFunctor.pmap.

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

Canonical Structure gFmod_pgFun := [pgFun by gFmod_hereditary].

End PartialFunctorTheory.

Section MonotonicFunctorTheory.

Implicit Types gT rT : finGroupType.

Lemma gFunctorS : forall 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 Structure gFcomp_igFun := [igFun by gFcomp_closed & gFcomp_cont].

Canonical Structure gFcomp_gFun :=[gFun by gFcomp_cont].

End Composition.

Variables F1 F2 : GFunctor.mono_map.

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

Canonical Structure 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 Structure bgFunc_id := [igFun by idGfun_closed & idGfun_cont].

Canonical Structure gFunc_id := [gFun by idGfun_cont].

Canonical Structure mgFunc_id := [mgFun by idGfun_monotonic].

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

Lemma trivGfun_cont : GFunctor.pcontinuous trivGfun.

Canonical Structure trivGfun_igFun := [igFun by sub1G & trivGfun_cont].

Canonical Structure trivGfun_gFun := [gFun by trivGfun_cont].

Canonical Structure trivGfun_pgFun := [pgFun by trivGfun_cont].

End GFunctorExamples.