Orbits of concrete group actions
Content created by Jonathan Prieto-Cubides, Egbert Rijke and Fredrik Bakke.
Created on 2022-07-09.
Last modified on 2023-11-24.
module group-theory.orbits-concrete-group-actions where
Imports
open import foundation.dependent-pair-types open import foundation.function-types open import foundation.sets open import foundation.universe-levels open import group-theory.concrete-group-actions open import group-theory.concrete-groups
Idea
The type of orbits of a
concrete group action of G
on X
is
defined to be the total space
Σ (u : BG), X u.
of the type family X
over the classifying type of the
concrete group G
. The idea is that the
"standard" elements of this type are of the form (* , x)
, where x
is an
element of the underlying set X *
of X
, and that
the type of identifications from (* , x)
to (* , y)
is equivalent to the type
Σ (g : G), g x = y.
In other words, identifications between the elements (* , x)
and (* , y)
in
the type of orbits of X
are equivalently described as group elements g
such
that g x = y
.
Note that the type of orbits of a concrete group is typically a
1
-type. In
Free concrete group actions we
will show that the type of orbits is a set if and only if the action of G
on
X
is free, and in
Transitive concrete group actions
we will show that the type of orbits is
0
-connected if and only if the action is
transitive.
Definition
orbit-action-Concrete-Group : {l1 l2 : Level} (G : Concrete-Group l1) (X : action-Concrete-Group l2 G) → UU (l1 ⊔ l2) orbit-action-Concrete-Group G X = Σ (classifying-type-Concrete-Group G) (type-Set ∘ X)
See also
Recent changes
- 2023-11-24. Egbert Rijke. Abelianization (#877).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 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).