# Quotient groups

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Daniel Gratzer, Elisabeth Stenholm, Julian KG, Maša Žaucer, fernabnor, Gregor Perčič and louismntnu.

Created on 2023-02-02.

module group-theory.quotient-groups where

Imports
open import foundation.action-on-identifications-functions
open import foundation.binary-functoriality-set-quotients
open import foundation.commuting-triangles-of-maps
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.effective-maps-equivalence-relations
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-set-quotients
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.reflecting-maps-equivalence-relations
open import foundation.set-quotients
open import foundation.sets
open import foundation.subtypes
open import foundation.surjective-maps
open import foundation.universal-property-set-quotients
open import foundation.universe-levels

open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.kernels-homomorphisms-groups
open import group-theory.normal-subgroups
open import group-theory.nullifying-group-homomorphisms
open import group-theory.semigroups


## Idea

Given a normal subgroup N of G, the quotient group G/N is a group equipped with a group homomorphism q : G → G/N such that N ⊆ ker q, and such that q satisfies the universal property of the quotient group, which asserts that any group homomorphism f : G → H such that N ⊆ ker f extends uniquely along q to a group homomorphism G/N → H. In other words, the universal property of the quotient group G/N asserts that the map

  hom-Group G/N H → nullifying-hom-Group G H N


from group homomorphisms G/N → H to N-nullifying group homomorphism G → H is an equivalence. Recall that a group homomorphism is said to be N-nullifying if N is contained in the kernel of f.

## Definitions

### The universal property of quotient groups

precomp-nullifying-hom-Group :
{l1 l2 l3 l4 : Level} (G : Group l1) (N : Normal-Subgroup l2 G)
(H : Group l3) (f : nullifying-hom-Group G H N)
(K : Group l4) → hom-Group H K → nullifying-hom-Group G K N
pr1 (precomp-nullifying-hom-Group G N H f K g) =
comp-hom-Group G H K g (hom-nullifying-hom-Group G H N f)
pr2 (precomp-nullifying-hom-Group G N H f K g) h p =
( inv (preserves-unit-hom-Group H K g)) ∙
( ap
( map-hom-Group H K g)
( nullifies-normal-subgroup-nullifying-hom-Group G H N f h p))

universal-property-quotient-Group :
{l1 l2 l3 : Level} (G : Group l1)
(N : Normal-Subgroup l2 G) (Q : Group l3)
(q : nullifying-hom-Group G Q N) → UUω
universal-property-quotient-Group G N Q q =
{l : Level} (H : Group l) → is-equiv (precomp-nullifying-hom-Group G N Q q H)


### The quotient group

#### The quotient map and the underlying set of the quotient group

The underlying set of the quotient group is defined as the set quotient of the equivalence relation induced by the normal subgroup N of G. By this construction we immediately obtain the quotient map q : G → G/N, which will be surjective and effective. This means that the quotient group satisfies the condition

  x⁻¹y ∈ N ↔ q x ＝ q y.


We will conclude later that this implies that the quotient map nullifies the normal subgroup N.

module _
{l1 l2 : Level} (G : Group l1) (N : Normal-Subgroup l2 G)
where

set-quotient-Group : Set (l1 ⊔ l2)
set-quotient-Group =
quotient-Set (equivalence-relation-congruence-Normal-Subgroup G N)

type-quotient-Group : UU (l1 ⊔ l2)
type-quotient-Group =
set-quotient (equivalence-relation-congruence-Normal-Subgroup G N)

is-set-type-quotient-Group : is-set type-quotient-Group
is-set-type-quotient-Group =
is-set-set-quotient (equivalence-relation-congruence-Normal-Subgroup G N)

map-quotient-hom-Group : type-Group G → type-quotient-Group
map-quotient-hom-Group =
quotient-map (equivalence-relation-congruence-Normal-Subgroup G N)

is-surjective-map-quotient-hom-Group :
is-surjective map-quotient-hom-Group
is-surjective-map-quotient-hom-Group =
is-surjective-quotient-map
( equivalence-relation-congruence-Normal-Subgroup G N)

