# Homomorphisms of generated subgroups

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Eléonore Mangel and Maša Žaucer.

Created on 2022-04-24.

module group-theory.homomorphisms-generated-subgroups where

Imports
open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.unit-type
open import foundation.universe-levels

open import group-theory.epimorphisms-groups
open import group-theory.full-subgroups
open import group-theory.generating-sets-groups
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.subgroups
open import group-theory.subgroups-generated-by-subsets-groups
open import group-theory.subsets-groups

open import lists.lists

open import univalent-combinatorics.standard-finite-types


## Idea

A group homomorphism from a subgroup generated by a subset S is defined by its values on S.

## Theorem

module _
{l1 l2 l3 : Level} (G : Group l1) (S : subset-Group l2 G) (G' : Group l3)
where

distributivity-hom-group-ev-formal-combination :
( f : hom-Group (group-Subgroup G (subgroup-subset-Group G S)) G') →
( l : formal-combination-subset-Group G S) →
Id
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( f)
( ( ev-formal-combination-subset-Group G S l) ,
( unit-trunc-Prop (l , refl))))
( fold-list
( unit-Group G')
( λ (s , x) →
mul-Group
( G')
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( f)
( ( ev-formal-combination-subset-Group G S (unit-list (s , x))) ,
( unit-trunc-Prop (unit-list (s , x) , refl)))))
( l))
distributivity-hom-group-ev-formal-combination f nil =
preserves-unit-hom-Group (group-Subgroup G (subgroup-subset-Group G S)) G' f
distributivity-hom-group-ev-formal-combination f (cons (s , x) l) =
( ap
( map-hom-Group (group-Subgroup G (subgroup-subset-Group G S)) G' f)
( eq-pair-Σ
( preserves-concat-ev-formal-combination-subset-Group G S
( unit-list (s , x))
( l))
( eq-is-prop is-prop-type-trunc-Prop))) ∙
( preserves-mul-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( f)) ∙
( ap
( mul-Group G'
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( f)
( pair
( ev-formal-combination-subset-Group G S (unit-list (s , x)))
( unit-trunc-Prop (unit-list (s , x) , refl)))))
( distributivity-hom-group-ev-formal-combination f l))

map-restriction-generating-subset-Subgroup :
hom-Group (group-Subgroup G (subgroup-subset-Group G S)) G' →
type-subtype S → type-Group G'
map-restriction-generating-subset-Subgroup f x =
map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( f)
( pair
( ev-formal-combination-subset-Group
( G)
( S)
( unit-list (inr star , x)))
( unit-trunc-Prop
( unit-list (inr star , x) , refl)))

is-emb-map-restriction-generating-subset-Subgroup :
is-emb (map-restriction-generating-subset-Subgroup)
is-emb-map-restriction-generating-subset-Subgroup f g =
is-equiv-is-invertible
( λ P →
eq-htpy-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( λ x →
apply-universal-property-trunc-Prop
( pr2 x)
( Id-Prop
( set-Group G')
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( f)
( x))
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( g)
( x)))
( λ (y , Q) →
( ap
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( f))
( eq-pair-Σ (inv Q) (eq-is-prop is-prop-type-trunc-Prop))) ∙
( distributivity-hom-group-ev-formal-combination f y) ∙
( ap
( λ F →
fold-list (unit-Group G') (λ Y → mul-Group G' (F Y)) y)
( eq-htpy (lemma (htpy-eq P)))) ∙
( inv
( distributivity-hom-group-ev-formal-combination g y)) ∙
( ap
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( g))
( eq-pair-Σ
( Q)
( eq-is-prop is-prop-type-trunc-Prop))))))
( λ p →
eq-is-prop
( is-trunc-Π
( zero-𝕋)
( λ z → is-set-type-Group G')
( λ S → map-restriction-generating-subset-Subgroup f S)
( λ S → map-restriction-generating-subset-Subgroup g S)))
( λ p →
eq-is-prop
( is-set-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( f)
( g)))
where
lemma :
( (x : type-subtype S) →
Id
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( f)
( pair
( ev-formal-combination-subset-Group
( G)
( S)
( unit-list (inr star , x)))
( unit-trunc-Prop (unit-list (pair (inr star) x) , refl))))
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( g)
( pair
( ev-formal-combination-subset-Group
( G)
( S)
( unit-list (inr star , x)))
( unit-trunc-Prop
( unit-list (pair (inr star) x) , refl))))) →
( z : Fin 2 × type-subtype S) →
Id
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( f)
( pair
( ev-formal-combination-subset-Group G S (unit-list z))
( unit-trunc-Prop (unit-list z , refl))))
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( g)
( pair
( ev-formal-combination-subset-Group G S (unit-list z))
( unit-trunc-Prop (unit-list z , refl))))
lemma P (inl (inr star) , x , s) =
( ap
( map-hom-Group (group-Subgroup G (subgroup-subset-Group G S)) G' f)
( eq-pair-Σ
( right-unit-law-mul-Group G (inv-Group G x))
( eq-is-prop is-prop-type-trunc-Prop))) ∙
( preserves-inv-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( f)) ∙
( ap
( inv-Group G')
( ( ap
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( f))
( eq-pair-Σ
{ s =
pair
( x)
( unit-trunc-Prop
( pair
( unit-list (inr star , x , s))
( right-unit-law-mul-Group G x)))}
( inv (right-unit-law-mul-Group G x))
( eq-is-prop is-prop-type-trunc-Prop))) ∙
( ( P (x , s)) ∙
( ap
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( g))
( eq-pair-Σ
{ s =
pair
( mul-Group G x (unit-Group G))
( unit-trunc-Prop
( pair
( unit-list (inr star , x , s))
( refl)))}
{ t =
pair
( x)
( unit-trunc-Prop
( pair
( unit-list (inr star , x , s))
( right-unit-law-mul-Group G x)))}
( right-unit-law-mul-Group G x)
( eq-is-prop is-prop-type-trunc-Prop)))))) ∙
( inv
( preserves-inv-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( g))) ∙
( ap
( map-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G')
( g))
( eq-pair-Σ
( inv (right-unit-law-mul-Group G (inv-Group G x)))
( eq-is-prop is-prop-type-trunc-Prop)))
lemma P (inr star , x) = P x

