Library mathcomp.fingroup.fingroup

Finite groups NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. This file defines the main interface for finite groups: finGroupType == the structure for finite types with a group law The HB class is called FinGroup. {group gT} == type of groups with elements of type gT finStarMonoidType == the structure for finite star-monoids The HB class is called FinStarMonoid. FinGroupType mulVg == the finGroupType structure for an existing finStarMonoidType structure, built from a proof of the left inverse group axiom for that structure's operations [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 finStarMonoidType 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. 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 finStarMonoidType, 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 = y^-1 * x^-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.

These are the operation notations introduced by this file.

Plucking a set representative.

We only assume a finStarMonoidType 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 finStarMonoidType. 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.