is-effective-map-quotient-hom-Group :
is-effective
( equivalence-relation-congruence-Normal-Subgroup G N)
( map-quotient-hom-Group)
is-effective-map-quotient-hom-Group =
is-effective-quotient-map
( equivalence-relation-congruence-Normal-Subgroup G N)

abstract
apply-effectiveness-map-quotient-hom-Group :
{x y : type-Group G} →
map-quotient-hom-Group x ＝ map-quotient-hom-Group y →
sim-congruence-Normal-Subgroup G N x y
apply-effectiveness-map-quotient-hom-Group =
apply-effectiveness-quotient-map
( equivalence-relation-congruence-Normal-Subgroup G N)

abstract
apply-effectiveness-map-quotient-hom-Group' :
{x y : type-Group G} →
sim-congruence-Normal-Subgroup G N x y →
map-quotient-hom-Group x ＝ map-quotient-hom-Group y
apply-effectiveness-map-quotient-hom-Group' =
apply-effectiveness-quotient-map'
( equivalence-relation-congruence-Normal-Subgroup G N)

reflecting-map-quotient-hom-Group :
reflecting-map-equivalence-relation
( equivalence-relation-congruence-Normal-Subgroup G N)
( type-quotient-Group)
reflecting-map-quotient-hom-Group =
reflecting-map-quotient-map
( equivalence-relation-congruence-Normal-Subgroup G N)

is-set-quotient-set-quotient-Group :
is-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( set-quotient-Group)
( reflecting-map-quotient-hom-Group)
is-set-quotient-set-quotient-Group =
is-set-quotient-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)


#### The group structure on the quotient group

We now introduce the group structure on the underlying set of the quotient group. The multiplication, unit, and inverses are defined by the universal property of the set quotient as the unique maps equipped with identifications

  (qx)(qy) ＝ q(xy)
1 ＝ q1
(qx)⁻¹ ＝ q(x⁻¹)


The group laws follow by the induction principle for set quotients.

module _
{l1 l2 : Level} (G : Group l1) (N : Normal-Subgroup l2 G)
where

unit-quotient-Group : type-quotient-Group G N
unit-quotient-Group = map-quotient-hom-Group G N (unit-Group G)

binary-hom-mul-quotient-Group :
binary-hom-equivalence-relation
( equivalence-relation-congruence-Normal-Subgroup G N)
( equivalence-relation-congruence-Normal-Subgroup G N)
( equivalence-relation-congruence-Normal-Subgroup G N)
pr1 binary-hom-mul-quotient-Group = mul-Group G
pr2 binary-hom-mul-quotient-Group =
mul-congruence-Normal-Subgroup G N

mul-quotient-Group :
(x y : type-quotient-Group G N) → type-quotient-Group G N
mul-quotient-Group =
binary-map-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( equivalence-relation-congruence-Normal-Subgroup G N)
( equivalence-relation-congruence-Normal-Subgroup G N)
( binary-hom-mul-quotient-Group)

mul-quotient-Group' :
(x y : type-quotient-Group G N) → type-quotient-Group G N
mul-quotient-Group' x y = mul-quotient-Group y x

abstract
compute-mul-quotient-Group :
(x y : type-Group G) →
mul-quotient-Group
( map-quotient-hom-Group G N x)
( map-quotient-hom-Group G N y) ＝
map-quotient-hom-Group G N (mul-Group G x y)
compute-mul-quotient-Group =
compute-binary-map-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( equivalence-relation-congruence-Normal-Subgroup G N)
( equivalence-relation-congruence-Normal-Subgroup G N)
( binary-hom-mul-quotient-Group)

hom-inv-quotient-Group :
hom-equivalence-relation
( equivalence-relation-congruence-Normal-Subgroup G N)
( equivalence-relation-congruence-Normal-Subgroup G N)
pr1 hom-inv-quotient-Group = inv-Group G
pr2 hom-inv-quotient-Group = inv-congruence-Normal-Subgroup G N

inv-quotient-Group : type-quotient-Group G N → type-quotient-Group G N
inv-quotient-Group =
map-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( equivalence-relation-congruence-Normal-Subgroup G N)
( hom-inv-quotient-Group)

