In FORMAT a formation is described by a function that computes GF for each (finite solvable) group G, and from that perspective F consists of the groups G for which GF is trivial. To define a formation that is not one of the standard examples provided (see below), one must give GAP an identifier for the formation and also some method for computing residual subgroups.
Some of the most interesting formations can also be described by ``local definition.'' For each prime p let F(p) be a formation or the empty class, and let F be the class of all finite solvable groups G such that for each prime p and each p-chief factor H/K of G the group of automorphisms that G induces on H/K by conjugation belongs to F(p). Then F is a formation, with local definition { F(p) mid p is prime }. The set { p mid p is prime and F(p) neq emptyset } is called the support of F. A p-chief factor is F-central in case G induces an F(p)-group on it or, equivalently, in case GF(p) centralizes it. It is possible to define a formation in FORMAT by giving such a local definition. Indeed one can define a kind of generalized formation by giving what is called a normal subgroup function or screen, which specifies arbitrary normal subgroups, not necessarily of form GF(p), to test ``centrality.'' Section Other Applications describes one such usage of general screens. Most applications of formation theory to solvable groups require local definition, as do the GAP functions for computing F-normalizers and F-covering subgroups.
The definition of a formation in FORMAT begins with the creation
of a record rec, which must contain a name component and
at least one of the components fResidual or fScreen. The
component name is a string, fResidual is a function that
computes a normal subgroup of each group, and fScreen is a function
of two variables, a group and a prime, that returns a normal subgroup of
the input group.
In the second form the function Formation can be used to obtain a formation from the supplied library of formations. The formations provided are:
IsFormation returns true if and only if F
is a GAP formation. NameOfFormation returns the name of a formation
and ResidualFunctionOfFormation returns the residual function
of a formation.
If F is locally defined by some screen {F(p)
| p is prime }, then HasScreenOfFormation( F
) is true, ScreenOfFormation( F )
is a function of two variables, group and prime, and the
command ScreenOfFormation( F )( G,
p ) returns GF(p) if p is
in the support of F and gives the empty list otherwise.
The attribute SupportOfFormation is optional. It may be
bound by
SetSupportOfFormation. If SupportOfFormation
is not bound, then the support of the formation is taken to be the set
of all primes. In case the support of
F is a finite set of primes,
then SupportOfFormation( F ) is a list of those
primes, and HasSupportOfFormation( F ) returns
true. In case the support of F is an infinite set but not the set
of all primes, then the user will need to make sure, perhaps with ChangedSupport
or
SetSupportOfFormation, that all primes dividing the orders
of relevant groups are considered.
This function may be used to change the support of a formation.
Let F be a formation and primes a list of primes. Then ChangedSupport
returns a formation with a new name whose support is the intersection of
the support of F and primes.
The local definition is called integrated in case F(p)
subseteq
F for each prime p.
The property IsIntegrated is also optional. It makes sense only
if HasScreenOfFormation( F ) is true.
Notice that some of the functions described below will require that HasScreenOfFormation(
F
), HasIsIntegrated( F ) and IsIntegrated(
F ) are true. If unbound, this property can
be bound with SetIsIntegrated, but it is up to the user to determine
whether such a setting is appropriate. Section Formation
Examples contains an example of such usage.
A local definition of a formation may always be replaced by an integrated
one without changing the formation itself, though the meaning of F-central
may change. Let F be a locally defined formation with name name.
If F is already integrated, then Integrated( F
) yields F itself. Otherwise, it yields a formation nameInt
that is abstractly the same as F but has integrated local definition.
Two formations F1 and F2 are considered to be equal
in case they have the same name. The natural ordering on strings gives
an ordering on formations. This ordering is useful for organizing key-dependent
lists but has no mathematical significance.
The intersection F := F1 cap F2 of two formations F1
and F2 is again a formation. Intersection produces the
new formation
(name1Andname2),
which has attribute ResidualFunctionOfFormation if either F1
or F2 does, has FScreen whenever both formations have it,
and is integrated if both are.
The product of two formations F1 and F2 is the formation
F such that a finite group G is a member of F if and
only if
GF2 is in F1. (Notice that the product
of F1 by F2 is not necessarily equal to the product of F2
by F1, and unless F1 is normal subgroup-closed the product
need not contain all extensions of a group in F1 by a group in F2.)
The function ProductOfFormations( F1, F2
) yields the product (name1Byname2)
of the two formations. The product has the attribute ResidualFunctionOfFormation
and has the attribute ScreenOfFormation whenever both F1
and F2 have this entry or whenever both HasScreenOfFormation(
F2 ) and not HasSupportOfFormation(
F1
) are true. In these cases the property IsIntegrated
will be inherited if possible.