Nullifying group homomorphisms

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-22.
Last modified on 2023-11-24.

module group-theory.nullifying-group-homomorphisms where
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.propositions
open import foundation.reflecting-maps-equivalence-relations
open import foundation.subtypes
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.homomorphisms-groups-equipped-with-normal-subgroups
open import group-theory.kernels-homomorphisms-groups
open import group-theory.normal-subgroups


Consider a group homomorphism f : G → H and a normal subgroup N of the group G. We say that f nullifies N if it satisfies the condition

  N ⊆ ker f,

i.e., if f x = 1 for all x ∈ N. Nullifying group homomorphisms are used to define quotient groups.


The predicate of nullifying a normal subgroup

module _
  {l1 l2 l3 : Level} (G : Group l1) (K : Group l2)

  nullifies-normal-subgroup-prop-hom-Group :
    hom-Group G K  Normal-Subgroup l3 G  Prop (l1  l2  l3)
  nullifies-normal-subgroup-prop-hom-Group f H =
    leq-prop-Normal-Subgroup G H (kernel-hom-Group G K f)

  nullifies-normal-subgroup-hom-Group :
    hom-Group G K  Normal-Subgroup l3 G  UU (l1  l2  l3)
  nullifies-normal-subgroup-hom-Group f H =
    type-Prop (nullifies-normal-subgroup-prop-hom-Group f H)

Group homomorphisms that nullify a normal subgroup, i.e., that contain a normal subgroup in their kernel

module _
  {l1 l2 l3 : Level} (G : Group l1) (K : Group l2) (H : Normal-Subgroup l3 G)

  nullifying-hom-Group : UU (l1  l2  l3)
  nullifying-hom-Group =
    type-subtype  f  nullifies-normal-subgroup-prop-hom-Group G K f H)

  hom-nullifying-hom-Group :
    nullifying-hom-Group  hom-Group G K
  hom-nullifying-hom-Group = pr1

  nullifies-normal-subgroup-nullifying-hom-Group :
    (f : nullifying-hom-Group) 
    nullifies-normal-subgroup-hom-Group G K
      ( hom-nullifying-hom-Group f) H
  nullifies-normal-subgroup-nullifying-hom-Group = pr2


A group homomorphism nullifies a normal subgroup if and only if it reflects the equivalence relation induced by the normal subgroup

module _
  {l1 l2 l3 : Level} (G : Group l1) (K : Group l2)
  (H : Normal-Subgroup l3 G)

  reflects-equivalence-relation-nullifies-normal-subgroup-hom-Group :
    (f : hom-Group G K) 
    nullifies-normal-subgroup-hom-Group G K f H 
      ( equivalence-relation-congruence-Normal-Subgroup G H)
      ( map-hom-Group G K f)
  reflects-equivalence-relation-nullifies-normal-subgroup-hom-Group f p α =
    ( inv (right-unit-law-mul-Group K _)) 
    ( inv-transpose-eq-mul-Group' K
      ( ( p (left-div-Group G _ _) α) 
        ( preserves-left-div-hom-Group G K f)))

  nullifies-normal-subgroup-reflects-equivalence-relation-hom-Group :
    (f : hom-Group G K) 
      ( equivalence-relation-congruence-Normal-Subgroup G H)
      ( map-hom-Group G K f) 
    nullifies-normal-subgroup-hom-Group G K f H
  nullifies-normal-subgroup-reflects-equivalence-relation-hom-Group f p x q =
    ( inv (preserves-unit-hom-Group G K f)) 
    ( p ( is-closed-under-multiplication-Normal-Subgroup G H
          ( is-closed-under-inverses-Normal-Subgroup G H
            ( contains-unit-Normal-Subgroup G H))
          ( q)))

  compute-nullifying-hom-Group :
    Σ ( reflecting-map-equivalence-relation
        ( equivalence-relation-congruence-Normal-Subgroup G H)
        ( type-Group K))
      ( λ f  preserves-mul-Group G K (pr1 f)) 
    nullifying-hom-Group G K H
  compute-nullifying-hom-Group =
    ( equiv-type-subtype
      ( λ f 
          ( equivalence-relation-congruence-Normal-Subgroup G H)
          ( set-Group K)
          ( pr1 f))
      ( λ f  is-prop-leq-Normal-Subgroup G H (kernel-hom-Group G K f))
      ( nullifies-normal-subgroup-reflects-equivalence-relation-hom-Group)
      ( reflects-equivalence-relation-nullifies-normal-subgroup-hom-Group)) ∘e
    ( equiv-right-swap-Σ)

Composition of nullifying homomorphisms and reflecting homomorphisms

module _
  {l1 l2 l3 l4 l5 : Level}
  (G : Group l1) (H : Group l2) (K : Group l3)
  (N : Normal-Subgroup l4 G) (M : Normal-Subgroup l5 H)

  hom-comp-nullifying-hom-reflecting-hom-Group :
    nullifying-hom-Group H K M 
    reflecting-hom-Group G H N M 
    hom-Group G K
  hom-comp-nullifying-hom-reflecting-hom-Group g f =
    comp-hom-Group G H K
      ( hom-nullifying-hom-Group H K M g)
      ( hom-reflecting-hom-Group G H N M f)

  nullifies-normal-subgroup-comp-nullifying-hom-reflecting-hom-Group :
    ( g : nullifying-hom-Group H K M)
    ( f : reflecting-hom-Group G H N M) 
    nullifies-normal-subgroup-hom-Group G K
      ( hom-comp-nullifying-hom-reflecting-hom-Group g f)
      ( N)
  nullifies-normal-subgroup-comp-nullifying-hom-reflecting-hom-Group g f x n =
    nullifies-normal-subgroup-nullifying-hom-Group H K M g
      ( map-reflecting-hom-Group G H N M f x)
      ( reflects-normal-subgroup-reflecting-hom-Group G H N M f x n)

  comp-nullifying-hom-reflecting-hom-Group :
    nullifying-hom-Group H K M 
    reflecting-hom-Group G H N M 
    nullifying-hom-Group G K N
  pr1 (comp-nullifying-hom-reflecting-hom-Group g f) =
    hom-comp-nullifying-hom-reflecting-hom-Group g f
  pr2 (comp-nullifying-hom-reflecting-hom-Group g f) =
    nullifies-normal-subgroup-comp-nullifying-hom-reflecting-hom-Group g f

See also

Recent changes