diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index 44d80c4..43f9d2a 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -62,10 +62,12 @@ open import Rings.Homomorphisms.Kernel
 open import Rings.Ideals.FirstIsomorphismTheorem
 open import Rings.Ideals.Lemmas
 open import Rings.Ideals.Prime.Definition
+open import Rings.Ideals.Prime.Lemmas
 open import Rings.Ideals.Principal.Definition
 open import Rings.IntegralDomains.Examples
 open import Rings.PrincipalIdealDomain
 open import Rings.Subrings.Definition
+open import Rings.Ideals.Maximal.Lemmas
 
 open import Setoids.Setoids
 open import Setoids.DirectSum
diff --git a/Rings/Homomorphisms/Kernel.agda b/Rings/Homomorphisms/Kernel.agda
index a68ba47..7448ab1 100644
--- a/Rings/Homomorphisms/Kernel.agda
+++ b/Rings/Homomorphisms/Kernel.agda
@@ -12,10 +12,17 @@ open import Sets.EquivalenceRelations
 open import Rings.Definition
 open import Rings.Homomorphisms.Definition
 open import Groups.Homomorphisms.Lemmas
+open import Rings.Ideals.Definition
 
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
 module Rings.Homomorphisms.Kernel {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_+1_ _*1_ : A → A → A} {_+2_ _*2_ : B → B → B} {R1 : Ring S _+1_ _*1_} {R2 : Ring T _+2_ _*2_} {f : A → B} (fHom : RingHom R1 R2 f) where
 
-ringKernel : Set (a ⊔ d)
-ringKernel = Sg A (λ a → Setoid._∼_ T (f a) (Ring.0R R2))
+open import Groups.Homomorphisms.Kernel (RingHom.groupHom fHom)
+
+ringKernelIsIdeal : Ideal R1 groupKernelPred
+Ideal.isSubgroup ringKernelIsIdeal = groupKernelIsSubgroup
+Ideal.accumulatesTimes ringKernelIsIdeal {x} {y} fx=0 = transitive (RingHom.ringHom fHom) (transitive (Ring.*WellDefined R2 fx=0 reflexive) (transitive (Ring.*Commutative R2) (Ring.timesZero R2)))
+  where
+    open Setoid T
+    open Equivalence eq
diff --git a/Rings/Ideals/Definition.agda b/Rings/Ideals/Definition.agda
index e037428..51c528e 100644
--- a/Rings/Ideals/Definition.agda
+++ b/Rings/Ideals/Definition.agda
@@ -2,8 +2,10 @@
 
 open import LogicalFormulae
 open import Groups.Groups
+open import Groups.Lemmas
 open import Groups.Homomorphisms.Definition
 open import Groups.Definition
+open import Groups.Subgroups.Definition
 open import Numbers.Naturals.Naturals
 open import Setoids.Orders
 open import Setoids.Setoids
@@ -17,13 +19,29 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
 module Rings.Ideals.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
 
-open import Groups.Subgroups.Definition (Ring.additiveGroup R)
+open Ring R
+open Setoid S
+open Equivalence eq
+open Group additiveGroup
+
+open import Rings.Lemmas R
 
 record Ideal {c : _} (pred : A → Set c) : Set (a ⊔ b ⊔ c) where
   field
-    isSubgroup : Subgroup pred
+    isSubgroup : Subgroup additiveGroup pred
     accumulatesTimes : {x : A} → {y : A} → pred x → pred (x * y)
   closedUnderPlus = Subgroup.closedUnderPlus isSubgroup
   closedUnderInverse = Subgroup.closedUnderInverse isSubgroup
   containsIdentity = Subgroup.containsIdentity isSubgroup
   isSubset = Subgroup.isSubset isSubgroup
