Transitive higher group actions

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-30.

module higher-group-theory.transitive-higher-group-actions where

Imports
open import foundation.0-connected-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.inhabited-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.regensburg-extension-fundamental-theorem-of-identity-types
open import foundation.surjective-maps
open import foundation.transport-along-identifications
open import foundation.universe-levels

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


Idea

Consider an ∞-group G and an ∞-group action of G on X. We say that X is transitive if its type of orbits is connected.

Equivalently, we say that X is abstractly transitive if the underlying type of X is inhabited and for any element x : X (sh G) of the underlying type of X the action map

  g ↦ mul-action-∞-Group G X g x


is surjective. The equivalence of these two conditions is established via the Regensburg extension of the fundamental theorem of identity types.

Note that it is necessary to include the condition that X is inhabited in the condition that G acts transitively on X. A first reason is that this makes the condition of being abstractly transitive equivalent to the condition of being transitive. A second reason is that this way we will be able to recover the familiar property that a G-action X is a G-torsor if and only if it is both free and transitive.

Definitions

The predicate of being a transitive higher group action

module _
{l1 l2 : Level} (G : ∞-Group l1) (X : action-∞-Group l2 G)
where

is-transitive-prop-action-∞-Group : Prop (l1 ⊔ l2)
is-transitive-prop-action-∞-Group =
is-0-connected-Prop (orbit-action-∞-Group 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


The predicate of being an abstractly transitive higher group action

module _
{l1 l2 : Level} (G : ∞-Group l1) (X : action-∞-Group l2 G)
where

is-abstractly-transitive-prop-action-∞-Group : Prop (l1 ⊔ l2)
is-abstractly-transitive-prop-action-∞-Group =
product-Prop
( is-inhabited-Prop (type-action-∞-Group G X))
( Π-Prop
( type-action-∞-Group G X)
( λ x → is-surjective-Prop (λ g → mul-action-∞-Group G X g x)))

is-abstractly-transitive-action-∞-Group : UU (l1 ⊔ l2)
is-abstractly-transitive-action-∞-Group =
type-Prop is-abstractly-transitive-prop-action-∞-Group

is-prop-is-abstractly-transitive-action-∞-Group :
is-prop is-abstractly-transitive-action-∞-Group
is-prop-is-abstractly-transitive-action-∞-Group =
is-prop-type-Prop is-abstractly-transitive-prop-action-∞-Group


Transitive higher group actions

transitive-action-∞-Group :
{l1 : Level} (l2 : Level) (G : ∞-Group l1) → UU (l1 ⊔ lsuc l2)
transitive-action-∞-Group l2 G =
Σ (action-∞-Group l2 G) (is-transitive-action-∞-Group G)

module _
{l1 l2 : Level} (G : ∞-Group l1) (X : transitive-action-∞-Group l2 G)
where

action-transitive-action-∞-Group : action-∞-Group l2 G
action-transitive-action-∞-Group = pr1 X

is-transitive-transitive-action-∞-Group :
is-transitive-action-∞-Group G action-transitive-action-∞-Group
is-transitive-transitive-action-∞-Group = pr2 X

type-transitive-action-∞-Group : UU l2
type-transitive-action-∞-Group =
type-action-∞-Group G action-transitive-action-∞-Group

mul-transitive-action-∞-Group :
type-∞-Group G →
type-transitive-action-∞-Group → type-transitive-action-∞-Group
mul-transitive-action-∞-Group =
mul-action-∞-Group G action-transitive-action-∞-Group

associative-mul-transitive-action-∞-Group :
(g h : type-∞-Group G) (x : type-transitive-action-∞-Group) →
mul-transitive-action-∞-Group (mul-∞-Group G g h) x ＝
mul-transitive-action-∞-Group h (mul-transitive-action-∞-Group g x)
associative-mul-transitive-action-∞-Group =
associative-mul-action-∞-Group G action-transitive-action-∞-Group

unit-law-mul-transitive-action-∞-Group :
(x : type-transitive-action-∞-Group) →
mul-transitive-action-∞-Group (unit-∞-Group G) x ＝ x
unit-law-mul-transitive-action-∞-Group =
unit-law-mul-action-∞-Group G action-transitive-action-∞-Group


Properties

If an action is abstractly transitive, then transport is surjective

module _
{l1 l2 : Level} (G : ∞-Group l1) (X : action-∞-Group l2 G)
where

abstract
is-surjective-tr-is-abstractly-transitive-action-∞-Group :
is-abstractly-transitive-action-∞-Group G X →
(u : classifying-type-∞-Group G)
(x : X (shape-∞-Group G)) →
is-surjective (λ (p : shape-∞-Group G ＝ u) → tr X p x)
is-surjective-tr-is-abstractly-transitive-action-∞-Group H u x =
apply-universal-property-trunc-Prop
( mere-eq-classifying-type-∞-Group G (shape-∞-Group G) u)
( is-surjective-Prop _)
( λ where refl → pr2 H x)


An action is transitive if and only if it is abstractly transitive

module _
{l1 l2 : Level} (G : ∞-Group l1) (X : action-∞-Group l2 G)
where

is-transitive-is-abstractly-transitive-action-∞-Group :
is-abstractly-transitive-action-∞-Group G X →
is-transitive-action-∞-Group G X
is-transitive-is-abstractly-transitive-action-∞-Group (H , K) =
forward-implication-extended-fundamental-theorem-id-surjective
( shape-∞-Group G)
( is-0-connected-classifying-type-∞-Group G)
( λ f u →
is-surjective-htpy
( compute-map-out-of-identity-type f u)
( is-surjective-tr-is-abstractly-transitive-action-∞-Group G X
( H , K)
( u)
( f (shape-∞-Group G) refl)))
( H)

abstract
is-inhabited-is-transitive-action-∞-Group :
is-transitive-action-∞-Group G X → is-inhabited (type-action-∞-Group G X)
is-inhabited-is-transitive-action-∞-Group H =
apply-universal-property-trunc-Prop
( is-inhabited-is-0-connected H)
( is-inhabited-Prop _)
( λ (u , x) →
apply-universal-property-trunc-Prop
( mere-eq-classifying-type-∞-Group G (shape-∞-Group G) u)
( is-inhabited-Prop _)
( λ where refl → unit-trunc-Prop x))

is-surjective-mul-right-is-transitive-action-∞-Group :
is-transitive-action-∞-Group G X →
(x : type-action-∞-Group G X) →
is-surjective (λ g → mul-action-∞-Group G X g x)
is-surjective-mul-right-is-transitive-action-∞-Group H x =
backward-implication-extended-fundamental-theorem-id-surjective
( shape-∞-Group G)
( H)
( λ u p → tr X p x)
( shape-∞-Group G)

is-abstractly-transitive-is-transitive-action-∞-Group :
is-transitive-action-∞-Group G X →
is-abstractly-transitive-action-∞-Group G X
pr1 (is-abstractly-transitive-is-transitive-action-∞-Group H) =
is-inhabited-is-transitive-action-∞-Group H
pr2 (is-abstractly-transitive-is-transitive-action-∞-Group H) =
is-surjective-mul-right-is-transitive-action-∞-Group H

module _
{l1 l2 : Level} (G : ∞-Group l1) (X : transitive-action-∞-Group l2 G)
where

is-inhabited-transitive-action-∞-Group :
is-inhabited (type-transitive-action-∞-Group G X)
is-inhabited-transitive-action-∞-Group =
is-inhabited-is-transitive-action-∞-Group G
( action-transitive-action-∞-Group G X)
( is-transitive-transitive-action-∞-Group G X)

inhabited-type-transitive-action-∞-Group :
Inhabited-Type l2
pr1 inhabited-type-transitive-action-∞-Group =
type-transitive-action-∞-Group G X
pr2 inhabited-type-transitive-action-∞-Group =
is-inhabited-transitive-action-∞-Group

is-abstractly-transitive-transitive-action-∞-Group :
is-abstractly-transitive-action-∞-Group G
( action-transitive-action-∞-Group G X)
is-abstractly-transitive-transitive-action-∞-Group =
is-abstractly-transitive-is-transitive-action-∞-Group G
( action-transitive-action-∞-Group G X)
( is-transitive-transitive-action-∞-Group G X)

is-surjective-tr-transitive-action-∞-Group :
(u : classifying-type-∞-Group G) (x : type-transitive-action-∞-Group G X) →
is-surjective
( λ (p : shape-∞-Group G ＝ u) →
tr (action-transitive-action-∞-Group G X) p x)
is-surjective-tr-transitive-action-∞-Group =
is-surjective-tr-is-abstractly-transitive-action-∞-Group G
( action-transitive-action-∞-Group G X)
( is-abstractly-transitive-transitive-action-∞-Group)

is-surjective-mul-right-transitive-action-∞-Group :
(x : type-transitive-action-∞-Group G X) →
is-surjective (λ g → mul-transitive-action-∞-Group G X g x)
is-surjective-mul-right-transitive-action-∞-Group =
is-surjective-tr-transitive-action-∞-Group (shape-∞-Group G)