Cyclic higher groups

Content created by Egbert Rijke and Fredrik Bakke

Created on 2023-07-19.
Last modified on 2023-09-15.

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

References

  1. Haynes Miller. The Sullivan Conjecture on Maps from Classifying Spaces. Annals of Mathematics 120.1 (1984), pp. 39–87. issn: 0003486X. http://www.jstor.org/stable/2007071

Recent changes