+  predicate = pred
+
+generatedIdealPred : A → A → Set (a ⊔ b)
+generatedIdealPred a b = Sg A (λ c → Setoid._∼_ S (a * c) b)
+
+generatedIdeal : (a : A) → Ideal (generatedIdealPred a)
+Subgroup.isSubset (Ideal.isSubgroup (generatedIdeal a)) {x} {y} x=y (c , prC) = c , transitive prC x=y
+Subgroup.closedUnderPlus (Ideal.isSubgroup (generatedIdeal a)) {g} {h} (c , prC) (d , prD) = (c + d) , transitive *DistributesOver+ (+WellDefined prC prD)
+Subgroup.containsIdentity (Ideal.isSubgroup (generatedIdeal a)) = 0G , timesZero
+Subgroup.closedUnderInverse (Ideal.isSubgroup (generatedIdeal a)) {g} (c , prC) = inverse c , transitive ringMinusExtracts (inverseWellDefined additiveGroup prC)
+Ideal.accumulatesTimes (generatedIdeal a) {x} {y} (c , prC) = (c * y) , transitive *Associative (*WellDefined prC reflexive)
diff --git a/Rings/Ideals/FirstIsomorphismTheorem.agda b/Rings/Ideals/FirstIsomorphismTheorem.agda
index 19e1a22..e29b0a0 100644
--- a/Rings/Ideals/FirstIsomorphismTheorem.agda
+++ b/Rings/Ideals/FirstIsomorphismTheorem.agda
@@ -4,6 +4,7 @@ open import LogicalFormulae
 open import Groups.Groups
 open import Groups.Homomorphisms.Definition
 open import Groups.Definition
+open import Groups.Lemmas
 open import Numbers.Naturals.Naturals
 open import Setoids.Orders
 open import Setoids.Setoids
@@ -13,6 +14,7 @@ open import Rings.Definition
 open import Rings.Homomorphisms.Definition
 open import Groups.Homomorphisms.Lemmas
 open import Rings.Subrings.Definition
+open import Rings.Cosets
 open import Rings.Isomorphisms.Definition
 open import Groups.Isomorphisms.Definition
 
