# Cyclic groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-07-20.

module group-theory.cyclic-groups where

Imports
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.identity-types
open import foundation.inhabited-subtypes
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.generating-elements-groups
open import group-theory.groups


## Idea

A group G is said to be cyclic if it is generated by a single element, i.e., if there exists an element g : G such that the group homomorphism

  g̃ : ℤ → G


equipped with an identification g̃(1) ＝ g is surjective

## Definitions

### Cyclic groups

#### The standard definition of cyclic groups

module _
{l1 : Level} (G : Group l1)
where

is-cyclic-prop-Group : Prop l1
is-cyclic-prop-Group =
∃ (type-Group G) (is-generating-element-prop-Group G)

is-cyclic-Group : UU l1
is-cyclic-Group = type-Prop is-cyclic-prop-Group

is-prop-is-cyclic-Group : is-prop is-cyclic-Group
is-prop-is-cyclic-Group = is-prop-type-Prop is-cyclic-prop-Group

Cyclic-Group : (l : Level) → UU (lsuc l)
Cyclic-Group l = type-subtype (is-cyclic-prop-Group {l})

module _
{l : Level} (C : Cyclic-Group l)
where

group-Cyclic-Group : Group l
group-Cyclic-Group = pr1 C

is-cyclic-Cyclic-Group : is-cyclic-Group group-Cyclic-Group
is-cyclic-Cyclic-Group = pr2 C

set-Cyclic-Group : Set l
set-Cyclic-Group = set-Group group-Cyclic-Group

type-Cyclic-Group : UU l
type-Cyclic-Group = type-Group group-Cyclic-Group

zero-Cyclic-Group : type-Cyclic-Group
zero-Cyclic-Group = unit-Group group-Cyclic-Group

add-Cyclic-Group : (x y : type-Cyclic-Group) → type-Cyclic-Group

neg-Cyclic-Group : type-Cyclic-Group → type-Cyclic-Group
neg-Cyclic-Group = inv-Group group-Cyclic-Group

(x y z : type-Cyclic-Group) →

(x y : type-Cyclic-Group) →
apply-universal-property-trunc-Prop
( is-cyclic-Cyclic-Group)
( λ (g , u) →
commutative-mul-is-generating-element-Group group-Cyclic-Group g u x y)

ab-Cyclic-Group : Ab l
pr1 ab-Cyclic-Group = group-Cyclic-Group


#### The definition where G has a generating element

module _
{l1 : Level} (G : Group l1)
where

has-generating-element-prop-Group : Prop l1
has-generating-element-prop-Group =
is-inhabited-subtype-Prop (generating-element-Group G)

has-generating-element-Group : UU l1
has-generating-element-Group = type-Prop has-generating-element-prop-Group


## Properties

### A group is cyclic if and only if it has a generating element

module _
{l1 : Level} (G : Group l1)
where

is-cyclic-has-generating-element-Group :
is-cyclic-Group G →
{l : Level} →
exists-structure
( type-Group G)
( λ g → is-emb-ev-element-hom-Group' G g l)
is-cyclic-has-generating-element-Group H {l} =
apply-universal-property-trunc-Prop H
( exists-structure-Prop
( type-Group G)
( λ g → is-emb-ev-element-hom-Group' G g l))
( λ (g , u) →
intro-exists g (is-emb-ev-element-is-generating-element-Group G g u))


• In group-theory.generating-elements-groups we show that groups equipped with a generating element are isomorphic to their endomorphism rings. Furthermore, the multiplicative structure of these rings is commutative, so that groups equipped with a generating element are also equipped with the structure of a commutative ring.
ConceptFile
Acyclic mapssynthetic-homotopy-theory.acyclic-maps
Acyclic typessynthetic-homotopy-theory.acyclic-types
Acyclic undirected graphsgraph-theory.acyclic-undirected-graphs
Braceletsunivalent-combinatorics.bracelets
The category of cyclic ringsring-theory.category-of-cyclic-rings
The circlesynthetic-homotopy-theory.circle
Connected set bundles over the circlesynthetic-homotopy-theory.connected-set-bundles-circle
Cyclic finite typesunivalent-combinatorics.cyclic-finite-types
Cyclic groupsgroup-theory.cyclic-groups
Cyclic higher groupshigher-group-theory.cyclic-higher-groups
Cyclic ringsring-theory.cyclic-rings
Cyclic typesstructured-types.cyclic-types
Euler's totient functionelementary-number-theory.eulers-totient-function
Finitely cyclic mapselementary-number-theory.finitely-cyclic-maps
Generating elements of groupsgroup-theory.generating-elements-groups
Hatcher's acyclic typesynthetic-homotopy-theory.hatchers-acyclic-type
Homomorphisms of cyclic ringsring-theory.homomorphisms-cyclic-rings
Infinite cyclic typessynthetic-homotopy-theory.infinite-cyclic-types
Multiplicative units in the standard cyclic ringselementary-number-theory.multiplicative-units-standard-cyclic-rings
Necklacesunivalent-combinatorics.necklaces
Polygonsgraph-theory.polygons
The poset of cyclic ringsring-theory.poset-of-cyclic-rings
Standard cyclic groups (ℤ/k)elementary-number-theory.standard-cyclic-groups
Standard cyclic rings (ℤ/k)elementary-number-theory.standard-cyclic-rings