Library mathcomp.fingroup.fingroup

This file defines the main interface for finite groups : finGroupType == the structure for finite types with a group law. {group gT} == type of groups with elements of type gT. baseFinGroupType == the structure for finite types with a monoid law and an involutive antimorphism; finGroupType is derived from baseFinGroupType (via a telescope). FinGroupType mulVg == the finGroupType structure for an existing baseFinGroupType structure, built from a proof of the left inverse group axiom for that structure's operations. BaseFinGroupType bgm == the baseFingroupType structure built by packaging bgm : FinGroup.mixin_of T for a type T with an existing finType structure. FinGroup.BaseMixin mulA mul1x invK invM == the mixin for a baseFinGroupType structure, built from proofs of the baseFinGroupType axioms. FinGroup.Mixin mulA mul1x mulVg == the mixin for a baseFinGroupType structure, built from proofs of the group axioms. [baseFinGroupType of T] == a clone of an existing baseFinGroupType structure on T, for T (the existing structure might be for some delta-expansion of T). [finGroupType of T] == a clone of an existing finGroupType structure on T, for the canonical baseFinGroupType structure of T (the existing structure might be for the baseFinGroupType of some delta-expansion of T). [group of G] == a clone for an existing {group gT} structure on G : {set gT} (the existing structure might be for some delta-expansion of G). If gT implements finGroupType, then we can form {set gT}, the type of finite sets with elements of type gT (as finGroupType extends finType). The group law extends pointwise to {set gT}, which thus implements a sub- interface baseFinGroupType of finGroupType. To be consistent with the predType interface, this is done by coercion to FinGroup.arg_sort, an alias for FinGroup.sort. Accordingly, all pointwise group operations below have arguments of type (FinGroup.arg_sort) gT and return results of type FinGroup.sort gT. The notations below are declared in two scopes: group_scope (delimiter %g) for point operations and set constructs. Group_scope (delimiter %G) for explicit {group gT} structures. These scopes should not be opened globally, although group_scope is often opened locally in group-theory files (via Import GroupScope). As {group gT} is both a subtype and an interface structure for {set gT}, the fact that a given G : {set gT} is a group can (and usually should) be inferred by type inference with canonical structures. This means that all `group' constructions (e.g., the normaliser 'N_G(H)) actually define sets with a canonical {group gT} structure; the %G delimiter can be used to specify the actual {group gT} structure (e.g., 'N_G(H)%G). Operations on elements of a group: x * y == the group product of x and y. x ^+ n == the nth power of x, i.e., x * ... * x (n times). x^-1 == the group inverse of x. x ^- n == the inverse of x ^+ n (notation for (x ^+ n)^-1). 1 == the unit element. x ^ y == the conjugate of x by y (i.e., y^-1 * (x * y)). [~ x, y] == the commutator of x and y (i.e., x^-1 * x ^ y). [~ x1, ..., xn] == the commutator of x1, ..., xn (associating left). \prod(i ...) x i == the product of the x i (order-sensitive). commute x y <-> x and y commute. centralises x A <-> x centralises A. 'C[x] == the set of elements that commute with x. 'C_G[x] == the set of elements of G that commute with x. < [x]> == the cyclic subgroup generated by the element x. # [x] == the order of the element x, i.e., #|< [x]>|. Operations on subsets/subgroups of a finite group: H * G == {xy | x \in H, y \in G}. 1 or [1] or [1 gT] == the unit group. [set: gT]%G == the group of all x : gT (in Group_scope). group_set G == G contains 1 and is closed under binary product; this is the characteristic property of the {group gT} subtype of {set gT}. [subg G] == the subtype, set, or group of all x \in G: this notation is defined simultaneously in %type, %g and %G scopes, and G must denote a {group gT} structure (G is in the %G scope). subg, sgval == the projection into and injection from [subg G]. H^# == the set H minus the unit element. repr H == some element of H if 1 \notin H != set0, else 1. (repr is defined over sets of a baseFinGroupType, so it can be used, e.g., to pick right cosets.) x *: H == left coset of H by x. lcosets H G == the set of the left cosets of H by elements of G. H :* x == right coset of H by x. rcosets H G == the set of the right cosets of H by elements of G. #|G : H| == the index of H in G, i.e., #|rcosets G H|. H :^ x == the conjugate of H by x. x ^: H == the conjugate class of x in H. classes G == the set of all conjugate classes of G. G :^: H == {G :^ x | x \in H}. class_support G H == {x ^ y | x \in G, y \in H}. commg_set G H == { [~ x, y] | x \in G, y \in H}; NOT the commutator! H == the subgroup generated by the set H. [~: G, H] == the commmutator subgroup of G and H, i.e., commg_set G H>. [~: H1, ..., Hn] == commutator subgroup of H1, ..., Hn (left assoc.). H <*> G == the subgroup generated by sets H and G (H join G). (H * G)%G == the join of G H : {group gT} (convertible, but not identical to (G <*> H)%G). (\prod(i ...) H i)%G == the group generated by the H i. {in G, centralised H} <-> G centralises H. {in G, normalised H} <-> G normalises H. <-> forall x, x \in G -> H :^ x = H. 'N(H) == the normaliser of H. 'N_G(H) == the normaliser of H in G. H <| G <=> H is a normal subgroup of G. 'C(H) == the centraliser of H. 'C_G(H) == the centraliser of H in G. gcore H G == the largest subgroup of H normalised by G. If H is a subgroup of G, this is the largest normal subgroup of G contained in H). abelian H <=> H is abelian. subgroups G == the set of subgroups of G, i.e., the set of all H : {group gT} such that H \subset G. In the notation below G is a variable that is bound in P. [max G | P] <=> G is the largest group such that P holds. [max H of G | P] <=> H is the largest group G such that P holds. [max G | P & Q] := [max G | P && Q], likewise [max H of G | P & Q]. [min G | P] <=> G is the smallest group such that P holds. [min G | P & Q] := [min G | P && Q], likewise [min H of G | P & Q]. [min H of G | P] <=> H is the smallest group G such that P holds. In addition to the generic suffixes described in ssrbool.v and finset.v, we associate the following suffixes to group operations: 1 - identity element, as in group1 : 1 \in G. M - multiplication, as is invMg : (x * y)^-1 = x^-1 * y^-1. Also nat multiplication, for expgM : x ^+ (m * n) = x ^+ m ^+ n. D - (nat) addition, for expgD : x ^+ (m + n) = x ^+ m * x ^+ n. V - inverse, as in mulgV : x * x^-1 = 1. X - exponentiation, as in conjXg : (x ^+ n) ^ y = (x ^ y) ^+ n. J - conjugation, as in orderJ : # [x ^ y] = # [x]. R - commutator, as in conjRg : [~ x, y] ^ z = [~ x ^ z, y ^ z]. Y - join, as in centY : 'C(G <*> H) = 'C(G) :&: 'C(H). We sometimes prefix these with an `s' to indicate a set-lifted operation, e.g., conjsMg : (A * B) :^ x = A :^ x * B :^ x.