restriction-generating-subset-Subgroup :
hom-Group (group-Subgroup G (subgroup-subset-Group G S)) G' ↪
( type-subtype S → type-Group G')
pr1 restriction-generating-subset-Subgroup =
map-restriction-generating-subset-Subgroup
pr2 restriction-generating-subset-Subgroup =
is-emb-map-restriction-generating-subset-Subgroup

module _
{l1 l2 l3 : Level}
(G : Group l1) (S : subset-Group l2 G) (H : is-generating-set-Group G S)
(G' : Group l3)
where

restriction-generating-subset-Group :
hom-Group G G' ↪ (type-subtype S → type-Group G')
restriction-generating-subset-Group =
comp-emb
( restriction-generating-subset-Subgroup G S G')
( pair
( λ f →
comp-hom-Group
( group-Subgroup G (subgroup-subset-Group G S))
( G)
( G')
( f)
( pr1 , λ {x} {y} → refl))
( is-epi-iso-Group l3
( group-Subgroup G (subgroup-subset-Group G S))
( G)
( iso-inclusion-is-full-Subgroup G (subgroup-subset-Group G S) H)
( G')))

eq-map-restriction-generating-subset-Group :
( f : hom-Group G G') (x : type-subtype S) →
Id
( map-emb restriction-generating-subset-Group f x)
( map-hom-Group G G' f (pr1 x))
eq-map-restriction-generating-subset-Group f x =
ap
( map-hom-Group G G' f)
( right-unit-law-mul-Group G (pr1 x))