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
Imports 
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 group-theory.group-actions
open import group-theory.groups

Idea

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.

Definitions

The predicate of being a transitive G-set

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

  is-transitive-prop-action-Group : Prop (l1 ⊔ l2)
  is-transitive-prop-action-Group =
    Π-Prop
      ( 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