abstract
compute-inv-quotient-Group :
(x : type-Group G) →
inv-quotient-Group (map-quotient-hom-Group G N x) ＝
map-quotient-hom-Group G N (inv-Group G x)
compute-inv-quotient-Group =
coherence-square-map-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( equivalence-relation-congruence-Normal-Subgroup G N)
( hom-inv-quotient-Group)

abstract
left-unit-law-mul-quotient-Group :
(x : type-quotient-Group G N) →
mul-quotient-Group unit-quotient-Group x ＝ x
left-unit-law-mul-quotient-Group =
induction-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( λ y →
Id-Prop
( set-quotient-Group G N)
( mul-quotient-Group unit-quotient-Group y)
( y))
( λ x →
( compute-mul-quotient-Group (unit-Group G) x) ∙
( ap (map-quotient-hom-Group G N) (left-unit-law-mul-Group G x)))

abstract
right-unit-law-mul-quotient-Group :
(x : type-quotient-Group G N) →
mul-quotient-Group x unit-quotient-Group ＝ x
right-unit-law-mul-quotient-Group =
induction-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( λ y →
Id-Prop
( set-quotient-Group G N)
( mul-quotient-Group y unit-quotient-Group)
( y))
( λ x →
( compute-mul-quotient-Group x (unit-Group G)) ∙
( ap (map-quotient-hom-Group G N) (right-unit-law-mul-Group G x)))

