Example Definitions Finite Groups - Mizar
Table of Contents
1. Introduction
This is a collection of definitions I intend to formalize in Mizar. The hard part of the formalizations is the proof of existence and uniqueness (or other correctness conditions).
We provide the proof skeletons for most of the relevant definitions, but do not provide proofs.
2. Extra-special groups
Rotman's Introduction to the Theory of Groups, 4th ed, defines on page 124:
Let \(G\) be a finite \(p\) -group. We call it Extra-special if \(Z(G)\) is cyclic and \(\Phi(G)=Z(G)=G'\).
This defines an attribute (hinted by being of the form "We call it <adjective>
if…"). Its formalization is straightforward.
definition
let p be prime Nat;
let IT be finite p-group Group;
attr IT is extra-special means
:Def:
(center IT is cyclic) & (Phi(IT) = center IT) &
(center IT = IT`);
end;
3. G Has Characteristic p
These definitions are taken from arXiv:1906.07216.
3.1. p-Local Subgroups
Let \(p\) be a prime number, \(G\) be a finite group whose order is divisible by \(p\). A $p$-local subgroup is one that looks like \(N_{H}(P)\) where \(P\) is a nontrivial $p$-subgroup of \(G\).
My intuition is that this definition introduces an attribute "$p$-local" for subgroups.
definition
let p be Nat;
let G be finite Group such that p divides card G;
let IT be Subgroup of G;
attr IT is p-local means
:Def:
p is prime &
ex P being p-group Subgroup of G
st P is non trivial & the multMagma of IT = Normalizer P;
end;
Since subgroup equality is defined only for strict subgroups, we cannot
say IT = Normalizer P without making IT a strict Subgroup of G. (The
normalizer of a subgroup is defined to be a strict subgroup.) For this
reason, we needed to check the multMagma of IT = Normalizer P.
Also, I am not sure if we need p to be prime; it's just those are
the cases we care about.
This also requires the following registrations:
registration
let G be Group;
cluster trivial for Subgroup of G;
existence
proof
take H = (1).G;
thus thesis;
end;
let p be Nat;
cluster p-group for Subgroup of G;
existence
proof
take H = (1).G;
A4: card H = 1 by GROUP_6:11
.= p |^ 0 by NEWTON:4;
hence thesis by GROUP_10:def 17;
end;
cluster trivial p-group for Subgroup of G;
existence
proof
take H = (1).G;
A4: card H = 1 by GROUP_6:11
.= p |^ 0 by NEWTON:4;
hence thesis by GROUP_10:def 17;
end;
end;
3.2. Subgroup has Characteristic p
Let \(p\) be a prime number, \(G\) be a finite group, \(L\leq G\) be a subgroup. We say \(L\) has Characteristic \(p\) if \(C_{G}(O_{p}(L))\leq O_{p}(L)\).
This introduces a new predicate, has_characteristic p for a subgroup.
definition
let p be prime Nat;
let G be Group;
let L be Subgroup of G;
pred L has_characteristic p means
:Def:
Centralizer (p-core L) is Subgroup of (p-core L);
end;
3.3. Group has local characteristic p
Let \(p\) be a prime number, \(G\) be a finite group. We say \(G\) has local Characteristic \(p\) if if for all $p$-local subgroups \(L\) of \(G\) has characteristic \(p\).
(A special case when \(p = 2\), we just say that \(G\) has even Characteristic.)
definition
let p be prime Nat;
let G be finite Group;
pred G has_local_characteristic p means
:Def:
for L being Subgroup of G st L is p-local holds L has_characteristic p;
end;
3.4. Group has characteristic p
From page ix of The Local Structure Theorem For Finite Groups With A Large p-Subgroup:
A finite group \(G\) has characteristic \(p\) if \(C_{G}(O_{p}(G))\leq O_{p}(G)\).
I would interpret this as a predicate (using the general heuristic "has <noun>"
is a predicate).
definition
let p be prime Nat;
let G be finite Group;
pred G has_characteristic p means
:Def:
Centralizer (p-core G) is Subgroup of (p-core G);
end;
notation
let G be finite Group;
synonym G has_even_characteristic for G has_characteristic 2;
end;
4. Parabolic Subgroup
Let \(G\) be a finite group. Any subgroup of \(G\) containing a Sylow p-subgroup of \(G\) is a parabolic subgroup of \(G\).
This defines an attribute "parabolic" for "Subgroup of \(G\)". We need to
use the Mizar predicate is_Sylow_p-subgroup_of_prime to do the heavy lifting:
definition
let p be prime Nat;
let G be finite Group;
let IT be Subgroup of G;
attr IT is parabolic means
:Def:
ex P being Subgroup of G st P is_Sylow_p-subgroup_of_prime p &
P is Subgroup of IT;
end;
I believe this definition of "parabolic" is nonstandard. For finite linear algebraic groups, this does not match the notion of parabolic subgroups there. Instead the nonstandard definition is analogous, using the analogy that Sylow p-subgroups "are like" maximal tori (since they're conjugate to each other). A parabolic subgroup contains a maximal torus.
Let \(p\) be a prime number, \(G\) be a finite group. We say \(G\) has parabolic characteristic \(p\) if every $p$-local parabolic subgroup of \(G\) has characteristic \(p\).
This defines a predicate (whenever a gadget "has <property>", it
defines a predicate).
definition
let p be prime Nat;
let G be finite Group;
pred G has_parabolic_characteristic p means
:Def:
for H being parabolic Subgroup of G st H is p-local
holds H has_characteristic p;
end;
5. Finite Group Theory
5.1. Sections of a Group
Kurzweill and Stellmacher's Theory of Finite Groups § 1.3 concludes with a brief definition in passing:
Let \(G\) be a group, \(N\trianglelefteq H\leq G\). We call the quotient \(H/N\) a Section of \(G\).
In particular, \(N\) is a normal subgroup of \(H\) (viz., \(N\) is not necessarily a normal subgroup of \(G\)).
This appears to define a new mode (as hinted by "<bork> of \(G\)").
However not all groups have a section (the quaternions famously do
not).
Consequently, we need to define this as a predicate.
definition
let K,G be Group;
pred K is_section_of G means :Def:
ex H being Subgroup of G st
ex N being normal Subgroup of H st
K = H./.N;
end;
Note: we may need to change the denominator to (H,N)`*` which will
"cast" N as a normal subgroup of H.
We also have a related notion "\(G\) is involved in \(K\)" means \(G\) is isomorphic to a section of \(K\). This is a transitive relation.
6. Exponent of Group
Let \(G\) be a group. Its Exponent is the least natural number \(n\in\mathbb{N}\) such that every \(g\in G\) satisfies \(g^{n}=1_{G}\). If there is an element of order 0 in the group, then the exponent of \(G\) is defined to be 0.
definition
let G be Group;
func exponent G -> Nat means
:Def:
it = 0 if ex g being Element of G st g is being_of_order_0
otherwise it > 0 &
for g being Element of G
holds g |^ it = 1_G &
(for n being Nat st g |^ n = 1_G holds it <= n);
existence
proof
thus (ex g being Element of G st g is being_of_order_0) implies
(ex k being Nat st k = 0);
thus (for g being Element of G holds not g is being_of_order_0) implies
(ex k being Nat st k > 0 &
for g being Element of G
holds g |^ k = 1_G & (for n being Nat st g |^ n = 1_G holds k <= n));
end;
uniqueness
proof
defpred P[Element of Nat] means $1 > 0 &
for g being Element of G
holds g |^ ($1) = 1_G & (for n being Nat st g |^ n = 1_G holds ($1) <= n);
let k1,k2 be Nat;
thus (ex g being Element of G st g is being_of_order_0) & k1 = 0 & k2 = 0
implies k1 = k2;
thus (for g being Element of G holds not g is being_of_order_0) & P[k1] & P[k2]
implies k1 = k2;
end;
consistency;
end;
7. Elementary Abelian Group
Aschbacher's Finite Group Theory nicely defines an elementary Abelian group right before §1.13:
Let \(p\) be a prime number, we define an Elementary Abelian \(p\) -Group to be an Abelian \(p\) -Group of exponent \(p\).
Luckily, groupp_1 defines p-commutative-group and which does a lot of
heavy lifting for us.
definition
let p be prime Nat;
let IT be finite Group;
attr IT is p-elementary_Abelian means
:Def:
IT is p-commutative-group & exponent IT = p;
end;
:: Kurzweil & Stellmacher, _Theory of Finite Groups_, Thm 5.2.6
theorem
for G being p-elementary_Abelian Group
holds Phi(G) is trivial;
:: Kurzweil & Stellmacher, _Theory of Finite Groups_, Thm 5.2.7 (a)
theorem
for P being p-group Group
holds P./.Phi(P) is p-elementary_Abelian Group;
We will also want to define the \(p\) rank of a finite group. This would
be the largest expon of the p-elementary_Abelian subgroups of G.
7.1. p-Rank of a Group
Let \(G\) be a group, \(p\) be a prime. The \(p\) -rank of \(G\) is the maximum rank of all elementary Abelian \(p\) -subgroups of \(G\).
This is only really well-defined if \(G\) is a finite group whose order is divisible by \(p\), or if there exists an element whose order is divisible by \(p\). Since we only really care about the \(p\) -rank for finite groups, we can restrict our definition to finite groups.
definition
let p be prime Nat;
let G be finite Group;
func p-rank G means
:Def:
it > 0 & for E being Subgroup of G
st E is p-elementary_Abelian
holds expon(E,p) <= it &
(for n being Nat
st n > 0 & expon(E,p) <= n
holds it <= n)
if p divides card G
otherwise it = 0;
existence
proof
defpred P[Nat] means
($1) > 0 & for E being Subgroup of G
st E is p-elementary_Abelian
holds expon(E,p) <= ($1) &
(for n being Nat st n > 0 & expon(E,p) <= n
holds ($1) <= n);
thus p divides card G implies ex k being Nat st P[k];
thus not p divides card G implies ex k being Nat st k=0;
end;
uniqueness
proof
defpred P[Nat] means
($1) > 0 & for E being Subgroup of G
st E is p-elementary_Abelian
holds expon(E,p) <= ($1) &
(for n being Nat st n > 0 & expon(E,p) <= n
holds ($1) <= n);
let k1,k2 be Nat;
thus p divides card G & P[k1] & P[k2] holds k1 = k2;
thus not (p divides card G) & (k1 = 0) & (k2 = 0) implies k1 = k2;
end;
consistency;
end;
notation
let p be prime Nat, G be finite Group;
synonym p-depth G for p-rank G;
end;
7.2. Depth of Group
Let \(G\) be a finite group. The Depth (or Rank) of \(G\) is the largest \(p\) -rank of the group, for all primes \(p\).
We will run into a "name collision" in homological algebra, since "rank" has a technical meaning there, and we need to use group cohomology later on.
definition
let G be finite Group;
func depth G -> Nat means
for p being prime Nat
holds p-rank G <= it & (for n being Nat
st p-rank G <= n
holds it <= n);
existence
proof
thus ex k being Nat st
for p being prime Nat
holds p-rank G <= k &
(for n being Nat st p-rank G <= n holds k <= n);
end;
uniqueness
proof
defpred P[Nat] means for p being prime Nat
holds p-rank G <= ($1) & (for n being Nat
st p-rank G <= n
holds ($1) <= n);
thus for k1,k2 being Nat st P[k1] & P[k2] holds k1=k2;
end;
end;
theorem
for G being trivial Group
for p being prime Nat
holds p-rank G = 0;
7.3. Thin and Quasithin groups
There is a way to measure the "size" of a finite group, \(e(G)\in\mathbb{N}_{0}\), defined as the largest \(p\) -rank (for odd primes \(p\)) among all the 2-local subgroups of \(G\).
- Aschbacher, in his "Groups of Characteristic 2-Type" refers to \(e(G) = \max\{m_{2,p}(G) : p\mbox{ odd prime}\}\) as the Rank of \(G\).
- Gorenstein's article, "Classification theory of finite simple groups" (1980) refers to \(e(G)\) as odd 2-local rank of \(G\). He also notes: "By a theorem of Frobenius, \(G\) has a normal 2-complement if \(e(G) = 0\), so \(e(G)\) is always positive in a simple group."
definition
let G be finite Group;
func odd_2-local_rank G -> Nat means
for p being odd prime Nat
for M being Subgroup of G
st M is 2-local
holds p-rank M <= it &
(for n being Nat
st p-rank M <= n
holds it <= n);
existence
proof
defpred P[Nat] means for p being odd prime Nat
for M being Subgroup of G
st M is 2-local
holds p-rank M <= ($1) &
(for n being Nat
st p-rank M <= n
holds ($1) <= n);
thus ex eG being Nat st P[eG];
end;
uniqueness
proof
defpred P[Nat] means for p being odd prime Nat
for M being Subgroup of G
st M is 2-local
holds p-rank M <= ($1) &
(for n being Nat
st p-rank M <= n
holds ($1) <= n);
thus for k1,k2 being Nat st P[k1] & P[k2] holds k1=k2;
end;
end;
This requires the following registration:
registration
cluster odd for prime Nat;
existence
proof
A1: 3 is prime by PEPIN:41;
3 = 2*1+1;
then 3 is odd by ABIAN:1;
hence thesis by A1,PEPIN:17;
end;
end;
We can now define thin and quasithin groups. They are defined using the maximum \(p\) -rank (over all odd prime \(p\)) for 2-local subgroups of \(G\).
definition
let IT be finite Group;
attr IT is thin means
:Def:
odd_2-local_rank IT <= 1;
attr IT is quasithin means
:Def:
odd_2-local_rank IT <= 2;
:: Aschbacher & Smith, Classification of Quasithin Groups, I, pg 4
attr IT is strongly_quasithin means
:Def:
for p being odd prime Nat
holds p-rank IT <= 2;
end;
theorem the trivial Group is thin;
theorem the trivial Group is quasithin;
registration
cluster thin finite Group
existence
proof
take the trivial Group;
hence thesis;
end;
cluster quasithin finite Group
existence
proof
take the trivial Group;
hence thesis;
end;
end;
registration
cluster thin -> quasithin finite Group;
coherence
proof
thus for G being finite Group st G is thin holds G is quasithin;
end;
end;
8. Feit-Thompson Odd-Order Theorem
The statement is quite easy:
theorem
for G being finite Group
st card G is odd
holds G is solvable;
The proof has been revised and can be found spanning two books:
- Helmut Bender and George Glauberman,
Local Analysis for the Odd Order Theorem.
Cambridge University Press, 1995. - Thomas Peterfalvi,
Character Theory for the Odd Order Theorem.
Cambridge University Press, 2000.
The main dependency seems to be the first 7 chapters of I. Martin Isaacs's Character Theory of Finite Groups, which Dover has reprinted in 1994.
9. Group Extensions
Group extensions are ambiguously used in the literature. Sometimes it refers to a short exact sequence \(1\to A\to E\to G\to 1\), other times it refers to the group \(E\), other times it is the surjective morphism \(E\to G\) from the short exact sequence. Bourbaki defines a group extension in definition 1 (Algebra ch. I §6.1) as:
Let \(F\) and \(G\) be two groups. A Extension of \(G\) by \(F\) is a triple \(\mathcal{E} = (E,i\colon F\hookrightarrow E, p\colon E\to G)\) where \(E\) is a group, \(i\colon F\hookrightarrow E\) is an injective group morphism, and \(p\colon E\to G\) is a surjective group morphism such that \(\mathrm{Im}(i)=\mathrm{Ker}(p)\).
This seems like something which should be considered after formalizing Homological Algebra (or during its formalization)…
theorem Th1:
for G being Group
for H being Subgroup of G
ex f being Homomorphism of H,G
st (for h being Element of H holds f.h = h) & f is one-to-one &
Image f = the multMagma of H;
::> *4
definition
let G be Group;
mode Extension of G -> Group means :Def:
ex A being Group st
ex f being Homomorphism of A,it st
ex p being Homomorphism of it,G
st Image f is Subgroup of Ker p &
f is one-to-one & p is onto;
existence
proof
thus ex E being Group st
ex A being Group st
ex f being Homomorphism of A,E st
ex p being Homomorphism of E,G
st Image f is Subgroup of Ker p &
f is one-to-one & p is onto
proof
take E=G;
take A=(1).G;
consider f being Homomorphism of A,E such that
A1: for g being Element of A holds f.g = g and
A2: f is one-to-one and
A3: Image f = the multMagma of A
by Th1;
take f;
reconsider p=id G as Homomorphism of E,G by GROUP_6:38;
id the carrier of G is onto;
then A4: p is onto;
(1).(Ker p) = (1).G by GROUP_2:63;
then (1).G is Subgroup of Ker p;
then Image f is Subgroup of Ker p by A3;
hence thesis by A2,A3;
end;
end;
end;
definition
let G be Group;
mode CentralExtension of G -> Group means :Def:
ex A being Group st
ex f being Homomorphism of A,it st
ex p being Homomorphism of it,G
st Image f is Subgroup of Ker p & Image f is Subgroup of center it &
f is one-to-one & p is onto;
existence
proof
thus ex E being Group st
ex A being Group st
ex f being Homomorphism of A,E st
ex p being Homomorphism of E,G
st Image f is Subgroup of Ker p &
Image f is Subgroup of center E &
f is one-to-one & p is onto
proof
take E=G;
take A=(1).G;
consider f being Homomorphism of A,E such that
A1: for g being Element of A holds f.g = g and
A2: f is one-to-one and
A3: Image f = the multMagma of A
by Th1;
take f;
reconsider p=id G as Homomorphism of E,G by GROUP_6:38;
id the carrier of G is onto;
then A4: p is onto;
(1).(Ker p) = (1).G by GROUP_2:63;
then (1).G is Subgroup of Ker p;
then A5: Image f is Subgroup of Ker p by A3;
(1).(center E) = (1).G by GROUP_2:63;
then (1).G is Subgroup of center E;
then Image f is Subgroup of center E by A3;
hence thesis by A2,A3,A5;
end;
end;
end;