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 that is, every element of the group can be written as some integer power of 1.

_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 to get a proposition. In fact, if generates then so does hence a non-trivial cyclic group has at least two generators!

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 , (
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 of the (additive) integers generated by but there is also a finite cyclic group of order for every As it turns out, we can construct all the cyclic groups using the same machine: the quotient group where is the normal subgroup of multiples of is the cyclic group of order when and is the infinite cyclic group when

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 Β·β€


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 25 β€-ab/_
β€-ab/_ : Nat β Abelian-group lzero
β€-ab/_ n = from-commutative-group (β€/ n) (β€/n-commutative n)


Furthermore, is, by construction, cyclic, and is generated by

module _ (n : Nat) where
open Group-on ((β€/ n) .snd)

  β€/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 a group homomorphism is uniquely determined by an element of order i.e.Β such that Note that this condition is trivially satisfied if so we donβt need a special case.

This follows from the fact that a group homomorphism out of the group of integers is uniquely determined by an element of and some basic algebra.

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 β€-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 we show that is finite; more precisely, we construct an equivalence which sends to the representative of its congruence class modulo β€/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 we can check that is isomorphic to the symmetric group We start by defining a homomorphism that sends 1 to the equivalence that swaps the two elements, which corresponds to

β€/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 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β : β€/ 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))


1. Some authors (namely, Bourbaki) call such groups monogeneous, and reserve βcyclicβ for the finite cyclic groups.β©οΈ