Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Deloopings and Eilenberg-Mac Lane spaces (#1079)
In this pull request we add: - A definition of what it means for a pointed type to be deloopable - A definition of what it means for an H-space to be deloopable - A definition of Eilenberg-Mac Lane spaces There were some universe level questions that one can ask about the type of deloopings. One can show that the type of deloopings of `X` in universe `l2` is equivalent to the type of deloopings of `X` in the universe level of `X`. Showing the forward implication required me to do some work on smallness of pointed types and higher groups, which is included in this pull request. Furthermore, the file about morphisms of H-spaces has been revamped, for better formalization of the preservation of the coherence law. This was needed for the notion of equivalence of H-spaces, which was prerequisite to the notion of delooping of H-spaces.
- Loading branch information
1 parent
cacce49
commit ae24502
Showing
22 changed files
with
1,846 additions
and
286 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,58 @@ | ||
| # Deloopable groups | ||
|
|
||
| ```agda | ||
| module higher-group-theory.deloopable-groups where | ||
| ``` | ||
|
|
||
| <details><summary>Imports</summary> | ||
|
|
||
| ```agda | ||
| open import foundation.dependent-pair-types | ||
| open import foundation.universe-levels | ||
|
|
||
| open import group-theory.groups | ||
|
|
||
| open import higher-group-theory.deloopable-h-spaces | ||
| ``` | ||
|
|
||
| </details> | ||
|
|
||
| ## Idea | ||
|
|
||
| A {{#concept "delooping" Disambiguation="group" Agda=delooping-Group}} of a | ||
| [group](group-theory.groups.md) `G` is a | ||
| [delooping](higher-group-theory.deloopable-h-spaces.md) of the underlying | ||
| [H-space](structured-types.h-spaces.md) of `G`. In other words, a delooping of a | ||
| group `G` consists of a [higher group](higher-group-theory.higher-groups.md) | ||
| `H`, which is defined to be a [pointed](structured-types.pointed-types.md) | ||
| [connected](foundation.0-connected-types.md) type, equipped with an | ||
| [equivalence of H-spaces](structured-types.equivalences-h-spaces.md) | ||
| `G ≃ h-space-∞-Group H` from `G` to the underlying H-space of `H`. | ||
|
|
||
| ## Definitions | ||
|
|
||
| ### Deloopings of groups of a given universe level | ||
|
|
||
| ```agda | ||
| module _ | ||
| {l1 : Level} (l2 : Level) (G : Group l1) | ||
| where | ||
|
|
||
| delooping-Group-Level : UU (l1 ⊔ lsuc l2) | ||
| delooping-Group-Level = delooping-H-Space-Level l2 (h-space-Group G) | ||
| ``` | ||
|
|
||
| ### Deloopings of groups | ||
|
|
||
| ```agda | ||
| module _ | ||
| {l1 : Level} (G : Group l1) | ||
| where | ||
|
|
||
| delooping-Group : UU (lsuc l1) | ||
| delooping-Group = delooping-Group-Level l1 G | ||
| ``` | ||
|
|
||
| ## See also | ||
|
|
||
| - [Eilenberg-Mac Lane spaces](higher-group-theory.eilenberg-mac-lane-spaces.md) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,68 @@ | ||
| # Deloopable H-spaces | ||
|
|
||
| ```agda | ||
| module higher-group-theory.deloopable-h-spaces where | ||
| ``` | ||
|
|
||
| <details><summary>Imports</summary> | ||
|
|
||
| ```agda | ||
| open import foundation.dependent-pair-types | ||
| open import foundation.universe-levels | ||
|
|
||
| open import higher-group-theory.higher-groups | ||
|
|
||
| open import structured-types.equivalences-h-spaces | ||
| open import structured-types.h-spaces | ||
| ``` | ||
|
|
||
| </details> | ||
|
|
||
| ## Idea | ||
|
|
||
| Consider an [H-space](structured-types.h-spaces.md) with underlying | ||
| [pointed type](structured-types.pointed-types.md) `(X , *)` and with | ||
| multiplication `μ` satisfying | ||
|
|
||
| ```text | ||
| left-unit-law : (x : X) → μ * x ＝ x | ||
| right-unit-law : (x : X) → μ x * ＝ x | ||
| coh-unit-law : left-unit-law * ＝ right-unit-law *. | ||
| ``` | ||
|
|
||
| A {{#concept "delooping" Disambiguation="H-space" Agda=delooping-H-Space}} of | ||
| the H-space `X` consists of an [∞-group](higher-group-theory.higher-groups.md) | ||
| `G` and an [equivalence of H-spaces](structured-types.equivalences-h-spaces.md) | ||
|
|
||
| ```text | ||
| X ≃ h-space-∞-Group G. | ||
| ``` | ||
|
|
||
| ## Definitions | ||
|
|
||
| ### Deloopings of H-spaces of a given universe level | ||
|
|
||
| ```agda | ||
| module _ | ||
| {l1 : Level} (l2 : Level) (A : H-Space l1) | ||
| where | ||
|
|
||
| delooping-H-Space-Level : UU (l1 ⊔ lsuc l2) | ||
| delooping-H-Space-Level = | ||
| Σ (∞-Group l2) (λ G → equiv-H-Space A (h-space-∞-Group G)) | ||
| ``` | ||
|
|
||
| ### Deloopings of H-spaces | ||
|
|
||
| ```agda | ||
| module _ | ||
| {l1 : Level} (A : H-Space l1) | ||
| where | ||
|
|
||
| delooping-H-Space : UU (lsuc l1) | ||
| delooping-H-Space = delooping-H-Space-Level l1 A | ||
| ``` | ||
|
|
||
| ## See also | ||
|
|
||
| - [Deloopable groups](higher-group-theory.deloopable-groups.md) |
Oops, something went wrong.