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
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


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 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.


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)

  is-cyclic-prop-∞-Group : Prop (l1  lsuc l2)
  is-cyclic-prop-∞-Group =
      ( 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


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