- -

Library mathcomp.solvable.gfunctor

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

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

-Definition 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 -

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