Abelian ∞-groups (#1178)

Defines abelian ∞-groups as ∞-groups that are $n$-deloopable for all
$n$. In other words, there is a connective spectrum where the group
appears as the first type in the sequence.

references.bib

@@ -81,7 +81,7 @@ @book{BSCS05
   langid    = {hungarian}
 }
 
-@online{BvDR18,
+@inproceedings{BvDR18,
   title       = {Higher {{Groups}} in {{Homotopy Type Theory}}},
   author      = {Buchholtz, Ulrik and van Doorn, Floris and Rijke, Egbert},
   date        = {2018-02-12},
@@ -91,8 +91,15 @@ @online{BvDR18
   eprinttype  = {arxiv},
   eprintclass = {cs, math},
   abstract    = {We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-L\"of type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.},
-  pubstate    = {preprint},
-  keywords    = {03B15,Computer Science - Logic in Computer Science,F.4.1,Mathematics - Algebraic Topology,Mathematics - Logic}
+  isbn        = {9781450355834},
+  doi         = {10.1145/3209108.3209150},
+  pages       = {205--214},
+  numpages    = {10},
+  location    = {Oxford, United Kingdom},
+  booktitle   = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
+  address     = {New York, NY, USA},
+  publisher   = {Association for Computing Machinery},
+  series      = {LICS '18}
 }
 
 @article{BW23,

src/foundation/connected-types.lagda.md

@@ -220,6 +220,6 @@ module _
     A retract-of B →
     is-connected k B →
     is-connected k A
-  is-connected-retract-of R c =
-    is-contr-retract-of (type-trunc k B) (retract-of-trunc-retract-of R) c
+  is-connected-retract-of R =
+    is-contr-retract-of (type-trunc k B) (retract-of-trunc-retract-of R)
 ```

src/higher-group-theory.lagda.md

@@ -5,6 +5,7 @@
 ```agda
 module higher-group-theory where
 
+open import higher-group-theory.abelian-higher-groups public
 open import higher-group-theory.cartesian-products-higher-groups public
 open import higher-group-theory.conjugation public
 open import higher-group-theory.cyclic-higher-groups public

src/higher-group-theory/abelian-higher-groups.lagda.md

@@ -0,0 +1,81 @@
+# Abelian higher groups
+
+```agda
+module higher-group-theory.abelian-higher-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+```
+
+</details>
+
+## Idea
+
+An {{#concept "abelian" Disambiguation="∞-group"}}, or
+{{#concept "commutative" Disambiguation="∞-group"}} ∞-group is a
+[higher group](higher-group-theory.higher-groups.md) `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](synthetic-homotopy-theory.connective-spectra.md) `𝒜` such
+that the ∞-group appears as the first type in the sequence. {{#cite BvDR18}}
+I.e., there exists a sequence of increasingly
+[connected](foundation.connected-types.md) ∞-groups
+
+```text
+  A₀   A₁   A₂   A₃   ⋯   Aᵢ   ⋯
+```
+
+such that
+
+```text
+  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
+
+```agda
+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
+
+```agda
+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
+
+{{#bibliography}}
+
+## External links
+
+- [abelian infinity-group](https://ncatlab.org/nlab/show/abelian+infinity-group)
+  at $n$Lab

src/synthetic-homotopy-theory.lagda.md

@@ -28,6 +28,8 @@ open import synthetic-homotopy-theory.coforks public
 open import synthetic-homotopy-theory.coforks-cocones-under-sequential-diagrams public
 open import synthetic-homotopy-theory.conjugation-loops public
 open import synthetic-homotopy-theory.connected-set-bundles-circle public
+open import synthetic-homotopy-theory.connective-prespectra public
+open import synthetic-homotopy-theory.connective-spectra public
 open import synthetic-homotopy-theory.dependent-cocones-under-sequential-diagrams public
 open import synthetic-homotopy-theory.dependent-cocones-under-spans public
 open import synthetic-homotopy-theory.dependent-coforks public

src/synthetic-homotopy-theory/connective-prespectra.lagda.md

@@ -0,0 +1,143 @@
+# Connective prespectra
+
+```agda
+module synthetic-homotopy-theory.connective-prespectra where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.connected-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.truncation-levels
+open import foundation.universe-levels
+
+open import structured-types.pointed-equivalences
+open import structured-types.pointed-maps
+open import structured-types.pointed-types
+
+open import synthetic-homotopy-theory.loop-spaces
+open import synthetic-homotopy-theory.prespectra
+open import synthetic-homotopy-theory.suspensions-of-pointed-types
+open import synthetic-homotopy-theory.suspensions-of-types
+```
+
+</details>
+
+## Idea
+
+A [prespectrum](synthetic-homotopy-theory.prespectra.md) is
+{{#concept "connective" Disambiguation="prespectrum" Agda=is-connective-Prespectrum}}
+if the $n$th type in the [sequence](foundation.sequences.md) is
+$n$-[connected](foundation.connected-types.md).
+
+### The predicate on prespectra of being connective
+
+```agda
+module _
+  {l : Level} (A : Prespectrum l)
+  where
+
+  is-connective-Prespectrum : UU l
+  is-connective-Prespectrum =
+    (n : ℕ) → is-connected (truncation-level-ℕ n) (type-Prespectrum A n)
+
+  is-prop-is-connective-Prespectrum : is-prop is-connective-Prespectrum
+  is-prop-is-connective-Prespectrum =
+    is-prop-Π
+      ( λ n →
+        is-prop-is-connected (truncation-level-ℕ n) (type-Prespectrum A n))
+
+  is-connective-prop-Prespectrum : Prop l
+  is-connective-prop-Prespectrum =
+    is-connective-Prespectrum , is-prop-is-connective-Prespectrum
+```
+
+### The type of connective prespectra
+
+```agda
+Connective-Prespectrum : (l : Level) → UU (lsuc l)
+Connective-Prespectrum l = Σ (Prespectrum l) (is-connective-Prespectrum)
+
+module _
+  {l : Level} (A : Connective-Prespectrum l)
+  where
+
+  prespectrum-Connective-Prespectrum : Prespectrum l
+  prespectrum-Connective-Prespectrum = pr1 A
+
+  pointed-type-Connective-Prespectrum : ℕ → Pointed-Type l
+  pointed-type-Connective-Prespectrum =
+    pointed-type-Prespectrum prespectrum-Connective-Prespectrum
+
+  type-Connective-Prespectrum : ℕ → UU l
+  type-Connective-Prespectrum =
+    type-Prespectrum prespectrum-Connective-Prespectrum
+
+  point-Connective-Prespectrum : (n : ℕ) → type-Connective-Prespectrum n
+  point-Connective-Prespectrum =
+    point-Prespectrum prespectrum-Connective-Prespectrum
+
+  pointed-adjoint-structure-map-Connective-Prespectrum :
+    (n : ℕ) →
+    pointed-type-Connective-Prespectrum n →∗
+    Ω (pointed-type-Connective-Prespectrum (succ-ℕ n))
+  pointed-adjoint-structure-map-Connective-Prespectrum =
+    pointed-adjoint-structure-map-Prespectrum prespectrum-Connective-Prespectrum
+
+  adjoint-structure-map-Connective-Prespectrum :
+    (n : ℕ) →
+    type-Connective-Prespectrum n →
+    type-Ω (pointed-type-Connective-Prespectrum (succ-ℕ n))
+  adjoint-structure-map-Connective-Prespectrum =
+    adjoint-structure-map-Prespectrum prespectrum-Connective-Prespectrum
+
+  preserves-point-adjoint-structure-map-Connective-Prespectrum :
+    (n : ℕ) →
+    adjoint-structure-map-Prespectrum (pr1 A) n (point-Prespectrum (pr1 A) n) ＝
+    refl-Ω (pointed-type-Prespectrum (pr1 A) (succ-ℕ n))
+  preserves-point-adjoint-structure-map-Connective-Prespectrum =
+    preserves-point-adjoint-structure-map-Prespectrum
+      prespectrum-Connective-Prespectrum
+
+  is-connective-Connective-Prespectrum :
+    is-connective-Prespectrum prespectrum-Connective-Prespectrum
+  is-connective-Connective-Prespectrum = pr2 A
+```
+
+### The structure maps of a connective prespectrum
+
+```agda
+module _
+  {l : Level} (A : Connective-Prespectrum l) (n : ℕ)
+  where
+
+  pointed-structure-map-Connective-Prespectrum :
+    suspension-Pointed-Type (pointed-type-Connective-Prespectrum A n) →∗
+    pointed-type-Connective-Prespectrum A (succ-ℕ n)
+  pointed-structure-map-Connective-Prespectrum =
+    pointed-structure-map-Prespectrum (prespectrum-Connective-Prespectrum A) n
+
+  structure-map-Connective-Prespectrum :
+    suspension (type-Connective-Prespectrum A n) →
+    type-Connective-Prespectrum A (succ-ℕ n)
+  structure-map-Connective-Prespectrum =
+    map-pointed-map pointed-structure-map-Connective-Prespectrum
+
+  preserves-point-structure-map-Connective-Prespectrum :
+    structure-map-Connective-Prespectrum north-suspension ＝
+    point-Connective-Prespectrum A (succ-ℕ n)
+  preserves-point-structure-map-Connective-Prespectrum =
+    preserves-point-pointed-map pointed-structure-map-Connective-Prespectrum
+```
+
+## External links
+
+- [connective spectrum](https://ncatlab.org/nlab/show/connective+spectrum) at
+  $n$Lab