Orbits of group actions

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

Created on 2022-03-17.
Last modified on 2023-11-24.

module group-theory.orbits-group-actions where
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

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


The groupoid of orbits of a group action consists of elements of X, and a morphism from x to y is given by an element g of the group G such that gx = y.


module _
  {l1 l2 : Level} (G : Group l1) (X : action-Group G l2)

  hom-orbit-action-Group :
    (x y : type-action-Group G X)  UU (l1  l2)
  hom-orbit-action-Group x y =
    Σ (type-Group G)  g  mul-action-Group G X g x  y)

Recent changes