Homomorphisms of generated subgroups

module group-theory.homomorphisms-generated-subgroups where
Imports 
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.groups
open import group-theory.homomorphisms-groups
open import group-theory.subgroups
open import group-theory.subgroups-generated-by-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.

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

  distributivity-hom-group-ev-formal-combination :
    ( f : type-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)
        ( pair
          ( ev-formal-combination-subset-Group G S l)
          ( unit-trunc-Prop (pair l refl))))
      ( fold-list
        ( unit-Group G')
        ( λ (pair s x) →
          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 (pair s x)))
                ( unit-trunc-Prop (pair (unit-list (pair 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 (pair 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 (pair 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)
        ( pair
          ( ev-formal-combination-subset-Group G S (unit-list (pair s x)))
          ( unit-trunc-Prop (pair (unit-list (pair s x)) refl)))
        ( pair
          ( ev-formal-combination-subset-Group G S l)
          ( unit-trunc-Prop (pair l refl))) ∙
        ( 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 (pair s x)))
                ( unit-trunc-Prop (pair (unit-list (pair s x)) refl)))))
          ( distributivity-hom-group-ev-formal-combination f l)))

  map-restriction-generating-subset-Subgroup :
    type-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 (pair (inr star) x)))
        ( unit-trunc-Prop
          ( pair (unit-list (pair (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-has-inverse
      ( λ 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)))
              ( λ (pair 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)
                      { x =
                        λ z →
                          ( 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 (pair (unit-list z) refl))))}
                      { y =
                        λ z →
                          ( 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 (pair (unit-list z) refl))))}
                      ( 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-type-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 (pair (inr star) x)))
              ( unit-trunc-Prop (pair (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 (pair (inr star) x)))
              ( unit-trunc-Prop
                ( pair (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 (pair (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 (pair (unit-list z) refl))))
    lemma P (pair (inl (inr star)) (pair 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)
          ( pair
            ( x)
            ( unit-trunc-Prop
              ( pair
                ( unit-list (pair (inr star) (pair x s)))
                ( right-unit-law-mul-Group G x)))) ∙
          ( (ap
            ( inv-Group G')
            ( ( ap
              ( map-hom-Group
                ( group-Subgroup G (subgroup-subset-Group G S))
                ( G')
                ( f))
              ( eq-pair-Σ
                ( inv (right-unit-law-mul-Group G x))
                ( eq-is-prop is-prop-type-trunc-Prop))) ∙
              ( ( P (pair x s)) ∙
                ( ap
                  ( map-hom-Group
                    ( group-Subgroup G (subgroup-subset-Group G S))
                    ( G')
                    ( g))
                  ( eq-pair-Σ
                    ( 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)
                ( pair
                  ( x)
                  ( unit-trunc-Prop
                    ( pair
                      ( unit-list (pair (inr star) (pair x s)))
                      ( right-unit-law-mul-Group G x)))))) ∙
                ( 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 (pair (inr star) x) = P x

  restriction-generating-subset-Subgroup :
    type-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-subset-Group G S)
  (G' : Group l3)
  where

  restriction-generating-subset-Group :
    type-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)
            ( pair 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 : type-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))