From 4db82b1afc142a6eadf089a86b52ef5d58e61684 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <smaug451@gmail.com>
Date: Fri, 8 Nov 2019 18:00:16 +0000
Subject: [PATCH] Tidy up groups more (#68)

---
 Everything/Safe.agda                    |   1 +
 Groups/Cyclic/Definition.agda           |  39 ++++
 Groups/Cyclic/Lemmas.agda               |  50 +++++
 Groups/CyclicGroups.agda                |  66 +------
 Groups/Examples/Examples.agda           | 245 +++++++++++++-----------
 Groups/Groups2.agda                     | 122 +-----------
 Groups/Homomorphisms/Image.agda         |  64 +++++++
 Groups/Homomorphisms/Lemmas.agda        |   4 +
 Groups/Subgroups/Normal/Definition.agda |  29 +++
 Groups/Subgroups/Normal/Lemmas.agda     |  82 ++++++++
 10 files changed, 418 insertions(+), 284 deletions(-)
 create mode 100644 Groups/Cyclic/Definition.agda
 create mode 100644 Groups/Cyclic/Lemmas.agda
 create mode 100644 Groups/Homomorphisms/Image.agda
 create mode 100644 Groups/Subgroups/Normal/Definition.agda
 create mode 100644 Groups/Subgroups/Normal/Lemmas.agda

diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index 25dbc7d..bdd02a3 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -26,6 +26,7 @@ open import Groups.SymmetricGroups.Definition
 open import Groups.Actions.Stabiliser
 open import Groups.Actions.Orbit
 open import Groups.SymmetricGroups.Lemmas
+open import Groups.Cyclic.Definition
 
 open import Fields.Fields
 open import Fields.Orders.Partial.Definition
diff --git a/Groups/Cyclic/Definition.agda b/Groups/Cyclic/Definition.agda
new file mode 100644
index 0000000..eb37bdc
--- /dev/null
+++ b/Groups/Cyclic/Definition.agda
@@ -0,0 +1,39 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Setoids.Setoids
+open import Sets.EquivalenceRelations
+open import Functions
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Numbers.Naturals.Naturals
+open import Numbers.Integers.Integers
+open import Numbers.Integers.Addition
+open import Sets.FinSet
+open import Groups.Homomorphisms.Definition
+open import Groups.Groups
+open import Groups.Subgroups.Definition
+open import Groups.Abelian.Definition
+open import Groups.Definition
+
+module Groups.Cyclic.Definition {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) where
+
+open Setoid S
+open Group G
+open Equivalence eq
+
+positiveEltPower : (x : A) (i : ℕ) → A
+positiveEltPower x 0 = Group.0G G
+positiveEltPower x (succ i) = x · (positiveEltPower x i)
+
+positiveEltPowerCollapse : (x : A) (i j : ℕ) → Setoid._∼_ S ((positiveEltPower x i) · (positiveEltPower x j)) (positiveEltPower x (i +N j))
+positiveEltPowerCollapse x zero j = Group.identLeft G
+positiveEltPowerCollapse x (succ i) j = transitive (symmetric +Associative) (+WellDefined reflexive (positiveEltPowerCollapse x i j))
+
+elementPower : (x : A) (i : ℤ) → A
+elementPower x (nonneg i) = positiveEltPower x i
+elementPower x (negSucc i) = Group.inverse G (positiveEltPower x (succ i))
+
+record CyclicGroup : Set (m ⊔ n) where
+  field
+    generator : A
+    cyclic : {a : A} → (Sg ℤ (λ i → Setoid._∼_ S (elementPower generator i) a))
diff --git a/Groups/Cyclic/Lemmas.agda b/Groups/Cyclic/Lemmas.agda
new file mode 100644
index 0000000..517731c
--- /dev/null
+++ b/Groups/Cyclic/Lemmas.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Setoids.Setoids
+open import Sets.EquivalenceRelations
+open import Functions
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Numbers.Naturals.Naturals
+open import Numbers.Integers.Integers
+open import Numbers.Integers.Addition
+open import Sets.FinSet
+open import Groups.Homomorphisms.Definition
+open import Groups.Groups
+open import Groups.Subgroups.Definition
+open import Groups.Abelian.Definition
+open import Groups.Definition
+open import Groups.Cyclic.Definition
+
+module Groups.Cyclic.Lemmas where
+
+elementPowerCollapse : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) (x : A) (i j : ℤ) → Setoid._∼_ S ((elementPower G x i) · (elementPower G x j)) (elementPower G x (i +Z j))
+elementPowerCollapse G x (nonneg a) (nonneg b) rewrite equalityCommutative (+Zinherits a b) = positiveEltPowerCollapse G x a b
+elementPowerCollapse G x (nonneg a) (negSucc b) = {!!}
+elementPowerCollapse G x (negSucc a) (nonneg b) = {!!}
+elementPowerCollapse G x (negSucc a) (negSucc b) = {!!}
+
+elementPowerHom : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) (x : A) → GroupHom ℤGroup G (λ i → elementPower G x i)
+GroupHom.groupHom (elementPowerHom {S = S} G x) {a} {b} = symmetric (elementPowerCollapse G x a b)
+  where
+    open Equivalence (Setoid.eq S)
+GroupHom.wellDefined (elementPowerHom {S = S} G x) {.y} {y} refl = reflexive
+  where
+    open Equivalence (Setoid.eq S)
+
+subgroupOfCyclicIsCyclic : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : B → A} {fHom : GroupHom H G f} → Subgroup G H fHom → CyclicGroup G → CyclicGroup H
+CyclicGroup.generator (subgroupOfCyclicIsCyclic {f = f} subgrp record { generator = generator ; cyclic = cyclic }) = {!f generator!}
+CyclicGroup.cyclic (subgroupOfCyclicIsCyclic subgrp gCyclic) = {!!}
+
+-- Prefer to prove that subgroup of cyclic is cyclic, then deduce this like with abelian groups
+{-
+cyclicIsGroupProperty : {m n o p : _} {A : Set m} {B : Set o} {S : Setoid {m} {n} A} {T : Setoid {o} {p} B} {_+_ : A → A → A} {_*_ : B → B → B} {G : Group S _+_} {H : Group T _*_} → GroupsIsomorphic G H → CyclicGroup G → CyclicGroup H
+CyclicGroup.generator (cyclicIsGroupProperty {H = H} iso G) = GroupsIsomorphic.isomorphism iso (CyclicGroup.generator G)
+CyclicGroup.cyclic (cyclicIsGroupProperty {H = H} iso G) {a} with GroupIso.surj (GroupsIsomorphic.proof iso) {a}
+CyclicGroup.cyclic (cyclicIsGroupProperty {H = H} iso G) {a} | a' , b with CyclicGroup.cyclic G {a'}
+... | pow , prPow = pow , {!!}
+-}
+
+-- Proof of abelianness of cyclic groups: a cyclic group is the image of elementPowerHom into Z, so is isomorphic to a subgroup of Z. All subgroups of an abelian group are abelian.
+cyclicGroupIsAbelian : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {G : Group S _+_} (cyclic : CyclicGroup G) → AbelianGroup G
+cyclicGroupIsAbelian cyclic = {!!}
diff --git a/Groups/CyclicGroups.agda b/Groups/CyclicGroups.agda
index b06fad1..7985065 100644
--- a/Groups/CyclicGroups.agda
+++ b/Groups/CyclicGroups.agda
@@ -1,67 +1,19 @@
-{-# OPTIONS --safe --warning=error #-}
+{-# OPTIONS --safe --warning=error --without-K #-}
 
 open import LogicalFormulae
 open import Setoids.Setoids
+open import Sets.EquivalenceRelations
 open import Functions
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-open import Numbers.Naturals
-open import Numbers.Integers
+open import Numbers.Naturals.Naturals
+open import Numbers.Integers.Integers
+open import Numbers.Integers.Addition
 open import Sets.FinSet
+open import Groups.Homomorphisms.Definition
 open import Groups.Groups
+open import Groups.Subgroups.Definition
+open import Groups.Abelian.Definition
 open import Groups.Definition
 
-module Groups.CyclicGroups where
+module Groups.CyclicGroups {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) where
 
-    positiveEltPower : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) (x : A) (i : ℕ) → A
-    positiveEltPower G x 0 = Group.identity G
-    positiveEltPower {_·_ = _·_} G x (succ i) = x · (positiveEltPower G x i)
-
-    positiveEltPowerCollapse : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} (G : Group S _+_) (x : A) (i j : ℕ) → Setoid._∼_ S ((positiveEltPower G x i) + (positiveEltPower G x j)) (positiveEltPower G x (i +N j))
-    positiveEltPowerCollapse G x zero j = Group.multIdentLeft G
-    positiveEltPowerCollapse {S = S} G x (succ i) j = transitive (symmetric multAssoc) (wellDefined reflexive (positiveEltPowerCollapse G x i j))
-      where
-        open Setoid S
-        open Group G
-        open Transitive (Equivalence.transitiveEq eq)
-        open Symmetric (Equivalence.symmetricEq eq)
-        open Reflexive (Equivalence.reflexiveEq eq)
-
-    elementPower : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) (x : A) (i : ℤ) → A
-    elementPower G x (nonneg i) = positiveEltPower G x i
-    elementPower {_·_ = _·_} G x (negSucc i) = Group.inverse G (positiveEltPower G x (succ i))
-
-    record CyclicGroup {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) : Set (m ⊔ n) where
-      field
-        generator : A
-        cyclic : {a : A} → (Sg ℤ (λ i → Setoid._∼_ S (elementPower G generator i) a))
-
-    elementPowerCollapse : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) (x : A) (i j : ℤ) → Setoid._∼_ S ((elementPower G x i) · (elementPower G x j)) (elementPower G x (i +Z j))
-    elementPowerCollapse {S = S} {_+_} G x (nonneg a) (nonneg b) rewrite addingNonnegIsHom a b = positiveEltPowerCollapse G x a b
-    elementPowerCollapse G x (nonneg a) (negSucc b) = {!!}
-    elementPowerCollapse G x (negSucc a) (nonneg b) = {!!}
-    elementPowerCollapse G x (negSucc a) (negSucc b) = {!!}
-
-    elementPowerHom : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) (x : A) → GroupHom ℤGroup G (λ i → elementPower G x i)
-    GroupHom.groupHom (elementPowerHom {S = S} G x) {a} {b} = symmetric (elementPowerCollapse G x a b)
-      where
-        open Setoid S
-        open Group G
-        open Symmetric (Equivalence.symmetricEq eq)
-    GroupHom.wellDefined (elementPowerHom {S = S} G x) {.y} {y} refl = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
-
-    subgroupOfCyclicIsCyclic : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : B → A} {fHom : GroupHom H G f} → Subgroup G H fHom → CyclicGroup G → CyclicGroup H
-    CyclicGroup.generator (subgroupOfCyclicIsCyclic {f = f} subgrp record { generator = generator ; cyclic = cyclic }) = {!f generator!}
-    CyclicGroup.cyclic (subgroupOfCyclicIsCyclic subgrp gCyclic) = {!!}
-
--- Prefer to prove that subgroup of cyclic is cyclic, then deduce this like with abelian groups
-{-
-    cyclicIsGroupProperty : {m n o p : _} {A : Set m} {B : Set o} {S : Setoid {m} {n} A} {T : Setoid {o} {p} B} {_+_ : A → A → A} {_*_ : B → B → B} {G : Group S _+_} {H : Group T _*_} → GroupsIsomorphic G H → CyclicGroup G → CyclicGroup H
-    CyclicGroup.generator (cyclicIsGroupProperty {H = H} iso G) = GroupsIsomorphic.isomorphism iso (CyclicGroup.generator G)
-    CyclicGroup.cyclic (cyclicIsGroupProperty {H = H} iso G) {a} with GroupIso.surj (GroupsIsomorphic.proof iso) {a}
-    CyclicGroup.cyclic (cyclicIsGroupProperty {H = H} iso G) {a} | a' , b with CyclicGroup.cyclic G {a'}
-    ... | pow , prPow = pow , {!!}
-    -}
-
--- Proof of abelianness of cyclic groups: a cyclic group is the image of elementPowerHom into Z, so is isomorphic to a subgroup of Z. All subgroups of an abelian group are abelian.
-    cyclicGroupIsAbelian : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {G : Group S _+_} (cyclic : CyclicGroup G) → AbelianGroup G
-    cyclicGroupIsAbelian cyclic = {!!}
diff --git a/Groups/Examples/Examples.agda b/Groups/Examples/Examples.agda
index 8c9634a..4e2b32d 100644
--- a/Groups/Examples/Examples.agda
+++ b/Groups/Examples/Examples.agda
@@ -1,128 +1,157 @@
-{-# OPTIONS --safe --warning=error #-}
+{-# OPTIONS --safe --warning=error --with-K #-}
 
+open import Sets.EquivalenceRelations
 open import Groups.Definition
 open import Orders
-open import Numbers.Integers
+open import Rings.Definition
+open import Numbers.Integers.Integers
+open import Numbers.Integers.Multiplication
 open import Setoids.Setoids
 open import LogicalFormulae
 open import Sets.FinSet
 open import Functions
-open import Numbers.Naturals
-open import IntegersModN
+open import Numbers.Naturals.Naturals
+open import Numbers.Naturals.WithK
+open import Numbers.Modulo.Definition
+open import Numbers.Modulo.Addition
+open import Numbers.Modulo.Group
 open import Rings.Examples.Examples
-open import PrimeNumbers
-open import Groups.Groups2
-open import Groups.CyclicGroups
+open import Numbers.Primes.PrimeNumbers
+open import Groups.Lemmas
+open import Groups.Homomorphisms.Definition
+open import Groups.Homomorphisms.Lemmas
+open import Groups.Isomorphisms.Definition
+open import Groups.Cyclic.Definition
+open import Groups.QuotientGroup.Definition
+open import Groups.Subgroups.Definition
+open import Groups.Subgroups.Normal.Definition
 
 module Groups.Examples.Examples where
-  elementPowZ : (n : ℕ) → (elementPower ℤGroup (nonneg 1) n) ≡ nonneg n
-  elementPowZ zero = refl
-  elementPowZ (succ n) rewrite elementPowZ n = refl
 
-  ℤCyclic : CyclicGroup ℤGroup
-  CyclicGroup.generator ℤCyclic = nonneg 1
-  CyclicGroup.cyclic ℤCyclic {nonneg x} = inl (x , elementPowZ x)
-  CyclicGroup.cyclic ℤCyclic {negSucc x} = inr (succ x , ans)
-    where
-      ans : additiveInverseZ (nonneg 1 +Z elementPower ℤGroup (nonneg 1) x) ≡ negSucc x
-      ans rewrite elementPowZ x = refl
+trivialGroup : Group (reflSetoid (FinSet 1)) λ _ _ → fzero
+Group.+WellDefined trivialGroup _ _ = refl
+Group.0G trivialGroup = fzero
+Group.inverse trivialGroup _ = fzero
+Group.+Associative trivialGroup = refl
+Group.identRight trivialGroup {fzero} = refl
+Group.identRight trivialGroup {fsucc ()}
+Group.identLeft trivialGroup {fzero} = refl
+Group.identLeft trivialGroup {fsucc ()}
+Group.invLeft trivialGroup = refl
+Group.invRight trivialGroup = refl
 
-  elementPowZn : (n : ℕ) → {pr : 0 <N succ (succ n)} → (power : ℕ) → (powerLess : power <N succ (succ n)) → {p : 1 <N succ (succ n)} → elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) power ≡ record { x = power ; xLess = powerLess }
-  elementPowZn n zero powerLess = equalityZn _ _ refl
-  elementPowZn n {pr} (succ power) powerLess {p} with orderIsTotal (ℤn.x (elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) power)) (succ n)
-  elementPowZn n {pr} (succ power) powerLess {p} | inl (inl x) = equalityZn _ _ (applyEquality succ v)
-    where
-      t : elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = succPreservesInequality (succIsPositive n) }) power ≡ record { x = power ; xLess = PartialOrder.transitive (TotalOrder.order ℕTotalOrder) (a<SuccA power) powerLess }
-      t = elementPowZn n {pr} power (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) (a<SuccA power) powerLess) {succPreservesInequality (succIsPositive n)}
-      u : elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) power ≡ record { x = power ; xLess = PartialOrder.transitive (TotalOrder.order ℕTotalOrder) (a<SuccA power) powerLess }
-      u rewrite <NRefl p (succPreservesInequality (succIsPositive n)) = t
-      v : ℤn.x (elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) power) ≡ power
-      v rewrite u = refl
-  elementPowZn n {pr} (succ power) powerLess {p} | inl (inr x) with elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) power
-  elementPowZn n {pr} (succ power) powerLess {p} | inl (inr x) | record { x = x' ; xLess = xLess } = exFalso (noIntegersBetweenXAndSuccX _ x xLess)
-  elementPowZn n {pr} (succ power) powerLess {p} | inr x with inspect (elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) power)
-  elementPowZn n {pr} (succ power) powerLess {p} | inr x | record { x = x' ; xLess = p' } with≡ inspected rewrite elementPowZn n {pr} power (PartialOrder.transitive (TotalOrder.order ℕTotalOrder) (a<SuccA power) powerLess) {p} | x = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) powerLess)
+elementPowZ : (n : ℕ) → (elementPower ℤGroup (nonneg 1) (nonneg n)) ≡ nonneg n
+elementPowZ zero = refl
+elementPowZ (succ n) rewrite elementPowZ n = refl
 
