Free concrete group actions

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

Created on 2022-07-09.
Last modified on 2023-03-10.

module group-theory.free-concrete-group-actions where

Imports

open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import group-theory.concrete-group-actions
open import group-theory.concrete-groups
open import group-theory.orbits-concrete-group-actions

Definition

is-free-action-Concrete-Group-Prop :
  {l1 l2 : Level} (G : Concrete-Group l1) → action-Concrete-Group l2 G →
  Prop (l1 ⊔ l2)
is-free-action-Concrete-Group-Prop G X =
  is-set-Prop (orbit-action-Concrete-Group G X)

is-free-action-Concrete-Group :
  {l1 l2 : Level} (G : Concrete-Group l1) → action-Concrete-Group l2 G →
  UU (l1 ⊔ l2)
is-free-action-Concrete-Group G X =
  type-Prop (is-free-action-Concrete-Group-Prop G X)

is-prop-is-free-action-Concrete-Group :
  {l1 l2 : Level} (G : Concrete-Group l1) (X : action-Concrete-Group l2 G) →
  is-prop (is-free-action-Concrete-Group G X)
is-prop-is-free-action-Concrete-Group G X =
  is-prop-type-Prop (is-free-action-Concrete-Group-Prop G X)

Recent changes

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).
2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).