The orbit category of a group

Content created by Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2023-11-24.

module group-theory.category-of-orbits-groups where
Imports 
open import category-theory.categories
open import category-theory.full-large-subcategories
open import category-theory.isomorphisms-in-large-precategories
open import category-theory.large-categories
open import category-theory.large-precategories
open import category-theory.precategories

open import foundation.dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.universe-levels

open import group-theory.category-of-group-actions
open import group-theory.group-actions
open import group-theory.groups
open import group-theory.homomorphisms-group-actions
open import group-theory.isomorphisms-group-actions
open import group-theory.precategory-of-group-actions
open import group-theory.transitive-group-actions

Idea

The orbit category of a group 𝒪(G) is the full subcategory of the category of G-sets consisting of orbits of G, i.e. transitive G-sets. Equivalently, an orbit of G is a G-set that is merely equivalent to a quotient G-set G/H for some subgroup H.

Definitions

The large orbit category of a group

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

  orbit-Group-Full-Large-Subcategory :
    Full-Large-Subcategory (l1 ⊔_) (action-Group-Large-Category G)
  orbit-Group-Full-Large-Subcategory = is-transitive-prop-action-Group G

  orbit-Group-Large-Category :
    Large-Category (λ l → l1 ⊔ lsuc l) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
  orbit-Group-Large-Category =
    large-category-Full-Large-Subcategory
      ( action-Group-Large-Category G)
      ( orbit-Group-Full-Large-Subcategory)

The large orbit precategory of a group

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

  orbit-Group-Large-Precategory :
    Large-Precategory (λ l → l1 ⊔ lsuc l) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
  orbit-Group-Large-Precategory =
    large-precategory-Large-Category (orbit-Group-Large-Category G)

The small orbit category of a group

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

  orbit-Group-Category : (l2 : Level) → Category (l1 ⊔ lsuc l2) (l1 ⊔ l2)
  orbit-Group-Category = category-Large-Category (orbit-Group-Large-Category G)

The small orbit precategory of a group

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

  orbit-Group-Precategory : (l2 : Level) → Precategory (l1 ⊔ lsuc l2) (l1 ⊔ l2)
  orbit-Group-Precategory =
    precategory-Large-Category (orbit-Group-Large-Category G)

Recent changes