Library mathcomp.solvable.gfunctor

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.

Group closure.

Subgroup closure.

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

Functoriality on the Grp groupoid (arrows are restricted to isos).

Functoriality on Grp with partial morphisms.

Heredity with respect to inclusion

Monotonicity with respect to inclusion

Self-expanding composition, and modulo