Transitive group actions

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

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

module group-theory.transitive-group-actions where
open import foundation.existential-quantification
open import foundation.identity-types
open import foundation.propositions
open import foundation.surjective-maps
open import foundation.universe-levels

open import
open import group-theory.groups


A group G is said to act transitively on a set X if for every x : X the map

  g ↦ gx : G → X

is surjective. In other words, a group action is transitive if any two elements are in the same orbit.


The predicate of being a transitive G-set

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

  is-transitive-prop-action-Group : Prop (l1  l2)
  is-transitive-prop-action-Group =
      ( type-action-Group G X)
      ( λ x  is-surjective-Prop  g  mul-action-Group G X g x))

  is-transitive-action-Group : UU (l1  l2)
  is-transitive-action-Group = type-Prop is-transitive-prop-action-Group

  is-prop-is-transitive-action-Group : is-prop is-transitive-action-Group
  is-prop-is-transitive-action-Group =
    is-prop-type-Prop is-transitive-prop-action-Group

Recent changes