Library mathcomp.solvable.gfunctor
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ 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.
+ +
+
+
++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.
+
+
+
+
+ Subgroup closure.
+
+
+
+
+ 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).
+ +
+
+
++ ∀ 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.
+ +
+
+
++ ∀ 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.
+ +
+
+
++ ∀ 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 :=
+ ∀ gT (H G : {group gT}), H \subset G → F G :&: H \subset F H.
+ +
+Lemma pcontinuous_is_hereditary : pcontinuous → hereditary.
+ +
+
+
++ ∀ 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
+}.
+ +
+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 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 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_class) :
+ 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_class) (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.
+ +
+
++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
+}.
+ +
+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 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 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_class) :
+ 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_class) (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.
+ +
+