Quotient rings

Author: Taneb

src/Algebra/Construct/Quotient/Ring.agda

@@ -0,0 +1,57 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Quotient rings
+------------------------------------------------------------------------
+
+open import Algebra.Bundles using (Ring)
+open import Algebra.Ideal using (Ideal)
+
+module Algebra.Construct.Quotient.Ring {c ℓ c′ ℓ′} (R : Ring c ℓ) (I : Ideal R c′ ℓ′) where
+
+open Ring R
+open Ideal I
+
+open import Algebra.Construct.Quotient.Group +-group normalSubgroup
+  public
+  using (_≋_; _by_; ≋-refl; ≋-sym; ≋-trans; ≋-isEquivalence; ≈⇒≋; quotientIsGroup; quotientGroup)
+  renaming (≋-∙-cong to ≋-+-cong; ≋-⁻¹-cong to ≋‿-‿cong)
+
+open import Algebra.Definitions _≋_
+open import Algebra.Properties.Ring R
+open import Algebra.Structures
+open import Level
+open import Relation.Binary.Reasoning.Setoid setoid
+
+≋-*-cong : Congruent₂ _*_
+≋-*-cong {x} {y} {u} {v} (j by x-y≈ιj) (k by u-v≈ιk) = j I.*ᵣ u I.+ᴹ y I.*ₗ k by begin
+    x * u - y * v                       ≈⟨ +-congʳ (+-identityʳ (x * u)) ⟨
+    x * u + 0# - y * v                  ≈⟨ +-congʳ (+-congˡ (-‿inverseˡ (y * u))) ⟨
+    x * u + (- (y * u) + y * u) - y * v ≈⟨ +-congʳ (+-assoc (x * u) (- (y * u)) (y * u)) ⟨
+    ((x * u - y * u) + y * u) - y * v   ≈⟨ +-assoc (x * u - y * u) (y * u) (- (y * v)) ⟩
+    (x * u - y * u) + (y * u - y * v)   ≈⟨ +-cong ([y-z]x≈yx-zx u x y) (x[y-z]≈xy-xz y u v) ⟨
+    (x - y) * u + y * (u - v)           ≈⟨ +-cong (*-congʳ x-y≈ιj) (*-congˡ u-v≈ιk) ⟩
+    ι j * u + y * ι k                   ≈⟨ +-cong (ι.*ᵣ-homo u j) (ι.*ₗ-homo y k) ⟨
+    ι (j I.*ᵣ u) + ι (y I.*ₗ k)         ≈⟨ ι.+ᴹ-homo (j I.*ᵣ u) (y I.*ₗ k) ⟨
+    ι (j I.*ᵣ u I.+ᴹ y I.*ₗ k)          ∎
+
+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 }

src/Algebra/Ideal.agda

@@ -0,0 +1,47 @@
+------------------------------------------------------------------------
+-- Ideals of a ring
+--
+-- The Agda standard library
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles
+
+module Algebra.Ideal {c ℓ} (R : Ring c ℓ) where
+
+open Ring R
+
+open import Algebra.Module.Bundles.Raw
+import Algebra.Module.Construct.TensorUnit as TU
+open import Algebra.Module.Morphism.Structures
+open import Algebra.NormalSubgroup (+-group)
+open import Data.Product.Base
+open import Level
+open import Relation.Binary.Reasoning.Setoid setoid
+
+record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
+  field
+    I : RawModule Carrier c′ ℓ′
+    ι : RawModule.Carrierᴹ I → Carrier
+    ι-monomorphism : IsModuleMonomorphism I (TU.rawModule {R = rawRing}) ι
+
+  module I = RawModule I
+  module ι = IsModuleMonomorphism ι-monomorphism
+
+  normalSubgroup : NormalSubgroup c′ ℓ′
+  normalSubgroup = record
+    { N = I.+ᴹ-rawGroup
+    ; ι = ι
+    ; ι-monomorphism = ι.+ᴹ-isGroupMonomorphism
+    ; normal = λ n g → record
+      { fst = n
+      ; snd = begin
+        g + ι n - g     ≈⟨ +-assoc g (ι n) (- g) ⟩
+        g + (ι n - g)   ≈⟨ +-congˡ (+-comm (ι n) (- g)) ⟩
+        g + (- g + ι n) ≈⟨ +-assoc g (- g) (ι n) ⟨
+        g - g + ι n     ≈⟨ +-congʳ (-‿inverseʳ g) ⟩
+        0# + ι n        ≈⟨ +-identityˡ (ι n) ⟩
+        ι n             ∎
+      }
+    }

