Orbits of group actions
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-03-17.
Last modified on 2023-03-13.
module group-theory.orbits-group-actions where
Imports
open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels open import group-theory.group-actions open import group-theory.groups
Idea
The orbit of an element x
in a G-set X
is the set of elements of the form
gx
.
Definition
module _ {l1 l2 : Level} (G : Group l1) (X : Abstract-Group-Action G l2) where hom-orbit-Abstract-Group-Action : (x y : type-Abstract-Group-Action G X) → UU (l1 ⊔ l2) hom-orbit-Abstract-Group-Action x y = Σ (type-Group G) (λ g → Id (mul-Abstract-Group-Action G X g x) y)
Recent changes
- 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). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).