Classical.Structures.CommutativeRing

Commutative Rings

This is the Classical.Structures.CommutativeRing module of the Agda Universal Algebra Library.

A commutative ring is an inhabitant of the type Σ[ 𝑨 ∈ Algebra α ρ ] 𝑨 ⊨ Th-CommutativeRing, where Algebra is parameterized by the Sig-Ring type.

This module naturally codifies a commutative ring as an equational extension of Ring, the same way CommutativeMonoid extends Monoid and AbelianGroup extends Group: commutativeRing→ring is a pure theory-reindex (proj₁ on the underlying algebra), and CommutativeRing-Op inherits the additive (_+_, 0R, -_), the multiplicative (_·_, 1R), and all eleven ring laws through it, adding ·-comm-law.

{-# OPTIONS --without-K --exact-split --safe #-}

module Classical.Structures.CommutativeRing where

open import Agda.Primitive                         using () renaming ( Set to Type )


-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Fin.Base                          using ( Fin )
open import Data.Fin.Patterns                      using ( 0F ; 1F ; 2F )
open import Data.Product                           using ( Σ-syntax ; _×_ ; _,_ ; proj₁ ; proj₂ )
open import Level                                  using ( Level ; _⊔_ ; suc )
open import Relation.Binary                        using ( Setoid )
open import Relation.Binary.PropositionalEquality  using ( _≡_ )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Classical.Signatures.Ring            using  ( Sig-Ring )
open import Classical.Structures.Ring            using  ( Ring ; module Ring-Op
                                                        ; opsToBareRing )
open import Classical.Theories.Ring              using  ( +-assoc ; +-idˡ ; +-idʳ
                                                        ; +-invˡ ; +-invʳ ; +-comm
                                                        ; ·-assoc ; ·-idˡ ; ·-idʳ
                                                        ; distribˡ ; distribʳ )
open import Classical.Theories.CommutativeRing   using  ( Eq-CommutativeRing
                                                        ; Th-CommutativeRing
                                                        ; ·-comm )
                                                 renaming  ( +-assoc to +-assocᶜ
                                                           ; +-idˡ to +-idˡᶜ
                                                           ; +-idʳ to +-idʳᶜ
                                                           ; +-invˡ to +-invˡᶜ
                                                           ; +-invʳ to +-invʳᶜ
                                                           ; +-comm to +-commᶜ
                                                           ; ·-assoc to ·-assocᶜ
                                                           ; ·-idˡ to ·-idˡᶜ
                                                           ; ·-idʳ to ·-idʳᶜ
                                                           ; distribˡ to distribˡᶜ
                                                           ; distribʳ to distribʳᶜ )
open import Overture.Terms {𝑆 = Sig-Ring}        using  ( Term ; ℊ )
open import Setoid.Algebras.Basic                using  ( Algebra ; 𝔻[_] ; 𝕌[_] )
open import Setoid.Varieties.EquationalLogic     using  ( _⊧_≈_ )

private variable α ρ : Level

Satisfaction predicate and the CommutativeRing type

infix  _⊨ᶜʳᵍ_
_⊨ᶜʳᵍ_ : (𝑨 : Algebra {𝑆 = Sig-Ring} α ρ) (ℰ : Eq-CommutativeRing → Term (Fin ) × Term (Fin )) → Type (α ⊔ ρ)
𝑨 ⊨ᶜʳᵍ ℰ = ∀ i → 𝑨 ⊧ proj₁ (ℰ i) ≈ proj₂ (ℰ i)

CommutativeRing : (α ρ : Level) → Type (suc α ⊔ suc ρ)
CommutativeRing α ρ = Σ[ 𝑨 ∈ Algebra {𝑆 = Sig-Ring} α ρ ] 𝑨 ⊨ᶜʳᵍ Th-CommutativeRing

The forgetful projection to rings

commutativeRing→ring discards multiplicative commutativity. As with the commutative monoid, the signature is unchanged and the work is re-indexing the satisfaction witness; but here the theory has eleven equations rather than three, so the clause is a table of eleven constructor renamings mapping each of Eq-Ring to its ᶜ-suffixed counterpart in Eq-CommutativeRing. Long, but entirely mechanical: nothing is proved, only relabelled.

commutativeRing→ring : CommutativeRing α ρ → Ring α ρ
commutativeRing→ring (𝑨 , mod) = 𝑨 , λ  { +-assoc   → mod +-assocᶜ
                                        ; +-idˡ     → mod +-idˡᶜ
                                        ; +-idʳ     → mod +-idʳᶜ
                                        ; +-invˡ    → mod +-invˡᶜ
                                        ; +-invʳ    → mod +-invʳᶜ
                                        ; +-comm    → mod +-commᶜ
                                        ; ·-assoc   → mod ·-assocᶜ
                                        ; ·-idˡ     → mod ·-idˡᶜ
                                        ; ·-idʳ     → mod ·-idʳᶜ
                                        ; distribˡ  → mod distribˡᶜ
                                        ; distribʳ  → mod distribʳᶜ }

The CommutativeRing-Op module

CommutativeRing-Op 𝑪 inherits the entire ring interface through the forgetful: two operations with their units and the additive inverse, three congruences, five containment lemmas, and all eleven laws. It adds equations and one new law, ·-comm-law.

The ratio is what makes the idiom worth having. Twenty-four inherited names are re-exported (five operations and constants, three congruences, five containment lemmas and eleven laws) and one law is proved, and that proof is the same three-step shape as comm-law in the commutative monoid and semigroup; the equations ·-comm step between two applications of the containment lemma for the relevant symbol, here interp-node-·.

module CommutativeRing-Op {α ρ : Level} (𝑪 : CommutativeRing α ρ) where
  private 𝑨 = proj₁ 𝑪
  open Setoid 𝔻[ 𝑨 ]

  open Ring-Op (commutativeRing→ring 𝑪) public
    using ( _+_ ; _·_ ; 0R ; 1R ; -_ ; +-cong ; ·-cong ; neg-cong
          ; interp-node-+ ; interp-node-· ; interp-node-0 ; interp-node-1 ; interp-node-neg
          ; +-assoc-law ; +-idˡ-law ; +-idʳ-law ; +-invˡ-law ; +-invʳ-law ; +-comm-law
          ; ·-assoc-law ; ·-idˡ-law ; ·-idʳ-law ; distribˡ-law ; distribʳ-law )

  equations : 𝑨 ⊨ᶜʳᵍ Th-CommutativeRing
  equations = proj₂ 𝑪

  ·-comm-law : ∀ x y → x · y ≈ y · x
  ·-comm-law x y = trans (sym (interp-node-· (ℊ 0F) (ℊ 1F) {η}))
                         (trans (equations ·-comm η) (interp-node-· (ℊ 1F) (ℊ 0F) {η}))
    where η : Fin  → 𝕌[ 𝑨 ]
          η = λ { 0F → x ; 1F → y ; 2F → x }

eqsToCommutativeRing

eqsToCommutativeRing is the largest constructor of the family: two binary operations, two constants, an additive inverse, and twelve propositional laws (the ring's eleven, plus multiplicative commutativity). All twelve obligations discharge exactly as the smaller cases do, by definitional reduction under ≡.setoid A, so the size of the signature costs argument count and nothing else.

eqsToCommutativeRing :
  (A : Type α)
  (_+'_ : A → A → A) (0' : A) (-'_ : A → A) (_*'_ : A → A → A) (1' : A)
  → (+-assoc-≡ : ∀ a b c → (a +' b) +' c ≡ a +' (b +' c))
  → (+-idˡ-≡ : ∀ a → 0' +' a ≡ a) (+-idʳ-≡ : ∀ a → a +' 0' ≡ a)
  → (+-invˡ-≡ : ∀ a → (-' a) +' a ≡ 0') (+-invʳ-≡ : ∀ a → a +' (-' a) ≡ 0')
  → (+-comm-≡ : ∀ a b → a +' b ≡ b +' a)
  → (*-assoc-≡ : ∀ a b c → (a *' b) *' c ≡ a *' (b *' c))
  → (*-idˡ-≡ : ∀ a → 1' *' a ≡ a) (*-idʳ-≡ : ∀ a → a *' 1' ≡ a)
  → (*-comm-≡ : ∀ a b → a *' b ≡ b *' a)
  → (distribˡ-≡ : ∀ a b c → a *' (b +' c) ≡ (a *' b) +' (a *' c))
  → (distribʳ-≡ : ∀ a b c → (b +' c) *' a ≡ (b *' a) +' (c *' a))
  → CommutativeRing α α
eqsToCommutativeRing A _+'_ 0' -'_ _*'_ 1'
  +-assoc-≡ +-idˡ-≡ +-idʳ-≡ +-invˡ-≡ +-invʳ-≡ +-comm-≡ *-assoc-≡ *-idˡ-≡ *-idʳ-≡ *-comm-≡ distribˡ-≡ distribʳ-≡ =
  opsToBareRing A _+'_ 0' -'_ _*'_ 1' , proof
  where
  proof : opsToBareRing A _+'_ 0' -'_ _*'_ 1' ⊨ᶜʳᵍ Th-CommutativeRing
  proof +-assocᶜ  ρ = +-assoc-≡  (ρ 0F) (ρ 1F) (ρ 2F)
  proof +-idˡᶜ    ρ = +-idˡ-≡    (ρ 0F)
  proof +-idʳᶜ    ρ = +-idʳ-≡    (ρ 0F)
  proof +-invˡᶜ   ρ = +-invˡ-≡   (ρ 0F)
  proof +-invʳᶜ   ρ = +-invʳ-≡   (ρ 0F)
  proof +-commᶜ   ρ = +-comm-≡   (ρ 0F) (ρ 1F)
  proof ·-assocᶜ  ρ = *-assoc-≡  (ρ 0F) (ρ 1F) (ρ 2F)
  proof ·-idˡᶜ    ρ = *-idˡ-≡    (ρ 0F)
  proof ·-idʳᶜ    ρ = *-idʳ-≡    (ρ 0F)
  proof ·-comm    ρ = *-comm-≡   (ρ 0F) (ρ 1F)
  proof distribˡᶜ ρ = distribˡ-≡ (ρ 0F) (ρ 1F) (ρ 2F)
  proof distribʳᶜ ρ = distribʳ-≡ (ρ 0F) (ρ 1F) (ρ 2F)