Abelian higher groups

Content created by Fredrik Bakke.

Created on 2024-10-18.
Last modified on 2024-10-18.

module higher-group-theory.abelian-higher-groups where
Imports 
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.small-types
open import foundation.universe-levels

open import higher-group-theory.equivalences-higher-groups
open import higher-group-theory.higher-groups
open import higher-group-theory.small-higher-groups

open import structured-types.pointed-equivalences
open import structured-types.pointed-types
open import structured-types.small-pointed-types

open import synthetic-homotopy-theory.connective-spectra

Idea

An abelian, or commutative ∞-group is a higher group A₀ that is commutative in a fully coherent way. There are multiple ways to express this in Homotopy Type Theory. One way is to say there is a connective spectrum 𝒜 such that the ∞-group appears as the first type in the sequence. [BvDR18] I.e., there exists a sequence of increasingly connected ∞-groups

  A₀   A₁   A₂   A₃   ⋯   Aᵢ   ⋯

such that

  Aᵢ ≃∗ Ω Aᵢ₊₁

Abelian ∞-groups thus give an example of another infinitely coherent structure that is definable in Homotopy Type Theory.

Definitions

The connective spectrum condition of being abelian with respect to a universe level

is-abelian-level-connective-spectrum-condition-∞-Group :
  {l : Level} (l1 : Level) → ∞-Group l → UU (l ⊔ lsuc l1)
is-abelian-level-connective-spectrum-condition-∞-Group l1 G =
  Σ ( Connective-Spectrum l1)
    ( λ A → pointed-type-∞-Group G ≃∗ pointed-type-Connective-Spectrum A 0)

The connective spectrum condition of being abelian

is-abelian-connective-spectrum-condition-∞-Group :
  {l : Level} → ∞-Group l → UU (lsuc l)
is-abelian-connective-spectrum-condition-∞-Group {l} G =
  is-abelian-level-connective-spectrum-condition-∞-Group l G

References

[BvDR18]
Ulrik Buchholtz, Floris van Doorn, and Egbert Rijke. Higher Groups in Homotopy Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, 205–214. New York, NY, USA, 02 2018. Association for Computing Machinery. arXiv:1802.04315, doi:10.1145/3209108.3209150.

Recent changes