From 29d6a825aff60570387a7bc829589a39470438a6 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 31 Oct 2025 14:27:22 +0100 Subject: [PATCH 1/4] 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 8b481e31e4..b531261602 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -81,8 +81,12 @@ New modules * `Algebra.Construct.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..ccfc531187 --- /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; π; π-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 } + +π-isHomomorphism : IsRingHomomorphism rawRing quotientRawRing π +π-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 + } From b6ef0300d96468e816fd0da30bc4a3f81c1e7049 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 10 Nov 2025 08:57:09 +0100 Subject: [PATCH 2/4] Jiggle comment --- src/Algebra/Ideal.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Ideal.agda b/src/Algebra/Ideal.agda index 59527b93bf..315674aa93 100644 --- a/src/Algebra/Ideal.agda +++ b/src/Algebra/Ideal.agda @@ -17,9 +17,12 @@ import Algebra.Module.Construct.TensorUnit as TU open import Algebra.NormalSubgroup (+-group) open import Level +------------------------------------------------------------------------ +-- Definition + +-- a (two sided) ideal is exactly a subbimodule of R considered as a bimodule over itself 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 From 1edd49caef3ecf06c6edcf3a6cf134eecb5d0eaa Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 10 Nov 2025 08:58:24 +0100 Subject: [PATCH 3/4] Paramaterize Subbimodule rather than TU.bimodule --- src/Algebra/Ideal.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Ideal.agda b/src/Algebra/Ideal.agda index 315674aa93..760284f541 100644 --- a/src/Algebra/Ideal.agda +++ b/src/Algebra/Ideal.agda @@ -23,7 +23,7 @@ open import Level -- a (two sided) ideal is exactly a subbimodule of R considered as a bimodule over itself record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where field - subbimodule : Subbimodule (TU.bimodule {R = R}) c′ ℓ′ + subbimodule : Subbimodule {R = R} TU.bimodule c′ ℓ′ open Subbimodule subbimodule public From e18c5880e2eae0e0eaab85cc28103440cf3ce7de Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 10 Nov 2025 08:59:34 +0100 Subject: [PATCH 4/4] Rearrange imports --- src/Algebra/Construct/Quotient/Ring.agda | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/Algebra/Construct/Quotient/Ring.agda b/src/Algebra/Construct/Quotient/Ring.agda index ccfc531187..e4902f8c57 100644 --- a/src/Algebra/Construct/Quotient/Ring.agda +++ b/src/Algebra/Construct/Quotient/Ring.agda @@ -11,6 +11,11 @@ open import Algebra.Ideal using (Ideal) module Algebra.Construct.Quotient.Ring {c ℓ} (R : Ring c ℓ) {c′ ℓ′} (I : Ideal R c′ ℓ′) where +open import Algebra.Morphism.Structures using (IsRingHomomorphism) +open import Algebra.Properties.Ring R +open import Algebra.Structures +open import Level + open Ring R private module I = Ideal I open I using (ι; normalSubgroup) @@ -18,14 +23,8 @@ open I using (ι; normalSubgroup) open import Algebra.Construct.Quotient.Group +-group normalSubgroup public using (_≋_; _by_; ≋-refl; ≋-sym; ≋-trans; ≋-isEquivalence; ≈⇒≋; quotientIsGroup; quotientGroup; π; π-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₂ _*_