Cyclic groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-07-20.
Last modified on 2024-04-11.

module group-theory.cyclic-groups where

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
  add-Cyclic-Group = mul-Group group-Cyclic-Group

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

  associative-add-Cyclic-Group :
    (x y z : type-Cyclic-Group) →
    add-Cyclic-Group (add-Cyclic-Group x y) z ＝
    add-Cyclic-Group x (add-Cyclic-Group y z)
  associative-add-Cyclic-Group = associative-mul-Group group-Cyclic-Group

  commutative-add-Cyclic-Group :
    (x y : type-Cyclic-Group) →
    add-Cyclic-Group x y ＝ add-Cyclic-Group y x
  commutative-add-Cyclic-Group x y =
    apply-universal-property-trunc-Prop
      ( is-cyclic-Cyclic-Group)
      ( Id-Prop set-Cyclic-Group (add-Cyclic-Group x y) (add-Cyclic-Group y x))
      ( λ (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
  pr2 ab-Cyclic-Group = commutative-add-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))

See also

• 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.

Table of files related to cyclic types, groups, and rings

Recent changes

• 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
• 2023-10-09. Egbert Rijke. Navigation tables for all files related to cyclic types, groups, and rings (#823).
• 2023-09-15. Egbert Rijke. update contributors, remove unused imports (#772).
• 2023-09-10. Egbert Rijke and Fredrik Bakke. Cyclic groups (#723).
• 2023-08-21. Egbert Rijke and Fredrik Bakke. Cyclic groups (#697).