Add principal ideal construction

CHANGELOG.md

@@ -87,6 +87,8 @@ New modules
 
 * `Algebra.Ideal` for the definition of (two sided) ideals of rings.
 
+* `Algebra.Ideal.Construct.Principal` for ideals generated by a single element of a commutative ring.
+
 * `Algebra.Module.Construct.Sub.Bimodule` for the definition of subbimodules.
 
 * `Algebra.NormalSubgroup` for the definition of normal subgroups.

src/Algebra/Ideal/Construct/Principal.agda

@@ -0,0 +1,54 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Ideals generated by a single element of a commutative ring
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (CommutativeRing)
+
+module Algebra.Ideal.Construct.Principal {c ℓ} (R : CommutativeRing c ℓ) where
+
+open import Function.Base using (id; _on_)
+
+open CommutativeRing R
+
+open import Algebra.Ideal ring
+open import Algebra.Properties.CommutativeSemigroup *-commutativeSemigroup
+open import Algebra.Properties.Ring ring
+
+⟨_⟩ : Carrier → Ideal c ℓ
+⟨ a ⟩ = record
+  { subbimodule = record
+    { domain = record
+      { Carrierᴹ = Carrier
+      ; _≈ᴹ_ = _≈_ on a *_
+      ; _+ᴹ_ = _+_
+      ; _*ₗ_ = _*_
+      ; _*ᵣ_ = _*_
+      ; 0ᴹ = 0#
+      ; -ᴹ_ = -_
+      }
+    ; ι = a *_
+    ; ι-monomorphism = record
+      { isBimoduleHomomorphism = record
+        { +ᴹ-isGroupHomomorphism = record
+          { isMonoidHomomorphism = record
+            { isMagmaHomomorphism = record
+              { isRelHomomorphism = record
+                { cong = id
+                }
+              ; homo = distribˡ a
+              }
+            ; ε-homo = zeroʳ a
+            }
+          ; ⁻¹-homo = λ x → sym (-‿distribʳ-* a x)
+          }
+        ; *ₗ-homo = x∙yz≈y∙xz a
+        ; *ᵣ-homo = λ r x → sym (*-assoc a x r)
+        }
+      ; injective = id
+      }
+    }
+  }