Trivial concrete groups

Content created by Fredrik Bakke.

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

module group-theory.trivial-concrete-groups where
Imports 
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.truncation-levels
open import foundation.unit-type
open import foundation.universe-levels

open import group-theory.concrete-groups

open import higher-group-theory.trivial-higher-groups

Idea

A concrete group G is trivial if its classifying type is contractible.

Definitions

Trivial higher groups

module _
  {l : Level} (G : Concrete-Group l)
  where

  is-trivial-prop-Concrete-Group : Prop l
  is-trivial-prop-Concrete-Group =
    is-trivial-prop-∞-Group (∞-group-Concrete-Group G)

  is-trivial-Concrete-Group : UU l
  is-trivial-Concrete-Group = type-Prop is-trivial-prop-Concrete-Group

  is-property-is-trivial-Concrete-Group : is-prop (is-trivial-Concrete-Group)
  is-property-is-trivial-Concrete-Group =
    is-prop-type-Prop is-trivial-prop-Concrete-Group

Higher groups with contractible classifying type

module _
  {l : Level} (G : Concrete-Group l)
  where

  has-contractible-classifying-type-prop-Concrete-Group : Prop l
  has-contractible-classifying-type-prop-Concrete-Group =
    has-contractible-classifying-type-prop-∞-Group (∞-group-Concrete-Group G)

  has-contractible-classifying-type-Concrete-Group : UU l
  has-contractible-classifying-type-Concrete-Group =
    type-Prop has-contractible-classifying-type-prop-Concrete-Group

  is-property-has-contractible-classifying-type-Concrete-Group :
    is-prop (has-contractible-classifying-type-Concrete-Group)
  is-property-has-contractible-classifying-type-Concrete-Group =
    is-prop-type-Prop has-contractible-classifying-type-prop-Concrete-Group

The trivial concrete group

trivial-Concrete-Group : {l : Level} → Concrete-Group l
pr1 trivial-Concrete-Group = trivial-∞-Group
pr2 trivial-Concrete-Group =
  is-trunc-is-contr (one-𝕋) (is-contr-raise-unit) (raise-star) (raise-star)

has-contractible-classifying-type-trivial-Concrete-Group :
  {l : Level} →
  has-contractible-classifying-type-Concrete-Group (trivial-Concrete-Group {l})
has-contractible-classifying-type-trivial-Concrete-Group =
  has-contractible-classifying-type-trivial-∞-Group

Properties

Having contractible classifying type is equivalent to having contractible underlying type

This remains to be formalized.

Recent changes