-  ℤnCyclic : (n : ℕ) → (pr : 0 <N n) → CyclicGroup (ℤnGroup n pr)
-  ℤnCyclic zero ()
-  CyclicGroup.generator (ℤnCyclic (succ zero) pr) = record { x = 0 ; xLess = pr }
-  CyclicGroup.cyclic (ℤnCyclic (succ zero) pr) {record { x = zero ; xLess = xLess }} rewrite <NRefl xLess (succIsPositive 0) | <NRefl pr (succIsPositive 0) = inl (0 , refl)
-  CyclicGroup.cyclic (ℤnCyclic (succ zero) _) {record { x = succ x ; xLess = xLess }} = exFalso (zeroNeverGreater (canRemoveSuccFrom<N xLess))
-  ℤnCyclic (succ (succ n)) pr = record { generator = record { x = 1 ; xLess = succPreservesInequality (succIsPositive n) } ; cyclic = λ {x} → inl (ans x) }
-    where
-      ans : (z : ℤn (succ (succ n)) pr) → Sg ℕ (λ i → (elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = succPreservesInequality (succIsPositive n) }) i) ≡ z)
-      ans record { x = x ; xLess = xLess } = x , elementPowZn n x xLess
+ℤCyclic : CyclicGroup ℤGroup
+CyclicGroup.generator ℤCyclic = nonneg 1
+CyclicGroup.cyclic ℤCyclic {nonneg x} = (nonneg x , elementPowZ x)
+CyclicGroup.cyclic ℤCyclic {negSucc x} = (negSucc x , ans)
+  where
+    ans : (Group.inverse ℤGroup ((nonneg 1) +Z elementPower ℤGroup (nonneg 1) (nonneg x))) ≡ negSucc x
+    ans rewrite elementPowZ x = refl
 
