Generating elements of groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-08-21.
Last modified on 2023-11-24.

module group-theory.generating-elements-groups where

Imports

open import commutative-algebra.commutative-rings

open import elementary-number-theory.integers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.identity-types
open import foundation.images
open import foundation.injective-maps
open import foundation.propositional-maps
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.surjective-maps
open import foundation.unit-type
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.addition-homomorphisms-abelian-groups
open import group-theory.commuting-elements-groups
open import group-theory.conjugation
open import group-theory.endomorphism-rings-abelian-groups
open import group-theory.free-groups-with-one-generator
open import group-theory.full-subgroups
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.integer-multiples-of-elements-abelian-groups
open import group-theory.integer-powers-of-elements-groups
open import group-theory.isomorphisms-abelian-groups
open import group-theory.normal-subgroups
open import group-theory.quotient-groups
open import group-theory.subgroups-generated-by-elements-groups
open import group-theory.subsets-groups
open import group-theory.trivial-group-homomorphisms

open import ring-theory.integer-multiples-of-elements-rings
open import ring-theory.rings
open import ring-theory.transporting-ring-structure-along-isomorphisms-abelian-groups

Idea

An element $g$ of a group G is said to be a generating element if the unique morphism g̃ : ℤ → G equipped with an identification g̃(1) = g is surjective. Equivalently, g is a generating element if the subgroup ⟨g⟩ of G generated by the element g is the full subgroup of G. We give in total four different characterizations of the notion of generating element:

The subgroup generated by the element g is full.
The full subgroup of G is generated by the element g.
The group homomorphism g̃ : ℤ → G mapping 1 to g is surjective.
The evaluation map hom(G,H) → H at g is an embedding for every group H.

Of these four equivalent characterizations, we take the first as our standard definition.

We note that the concept of group equipped with a generating element is subtly different from the concept of cyclic group. Groups equipped with generating elements have a specified generating element as part of their structure, whereas cyclic groups are groups with the property that there exists a generating element.

Furthermore, we show that for any group G equipped with a generating element, the evaluation map hom(G,G) → G is an equivalence. Since groups equipped with a generating element are abelian, it follows that hom(G,G) is the endomorphism ring of an abelian group. The evaluation map on an endomorphism ring is always a group homomorphism, so it follows from the isomorphism

  hom(G,G) ≅ G

that any group equipped with a generating element is in fact a commutative ring. Here we see another difference between groups equipped with a specified generating element and cyclic groups: Equipping a cyclic group with the structure of a commutative ring amounts to equipping the cyclic group with a specified generating element, which corresponds to the unit element of the commutative ring structure.

Definitions