Infinite cyclic types

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-03-02.
Last modified on 2024-01-17.

module synthetic-homotopy-theory.infinite-cyclic-types where

Imports

open import elementary-number-theory.addition-integers
open import elementary-number-theory.integers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.torsorial-type-families
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import structured-types.equivalences-types-equipped-with-endomorphisms
open import structured-types.initial-pointed-type-equipped-with-automorphism
open import structured-types.mere-equivalences-types-equipped-with-endomorphisms
open import structured-types.pointed-types
open import structured-types.pointed-types-equipped-with-automorphisms
open import structured-types.types-equipped-with-endomorphisms

open import synthetic-homotopy-theory.loop-spaces

open import univalent-combinatorics.cyclic-finite-types

Definitions

Infinite-Cyclic-Type : (l : Level) → UU (lsuc l)
Infinite-Cyclic-Type l = Cyclic-Type l zero-ℕ

ℤ-Infinite-Cyclic-Type : Infinite-Cyclic-Type lzero
ℤ-Infinite-Cyclic-Type = ℤ-Mod-Cyclic-Type zero-ℕ

Infinite-Cyclic-Type-Pointed-Type : Pointed-Type (lsuc lzero)
Infinite-Cyclic-Type-Pointed-Type = Cyclic-Type-Pointed-Type zero-ℕ

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

  endo-Infinite-Cyclic-Type : Type-With-Endomorphism l
  endo-Infinite-Cyclic-Type = endo-Cyclic-Type zero-ℕ X

  type-Infinite-Cyclic-Type : UU l
  type-Infinite-Cyclic-Type = type-Cyclic-Type zero-ℕ X

  endomorphism-Infinite-Cyclic-Type :
    type-Infinite-Cyclic-Type → type-Infinite-Cyclic-Type
  endomorphism-Infinite-Cyclic-Type = endomorphism-Cyclic-Type zero-ℕ X

  mere-equiv-ℤ-Infinite-Cyclic-Type :
    mere-equiv-Type-With-Endomorphism
      ( ℤ-Type-With-Endomorphism)
      ( endo-Infinite-Cyclic-Type)
  mere-equiv-ℤ-Infinite-Cyclic-Type = pr2 X

module _
  (l : Level)
  where

  point-Infinite-Cyclic-Type : Infinite-Cyclic-Type l
  pr1 (pr1 point-Infinite-Cyclic-Type) = raise l ℤ
  pr2 (pr1 point-Infinite-Cyclic-Type) = (map-raise ∘ succ-ℤ) ∘ map-inv-raise
  pr2 point-Infinite-Cyclic-Type =
    unit-trunc-Prop (pair (compute-raise l ℤ) refl-htpy)

  Infinite-Cyclic-Type-Pointed-Type-Level : Pointed-Type (lsuc l)
  pr1 Infinite-Cyclic-Type-Pointed-Type-Level = Infinite-Cyclic-Type l
  pr2 Infinite-Cyclic-Type-Pointed-Type-Level = point-Infinite-Cyclic-Type

