Library mathcomp.fingroup.fingroup
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import fintype div path tuple bigop prime finset.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import fintype div path tuple bigop prime finset.
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 = 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.
Set Implicit Arguments.
Delimit Scope group_scope with g.
Delimit Scope Group_scope with G.
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.
Reserved Notation "[ ~ x1 , x2 , .. , xn ]" (at level 0,
format "'[ ' [ ~ x1 , '/' x2 , '/' .. , '/' xn ] ']'").
Reserved Notation "[ 1 gT ]" (at level 0, format "[ 1 gT ]").
Reserved Notation "[ 1 ]" (at level 0, format "[ 1 ]").
Reserved Notation "[ 'subg' G ]" (at level 0, format "[ 'subg' G ]").
Reserved Notation "A ^#" (at level 2, format "A ^#").
Reserved Notation "A :^ x" (at level 35, right associativity).
Reserved Notation "x ^: B" (at level 35, right associativity).
Reserved Notation "A :^: B" (at level 35, right associativity).
Reserved Notation "#| B : A |" (at level 0, B, A at level 99,
format "#| B : A |").
Reserved Notation "''N' ( A )" (at level 8, format "''N' ( A )").
Reserved Notation "''N_' G ( A )" (at level 8, G at level 2,
format "''N_' G ( A )").
Reserved Notation "A <| B" (at level 70, no associativity).
Reserved Notation "A <*> B" (at level 40, left associativity).
Reserved Notation "[ ~: A1 , A2 , .. , An ]" (at level 0,
format "[ ~: '[' A1 , '/' A2 , '/' .. , '/' An ']' ]").
Reserved Notation "[ 'max' A 'of' G | gP ]" (at level 0,
format "[ '[hv' 'max' A 'of' G '/ ' | gP ']' ]").
Reserved Notation "[ 'max' G | gP ]" (at level 0,
format "[ '[hv' 'max' G '/ ' | gP ']' ]").
Reserved Notation "[ 'max' A 'of' G | gP & gQ ]" (at level 0,
format "[ '[hv' 'max' A 'of' G '/ ' | gP '/ ' & gQ ']' ]").
Reserved Notation "[ 'max' G | gP & gQ ]" (at level 0,
format "[ '[hv' 'max' G '/ ' | gP '/ ' & gQ ']' ]").
Reserved Notation "[ 'min' A 'of' G | gP ]" (at level 0,
format "[ '[hv' 'min' A 'of' G '/ ' | gP ']' ]").
Reserved Notation "[ 'min' G | gP ]" (at level 0,
format "[ '[hv' 'min' G '/ ' | gP ']' ]").
Reserved Notation "[ 'min' A 'of' G | gP & gQ ]" (at level 0,
format "[ '[hv' 'min' A 'of' G '/ ' | gP '/ ' & gQ ']' ]").
Reserved Notation "[ 'min' G | gP & gQ ]" (at level 0,
format "[ '[hv' 'min' G '/ ' | gP '/ ' & gQ ']' ]").
Module FinGroup.
format "'[ ' [ ~ x1 , '/' x2 , '/' .. , '/' xn ] ']'").
Reserved Notation "[ 1 gT ]" (at level 0, format "[ 1 gT ]").
Reserved Notation "[ 1 ]" (at level 0, format "[ 1 ]").
Reserved Notation "[ 'subg' G ]" (at level 0, format "[ 'subg' G ]").
Reserved Notation "A ^#" (at level 2, format "A ^#").
Reserved Notation "A :^ x" (at level 35, right associativity).
Reserved Notation "x ^: B" (at level 35, right associativity).
Reserved Notation "A :^: B" (at level 35, right associativity).
Reserved Notation "#| B : A |" (at level 0, B, A at level 99,
format "#| B : A |").
Reserved Notation "''N' ( A )" (at level 8, format "''N' ( A )").
Reserved Notation "''N_' G ( A )" (at level 8, G at level 2,
format "''N_' G ( A )").
Reserved Notation "A <| B" (at level 70, no associativity).
Reserved Notation "A <*> B" (at level 40, left associativity).
Reserved Notation "[ ~: A1 , A2 , .. , An ]" (at level 0,
format "[ ~: '[' A1 , '/' A2 , '/' .. , '/' An ']' ]").
Reserved Notation "[ 'max' A 'of' G | gP ]" (at level 0,
format "[ '[hv' 'max' A 'of' G '/ ' | gP ']' ]").
Reserved Notation "[ 'max' G | gP ]" (at level 0,
format "[ '[hv' 'max' G '/ ' | gP ']' ]").
Reserved Notation "[ 'max' A 'of' G | gP & gQ ]" (at level 0,
format "[ '[hv' 'max' A 'of' G '/ ' | gP '/ ' & gQ ']' ]").
Reserved Notation "[ 'max' G | gP & gQ ]" (at level 0,
format "[ '[hv' 'max' G '/ ' | gP '/ ' & gQ ']' ]").
Reserved Notation "[ 'min' A 'of' G | gP ]" (at level 0,
format "[ '[hv' 'min' A 'of' G '/ ' | gP ']' ]").
Reserved Notation "[ 'min' G | gP ]" (at level 0,
format "[ '[hv' 'min' G '/ ' | gP ']' ]").
Reserved Notation "[ 'min' A 'of' G | gP & gQ ]" (at level 0,
format "[ '[hv' 'min' A 'of' G '/ ' | gP '/ ' & gQ ']' ]").
Reserved Notation "[ 'min' G | gP & gQ ]" (at level 0,
format "[ '[hv' 'min' G '/ ' | gP '/ ' & gQ ']' ]").
Module FinGroup.
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.
Record mixin_of (T : Type) : Type := BaseMixin {
mul : T → T → T;
one : T;
inv : T → T;
_ : associative mul;
_ : left_id one mul;
_ : involutive inv;
_ : {morph inv : x y / mul x y >-> mul y x}
}.
Structure base_type : Type := PackBase {
sort : Type;
_ : mixin_of sort;
_ : Finite.class_of sort
}.
mul : T → T → T;
one : T;
inv : T → T;
_ : associative mul;
_ : left_id one mul;
_ : involutive inv;
_ : {morph inv : x y / mul x y >-> mul y x}
}.
Structure base_type : Type := PackBase {
sort : Type;
_ : mixin_of sort;
_ : Finite.class_of sort
}.
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_type >-> 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.
Definition arg_sort := sort.
Definition mixin T :=
let: PackBase _ m _ := T return mixin_of (sort T) in m.
Definition finClass T :=
let: PackBase _ _ m := T return Finite.class_of (sort T) in m.
Structure type : Type := Pack {
base : base_type;
_ : left_inverse (one (mixin base)) (inv (mixin base)) (mul (mixin base))
}.
Definition mixin T :=
let: PackBase _ m _ := T return mixin_of (sort T) in m.
Definition finClass T :=
let: PackBase _ _ m := T return Finite.class_of (sort T) in m.
Structure type : Type := Pack {
base : base_type;
_ : left_inverse (one (mixin base)) (inv (mixin base)) (mul (mixin base))
}.
We only need three axioms to make a true group.
Section Mixin.
Variables (T : Type) (one : T) (mul : T → T → T) (inv : T → T).
Hypothesis mulA : associative mul.
Hypothesis mul1 : left_id one mul.
Hypothesis mulV : left_inverse one inv mul.
Notation "1" := one.
Infix "×" := mul.
Notation "x ^-1" := (inv x).
Lemma mk_invgK : involutive inv.
Lemma mk_invMg : {morph inv : x y / x × y >-> y × x}.
Definition Mixin := BaseMixin mulA mul1 mk_invgK mk_invMg.
End Mixin.
Definition pack_base T m :=
fun c cT & phant_id (Finite.class cT) c ⇒ @PackBase T m c.
Definition clone_base T :=
fun bT & sort bT → T ⇒
fun m c (bT' := @PackBase T m c) & phant_id bT' bT ⇒ bT'.
Definition clone T :=
fun bT gT & sort bT × sort (base gT) → T × T ⇒
fun m (gT' := @Pack bT m) & phant_id gT' gT ⇒ gT'.
Section InheritedClasses.
Variable bT : base_type.
Canonical eqType := Equality.Pack class.
Canonical choiceType := Choice.Pack class.
Canonical countType := Countable.Pack class.
Canonical finType := Finite.Pack class.
Definition arg_eqType := Eval hnf in [eqType of T].
Definition arg_choiceType := Eval hnf in [choiceType of T].
Definition arg_countType := Eval hnf in [countType of T].
Definition arg_finType := Eval hnf in [finType of T].
End InheritedClasses.
Module Import Exports.
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.
Coercion arg_sort : base_type >-> Sortclass.
Coercion sort : base_type >-> Sortclass.
Coercion mixin : base_type >-> mixin_of.
Coercion base : type >-> base_type.
Canonical eqType.
Canonical choiceType.
Canonical countType.
Canonical finType.
Coercion arg_eqType : base_type >-> Equality.type.
Canonical arg_eqType.
Coercion arg_choiceType : base_type >-> Choice.type.
Canonical arg_choiceType.
Coercion arg_countType : base_type >-> Countable.type.
Canonical arg_countType.
Coercion arg_finType : base_type >-> Finite.type.
Canonical arg_finType.
Notation baseFinGroupType := base_type.
Notation finGroupType := type.
Notation BaseFinGroupType T m := (@pack_base T m _ _ id).
Notation FinGroupType := Pack.
Notation "[ 'baseFinGroupType' 'of' T ]" := (@clone_base T _ id _ _ id)
(at level 0, format "[ 'baseFinGroupType' 'of' T ]") : form_scope.
Notation "[ 'finGroupType' 'of' T ]" := (@clone T _ _ id _ id)
(at level 0, format "[ 'finGroupType' 'of' T ]") : form_scope.
End Exports.
End FinGroup.
Export FinGroup.Exports.
Section ElementOps.
Variable T : baseFinGroupType.
Notation rT := (FinGroup.sort T).
Definition oneg : rT := FinGroup.one T.
Definition mulg : T → T → rT := FinGroup.mul T.
Definition invg : T → rT := FinGroup.inv T.
Definition expgn_rec (x : T) n : rT := iterop n mulg x oneg.
End ElementOps.
Definition expgn := nosimpl expgn_rec.
Notation "1" := (oneg _) : group_scope.
Notation "x1 * x2" := (mulg x1 x2) : group_scope.
Notation "x ^-1" := (invg x) : group_scope.
Notation "x ^+ n" := (expgn x n) : group_scope.
Notation "x ^- n" := (x ^+ n)^-1 : group_scope.
Coercion sort : base_type >-> Sortclass.
Coercion mixin : base_type >-> mixin_of.
Coercion base : type >-> base_type.
Canonical eqType.
Canonical choiceType.
Canonical countType.
Canonical finType.
Coercion arg_eqType : base_type >-> Equality.type.
Canonical arg_eqType.
Coercion arg_choiceType : base_type >-> Choice.type.
Canonical arg_choiceType.
Coercion arg_countType : base_type >-> Countable.type.
Canonical arg_countType.
Coercion arg_finType : base_type >-> Finite.type.
Canonical arg_finType.
Notation baseFinGroupType := base_type.
Notation finGroupType := type.
Notation BaseFinGroupType T m := (@pack_base T m _ _ id).
Notation FinGroupType := Pack.
Notation "[ 'baseFinGroupType' 'of' T ]" := (@clone_base T _ id _ _ id)
(at level 0, format "[ 'baseFinGroupType' 'of' T ]") : form_scope.
Notation "[ 'finGroupType' 'of' T ]" := (@clone T _ _ id _ id)
(at level 0, format "[ 'finGroupType' 'of' T ]") : form_scope.
End Exports.
End FinGroup.
Export FinGroup.Exports.
Section ElementOps.
Variable T : baseFinGroupType.
Notation rT := (FinGroup.sort T).
Definition oneg : rT := FinGroup.one T.
Definition mulg : T → T → rT := FinGroup.mul T.
Definition invg : T → rT := FinGroup.inv T.
Definition expgn_rec (x : T) n : rT := iterop n mulg x oneg.
End ElementOps.
Definition expgn := nosimpl expgn_rec.
Notation "1" := (oneg _) : group_scope.
Notation "x1 * x2" := (mulg x1 x2) : group_scope.
Notation "x ^-1" := (invg x) : group_scope.
Notation "x ^+ n" := (expgn x n) : group_scope.
Notation "x ^- n" := (x ^+ n)^-1 : group_scope.
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}
Definition conjg (T : finGroupType) (x y : T) := y^-1 × (x × y).
Notation "x1 ^ x2" := (conjg x1 x2) : group_scope.
Definition commg (T : finGroupType) (x y : T) := x^-1 × x ^ y.
Notation "[ ~ x1 , x2 , .. , xn ]" := (commg .. (commg x1 x2) .. xn)
: group_scope.
Notation "\prod_ ( i <- r | P ) F" :=
(\big[mulg/1]_(i <- r | P%B) F%g) : group_scope.
Notation "\prod_ ( i <- r ) F" :=
(\big[mulg/1]_(i <- r) F%g) : group_scope.
Notation "\prod_ ( m <= i < n | P ) F" :=
(\big[mulg/1]_(m ≤ i < n | P%B) F%g) : group_scope.
Notation "\prod_ ( m <= i < n ) F" :=
(\big[mulg/1]_(m ≤ i < n) F%g) : group_scope.
Notation "\prod_ ( i | P ) F" :=
(\big[mulg/1]_(i | P%B) F%g) : group_scope.
Notation "\prod_ i F" :=
(\big[mulg/1]_i F%g) : group_scope.
Notation "\prod_ ( i : t | P ) F" :=
(\big[mulg/1]_(i : t | P%B) F%g) (only parsing) : group_scope.
Notation "\prod_ ( i : t ) F" :=
(\big[mulg/1]_(i : t) F%g) (only parsing) : group_scope.
Notation "\prod_ ( i < n | P ) F" :=
(\big[mulg/1]_(i < n | P%B) F%g) : group_scope.
Notation "\prod_ ( i < n ) F" :=
(\big[mulg/1]_(i < n) F%g) : group_scope.
Notation "\prod_ ( i 'in' A | P ) F" :=
(\big[mulg/1]_(i in A | P%B) F%g) : group_scope.
Notation "\prod_ ( i 'in' A ) F" :=
(\big[mulg/1]_(i in A) F%g) : group_scope.
Section PreGroupIdentities.
Variable T : baseFinGroupType.
Implicit Types x y z : T.
Lemma mulgA : associative mulgT.
Lemma mul1g : left_id 1 mulgT.
Lemma invgK : @involutive T invg.
Lemma invMg x y : (x × y)^-1 = y^-1 × x^-1.
Lemma invg_inj : @injective T T invg.
Lemma eq_invg_sym x y : (x^-1 == y) = (x == y^-1).
Lemma invg1 : 1^-1 = 1 :> T.
Lemma eq_invg1 x : (x^-1 == 1) = (x == 1).
Lemma mulg1 : right_id 1 mulgT.
Canonical finGroup_law := Monoid.Law mulgA mul1g mulg1.
Lemma expgnE x n : x ^+ n = expgn_rec x n.
Lemma expg0 x : x ^+ 0 = 1.
Lemma expg1 x : x ^+ 1 = x.
Lemma expgS x n : x ^+ n.+1 = x × x ^+ n.
Lemma expg1n n : 1 ^+ n = 1 :> T.
Lemma expgD x n m : x ^+ (n + m) = x ^+ n × x ^+ m.
Lemma expgSr x n : x ^+ n.+1 = x ^+ n × x.
Lemma expgM x n m : x ^+ (n × m) = x ^+ n ^+ m.
Lemma expgAC x m n : x ^+ m ^+ n = x ^+ n ^+ m.
Definition commute x y := x × y = y × x.
Lemma commute_refl x : commute x x.
Lemma commute_sym x y : commute x y → commute y x.
Lemma commute1 x : commute x 1.
Lemma commuteM x y z : commute x y → commute x z → commute x (y × z).
Lemma commuteX x y n : commute x y → commute x (y ^+ n).
Lemma commuteX2 x y m n : commute x y → commute (x ^+ m) (y ^+ n).
Lemma expgVn x n : x^-1 ^+ n = x ^- n.
Lemma expgMn x y n : commute x y → (x × y) ^+ n = x ^+ n × y ^+ n.
End PreGroupIdentities.
Hint Resolve commute1 : core.
Section GroupIdentities.
Variable T : finGroupType.
Implicit Types x y z : T.
Lemma mulVg : left_inverse 1 invg mulgT.
Lemma mulgV : right_inverse 1 invg mulgT.
Lemma mulKg : left_loop invg mulgT.
Lemma mulKVg : rev_left_loop invg mulgT.
Lemma mulgI : right_injective mulgT.
Lemma mulgK : right_loop invg mulgT.
Lemma mulgKV : rev_right_loop invg mulgT.
Lemma mulIg : left_injective mulgT.
Lemma eq_invg_mul x y : (x^-1 == y :> T) = (x × y == 1 :> T).
Lemma eq_mulgV1 x y : (x == y) = (x × y^-1 == 1 :> T).
Lemma eq_mulVg1 x y : (x == y) = (x^-1 × y == 1 :> T).
Lemma commuteV x y : commute x y → commute x y^-1.
Lemma conjgE x y : x ^ y = y^-1 × (x × y).
Lemma conjgC x y : x × y = y × x ^ y.
Lemma conjgCV x y : x × y = y ^ x^-1 × x.
Lemma conjg1 x : x ^ 1 = x.
Lemma conj1g x : 1 ^ x = 1.
Lemma conjMg x y z : (x × y) ^ z = x ^ z × y ^ z.
Lemma conjgM x y z : x ^ (y × z) = (x ^ y) ^ z.
Lemma conjVg x y : x^-1 ^ y = (x ^ y)^-1.
Lemma conjJg x y z : (x ^ y) ^ z = (x ^ z) ^ y ^ z.
Lemma conjXg x y n : (x ^+ n) ^ y = (x ^ y) ^+ n.
Lemma conjgK : @right_loop T T invg conjg.
Lemma conjgKV : @rev_right_loop T T invg conjg.
Lemma conjg_inj : @left_injective T T T conjg.
Lemma conjg_eq1 x y : (x ^ y == 1) = (x == 1).
Lemma conjg_prod I r (P : pred I) F z :
(\prod_(i <- r | P i) F i) ^ z = \prod_(i <- r | P i) (F i ^ z).
Lemma commgEl x y : [~ x, y] = x^-1 × x ^ y.
Lemma commgEr x y : [~ x, y] = y^-1 ^ x × y.
Lemma commgC x y : x × y = y × x × [~ x, y].
Lemma commgCV x y : x × y = [~ x^-1, y^-1] × (y × x).
Lemma conjRg x y z : [~ x, y] ^ z = [~ x ^ z, y ^ z].
Lemma invg_comm x y : [~ x, y]^-1 = [~ y, x].
Lemma commgP x y : reflect (commute x y) ([~ x, y] == 1 :> T).
Lemma conjg_fixP x y : reflect (x ^ y = x) ([~ x, y] == 1 :> T).
Lemma commg1_sym x y : ([~ x, y] == 1 :> T) = ([~ y, x] == 1 :> T).
Lemma commg1 x : [~ x, 1] = 1.
Lemma comm1g x : [~ 1, x] = 1.
Lemma commgg x : [~ x, x] = 1.
Lemma commgXg x n : [~ x, x ^+ n] = 1.
Lemma commgVg x : [~ x, x^-1] = 1.
Lemma commgXVg x n : [~ x, x ^- n] = 1.
Notation "x1 ^ x2" := (conjg x1 x2) : group_scope.
Definition commg (T : finGroupType) (x y : T) := x^-1 × x ^ y.
Notation "[ ~ x1 , x2 , .. , xn ]" := (commg .. (commg x1 x2) .. xn)
: group_scope.
Notation "\prod_ ( i <- r | P ) F" :=
(\big[mulg/1]_(i <- r | P%B) F%g) : group_scope.
Notation "\prod_ ( i <- r ) F" :=
(\big[mulg/1]_(i <- r) F%g) : group_scope.
Notation "\prod_ ( m <= i < n | P ) F" :=
(\big[mulg/1]_(m ≤ i < n | P%B) F%g) : group_scope.
Notation "\prod_ ( m <= i < n ) F" :=
(\big[mulg/1]_(m ≤ i < n) F%g) : group_scope.
Notation "\prod_ ( i | P ) F" :=
(\big[mulg/1]_(i | P%B) F%g) : group_scope.
Notation "\prod_ i F" :=
(\big[mulg/1]_i F%g) : group_scope.
Notation "\prod_ ( i : t | P ) F" :=
(\big[mulg/1]_(i : t | P%B) F%g) (only parsing) : group_scope.
Notation "\prod_ ( i : t ) F" :=
(\big[mulg/1]_(i : t) F%g) (only parsing) : group_scope.
Notation "\prod_ ( i < n | P ) F" :=
(\big[mulg/1]_(i < n | P%B) F%g) : group_scope.
Notation "\prod_ ( i < n ) F" :=
(\big[mulg/1]_(i < n) F%g) : group_scope.
Notation "\prod_ ( i 'in' A | P ) F" :=
(\big[mulg/1]_(i in A | P%B) F%g) : group_scope.
Notation "\prod_ ( i 'in' A ) F" :=
(\big[mulg/1]_(i in A) F%g) : group_scope.
Section PreGroupIdentities.
Variable T : baseFinGroupType.
Implicit Types x y z : T.
Lemma mulgA : associative mulgT.
Lemma mul1g : left_id 1 mulgT.
Lemma invgK : @involutive T invg.
Lemma invMg x y : (x × y)^-1 = y^-1 × x^-1.
Lemma invg_inj : @injective T T invg.
Lemma eq_invg_sym x y : (x^-1 == y) = (x == y^-1).
Lemma invg1 : 1^-1 = 1 :> T.
Lemma eq_invg1 x : (x^-1 == 1) = (x == 1).
Lemma mulg1 : right_id 1 mulgT.
Canonical finGroup_law := Monoid.Law mulgA mul1g mulg1.
Lemma expgnE x n : x ^+ n = expgn_rec x n.
Lemma expg0 x : x ^+ 0 = 1.
Lemma expg1 x : x ^+ 1 = x.
Lemma expgS x n : x ^+ n.+1 = x × x ^+ n.
Lemma expg1n n : 1 ^+ n = 1 :> T.
Lemma expgD x n m : x ^+ (n + m) = x ^+ n × x ^+ m.
Lemma expgSr x n : x ^+ n.+1 = x ^+ n × x.
Lemma expgM x n m : x ^+ (n × m) = x ^+ n ^+ m.
Lemma expgAC x m n : x ^+ m ^+ n = x ^+ n ^+ m.
Definition commute x y := x × y = y × x.
Lemma commute_refl x : commute x x.
Lemma commute_sym x y : commute x y → commute y x.
Lemma commute1 x : commute x 1.
Lemma commuteM x y z : commute x y → commute x z → commute x (y × z).
Lemma commuteX x y n : commute x y → commute x (y ^+ n).
Lemma commuteX2 x y m n : commute x y → commute (x ^+ m) (y ^+ n).
Lemma expgVn x n : x^-1 ^+ n = x ^- n.
Lemma expgMn x y n : commute x y → (x × y) ^+ n = x ^+ n × y ^+ n.
End PreGroupIdentities.
Hint Resolve commute1 : core.
Section GroupIdentities.
Variable T : finGroupType.
Implicit Types x y z : T.
Lemma mulVg : left_inverse 1 invg mulgT.
Lemma mulgV : right_inverse 1 invg mulgT.
Lemma mulKg : left_loop invg mulgT.
Lemma mulKVg : rev_left_loop invg mulgT.
Lemma mulgI : right_injective mulgT.
Lemma mulgK : right_loop invg mulgT.
Lemma mulgKV : rev_right_loop invg mulgT.
Lemma mulIg : left_injective mulgT.
Lemma eq_invg_mul x y : (x^-1 == y :> T) = (x × y == 1 :> T).
Lemma eq_mulgV1 x y : (x == y) = (x × y^-1 == 1 :> T).
Lemma eq_mulVg1 x y : (x == y) = (x^-1 × y == 1 :> T).
Lemma commuteV x y : commute x y → commute x y^-1.
Lemma conjgE x y : x ^ y = y^-1 × (x × y).
Lemma conjgC x y : x × y = y × x ^ y.
Lemma conjgCV x y : x × y = y ^ x^-1 × x.
Lemma conjg1 x : x ^ 1 = x.
Lemma conj1g x : 1 ^ x = 1.
Lemma conjMg x y z : (x × y) ^ z = x ^ z × y ^ z.
Lemma conjgM x y z : x ^ (y × z) = (x ^ y) ^ z.
Lemma conjVg x y : x^-1 ^ y = (x ^ y)^-1.
Lemma conjJg x y z : (x ^ y) ^ z = (x ^ z) ^ y ^ z.
Lemma conjXg x y n : (x ^+ n) ^ y = (x ^ y) ^+ n.
Lemma conjgK : @right_loop T T invg conjg.
Lemma conjgKV : @rev_right_loop T T invg conjg.
Lemma conjg_inj : @left_injective T T T conjg.
Lemma conjg_eq1 x y : (x ^ y == 1) = (x == 1).
Lemma conjg_prod I r (P : pred I) F z :
(\prod_(i <- r | P i) F i) ^ z = \prod_(i <- r | P i) (F i ^ z).
Lemma commgEl x y : [~ x, y] = x^-1 × x ^ y.
Lemma commgEr x y : [~ x, y] = y^-1 ^ x × y.
Lemma commgC x y : x × y = y × x × [~ x, y].
Lemma commgCV x y : x × y = [~ x^-1, y^-1] × (y × x).
Lemma conjRg x y z : [~ x, y] ^ z = [~ x ^ z, y ^ z].
Lemma invg_comm x y : [~ x, y]^-1 = [~ y, x].
Lemma commgP x y : reflect (commute x y) ([~ x, y] == 1 :> T).
Lemma conjg_fixP x y : reflect (x ^ y = x) ([~ x, y] == 1 :> T).
Lemma commg1_sym x y : ([~ x, y] == 1 :> T) = ([~ y, x] == 1 :> T).
Lemma commg1 x : [~ x, 1] = 1.
Lemma comm1g x : [~ 1, x] = 1.
Lemma commgg x : [~ x, x] = 1.
Lemma commgXg x n : [~ x, x ^+ n] = 1.
Lemma commgVg x : [~ x, x^-1] = 1.
Lemma commgXVg x n : [~ x, x ^- n] = 1.
Other commg identities should slot in here.
End GroupIdentities.
Hint Rewrite mulg1 mul1g invg1 mulVg mulgV (@invgK) mulgK mulgKV
invMg mulgA : gsimpl.
Ltac gsimpl := autorewrite with gsimpl; try done.
Definition gsimp := (mulg1 , mul1g, (invg1, @invgK), (mulgV, mulVg)).
Definition gnorm := (gsimp, (mulgK, mulgKV, (mulgA, invMg))).
Section Repr.
Plucking a set representative.
Variable gT : baseFinGroupType.
Implicit Type A : {set gT}.
Definition repr A := if 1 \in A then 1 else odflt 1 [pick x in A].
Lemma mem_repr A x : x \in A → repr A \in A.
Lemma card_mem_repr A : #|A| > 0 → repr A \in A.
Lemma repr_set1 x : repr [set x] = x.
Lemma repr_set0 : repr set0 = 1.
End Repr.
Section BaseSetMulDef.
We only assume a baseFinGroupType to allow this construct to be iterated.
Set-lifted group operations.
The pre-group structure of group subsets.
Lemma set_mul1g : left_id [set 1] set_mulg.
Lemma set_mulgA : associative set_mulg.
Lemma set_invgK : involutive set_invg.
Lemma set_invgM : {morph set_invg : A B / set_mulg A B >-> set_mulg B A}.
Definition group_set_baseGroupMixin : FinGroup.mixin_of (set_type gT) :=
FinGroup.BaseMixin set_mulgA set_mul1g set_invgK set_invgM.
Canonical group_set_baseGroupType :=
Eval hnf in BaseFinGroupType (set_type gT) group_set_baseGroupMixin.
Canonical group_set_of_baseGroupType :=
Eval hnf in [baseFinGroupType of {set gT}].
End BaseSetMulDef.
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.
Module GroupSet.
Definition sort (gT : baseFinGroupType) := {set gT}.
End GroupSet.
Identity Coercion GroupSet_of_sort : GroupSet.sort >-> set_of.
Module Type GroupSetBaseGroupSig.
Definition sort gT := group_set_of_baseGroupType gT : Type.
End GroupSetBaseGroupSig.
Module MakeGroupSetBaseGroup (Gset_base : GroupSetBaseGroupSig).
Identity Coercion of_sort : Gset_base.sort >-> FinGroup.arg_sort.
End MakeGroupSetBaseGroup.
Module Export GroupSetBaseGroup := MakeGroupSetBaseGroup GroupSet.
Canonical group_set_eqType gT := Eval hnf in [eqType of GroupSet.sort gT].
Canonical group_set_choiceType gT :=
Eval hnf in [choiceType of GroupSet.sort gT].
Canonical group_set_countType gT := Eval hnf in [countType of GroupSet.sort gT].
Canonical group_set_finType gT := Eval hnf in [finType of GroupSet.sort gT].
Section GroupSetMulDef.
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.
Variable gT : finGroupType.
Implicit Types A B : {set gT}.
Implicit Type x y : gT.
Definition lcoset A x := mulg x @: A.
Definition rcoset A x := mulg^~ x @: A.
Definition lcosets A B := lcoset A @: B.
Definition rcosets A B := rcoset A @: B.
Definition indexg B A := #|rcosets A B|.
Definition conjugate A x := conjg^~ x @: A.
Definition conjugates A B := conjugate A @: B.
Definition class x B := conjg x @: B.
Definition classes A := class^~ A @: A.
Definition class_support A B := conjg @2: (A, B).
Definition commg_set A B := commg @2: (A, B).
Implicit Types A B : {set gT}.
Implicit Type x y : gT.
Definition lcoset A x := mulg x @: A.
Definition rcoset A x := mulg^~ x @: A.
Definition lcosets A B := lcoset A @: B.
Definition rcosets A B := rcoset A @: B.
Definition indexg B A := #|rcosets A B|.
Definition conjugate A x := conjg^~ x @: A.
Definition conjugates A B := conjugate A @: B.
Definition class x B := conjg x @: B.
Definition classes A := class^~ A @: A.
Definition class_support A B := conjg @2: (A, B).
Definition commg_set A B := commg @2: (A, B).
These will only be used later, but are defined here so that we can
keep all the Notation together.
Definition normaliser A := [set x | conjugate A x \subset A].
Definition centraliser A := \bigcap_(x in A) normaliser [set x].
Definition abelian A := A \subset centraliser A.
Definition normal A B := (A \subset B) && (B \subset normaliser A).
Definition centraliser A := \bigcap_(x in A) normaliser [set x].
Definition abelian A := A \subset centraliser A.
Definition normal A B := (A \subset B) && (B \subset normaliser A).
"normalised" and "centralise[s|d]" are intended to be used with
the {in ...} form, as in abelian below.
Definition normalised A := ∀ x, conjugate A x = A.
Definition centralises x A := ∀ y, y \in A → commute x y.
Definition centralised A := ∀ x, centralises x A.
End GroupSetMulDef.
Notation "[ 1 gT ]" := (1 : {set gT}) : group_scope.
Notation "[ 1 ]" := [1 FinGroup.sort _] : group_scope.
Notation "A ^#" := (A :\ 1) : group_scope.
Notation "x *: A" := ([set x%g] × A) : group_scope.
Notation "A :* x" := (A × [set x%g]) : group_scope.
Notation "A :^ x" := (conjugate A x) : group_scope.
Notation "x ^: B" := (class x B) : group_scope.
Notation "A :^: B" := (conjugates A B) : group_scope.
Notation "#| B : A |" := (indexg B A) : group_scope.
Definition centralises x A := ∀ y, y \in A → commute x y.
Definition centralised A := ∀ x, centralises x A.
End GroupSetMulDef.
Notation "[ 1 gT ]" := (1 : {set gT}) : group_scope.
Notation "[ 1 ]" := [1 FinGroup.sort _] : group_scope.
Notation "A ^#" := (A :\ 1) : group_scope.
Notation "x *: A" := ([set x%g] × A) : group_scope.
Notation "A :* x" := (A × [set x%g]) : group_scope.
Notation "A :^ x" := (conjugate A x) : group_scope.
Notation "x ^: B" := (class x B) : group_scope.
Notation "A :^: B" := (conjugates A B) : group_scope.
Notation "#| B : A |" := (indexg B A) : group_scope.
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.
Notation "''N' ( A )" := (normaliser A) : group_scope.
Notation "''N_' G ( A )" := (G%g :&: 'N(A)) : group_scope.
Notation "A <| B" := (normal A B) : group_scope.
Notation "''C' ( A )" := (centraliser A) : group_scope.
Notation "''C_' G ( A )" := (G%g :&: 'C(A)) : group_scope.
Notation "''C_' ( G ) ( A )" := 'C_G(A) (only parsing) : group_scope.
Notation "''C' [ x ]" := 'N([set x%g]) : group_scope.
Notation "''C_' G [ x ]" := 'N_G([set x%g]) : group_scope.
Notation "''C_' ( G ) [ x ]" := 'C_G[x] (only parsing) : group_scope.
Section BaseSetMulProp.
Properties of the purely multiplicative structure.
Set product. We already have all the pregroup identities, so we
only need to add the monotonicity rules.
Lemma mulsgP A B x :
reflect (imset2_spec mulg (mem A) (fun _ ⇒ mem B) x) (x \in A × B).
Lemma mem_mulg A B x y : x \in A → y \in B → x × y \in A × B.
Lemma prodsgP (I : finType) (P : pred I) (A : I → {set gT}) x :
reflect (exists2 c, ∀ i, P i → c i \in A i & x = \prod_(i | P i) c i)
(x \in \prod_(i | P i) A i).
Lemma mem_prodg (I : finType) (P : pred I) (A : I → {set gT}) c :
(∀ i, P i → c i \in A i) → \prod_(i | P i) c i \in \prod_(i | P i) A i.
Lemma mulSg A B C : A \subset B → A × C \subset B × C.
Lemma mulgS A B C : B \subset C → A × B \subset A × C.
Lemma mulgSS A B C D : A \subset B → C \subset D → A × C \subset B × D.
Lemma mulg_subl A B : 1 \in B → A \subset A × B.
Lemma mulg_subr A B : 1 \in A → B \subset A × B.
Lemma mulUg A B C : (A :|: B) × C = (A × C) :|: (B × C).
Lemma mulgU A B C : A × (B :|: C) = (A × B) :|: (A × C).
Set (pointwise) inverse.
Lemma invUg A B : (A :|: B)^-1 = A^-1 :|: B^-1.
Lemma invIg A B : (A :&: B)^-1 = A^-1 :&: B^-1.
Lemma invDg A B : (A :\: B)^-1 = A^-1 :\: B^-1.
Lemma invCg A : (~: A)^-1 = ~: A^-1.
Lemma invSg A B : (A^-1 \subset B^-1) = (A \subset B).
Lemma mem_invg x A : (x \in A^-1) = (x^-1 \in A).
Lemma memV_invg x A : (x^-1 \in A^-1) = (x \in A).
Lemma card_invg A : #|A^-1| = #|A|.
Product with singletons.
Lemma set1gE : 1 = [set 1] :> {set gT}.
Lemma set1gP x : reflect (x = 1) (x \in [1]).
Lemma mulg_set1 x y : [set x] :* y = [set x × y].
Lemma invg_set1 x : [set x]^-1 = [set x^-1].
End BaseSetMulProp.
Section GroupSetMulProp.
Constructs that need a finGroupType
Left cosets.
Lemma lcosetE A x : lcoset A x = x *: A.
Lemma card_lcoset A x : #|x *: A| = #|A|.
Lemma mem_lcoset A x y : (y \in x *: A) = (x^-1 × y \in A).
Lemma lcosetP A x y : reflect (exists2 a, a \in A & y = x × a) (y \in x *: A).
Lemma lcosetsP A B C :
reflect (exists2 x, x \in B & C = x *: A) (C \in lcosets A B).
Lemma lcosetM A x y : (x × y) *: A = x *: (y *: A).
Lemma lcoset1 A : 1 *: A = A.
Lemma lcosetK : left_loop invg (fun x A ⇒ x *: A).
Lemma lcosetKV : rev_left_loop invg (fun x A ⇒ x *: A).
Lemma lcoset_inj : right_injective (fun x A ⇒ x *: A).
Lemma lcosetS x A B : (x *: A \subset x *: B) = (A \subset B).
Lemma sub_lcoset x A B : (A \subset x *: B) = (x^-1 *: A \subset B).
Lemma sub_lcosetV x A B : (A \subset x^-1 *: B) = (x *: A \subset B).
Right cosets.
Lemma rcosetE A x : rcoset A x = A :* x.
Lemma card_rcoset A x : #|A :* x| = #|A|.
Lemma mem_rcoset A x y : (y \in A :* x) = (y × x^-1 \in A).
Lemma rcosetP A x y : reflect (exists2 a, a \in A & y = a × x) (y \in A :* x).
Lemma rcosetsP A B C :
reflect (exists2 x, x \in B & C = A :* x) (C \in rcosets A B).
Lemma rcosetM A x y : A :* (x × y) = A :* x :* y.
Lemma rcoset1 A : A :* 1 = A.
Lemma rcosetK : right_loop invg (fun A x ⇒ A :* x).
Lemma rcosetKV : rev_right_loop invg (fun A x ⇒ A :* x).
Lemma rcoset_inj : left_injective (fun A x ⇒ A :* x).
Lemma rcosetS x A B : (A :* x \subset B :* x) = (A \subset B).
Lemma sub_rcoset x A B : (A \subset B :* x) = (A :* x ^-1 \subset B).
Lemma sub_rcosetV x A B : (A \subset B :* x^-1) = (A :* x \subset B).
Inverse maps lcosets to rcosets
Conjugates.
Lemma conjg_preim A x : A :^ x = (conjg^~ x^-1) @^-1: A.
Lemma mem_conjg A x y : (y \in A :^ x) = (y ^ x^-1 \in A).
Lemma mem_conjgV A x y : (y \in A :^ x^-1) = (y ^ x \in A).
Lemma memJ_conjg A x y : (y ^ x \in A :^ x) = (y \in A).
Lemma conjsgE A x : A :^ x = x^-1 *: (A :* x).
Lemma conjsg1 A : A :^ 1 = A.
Lemma conjsgM A x y : A :^ (x × y) = (A :^ x) :^ y.
Lemma conjsgK : @right_loop _ gT invg conjugate.
Lemma conjsgKV : @rev_right_loop _ gT invg conjugate.
Lemma conjsg_inj : @left_injective _ gT _ conjugate.
Lemma cardJg A x : #|A :^ x| = #|A|.
Lemma conjSg A B x : (A :^ x \subset B :^ x) = (A \subset B).
Lemma properJ A B x : (A :^ x \proper B :^ x) = (A \proper B).
Lemma sub_conjg A B x : (A :^ x \subset B) = (A \subset B :^ x^-1).
Lemma sub_conjgV A B x : (A :^ x^-1 \subset B) = (A \subset B :^ x).
Lemma conjg_set1 x y : [set x] :^ y = [set x ^ y].
Lemma conjs1g x : 1 :^ x = 1.
Lemma conjsg_eq1 A x : (A :^ x == 1%g) = (A == 1%g).
Lemma conjsMg A B x : (A × B) :^ x = A :^ x × B :^ x.
Lemma conjIg A B x : (A :&: B) :^ x = A :^ x :&: B :^ x.
Lemma conj0g x : set0 :^ x = set0.
Lemma conjTg x : [set: gT] :^ x = [set: gT].
Lemma bigcapJ I r (P : pred I) (B : I → {set gT}) x :
\bigcap_(i <- r | P i) (B i :^ x) = (\bigcap_(i <- r | P i) B i) :^ x.
Lemma conjUg A B x : (A :|: B) :^ x = A :^ x :|: B :^ x.
Lemma bigcupJ I r (P : pred I) (B : I → {set gT}) x :
\bigcup_(i <- r | P i) (B i :^ x) = (\bigcup_(i <- r | P i) B i) :^ x.
Lemma conjCg A x : (~: A) :^ x = ~: A :^ x.
Lemma conjDg A B x : (A :\: B) :^ x = A :^ x :\: B :^ x.
Lemma conjD1g A x : A^# :^ x = (A :^ x)^#.
Classes; not much for now.
Lemma memJ_class x y A : y \in A → x ^ y \in x ^: A.
Lemma classS x A B : A \subset B → x ^: A \subset x ^: B.
Lemma class_set1 x y : x ^: [set y] = [set x ^ y].
Lemma class1g x A : x \in A → 1 ^: A = 1.
Lemma classVg x A : x^-1 ^: A = (x ^: A)^-1.
Lemma mem_classes x A : x \in A → x ^: A \in classes A.
Lemma memJ_class_support A B x y :
x \in A → y \in B → x ^ y \in class_support A B.
Lemma class_supportM A B C :
class_support A (B × C) = class_support (class_support A B) C.
Lemma class_support_set1l A x : class_support [set x] A = x ^: A.
Lemma class_support_set1r A x : class_support A [set x] = A :^ x.
Lemma classM x A B : x ^: (A × B) = class_support (x ^: A) B.
Lemma class_lcoset x y A : x ^: (y *: A) = (x ^ y) ^: A.
Lemma class_rcoset x A y : x ^: (A :* y) = (x ^: A) :^ y.
Conjugate set.
Lemma conjugatesS A B C : B \subset C → A :^: B \subset A :^: C.
Lemma conjugates_set1 A x : A :^: [set x] = [set A :^ x].
Lemma conjugates_conj A x B : (A :^ x) :^: B = A :^: (x *: B).
Class support.
Lemma class_supportEl A B : class_support A B = \bigcup_(x in A) x ^: B.
Lemma class_supportEr A B : class_support A B = \bigcup_(x in B) A :^ x.
Groups (at last!)
Definition group_set A := (1 \in A) && (A × A \subset A).
Lemma group_setP A :
reflect (1 \in A ∧ {in A & A, ∀ x y, x × y \in A}) (group_set A).
Structure group_type : Type := Group {
gval :> GroupSet.sort gT;
_ : group_set gval
}.
Definition group_of of phant gT : predArgType := group_type.
Identity Coercion type_of_group : group_of >-> group_type.
Canonical group_subType := Eval hnf in [subType for gval].
Definition group_eqMixin := Eval hnf in [eqMixin of group_type by <:].
Canonical group_eqType := Eval hnf in EqType group_type group_eqMixin.
Definition group_choiceMixin := [choiceMixin of group_type by <:].
Canonical group_choiceType :=
Eval hnf in ChoiceType group_type group_choiceMixin.
Definition group_countMixin := [countMixin of group_type by <:].
Canonical group_countType := Eval hnf in CountType group_type group_countMixin.
Canonical group_subCountType := Eval hnf in [subCountType of group_type].
Definition group_finMixin := [finMixin of group_type by <:].
Canonical group_finType := Eval hnf in FinType group_type group_finMixin.
Canonical group_subFinType := Eval hnf in [subFinType of group_type].
No predType or baseFinGroupType structures, as these would hide the
group-to-set coercion and thus spoil unification.
Canonical group_of_subType := Eval hnf in [subType of groupT].
Canonical group_of_eqType := Eval hnf in [eqType of groupT].
Canonical group_of_choiceType := Eval hnf in [choiceType of groupT].
Canonical group_of_countType := Eval hnf in [countType of groupT].
Canonical group_of_subCountType := Eval hnf in [subCountType of groupT].
Canonical group_of_finType := Eval hnf in [finType of groupT].
Canonical group_of_subFinType := Eval hnf in [subFinType of groupT].
Definition group (A : {set gT}) gA : groupT := @Group A gA.
Definition clone_group G :=
let: Group _ gP := G return {type of Group for G} → groupT in fun k ⇒ k gP.
Lemma group_inj : injective gval.
Lemma groupP (G : groupT) : group_set G.
Lemma congr_group (H K : groupT) : H = K → H :=: K.
Lemma isgroupP A : reflect (∃ G : groupT, A = G) (group_set A).
Lemma group_set_one : group_set 1.
Canonical one_group := group group_set_one.
Canonical set1_group := @group [set 1] group_set_one.
Lemma group_setT (phT : phant gT) : group_set (setTfor phT).
Canonical setT_group phT := group (group_setT phT).
These definitions come early so we can establish the Notation.
Definition generated A := \bigcap_(G : groupT | A \subset G) G.
Definition gcore A B := \bigcap_(x in B) A :^ x.
Definition joing A B := generated (A :|: B).
Definition commutator A B := generated (commg_set A B).
Definition cycle x := generated [set x].
Definition order x := #|cycle x|.
End GroupSetMulProp.
Notation "{ 'group' gT }" := (group_of (Phant gT))
(at level 0, format "{ 'group' gT }") : type_scope.
Notation "[ 'group' 'of' G ]" := (clone_group (@group _ G))
(at level 0, format "[ 'group' 'of' G ]") : form_scope.
Notation "1" := (one_group _) : Group_scope.
Notation "[ 1 gT ]" := (1%G : {group gT}) : Group_scope.
Notation "[ 'set' : gT ]" := (setT_group (Phant gT)) : Group_scope.
Definition gcore A B := \bigcap_(x in B) A :^ x.
Definition joing A B := generated (A :|: B).
Definition commutator A B := generated (commg_set A B).
Definition cycle x := generated [set x].
Definition order x := #|cycle x|.
End GroupSetMulProp.
Notation "{ 'group' gT }" := (group_of (Phant gT))
(at level 0, format "{ 'group' gT }") : type_scope.
Notation "[ 'group' 'of' G ]" := (clone_group (@group _ G))
(at level 0, format "[ 'group' 'of' G ]") : form_scope.
Notation "1" := (one_group _) : Group_scope.
Notation "[ 1 gT ]" := (1%G : {group gT}) : Group_scope.
Notation "[ 'set' : gT ]" := (setT_group (Phant gT)) : Group_scope.
Helper notation for defining new groups that need a bespoke finGroupType.
The actual group for such a type (say, my_gT) will be the full group,
i.e., [set: my_gT] or [set: my_gT]%G, but Coq will not recognize
specific notation for these because of the coercions inserted during type
inference, unless they are defined as [set: gsort my_gT] using the
Notation below.
Notation gsort gT := (FinGroup.arg_sort (FinGroup.base gT%type)) (only parsing).
Notation "<< A >>" := (generated A) : group_scope.
Notation "<[ x ] >" := (cycle x) : group_scope.
Notation "#[ x ]" := (order x) : group_scope.
Notation "A <*> B" := (joing A B) : group_scope.
Notation "[ ~: A1 , A2 , .. , An ]" :=
(commutator .. (commutator A1 A2) .. An) : group_scope.
Section GroupProp.
Variable gT : finGroupType.
Notation sT := {set gT}.
Implicit Types A B C D : sT.
Implicit Types x y z : gT.
Implicit Types G H K : {group gT}.
Section OneGroup.
Variable G : {group gT}.
Lemma valG : val G = G.
Notation "<< A >>" := (generated A) : group_scope.
Notation "<[ x ] >" := (cycle x) : group_scope.
Notation "#[ x ]" := (order x) : group_scope.
Notation "A <*> B" := (joing A B) : group_scope.
Notation "[ ~: A1 , A2 , .. , An ]" :=
(commutator .. (commutator A1 A2) .. An) : group_scope.
Section GroupProp.
Variable gT : finGroupType.
Notation sT := {set gT}.
Implicit Types A B C D : sT.
Implicit Types x y z : gT.
Implicit Types G H K : {group gT}.
Section OneGroup.
Variable G : {group gT}.
Lemma valG : val G = G.
Non-triviality.
Lemma group1 : 1 \in G.
Hint Resolve group1 : core.
Lemma group1_contra x : x \notin G → x != 1.
Lemma sub1G : [1 gT] \subset G.
Lemma subG1 : (G \subset [1]) = (G :==: 1).
Lemma setI1g : 1 :&: G = 1.
Lemma setIg1 : G :&: 1 = 1.
Lemma subG1_contra H : G \subset H → G :!=: 1 → H :!=: 1.
Lemma repr_group : repr G = 1.
Lemma cardG_gt0 : 0 < #|G|.
Lemma indexg_gt0 A : 0 < #|G : A|.
Lemma trivgP : reflect (G :=: 1) (G \subset [1]).
Lemma trivGP : reflect (G = 1%G) (G \subset [1]).
Lemma proper1G : ([1] \proper G) = (G :!=: 1).
Lemma trivgPn : reflect (exists2 x, x \in G & x != 1) (G :!=: 1).
Lemma trivg_card_le1 : (G :==: 1) = (#|G| ≤ 1).
Lemma trivg_card1 : (G :==: 1) = (#|G| == 1%N).
Lemma cardG_gt1 : (#|G| > 1) = (G :!=: 1).
Lemma card_le1_trivg : #|G| ≤ 1 → G :=: 1.
Lemma card1_trivg : #|G| = 1%N → G :=: 1.
Inclusion and product.
Lemma mulG_subl A : A \subset A × G.
Lemma mulG_subr A : A \subset G × A.
Lemma mulGid : G × G = G.
Lemma mulGS A B : (G × A \subset G × B) = (A \subset G × B).
Lemma mulSG A B : (A × G \subset B × G) = (A \subset B × G).
Lemma mul_subG A B : A \subset G → B \subset G → A × B \subset G.
Membership lemmas
Lemma groupM x y : x \in G → y \in G → x × y \in G.
Lemma groupX x n : x \in G → x ^+ n \in G.
Lemma groupVr x : x \in G → x^-1 \in G.
Lemma groupVl x : x^-1 \in G → x \in G.
Lemma groupV x : (x^-1 \in G) = (x \in G).
Lemma groupMl x y : x \in G → (x × y \in G) = (y \in G).
Lemma groupMr x y : x \in G → (y × x \in G) = (y \in G).
Definition in_group := (group1, groupV, (groupMl, groupX)).
Lemma groupJ x y : x \in G → y \in G → x ^ y \in G.
Lemma groupJr x y : y \in G → (x ^ y \in G) = (x \in G).
Lemma groupR x y : x \in G → y \in G → [~ x, y] \in G.
Lemma group_prod I r (P : pred I) F :
(∀ i, P i → F i \in G) → \prod_(i <- r | P i) F i \in G.
Inverse is an anti-morphism.
Lemma invGid : G^-1 = G.
Lemma inv_subG A : (A^-1 \subset G) = (A \subset G).
Lemma invg_lcoset x : (x *: G)^-1 = G :* x^-1.
Lemma invg_rcoset x : (G :* x)^-1 = x^-1 *: G.
Lemma memV_lcosetV x y : (y^-1 \in x^-1 *: G) = (y \in G :* x).
Lemma memV_rcosetV x y : (y^-1 \in G :* x^-1) = (y \in x *: G).
Product idempotence
Lemma mulSgGid A x : x \in A → A \subset G → A × G = G.
Lemma mulGSgid A x : x \in A → A \subset G → G × A = G.
Left cosets
Lemma lcoset_refl x : x \in x *: G.
Lemma lcoset_sym x y : (x \in y *: G) = (y \in x *: G).
Lemma lcoset_eqP {x y} : reflect (x *: G = y *: G) (x \in y *: G).
Lemma lcoset_transl x y z : x \in y *: G → (x \in z *: G) = (y \in z *: G).
Lemma lcoset_trans x y z : x \in y *: G → y \in z *: G → x \in z *: G.
Lemma lcoset_id x : x \in G → x *: G = G.
Right cosets, with an elimination form for repr.
Lemma rcoset_refl x : x \in G :* x.
Lemma rcoset_sym x y : (x \in G :* y) = (y \in G :* x).
Lemma rcoset_eqP {x y} : reflect (G :* x = G :* y) (x \in G :* y).
Lemma rcoset_transl x y z : x \in G :* y → (x \in G :* z) = (y \in G :* z).
Lemma rcoset_trans x y z : x \in G :* y → y \in G :* z → x \in G :* z.
Lemma rcoset_id x : x \in G → G :* x = G.
Elimination form.
Variant rcoset_repr_spec x : gT → Type :=
RcosetReprSpec g : g \in G → rcoset_repr_spec x (g × x).
Lemma mem_repr_rcoset x : repr (G :* x) \in G :* x.
This form sometimes fails because ssreflect 1.1 delegates matching to the
(weaker) primitive Coq algorithm for general (co)inductive type families.
Lemma repr_rcosetP x : rcoset_repr_spec x (repr (G :* x)).
Lemma rcoset_repr x : G :* (repr (G :* x)) = G :* x.
Lemma rcoset_repr x : G :* (repr (G :* x)) = G :* x.
Coset spaces.
Lemma mem_rcosets A x : (G :* x \in rcosets G A) = (x \in G × A).
Lemma mem_lcosets A x : (x *: G \in lcosets G A) = (x \in A × G).
Conjugates.
Lemma group_setJ A x : group_set (A :^ x) = group_set A.
Lemma group_set_conjG x : group_set (G :^ x).
Canonical conjG_group x := group (group_set_conjG x).
Lemma conjGid : {in G, normalised G}.
Lemma conj_subG x A : x \in G → A \subset G → A :^ x \subset G.
Classes
Lemma class1G : 1 ^: G = 1.
Lemma classes1 : [1] \in classes G.
Lemma classGidl x y : y \in G → (x ^ y) ^: G = x ^: G.
Lemma classGidr x : {in G, normalised (x ^: G)}.
Lemma class_refl x : x \in x ^: G.
Hint Resolve class_refl : core.
Lemma class_eqP x y : reflect (x ^: G = y ^: G) (x \in y ^: G).
Lemma class_sym x y : (x \in y ^: G) = (y \in x ^: G).
Lemma class_transl x y z : x \in y ^: G → (x \in z ^: G) = (y \in z ^: G).
Lemma class_trans x y z : x \in y ^: G → y \in z ^: G → x \in z ^: G.
Lemma repr_class x : {y | y \in G & repr (x ^: G) = x ^ y}.
Lemma classG_eq1 x : (x ^: G == 1) = (x == 1).
Lemma class_subG x A : x \in G → A \subset G → x ^: A \subset G.
Lemma repr_classesP xG :
reflect (repr xG \in G ∧ xG = repr xG ^: G) (xG \in classes G).
Lemma mem_repr_classes xG : xG \in classes G → repr xG \in xG.
Lemma classes_gt0 : 0 < #|classes G|.
Lemma classes_gt1 : (#|classes G| > 1) = (G :!=: 1).
Lemma mem_class_support A x : x \in A → x \in class_support A G.
Lemma class_supportGidl A x :
x \in G → class_support (A :^ x) G = class_support A G.
Lemma class_supportGidr A : {in G, normalised (class_support A G)}.
Lemma class_support_subG A : A \subset G → class_support A G \subset G.
Lemma sub_class_support A : A \subset class_support A G.
Lemma class_support_id : class_support G G = G.
Lemma class_supportD1 A : (class_support A G)^# = cover (A^# :^: G).
Subgroup Type construction.
We only expect to use this for abstract groups, so we don't project
the argument to a set.
Inductive subg_of : predArgType := Subg x & x \in G.
Definition sgval u := let: Subg x _ := u in x.
Canonical subg_subType := Eval hnf in [subType for sgval].
Definition subg_eqMixin := Eval hnf in [eqMixin of subg_of by <:].
Canonical subg_eqType := Eval hnf in EqType subg_of subg_eqMixin.
Definition subg_choiceMixin := [choiceMixin of subg_of by <:].
Canonical subg_choiceType := Eval hnf in ChoiceType subg_of subg_choiceMixin.
Definition subg_countMixin := [countMixin of subg_of by <:].
Canonical subg_countType := Eval hnf in CountType subg_of subg_countMixin.
Canonical subg_subCountType := Eval hnf in [subCountType of subg_of].
Definition subg_finMixin := [finMixin of subg_of by <:].
Canonical subg_finType := Eval hnf in FinType subg_of subg_finMixin.
Canonical subg_subFinType := Eval hnf in [subFinType of subg_of].
Lemma subgP u : sgval u \in G.
Lemma subg_inj : injective sgval.
Lemma congr_subg u v : u = v → sgval u = sgval v.
Definition subg_one := Subg group1.
Definition subg_inv u := Subg (groupVr (subgP u)).
Definition subg_mul u v := Subg (groupM (subgP u) (subgP v)).
Lemma subg_oneP : left_id subg_one subg_mul.
Lemma subg_invP : left_inverse subg_one subg_inv subg_mul.
Lemma subg_mulP : associative subg_mul.
Definition subFinGroupMixin := FinGroup.Mixin subg_mulP subg_oneP subg_invP.
Canonical subBaseFinGroupType :=
Eval hnf in BaseFinGroupType subg_of subFinGroupMixin.
Canonical subFinGroupType := FinGroupType subg_invP.
Lemma sgvalM : {in setT &, {morph sgval : x y / x × y}}.
Lemma valgM : {in setT &, {morph val : x y / (x : subg_of) × y >-> x × y}}.
Definition subg : gT → subg_of := insubd (1 : subg_of).
Lemma subgK x : x \in G → val (subg x) = x.
Lemma sgvalK : cancel sgval subg.
Lemma subg_default x : (x \in G) = false → val (subg x) = 1.
Lemma subgM : {in G &, {morph subg : x y / x × y}}.
End OneGroup.
Hint Resolve group1 : core.
Lemma groupD1_inj G H : G^# = H^# → G :=: H.
Lemma invMG G H : (G × H)^-1 = H × G.
Lemma mulSGid G H : H \subset G → H × G = G.
Lemma mulGSid G H : H \subset G → G × H = G.
Lemma mulGidPl G H : reflect (G × H = G) (H \subset G).
Lemma mulGidPr G H : reflect (G × H = H) (G \subset H).
Lemma comm_group_setP G H : reflect (commute G H) (group_set (G × H)).
Lemma card_lcosets G H : #|lcosets H G| = #|G : H|.
Group Modularity equations
Lemma group_modl A B G : A \subset G → A × (B :&: G) = A × B :&: G.
Lemma group_modr A B G : B \subset G → (G :&: A) × B = G :&: A × B.
End GroupProp.
Hint Extern 0 (is_true (1%g \in _)) ⇒ apply: group1 : core.
Hint Extern 0 (is_true (0 < #|_|)) ⇒ apply: cardG_gt0 : core.
Hint Extern 0 (is_true (0 < #|_ : _|)) ⇒ apply: indexg_gt0 : core.
Notation "G :^ x" := (conjG_group G x) : Group_scope.
Notation "[ 'subg' G ]" := (subg_of G) : type_scope.
Notation "[ 'subg' G ]" := [set: subg_of G] : group_scope.
Notation "[ 'subg' G ]" := [set: subg_of G]%G : Group_scope.
Section GroupInter.
Variable gT : finGroupType.
Implicit Types A B : {set gT}.
Implicit Types G H : {group gT}.
Lemma group_setI G H : group_set (G :&: H).
Canonical setI_group G H := group (group_setI G H).
Section Nary.
Variables (I : finType) (P : pred I) (F : I → {group gT}).
Lemma group_set_bigcap : group_set (\bigcap_(i | P i) F i).
Canonical bigcap_group := group group_set_bigcap.
End Nary.
Canonical generated_group A : {group _} := Eval hnf in [group of <<A>>].
Canonical gcore_group G A : {group _} := Eval hnf in [group of gcore G A].
Canonical commutator_group A B : {group _} := Eval hnf in [group of [~: A, B]].
Canonical joing_group A B : {group _} := Eval hnf in [group of A <*> B].
Canonical cycle_group x : {group _} := Eval hnf in [group of <[x]>].
Definition joinG G H := joing_group G H.
Definition subgroups A := [set G : {group gT} | G \subset A].
Lemma order_gt0 (x : gT) : 0 < #[x].
End GroupInter.
Hint Resolve order_gt0 : core.
Notation "G :&: H" := (setI_group G H) : Group_scope.
Notation "<< A >>" := (generated_group A) : Group_scope.
Notation "<[ x ] >" := (cycle_group x) : Group_scope.
Notation "[ ~: A1 , A2 , .. , An ]" :=
(commutator_group .. (commutator_group A1 A2) .. An) : Group_scope.
Notation "A <*> B" := (joing_group A B) : Group_scope.
Notation "G * H" := (joinG G H) : Group_scope.
Notation "\prod_ ( i <- r | P ) F" :=
(\big[joinG/1%G]_(i <- r | P%B) F%G) : Group_scope.
Notation "\prod_ ( i <- r ) F" :=
(\big[joinG/1%G]_(i <- r) F%G) : Group_scope.
Notation "\prod_ ( m <= i < n | P ) F" :=
(\big[joinG/1%G]_(m ≤ i < n | P%B) F%G) : Group_scope.
Notation "\prod_ ( m <= i < n ) F" :=
(\big[joinG/1%G]_(m ≤ i < n) F%G) : Group_scope.
Notation "\prod_ ( i | P ) F" :=
(\big[joinG/1%G]_(i | P%B) F%G) : Group_scope.
Notation "\prod_ i F" :=
(\big[joinG/1%G]_i F%G) : Group_scope.
Notation "\prod_ ( i : t | P ) F" :=
(\big[joinG/1%G]_(i : t | P%B) F%G) (only parsing) : Group_scope.
Notation "\prod_ ( i : t ) F" :=
(\big[joinG/1%G]_(i : t) F%G) (only parsing) : Group_scope.
Notation "\prod_ ( i < n | P ) F" :=
(\big[joinG/1%G]_(i < n | P%B) F%G) : Group_scope.
Notation "\prod_ ( i < n ) F" :=
(\big[joinG/1%G]_(i < n) F%G) : Group_scope.
Notation "\prod_ ( i 'in' A | P ) F" :=
(\big[joinG/1%G]_(i in A | P%B) F%G) : Group_scope.
Notation "\prod_ ( i 'in' A ) F" :=
(\big[joinG/1%G]_(i in A) F%G) : Group_scope.
Section Lagrange.
Variable gT : finGroupType.
Implicit Types G H K : {group gT}.
Lemma LagrangeI G H : (#|G :&: H| × #|G : H|)%N = #|G|.
Lemma divgI G H : #|G| %/ #|G :&: H| = #|G : H|.
Lemma divg_index G H : #|G| %/ #|G : H| = #|G :&: H|.
Lemma dvdn_indexg G H : #|G : H| %| #|G|.
Theorem Lagrange G H : H \subset G → (#|H| × #|G : H|)%N = #|G|.
Lemma cardSg G H : H \subset G → #|H| %| #|G|.
Lemma lognSg p G H : G \subset H → logn p #|G| ≤ logn p #|H|.
Lemma piSg G H : G \subset H → {subset \pi(gval G) ≤ \pi(gval H)}.
Lemma divgS G H : H \subset G → #|G| %/ #|H| = #|G : H|.
Lemma divg_indexS G H : H \subset G → #|G| %/ #|G : H| = #|H|.
Lemma coprimeSg G H p : H \subset G → coprime #|G| p → coprime #|H| p.
Lemma coprimegS G H p : H \subset G → coprime p #|G| → coprime p #|H|.
Lemma indexJg G H x : #|G :^ x : H :^ x| = #|G : H|.
Lemma indexgg G : #|G : G| = 1%N.
Lemma rcosets_id G : rcosets G G = [set G : {set gT}].
Lemma Lagrange_index G H K :
H \subset G → K \subset H → (#|G : H| × #|H : K|)%N = #|G : K|.
Lemma indexgI G H : #|G : G :&: H| = #|G : H|.
Lemma indexgS G H K : H \subset K → #|G : K| %| #|G : H|.
Lemma indexSg G H K : H \subset K → K \subset G → #|K : H| %| #|G : H|.
Lemma indexg_eq1 G H : (#|G : H| == 1%N) = (G \subset H).
Lemma indexg_gt1 G H : (#|G : H| > 1) = ~~ (G \subset H).
Lemma index1g G H : H \subset G → #|G : H| = 1%N → H :=: G.
Lemma indexg1 G : #|G : 1| = #|G|.
Lemma indexMg G A : #|G × A : G| = #|A : G|.
Lemma rcosets_partition_mul G H : partition (rcosets H G) (H × G).
Lemma rcosets_partition G H : H \subset G → partition (rcosets H G) G.
Lemma LagrangeMl G H : (#|G| × #|H : G|)%N = #|G × H|.
Lemma LagrangeMr G H : (#|G : H| × #|H|)%N = #|G × H|.
Lemma mul_cardG G H : (#|G| × #|H| = #|G × H|%g × #|G :&: H|)%N.
Lemma dvdn_cardMg G H : #|G × H| %| #|G| × #|H|.
Lemma cardMg_divn G H : #|G × H| = (#|G| × #|H|) %/ #|G :&: H|.
Lemma cardIg_divn G H : #|G :&: H| = (#|G| × #|H|) %/ #|G × H|.
Lemma TI_cardMg G H : G :&: H = 1 → #|G × H| = (#|G| × #|H|)%N.
Lemma cardMg_TI G H : #|G| × #|H| ≤ #|G × H| → G :&: H = 1.
Lemma coprime_TIg G H : coprime #|G| #|H| → G :&: H = 1.
Lemma prime_TIg G H : prime #|G| → ~~ (G \subset H) → G :&: H = 1.
Lemma prime_meetG G H : prime #|G| → G :&: H != 1 → G \subset H.
Lemma coprime_cardMg G H : coprime #|G| #|H| → #|G × H| = (#|G| × #|H|)%N.
Lemma coprime_index_mulG G H K :
H \subset G → K \subset G → coprime #|G : H| #|G : K| → H × K = G.
End Lagrange.
Section GeneratedGroup.
Variable gT : finGroupType.
Implicit Types x y z : gT.
Implicit Types A B C D : {set gT}.
Implicit Types G H K : {group gT}.
Lemma subset_gen A : A \subset <<A>>.
Lemma sub_gen A B : A \subset B → A \subset <<B>>.
Lemma mem_gen x A : x \in A → x \in <<A>>.
Lemma generatedP x A : reflect (∀ G, A \subset G → x \in G) (x \in <<A>>).
Lemma gen_subG A G : (<<A>> \subset G) = (A \subset G).
Lemma genGid G : <<G>> = G.
Lemma genGidG G : <<G>>%G = G.
Lemma gen_set_id A : group_set A → <<A>> = A.
Lemma genS A B : A \subset B → <<A>> \subset <<B>>.
Lemma gen0 : <<set0>> = 1 :> {set gT}.
Lemma gen_expgs A : {n | <<A>> = (1 |: A) ^+ n}.
Lemma gen_prodgP A x :
reflect (∃ n, exists2 c, ∀ i : 'I_n, c i \in A & x = \prod_i c i)
(x \in <<A>>).
Lemma genD A B : A \subset <<A :\: B>> → <<A :\: B>> = <<A>>.
Lemma genV A : <<A^-1>> = <<A>>.
Lemma genJ A z : <<A :^z>> = <<A>> :^ z.
Lemma conjYg A B z : (A <*> B) :^z = A :^ z <*> B :^ z.
Lemma genD1 A x : x \in <<A :\ x>> → <<A :\ x>> = <<A>>.
Lemma genD1id A : <<A^#>> = <<A>>.
Notation joingT := (@joing gT) (only parsing).
Notation joinGT := (@joinG gT) (only parsing).
Lemma joingE A B : A <*> B = <<A :|: B>>.
Lemma joinGE G H : (G × H)%G = (G <*> H)%G.
Lemma joingC : commutative joingT.
Lemma joing_idr A B : A <*> <<B>> = A <*> B.
Lemma joing_idl A B : <<A>> <*> B = A <*> B.
Lemma joing_subl A B : A \subset A <*> B.
Lemma joing_subr A B : B \subset A <*> B.
Lemma join_subG A B G : (A <*> B \subset G) = (A \subset G) && (B \subset G).
Lemma joing_idPl G A : reflect (G <*> A = G) (A \subset G).
Lemma joing_idPr A G : reflect (A <*> G = G) (A \subset G).
Lemma joing_subP A B G :
reflect (A \subset G ∧ B \subset G) (A <*> B \subset G).
Lemma joing_sub A B C : A <*> B = C → A \subset C ∧ B \subset C.
Lemma genDU A B C : A \subset C → <<C :\: A>> = <<B>> → <<A :|: B>> = <<C>>.
Lemma joingA : associative joingT.
Lemma joing1G G : 1 <*> G = G.
Lemma joingG1 G : G <*> 1 = G.
Lemma genM_join G H : <<G × H>> = G <*> H.
Lemma mulG_subG G H K : (G × H \subset K) = (G \subset K) && (H \subset K).
Lemma mulGsubP K H G : reflect (K \subset G ∧ H \subset G) (K × H \subset G).
Lemma mulG_sub K H A : K × H = A → K \subset A ∧ H \subset A.
Lemma trivMg G H : (G × H == 1) = (G :==: 1) && (H :==: 1).
Lemma comm_joingE G H : commute G H → G <*> H = G × H.
Lemma joinGC : commutative joinGT.
Lemma joinGA : associative joinGT.
Lemma join1G : left_id 1%G joinGT.
Lemma joinG1 : right_id 1%G joinGT.
Canonical joinG_law := Monoid.Law joinGA join1G joinG1.
Canonical joinG_abelaw := Monoid.ComLaw joinGC.
Lemma bigprodGEgen I r (P : pred I) (F : I → {set gT}) :
(\prod_(i <- r | P i) <<F i>>)%G :=: << \bigcup_(i <- r | P i) F i >>.
Lemma bigprodGE I r (P : pred I) (F : I → {group gT}) :
(\prod_(i <- r | P i) F i)%G :=: << \bigcup_(i <- r | P i) F i >>.
Lemma mem_commg A B x y : x \in A → y \in B → [~ x, y] \in [~: A, B].
Lemma commSg A B C : A \subset B → [~: A, C] \subset [~: B, C].
Lemma commgS A B C : B \subset C → [~: A, B] \subset [~: A, C].
Lemma commgSS A B C D :
A \subset B → C \subset D → [~: A, C] \subset [~: B, D].
Lemma der1_subG G : [~: G, G] \subset G.
Lemma comm_subG A B G : A \subset G → B \subset G → [~: A, B] \subset G.
Lemma commGC A B : [~: A, B] = [~: B, A].
Lemma conjsRg A B x : [~: A, B] :^ x = [~: A :^ x, B :^ x].
End GeneratedGroup.
Section Cycles.
Elementary properties of cycles and order, needed in perm.v.
More advanced results on the structure of cyclic groups will
be given in cyclic.v.
Variable gT : finGroupType.
Implicit Types x y : gT.
Implicit Types G : {group gT}.
Import Monoid.Theory.
Lemma cycle1 : <[1]> = [1 gT].
Lemma order1 : #[1 : gT] = 1%N.
Lemma cycle_id x : x \in <[x]>.
Lemma mem_cycle x i : x ^+ i \in <[x]>.
Lemma cycle_subG x G : (<[x]> \subset G) = (x \in G).
Lemma cycle_eq1 x : (<[x]> == 1) = (x == 1).
Lemma orderE x : #[x] = #|<[x]>|.
Lemma order_eq1 x : (