open import Algebra.Group.Instances.Symmetric
open import Algebra.Group.Instances.Integers
open import Algebra.Group.Cat.Base
open import Algebra.Group.Subgroup
open import Algebra.Group.Ab
open import Algebra.Group

open import Cat.Prelude

open import Data.Int.Divisible
open import Data.Int.Universal
open import Data.Fin.Closure
open import Data.Int.DivMod
open import Data.Fin
open import Data.Int hiding (Positive)
open import Data.Nat

open represents-subgroup
open normal-subgroup
open is-group-hom

module Algebra.Group.Instances.Cyclic where

private module ℤ = Group-on (ℤ .snd) hiding (magma-hlevel)

Cyclic groups🔗

We say that a group is cyclic if it is generated by a single element $g\text{:}$ that is, every element of the group can be written as some integer power of $g$¹.

_is-generated-by_ : ∀ {ℓ} (G : Group ℓ) (g : ⌞ G ⌟) → Type ℓ
G is-generated-by g = ∀ x → ∃[ n ∈ Int ] x ≡ pow G g n

is-cyclic : ∀ {ℓ} (G : Group ℓ) → Type ℓ
is-cyclic G = ∃[ g ∈ G ] G is-generated-by g

module _ {ℓ} (G : Group ℓ) (open Group-on (G .snd)) where
  inverse-generates
    : ∀ g → G is-generated-by g → G is-generated-by g ⁻¹
  inverse-generates g gen x = gen x <&> λ (n , p) → negℤ n , (
    x                     ≡⟨ p ⟩≡
    pow G g n             ≡˘⟨ inv-inv ⟩≡˘
    pow G g n ⁻¹ ⁻¹       ≡˘⟨ ap _⁻¹ (pres-inv (pow-hom G g .preserves) {lift n}) ⟩≡˘
    pow G g (negℤ n) ⁻¹   ≡˘⟨ pow-inverse G g (negℤ n) ⟩≡˘
    pow G (g ⁻¹) (negℤ n) ∎)

The obvious example is the infinite cyclic group $\mathbb{Z}$ of the (additive) integers generated by $1\text{,}$ but there is also a finite cyclic group of order $n$ for every $n\ge 1\text{.}$ As it turns out, we can construct all the cyclic groups using the same machine: the quotient group $\mathbb{Z}/n\mathbb{Z}\text{,}$ where $n\mathbb{Z}$ is the normal subgroup of multiples of $n\text{,}$ is the cyclic group of order $n$ when $n\ge 1\text{,}$ and is the infinite cyclic group when $n=0\text{.}$

infix  _·ℤ
_·ℤ : ∀ (n : Nat) → normal-subgroup ℤ λ i → el (n ∣ℤ i) (∣ℤ-is-prop n i)
(n ·ℤ) .has-rep .has-unit = ∣ℤ-zero
(n ·ℤ) .has-rep .has-⋆ = ∣ℤ-+
(n ·ℤ) .has-rep .has-inv = ∣ℤ-negℤ
(n ·ℤ) .has-conjugate {x} {y} = subst (n ∣ℤ_) x≡y+x-y
  where
    x≡y+x-y : x ≡ y +ℤ (x -ℤ y)
    x≡y+x-y =
      x                  ≡⟨ ℤ.insertl {y} (ℤ.inverser {x = y}) ⟩≡
      y +ℤ (negℤ y +ℤ x) ≡⟨ ap (y +ℤ_) (+ℤ-commutative (negℤ y) x) ⟩≡
      y +ℤ (x -ℤ y)      ∎

infix  ℤ/_
ℤ/_ : Nat → Group lzero
ℤ/ n = ℤ /ᴳ n ·ℤ

$\mathbb{Z}/n\mathbb{Z}$ is an abelian group, since the commutativity of addition descends to the quotient.

ℤ/n-commutative : ∀ n → is-commutative-group (ℤ/ n)
ℤ/n-commutative n = elim! λ x y → ap inc (+ℤ-commutative x y)

infix  ℤ-ab/_
ℤ-ab/_ : Nat → Abelian-group lzero
ℤ-ab/_ n = from-commutative-group (ℤ/ n) (ℤ/n-commutative n)

Furthermore, $\mathbb{Z}/n\mathbb{Z}$ is, by construction, cyclic, and is generated by $1\text{.}$

module _ (n : Nat) where
  open Group-on ((ℤ/ n) .snd)

  ℤ/n-cyclic : is-cyclic (ℤ/ n)
  ℤ/n-cyclic = inc ( , gen) where
    gen : ℤ/ n is-generated-by 
    gen = elim! λ x → inc (x , Integers.induction Int-integers
      {P = λ x → inc x ≡ pow (ℤ/ n)  x}
      refl
      (λ x →
        inc x        ≡ pow (ℤ/ n)  x        ≃⟨ _ , equiv→cancellable (⋆-equivr ) ⟩≃
        inc x ⋆     ≡ pow (ℤ/ n)  x ⋆     ≃⟨ ∙-pre-equiv (sym (ap inc (+ℤ-oner x))) ⟩≃
        inc (sucℤ x) ≡ pow (ℤ/ n)  x ⋆     ≃⟨ ∙-post-equiv (sym (pow-sucr (ℤ/ n)  x)) ⟩≃
        inc (sucℤ x) ≡ pow (ℤ/ n)  (sucℤ x) ≃∎)
      x)

