The precategory of group actions

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

Created on 2022-03-17.
Last modified on 2024-03-11.

module group-theory.precategory-of-group-actions where
Imports
open import category-theory.large-precategories
open import category-theory.precategories

open import foundation.universe-levels

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

Idea

The large precategory of group actions consists of group actions and morphisms of group actions between them.

Definitions

The large precategory of G-sets

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

  action-Group-Large-Precategory :
    Large-Precategory  l2  l1  lsuc l2)  l2 l3  l1  l2  l3)
  action-Group-Large-Precategory =
    make-Large-Precategory
      ( action-Group G)
      ( hom-set-action-Group G)
      ( λ {l1} {l2} {l3} {X} {Y} {Z}  comp-hom-action-Group G X Y Z)
      ( λ {l1} {X}  id-hom-action-Group G X)
      ( λ {l1} {l2} {l3} {l4} {X} {Y} {Z} {W} 
        associative-comp-hom-action-Group G X Y Z W)
      ( λ {l1} {l2} {X} {Y}  left-unit-law-comp-hom-action-Group G X Y)
      ( λ {l1} {l2} {X} {Y}  right-unit-law-comp-hom-action-Group G X Y)

The small precategory of G-sets

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

  action-Group-Precategory :
    (l2 : Level)  Precategory (l1  lsuc l2) (l1  l2)
  action-Group-Precategory =
    precategory-Large-Precategory (action-Group-Large-Precategory G)

Recent changes