Algebra in Lean

3 Subgroups

3.1 Defining the Subgroup

Definition 3.1
#

Let \(G\) be a group. A subgroup \(H\) of \(G\) is a subset that is itself a group under the group operation of \(G\). This requires that the subgroup satisfies three operations.

  1. The identity of \(G\) is contained within \(H\).

  2. \(H\) must be closed under \(G\)’s group operation: for any \(a,b \in H\), \(\mu (a,b) \in H\).

  3. \(H\) must be closed under \(G\)’s inversion operation: for any \(a \in H\), \(\iota (a) \in H\).

Definition 3.2
#

For any group \(G\), the maximal subgroup \(H\) is the group that contains every element of \(G\).

Definition 3.3
#

For any group \(G\), the minimal subgroup \(H\) is the group that contains exclusively the identity of \(G\).

3.2 The Power Function

Let \(M\) be a monoid and \(G\) be a group.

Definition 3.4
#

For \(x \in M\), the \(n\)th power of \(x\) (where \(n \in \mathbb {N}\)) is defined as the left-multiplication of \(x\) with the identity of \(M\) \(n\) times. It is defined inductively below

\begin{equation*} x^n := \begin{cases} \mathbb {e}, & n = 0 \\ \mu (x^{n-1}, x), & n ~ {\gt}~ 0 \end{cases}\end{equation*}
Definition 3.5
#

For a group \(G\) and \(x \in G\), we extend the domain of the power function to include all of \(\mathbb {Z}\) such that if \(n ~ {\lt}~ 0\), then \(x^n\) is equal to \(\iota (x^{-n})\). It is defined inductively below:

\begin{equation*} x^n := \begin{cases} \mathbb {e}, & n = 0 \\ \mu (x^{n-1}, x), & n ~ {\gt}~ 0 \\ \iota (\mu (x^{n+1}, x)), & n ~ {\lt}~ 0 \end{cases}\end{equation*}

3.3 Order

Definition 3.6
#

Let \(M\) be a monoid and \(x \in M\). Then the order of \(x\), denoted \(|x|\), is the smallest \(n \in \mathbb {N}\) satisfying \(x^n = \mathbb {e}\). If no such \(n\) exists, then we define the order of \(x\) to be zero.

Theorem 3.7

Let \(G\) be a group and \(x \in G\). Suppose that for two integers \(m\) and \(n\), \(x^m = x^n\). Then \(m \equiv n\) (mod \(|x|\)). Note that if two integers are equivalent mod 0, then they are equal, implying that if \(|x| = 0\), then the power function over \(\mathbb {Z}\) is injective.

3.4 Generators and the Cyclic Group

Theorem 3.8
#

Inclusion (\(\subseteq \)) forms a partial order over the set of all subgroups of \(G\).

Definition 3.9
#

The subgroup of \(G\) generated by a subset \(S \subset G\) is defined to be the smallest subgroup containing all of \(S\). Notated \(\langle S \rangle \), it is written as

\begin{equation*} \langle S \rangle := \bigcap _{\genfrac {}{}{0pt}{}{G \le H}{S \subset H}} H \end{equation*}
Definition 3.10
#

For a group \(G\), the power subgroup of \(x \in G\) is defined as

\[ \text{Pows}(x) := \left\{ x^n \middle | n \in \mathbb {Z} \right\} \]

For the following theorems, let \(G\) be a group and let \(x \in G\).

Theorem 3.11

\(\text{Pows}(x) = \langle \{ x\} \rangle \).

Theorem 3.12

\(|\text{Pows}(x)| = |x|\).

3.5 More Examples of Subgroups

Definition 3.13
#

Let \(\phi : G \rightarrow G'\) be a group homomorphism. The kernel of \(\phi \), denoted \(\text{ker}(\phi )\), is defined as

\[ \left\{ x \in G \middle | \phi (x) = \mathbb {e} \right\} . \]

This definition implicitly encodes that the kernel of a group homomorphism is a subgroup of \(G\).

Definition 3.14
#

Let \(\phi : G \rightarrow G'\) be a group homomorphism. The kernel of \(\phi \), denoted \(\text{img}(\phi )\), is defined as

\[ \left\{ y \in G' \middle | \exists \, x,\; \phi (x) = y \right\} . \]

This definition implicitly encodes that the image of a group homomorphism is a subgroup of \(G'\).

Definition 3.15
#

A subgroup \(H\) of a group \(G\) is normal if a subgroup is closed under conjugation of any element in \(G\). In other terms, for any \(g \in G\) and \(h \in H\), \(ghg^{-1} \in H\).

Theorem 3.16

The minimal subgroup of \(G\) is a normal subgroup of \(G\).

Theorem 3.17

The maximal subgroup of \(G\) is a normal subgroup of \(G\).

Theorem 3.18

If \(\phi \) is a group homomorphism with domain \(G\), then \(ker(\phi )\) is a normal subgroup of \(G\).

Definition 3.19
#

Let \(G\) be a group, \(g \in G\) and \(S \subset G\). Then we define the conjugate of \(S\) by \(g\) to be

\begin{equation*} gSg^{-1} := \left\{ gsg^{-1} \middle | s \in S \right\} \end{equation*}
Definition 3.20
#

Let \(G\) be a group and \(S \subset G\). The normalizer in \(G\) of \(S\), denoted \(N_G(S)\), is defined as

\[ N_G(S) := \left\{ x \in G \middle | gSg^{-1} = S \right\} . \]

Implicit in this definition is that the normalizer is a subgroup of \(G\).

Definition 3.21
#

Let \(G\) be a group and \(S \subset G\). The centralizer in \(G\) of \(S\), denoted \(C_G(S)\), is defined as

\[ C_G(S) := \left\{ x \in G \middle | gs = sg\; \forall \; s \in S\right\} . \]

Implicit in this definition is that the centralizer is a subgroup of \(G\).

Definition 3.22
#

The center of \(G\), denoted \(Z(G)\), is the set of all elements that commute with every element of \(G\), or \(C_G(G)\).

Theorem 3.23

If \(\phi : G \rightarrow G'\) is a group homomorphism, then it is injective if and only if \(\text{ker}(\phi )\) is trivial, meaning \(\text{ker}(\phi ) = \{ \mathbb {e}\} \).