@@ -22,10 +24,22 @@ module Rings.Ideals.FirstIsomorphismTheorem {a b c d : _} {A : Set a} {B : Set c
 
 open import Rings.Quotients.Definition R1 R2 hom
 open import Rings.Homomorphisms.Image hom
+open import Rings.Homomorphisms.Kernel hom
 open Setoid T
 open Equivalence eq
 open import Groups.FirstIsomorphismTheorem (RingHom.groupHom hom)
 
+ringFirstIsomorphismTheorem : RingsIsomorphic (cosetRing R1 ringKernelIsIdeal) (subringIsRing R2 imageGroupSubring)
+RingsIsomorphic.f ringFirstIsomorphismTheorem = GroupsIsomorphic.isomorphism groupFirstIsomorphismTheorem
+RingHom.preserves1 (RingIso.ringHom (RingsIsomorphic.iso ringFirstIsomorphismTheorem)) = RingHom.preserves1 hom
+RingHom.ringHom (RingIso.ringHom (RingsIsomorphic.iso ringFirstIsomorphismTheorem)) = RingHom.ringHom hom
+GroupHom.groupHom (RingHom.groupHom (RingIso.ringHom (RingsIsomorphic.iso ringFirstIsomorphismTheorem))) = GroupHom.groupHom (RingHom.groupHom hom)
+GroupHom.wellDefined (RingHom.groupHom (RingIso.ringHom (RingsIsomorphic.iso ringFirstIsomorphismTheorem))) {x} {y} x=y = transferToRight (Ring.additiveGroup R2) t
+  where
+    t : f x +B Group.inverse (Ring.additiveGroup R2) (f y) ∼ Ring.0R R2
+    t = transitive (Ring.groupIsAbelian R2) (transitive (Group.+WellDefined (Ring.additiveGroup R2) (symmetric (homRespectsInverse (RingHom.groupHom hom))) reflexive) (transitive (symmetric (GroupHom.groupHom (RingHom.groupHom hom))) x=y))
+RingIso.bijective (RingsIsomorphic.iso ringFirstIsomorphismTheorem) = GroupIso.bij (GroupsIsomorphic.proof groupFirstIsomorphismTheorem)
+
 ringFirstIsomorphismTheorem' : RingsIsomorphic quotientByRingHom (subringIsRing R2 imageGroupSubring)
 RingsIsomorphic.f ringFirstIsomorphismTheorem' a = f a , (a , reflexive)
 RingHom.preserves1 (RingIso.ringHom (RingsIsomorphic.iso ringFirstIsomorphismTheorem')) = RingHom.preserves1 hom
diff --git a/Rings/Ideals/Lemmas.agda b/Rings/Ideals/Lemmas.agda
index d00a9b9..c5854fb 100644
--- a/Rings/Ideals/Lemmas.agda
+++ b/Rings/Ideals/Lemmas.agda
@@ -15,20 +15,21 @@ open import Groups.Homomorphisms.Lemmas
 open import Groups.Subgroups.Definition
 open import Rings.Homomorphisms.Kernel
 open import Rings.Cosets
+open import Groups.Lemmas
+open import Setoids.Functions.Lemmas
+open import Rings.Ideals.Definition
 
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
 module Rings.Ideals.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
 
-open import Rings.Ideals.Definition R
-
 idealPredForKernel : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} (R2 : Ring T _+2_ _*2_) {f : A → C} (fHom : RingHom R R2 f) → A → Set d
 idealPredForKernel {T = T} R2 {f} fHom a = Setoid._∼_ T (f a) (Ring.0R R2)
 
 idealPredForKernelWellDefined : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} (R2 : Ring T _+2_ _*2_) {f : A → C} (fHom : RingHom R R2 f) → {x y : A} → (Setoid._∼_ S x y) → (idealPredForKernel R2 fHom x → idealPredForKernel R2 fHom y)
 idealPredForKernelWellDefined {T = T} R2 {f} fHom a x=0 = Equivalence.transitive (Setoid.eq T) (GroupHom.wellDefined (RingHom.groupHom fHom) (Equivalence.symmetric (Setoid.eq S) a)) x=0
 
-kernelIdealIsIdeal : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} {R2 : Ring T _+2_ _*2_} {f : A → C} (fHom : RingHom R R2 f) → Ideal (idealPredForKernel R2 fHom)
+kernelIdealIsIdeal : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} {R2 : Ring T _+2_ _*2_} {f : A → C} (fHom : RingHom R R2 f) → Ideal R (idealPredForKernel R2 fHom)
 Subgroup.isSubset (Ideal.isSubgroup (kernelIdealIsIdeal {R2 = R2} fHom)) = idealPredForKernelWellDefined R2 fHom
 Subgroup.closedUnderPlus (Ideal.isSubgroup (kernelIdealIsIdeal {T = T} {R2 = R2} fHom)) {x} {y} fx=0 fy=0 = transitive (transitive (GroupHom.groupHom (RingHom.groupHom fHom)) (+WellDefined fx=0 fy=0)) identLeft
   where
