This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Cyclic types

module structured-types.cyclic-types where

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:

• A cyclic set is a connected set bundle over the circle.
• A cyclic set is a set equipped with a transitive ℤ-action.
• A cyclic set is a set which is a C-torsor for some cyclic group C.

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

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