Principal ideals

Author: Taneb

src/Algebra/Ideal/Construct/Principal.agda

@@ -0,0 +1,57 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Ideals generated by a single element
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles
+
+module Algebra.Ideal.Construct.Principal {c ℓ} (R : CommutativeRing c ℓ) where
+
+open CommutativeRing R
+
+open import Algebra.Ideal ring
+open import Algebra.Properties.Ring ring
+open import Function.Base
+open import Relation.Binary.Reasoning.Setoid setoid
+
+⟨_⟩ : Carrier → Ideal c ℓ
+⟨ a ⟩ = record
+  { I = record
+    { Carrierᴹ = Carrier
+    ; _≈ᴹ_ = _≈_ on _* a
+    ; _+ᴹ_ = _+_
+    ; _*ₗ_ = _*_
+    ; _*ᵣ_ = _*_
+    ; 0ᴹ = 0#
+    ; -ᴹ_ = -_
+    }
+  ; ι = _* a
+  ; ι-monomorphism = record
+    { isModuleHomomorphism = record
+      { isBimoduleHomomorphism = record
+        { +ᴹ-isGroupHomomorphism = record
+          { isMonoidHomomorphism = record
+            { isMagmaHomomorphism = record
+              { isRelHomomorphism = record
+                { cong = λ p → p
+                }
+              ; homo = distribʳ a
+              }
+            ; ε-homo = zeroˡ a
+            }
+          ; ⁻¹-homo = λ x → sym (-‿distribˡ-* x a)
+          }
+        ; *ₗ-homo = λ r x → *-assoc r x a
+        ; *ᵣ-homo = λ r x → begin
+          x * r * a   ≈⟨ *-assoc x r a ⟩
+          x * (r * a) ≈⟨ *-congˡ (*-comm r {!a!}) ⟩
+          x * (a * r) ≈⟨ *-assoc x a r ⟨
+          x * a * r   ∎
+        }
+      }
+    ; injective = λ p → p
+    }
+  }