-  multiplyByNHom : (n : ℕ) → GroupHom ℤGroup ℤGroup (λ i → i *Z nonneg n)
-  GroupHom.groupHom (multiplyByNHom n) {x} {y} = lemma1
-    where
-      open Setoid (reflSetoid ℤ)
-      open Group ℤGroup
-      lemma : nonneg n *Z (x +Z y) ≡ (nonneg n) *Z x +Z nonneg n *Z y
-      lemma = additionZDistributiveMulZ (nonneg n) x y
-      lemma1 : (x +Z y) *Z nonneg n ≡ x *Z nonneg n +Z y *Z nonneg n
-      lemma1 rewrite multiplicationZIsCommutative (x +Z y) (nonneg n) | multiplicationZIsCommutative x (nonneg n) | multiplicationZIsCommutative y (nonneg n) = lemma
-  GroupHom.wellDefined (multiplyByNHom n) {x} {.x} refl = refl
+elementPowZn : (n : ℕ) → {pr : 0 <N succ (succ n)} → (power : ℕ) → (powerLess : power <N succ (succ n)) → {p : 1 <N succ (succ n)} → elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) (nonneg power) ≡ record { x = power ; xLess = powerLess }
+elementPowZn n zero powerLess = equalityZn _ _ refl
+elementPowZn n {pr} (succ power) powerLess {p} with orderIsTotal (ℤn.x (elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) (nonneg power))) (succ n)
+elementPowZn n {pr} (succ power) powerLess {p} | inl (inl x) = equalityZn _ _ (applyEquality succ v)
+  where
+    t : elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = succPreservesInequality (succIsPositive n) }) (nonneg power) ≡ record { x = power ; xLess = PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (a<SuccA power) powerLess }
+    t = elementPowZn n {pr} power (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (a<SuccA power) powerLess) {succPreservesInequality (succIsPositive n)}
+    u : elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) (nonneg power) ≡ record { x = power ; xLess = PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (a<SuccA power) powerLess }
+    u rewrite <NRefl p (succPreservesInequality (succIsPositive n)) = t
+    v : ℤn.x (elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) (nonneg power)) ≡ power
+    v rewrite u = refl
+elementPowZn n {pr} (succ power) powerLess {p} | inl (inr x) with elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) (nonneg power)
+elementPowZn n {pr} (succ power) powerLess {p} | inl (inr x) | record { x = x' ; xLess = xLess } = exFalso (noIntegersBetweenXAndSuccX _ x xLess)
+elementPowZn n {pr} (succ power) powerLess {p} | inr x with inspect (elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) (nonneg power))
+elementPowZn n {pr} (succ power) powerLess {p} | inr x | record { x = x' ; xLess = p' } with≡ inspected rewrite elementPowZn n {pr} power (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (a<SuccA power) powerLess) {p} | x = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) powerLess)
 
-  modNExampleGroupHom : (n : ℕ) → (pr : 0 <N n) → GroupHom ℤGroup (ℤnGroup n pr) (mod n pr)
-  modNExampleGroupHom = {!!}
+ℤnCyclic : (n : ℕ) → (pr : 0 <N n) → CyclicGroup (ℤnGroup n pr)
+ℤnCyclic zero ()
+CyclicGroup.generator (ℤnCyclic (succ zero) pr) = record { x = 0 ; xLess = pr }
+CyclicGroup.cyclic (ℤnCyclic (succ zero) pr) {record { x = zero ; xLess = xLess }} rewrite <NRefl xLess (succIsPositive 0) | <NRefl pr (succIsPositive 0) = (nonneg 0 , refl)
+CyclicGroup.cyclic (ℤnCyclic (succ zero) _) {record { x = succ x ; xLess = xLess }} = exFalso (zeroNeverGreater (canRemoveSuccFrom<N xLess))
+ℤnCyclic (succ (succ n)) pr = record { generator = record { x = 1 ; xLess = succPreservesInequality (succIsPositive n) } ; cyclic = λ {x} → ans x }
+  where
+    ans : (z : ℤn (succ (succ n)) pr) → Sg ℤ (λ i → (elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = succPreservesInequality (succIsPositive n) }) i) ≡ z)
+    ans record { x = x ; xLess = xLess } = nonneg x , elementPowZn n x xLess
 