This module can be imported to open the scope for group element operations locally to a file, without exporting the Open to clients of that file (as Open would do).

These are the operation notations introduced by this file.

We split the group axiomatisation in two. We define a class of "base groups", which are basically monoids with an involutive antimorphism, from which we derive the class of groups proper. This allows use to reuse much of the group notation and algebraic axioms for group subsets, by defining a base group class on them. We use class/mixins here rather than telescopes to be able to interoperate with the type coercions. Another potential benefit (not exploited here) would be to define a class for infinite groups, which could share all of the algebraic laws.

We want to use sort as a coercion class, both to infer argument scopes properly, and to allow groups and cosets to coerce to the base group of group subsets. However, the return type of group operations should NOT be a coercion class, since this would trump the real (head-normal) coercion class for concrete group types, thus spoiling the coercion of A * B to pred_sort in x \in A * B, or rho * tau to ffun and Funclass in (rho * tau) x, when rho tau : perm T. Therefore we define an alias of sort for argument types, and make it the default coercion FinGroup.base_class >-> Sortclass so that arguments of a functions whose parameters are of type, say, gT : finGroupType, can be coerced to the coercion class of arg_sort. Care should be taken, however, to declare the return type of functions and operators as FinGroup.sort gT rather than gT, e.g., mulg : gT -> gT -> FinGroup.sort gT. Note that since we do this here and in quotient.v for all the basic functions, the inferred return type should generally be correct.

We only need three axioms to make a true group.

Declaring sort as a Coercion is clearly redundant; it only serves the purpose of eliding FinGroup.sort in the display of return types. The warning could be eliminated by using the functor trick to replace Sortclass by a dummy target.

Arguments of conjg are restricted to true groups to avoid an improper interpretation of A ^ B with A and B sets, namely: {x^-1 * (y * z) | y \in A, x, z \in B}

Other commg identities should slot in here.

Plucking a set representative.

We only assume a baseFinGroupType to allow this construct to be iterated.

Set-lifted group operations.

The pre-group structure of group subsets.

Time to open the bag of dirty tricks. When we define groups down below as a subtype of {set gT}, we need them to be able to coerce to sets in both set-style contexts (x \in G) and monoid-style contexts (G * H), and we need the coercion function to be EXACTLY the structure projection in BOTH cases -- otherwise the canonical unification breaks. Alas, Coq doesn't let us use the same coercion function twice, even when the targets are convertible. Our workaround (ab)uses the module system to declare two different identity coercions on an alias class.

Some of these constructs could be defined on a baseFinGroupType. We restrict them to proper finGroupType because we only develop the theory for that case.

These will only be used later, but are defined here so that we can keep all the Notation together.

"normalised" and "centralise[s|d]" are intended to be used with the {in ...} form, as in abelian below.

No notation for lcoset and rcoset, which are to be used mostly in curried form; x *: B and A :* 1 denote singleton products, so we can use mulgA, mulg1, etc, on, say, A :* 1 * B :* x. No notation for the set commutator generator set commg_set.

Properties of the purely multiplicative structure.

Set product. We already have all the pregroup identities, so we only need to add the monotonicity rules.

Set (pointwise) inverse.

Product with singletons.

Constructs that need a finGroupType

Left cosets.

Right cosets.

Inverse maps lcosets to rcosets

Conjugates.

Classes; not much for now.

Conjugate set.

Class support.

Groups (at last!)