module _
  {l1 : Level} (X : Infinite-Cyclic-Type l1)
  where

  equiv-Infinite-Cyclic-Type :
    {l2 : Level} → Infinite-Cyclic-Type l2 → UU (l1 ⊔ l2)
  equiv-Infinite-Cyclic-Type = equiv-Cyclic-Type zero-ℕ X

  id-equiv-Infinite-Cyclic-Type : equiv-Infinite-Cyclic-Type X
  id-equiv-Infinite-Cyclic-Type = id-equiv-Cyclic-Type zero-ℕ X

  equiv-eq-Infinite-Cyclic-Type :
    (Y : Infinite-Cyclic-Type l1) → Id X Y → equiv-Infinite-Cyclic-Type Y
  equiv-eq-Infinite-Cyclic-Type = equiv-eq-Cyclic-Type zero-ℕ X

  is-torsorial-equiv-Infinite-Cyclic-Type :
    is-torsorial equiv-Infinite-Cyclic-Type
  is-torsorial-equiv-Infinite-Cyclic-Type =
    is-torsorial-equiv-Cyclic-Type zero-ℕ X

  is-equiv-equiv-eq-Infinite-Cyclic-Type :
    (Y : Infinite-Cyclic-Type l1) → is-equiv (equiv-eq-Infinite-Cyclic-Type Y)
  is-equiv-equiv-eq-Infinite-Cyclic-Type =
    is-equiv-equiv-eq-Cyclic-Type zero-ℕ X

  extensionality-Infinite-Cyclic-Type :
    (Y : Infinite-Cyclic-Type l1) → Id X Y ≃ equiv-Infinite-Cyclic-Type Y
  extensionality-Infinite-Cyclic-Type = extensionality-Cyclic-Type zero-ℕ X

module _
  where

  map-left-factor-compute-Ω-Infinite-Cyclic-Type :
    equiv-Infinite-Cyclic-Type ℤ-Infinite-Cyclic-Type ℤ-Infinite-Cyclic-Type → ℤ
  map-left-factor-compute-Ω-Infinite-Cyclic-Type e =
    map-equiv-Type-With-Endomorphism
      ( ℤ-Type-With-Endomorphism)
      ( ℤ-Type-With-Endomorphism)
      ( e)
      ( zero-ℤ)

  abstract
    is-equiv-map-left-factor-compute-Ω-Infinite-Cyclic-Type :
      is-equiv map-left-factor-compute-Ω-Infinite-Cyclic-Type
    is-equiv-map-left-factor-compute-Ω-Infinite-Cyclic-Type =
      is-equiv-is-contr-map
        ( λ x →
          is-contr-equiv
            ( hom-Pointed-Type-With-Aut
                ℤ-Pointed-Type-With-Aut
                ℤ-Pointed-Type-With-Aut)
            ( ( right-unit-law-Σ-is-contr
                { B = λ f → is-equiv (pr1 f)}
                ( λ f →
                  is-proof-irrelevant-is-prop
                    ( is-property-is-equiv (pr1 f))
                    ( is-equiv-htpy id
                      ( htpy-eq
                        ( ap
                          ( pr1)
                          { x = f}
                          { y = pair id (pair refl refl-htpy)}
                          ( eq-is-contr
                            ( is-initial-ℤ-Pointed-Type-With-Aut
                              ℤ-Pointed-Type-With-Aut))))
                      ( is-equiv-id)))) ∘e
              ( ( equiv-right-swap-Σ) ∘e
                ( ( associative-Σ
                    ( ℤ ≃ ℤ)
                    ( λ e → Id (map-equiv e zero-ℤ) zero-ℤ)
                    ( λ e →
                      ( map-equiv (pr1 e) ∘ succ-ℤ) ~
                      ( succ-ℤ ∘ map-equiv (pr1 e)))) ∘e
                  ( ( equiv-right-swap-Σ) ∘e
                    ( equiv-Σ
                      ( λ e → Id (map-equiv (pr1 e) zero-ℤ) zero-ℤ)
                      ( equiv-Σ
                        ( λ e → (map-equiv e ∘ succ-ℤ) ~ (succ-ℤ ∘ map-equiv e))
                        ( equiv-postcomp-equiv (equiv-left-add-ℤ (neg-ℤ x)) ℤ)
                        ( λ e →
                          equiv-Π-equiv-family
                            ( λ k →
                              ( equiv-concat'
                                ( (neg-ℤ x) +ℤ (map-equiv e (succ-ℤ k)))
                                ( right-successor-law-add-ℤ
                                  ( neg-ℤ x)
                                  ( map-equiv e k))) ∘e
                              ( equiv-ap
                                ( equiv-left-add-ℤ (neg-ℤ x))
                                ( map-equiv e (succ-ℤ k))
                                ( succ-ℤ (map-equiv e k))))))
                      ( λ e →
                        ( equiv-concat'
                          ( (neg-ℤ x) +ℤ (map-equiv (pr1 e) zero-ℤ))
                          ( left-inverse-law-add-ℤ x)) ∘e
                        ( equiv-ap
                          ( equiv-left-add-ℤ (neg-ℤ x))
                          ( map-equiv (pr1 e) zero-ℤ)
                          ( x))))))))
            ( is-initial-ℤ-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut))

  equiv-left-factor-compute-Ω-Infinite-Cyclic-Type :
    equiv-Infinite-Cyclic-Type
      ℤ-Infinite-Cyclic-Type
      ℤ-Infinite-Cyclic-Type ≃ ℤ
  pr1 equiv-left-factor-compute-Ω-Infinite-Cyclic-Type =
    map-left-factor-compute-Ω-Infinite-Cyclic-Type
  pr2 equiv-left-factor-compute-Ω-Infinite-Cyclic-Type =
    is-equiv-map-left-factor-compute-Ω-Infinite-Cyclic-Type

  compute-Ω-Infinite-Cyclic-Type :
    type-Ω (Infinite-Cyclic-Type-Pointed-Type) ≃ ℤ
  compute-Ω-Infinite-Cyclic-Type =
    ( equiv-left-factor-compute-Ω-Infinite-Cyclic-Type) ∘e
    ( extensionality-Infinite-Cyclic-Type
        ℤ-Infinite-Cyclic-Type
        ℤ-Infinite-Cyclic-Type)

