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

Recent changes