Example Definitions Finite Groups - Mizar

1. Introduction
2. Extra-special groups
3. G Has Characteristic p
4. Parabolic Subgroup
5. Finite Group Theory
- 5.1. Sections of a Group
6. Exponent of Group
7. Elementary Abelian Group
8. Feit-Thompson Odd-Order Theorem
9. Group Extensions

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;