Modular arithmetic in terms of ideals

src/Algebra/Construct/Quotient/Group.agda

@@ -0,0 +1,140 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Quotient groups
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles using (Group)
+open import Algebra.NormalSubgroup using (NormalSubgroup)
+
+module Algebra.Construct.Quotient.Group  {c ℓ} (G : Group c ℓ) {c′ ℓ′} (N : NormalSubgroup G c′ ℓ′) where
+
+open Group G
+
+import Algebra.Definitions as AlgDefs
+open import Algebra.Morphism.Structures
+open import Algebra.Properties.Group G
+open import Algebra.Structures using (IsGroup)
+open import Data.Product.Base
+open import Level using (_⊔_)
+open import Relation.Binary.Core using (_⇒_)
+open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Binary.Reasoning.Setoid setoid
+
+open NormalSubgroup N
+
+infix 0 _by_
+
+data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where
+  _by_ : ∀ g → x // y ≈ ι g → x ≋ y
+
+≋-refl : Reflexive _≋_
+≋-refl {x} = N.ε by begin
+  x // x ≈⟨ inverseʳ x ⟩
+  ε      ≈⟨ ι.ε-homo ⟨
+  ι N.ε  ∎
+
+≋-sym : Symmetric _≋_
+≋-sym {x} {y} (g by x//y≈ιg) = g N.⁻¹ by begin
+  y // x      ≈⟨ ⁻¹-anti-homo-// x y ⟨
+  (x // y) ⁻¹ ≈⟨ ⁻¹-cong x//y≈ιg ⟩
+  ι g ⁻¹      ≈⟨ ι.⁻¹-homo g ⟨
+  ι (g N.⁻¹)  ∎
+
+
+≋-trans : Transitive _≋_
+≋-trans {x} {y} {z} (g by x//y≈ιg) (h by y//z≈ιh) = g N.∙ h by begin
+  x // z              ≈⟨ ∙-congʳ (identityʳ x) ⟨
+  x ∙ ε // z          ≈⟨ ∙-congʳ (∙-congˡ (inverseˡ y)) ⟨
+  x ∙ (y \\ y) // z   ≈⟨ ∙-congʳ (assoc x (y ⁻¹) y) ⟨
+  (x // y) ∙ y // z   ≈⟨ assoc (x // y) y (z ⁻¹) ⟩
+  (x // y) ∙ (y // z) ≈⟨ ∙-cong x//y≈ιg y//z≈ιh ⟩
+  ι g ∙ ι h           ≈⟨ ι.∙-homo g h ⟨
+  ι (g N.∙ h)         ∎
+
+≋-isEquivalence : IsEquivalence _≋_
+≋-isEquivalence = record
+  { refl = ≋-refl
+  ; sym = ≋-sym
+  ; trans = ≋-trans
+  }
+
+≈⇒≋ : _≈_ ⇒ _≋_
+≈⇒≋ {x} {y} x≈y = N.ε by begin
+  x // y ≈⟨ x≈y⇒x∙y⁻¹≈ε x≈y ⟩
+  ε      ≈⟨ ι.ε-homo ⟨
+  ι N.ε  ∎
+
+open AlgDefs _≋_
+
+≋-∙-cong : Congruent₂ _∙_
+≋-∙-cong {x} {y} {u} {v} (g by x//y≈ιg) (h by u//v≈ιh) = g N.∙ normal h y .proj₁ by begin
+  x ∙ u // y ∙ v              ≈⟨ ∙-congˡ (⁻¹-anti-homo-∙ y v) ⟩
+  x ∙ u ∙ (v ⁻¹ ∙ y ⁻¹)       ≈⟨ assoc (x ∙ u) (v ⁻¹) (y ⁻¹) ⟨
+  (x ∙ u // v) // y           ≈⟨ ∙-congʳ (assoc x u (v ⁻¹)) ⟩
+  x ∙ (u // v) // y           ≈⟨ ∙-congʳ (∙-congˡ u//v≈ιh) ⟩
+  x ∙ ι h // y                ≈⟨ ∙-congʳ (∙-congˡ (identityˡ (ι h))) ⟨
+  x ∙ (ε ∙ ι h) // y          ≈⟨ ∙-congʳ (∙-congˡ (∙-congʳ (inverseˡ y))) ⟨
+  x ∙ ((y \\ y) ∙ ι h) // y   ≈⟨ ∙-congʳ (∙-congˡ (assoc (y ⁻¹) y (ι h))) ⟩
+  x ∙ (y \\ y ∙ ι h) // y     ≈⟨ ∙-congʳ (assoc x (y ⁻¹) (y ∙ ι h)) ⟨
+  (x // y) ∙ (y ∙ ι h) // y   ≈⟨ assoc (x // y) (y ∙ ι h) (y ⁻¹) ⟩
+  (x // y) ∙ (y ∙ ι h // y)   ≈⟨ ∙-cong x//y≈ιg (proj₂ (normal h y)) ⟩
+  ι g ∙ ι (normal h y .proj₁) ≈⟨ ι.∙-homo g (normal h y .proj₁) ⟨
+  ι (g N.∙ normal h y .proj₁) ∎
+
+≋-⁻¹-cong : Congruent₁ _⁻¹
+≋-⁻¹-cong {x} {y} (g by x//y≈ιg) = normal (g N.⁻¹) (y ⁻¹) .proj₁ by begin
+  x ⁻¹ ∙ y ⁻¹ ⁻¹                      ≈⟨ ∙-congʳ (identityˡ (x ⁻¹)) ⟨
+  (ε ∙ x ⁻¹) ∙ y ⁻¹ ⁻¹                ≈⟨ ∙-congʳ (∙-congʳ (inverseʳ (y ⁻¹))) ⟨
+  ((y ⁻¹ ∙ y ⁻¹ ⁻¹) ∙ x ⁻¹) ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (assoc (y ⁻¹) ((y ⁻¹) ⁻¹) (x ⁻¹)) ⟩
+  y ⁻¹ ∙ (y ⁻¹ ⁻¹ ∙ x ⁻¹) ∙ y ⁻¹ ⁻¹   ≈⟨ ∙-congʳ (∙-congˡ (⁻¹-anti-homo-∙ x (y ⁻¹))) ⟨
+  y ⁻¹ ∙ (x ∙ y ⁻¹) ⁻¹ ∙ y ⁻¹ ⁻¹      ≈⟨ ∙-congʳ (∙-congˡ (⁻¹-cong x//y≈ιg)) ⟩
+  y ⁻¹ ∙ ι g ⁻¹ ∙ y ⁻¹ ⁻¹             ≈⟨ ∙-congʳ (∙-congˡ (ι.⁻¹-homo g)) ⟨
+  y ⁻¹ ∙ ι (g N.⁻¹) ∙ y ⁻¹ ⁻¹         ≈⟨ proj₂ (normal (g N.⁻¹) (y ⁻¹)) ⟩
+  ι (normal (g N.⁻¹) (y ⁻¹) .proj₁)   ∎
+
+quotientIsGroup : IsGroup _≋_ _∙_ ε _⁻¹
+quotientIsGroup = record
+  { isMonoid = record
+    { isSemigroup = record
+      { isMagma = record
+        { isEquivalence = ≋-isEquivalence
+        ; ∙-cong = ≋-∙-cong
+        }
+      ; assoc = λ x y z → ≈⇒≋ (assoc x y z)
+      }
+    ; identity = record
+      { fst = λ x → ≈⇒≋ (identityˡ x)
+      ; snd = λ x → ≈⇒≋ (identityʳ x)
+      }
+    }
+  ; inverse = record
+    { fst = λ x → ≈⇒≋ (inverseˡ x)
+    ; snd = λ x → ≈⇒≋ (inverseʳ x)
+    }
+  ; ⁻¹-cong = ≋-⁻¹-cong
+  }
+
+quotientGroup : Group c (c ⊔ ℓ ⊔ c′)
+quotientGroup = record { isGroup = quotientIsGroup }
+
+η : Group.Carrier G → Group.Carrier quotientGroup
+η x = x -- because we do all the work in the relation
+
+η-isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) η
+η-isHomomorphism = record
+  { isMonoidHomomorphism = record
+    { isMagmaHomomorphism = record
+      { isRelHomomorphism = record
+        { cong = ≈⇒≋
+        }
+      ; homo = λ _ _ → ≋-refl
+      }
+    ; ε-homo = ≋-refl
+    }
+  ; ⁻¹-homo = λ _ → ≋-refl
+  }
+

src/Algebra/Construct/Quotient/Ring.agda

@@ -0,0 +1,69 @@
+------------------------------------------------------------------------
+-- 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
+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)          ∎
+
+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 }

src/Algebra/Construct/Quotient/Ring/Properties/ChineseRemainderTheorem.agda

@@ -0,0 +1,109 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The Chinese Remainder Theorem for arbitrary rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+open import Algebra.Bundles
+
+module Algebra.Construct.Quotient.Ring.Properties.ChineseRemainderTheorem {c ℓ} (R : Ring c ℓ) where
+
+open Ring R
+
+import Algebra.Construct.DirectProduct as DP
+open import Algebra.Construct.Quotient.Ring as QR using (quotientRawRing)
+open import Algebra.Ideal R
+open import Algebra.Ideal.Coprimality R using (Coprime)
+open import Algebra.Ideal.Construct.Intersection R
+open import Algebra.Morphism.Structures
+open import Algebra.Properties.Ring R
+open import Data.Product.Base
+open import Relation.Binary.Reasoning.Setoid setoid
+
+module _
+  {c₁ c₂ ℓ₁ ℓ₂}
+  (I : Ideal c₁ ℓ₁) (J : Ideal c₂ ℓ₂)
+  where
+
+  private
+    module I = Ideal I
+    module J = Ideal J
+
+  CRT : Coprime I J → IsRingIsomorphism (quotientRawRing R (I ∩ J)) (DP.rawRing (quotientRawRing R I) (quotientRawRing R J)) λ x → x , x
+  CRT ((m , n) , m+n≈1) = record
+    { isRingMonomorphism = record
+      { isRingHomomorphism = record
+        { isSemiringHomomorphism = record
+          { isNearSemiringHomomorphism = record
+            { +-isMonoidHomomorphism = record
+              { isMagmaHomomorphism = record
+                { isRelHomomorphism = record
+                  { cong = λ { (t R/I∩J.by p) → (ICarrier.a t R/I.by p) , (ICarrier.b t R/J.by trans p (ICarrier.a≈b t)) }
+                  }
+                ; homo = λ x y → R/I.≋-refl , R/J.≋-refl
+                }
+              ; ε-homo = R/I.≋-refl , R/J.≋-refl
+              }
+            ; *-homo = λ x y → R/I.≋-refl , R/J.≋-refl
+            }
+          ; 1#-homo = R/I.≋-refl , R/J.≋-refl
+          }
+        ; -‿homo = λ x → R/I.≋-refl , R/J.≋-refl
+        }
+        ; injective = λ {((i R/I.by p) , (j R/J.by q)) → record { a≈b = trans (sym p) q } R/I∩J.by p}
+      }
+    ; surjective = λ (a₁ , a₂) → a₁ * J.ι n + a₂ * I.ι m , λ {z} → λ
+      { (record {a = a; b = b; a≈b = a≈b}  R/I∩J.by p) → record
+        { fst = a I.I.+ᴹ (a₂ - a₁) I.I.*ₗ m R/I.by begin
+          -- introduce a coprimality term
+          z - a₁                   ≈⟨ +-congˡ (-‿cong (*-identityʳ a₁)) ⟨
+          z - a₁ * 1#              ≈⟨ +-congˡ (-‿cong (*-congˡ m+n≈1)) ⟨
+          -- lots and lots of rearrangement
+          z - a₁ * (I.ι m + J.ι n)                                          ≈⟨ +-congˡ (-‿cong (distribˡ a₁ (I.ι m) (J.ι n))) ⟩
+          z - (a₁ * I.ι m + a₁ * J.ι n)                                     ≈⟨ +-congˡ (-‿cong (+-comm (a₁ * I.ι m) (a₁ * J.ι n))) ⟩
+          z - (a₁ * J.ι n + a₁ * I.ι m)                                     ≈⟨ +-congˡ (-‿cong (+-congʳ (+-identityʳ (a₁ * J.ι n)))) ⟨
+          z - (a₁ * J.ι n + 0# + a₁ * I.ι m)                                ≈⟨ +-congˡ (-‿cong (+-congʳ (+-congˡ (-‿inverseʳ (a₂ * I.ι m))))) ⟨
+          z - (a₁ * J.ι n + (a₂ * I.ι m - a₂ * I.ι m) + a₁ * I.ι m)         ≈⟨ +-congˡ (-‿cong (+-congʳ (+-assoc _ _ _))) ⟨
+          z - (a₁ * J.ι n + a₂ * I.ι m - a₂ * I.ι m + a₁ * I.ι m)           ≈⟨ +-congˡ (-‿cong (+-assoc _ _ _)) ⟩
+          z - (a₁ * J.ι n + a₂ * I.ι m + (- (a₂ * I.ι m) + a₁ * I.ι m))     ≈⟨ +-congˡ (-‿+-comm _ _) ⟨
+          z + (- (a₁ * J.ι n + a₂ * I.ι m) - (- (a₂ * I.ι m) + a₁ * I.ι m)) ≈⟨ +-assoc z _ _ ⟨
+          z - (a₁ * J.ι n + a₂ * I.ι m) - (- (a₂ * I.ι m) + a₁ * I.ι m)     ≈⟨ +-congˡ (-‿+-comm _ _) ⟨
+          z - (a₁ * J.ι n + a₂ * I.ι m) + (- - (a₂ * I.ι m) - a₁ * I.ι m)   ≈⟨ +-congˡ (+-congʳ (-‿involutive _)) ⟩
+          z - (a₁ * J.ι n + a₂ * I.ι m) + (a₂ * I.ι m - a₁ * I.ι m)         ≈⟨ +-congˡ ([y-z]x≈yx-zx _ _ _) ⟨
+          -- substitute z-t
+          z - (a₁ * J.ι n + a₂ * I.ι m) + (a₂ - a₁) * I.ι m ≈⟨ +-congʳ p ⟩
+          -- show we're in I
+          I.ι a + (a₂ - a₁) * I.ι m         ≈⟨ +-congˡ (I.ι.*ₗ-homo (a₂ - a₁) m) ⟨
+          I.ι a + I.ι ((a₂ - a₁) I.I.*ₗ m)  ≈⟨ I.ι.+ᴹ-homo a _ ⟨
+          I.ι (a I.I.+ᴹ (a₂ - a₁) I.I.*ₗ m) ∎
+        ; snd = b J.I.+ᴹ (a₁ - a₂) J.I.*ₗ n R/J.by begin
+          -- introduce a coprimality term
+          z - a₂                   ≈⟨ +-congˡ (-‿cong (*-identityʳ a₂)) ⟨
+          z - a₂ * 1#              ≈⟨ +-congˡ (-‿cong (*-congˡ m+n≈1)) ⟨
+          -- lots and lots of rearrangement
+          z - a₂ * (I.ι m + J.ι n)                                          ≈⟨ +-congˡ (-‿cong (distribˡ a₂ (I.ι m) (J.ι n))) ⟩
+          z - (a₂ * I.ι m + a₂ * J.ι n)                                     ≈⟨ +-congˡ (-‿cong (+-congʳ (+-identityʳ (a₂ * I.ι m)))) ⟨
+          z - (a₂ * I.ι m + 0# + a₂ * J.ι n)                                ≈⟨ +-congˡ (-‿cong (+-congʳ (+-congˡ (-‿inverseʳ (a₁ * J.ι n))))) ⟨
+          z - (a₂ * I.ι m + (a₁ * J.ι n - a₁ * J.ι n) + a₂ * J.ι n)         ≈⟨ +-congˡ (-‿cong (+-congʳ (+-assoc (a₂ * I.ι m) (a₁ * J.ι n) _))) ⟨
+          z - (a₂ * I.ι m + a₁ * J.ι n - a₁ * J.ι n + a₂ * J.ι n)           ≈⟨ +-congˡ (-‿cong (+-assoc (a₂ * I.ι m + a₁ * J.ι n) (- (a₁ * J.ι n)) _)) ⟩
+          z - (a₂ * I.ι m + a₁ * J.ι n + (- (a₁ * J.ι n) + a₂ * J.ι n))     ≈⟨ +-congˡ (-‿+-comm (a₂ * I.ι m + a₁ * J.ι n) (- (a₁ * J.ι n) + a₂ * J.ι n)) ⟨
+          z + (- (a₂ * I.ι m + a₁ * J.ι n) - (- (a₁ * J.ι n) + a₂ * J.ι n)) ≈⟨ +-assoc z (- (a₂ * I.ι m + a₁ * J.ι n)) (- (- (a₁ * J.ι n) + a₂ * J.ι n)) ⟨
+          z - (a₂ * I.ι m + a₁ * J.ι n) - (- (a₁ * J.ι n) + a₂ * J.ι n)     ≈⟨ +-cong (+-congˡ (-‿cong (+-comm _ _))) (-‿cong (+-congˡ (-‿involutive _))) ⟨
+          z - (a₁ * J.ι n + a₂ * I.ι m) - (- (a₁ * J.ι n) - - (a₂ * J.ι n)) ≈⟨ +-congˡ (-‿cong (-‿+-comm (a₁ * J.ι n) (- (a₂ * J.ι n)))) ⟩
+          z - (a₁ * J.ι n + a₂ * I.ι m) - - (a₁ * J.ι n - a₂ * J.ι n)       ≈⟨ +-congˡ (-‿involutive (a₁ * J.ι n - a₂ * J.ι n)) ⟩
+          z - (a₁ * J.ι n + a₂ * I.ι m) + (a₁ * J.ι n - a₂ * J.ι n)         ≈⟨ +-congˡ ([y-z]x≈yx-zx (J.ι n) a₁ a₂) ⟨
+          -- substitute z-t
+          z - (a₁ * J.ι n + a₂ * I.ι m) + (a₁ - a₂) * J.ι n ≈⟨ +-congʳ (trans p a≈b) ⟩
+          -- show we're in I
+          J.ι b + (a₁ - a₂) * J.ι n          ≈⟨ +-congˡ (J.ι.*ₗ-homo (a₁ - a₂) n) ⟨
+          J.ι b + J.ι ((a₁ - a₂) J.I.*ₗ n)   ≈⟨ J.ι.+ᴹ-homo b ((a₁ - a₂) J.I.*ₗ n) ⟨
+          J.ι (b J.I.+ᴹ  (a₁ - a₂) J.I.*ₗ n) ∎
+        }
+      }
+    }
+    where
+      module R/I = QR R I
+      module R/J = QR R J
+      module R/I∩J = QR R (I ∩ J)

src/Algebra/Ideal.agda

@@ -0,0 +1,47 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Ideals of a ring
+------------------------------------------------------------------------
+
+{-# 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             ∎
+      }
+    }