We prove the following mapping-out property for $\mathbb{Z}/n\mathbb{Z}\text{:}$ a group homomorphism $\mathbb{Z}/n\mathbb{Z}\to G$ is uniquely determined by an element $x:G$ of order $n\text{,}$ i.e. such that $x^n=1\text{.}$ Note that this condition is trivially satisfied if $n=0\text{,}$ so we don’t need a special case.

This follows from the fact that a group homomorphism $\mathbb{Z}\to G$ out of the group of integers is uniquely determined by an element of $G\text{,}$ and some basic algebra.

module _
  (n : Nat)
  {ℓ} {G : Group ℓ} (open Group-on (G .snd))
  (x : ⌞ G ⌟) (open pow G x renaming (pow to infixr  x^_; pow-hom to x^-))
  (wraps : x^ pos n ≡ unit)
  where

  ℤ/-out : Groups.Hom (LiftGroup ℓ (ℤ/ n)) G
  ℤ/-out .hom (lift i) = Coeq-rec (apply x^- ⊙ lift) (λ (a , b , n∣a-b) → zero-diff $
    let k , k*n≡a-b = ∣ℤ→fibre n∣a-b in
    x^ a — x^ b          ≡˘⟨ pres-diff (x^- .preserves) {lift a} {lift b} ⟩≡˘
    x^ (a -ℤ b)          ≡˘⟨ ap x^_ k*n≡a-b ⟩≡˘
    x^ (k *ℤ pos n)      ≡⟨ ap x^_ (*ℤ-commutative k (pos n)) ⟩≡
    x^ (pos n *ℤ k)      ≡⟨ pow-* G x (pos n) k ⟩≡
    pow G ⌜ x^ pos n ⌝ k ≡⟨ ap! wraps ⟩≡
    pow G unit k         ≡⟨ pow-unit G k ⟩≡
    unit                 ∎)
    i
  ℤ/-out .preserves .pres-⋆ = elim! λ x y →
    x^- .preserves .pres-⋆ (lift x) (lift y)

We can check that $\mathbb{Z}/0\mathbb{Z}\equiv \mathbb{Z}\text{:}$

ℤ-ab/0≡ℤ-ab : ℤ-ab/  ≡ ℤ-ab
ℤ-ab/0≡ℤ-ab = ∫-Path
  (total-hom
    (Coeq-rec (λ z → z) (λ (_ , _ , p) → ℤ.zero-diff p))
    (record { pres-⋆ = elim! λ _ _ → refl }))
  (is-iso→is-equiv (iso inc (λ _ → refl) (elim! λ _ → refl)))

ℤ/0≡ℤ : ℤ/  ≡ ℤ
ℤ/0≡ℤ = Grp→Ab→Grp (ℤ/ ) (ℤ/n-commutative ) ∙ ap Abelian→Group ℤ-ab/0≡ℤ-ab

For positive $n\text{,}$ we show that $\mathbb{Z}/n\mathbb{Z}$ is finite; more precisely, we construct an equivalence $\mathbb{Z}/n\mathbb{Z}\simeq {\mathbb{N}}^{<n}$ which sends $x:\mathbb{Z}$ to the representative of its congruence class modulo $n\text{,}$ $x\%n\text{.}$

ℤ/n≃ℕ<n : ∀ n → .⦃ Positive n ⦄ → ⌞ ℤ/ n ⌟ ≃ ℕ< n
ℤ/n≃ℕ<n n .fst = Coeq-rec (λ i → i %ℤ n , x%ℤy<y i n)
  λ (x , y , p) → Σ-prop-path! (divides-diff→same-rem n x y p)
ℤ/n≃ℕ<n n .snd = is-iso→is-equiv $ iso
  (λ (i , p) → inc (pos i))
  (λ i → Σ-prop-path! (ℕ<-%ℤ i))
  (elim! λ i → quot (same-rem→divides-diff n (pos (i %ℤ n)) i
    (ℕ<-%ℤ (_ , x%ℤy<y i n))))

Finite-ℤ/n : ∀ n → .⦃ Positive n ⦄ → ⌞ ℤ/ n ⌟ ≃ Fin n
Finite-ℤ/n n = ℤ/n≃ℕ<n n ∙e Fin≃ℕ< e⁻¹

Using this and the fact that $([2]\simeq [2])\simeq [2!]=[2]\text{,}$ we can check that $\mathbb{Z}/2\mathbb{Z}$ is isomorphic to the symmetric group $S_2\text{.}$ We start by defining a homomorphism $\mathbb{Z}/2\mathbb{Z}\to S_2$ that sends 1 to the equivalence $[2]\simeq [2]$ that swaps the two elements, which corresponds to $1:[2!]\text{.}$

ℤ/2→S₂ : Groups.Hom (ℤ/ ) (S )
ℤ/2→S₂ = ℤ/-out  (Equiv.from (Fin-permutations ) )
  (Equiv.injective (Fin-permutations ) refl)
  Groups.∘ G→LiftG (ℤ/ )

In order to conclude the proof, we show that the function $f:\mathbb{Z}/2\mathbb{Z}\to S_2$ thus defined is an equivalence, by showing that it factors as in the following diagram and using the two-out-of-three property of equivalences:

ℤ/2≡S₂ : ℤ/  ≡ S 
ℤ/2≡S₂ = ∫-Path ℤ/2→S₂ $
  equiv-cancell (Fin-permutations  .snd)
    (equiv-cancelr ((Finite-ℤ/n  e⁻¹) .snd)
      (subst is-equiv (ext λ where
        fzero → refl
        (fsuc fzero) → refl)
      id-equiv))