# Cyclic types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-28.
Last modified on 2024-02-06.

module structured-types.cyclic-types where

Imports
open import foundation.automorphisms
open import foundation.dependent-pair-types
open import foundation.iterating-automorphisms
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.surjective-maps
open import foundation.universe-levels

open import structured-types.sets-equipped-with-automorphisms


## Idea

A cyclic set consists of a set A equipped with an automorphism e : A ≃ A which is cyclic in the sense that its underlying set is inhabited and the map

  k ↦ eᵏ x


is surjective for every x : A. There are several equivalent ways of stating the concept of cyclic sets. Two further equivalent ways are:

Note that the empty set equipped with the identity automorphism is not considered to be a cyclic set, for reasons similar to those of not considering empty group actions to be transitive.

## Definition

### The predicate of being a cyclic set

module _
{l : Level} (X : Set-With-Automorphism l)
where

is-cyclic-prop-Set-With-Automorphism : Prop l
is-cyclic-prop-Set-With-Automorphism =
product-Prop
( trunc-Prop (type-Set-With-Automorphism X))
( Π-Prop
( type-Set-With-Automorphism X)
( λ x →
is-surjective-Prop
( λ k →
map-iterate-automorphism-ℤ k (aut-Set-With-Automorphism X) x)))

is-cyclic-Set-With-Automorphism : UU l
is-cyclic-Set-With-Automorphism =
type-Prop is-cyclic-prop-Set-With-Automorphism


### Cyclic sets

Cyclic-Set :
(l : Level) → UU (lsuc l)
Cyclic-Set l =
Σ (Set-With-Automorphism l) (λ X → is-cyclic-Set-With-Automorphism X)

module _
{l : Level} (X : Cyclic-Set l)
where

set-with-automorphism-Cyclic-Set : Set-With-Automorphism l
set-with-automorphism-Cyclic-Set = pr1 X

set-Cyclic-Set : Set l
set-Cyclic-Set = set-Set-With-Automorphism set-with-automorphism-Cyclic-Set

type-Cyclic-Set : UU l
type-Cyclic-Set = type-Set-With-Automorphism set-with-automorphism-Cyclic-Set

is-set-type-Cyclic-Set : is-set type-Cyclic-Set
is-set-type-Cyclic-Set =
is-set-type-Set-With-Automorphism set-with-automorphism-Cyclic-Set

aut-Cyclic-Set : Aut type-Cyclic-Set
aut-Cyclic-Set = aut-Set-With-Automorphism set-with-automorphism-Cyclic-Set

map-Cyclic-Set : type-Cyclic-Set → type-Cyclic-Set
map-Cyclic-Set = map-Set-With-Automorphism set-with-automorphism-Cyclic-Set


## See also

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