@@ -48,11 +49,19 @@ Ideal.accumulatesTimes (kernelIdealIsIdeal {T = T} {R2 = R2} {f = f} fHom) {x} {
     open Setoid T
     open Equivalence eq
 
-open Setoid S
 open Ring R
 open Group additiveGroup
+open Setoid S
 open Equivalence eq
-open import Groups.Lemmas additiveGroup
 
-idealIsKernelMap : {c : _} {pred : A → Set c} → (i : Ideal pred) → {x : A} → pred x → ringKernel {R1 = R} {R2 = cosetRing R i} (cosetRingHom R i)
-idealIsKernelMap {c} {pred} i {x} predX = x , (Ideal.isSubset i (transitive (symmetric identLeft) (+WellDefined (symmetric invIdent) reflexive)) predX)
+translate : {c : _} {pred : A → Set c} → (i : Ideal R pred) → {a : A} → pred a → pred (inverse (Ring.0R (cosetRing R i)) + a)
+translate {a} i predA = Ideal.isSubset i (transitive (symmetric identLeft) (+WellDefined (symmetric (invIdent additiveGroup)) reflexive)) predA
+translate' : {c : _} {pred : A → Set c} → (i : Ideal R pred) → {a : A} → pred (inverse (Ring.0R (cosetRing R i)) + a) → pred a
+translate' i = Ideal.isSubset i (transitive (+WellDefined (invIdent additiveGroup) reflexive) identLeft)
+
+inverseImageIsIdeal : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} {R2 : Ring T _+2_ _*2_} {f : C → A} (fHom : RingHom R2 R f) → {e : _} {pred : A → Set e} → (i : Ideal R pred) → Ideal R2 (inverseImagePred {S = T} {S} {f} (GroupHom.wellDefined (RingHom.groupHom fHom)) (Ideal.isSubset i))
+Subgroup.isSubset (Ideal.isSubgroup (inverseImageIsIdeal {T = T} fHom i)) = inverseImageWellDefined {S = T} {S} (GroupHom.wellDefined (RingHom.groupHom fHom)) (Ideal.isSubset i)
+Subgroup.closedUnderPlus (Ideal.isSubgroup (inverseImageIsIdeal fHom i)) {g} {h} (c , (prC ,, fg=c)) (d , (prD ,, fh=d)) = (c + d) , (Ideal.closedUnderPlus i prC prD ,, transitive (GroupHom.groupHom (RingHom.groupHom fHom)) (+WellDefined fg=c fh=d))
+Subgroup.containsIdentity (Ideal.isSubgroup (inverseImageIsIdeal fHom i)) = 0G , (Ideal.containsIdentity i ,, imageOfIdentityIsIdentity (RingHom.groupHom fHom))
+Subgroup.closedUnderInverse (Ideal.isSubgroup (inverseImageIsIdeal fHom i)) (a , (prA ,, fg=a)) = inverse a , (Ideal.closedUnderInverse i prA ,, transitive (homRespectsInverse (RingHom.groupHom fHom)) (inverseWellDefined additiveGroup fg=a))
+Ideal.accumulatesTimes (inverseImageIsIdeal {_*2_ = _*2_} {f = f} fHom i) {g} {h} (a , (prA ,, fg=a)) = (a * f h) , (Ideal.accumulatesTimes i prA ,, transitive (RingHom.ringHom fHom) (*WellDefined fg=a reflexive))
diff --git a/Rings/Ideals/Maximal/Definition.agda b/Rings/Ideals/Maximal/Definition.agda
new file mode 100644
index 0000000..b956b2f
--- /dev/null
+++ b/Rings/Ideals/Maximal/Definition.agda
@@ -0,0 +1,21 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Lemmas
+open import Groups.Definition
+open import Setoids.Setoids
+open import Rings.Definition
+open import Rings.Lemmas
+open import Sets.EquivalenceRelations
+open import Rings.Ideals.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.Ideals.Maximal.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {pred : A → Set c} (i : Ideal R pred) where
+
+record MaximalIdeal {d : _} : Set (a ⊔ b ⊔ c ⊔ lsuc d) where
+  field
+    notContained : A
+    notContainedIsNotContained : (pred notContained) → False
+    isMaximal : {bigger : A → Set d} → Ideal R bigger → ({a : A} → pred a → bigger a) → (Sg A (λ a → bigger a && (pred a → False))) → ({a : A} → bigger a)
diff --git a/Rings/Ideals/Maximal/Lemmas.agda b/Rings/Ideals/Maximal/Lemmas.agda
new file mode 100644
index 0000000..ad40ff1
--- /dev/null
+++ b/Rings/Ideals/Maximal/Lemmas.agda
@@ -0,0 +1,79 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Cosets
+open import Groups.Homomorphisms.Definition
+open import Rings.Homomorphisms.Definition
+open import Groups.Lemmas
+open import Groups.Definition
+open import Setoids.Setoids
+open import Setoids.Subset
+open import Setoids.Functions.Definition
+open import Setoids.Functions.Lemmas
+open import Rings.Definition
+open import Rings.Lemmas
+open import Sets.EquivalenceRelations
+open import Rings.Ideals.Definition
+open import Fields.Fields
+open import Rings.Cosets
+open import Rings.Ideals.Maximal.Definition
+open import Rings.Ideals.Lemmas
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.Ideals.Maximal.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {pred : A → Set c} (i : Ideal R pred) (proper : A) (isProper : pred proper → False) where
+
+open Ring R
+open Group additiveGroup
+open Setoid S
+open Equivalence eq
+
+idealMaximalImpliesQuotientField : ({d : Level} → MaximalIdeal i {d}) → Field (cosetRing R i)
+Field.allInvertible (idealMaximalImpliesQuotientField max) cosetA cosetA!=0 = ans' , ans''
+  where
+    gen : Ideal (cosetRing R i) (generatedIdealPred (cosetRing R i) cosetA)
+    gen = generatedIdeal (cosetRing R i) cosetA
+    inv : Ideal R (inverseImagePred {S = S} {T = cosetSetoid additiveGroup (Ideal.isSubgroup i)} (GroupHom.wellDefined (RingHom.groupHom (cosetRingHom R i))) (Ideal.isSubset gen))
+    inv = inverseImageIsIdeal (cosetRing R i) (cosetRingHom R i) gen
+    containsOnce : {a : A} → (Ideal.predicate i a) → (Ideal.predicate inv a)
+    containsOnce {x} ix = x , ((x , Ideal.closedUnderPlus i (Ideal.closedUnderInverse i ix) (Ideal.isSubset i *Commutative (Ideal.accumulatesTimes i ix))) ,, Ideal.isSubset i (symmetric invLeft) (Ideal.containsIdentity i))
+    notInI : A
+    notInI = cosetA
+    notInIIsInInv : Ideal.predicate inv notInI
+    notInIIsInInv = cosetA , ((1R , Ideal.isSubset i {0R} (symmetric (transitive (+WellDefined reflexive (transitive *Commutative identIsIdent)) (invLeft {cosetA}))) (Ideal.containsIdentity i)) ,, Ideal.isSubset i (symmetric invLeft) (Ideal.containsIdentity i))
+    notInIPr : (Ideal.predicate i notInI) → False
+    notInIPr iInI = cosetA!=0 (Ideal.isSubset i (transitive (symmetric identLeft) (+WellDefined (symmetric (invIdent additiveGroup)) reflexive)) iInI)
+    ans : {a : A} → Ideal.predicate inv a
+    ans = MaximalIdeal.isMaximal max inv containsOnce (notInI , (notInIIsInInv ,, notInIPr))
+    ans' : A
+    ans' with ans {1R}
+    ... | _ , ((b , _) ,, _) = b
+    ans'' : pred (inverse (Ring.1R (cosetRing R i)) + (ans' * cosetA))
+    ans'' with ans {1R}
+    ans'' | a , ((b , predCAb-a) ,, pred1-a) = Ideal.isSubset i (transitive (+WellDefined (invContravariant additiveGroup) reflexive) (transitive +Associative (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) *Commutative))) (Ideal.closedUnderPlus i (Ideal.closedUnderInverse i pred1-a) predCAb-a)
+Field.nontrivial (idealMaximalImpliesQuotientField max) 1=0 = isProper (Ideal.isSubset i (identIsIdent {proper}) (Ideal.accumulatesTimes i p))
+  where
+    have : pred (inverse 1R)
+    have = Ideal.isSubset i identRight 1=0
+    p : pred 1R
+    p = Ideal.isSubset i (invTwice additiveGroup 1R) (Ideal.closedUnderInverse i have)
+
+quotientFieldImpliesIdealMaximal : Field (cosetRing R i) → ({d : _} → MaximalIdeal i {d})
+MaximalIdeal.notContained (quotientFieldImpliesIdealMaximal f) = proper
+MaximalIdeal.notContainedIsNotContained (quotientFieldImpliesIdealMaximal f) = isProper
+MaximalIdeal.isMaximal (quotientFieldImpliesIdealMaximal f) {bigger} biggerIdeal contained (a , (biggerA ,, notPredA)) = Ideal.isSubset biggerIdeal identIsIdent (Ideal.accumulatesTimes biggerIdeal v)
+  where
+    inv : Sg A (λ t → pred (inverse 1R + (t * a)))
+    inv = Field.allInvertible f a λ r → notPredA (translate' R i r)
+    r : A
+    r = underlying inv
+    s : pred (inverse 1R + (r * a))
+    s with inv
+    ... | _ , p = p
+    t : bigger (inverse 1R + (r * a))
+    t = contained s
+    u : bigger (inverse (r * a))
+    u = Ideal.closedUnderInverse biggerIdeal (Ideal.isSubset biggerIdeal *Commutative (Ideal.accumulatesTimes biggerIdeal biggerA))
+    v : bigger 1R
+    v = Ideal.isSubset biggerIdeal (invTwice additiveGroup 1R) (Ideal.closedUnderInverse biggerIdeal (Ideal.isSubset biggerIdeal (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) (Ideal.closedUnderPlus biggerIdeal t u)))
diff --git a/Rings/Ideals/Prime/Definition.agda b/Rings/Ideals/Prime/Definition.agda
index 55128b2..66e4903 100644
--- a/Rings/Ideals/Prime/Definition.agda
+++ b/Rings/Ideals/Prime/Definition.agda
@@ -18,5 +18,8 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
 module Rings.Ideals.Prime.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {pred : A → Set c} (i : Ideal R pred) where
 
-PrimeIdeal : Set (a ⊔ c)
-PrimeIdeal = {a b : A} → pred (a * b) → ((pred a) → False) → pred b
+record PrimeIdeal : Set (a ⊔ c) where
+  field
+    isPrime : {a b : A} → pred (a * b) → ((pred a) → False) → pred b
+    notContained : A
+    notContainedIsNotContained : (pred notContained) → False
diff --git a/Rings/Ideals/Prime/Lemmas.agda b/Rings/Ideals/Prime/Lemmas.agda
new file mode 100644
index 0000000..dee9b86
--- /dev/null
+++ b/Rings/Ideals/Prime/Lemmas.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Lemmas
+open import Groups.Definition
+open import Setoids.Setoids
+open import Rings.Definition
+open import Sets.EquivalenceRelations
+open import Rings.Ideals.Definition
+open import Rings.IntegralDomains.Definition
+open import Rings.Ideals.Prime.Definition
+open import Rings.Cosets
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.Ideals.Prime.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {pred : A → Set c} (i : Ideal R pred) where
+
+open Ring R
+open Group additiveGroup
+open Setoid S
+open Equivalence eq
+open import Rings.Ideals.Lemmas R
+
+idealPrimeImpliesQuotientIntDom : PrimeIdeal i → IntegralDomain (cosetRing R i)
+IntegralDomain.intDom (idealPrimeImpliesQuotientIntDom isPrime) {a} {b} ab=0 a!=0 = ans
+  where
+    ab=0' : pred (a * b)
+    ab=0' = translate' i ab=0
+    a!=0' : (pred a) → False
+    a!=0' prA = a!=0 (translate i prA)
+    ans' : pred b
+    ans' = PrimeIdeal.isPrime isPrime ab=0' a!=0'
+    ans : pred (inverse (Ring.0R (cosetRing R i)) + b)
+    ans = translate i ans'
+IntegralDomain.nontrivial (idealPrimeImpliesQuotientIntDom isPrime) 1=0 = PrimeIdeal.notContainedIsNotContained isPrime u
+  where
+    t : pred (Ring.1R (cosetRing R i))
+    t = translate' i 1=0
+    u : pred (PrimeIdeal.notContained isPrime)
+    u = Ideal.isSubset i identIsIdent (Ideal.accumulatesTimes i {y = PrimeIdeal.notContained isPrime} t)
+
+quotientIntDomImpliesIdealPrime : IntegralDomain (cosetRing R i) → PrimeIdeal i
+quotientIntDomImpliesIdealPrime intDom = record { isPrime = isPrime ; notContained = Ring.1R R ; notContainedIsNotContained = notCon }
+  where
+    abstract
+      notCon : pred 1R → False
+      notCon 1=0 = IntegralDomain.nontrivial intDom (translate i 1=0)
+      isPrime : {a b : A} → pred (a * b) → (pred a → False) → pred b
+      isPrime {a} {b} predAB !predA = translate' i (IntegralDomain.intDom intDom (translate i predAB) λ t → !predA (translate' i t))
diff --git a/Rings/Ideals/Principal/Lemmas.agda b/Rings/Ideals/Principal/Lemmas.agda
new file mode 100644
index 0000000..9b417be
--- /dev/null
+++ b/Rings/Ideals/Principal/Lemmas.agda
@@ -0,0 +1,20 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Naturals
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+open import Rings.Homomorphisms.Definition
+open import Groups.Homomorphisms.Lemmas
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.Ideals.Principal.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
+
+fieldsArePid : 
diff --git a/Setoids/Functions/Definition.agda b/Setoids/Functions/Definition.agda
index bdd0684..e2c1020 100644
--- a/Setoids/Functions/Definition.agda
+++ b/Setoids/Functions/Definition.agda
@@ -1,10 +1,11 @@
 {-# OPTIONS --safe --warning=error --without-K #-}
 
+open import LogicalFormulae
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import Setoids.Setoids
+open import Setoids.Subset
 
-module Setoids.Functions.Definition where
-
-WellDefined : {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) → Set (a ⊔ c ⊔ d)
-WellDefined {A = A} S T f = {x y : A} → Setoid._∼_ S x y → Setoid._∼_ T (f x) (f y)
+module Setoids.Functions.Definition {a b c d : _} {A : Set a} {B : Set b} where
 
+WellDefined : (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) → Set (a ⊔ c ⊔ d)
+WellDefined S T f = {x y : A} → Setoid._∼_ S x y → Setoid._∼_ T (f x) (f y)
diff --git a/Setoids/Functions/Lemmas.agda b/Setoids/Functions/Lemmas.agda
new file mode 100644
index 0000000..2ff86ab
--- /dev/null
+++ b/Setoids/Functions/Lemmas.agda
@@ -0,0 +1,19 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Setoids.Setoids
+open import Setoids.Subset
+open import Setoids.Functions.Definition
+open import Sets.EquivalenceRelations
+
+module Setoids.Functions.Lemmas {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {f : A → B} (w : WellDefined S T f) where
+
+inverseImagePred : {e : _} → {pred : B → Set e} → (sub : subset T pred) → A → Set (b ⊔ d ⊔ e)
+inverseImagePred {pred = pred} subset a = Sg B (λ b → (pred b) && (Setoid._∼_ T (f a) b))
+
+inverseImageWellDefined : {e : _} {pred : B → Set e} → (sub : subset T pred) → subset S (inverseImagePred sub)
+inverseImageWellDefined sub {x} {y} x=y (b , (predB ,, fx=b)) = f x , (sub (symmetric fx=b) predB ,, symmetric (w x=y))
+  where
+    open Setoid T
+    open Equivalence eq