# The substitution functor of group actions

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Elisabeth Stenholm, Julian KG, Victor Blanchi, fernabnor and louismntnu.

Created on 2022-03-17.

module group-theory.substitution-functor-group-actions where

Imports
open import category-theory.functors-large-precategories

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalence-classes
open import foundation.equivalence-relations
open import foundation.existential-quantification
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.sets
open import foundation.universe-levels

open import group-theory.group-actions
open import group-theory.groups
open import group-theory.homomorphisms-group-actions
open import group-theory.homomorphisms-groups
open import group-theory.precategory-of-group-actions
open import group-theory.symmetric-groups


## Idea

Given a group homomorphism f : G → H and an H-set Y, we obtain a G-action on Y by g,x ↦ f(g)x. This operation is functorial in Y.

## Definition

module _
{l1 l2 : Level} {G : Group l1} {H : Group l2} (f : hom-Group G H)
where

obj-subst-action-Group :
{l3 : Level} → action-Group H l3 → action-Group G l3
pr1 (obj-subst-action-Group X) = set-action-Group H X
pr2 (obj-subst-action-Group X) =
comp-hom-Group G H
( symmetric-Group (set-action-Group H X))
( pr2 X)
( f)

hom-subst-action-Group :
{l3 l4 : Level}
(X : action-Group H l3) (Y : action-Group H l4) →
hom-action-Group H X Y →
hom-action-Group G
( obj-subst-action-Group X)
( obj-subst-action-Group Y)
pr1 (hom-subst-action-Group X Y h) = pr1 h
pr2 (hom-subst-action-Group X Y h) x = pr2 h (map-hom-Group G H f x)

preserves-id-subst-action-Group :
{l3 : Level} (X : action-Group H l3) →
Id
( hom-subst-action-Group X X (id-hom-action-Group H X))
( id-hom-action-Group G (obj-subst-action-Group X))
preserves-id-subst-action-Group X = refl

preserves-comp-subst-action-Group :
{l3 l4 l5 : Level} (X : action-Group H l3)
(Y : action-Group H l4) (Z : action-Group H l5)
(g : hom-action-Group H Y Z)
(f : hom-action-Group H X Y) →
Id
( hom-subst-action-Group X Z
( comp-hom-action-Group H X Y Z g f))
( comp-hom-action-Group G
( obj-subst-action-Group X)
( obj-subst-action-Group Y)
( obj-subst-action-Group Z)
( hom-subst-action-Group Y Z g)
( hom-subst-action-Group X Y f))
preserves-comp-subst-action-Group X Y Z g f = refl

subst-action-Group :
functor-Large-Precategory (λ l → l)
( action-Group-Large-Precategory H)
( action-Group-Large-Precategory G)
obj-functor-Large-Precategory subst-action-Group =
obj-subst-action-Group
hom-functor-Large-Precategory subst-action-Group {X = X} {Y} =
hom-subst-action-Group X Y
preserves-comp-functor-Large-Precategory subst-action-Group
{l1} {l2} {l3} {X} {Y} {Z} =
preserves-comp-subst-action-Group X Y Z
preserves-id-functor-Large-Precategory
subst-action-Group {l1} {X} =
preserves-id-subst-action-Group X


## Properties

### The substitution functor has a left adjoint

module _
{l1 l2 : Level} {G : Group l1} {H : Group l2} (f : hom-Group G H)
where

{l3 : Level} → action-Group G l3 → Set (l2 ⊔ l3)
product-Set (set-Group H) (set-action-Group G X)

{l3 : Level} → action-Group G l3 → UU (l2 ⊔ l3)

{l3 : Level} (X : action-Group G l3) →

{l3 : Level} (X : action-Group G l3) →
equivalence-relation
( l1 ⊔ l2 ⊔ l3)
pr1
( h , x)
( h' , x') =
exists-structure-Prop
( type-Group G)
( λ g →
( Id (mul-Group H (map-hom-Group G H f g) h) h') ×
( Id (mul-action-Group G X g x) x'))
pr1
( h , x) =
intro-exists
( unit-Group G)
( pair
( ( ap (mul-Group' H h) (preserves-unit-hom-Group G H f)) ∙
( left-unit-law-mul-Group H h))
( preserves-unit-mul-action-Group G X x))
pr1
( pr2
( pr2
( h , x)
( h' , x')
( e) =
apply-universal-property-trunc-Prop e
( pr1
( h' , x')
( h , x))
( λ (g , p , q) →
intro-exists
( inv-Group G g)
( ( ( ap
( mul-Group' H h')
( preserves-inv-hom-Group G H f)) ∙
( inv (transpose-eq-mul-Group' H p))) ,
( inv (transpose-eq-mul-action-Group G X g x x' q))))
pr2
( pr2
( pr2
( h , x)
( h' , x')
( h'' , x'')
( d)
( e) =
apply-universal-property-trunc-Prop e
( pr1
( h , x)
( h'' , x''))
( λ (g , p , q) →
apply-universal-property-trunc-Prop d
( pr1
( X))
( h , x)
( h'' , x''))
( λ (g' , p' , q') →
intro-exists
( mul-Group G g' g)
( ( ( ap
( mul-Group' H h)
( preserves-mul-hom-Group G H f)) ∙
( associative-mul-Group H
( map-hom-Group G H f g')
( map-hom-Group G H f g)
( h)) ∙
( ap (mul-Group H (map-hom-Group G H f g')) p) ∙
( p')) ,
( ( preserves-mul-action-Group G X g' g x) ∙
( ap (mul-action-Group G X g') q) ∙
( q')))))