-  intoZn : {n : ℕ} → {pr : 0 <N n} → (x : ℕ) → (x<n : x <N n) → mod n pr (nonneg x) ≡ record { x = x ; xLess = x<n }
-  intoZn {zero} {()}
-  intoZn {succ n} {0<n} x x<n with divisionAlg (succ n) x
-  intoZn {succ n} {0<n} x x<n | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl y ; quotSmall = quotSmall } = equalityZn _ _ (modIsUnique (record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl y ; quotSmall = quotSmall }) (record { quot = 0 ; rem = x ; pr = ans ; remIsSmall = inl x<n ; quotSmall = inl (succIsPositive n)}))
-    where
-      ans : n *N 0 +N x ≡ x
-      ans rewrite multiplicationNIsCommutative n 0 = refl
-  intoZn {succ n} {0<n} x x<n | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inr () ; quotSmall = quotSmall }
+multiplyByNHom : (n : ℕ) → GroupHom ℤGroup ℤGroup (λ i → i *Z nonneg n)
+GroupHom.groupHom (multiplyByNHom n) {x} {y} = lemma1
+  where
+    open Setoid (reflSetoid ℤ)
+    open Group ℤGroup
+    lemma : nonneg n *Z (x +Z y) ≡ (nonneg n) *Z x +Z nonneg n *Z y
+    lemma = Ring.*DistributesOver+ ℤRing {nonneg n} {x} {y}
+    lemma1 : (x +Z y) *Z nonneg n ≡ x *Z nonneg n +Z y *Z nonneg n
+    lemma1 rewrite Ring.*Commutative ℤRing {x +Z y} {nonneg n} | Ring.*Commutative ℤRing {x} {nonneg n} | Ring.*Commutative ℤRing {y} {nonneg n} = lemma
+GroupHom.wellDefined (multiplyByNHom n) {x} {.x} refl = refl
 
-  quotientZn : (n : ℕ) → (pr : 0 <N n) → GroupIso (quotientGroup ℤGroup (modNExampleGroupHom n pr)) (ℤnGroup n pr) (mod n pr)
-  GroupHom.groupHom (GroupIso.groupHom (quotientZn n pr)) = GroupHom.groupHom (modNExampleGroupHom n pr)
-  GroupHom.wellDefined (GroupIso.groupHom (quotientZn n pr)) {x} {y} x~y = need
-    where
-      given : mod n pr (x +Z (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr }
-      given = x~y
-      given' : (mod n pr x) +n (mod n pr (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr }
-      given' = transitivity (equalityCommutative (GroupHom.groupHom (modNExampleGroupHom n pr))) given
-      given'' : (mod n pr x) +n Group.inverse (ℤnGroup n pr) (mod n pr y) ≡ record { x = 0 ; xLess = pr}
-      given'' = transitivity (applyEquality (λ i → mod n pr x +n i) (equalityCommutative (homRespectsInverse (modNExampleGroupHom n pr)))) given'
-      need : mod n pr x ≡ mod n pr y
-      need = transferToRight (ℤnGroup n pr) given''
-  GroupIso.inj (quotientZn n pr) {x} {y} fx~fy = need
-    where
-      given : mod n pr x +n Group.inverse (ℤnGroup n pr) (mod n pr y) ≡ record { x = 0 ; xLess = pr }
-      given = transferToRight'' (ℤnGroup n pr) fx~fy
-      given' : mod n pr (x +Z (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr }
-      given' = identityOfIndiscernablesLeft _ _ _ _≡_ given (equalityCommutative (transitivity (GroupHom.groupHom (modNExampleGroupHom n pr) {x}) (applyEquality (λ i → mod n pr x +n i) (homRespectsInverse (modNExampleGroupHom n pr)))))
-      need' : (mod n pr x) +n (mod n pr (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr }
-      need' rewrite equalityCommutative (GroupHom.groupHom (modNExampleGroupHom n pr) {x} {Group.inverse ℤGroup y}) = given'
-      need : mod n pr (x +Z (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr}
-      need = identityOfIndiscernablesLeft _ _ _ _≡_ need' (equalityCommutative (GroupHom.groupHom (modNExampleGroupHom n pr)))
-  GroupIso.surj (quotientZn n pr) {record { x = x ; xLess = xLess }} = nonneg x , intoZn x xLess
+modNExampleGroupHom : (n : ℕ) → (pr : 0 <N n) → GroupHom ℤGroup (ℤnGroup n pr) (mod n pr)
+GroupHom.groupHom (modNExampleGroupHom n 0<n) {x} {y} = {!!}
+GroupHom.wellDefined (modNExampleGroupHom n 0<n) {x} {.x} refl = refl
 
-  trivialGroupHom : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) → GroupHom trivialGroup G (λ _ → Group.identity G)
-  GroupHom.groupHom (trivialGroupHom {S = S} G) = symmetric multIdentRight
-    where
-      open Setoid S
-      open Group G
-      open Symmetric (Equivalence.symmetricEq eq)
-  GroupHom.wellDefined (trivialGroupHom {S = S} G) _ = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+intoZn : {n : ℕ} → {pr : 0 <N n} → (x : ℕ) → (x<n : x <N n) → mod n pr (nonneg x) ≡ record { x = x ; xLess = x<n }
+intoZn {zero} {()}
+intoZn {succ n} {0<n} x x<n with divisionAlg (succ n) x
+intoZn {succ n} {0<n} x x<n | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl y ; quotSmall = quotSmall } = equalityZn _ _ (modIsUnique (record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl y ; quotSmall = quotSmall }) (record { quot = 0 ; rem = x ; pr = ans ; remIsSmall = inl x<n ; quotSmall = inl (succIsPositive n)}))
+  where
+    ans : n *N 0 +N x ≡ x
+    ans rewrite multiplicationNIsCommutative n 0 = refl
+intoZn {succ n} {0<n} x x<n | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inr () ; quotSmall = quotSmall }
 
-  trivialSubgroupIsNormal : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+A_ : A → A → A} (G : Group S _+A_) → NormalSubgroup G trivialGroup (trivialGroupHom G)
-  Subgroup.fInj (NormalSubgroup.subgroup (trivialSubgroupIsNormal G)) {fzero} {fzero} _ = refl
-  Subgroup.fInj (NormalSubgroup.subgroup (trivialSubgroupIsNormal G)) {fzero} {fsucc ()} _
-  Subgroup.fInj (NormalSubgroup.subgroup (trivialSubgroupIsNormal G)) {fsucc ()} {y} _
-  NormalSubgroup.normal (trivialSubgroupIsNormal {S = S} {_+A_ = _+A_} G) = fzero , transitive (wellDefined (multIdentRight) reflexive) invRight
-    where
-      open Setoid S
-      open Group G
-      open Transitive (Equivalence.transitiveEq eq)
-      open Reflexive (Equivalence.reflexiveEq eq)
+quotientZn : (n : ℕ) → (pr : 0 <N n) → GroupIso (quotientGroup ℤGroup (modNExampleGroupHom n pr)) (ℤnGroup n pr) (mod n pr)
+GroupHom.groupHom (GroupIso.groupHom (quotientZn n pr)) = GroupHom.groupHom (modNExampleGroupHom n pr)
+GroupHom.wellDefined (GroupIso.groupHom (quotientZn n pr)) {x} {y} x~y = need
+  where
+    given : mod n pr (x +Z (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr }
+    given = x~y
+    given' : (mod n pr x) +n (mod n pr (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr }
+    given' = transitivity (equalityCommutative (GroupHom.groupHom (modNExampleGroupHom n pr))) given
+    given'' : (mod n pr x) +n Group.inverse (ℤnGroup n pr) (mod n pr y) ≡ record { x = 0 ; xLess = pr}
+    given'' = transitivity (applyEquality (λ i → mod n pr x +n i) (equalityCommutative (homRespectsInverse (modNExampleGroupHom n pr)))) given'
+    need : mod n pr x ≡ mod n pr y
+    need = transferToRight (ℤnGroup n pr) given''
+SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (quotientZn n pr))) {x} {y} x=y = {!!}
+SetoidSurjection.wellDefined (SetoidBijection.surj (GroupIso.bij (quotientZn n pr))) {x} {y} = SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (quotientZn n pr))) {x} {y}
+SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij (quotientZn n pr))) {x} {y} fx~fy = need
+  where
+    given : mod n pr x +n Group.inverse (ℤnGroup n pr) (mod n pr y) ≡ record { x = 0 ; xLess = pr }
+    given = transferToRight'' (ℤnGroup n pr) fx~fy
+    given' : mod n pr (x +Z (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr }
+    given' = identityOfIndiscernablesLeft _≡_ given (equalityCommutative (transitivity (GroupHom.groupHom (modNExampleGroupHom n pr) {x}) (applyEquality (λ i → mod n pr x +n i) (homRespectsInverse (modNExampleGroupHom n pr)))))
+    need' : (mod n pr x) +n (mod n pr (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr }
+    need' rewrite equalityCommutative (GroupHom.groupHom (modNExampleGroupHom n pr) {x} {Group.inverse ℤGroup y}) = given'
+    need : mod n pr (x +Z (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr}
+    need = identityOfIndiscernablesLeft _≡_ need' (equalityCommutative (GroupHom.groupHom (modNExampleGroupHom n pr)))
+SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (quotientZn n pr))) {record { x = x ; xLess = xLess }} = nonneg x , intoZn x xLess
 
