From 2e5866b81a139c8042d38b3ffba4d9bb754be674 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Fri, 31 Oct 2025 14:27:22 +0100
Subject: [PATCH] Add ideals and quotient rings

---
 CHANGELOG.md                             |  4 ++
 src/Algebra/Construct/Quotient/Ring.agda | 90 ++++++++++++++++++++++++
 src/Algebra/Ideal.agda                   | 30 ++++++++
 3 files changed, 124 insertions(+)
 create mode 100644 src/Algebra/Construct/Quotient/Ring.agda
 create mode 100644 src/Algebra/Ideal.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 69a0890a64..e2dce6eb33 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -81,8 +81,12 @@ New modules
 
 * `Algebra.Cosntruct.Quotient.Group` for the definition of quotient groups.
 
+* `Algebra.Construct.Quotient.Ring` for the definition of quotient rings.
+
 * `Algebra.Construct.Sub.Group` for the definition of subgroups.
 
+* `Algebra.Ideal` for the definition of (two sided) ideals of rings.
+
 * `Algebra.Module.Construct.Sub.Bimodule` for the definition of subbimodules.
 
 * `Algebra.NormalSubgroup` for the definition of normal subgroups.
diff --git a/src/Algebra/Construct/Quotient/Ring.agda b/src/Algebra/Construct/Quotient/Ring.agda
new file mode 100644
index 0000000000..4df610936b
--- /dev/null
+++ b/src/Algebra/Construct/Quotient/Ring.agda
@@ -0,0 +1,90 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Quotient rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Ring; RawRing)
+open import Algebra.Ideal using (Ideal)
+
+module Algebra.Construct.Quotient.Ring {c ℓ} (R : Ring c ℓ) {c′ ℓ′} (I : Ideal R c′ ℓ′) where
+
+open Ring R
+private module I = Ideal I
+open I using (ι; normalSubgroup)
+
+open import Algebra.Construct.Quotient.Group +-group normalSubgroup public
+  using (_≋_; _by_; ≋-refl; ≋-sym; ≋-trans; ≋-isEquivalence; ≈⇒≋; quotientIsGroup; quotientGroup; project; project-surjective)
+  renaming (≋-∙-cong to ≋-+-cong; ≋-⁻¹-cong to ≋‿-‿cong)
+
+open import Algebra.Definitions _≋_
+open import Algebra.Morphism.Structures using (IsRingHomomorphism)
+open import Algebra.Properties.Semiring semiring
+open import Algebra.Properties.Ring R
+open import Algebra.Structures
+open import Function.Definitions using (Surjective)
+open import Level
+open import Relation.Binary.Reasoning.Setoid setoid
+
+≋-*-cong : Congruent₂ _*_
+≋-*-cong {x} {y} {u} {v} (j by ιj+x≈y) (k by ιk+u≈v) = ι j I.*ₗ k I.+ᴹ j I.*ᵣ u I.+ᴹ x I.*ₗ k by begin
+  ι (ι j I.*ₗ k I.+ᴹ j I.*ᵣ u I.+ᴹ x I.*ₗ k) + x * u   ≈⟨ +-congʳ (ι.+ᴹ-homo (ι j I.*ₗ k I.+ᴹ j I.*ᵣ u) (x I.*ₗ k)) ⟩
+  ι (ι j I.*ₗ k I.+ᴹ j I.*ᵣ u) + ι (x I.*ₗ k) + x * u  ≈⟨ +-congʳ (+-congʳ (ι.+ᴹ-homo (ι j I.*ₗ k) (j I.*ᵣ u))) ⟩
+  ι (ι j I.*ₗ k) + ι (j I.*ᵣ u) + ι (x I.*ₗ k) + x * u ≈⟨ +-congʳ (+-cong (+-cong (ι.*ₗ-homo (ι j) k) (ι.*ᵣ-homo u j)) (ι.*ₗ-homo x k)) ⟩
+  ι j * ι k + ι j * u + x * ι k + x * u                ≈⟨ binomial-expansion (ι j) x (ι k) u ⟨
+  (ι j + x) * (ι k + u)                                ≈⟨ *-cong ιj+x≈y ιk+u≈v ⟩
+  y * v                                                ∎
+
+quotientRawRing : RawRing c (c ⊔ ℓ ⊔ c′)
+quotientRawRing = record
+  { Carrier = Carrier
+  ; _≈_ = _≋_
+  ; _+_ = _+_
+  ; _*_ = _*_
+  ; -_ = -_
+  ; 0# = 0#
+  ; 1# = 1#
+  }
+
+quotientIsRing : IsRing _≋_ _+_ _*_ (-_) 0# 1#
+quotientIsRing = record
+  { +-isAbelianGroup = record
+    { isGroup = quotientIsGroup
+    ; comm = λ x y → ≈⇒≋ (+-comm x y)
+    }
+  ; *-cong = ≋-*-cong
+  ; *-assoc = λ x y z → ≈⇒≋ (*-assoc x y z)
+  ; *-identity = record
+    { fst = λ x → ≈⇒≋ (*-identityˡ x)
+    ; snd = λ x → ≈⇒≋ (*-identityʳ x)
+    }
+  ; distrib = record
+    { fst = λ x y z → ≈⇒≋ (distribˡ x y z)
+    ; snd = λ x y z → ≈⇒≋ (distribʳ x y z)
+    }
+  }
+
+quotientRing : Ring c (c ⊔ ℓ ⊔ c′)
+quotientRing = record { isRing = quotientIsRing }
+
+project-isHomomorphism : IsRingHomomorphism rawRing quotientRawRing project
+project-isHomomorphism = record
+  { isSemiringHomomorphism = record
+    { isNearSemiringHomomorphism = record
+      { +-isMonoidHomomorphism = record
+        { isMagmaHomomorphism = record
+          { isRelHomomorphism = record
+            { cong = ≈⇒≋
+            }
+          ; homo = λ _ _ → ≋-refl
+          }
+        ; ε-homo = ≋-refl
+        }
+      ; *-homo = λ _ _ → ≋-refl
+      }
+    ; 1#-homo = ≋-refl
+    }
+  ; -‿homo = λ _ → ≋-refl
+  }
diff --git a/src/Algebra/Ideal.agda b/src/Algebra/Ideal.agda
new file mode 100644
index 0000000000..59527b93bf
--- /dev/null
+++ b/src/Algebra/Ideal.agda
@@ -0,0 +1,30 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Ideals of a ring
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Ring)
+
+module Algebra.Ideal {c ℓ} (R : Ring c ℓ) where
+
+open Ring R using (+-group; +-comm)
+
+open import Algebra.Module.Construct.Sub.Bimodule using (Subbimodule)
+import Algebra.Module.Construct.TensorUnit as TU
+open import Algebra.NormalSubgroup (+-group)
+open import Level
+
+record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
+  field
+    -- a (two sided) ideal is exactly a subbimodule of R considered as a bimodule over itself
+    subbimodule : Subbimodule (TU.bimodule {R = R}) c′ ℓ′
+
+  open Subbimodule subbimodule public
+
+  normalSubgroup : NormalSubgroup c′ ℓ′
+  normalSubgroup = record
+    { isNormal = abelian⇒subgroup-normal +-comm subgroup
+    }