# Transitive group actions

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

Created on 2022-03-18.

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