<!--
```agda
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
```
-->

```agda
module Algebra.Group.Instances.Cyclic where
```

<!--
```agda
private module ℤ = Group-on (ℤ .snd) hiding (magma-hlevel)
```
-->

# Cyclic groups {defines="cyclic-group"}

We say that a [[group]] is **cyclic** if it is generated by a single
element $g$: that is, every element of the group can be written as some
integer power of $g$^[Some authors (namely, Bourbaki) call such groups
*monogeneous*, and reserve "cyclic" for the *finite* cyclic groups.].

```agda
_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
```

::: note
Generators are not unique, so we must use $\exists$ to get a [[proposition]].
In fact, if $g$ generates $G$, then so does $g^{-1}$, hence a non-trivial
cyclic group has at least two generators!

```agda
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** $\ZZ$ of the (additive)
integers generated by $1$, but there is also a **finite cyclic group** of order
$n$ for every $n \geq 1$. As it turns out, we can construct *all* the cyclic
groups using the same machine: the quotient group $\ZZ/n\ZZ$, where $n\ZZ$
is the [[normal subgroup]] of multiples of $n$, is the cyclic group of order
$n$ when $n \geq 1$, and is the infinite cyclic group when $n = 0$.

```agda
infix 30 _·ℤ
_·ℤ : ∀ (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 25 ℤ/_
ℤ/_ : Nat → Group lzero
ℤ/ n = ℤ /ᴳ n ·ℤ
```

$\ZZ/n\ZZ$ is an [[abelian group]], since the commutativity of
addition descends to the quotient.

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

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

Furthermore, $\ZZ/n\ZZ$ is, by construction, cyclic, and is generated
by $1$.

<!--
```agda
module _ (n : Nat) where
  open Group-on ((ℤ/ n) .snd)
```
-->

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

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

This follows from the fact that a group homomorphism $\ZZ \to G$ out of
the [[group of integers]] is uniquely determined by an element of $G$,
and some basic algebra.

```agda
module _
  (n : Nat)
  {ℓ} {G : Group ℓ} (open Group-on (G .snd))
  (x : ⌞ G ⌟) (open pow G x renaming (pow to infixr 30 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 $\ZZ/0\ZZ \is \ZZ$:

```agda
ℤ-ab/0≡ℤ-ab : ℤ-ab/ 0 ≡ ℤ-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 ≡ ℤ
ℤ/0≡ℤ = Grp→Ab→Grp (ℤ/ 0) (ℤ/n-commutative 0) ∙ ap Abelian→Group ℤ-ab/0≡ℤ-ab
```

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

```agda
ℤ/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]$,
we can check that $\ZZ/2\ZZ$ is isomorphic to the [[symmetric group]] $S_2$.
We start by defining a homomorphism $\ZZ/2\ZZ \to S_2$ that sends 1 to
the equivalence $[2] \simeq [2]$ that swaps the two elements, which
corresponds to $1 : [2!]$.

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

In order to conclude the proof, we show that the function $f : \ZZ/2\ZZ
\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:

~~~{.quiver}
\[\begin{tikzcd}
  {\mathbb{Z}/2\mathbb{Z}} & {S_2} \\
  {[2]} & {[2]}
  \arrow["f", from=1-1, to=1-2]
  \arrow["\simeq", from=1-2, to=2-2]
  \arrow["\simeq", from=2-1, to=1-1]
  \arrow["\simeq", "{\mathrm{id}}"', from=2-1, to=2-2]
\end{tikzcd}\]
~~~

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