Orbits of concrete group actions

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

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

module group-theory.orbits-concrete-group-actions where
Imports 
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.sets
open import foundation.universe-levels

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

Idea

The type of orbits of a concrete group action of G on X is defined to be the total space

  Σ (u : BG), X u.

of the type family X over the classifying type of the concrete group G. The idea is that the "standard" elements of this type are of the form (* , x), where x is an element of the underlying set X * of X, and that the type of identifications from (* , x) to (* , y) is equivalent to the type

  Σ (g : G), g x ＝ y.

In other words, identifications between the elements (* , x) and (* , y) in the type of orbits of X are equivalently described as group elements g such that g x ＝ y.

Note that the type of orbits of a concrete group is typically a 1-type. In Free concrete group actions we will show that the type of orbits is a set if and only if the action of G on X is free, and in Transitive concrete group actions we will show that the type of orbits is 0-connected if and only if the action is transitive.

Definition

orbit-action-Concrete-Group :
  {l1 l2 : Level} (G : Concrete-Group l1) (X : action-Concrete-Group l2 G) →
  UU (l1 ⊔ l2)
orbit-action-Concrete-Group G X =
  Σ (classifying-type-Concrete-Group G) (type-Set ∘ X)

See also

Recent changes