- -

Library mathcomp.fingroup.fingroup

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- 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). -

-Module GroupScope.
-Open Scope group_scope.
-End GroupScope.
-Import GroupScope.
- -
-

- -

- 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 "#[ x ]" (at level 0, format "#[ x ]").
-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
-}.
- -
-

- -

- 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))
-}.
- -
-

- -

- 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.
- -
-

- -

- 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.
- -
-

- -

- 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. -

-Variable gT : baseFinGroupType.
-Implicit Types A B : {set gT }.
- -
-

- -

- Set-lifted group operations. -

- -
-Definition set_mulg A B := mulg @2: (A , B ).
-Definition set_invg A := invg @^-1: A.
- -
-

- -

- 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 ).
- -
-

- -

- 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 ).
- -
-

- -

- "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.
- -
-

- -

- 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. -

-Variable gT : baseFinGroupType.
-Implicit Types A B C D : {set gT }.
-Implicit Type x y z : gT.
- -
-

- -

- 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 -

-Variable gT : finGroupType.
-Implicit Types A B C D : {set gT }.
-Implicit Type x y z : gT.
- -
-

- -

- 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 -

-Lemma invg_lcosets A B : (lcosets A B )^-1 = rcosets A ^-1 B ^-1.
- -
-

- -

- 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.
- -
-

- -

- 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.
- -
-

- -

- 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.
- -
-

- -

