Cyclic higher groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-07-19.
Last modified on 2024-04-11.

module higher-group-theory.cyclic-higher-groups where
Imports 
open import foundation.embeddings
open import foundation.existential-quantification
open import foundation.propositions
open import foundation.universe-levels

open import higher-group-theory.higher-groups
open import higher-group-theory.homomorphisms-higher-groups

Idea

One may wonder if the notion of cyclic group generalizes to higher groups. A naive way of defining cyclic higher groups is to extend the universal property of cyclic groups to all higher groups. Following this idea, we say that a higher group G is cyclic if there exists an element g of G such that the evaluation map

  hom-∞-Group G H → type-∞-Group H

given by f ↦ map-hom-∞-Group G H f g is an embedding for every higher group H. In other words, a higher group is cyclic if it is generated by a single element.

However, by Miller's theorem [Mil84] we don't expect there to be many higher groups that are cyclic in this sense. For example, the finite cyclic groups Bℤ/n are coherent spaces, whereas the 2-sphere S² is a finite CW-complex. Miller's theorem implies that the pointed mapping space Map∗(Bℤ/n,S²) is contractible. However, this implies that the evaluation map Map∗(Bℤ/n,S²) → ΩS² at the generator of ℤ/n is a point inclusion into a nondiscrete type, so it can't be an embedding.

Definitions

Cyclic higher groups

ev-element-∞-Group :
  {l1 l2 : Level} (G : ∞-Group l1) (H : ∞-Group l2) (g : type-∞-Group G) →
  hom-∞-Group G H → type-∞-Group H
ev-element-∞-Group G H g f = map-hom-∞-Group G H f g

module _
  {l1 : Level} (l2 : Level) (G : ∞-Group l1)
  where

  is-cyclic-prop-∞-Group : Prop (l1 ⊔ lsuc l2)
  is-cyclic-prop-∞-Group =
    exists-structure-Prop
      ( type-∞-Group G)
      ( λ g → (H : ∞-Group l2) → is-emb (ev-element-∞-Group G H g))

  is-cyclic-∞-Group : UU (l1 ⊔ lsuc l2)
  is-cyclic-∞-Group = type-Prop is-cyclic-prop-∞-Group

  is-prop-is-cyclic-∞-Group : is-prop is-cyclic-∞-Group
  is-prop-is-cyclic-∞-Group = is-prop-type-Prop is-cyclic-prop-∞-Group

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

References

[Mil84]
Haynes Miller. The Sullivan Conjecture on Maps from Classifying Spaces. Annals of Mathematics, 120(1):39–87, 1984. arXiv:2007071, doi:10.2307/2007071.

Recent changes