Dependencies

An abelian group is a group with the commutative property: \(\forall a,~ b \in G, ~ \mu (a,~ b) = \mu (b,~ a)\)

An automorphism is a bijective endomorphism; i.e. an isomorphism from a group \( G \) to itself.

A bijective function is one that is both injective and surjective.

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

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

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

\(C_n\) is the generalization of \(C_3\), and is therefore the group of rotations of a regular n-gon. It uses mathlib’s Fin n type, and addition on that type. Since Fin allows modular arithmetic, rotations that are seperated by a multiple of \(360^{\circ }\) are treated as equal. Similarly to \(C_3\), the identity is a \(0^{\circ }\) rotation, and the inverse of an \(x ^{\circ }\) rotation is a \((360 - x)^{\circ }\) rotation.

A commutative monoid is a monoid with the commutative property: \(\forall a,~ b \in G, ~ \mu (a, b) = \mu (b, a)\)

Two elements \( a,~ b \) of a group \( G \) are conjugates if there exists another element \( g \) in \( G \) such that \( b = gag^{-1} \) (i.e.,  \( \mu (\mu (g,~ a),~ \iota (g)) \) ).

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

\(C_3\) is the group of rotational symmetries of an equilateral triangle with the group operation being the composition of symmetries. This is treated as an inductive type with three elements. The identity is a \( 0 ^{\circ } \) rotation, and the inverse of an \(x ^{\circ } \) rotation is a \((360 - x)^{\circ } \) rotation.

\(D_n\) is the dihedral group of order \(2n\). This is the group of all symmetries of a regular n-gon. This includes n rotations and n reflections. It is represented by a pair of a boolean and an element of Fin n. The boolean represents whether the element is a rotation or not, and the element of Fin n represents how much the first vertex is rotated. The identity is a \(0^{\circ }\) rotation, the inverse of an \(x^{\circ }\) rotation is a \((360 - x)^{\circ }\) rotation, and any reflection is its own inverse.

An endomorphism is a homomorphism \( \phi \) mapping from a group \( G \) to itself.

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

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:

A group is a nonempty set \(G\) with a closed binary operation (\(\mu : G \times G \rightarrow G\)), satisfying the following group axioms:

• Associativity: \(\forall \, a, b, c \in G, ~ \mu (\mu (a, b), c) = \mu (a, \mu (b, c))\)

• Identity element: \(\mathbb {e}\in G\) where \(\forall \, a \in G, ~ \mu (a, \mathbb {e}) = \mu (\mathbb {e}, a) = a\)

• Inverses (\(\iota \)): \(\forall \, a \in G, ~ \mu (\iota (a), a) = \mathbb {e}\)

A homomorphism is a map \( \phi \) from a group \( G \) to a group \( H \), for elements \( g,~ h \in G \), \( \phi \) is a homomorphism if and only if:

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

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

Given a function \( f \) mapping from a set \( X \) to a set \( Y \):

Otherwise known as a “one-to-one” function.

\((\mathbb {Z},~ +)\), the integers over addition, form a group, The identity of the group is \(0\), and the inverse of an element \(x \in \mathbb {Z}\) is \(-x\).

An isomorphism \( \phi \) from a group \( G \) to a group \( H \) is a bijective homomorphism.

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

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

A magma is a set G with an operation \(\mu : G \rightarrow G \rightarrow G\)

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

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

A monoid is a semigroup with an identity \(\mathbb {e}\) where \(\forall a \in G, ~ \mu (a, \mathbb {e}) = \mu (\mathbb {e},~ a) = a\)

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

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

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

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

A group has the left cancellation property \(\forall a,~ b,~ c \in G, ~ \mu (a,~ b) = \mu (a,~ c) \Rightarrow b = c\)

A group has the right cancellation property \(\forall a, ~ b, ~ c \in G,~ \mu (b,~ a) = \mu (c,~ a) \Rightarrow b = c\)

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.

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

A semigroup is a magma with the associative property: \(\forall a,~ b,~ c \in G, ~ \mu (\mu (a, b), c) = \mu (a,~ \mu (b, c))\)

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

Given a function \( f \) mapping from a set \( X \) to a set \( Y \):

Otherwise known as an “onto” function.

\(S_n\), the symmetric group of order \(n!\), is the set of all permutations of \(n\) elements. It is represented as the set of all bijections from Fin n to Fin n, with function composition as the group operation. The identity is the identity function, and the inverse of a group element is its inverse function (which exists since all bijections are invertible).

Given a group \( G \) and an element \( a \in G \), conjugation by \( a \) is an automorphism.

\(D_3\) is the first example we’ve seen of a nonabelian group.

Suppose \( \phi : G \rightarrow H \) is a homomorphism. Then \( \phi (\mathbb e) = \mathbb e \).

Suppose \( \phi : G \rightarrow H \) is a homomorphism. If \(g \in G \), then \( \phi (\iota (g)) = \iota (\phi (g)) \).

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

In a monoid, the identity element is unique: \(\forall a \in G, ~ (\forall b \in G, ~ \mu (a,~ b) = \mu (b,~ a) = b) \Rightarrow a = \mathbb {e}\)

The inverse of a product is the product of the inverses in reverse order: \(\forall a,~ b \in G,~ \iota (\mu (a,~ b)) = \mu (\iota (b),~ \iota (a))\)

The inverse of the identity is itself: \(\iota (\mathbb {e}) = \mathbb {e}\)

The inverse of the inverse of an element is that element: \(\forall a \in G,~ \iota (\iota (a)) = a\)

In a group, each element has a unique inverse: \(\forall a,~ b \in G,~ (\mu (a,~ b) = \mu (b,~ a) = \mathbb {e}) \Rightarrow b = \iota (a)\)

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

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

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

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.

Applying the group operation to an element and its inverse returns the identity: \(\forall a \in G, ~ \mu (a, \iota (a)) = \mathbb {e}\)

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

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

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