- 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 <>.
- -
-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 <>.
- -
-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 <*> <> = 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 >> = <> → <<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 : (#[x ] == 1%N) = (x == 1).
- -
-Lemma order_gt1 x : (#[x ] > 1) = (x != 1).
- -
-Lemma cycle_traject x : <[x ]> =i traject (mulg x) 1 #[x ].
- -
-Lemma cycle2g x : #[x ] = 2 → <[x ]> = [set 1; x ].
- -
-Lemma cyclePmin x y : y \in <[x ]> → {i | i < #[x ] & y = x ^+ i }.
- -
-Lemma cycleP x y : reflect (∃ i, y = x ^+ i) (y \in <[x ]>).
- -
-Lemma expg_order x : x ^+ #[x ] = 1.
- -
-Lemma expg_mod p k x : x ^+ p = 1 → x ^+ (k %% p ) = x ^+ k.
- -
-Lemma expg_mod_order x i : x ^+ (i %% #[x ]) = x ^+ i.
- -
-Lemma invg_expg x : x ^-1 = x ^+ #[x ].-1.
- -
-Lemma invg2id x : #[x ] = 2 → x ^-1 = x.
- -
-Lemma cycleX x i : <[x ^+ i ]> \subset <[x ]>.
- -
-Lemma cycleV x : <[x ^-1 ]> = <[x ]>.
- -
-Lemma orderV x : #[x ^-1 ] = #[x ].
- -
-Lemma cycleJ x y : <[x ^ y ]> = <[x ]> :^ y.
- -
-Lemma orderJ x y : #[x ^ y ] = #[x ].
- -
-End Cycles.
- -
-Section Normaliser.
- -
-Variable gT : finGroupType.
-Implicit Types x y z : gT.
-Implicit Types A B C D : {set gT }.
-Implicit Type G H K : {group gT }.
- -
-Lemma normP x A : reflect (A :^ x = A) (x \in 'N (A )).
- -
-Lemma group_set_normaliser A : group_set 'N (A ).
- -
-Canonical normaliser_group A := group (group_set_normaliser A).
- -
-Lemma normsP A B : reflect {in A , normalised B } (A \subset 'N (B )).
- -
-Lemma memJ_norm x y A : x \in 'N (A ) → (y ^ x \in A ) = (y \in A ).
- -
-Lemma norms_cycle x y : (<[y ]> \subset 'N (<[x ]>)) = (x ^ y \in <[x ]>).
- -
-Lemma norm1 : 'N (1) = setT :> {set gT }.
- -
-Lemma norms1 A : A \subset 'N (1).
- -
-Lemma normCs A : 'N (~: A ) = 'N (A ).
- -
-Lemma normG G : G \subset 'N (G ).
- -
-Lemma normT : 'N ([set : gT ]) = [set : gT ].
- -
-Lemma normsG A G : A \subset G → A \subset 'N (G ).
- -
-Lemma normC A B : A \subset 'N (B ) → commute A B.
- -
-Lemma norm_joinEl G H : G \subset 'N (H ) → G <*> H = G × H.
- -
-Lemma norm_joinEr G H : H \subset 'N (G ) → G <*> H = G × H.
- -
-Lemma norm_rlcoset G x : x \in 'N (G ) → G :* x = x *: G.
- -
-Lemma rcoset_mul G x y : x \in 'N (G ) → (G :* x ) × (G :* y ) = G :* (x × y ).
- -
-Lemma normJ A x : 'N (A :^ x ) = 'N (A ) :^ x.
- -
-Lemma norm_conj_norm x A B :
- x \in 'N (A ) → (A \subset 'N (B :^ x )) = (A \subset 'N (B )).
- -
-Lemma norm_gen A : 'N (A ) \subset 'N (<<A >>).
- -
-Lemma class_norm x G : G \subset 'N (x ^: G ).
- -
-Lemma class_normal x G : x \in G → x ^: G <| G.
- -
-Lemma class_sub_norm G A x : G \subset 'N (A ) → (x ^: G \subset A ) = (x \in A ).
- -
-Lemma class_support_norm A G : G \subset 'N (class_support A G ).
- -
-Lemma class_support_sub_norm A B G :
- A \subset G → B \subset 'N (G ) → class_support A B \subset G.
- -
-Section norm_trans.
- -
-Variables (A B C D : {set gT }).
-Hypotheses (nBA : A \subset 'N (B )) (nCA : A \subset 'N (C )).
- -
-Lemma norms_gen : A \subset 'N (<>).
- -
-Lemma norms_norm : A \subset 'N ('N (B )).
- -
-Lemma normsI : A \subset 'N (B :&: C ).
- -
-Lemma normsU : A \subset 'N (B :|: C ).
- -
-Lemma normsIs : B \subset 'N (D ) → A :&: B \subset 'N (C :&: D ).
- -
-Lemma normsD : A \subset 'N (B :\: C ).
- -
-Lemma normsM : A \subset 'N (B × C ).
- -
-Lemma normsY : A \subset 'N (B <*> C ).
- -
-Lemma normsR : A \subset 'N ([~: B , C ]).
- -
-Lemma norms_class_support : A \subset 'N (class_support B C ).
- -
-End norm_trans.
- -
-Lemma normsIG A B G : A \subset 'N (B ) → A :&: G \subset 'N (B :&: G ).
- -
-Lemma normsGI A B G : A \subset 'N (B ) → G :&: A \subset 'N (G :&: B ).
- -
-Lemma norms_bigcap I r (P : pred I) A (B_ : I → {set gT }) :
- A \subset \bigcap_(i <- r | P i ) 'N (B_ i ) →
- A \subset 'N (\bigcap_(i <- r | P i ) B_ i ).
- -
-Lemma norms_bigcup I r (P : pred I) A (B_ : I → {set gT }) :
- A \subset \bigcap_(i <- r | P i ) 'N (B_ i ) →
- A \subset 'N (\bigcup_(i <- r | P i ) B_ i ).
- -
-Lemma normsD1 A B : A \subset 'N (B ) → A \subset 'N (B ^#).
- -
-Lemma normD1 A : 'N (A ^#) = 'N (A ).
- -
-Lemma normalP A B : reflect (A \subset B ∧ {in B , normalised A }) (A <| B).
- -
-Lemma normal_sub A B : A <| B → A \subset B.
- -
-Lemma normal_norm A B : A <| B → B \subset 'N (A ).
- -
-Lemma normalS G H K : K \subset H → H \subset G → K <| G → K <| H.
- -
-Lemma normal1 G : 1 <| G.
- -
-Lemma normal_refl G : G <| G.
- -
-Lemma normalG G : G <| 'N (G ).
- -
-Lemma normalSG G H : H \subset G → H <| 'N_G (H ).
- -
-Lemma normalJ A B x : (A :^ x <| B :^ x ) = (A <| B ).
- -
-Lemma normalM G A B : A <| G → B <| G → A × B <| G.
- -
-Lemma normalY G A B : A <| G → B <| G → A <*> B <| G.
- -
-Lemma normalYl G H : (H <| H <*> G ) = (G \subset 'N (H )).
- -
-Lemma normalYr G H : (H <| G <*> H ) = (G \subset 'N (H )).
- -
-Lemma normalI G A B : A <| G → B <| G → A :&: B <| G.
- -
-Lemma norm_normalI G A : G \subset 'N (A ) → G :&: A <| G.
- -
-Lemma normalGI G H A : H \subset G → A <| G → H :&: A <| H.
- -
-Lemma normal_subnorm G H : (H <| 'N_G (H )) = (H \subset G ).
- -
-Lemma normalD1 A G : (A ^# <| G ) = (A <| G ).
- -
-Lemma gcore_sub A G : gcore A G \subset A.
- -
-Lemma gcore_norm A G : G \subset 'N (gcore A G ).
- -
-Lemma gcore_normal A G : A \subset G → gcore A G <| G.
- -
-Lemma gcore_max A B G : B \subset A → G \subset 'N (B ) → B \subset gcore A G.
- -
-Lemma sub_gcore A B G :
- G \subset 'N (B ) → (B \subset gcore A G ) = (B \subset A ).
- -
-

- -

- An elementary proof that subgroups of index 2 are normal; it is almost as - short as the "advanced" proof using group actions; besides, the fact that - the coset is equal to the complement is used in extremal.v. -

-Lemma rcoset_index2 G H x :
- H \subset G → #|G : H | = 2 → x \in G :\: H → H :* x = G :\: H.
- -
-Lemma index2_normal G H : H \subset G → #|G : H | = 2 → H <| G.
- -
-Lemma cent1P x y : reflect (commute x y) (x \in 'C [y ]).
- -
-Lemma cent1id x : x \in 'C [x ].
- -
-Lemma cent1E x y : (x \in 'C [y ]) = (x × y == y × x ).
- -
-Lemma cent1C x y : (x \in 'C [y ]) = (y \in 'C [x ]).
- -
-Canonical centraliser_group A : {group _} := Eval hnf in [group of 'C (A )].
- -
-Lemma cent_set1 x : 'C ([set x ]) = 'C [x ].
- -
-Lemma cent1J x y : 'C [x ^ y ] = 'C [x ] :^ y.
- -
-Lemma centP A x : reflect (centralises x A) (x \in 'C (A )).
- -
-Lemma centsP A B : reflect {in A , centralised B } (A \subset 'C (B )).
- -
-Lemma centsC A B : (A \subset 'C (B )) = (B \subset 'C (A )).
- -
-Lemma cents1 A : A \subset 'C (1).
- -
-Lemma cent1T : 'C (1) = setT :> {set gT }.
- -
-Lemma cent11T : 'C [1] = setT :> {set gT }.
- -
-Lemma cent_sub A : 'C (A ) \subset 'N (A ).
- -
-Lemma cents_norm A B : A \subset 'C (B ) → A \subset 'N (B ).
- -
-Lemma centC A B : A \subset 'C (B ) → commute A B.
- -
-Lemma cent_joinEl G H : G \subset 'C (H ) → G <*> H = G × H.
- -
-Lemma cent_joinEr G H : H \subset 'C (G ) → G <*> H = G × H.
- -
-Lemma centJ A x : 'C (A :^ x ) = 'C (A ) :^ x.
- -
-Lemma cent_norm A : 'N (A ) \subset 'N ('C (A )).
- -
-Lemma norms_cent A B : A \subset 'N (B ) → A \subset 'N ('C (B )).
- -
-Lemma cent_normal A : 'C (A ) <| 'N (A ).
- -
-Lemma centS A B : B \subset A → 'C (A ) \subset 'C (B ).
- -
-Lemma centsS A B C : A \subset B → C \subset 'C (B ) → C \subset 'C (A ).
- -
-Lemma centSS A B C D :
- A \subset C → B \subset D → C \subset 'C (D ) → A \subset 'C (B ).
- -
-Lemma centI A B : 'C (A ) <*> 'C (B ) \subset 'C (A :&: B ).
- -
-Lemma centU A B : 'C (A :|: B ) = 'C (A ) :&: 'C (B ).
- -
-Lemma cent_gen A : 'C (<<A >>) = 'C (A ).
- -
-Lemma cent_cycle x : 'C (<[x ]>) = 'C [x ].
- -
-Lemma sub_cent1 A x : (A \subset 'C [x ]) = (x \in 'C (A )).
- -
-Lemma cents_cycle x y : commute x y → <[x ]> \subset 'C (<[y ]>).
- -
-Lemma cycle_abelian x : abelian <[x ]>.
- -
-Lemma centY A B : 'C (A <*> B ) = 'C (A ) :&: 'C (B ).
- -
-Lemma centM G H : 'C (G × H ) = 'C (G ) :&: 'C (H ).
- -
-Lemma cent_classP x G : reflect (x ^: G = [set x ]) (x \in 'C (G )).
- -
-Lemma commG1P A B : reflect ([~: A , B ] = 1) (A \subset 'C (B )).
- -
-Lemma abelianE A : abelian A = (A \subset 'C (A )).
- -
-Lemma abelian1 : abelian [1 gT ].
- -
-Lemma abelianS A B : A \subset B → abelian B → abelian A.
- -
-Lemma abelianJ A x : abelian (A :^ x) = abelian A.
- -
-Lemma abelian_gen A : abelian <<A >> = abelian A.
- -
-Lemma abelianY A B :
- abelian (A <*> B) = [&& abelian A , abelian B & B \subset 'C (A )].
- -
-Lemma abelianM G H :
- abelian (G × H) = [&& abelian G , abelian H & H \subset 'C (G )].
- -
-Section SubAbelian.
- -
-Variable A B C : {set gT }.
-Hypothesis cAA : abelian A.
- -
-Lemma sub_abelian_cent : C \subset A → A \subset 'C (C ).
- -
-Lemma sub_abelian_cent2 : B \subset A → C \subset A → B \subset 'C (C ).
- -
-Lemma sub_abelian_norm : C \subset A → A \subset 'N (C ).
- -
-Lemma sub_abelian_normal : (C \subset A ) = (C <| A ).
- -
-End SubAbelian.
- -
-End Normaliser.
- -
- -
- -
-Notation "''N' ( A )" := (normaliser_group A) : Group_scope.
-Notation "''C' ( A )" := (centraliser_group A) : Group_scope.
-Notation "''C' [ x ]" := (normaliser_group [set x%g]) : Group_scope.
-Notation "''N_' G ( A )" := (setI_group G 'N (A)) : Group_scope.
-Notation "''C_' G ( A )" := (setI_group G 'C (A)) : Group_scope.
-Notation "''C_' ( G ) ( A )" := (setI_group G 'C (A))
- (only parsing) : Group_scope.
-Notation "''C_' G [ x ]" := (setI_group G 'C [x]) : Group_scope.
-Notation "''C_' ( G ) [ x ]" := (setI_group G 'C [x])
- (only parsing) : Group_scope.
- -
-Hint Extern 0 (is_true (_ \subset _)) ⇒ apply: normG : core.
-Hint Extern 0 (is_true (_ <| _)) ⇒ apply: normal_refl : core.
- -
-Section MinMaxGroup.
- -
-Variable gT : finGroupType.
-Implicit Types gP : pred {group gT }.
- -
-Definition maxgroup A gP := maxset (fun A ⇒ group_set A && gP <<A >>%G) A.
-Definition mingroup A gP := minset (fun A ⇒ group_set A && gP <<A >>%G) A.
- -
-Variable gP : pred {group gT }.
- -
-Lemma ex_maxgroup : (∃ G, gP G ) → {G : {group gT } | maxgroup G gP }.
- -
-Lemma ex_mingroup : (∃ G, gP G ) → {G : {group gT } | mingroup G gP }.
- -
-Variable G : {group gT }.
- -
-Lemma mingroupP :
- reflect (gP G ∧ ∀ H, gP H → H \subset G → H :=: G) (mingroup G gP).
- -
-Lemma maxgroupP :
- reflect (gP G ∧ ∀ H, gP H → G \subset H → H :=: G) (maxgroup G gP).
- -
-Lemma maxgroupp : maxgroup G gP → gP G.
- -
-Lemma mingroupp : mingroup G gP → gP G.
- -
-Hypothesis gPG : gP G.
- -
-Lemma maxgroup_exists : {H : {group gT } | maxgroup H gP & G \subset H }.
- -
-Lemma mingroup_exists : {H : {group gT } | mingroup H gP & H \subset G }.
- -
-End MinMaxGroup.
- -
- -
-Notation "[ 'max' A 'of' G | gP ]" :=
- (maxgroup A (fun G : {group _} ⇒ gP)) : group_scope.
-Notation "[ 'max' G | gP ]" := [max gval G of G | gP] : group_scope.
-Notation "[ 'max' A 'of' G | gP & gQ ]" :=
- [max A of G | gP && gQ] : group_scope.
-Notation "[ 'max' G | gP & gQ ]" := [max G | gP && gQ] : group_scope.
-Notation "[ 'min' A 'of' G | gP ]" :=
- (mingroup A (fun G : {group _} ⇒ gP)) : group_scope.
-Notation "[ 'min' G | gP ]" := [min gval G of G | gP] : group_scope.
-Notation "[ 'min' A 'of' G | gP & gQ ]" :=
- [min A of G | gP && gQ] : group_scope.
-Notation "[ 'min' G | gP & gQ ]" := [min G | gP && gQ] : group_scope.
-