Principal torsors of concrete groups

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2022-07-09.
Last modified on 2023-11-04.

module group-theory.principal-torsors-concrete-groups where

open import foundation.universe-levels

open import group-theory.concrete-group-actions
open import group-theory.concrete-groups

Idea

The principal torsor of a concrete group G is the identity type of BG.

Definition

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

  principal-torsor-Concrete-Group :
    classifying-type-Concrete-Group G → action-Concrete-Group l1 G
  principal-torsor-Concrete-Group = Id-BG-Set G

Recent changes

• 2023-11-04. Fredrik Bakke. Small fixes concrete groups (#897).
• 2023-03-10. Fredrik Bakke. Additions to fix-import (#497).
• 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
• 2023-03-07. Fredrik Bakke. Add blank lines between <details> tags and markdown syntax (#490).
• 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).