abstract
associative-mul-quotient-Group :
(x y z : type-quotient-Group G N) →
( mul-quotient-Group (mul-quotient-Group x y) z) ＝
( mul-quotient-Group x (mul-quotient-Group y z))
associative-mul-quotient-Group =
triple-induction-set-quotient'
( equivalence-relation-congruence-Normal-Subgroup G N)
( λ x y z →
Id-Prop
( set-quotient-Group G N)
( mul-quotient-Group (mul-quotient-Group x y) z)
( mul-quotient-Group x (mul-quotient-Group y z)))
( λ x y z →
( ap
( mul-quotient-Group' (map-quotient-hom-Group G N z))
( compute-mul-quotient-Group x y)) ∙
( compute-mul-quotient-Group (mul-Group G x y) z) ∙
( ap
( map-quotient-hom-Group G N)
( associative-mul-Group G x y z)) ∙
( inv (compute-mul-quotient-Group x (mul-Group G y z))) ∙
( ap
( mul-quotient-Group (map-quotient-hom-Group G N x))
( inv (compute-mul-quotient-Group y z))))

abstract
left-inverse-law-mul-quotient-Group :
(x : type-quotient-Group G N) →
( mul-quotient-Group (inv-quotient-Group x) x) ＝
( unit-quotient-Group)
left-inverse-law-mul-quotient-Group =
induction-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( λ y →
Id-Prop
( set-quotient-Group G N)
( mul-quotient-Group (inv-quotient-Group y) y)
( unit-quotient-Group))
( λ x →
( ap
( mul-quotient-Group' (map-quotient-hom-Group G N x))
( compute-inv-quotient-Group x)) ∙
( compute-mul-quotient-Group (inv-Group G x) x) ∙
( ap
( map-quotient-hom-Group G N)
( left-inverse-law-mul-Group G x)))

abstract
right-inverse-law-mul-quotient-Group :
(x : type-quotient-Group G N) →
( mul-quotient-Group x (inv-quotient-Group x)) ＝
( unit-quotient-Group)
right-inverse-law-mul-quotient-Group =
induction-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( λ y →
Id-Prop
( set-quotient-Group G N)
( mul-quotient-Group y (inv-quotient-Group y))
( unit-quotient-Group))
( λ x →
( ap
( mul-quotient-Group (map-quotient-hom-Group G N x))
( compute-inv-quotient-Group x)) ∙
( compute-mul-quotient-Group x (inv-Group G x)) ∙
( ap
( map-quotient-hom-Group G N)
( right-inverse-law-mul-Group G x)))

semigroup-quotient-Group : Semigroup (l1 ⊔ l2)
pr1 semigroup-quotient-Group = set-quotient-Group G N
pr1 (pr2 semigroup-quotient-Group) = mul-quotient-Group
pr2 (pr2 semigroup-quotient-Group) = associative-mul-quotient-Group

quotient-Group : Group (l1 ⊔ l2)
pr1 quotient-Group = semigroup-quotient-Group
pr1 (pr1 (pr2 quotient-Group)) = unit-quotient-Group
pr1 (pr2 (pr1 (pr2 quotient-Group))) = left-unit-law-mul-quotient-Group
pr2 (pr2 (pr1 (pr2 quotient-Group))) = right-unit-law-mul-quotient-Group
pr1 (pr2 (pr2 quotient-Group)) = inv-quotient-Group
pr1 (pr2 (pr2 (pr2 quotient-Group))) = left-inverse-law-mul-quotient-Group
pr2 (pr2 (pr2 (pr2 quotient-Group))) = right-inverse-law-mul-quotient-Group


#### The quotient homomorphism into the quotient group

The quotient map q : G → G/N preserves the group structure and nullifies the normal subgroup N. Both these claims follow fairly directly from the definitions of the quotient map q and the group operations on G/N.

module _
{l1 l2 : Level} (G : Group l1) (N : Normal-Subgroup l2 G)
where

abstract
preserves-mul-quotient-hom-Group :
preserves-mul-Group G
( quotient-Group G N)
( map-quotient-hom-Group G N)
preserves-mul-quotient-hom-Group =
inv (compute-mul-quotient-Group G N _ _)

preserves-unit-quotient-hom-Group :
map-quotient-hom-Group G N (unit-Group G) ＝ unit-quotient-Group G N
preserves-unit-quotient-hom-Group = refl

abstract
preserves-inv-quotient-hom-Group :
(x : type-Group G) →
map-quotient-hom-Group G N (inv-Group G x) ＝
inv-quotient-Group G N (map-quotient-hom-Group G N x)
preserves-inv-quotient-hom-Group x =
inv (compute-inv-quotient-Group G N x)

quotient-hom-Group : hom-Group G (quotient-Group G N)
pr1 quotient-hom-Group = map-quotient-hom-Group G N
pr2 quotient-hom-Group = preserves-mul-quotient-hom-Group

nullifies-normal-subgroup-quotient-hom-Group :
nullifies-normal-subgroup-hom-Group G
( quotient-Group G N)
( quotient-hom-Group)
( N)
nullifies-normal-subgroup-quotient-hom-Group x n =
inv
( apply-effectiveness-map-quotient-hom-Group' G N
( unit-congruence-Normal-Subgroup' G N n))

nullifying-quotient-hom-Group : nullifying-hom-Group G (quotient-Group G N) N
pr1 nullifying-quotient-hom-Group = quotient-hom-Group
pr2 nullifying-quotient-hom-Group =
nullifies-normal-subgroup-quotient-hom-Group


#### Induction on quotient groups

The induction principle of quotient groups asserts that for any property P of elements of the quotient group G/N, in order to show that P x holds for all x : G/N it suffices to show that P qy holds for all y : G.

module _
{l1 l2 l3 : Level} (G : Group l1) (N : Normal-Subgroup l2 G)
(P : type-quotient-Group G N → Prop l3)
where

equiv-induction-quotient-Group :
((x : type-quotient-Group G N) → type-Prop (P x)) ≃
((x : type-Group G) → type-Prop (P (map-quotient-hom-Group G N x)))
equiv-induction-quotient-Group =
equiv-induction-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( P)

abstract
induction-quotient-Group :
((x : type-Group G) → type-Prop (P (map-quotient-hom-Group G N x))) →
((x : type-quotient-Group G N) → type-Prop (P x))
induction-quotient-Group =
induction-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( P)


#### Double induction on quotient groups

The double induction principle of quotient groups asserts that for any property P of pairs of elements of the quotient group G/N, in order to show that P x y holds for all x y : G/N it suffices to show that P qu qv holds for all u v : G.

module _
{l1 l2 l3 l4 l5 : Level}
(G : Group l1) (H : Group l2)
(N : Normal-Subgroup l3 G) (M : Normal-Subgroup l4 H)
(P : type-quotient-Group G N → type-quotient-Group H M → Prop l5)
where

equiv-double-induction-quotient-Group :
( (x : type-quotient-Group G N) (y : type-quotient-Group H M) →
type-Prop (P x y)) ≃
( (x : type-Group G) (y : type-Group H) →
type-Prop
( P (map-quotient-hom-Group G N x) (map-quotient-hom-Group H M y)))
equiv-double-induction-quotient-Group =
equiv-double-induction-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( equivalence-relation-congruence-Normal-Subgroup H M)
( P)

abstract
double-induction-quotient-Group :
( (x : type-Group G) (y : type-Group H) →
type-Prop
( P (map-quotient-hom-Group G N x) (map-quotient-hom-Group H M y))) →
( (x : type-quotient-Group G N) (y : type-quotient-Group H M) →
type-Prop (P x y))
double-induction-quotient-Group =
double-induction-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( equivalence-relation-congruence-Normal-Subgroup H M)
( P)


#### The universal property of the quotient group

The universal property of the quotient group G/N asserts that for any group H the precomposition function

  hom-Group G/N H → nullifying-hom-Group G H N


is an equivalence.

Proof: Let G and H be groups and let N be a normal subgroup of G. Our goal is to show that the precomposition function

  hom-Group G/N H → nullifying-hom-Group G H N


is an equivalence. To see this, note that the above map is a composite of the maps

  hom-Group G/N H → Σ (reflecting-map G H) (λ u → preserves-mul (pr1 u))
≃ Σ (hom-Group G H) (λ f → is-nullifying f)


The second map is the equivalence compute-nullifying-hom-Group constructed above. The first map is an equivalence by the universal property of set quotients, by which we have:

  (G/N → H) ≃ reflecting-map G H.

module _
{l1 l2 : Level} (G : Group l1) (N : Normal-Subgroup l2 G)
where

top-triangle-is-quotient-group-quotient-Group :
{l : Level} (H : Group l) →
hom-Group (quotient-Group G N) H →
Σ ( reflecting-map-equivalence-relation
( equivalence-relation-congruence-Normal-Subgroup G N)
( type-Group H))
( λ f → preserves-mul-Group G H (pr1 f))
top-triangle-is-quotient-group-quotient-Group H =
map-Σ
( λ f → preserves-mul-Group G H (pr1 f))
( precomp-Set-Quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( set-quotient-Group G N)
( reflecting-map-quotient-map
( equivalence-relation-congruence-Normal-Subgroup G N))
( set-Group H))
( λ f μ →
preserves-mul-comp-hom-Group G
( quotient-Group G N)
( H)
( f , μ)
( quotient-hom-Group G N))

triangle-is-quotient-group-quotient-Group :
{l : Level} (H : Group l) →
coherence-triangle-maps
( precomp-nullifying-hom-Group G N
( quotient-Group G N)
( nullifying-quotient-hom-Group G N)
( H))
( map-equiv (compute-nullifying-hom-Group G H N))
( top-triangle-is-quotient-group-quotient-Group H)
triangle-is-quotient-group-quotient-Group H x =
eq-type-subtype
( λ f → nullifies-normal-subgroup-prop-hom-Group G H f N)
( refl)

abstract
is-equiv-top-triangle-is-quotient-group-quotient-Group :
{l : Level} (H : Group l) →
is-equiv (top-triangle-is-quotient-group-quotient-Group H)
is-equiv-top-triangle-is-quotient-group-quotient-Group H =
is-equiv-map-Σ
( λ f → preserves-mul-Group G H (pr1 f))
( is-set-quotient-set-quotient
( equivalence-relation-congruence-Normal-Subgroup G N)
( set-Group H))
( λ f →
is-equiv-has-converse-is-prop
( is-prop-preserves-mul-Group (quotient-Group G N) H f)
( is-prop-preserves-mul-Group G H
( f ∘ map-quotient-hom-Group G N))
( λ μ {a} {b} →
double-induction-quotient-Group G G N N
( λ x y → Id-Prop (set-Group H) _ _)
( λ x y → ap f (compute-mul-quotient-Group G N x y) ∙ μ)
( a)
( b)))

abstract
is-quotient-group-quotient-Group :
universal-property-quotient-Group G N
( quotient-Group G N)
( nullifying-quotient-hom-Group G N)
is-quotient-group-quotient-Group H =
is-equiv-left-map-triangle
( precomp-nullifying-hom-Group G N
( quotient-Group G N)
( nullifying-quotient-hom-Group G N)
( H))
( map-equiv (compute-nullifying-hom-Group G H N))
( top-triangle-is-quotient-group-quotient-Group H)
( triangle-is-quotient-group-quotient-Group H)
( is-equiv-top-triangle-is-quotient-group-quotient-Group H)
( is-equiv-map-equiv (compute-nullifying-hom-Group G H N))


### The unique mapping property of the quotient group

The unique mapping property of the quotient group G/N asserts that for any group H and any N-nullifying group homomorphism f : G → H, the type of group homomorphisms g : G/N → H such that f ~ g ∘ q is contractible. In other words, it asserts that any nullifying group homomorphism f : G → H extends uniquely along q:

     G
| \
q |  \ f
|   \
∨    ∨
G/N -> H.
∃!

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

abstract
unique-mapping-property-quotient-Group :
(f : nullifying-hom-Group G H N) →
is-contr
( Σ ( hom-Group (quotient-Group G N) H)
( λ g →
htpy-hom-Group G H
( hom-nullifying-hom-Group G H N
( precomp-nullifying-hom-Group G N
( quotient-Group G N)
( nullifying-quotient-hom-Group G N)
( H)
( g)))
( hom-nullifying-hom-Group G H N f)))
unique-mapping-property-quotient-Group f =
is-contr-equiv' _
( equiv-tot
( λ g →
( extensionality-hom-Group G H _ _) ∘e
( extensionality-type-subtype'
( λ h → nullifies-normal-subgroup-prop-hom-Group G H h N)
( _)
( _))))
( is-contr-map-is-equiv
( is-quotient-group-quotient-Group G N H)
( f))

abstract
hom-universal-property-quotient-Group :
(f : hom-Group G H)
(n : nullifies-normal-subgroup-hom-Group G H f N) →
hom-Group (quotient-Group G N) H
hom-universal-property-quotient-Group f n =
pr1 (center (unique-mapping-property-quotient-Group (f , n)))

compute-hom-universal-property-quotient-Group :
(f : hom-Group G H)
(n : nullifies-normal-subgroup-hom-Group G H f N) →
htpy-hom-Group G H
( hom-nullifying-hom-Group G H N
( precomp-nullifying-hom-Group G N
( quotient-Group G N)
( nullifying-quotient-hom-Group G N)
( H)
( hom-universal-property-quotient-Group f n)))
( hom-nullifying-hom-Group G H N (f , n))
compute-hom-universal-property-quotient-Group f n =
pr2 (center (unique-mapping-property-quotient-Group (f , n)))


## Properties

### An element is in a normal subgroup N if and only if it is in the kernel of the quotient group homomorphism G → G/N

module _
{l1 l2 : Level} (G : Group l1) (N : Normal-Subgroup l2 G)
where

abstract
is-in-kernel-quotient-hom-is-in-Normal-Subgroup :
{x : type-Group G} → is-in-Normal-Subgroup G N x →
is-in-kernel-hom-Group G (quotient-Group G N) (quotient-hom-Group G N) x
is-in-kernel-quotient-hom-is-in-Normal-Subgroup =
nullifies-normal-subgroup-quotient-hom-Group G N _

abstract
is-in-normal-subgroup-is-in-kernel-quotient-hom-Group :
{x : type-Group G} →
is-in-kernel-hom-Group G (quotient-Group G N) (quotient-hom-Group G N) x →
is-in-Normal-Subgroup G N x
is-in-normal-subgroup-is-in-kernel-quotient-hom-Group {x} H =
unit-congruence-Normal-Subgroup G N
( apply-effectiveness-map-quotient-hom-Group G N (inv H))