-  improperSubgroupIsNormal : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+A_ : A → A → A} (G : Group S _+A_) → NormalSubgroup G G (identityHom G)
-  Subgroup.fInj (NormalSubgroup.subgroup (improperSubgroupIsNormal G)) = id
-  NormalSubgroup.normal (improperSubgroupIsNormal {S = S} {_+A_ = _+A_} G) {g} {h} =  ((g +A h) +A inverse g) , reflexive
-    where
-      open Group G
-      open Setoid S
-      open Reflexive (Equivalence.reflexiveEq eq)
+trivialGroupHom : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) → GroupHom trivialGroup G (λ _ → Group.0G G)
+GroupHom.groupHom (trivialGroupHom {S = S} G) = symmetric identRight
+  where
+    open Setoid S
+    open Group G
+    open Equivalence eq
+GroupHom.wellDefined (trivialGroupHom {S = S} G) _ = Equivalence.reflexive (Setoid.eq S)
+
+trivialSubgroupIsNormal : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+A_ : A → A → A} (G : Group S _+A_) → NormalSubgroup G trivialGroup (trivialGroupHom G)
+SetoidInjection.wellDefined (Subgroup.fInj (NormalSubgroup.subgroup (trivialSubgroupIsNormal {S = S} G))) {x} {.x} refl = Equivalence.reflexive (Setoid.eq S)
+SetoidInjection.injective (Subgroup.fInj (NormalSubgroup.subgroup (trivialSubgroupIsNormal G))) {fzero} {fzero} _ = refl
+SetoidInjection.injective (Subgroup.fInj (NormalSubgroup.subgroup (trivialSubgroupIsNormal G))) {fzero} {fsucc ()} _
+SetoidInjection.injective (Subgroup.fInj (NormalSubgroup.subgroup (trivialSubgroupIsNormal G))) {fsucc ()} {y} _
+NormalSubgroup.normal (trivialSubgroupIsNormal {S = S} {_+A_ = _+A_} G) = fzero , transitive (+WellDefined identRight reflexive) invRight
+  where
+    open Setoid S
+    open Group G
+    open Equivalence eq
+
+improperSubgroupIsNormal : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+A_ : A → A → A} (G : Group S _+A_) → NormalSubgroup G G (identityHom G)
+SetoidInjection.wellDefined (Subgroup.fInj (NormalSubgroup.subgroup (improperSubgroupIsNormal G))) {x} {y} x=y = x=y
+SetoidInjection.injective (Subgroup.fInj (NormalSubgroup.subgroup (improperSubgroupIsNormal G))) = id
+NormalSubgroup.normal (improperSubgroupIsNormal {S = S} {_+A_ = _+A_} G) {g} {h} =  ((g +A h) +A inverse g) , reflexive
+  where
+    open Group G
+    open Setoid S
+    open Equivalence eq
diff --git a/Groups/Groups2.agda b/Groups/Groups2.agda
index ae2d112..b7b7fed 100644
--- a/Groups/Groups2.agda
+++ b/Groups/Groups2.agda
@@ -12,8 +12,11 @@ open import Sets.EquivalenceRelations
 open import Numbers.Naturals.Naturals
 open import Groups.Homomorphisms.Definition
 open import Groups.Homomorphisms.Lemmas
+open import Groups.Homomorphisms.Image
 open import Groups.Isomorphisms.Definition
 open import Groups.Subgroups.Definition
+open import Groups.Subgroups.Normal.Definition
+open import Groups.Subgroups.Normal.Lemmas
 open import Groups.Lemmas
 open import Groups.Abelian.Definition
 open import Groups.QuotientGroup.Definition
@@ -22,46 +25,6 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
 module Groups.Groups2 where
 
-  data GroupHomImageElement {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : A → B} (fHom : GroupHom G H f) : Set (a ⊔ b ⊔ c ⊔ d) where
-    ofElt : (x : A) → GroupHomImageElement fHom
-
-  imageGroupSetoid : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : A → B} (fHom : GroupHom G H f) → Setoid (GroupHomImageElement fHom)
-  (imageGroupSetoid {T = T} {f = f} fHom Setoid.∼ ofElt b1) (ofElt b2) = Setoid._∼_ T (f b1) (f b2)
-  Equivalence.reflexive (Setoid.eq (imageGroupSetoid {T = T} fHom)) {ofElt b1} = Equivalence.reflexive (Setoid.eq T)
-  Equivalence.symmetric (Setoid.eq (imageGroupSetoid {T = T} fHom)) {ofElt b1} {ofElt b2} = Equivalence.symmetric (Setoid.eq T)
-  Equivalence.transitive (Setoid.eq (imageGroupSetoid {T = T} fHom)) {ofElt b1} {ofElt b2} {ofElt b3} = Equivalence.transitive (Setoid.eq T)
-
-  imageGroupOp : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : A → B} (fHom : GroupHom G H f) → GroupHomImageElement fHom → GroupHomImageElement fHom → GroupHomImageElement fHom
-  imageGroupOp {_+A_ = _+A_} fHom (ofElt a) (ofElt b) = ofElt (a +A b)
-
-  imageGroup : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : A → B} (fHom : GroupHom G H f) → Group (imageGroupSetoid fHom) (imageGroupOp fHom)
-  Group.+WellDefined (imageGroup {T = T} {_+A_ = _+A_} {H = H} {f = f} fHom) {ofElt x} {ofElt y} {ofElt a} {ofElt b} x~a y~b = ans
-    where
-      open Setoid T
-      open Equivalence eq
-      ans : f (x +A y) ∼ f (a +A b)
-      ans = transitive (GroupHom.groupHom fHom) (transitive (Group.+WellDefined H x~a y~b) (symmetric (GroupHom.groupHom fHom)))
-  Group.0G (imageGroup {G = G} fHom) = ofElt (Group.0G G)
-  Group.inverse (imageGroup {G = G} fHom) (ofElt a) = ofElt (Group.inverse G a)
-  Group.+Associative (imageGroup {G = G} fHom) {ofElt a} {ofElt b} {ofElt c} = GroupHom.wellDefined fHom (Group.+Associative G)
-  Group.identRight (imageGroup {G = G} fHom) {ofElt a} = GroupHom.wellDefined fHom (Group.identRight G)
-  Group.identLeft (imageGroup {G = G} fHom) {ofElt a} = GroupHom.wellDefined fHom (Group.identLeft G)
-  Group.invLeft (imageGroup {G = G} fHom) {ofElt a} = GroupHom.wellDefined fHom (Group.invLeft G)
-  Group.invRight (imageGroup {G = G} fHom) {ofElt a} = GroupHom.wellDefined fHom (Group.invRight G)
-
-  groupHomImageInclusion : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+G_ : A → A → A} {_+H_ : B → B → B} {G : Group S _+G_} {H : Group T _+H_} {f : A → B} (fHom : GroupHom G H f) → GroupHomImageElement fHom → B
-  groupHomImageInclusion {f = f} fHom (ofElt x) = f x
-
-  groupHomImageIncludes : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+G_ : A → A → A} {_+H_ : B → B → B} {G : Group S _+G_} {H : Group T _+H_} {f : A → B} (fHom : GroupHom G H f) → GroupHom (imageGroup fHom) H (groupHomImageInclusion fHom)
-  GroupHom.groupHom (groupHomImageIncludes fHom) {ofElt x} {ofElt y} = GroupHom.groupHom fHom
-  GroupHom.wellDefined (groupHomImageIncludes fHom) {ofElt x} {ofElt y} x~y = x~y
-
-  groupHomImageIsSubgroup : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+G_ : A → A → A} {_+H_ : B → B → B} {G : Group S _+G_} {H : Group T _+H_} {f : A → B} (fHom : GroupHom G H f) → Subgroup H (imageGroup fHom) (groupHomImageIncludes fHom)
-  Subgroup.fInj (groupHomImageIsSubgroup {S = S} {T} {_+G_} {_+H_} {G} {H} {f} fHom) = record { wellDefined = λ {x} {y} → GroupHom.wellDefined (groupHomImageIncludes fHom) {x} {y} ; injective = λ {x} {y} → inj {x} {y} }
-    where
-      inj : {x y : GroupHomImageElement fHom} → (Setoid._∼_ T (groupHomImageInclusion fHom x) (groupHomImageInclusion fHom y)) → Setoid._∼_ (imageGroupSetoid fHom) x y
-      inj {ofElt x} {ofElt y} x~y = x~y
-
   groupFirstIsomorphismIso : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+G_ : A → A → A} {_+H_ : B → B → B} {G : Group S _+G_} {H : Group T _+H_} {f : A → B} (fHom : GroupHom G H f) → GroupHomImageElement fHom → A
   groupFirstIsomorphismIso fHom (ofElt a) = a
 