Concept	File
Acyclic maps	`synthetic-homotopy-theory.acyclic-maps`
Acyclic types	`synthetic-homotopy-theory.acyclic-types`
Acyclic undirected graphs	`graph-theory.acyclic-undirected-graphs`
Bracelets	`univalent-combinatorics.bracelets`
The category of cyclic rings	`ring-theory.category-of-cyclic-rings`
The circle	`synthetic-homotopy-theory.circle`
Connected set bundles over the circle	`synthetic-homotopy-theory.connected-set-bundles-circle`
Cyclic finite types	`univalent-combinatorics.cyclic-finite-types`
Cyclic groups	`group-theory.cyclic-groups`
Cyclic higher groups	`higher-group-theory.cyclic-higher-groups`
Cyclic rings	`ring-theory.cyclic-rings`
Cyclic types	`structured-types.cyclic-types`
Euler’s totient function	`elementary-number-theory.eulers-totient-function`
Finitely cyclic maps	`elementary-number-theory.finitely-cyclic-maps`
Generating elements of groups	`group-theory.generating-elements-groups`
Hatcher’s acyclic type	`synthetic-homotopy-theory.hatchers-acyclic-type`
Homomorphisms of cyclic rings	`ring-theory.homomorphisms-cyclic-rings`
Infinite cyclic types	`synthetic-homotopy-theory.infinite-cyclic-types`
Multiplicative units in the standard cyclic rings	`elementary-number-theory.multiplicative-units-standard-cyclic-rings`
Necklaces	`univalent-combinatorics.necklaces`
Polygons	`graph-theory.polygons`
The poset of cyclic rings	`ring-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

2024-01-17. Egbert Rijke. Reformatting commented blocks of code (#1004).
2023-10-22. Egbert Rijke and Fredrik Bakke. Refactor synthetic homotopy theory (#654).
2023-10-21. Egbert Rijke and Fredrik Bakke. Implement is-torsorial throughout the library (#875).
2023-10-21. Egbert Rijke. Rename is-contr-total to is-torsorial (#871).
2023-10-09. Egbert Rijke. Navigation tables for all files related to cyclic types, groups, and rings (#823).

agda-unimath

Infinite cyclic types

Definitions

See also

Recent changes

agda-unimath

Infinite cyclic types

Definitions

See also

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

Recent changes