Transitive group actions
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Elisabeth Bonnevier.
Created on 2022-03-18.
Last modified on 2023-05-01.
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.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
and y
in
X
there is a group element g
such that gx = y
.
Definition
module _ {l1 l2 : Level} (G : Group l1) (X : Abstract-Group-Action G l2) where is-transitive-Abstract-Group-Action : Prop (l1 ⊔ l2) is-transitive-Abstract-Group-Action = Π-Prop ( type-Abstract-Group-Action G X) ( λ x → Π-Prop ( type-Abstract-Group-Action G X) ( λ y → ∃-Prop ( type-Group G) ( λ g → Id (mul-Abstract-Group-Action G X g x) y)))
Recent changes
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490).