@@ -89,82 +52,3 @@ module Groups.Groups2 where
   groupFirstIsomorphismTheorem : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+G_ : A → A → A} {_+H_ : B → B → B} {G : Group S _+G_} {H : Group T _+H_} {f : A → B} (fHom : GroupHom G H f) → GroupsIsomorphic (imageGroup fHom) (quotientGroup G fHom)
   groupFirstIsomorphismTheorem fHom = record { isomorphism = groupFirstIsomorphismIso fHom ; proof = groupFirstIsomorphismTheorem' fHom }
 
-  record NormalSubgroup {a} {b} {c} {d} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) (H : Group T _·B_) {f : B → A} (hom : GroupHom H G f) : Set (a ⊔ b ⊔ c ⊔ d) where
-    open Setoid S
-    field
-      subgroup : Subgroup G H hom
-      normal : {g : A} {h : B} → Sg B (λ fromH → (g ·A (f h)) ·A (Group.inverse G g) ∼ f fromH)
-
-  data GroupKernelElement {a} {b} {c} {d} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) : Set (a ⊔ b ⊔ c ⊔ d) where
-    kerOfElt : (x : A) → (Setoid._∼_ T (f x) (Group.0G H)) → GroupKernelElement G hom
-
-  groupKernel : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → Setoid (GroupKernelElement G hom)
-  Setoid._∼_ (groupKernel {S = S} G {H} {f} fHom) (kerOfElt x fx=0) (kerOfElt y fy=0) = Setoid._∼_ S x y
-  Equivalence.reflexive (Setoid.eq (groupKernel {S = S} G {H} {f} fHom)) {kerOfElt x x₁} = Equivalence.reflexive (Setoid.eq S)
-  Equivalence.symmetric (Setoid.eq (groupKernel {S = S} G {H} {f} fHom)) {kerOfElt x prX} {kerOfElt y prY} = Equivalence.symmetric (Setoid.eq S)
-  Equivalence.transitive (Setoid.eq (groupKernel {S = S} G {H} {f} fHom)) {kerOfElt x prX} {kerOfElt y prY} {kerOfElt z prZ} = Equivalence.transitive (Setoid.eq S)
-
-  groupKernelGroupOp : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → (GroupKernelElement G hom) → (GroupKernelElement G hom) → (GroupKernelElement G hom)
-  groupKernelGroupOp {T = T} {_·A_ = _+A_} G {H = H} hom (kerOfElt x prX) (kerOfElt y prY) = kerOfElt (x +A y) (transitive (GroupHom.groupHom hom) (transitive (Group.+WellDefined H prX prY) (Group.identLeft H)))
-    where
-      open Setoid T
-      open Equivalence eq
-
-  groupKernelGroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → Group (groupKernel G hom) (groupKernelGroupOp G hom)
-  Group.+WellDefined (groupKernelGroup G fHom) {kerOfElt x prX} {kerOfElt y prY} {kerOfElt a prA} {kerOfElt b prB} = Group.+WellDefined G
-  Group.0G (groupKernelGroup G fHom) = kerOfElt (Group.0G G) (imageOfIdentityIsIdentity fHom)
-  Group.inverse (groupKernelGroup {T = T} G {H = H} fHom) (kerOfElt x prX) = kerOfElt (Group.inverse G x) (transitive (homRespectsInverse fHom) (transitive (inverseWellDefined H prX) (invIdent H)))
-    where
-      open Setoid T
-      open Equivalence eq
-  Group.+Associative (groupKernelGroup {S = S} {_·A_ = _·A_} G fHom) {kerOfElt x prX} {kerOfElt y prY} {kerOfElt z prZ} = Group.+Associative G
-  Group.identRight (groupKernelGroup G fHom) {kerOfElt x prX} = Group.identRight G
-  Group.identLeft (groupKernelGroup G fHom) {kerOfElt x prX} = Group.identLeft G
-  Group.invLeft (groupKernelGroup G fHom) {kerOfElt x prX} = Group.invLeft G
-  Group.invRight (groupKernelGroup G fHom) {kerOfElt x prX} = Group.invRight G
-
-  injectionFromKernelToG : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → GroupKernelElement G hom → A
-  injectionFromKernelToG G hom (kerOfElt x _) = x
-
-  injectionFromKernelToGIsHom : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → GroupHom (groupKernelGroup G hom) G (injectionFromKernelToG G hom)
-  GroupHom.groupHom (injectionFromKernelToGIsHom {S = S} G hom) {kerOfElt x prX} {kerOfElt y prY} = Equivalence.reflexive (Setoid.eq S)
-  GroupHom.wellDefined (injectionFromKernelToGIsHom G hom) {kerOfElt x prX} {kerOfElt y prY} i = i
-
-  groupKernelGroupIsSubgroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → Subgroup G (groupKernelGroup G hom) (injectionFromKernelToGIsHom G hom)
-  Subgroup.fInj (groupKernelGroupIsSubgroup {S = S} {T = T} G {f = f} hom) = record { wellDefined = λ {x} {y} → GroupHom.wellDefined (injectionFromKernelToGIsHom G hom) {x} {y} ; injective = λ {x} {y} → inj {x} {y} }
-    where
-      inj : {x : GroupKernelElement G hom} → {y : GroupKernelElement G hom} → Setoid._∼_ S (injectionFromKernelToG G hom x) (injectionFromKernelToG G hom y) → Setoid._∼_ (groupKernel G hom) x y
-      inj {kerOfElt x prX} {kerOfElt y prY} = id
-
-  groupKernelGroupIsNormalSubgroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → NormalSubgroup G (groupKernelGroup G hom) (injectionFromKernelToGIsHom G hom)
-  NormalSubgroup.subgroup (groupKernelGroupIsNormalSubgroup G hom) = groupKernelGroupIsSubgroup G hom
-  NormalSubgroup.normal (groupKernelGroupIsNormalSubgroup {S = S} {T = T} {_·A_ = _·A_} G {H = H} {f = f} hom) {g} {kerOfElt h prH} = kerOfElt ((g ·A h) ·A Group.inverse G g) ans , Equivalence.reflexive (Setoid.eq S)
-    where
-      open Setoid T
-      open Equivalence eq
-      ans : f ((g ·A h) ·A Group.inverse G g) ∼ Group.0G H
-      ans = transitive (GroupHom.groupHom hom) (transitive (Group.+WellDefined H (GroupHom.groupHom hom) reflexive) (transitive (Group.+WellDefined H (Group.+WellDefined H reflexive prH) reflexive) (transitive (Group.+WellDefined H (Group.identRight H) reflexive) (transitive (symmetric (GroupHom.groupHom hom)) (transitive (GroupHom.wellDefined hom (Group.invRight G)) (imageOfIdentityIsIdentity hom))))))
-
-  abelianGroupSubgroupIsNormal : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {underG : Group S _+A_} (G : AbelianGroup underG) {H : Group T _+B_} {f : B → A} {hom : GroupHom H underG f} (s : Subgroup underG H hom) → NormalSubgroup underG H hom
-  NormalSubgroup.subgroup (abelianGroupSubgroupIsNormal G H) = H
-  NormalSubgroup.normal (abelianGroupSubgroupIsNormal {S = S} {underG = G} record { commutative = commutative } H) {g} {h} = h , transitive (+WellDefined commutative reflexive) (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight))
-    where
-      open Setoid S
-      open Group G
-      open Equivalence (Setoid.eq S)
-
-  trivialGroup : Group (reflSetoid (FinSet 1)) λ _ _ → fzero
-  Group.+WellDefined trivialGroup _ _ = refl
-  Group.0G trivialGroup = fzero
-  Group.inverse trivialGroup _ = fzero
-  Group.+Associative trivialGroup = refl
-  Group.identRight trivialGroup {fzero} = refl
-  Group.identRight trivialGroup {fsucc ()}
-  Group.identLeft trivialGroup {fzero} = refl
-  Group.identLeft trivialGroup {fsucc ()}
-  Group.invLeft trivialGroup = refl
-  Group.invRight trivialGroup = refl
-
-  identityHom : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+A_ : A → A → A} (G : Group S _+A_) → GroupHom G G id
-  GroupHom.groupHom (identityHom {S = S} G) = Equivalence.reflexive (Setoid.eq S)
-  GroupHom.wellDefined (identityHom G) = id
diff --git a/Groups/Homomorphisms/Image.agda b/Groups/Homomorphisms/Image.agda
new file mode 100644
index 0000000..5c16fa3
--- /dev/null
+++ b/Groups/Homomorphisms/Image.agda
@@ -0,0 +1,64 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Groups.Groups
+open import Groups.Definition
+open import Orders
+open import Numbers.Integers.Integers
+open import Setoids.Setoids
+open import LogicalFormulae
+open import Sets.FinSet
+open import Functions
+open import Sets.EquivalenceRelations
+open import Numbers.Naturals.Naturals
+open import Groups.Homomorphisms.Definition
+open import Groups.Homomorphisms.Lemmas
+open import Groups.Isomorphisms.Definition
+open import Groups.Subgroups.Definition
+open import Groups.Lemmas
+open import Groups.Abelian.Definition
+open import Groups.QuotientGroup.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Groups.Homomorphisms.Image where
+
+data GroupHomImageElement {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : A → B} (fHom : GroupHom G H f) : Set (a ⊔ b ⊔ c ⊔ d) where
+  ofElt : (x : A) → GroupHomImageElement fHom
+
+imageGroupSetoid : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : A → B} (fHom : GroupHom G H f) → Setoid (GroupHomImageElement fHom)
+(imageGroupSetoid {T = T} {f = f} fHom Setoid.∼ ofElt b1) (ofElt b2) = Setoid._∼_ T (f b1) (f b2)
+Equivalence.reflexive (Setoid.eq (imageGroupSetoid {T = T} fHom)) {ofElt b1} = Equivalence.reflexive (Setoid.eq T)
+Equivalence.symmetric (Setoid.eq (imageGroupSetoid {T = T} fHom)) {ofElt b1} {ofElt b2} = Equivalence.symmetric (Setoid.eq T)
+Equivalence.transitive (Setoid.eq (imageGroupSetoid {T = T} fHom)) {ofElt b1} {ofElt b2} {ofElt b3} = Equivalence.transitive (Setoid.eq T)
+
+imageGroupOp : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : A → B} (fHom : GroupHom G H f) → GroupHomImageElement fHom → GroupHomImageElement fHom → GroupHomImageElement fHom
+imageGroupOp {_+A_ = _+A_} fHom (ofElt a) (ofElt b) = ofElt (a +A b)
+
+imageGroup : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : A → B} (fHom : GroupHom G H f) → Group (imageGroupSetoid fHom) (imageGroupOp fHom)
+Group.+WellDefined (imageGroup {T = T} {_+A_ = _+A_} {H = H} {f = f} fHom) {ofElt x} {ofElt y} {ofElt a} {ofElt b} x~a y~b = ans
+  where
+    open Setoid T
+    open Equivalence eq
+    ans : f (x +A y) ∼ f (a +A b)
+    ans = transitive (GroupHom.groupHom fHom) (transitive (Group.+WellDefined H x~a y~b) (symmetric (GroupHom.groupHom fHom)))
+Group.0G (imageGroup {G = G} fHom) = ofElt (Group.0G G)
+Group.inverse (imageGroup {G = G} fHom) (ofElt a) = ofElt (Group.inverse G a)
+Group.+Associative (imageGroup {G = G} fHom) {ofElt a} {ofElt b} {ofElt c} = GroupHom.wellDefined fHom (Group.+Associative G)
+Group.identRight (imageGroup {G = G} fHom) {ofElt a} = GroupHom.wellDefined fHom (Group.identRight G)
+Group.identLeft (imageGroup {G = G} fHom) {ofElt a} = GroupHom.wellDefined fHom (Group.identLeft G)
+Group.invLeft (imageGroup {G = G} fHom) {ofElt a} = GroupHom.wellDefined fHom (Group.invLeft G)
+Group.invRight (imageGroup {G = G} fHom) {ofElt a} = GroupHom.wellDefined fHom (Group.invRight G)
+
+groupHomImageInclusion : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+G_ : A → A → A} {_+H_ : B → B → B} {G : Group S _+G_} {H : Group T _+H_} {f : A → B} (fHom : GroupHom G H f) → GroupHomImageElement fHom → B
+groupHomImageInclusion {f = f} fHom (ofElt x) = f x
+
+groupHomImageIncludes : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+G_ : A → A → A} {_+H_ : B → B → B} {G : Group S _+G_} {H : Group T _+H_} {f : A → B} (fHom : GroupHom G H f) → GroupHom (imageGroup fHom) H (groupHomImageInclusion fHom)
+GroupHom.groupHom (groupHomImageIncludes fHom) {ofElt x} {ofElt y} = GroupHom.groupHom fHom
+GroupHom.wellDefined (groupHomImageIncludes fHom) {ofElt x} {ofElt y} x~y = x~y
+
+groupHomImageIsSubgroup : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+G_ : A → A → A} {_+H_ : B → B → B} {G : Group S _+G_} {H : Group T _+H_} {f : A → B} (fHom : GroupHom G H f) → Subgroup H (imageGroup fHom) (groupHomImageIncludes fHom)
+Subgroup.fInj (groupHomImageIsSubgroup {S = S} {T} {_+G_} {_+H_} {G} {H} {f} fHom) = record { wellDefined = λ {x} {y} → GroupHom.wellDefined (groupHomImageIncludes fHom) {x} {y} ; injective = λ {x} {y} → inj {x} {y} }
+  where
+    inj : {x y : GroupHomImageElement fHom} → (Setoid._∼_ T (groupHomImageInclusion fHom x) (groupHomImageInclusion fHom y)) → Setoid._∼_ (imageGroupSetoid fHom) x y
+    inj {ofElt x} {ofElt y} x~y = x~y
+
diff --git a/Groups/Homomorphisms/Lemmas.agda b/Groups/Homomorphisms/Lemmas.agda
index cc862bb..a79c4ee 100644
--- a/Groups/Homomorphisms/Lemmas.agda
+++ b/Groups/Homomorphisms/Lemmas.agda
@@ -40,3 +40,7 @@ homRespectsInverse {T = T} {_·A_ = _·A_} {_·B_ = _·B_} {G = G} {H = H} {unde
   where
     open Setoid T
     open Equivalence eq
+
+identityHom : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+A_ : A → A → A} (G : Group S _+A_) → GroupHom G G id
+GroupHom.groupHom (identityHom {S = S} G) = Equivalence.reflexive (Setoid.eq S)
+GroupHom.wellDefined (identityHom G) = id
diff --git a/Groups/Subgroups/Normal/Definition.agda b/Groups/Subgroups/Normal/Definition.agda
new file mode 100644
index 0000000..bd3f1f0
--- /dev/null
+++ b/Groups/Subgroups/Normal/Definition.agda
@@ -0,0 +1,29 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Groups.Groups
+open import Groups.Definition
+open import Orders
+open import Numbers.Integers.Integers
+open import Setoids.Setoids
+open import LogicalFormulae
+open import Sets.FinSet
+open import Functions
+open import Sets.EquivalenceRelations
+open import Numbers.Naturals.Naturals
+open import Groups.Homomorphisms.Definition
+open import Groups.Homomorphisms.Lemmas
+open import Groups.Isomorphisms.Definition
+open import Groups.Subgroups.Definition
+open import Groups.Lemmas
+open import Groups.Abelian.Definition
+open import Groups.QuotientGroup.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Groups.Subgroups.Normal.Definition where
+
+record NormalSubgroup {a} {b} {c} {d} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) (H : Group T _·B_) {f : B → A} (hom : GroupHom H G f) : Set (a ⊔ b ⊔ c ⊔ d) where
+  open Setoid S
+  field
+    subgroup : Subgroup G H hom
+    normal : {g : A} {h : B} → Sg B (λ fromH → (g ·A (f h)) ·A (Group.inverse G g) ∼ f fromH)
diff --git a/Groups/Subgroups/Normal/Lemmas.agda b/Groups/Subgroups/Normal/Lemmas.agda
new file mode 100644
index 0000000..f1d2f74
--- /dev/null
+++ b/Groups/Subgroups/Normal/Lemmas.agda
@@ -0,0 +1,82 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Groups.Groups
+open import Groups.Definition
+open import Orders
+open import Numbers.Integers.Integers
+open import Setoids.Setoids
+open import LogicalFormulae
+open import Sets.FinSet
+open import Functions
+open import Sets.EquivalenceRelations
+open import Numbers.Naturals.Naturals
+open import Groups.Homomorphisms.Definition
+open import Groups.Homomorphisms.Lemmas
+open import Groups.Isomorphisms.Definition
+open import Groups.Subgroups.Definition
+open import Groups.Lemmas
+open import Groups.Abelian.Definition
+open import Groups.QuotientGroup.Definition
+open import Groups.Subgroups.Normal.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Groups.Subgroups.Normal.Lemmas where
+
+data GroupKernelElement {a} {b} {c} {d} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) : Set (a ⊔ b ⊔ c ⊔ d) where
+  kerOfElt : (x : A) → (Setoid._∼_ T (f x) (Group.0G H)) → GroupKernelElement G hom
+
+groupKernel : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → Setoid (GroupKernelElement G hom)
+Setoid._∼_ (groupKernel {S = S} G {H} {f} fHom) (kerOfElt x fx=0) (kerOfElt y fy=0) = Setoid._∼_ S x y
+Equivalence.reflexive (Setoid.eq (groupKernel {S = S} G {H} {f} fHom)) {kerOfElt x x₁} = Equivalence.reflexive (Setoid.eq S)
+Equivalence.symmetric (Setoid.eq (groupKernel {S = S} G {H} {f} fHom)) {kerOfElt x prX} {kerOfElt y prY} = Equivalence.symmetric (Setoid.eq S)
+Equivalence.transitive (Setoid.eq (groupKernel {S = S} G {H} {f} fHom)) {kerOfElt x prX} {kerOfElt y prY} {kerOfElt z prZ} = Equivalence.transitive (Setoid.eq S)
+
+groupKernelGroupOp : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → (GroupKernelElement G hom) → (GroupKernelElement G hom) → (GroupKernelElement G hom)
+groupKernelGroupOp {T = T} {_·A_ = _+A_} G {H = H} hom (kerOfElt x prX) (kerOfElt y prY) = kerOfElt (x +A y) (transitive (GroupHom.groupHom hom) (transitive (Group.+WellDefined H prX prY) (Group.identLeft H)))
+  where
+    open Setoid T
+    open Equivalence eq
+
+groupKernelGroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → Group (groupKernel G hom) (groupKernelGroupOp G hom)
+Group.+WellDefined (groupKernelGroup G fHom) {kerOfElt x prX} {kerOfElt y prY} {kerOfElt a prA} {kerOfElt b prB} = Group.+WellDefined G
+Group.0G (groupKernelGroup G fHom) = kerOfElt (Group.0G G) (imageOfIdentityIsIdentity fHom)
+Group.inverse (groupKernelGroup {T = T} G {H = H} fHom) (kerOfElt x prX) = kerOfElt (Group.inverse G x) (transitive (homRespectsInverse fHom) (transitive (inverseWellDefined H prX) (invIdent H)))
+  where
+    open Setoid T
+    open Equivalence eq
+Group.+Associative (groupKernelGroup {S = S} {_·A_ = _·A_} G fHom) {kerOfElt x prX} {kerOfElt y prY} {kerOfElt z prZ} = Group.+Associative G
+Group.identRight (groupKernelGroup G fHom) {kerOfElt x prX} = Group.identRight G
+Group.identLeft (groupKernelGroup G fHom) {kerOfElt x prX} = Group.identLeft G
+Group.invLeft (groupKernelGroup G fHom) {kerOfElt x prX} = Group.invLeft G
+Group.invRight (groupKernelGroup G fHom) {kerOfElt x prX} = Group.invRight G
+
+injectionFromKernelToG : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → GroupKernelElement G hom → A
+injectionFromKernelToG G hom (kerOfElt x _) = x
+
+injectionFromKernelToGIsHom : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → GroupHom (groupKernelGroup G hom) G (injectionFromKernelToG G hom)
+GroupHom.groupHom (injectionFromKernelToGIsHom {S = S} G hom) {kerOfElt x prX} {kerOfElt y prY} = Equivalence.reflexive (Setoid.eq S)
+GroupHom.wellDefined (injectionFromKernelToGIsHom G hom) {kerOfElt x prX} {kerOfElt y prY} i = i
+
+groupKernelGroupIsSubgroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → Subgroup G (groupKernelGroup G hom) (injectionFromKernelToGIsHom G hom)
+Subgroup.fInj (groupKernelGroupIsSubgroup {S = S} {T = T} G {f = f} hom) = record { wellDefined = λ {x} {y} → GroupHom.wellDefined (injectionFromKernelToGIsHom G hom) {x} {y} ; injective = λ {x} {y} → inj {x} {y} }
+  where
+    inj : {x : GroupKernelElement G hom} → {y : GroupKernelElement G hom} → Setoid._∼_ S (injectionFromKernelToG G hom x) (injectionFromKernelToG G hom y) → Setoid._∼_ (groupKernel G hom) x y
+    inj {kerOfElt x prX} {kerOfElt y prY} = id
+
+groupKernelGroupIsNormalSubgroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → NormalSubgroup G (groupKernelGroup G hom) (injectionFromKernelToGIsHom G hom)
+NormalSubgroup.subgroup (groupKernelGroupIsNormalSubgroup G hom) = groupKernelGroupIsSubgroup G hom
+NormalSubgroup.normal (groupKernelGroupIsNormalSubgroup {S = S} {T = T} {_·A_ = _·A_} G {H = H} {f = f} hom) {g} {kerOfElt h prH} = kerOfElt ((g ·A h) ·A Group.inverse G g) ans , Equivalence.reflexive (Setoid.eq S)
+  where
+    open Setoid T
+    open Equivalence eq
+    ans : f ((g ·A h) ·A Group.inverse G g) ∼ Group.0G H
+    ans = transitive (GroupHom.groupHom hom) (transitive (Group.+WellDefined H (GroupHom.groupHom hom) reflexive) (transitive (Group.+WellDefined H (Group.+WellDefined H reflexive prH) reflexive) (transitive (Group.+WellDefined H (Group.identRight H) reflexive) (transitive (symmetric (GroupHom.groupHom hom)) (transitive (GroupHom.wellDefined hom (Group.invRight G)) (imageOfIdentityIsIdentity hom))))))
+
+abelianGroupSubgroupIsNormal : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {underG : Group S _+A_} (G : AbelianGroup underG) {H : Group T _+B_} {f : B → A} {hom : GroupHom H underG f} (s : Subgroup underG H hom) → NormalSubgroup underG H hom
+NormalSubgroup.subgroup (abelianGroupSubgroupIsNormal G H) = H
+NormalSubgroup.normal (abelianGroupSubgroupIsNormal {S = S} {underG = G} record { commutative = commutative } H) {g} {h} = h , transitive (+WellDefined commutative reflexive) (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight))
+  where
+    open Setoid S
+    open Group G
+    open Equivalence (Setoid.eq S)