Small ∞-groups
Content created by Egbert Rijke.
Created on 2024-03-23.
Last modified on 2024-03-23.
module higher-group-theory.small-higher-groups where
Imports
open import foundation.0-connected-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.identity-types open import foundation.images open import foundation.locally-small-types open import foundation.propositional-truncations open import foundation.propositions open import foundation.replacement open import foundation.small-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universe-levels open import higher-group-theory.equivalences-higher-groups open import higher-group-theory.higher-groups open import structured-types.pointed-equivalences open import structured-types.pointed-types open import structured-types.small-pointed-types
Idea
An ∞-group G is said to be
small¶ with respect
to a universe 𝒰 if its underlying type is 𝒰-small. By the
type theoretic replacement principle it follows
that G is small if and only if its classifying type BG is small. This
observation implies that an ∞-group G is small if and only if it is
structurally small¶
in the sense that it comes equipped with an element of type
Σ (H : ∞-Group), G ≃ H,
where the type G ≃ H is the type of
equivalences of ∞-groups.
Finally, we also introduce the notion of pointed small ∞-group. An ∞-group G
is said to be
pointed small¶
if its classifying pointed type BG is
pointed small.
Definitions
The predicate of being a small ∞-group
module _ {l1 : Level} (l2 : Level) (G : ∞-Group l1) where is-small-prop-∞-Group : Prop (l1 ⊔ lsuc l2) is-small-prop-∞-Group = is-small-Prop l2 (type-∞-Group G) is-small-∞-Group : UU (l1 ⊔ lsuc l2) is-small-∞-Group = is-small l2 (type-∞-Group G) is-prop-is-small-∞-Group : is-prop is-small-∞-Group is-prop-is-small-∞-Group = is-prop-is-small l2 (type-∞-Group G)
The predicate of being a structurally small ∞-group
module _ {l1 : Level} (l2 : Level) (G : ∞-Group l1) where is-structurally-small-∞-Group : UU (l1 ⊔ lsuc l2) is-structurally-small-∞-Group = Σ (∞-Group l2) (equiv-∞-Group G) abstract is-prop-is-structurally-small-∞-Group : is-prop is-structurally-small-∞-Group is-prop-is-structurally-small-∞-Group = is-prop-equiv ( equiv-right-swap-Σ) ( is-prop-Σ ( is-prop-is-pointed-small-Pointed-Type ( classifying-pointed-type-∞-Group G)) ( λ H → is-prop-is-0-connected _)) is-structurally-small-prop-∞-Group : Prop (l1 ⊔ lsuc l2) pr1 is-structurally-small-prop-∞-Group = is-structurally-small-∞-Group pr2 is-structurally-small-prop-∞-Group = is-prop-is-structurally-small-∞-Group module _ {l1 l2 : Level} (G : ∞-Group l1) (H : is-structurally-small-∞-Group l2 G) where ∞-group-is-structurally-small-∞-Group : ∞-Group l2 ∞-group-is-structurally-small-∞-Group = pr1 H type-∞-group-is-structurally-small-∞-Group : UU l2 type-∞-group-is-structurally-small-∞-Group = type-∞-Group ∞-group-is-structurally-small-∞-Group equiv-∞-group-is-structurally-small-∞-Group : equiv-∞-Group G ∞-group-is-structurally-small-∞-Group equiv-∞-group-is-structurally-small-∞-Group = pr2 H equiv-is-structurally-small-∞-Group : type-∞-Group G ≃ type-∞-group-is-structurally-small-∞-Group equiv-is-structurally-small-∞-Group = equiv-equiv-∞-Group G ( ∞-group-is-structurally-small-∞-Group) ( equiv-∞-group-is-structurally-small-∞-Group)
The predicate of being a pointed small ∞-group
module _ {l1 : Level} (l2 : Level) (G : ∞-Group l1) where is-pointed-small-prop-∞-Group : Prop (l1 ⊔ lsuc l2) is-pointed-small-prop-∞-Group = is-pointed-small-prop-Pointed-Type l2 (classifying-pointed-type-∞-Group G) is-pointed-small-∞-Group : UU (l1 ⊔ lsuc l2) is-pointed-small-∞-Group = is-pointed-small-Pointed-Type l2 (classifying-pointed-type-∞-Group G) is-prop-is-pointed-small-∞-Group : is-prop is-pointed-small-∞-Group is-prop-is-pointed-small-∞-Group = is-prop-is-pointed-small-Pointed-Type (classifying-pointed-type-∞-Group G)
Properties
The classifying type of any small ∞-group is locally small
module _ {l1 l2 : Level} (G : ∞-Group l1) (H : is-small-∞-Group l2 G) where abstract is-locally-small-classifying-type-is-small-∞-Group' : (x y : classifying-type-∞-Group G) → shape-∞-Group G ＝ x → shape-∞-Group G ＝ y → is-small l2 (x ＝ y) is-locally-small-classifying-type-is-small-∞-Group' ._ ._ refl refl = H abstract is-locally-small-classifying-type-is-small-∞-Group : is-locally-small l2 (classifying-type-∞-Group G) is-locally-small-classifying-type-is-small-∞-Group x y = apply-twice-universal-property-trunc-Prop ( mere-eq-classifying-type-∞-Group G (shape-∞-Group G) x) ( mere-eq-classifying-type-∞-Group G (shape-∞-Group G) y) ( is-small-Prop l2 (x ＝ y)) ( is-locally-small-classifying-type-is-small-∞-Group' x y)
An ∞-group is small if and only if its classifying type is small
module _ {l1 l2 : Level} (G : ∞-Group l1) where abstract is-small-classifying-type-is-small-∞-Group : is-small-∞-Group l2 G → is-small l2 (classifying-type-∞-Group G) is-small-classifying-type-is-small-∞-Group H = is-small-equiv' ( im (point-∞-Group G)) ( compute-im-point-∞-Group G) ( replacement ( point-∞-Group G) ( is-small-unit) ( is-locally-small-classifying-type-is-small-∞-Group G H)) abstract is-small-is-small-classifying-type-∞-Group : is-small l2 (classifying-type-∞-Group G) → is-small-∞-Group l2 G is-small-is-small-classifying-type-∞-Group H = is-locally-small-is-small H (shape-∞-Group G) (shape-∞-Group G)
An ∞-group is small if and only if it is pointed small
module _ {l1 l2 : Level} (G : ∞-Group l1) where abstract is-pointed-small-is-small-∞-Group : is-small-∞-Group l2 G → is-pointed-small-∞-Group l2 G is-pointed-small-is-small-∞-Group H = is-pointed-small-is-small-Pointed-Type ( classifying-pointed-type-∞-Group G) ( is-small-classifying-type-is-small-∞-Group G H)
An ∞-group is small if and only if it is structurally small
module _ {l1 l2 : Level} (G : ∞-Group l1) where classifying-pointed-type-is-small-∞-Group : is-small-∞-Group l2 G → Pointed-Type l2 classifying-pointed-type-is-small-∞-Group H = pointed-type-is-pointed-small-Pointed-Type ( classifying-pointed-type-∞-Group G) ( is-pointed-small-is-small-∞-Group G H) classifying-type-is-small-∞-Group : is-small-∞-Group l2 G → UU l2 classifying-type-is-small-∞-Group H = type-is-pointed-small-Pointed-Type ( classifying-pointed-type-∞-Group G) ( is-pointed-small-is-small-∞-Group G H) abstract is-0-connected-classifying-type-is-small-∞-Group : (H : is-small-∞-Group l2 G) → is-0-connected (classifying-type-is-small-∞-Group H) is-0-connected-classifying-type-is-small-∞-Group H = is-0-connected-equiv' ( equiv-is-pointed-small-Pointed-Type ( classifying-pointed-type-∞-Group G) ( is-pointed-small-is-small-∞-Group G H)) ( is-0-connected-classifying-type-∞-Group G) ∞-group-is-small-∞-Group : is-small-∞-Group l2 G → ∞-Group l2 pr1 (∞-group-is-small-∞-Group H) = classifying-pointed-type-is-small-∞-Group H pr2 (∞-group-is-small-∞-Group H) = is-0-connected-classifying-type-is-small-∞-Group H pointed-type-∞-group-is-small-∞-Group : is-small-∞-Group l2 G → Pointed-Type l2 pointed-type-∞-group-is-small-∞-Group H = pointed-type-∞-Group (∞-group-is-small-∞-Group H) type-∞-group-is-small-∞-Group : is-small-∞-Group l2 G → UU l2 type-∞-group-is-small-∞-Group H = type-∞-Group (∞-group-is-small-∞-Group H) equiv-∞-group-is-small-∞-Group : (H : is-small-∞-Group l2 G) → equiv-∞-Group G (∞-group-is-small-∞-Group H) equiv-∞-group-is-small-∞-Group H = pointed-equiv-is-pointed-small-Pointed-Type ( classifying-pointed-type-∞-Group G) ( is-pointed-small-is-small-∞-Group G H) pointed-equiv-equiv-∞-group-is-small-∞-Group : (H : is-small-∞-Group l2 G) → pointed-type-∞-Group G ≃∗ pointed-type-∞-group-is-small-∞-Group H pointed-equiv-equiv-∞-group-is-small-∞-Group H = pointed-equiv-equiv-∞-Group G ( ∞-group-is-small-∞-Group H) ( equiv-∞-group-is-small-∞-Group H) equiv-equiv-∞-group-is-small-∞-Group : (H : is-small-∞-Group l2 G) → type-∞-Group G ≃ type-∞-group-is-small-∞-Group H equiv-equiv-∞-group-is-small-∞-Group H = equiv-equiv-∞-Group G ( ∞-group-is-small-∞-Group H) ( equiv-∞-group-is-small-∞-Group H) abstract is-structurally-small-is-small-∞-Group : is-small-∞-Group l2 G → is-structurally-small-∞-Group l2 G pr1 (is-structurally-small-is-small-∞-Group H) = ∞-group-is-small-∞-Group H pr2 (is-structurally-small-is-small-∞-Group H) = equiv-∞-group-is-small-∞-Group H abstract is-small-is-structurally-small-∞-Group : is-structurally-small-∞-Group l2 G → is-small-∞-Group l2 G pr1 (is-small-is-structurally-small-∞-Group H) = type-∞-group-is-structurally-small-∞-Group G H pr2 (is-small-is-structurally-small-∞-Group H) = equiv-is-structurally-small-∞-Group G H abstract is-small-∞-group-is-small-∞-Group : (H : is-small-∞-Group l2 G) → is-small-∞-Group l1 (∞-group-is-small-∞-Group H) pr1 (is-small-∞-group-is-small-∞-Group H) = type-∞-Group G pr2 (is-small-∞-group-is-small-∞-Group H) = inv-equiv (equiv-equiv-∞-group-is-small-∞-Group H)
Recent changes
- 2024-03-23. Egbert Rijke. Deloopings and Eilenberg-Mac Lane spaces (#1079).