src/Algebra/Ideal/Construct/Kernel.agda

@@ -0,0 +1,77 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Algebra.Bundles
+open import Algebra.Morphism.Structures
+
+module Algebra.Ideal.Construct.Kernel
+  {c ℓ c′ ℓ′}
+  {R : Ring c ℓ}
+  {S : Ring c′ ℓ′}
+  (ρ : Ring.Carrier R → Ring.Carrier S)
+  (homomorphism : IsRingHomomorphism (Ring.rawRing R) (Ring.rawRing S) ρ)
+  where
+
+private
+  module R = Ring R
+  module S = Ring S
+  module ρ = IsRingHomomorphism homomorphism
+
+open import Algebra.NormalSubgroup.Construct.Kernel {G = R.+-group} {H = S.+-group} ρ ρ.+-isGroupHomomorphism public
+  renaming (_∙ₖ_ to _+ₖ_; εₖ to 0#ₖ; _⁻¹ₖ to -ₖ_)
+
+open import Algebra.Ideal R
+open import Algebra.Module.Bundles.Raw
+open import Function.Base
+open import Level
+open import Relation.Binary.Reasoning.Setoid S.setoid
+
+
+_*ₗₖ_ : R.Carrier → Kernel → Kernel
+r *ₗₖ x = record
+  { element = r R.* X.element
+  ; inKernel = begin
+    ρ (r R.* X.element) ≈⟨ ρ.*-homo r X.element ⟩
+    ρ r S.* ρ X.element ≈⟨ S.*-congˡ X.inKernel ⟩
+    ρ r S.* S.0#        ≈⟨ S.zeroʳ (ρ r) ⟩
+    S.0#                ∎
+  }
+  where module X = Kernel x
+
+_*ᵣₖ_ : Kernel → R.Carrier → Kernel
+x *ᵣₖ r = record
+  { element = X.element R.* r
+  ; inKernel = begin
+    ρ (X.element R.* r) ≈⟨ ρ.*-homo X.element r ⟩
+    ρ X.element S.* ρ r ≈⟨ S.*-congʳ X.inKernel ⟩
+    S.0# S.* ρ r        ≈⟨ S.zeroˡ (ρ r) ⟩
+    S.0#                ∎
+  }
+  where module X = Kernel x
+
+Kernel-rawModule : RawModule R.Carrier (c ⊔ ℓ′) ℓ
+Kernel-rawModule = record
+  { Carrierᴹ = Kernel
+  ; _≈ᴹ_ = R._≈_ on Kernel.element
+  ; _+ᴹ_ = _+ₖ_
+  ; _*ₗ_ = _*ₗₖ_
+  ; _*ᵣ_ = _*ᵣₖ_
+  ; 0ᴹ = 0#ₖ
+  ; -ᴹ_ = -ₖ_
+  }
+  where open RawGroup Kernel-rawGroup
+
+kernelIdeal : Ideal (c ⊔ ℓ′) ℓ
+kernelIdeal = record
+  { I = Kernel-rawModule
+  ; ι = Kernel.element
+  ; ι-monomorphism = record
+    { isModuleHomomorphism = record
+      { isBimoduleHomomorphism = record
+        { +ᴹ-isGroupHomomorphism = IsGroupMonomorphism.isGroupHomomorphism element-isGroupMonomorphism
+        ; *ₗ-homo = λ _ _ → R.refl
+        ; *ᵣ-homo = λ _ _ → R.refl
+        }
+      }
+    ; injective = λ p → p
+    }
+  }