# The precategory of orbits of a monoid action

Content created by Fredrik Bakke.

Created on 2024-03-11.

module group-theory.precategory-of-orbits-monoid-actions where

Imports
open import category-theory.precategories

open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import group-theory.monoid-actions
open import group-theory.monoids


## Idea

The precategory of orbits of a monoid action of M on X consists of the elements of the set X as the objects, and a morphism from x to y is an element m of the monoid M such that mx = y.

## Definition

### The precategory of orbits of a monoid action

module _
{l1 l2 : Level} (M : Monoid l1) (X : action-Monoid l2 M)
where

hom-orbit-action-Monoid : (x y : type-action-Monoid M X) → UU (l1 ⊔ l2)
hom-orbit-action-Monoid x y =
Σ (type-Monoid M) ( λ m → Id (mul-action-Monoid M X m x) y)

element-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} → hom-orbit-action-Monoid x y → type-Monoid M
element-hom-orbit-action-Monoid f = pr1 f

eq-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} (f : hom-orbit-action-Monoid x y) →
Id (mul-action-Monoid M X (element-hom-orbit-action-Monoid f) x) y
eq-hom-orbit-action-Monoid f = pr2 f

htpy-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} (f g : hom-orbit-action-Monoid x y) →
UU l1
htpy-hom-orbit-action-Monoid {x} {y} f g =
Id
( element-hom-orbit-action-Monoid f)
( element-hom-orbit-action-Monoid g)

refl-htpy-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} (f : hom-orbit-action-Monoid x y) →
htpy-hom-orbit-action-Monoid f f
refl-htpy-hom-orbit-action-Monoid f = refl

htpy-eq-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} (f g : hom-orbit-action-Monoid x y) →
Id f g → htpy-hom-orbit-action-Monoid f g
htpy-eq-hom-orbit-action-Monoid f .f refl =
refl-htpy-hom-orbit-action-Monoid f

is-torsorial-htpy-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} (f : hom-orbit-action-Monoid x y) →
is-torsorial (htpy-hom-orbit-action-Monoid f)
is-torsorial-htpy-hom-orbit-action-Monoid {x} {y} f =
is-torsorial-Eq-subtype
( is-torsorial-Id (element-hom-orbit-action-Monoid f))
( λ u →
is-set-type-action-Monoid M X (mul-action-Monoid M X u x) y)
( element-hom-orbit-action-Monoid f)
( refl)
( eq-hom-orbit-action-Monoid f)

is-equiv-htpy-eq-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} (f g : hom-orbit-action-Monoid x y) →
is-equiv (htpy-eq-hom-orbit-action-Monoid f g)
is-equiv-htpy-eq-hom-orbit-action-Monoid f =
fundamental-theorem-id
( is-torsorial-htpy-hom-orbit-action-Monoid f)
( htpy-eq-hom-orbit-action-Monoid f)

extensionality-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} (f g : hom-orbit-action-Monoid x y) →
Id f g ≃ htpy-hom-orbit-action-Monoid f g
pr1 (extensionality-hom-orbit-action-Monoid f g) =
htpy-eq-hom-orbit-action-Monoid f g
pr2 (extensionality-hom-orbit-action-Monoid f g) =
is-equiv-htpy-eq-hom-orbit-action-Monoid f g

eq-htpy-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} {f g : hom-orbit-action-Monoid x y} →
htpy-hom-orbit-action-Monoid f g → Id f g
eq-htpy-hom-orbit-action-Monoid {x} {y} {f} {g} =
map-inv-is-equiv (is-equiv-htpy-eq-hom-orbit-action-Monoid f g)

is-prop-htpy-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} (f g : hom-orbit-action-Monoid x y) →
is-prop (htpy-hom-orbit-action-Monoid f g)
is-prop-htpy-hom-orbit-action-Monoid f g =
is-set-type-Monoid M
( element-hom-orbit-action-Monoid f)
( element-hom-orbit-action-Monoid g)

is-set-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} →
is-set (hom-orbit-action-Monoid x y)
is-set-hom-orbit-action-Monoid {x} {y} f g =
is-prop-equiv
( extensionality-hom-orbit-action-Monoid f g)
( is-prop-htpy-hom-orbit-action-Monoid f g)

hom-orbit-monoid-action-Set :
(x y : type-action-Monoid M X) → Set (l1 ⊔ l2)
pr1 (hom-orbit-monoid-action-Set x y) = hom-orbit-action-Monoid x y
pr2 (hom-orbit-monoid-action-Set x y) = is-set-hom-orbit-action-Monoid

id-hom-orbit-action-Monoid :
(x : type-action-Monoid M X) → hom-orbit-action-Monoid x x
pr1 (id-hom-orbit-action-Monoid x) = unit-Monoid M
pr2 (id-hom-orbit-action-Monoid x) = unit-law-mul-action-Monoid M X x

comp-hom-orbit-action-Monoid :
{x y z : type-action-Monoid M X} →
hom-orbit-action-Monoid y z → hom-orbit-action-Monoid x y →
hom-orbit-action-Monoid x z
pr1 (comp-hom-orbit-action-Monoid g f) =
mul-Monoid M
( element-hom-orbit-action-Monoid g)
( element-hom-orbit-action-Monoid f)
pr2 (comp-hom-orbit-action-Monoid {x} g f) =
( associative-mul-action-Monoid M X
( element-hom-orbit-action-Monoid g)
( element-hom-orbit-action-Monoid f)
( x)) ∙
( ap-mul-action-Monoid M X (eq-hom-orbit-action-Monoid f)) ∙
( eq-hom-orbit-action-Monoid g)

associative-comp-hom-orbit-action-Monoid :
{x y z w : type-action-Monoid M X} (h : hom-orbit-action-Monoid z w)
(g : hom-orbit-action-Monoid y z) (f : hom-orbit-action-Monoid x y) →
comp-hom-orbit-action-Monoid (comp-hom-orbit-action-Monoid h g) f ＝
comp-hom-orbit-action-Monoid h (comp-hom-orbit-action-Monoid g f)
associative-comp-hom-orbit-action-Monoid h g f =
eq-htpy-hom-orbit-action-Monoid
( associative-mul-Monoid M
( element-hom-orbit-action-Monoid h)
( element-hom-orbit-action-Monoid g)
( element-hom-orbit-action-Monoid f))

left-unit-law-comp-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} (f : hom-orbit-action-Monoid x y) →
Id (comp-hom-orbit-action-Monoid (id-hom-orbit-action-Monoid y) f) f
left-unit-law-comp-hom-orbit-action-Monoid f =
eq-htpy-hom-orbit-action-Monoid
( left-unit-law-mul-Monoid M (element-hom-orbit-action-Monoid f))

right-unit-law-comp-hom-orbit-action-Monoid :
{x y : type-action-Monoid M X} (f : hom-orbit-action-Monoid x y) →
Id (comp-hom-orbit-action-Monoid f (id-hom-orbit-action-Monoid x)) f
right-unit-law-comp-hom-orbit-action-Monoid f =
eq-htpy-hom-orbit-action-Monoid
( right-unit-law-mul-Monoid M (element-hom-orbit-action-Monoid f))

orbit-monoid-action-Precategory : Precategory l2 (l1 ⊔ l2)
orbit-monoid-action-Precategory =
make-Precategory
( type-action-Monoid M X)
( hom-orbit-monoid-action-Set)
( comp-hom-orbit-action-Monoid)
( id-hom-orbit-action-Monoid)
( associative-comp-hom-orbit-action-Monoid)
( left-unit-law-comp-hom-orbit-action-Monoid)
( right-unit-law-comp-hom-orbit-action-Monoid)