From ed05182cece6bb3706e09b2ce14af4a41a2e8141 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Apr 2018 10:54:22 +0200 Subject: generate the documentation for 1.7 --- docs/htmldoc/mathcomp.fingroup.fingroup.html | 3038 ++++++++++++++++++++++++++ 1 file changed, 3038 insertions(+) create mode 100644 docs/htmldoc/mathcomp.fingroup.fingroup.html (limited to 'docs/htmldoc/mathcomp.fingroup.fingroup.html') diff --git a/docs/htmldoc/mathcomp.fingroup.fingroup.html b/docs/htmldoc/mathcomp.fingroup.fingroup.html new file mode 100644 index 0000000..c406f39 --- /dev/null +++ b/docs/htmldoc/mathcomp.fingroup.fingroup.html @@ -0,0 +1,3038 @@ + + + + + +mathcomp.fingroup.fingroup + + + + +
+ + + +
+ +

Library mathcomp.fingroup.fingroup

+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
+ Distributed under the terms of CeCILL-B.                                  *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ +
+ 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 rT.
+Canonical choiceType := Choice.Pack class rT.
+Canonical countType := Countable.Pack class rT.
+Canonical finType := Finite.Pack class rT.
+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.
+ +
+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.
+ +
+
+ +
+ Loads of silly variants to placate the incompleteness of trivial. + An alternative would be to upgrade done, pending better support + in the ssreflect ML code. +
+
+Notation gTr := (FinGroup.sort gT).
+Notation Gcl := (pred_of_set G : pred gTr).
+Lemma group1_class1 : (1 : gTr) \in G.
+Lemma group1_class2 : 1 \in Gcl.
+Lemma group1_class12 : (1 : gTr) \in Gcl.
+Lemma group1_eqType : (1 : gT : eqType) \in G.
+Lemma group1_finType : (1 : gT : finType) \in G.
+ +
+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|.
+
+ +
+ Workaround for the fact that the simple matching used by Trivial does not + always allow conversion. In particular cardG_gt0 always fails to apply to + subgoals that have been simplified (by /=) because type inference in the + notation #|G| introduces redexes of the form + Finite.sort (arg_finGroupType (FinGroup.base gT)) + which get collapsed to Fingroup.arg_sort (FinGroup.base gT). +
+
+Definition cardG_gt0_reduced : 0 < card (@mem gT (predPredType gT) G)
+  := cardG_gt0.
+ +
+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. +
+
+ +
+CoInductive 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.
+ +
+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.
+ +
+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 Resolve group1 group1_class1 group1_class12 group1_class12.
+Hint Resolve group1_eqType group1_finType.
+Hint Resolve cardG_gt0 cardG_gt0_reduced indexg_gt0.
+ +
+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.
+ +
+ +
+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 : (#[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(<<B>>).
+ +
+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 Resolve normG normal_refl.
+ +
+Section MinMaxGroup.
+ +
+Variable gT : finGroupType.
+Variable gP : pred {group gT}.
+ +
+Definition maxgroup := maxset (fun A ⇒ group_set A && gP <<A>>).
+Definition mingroup := minset (fun A ⇒ group_set A && gP <<A>>).
+ +
+Lemma ex_maxgroup : (∃ G, gP G) → {G : {group gT} | maxgroup G}.
+ +
+Lemma ex_mingroup : (∃ G, gP G) → {G : {group gT} | mingroup G}.
+ +
+Variable G : {group gT}.
+ +
+Lemma mingroupP :
+  reflect (gP G ∧ ∀ H, gP H → H \subset G → H :=: G) (mingroup G).
+ +
+Lemma maxgroupP :
+  reflect (gP G ∧ ∀ H, gP H → G \subset H → H :=: G) (maxgroup G).
+ +
+Lemma maxgroupp : maxgroup G → gP G.
+ +
+Lemma mingroupp : mingroup G → gP G.
+ +
+Hypothesis gPG : gP G.
+ +
+Lemma maxgroup_exists : {H : {group gT} | maxgroup H & G \subset H}.
+ +
+Lemma mingroup_exists : {H : {group gT} | mingroup H & H \subset G}.
+ +
+End MinMaxGroup.
+ +
+Notation "[ 'max' A 'of' G | gP ]" :=
+  (maxgroup (fun G : {group _} ⇒ gP) A) : 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 (fun G : {group _} ⇒ gP) A) : 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.
+ +
+
+
+ + + +
+ + + \ No newline at end of file -- cgit v1.2.3