------------------------------------------------------------------------ -- The Agda standard library -- -- Commutative semirings with some additional structure ("almost" -- commutative rings), used by the ring solver ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Algebra.Solver.Ring.AlmostCommutativeRing where open import Algebra open import Algebra.Structures open import Algebra.Definitions import Algebra.Morphism as Morphism import Algebra.Morphism.Definitions as MorphismDefinitions open import Function.Base using (id) open import Level open import Relation.Binary.Core using (Rel) record IsAlmostCommutativeRing {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where field isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1# -‿cong : Congruent₁ _≈_ -_ -‿*-distribˡ : ∀ x y → ((- x) * y) ≈ (- (x * y)) -‿+-comm : ∀ x y → ((- x) + (- y)) ≈ (- (x + y)) open IsCommutativeSemiring isCommutativeSemiring public record AlmostCommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 -_ infixl 7 _*_ infixl 6 _+_ infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ _+_ : Op₂ Carrier _*_ : Op₂ Carrier -_ : Op₁ Carrier 0# : Carrier 1# : Carrier isAlmostCommutativeRing : IsAlmostCommutativeRing _≈_ _+_ _*_ -_ 0# 1# open IsAlmostCommutativeRing isAlmostCommutativeRing public commutativeSemiring : CommutativeSemiring _ _ commutativeSemiring = record { isCommutativeSemiring = isCommutativeSemiring } open CommutativeSemiring commutativeSemiring public using ( +-magma; +-semigroup ; *-magma; *-semigroup; *-commutativeSemigroup ; +-monoid; +-commutativeMonoid ; *-monoid; *-commutativeMonoid ; semiring ) rawRing : RawRing _ _ rawRing = record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; -_ = -_ ; 0# = 0# ; 1# = 1# } ------------------------------------------------------------------------ -- Homomorphisms record _-Raw-AlmostCommutative⟶_ {r₁ r₂ r₃ r₄} (From : RawRing r₁ r₄) (To : AlmostCommutativeRing r₂ r₃) : Set (r₁ ⊔ r₂ ⊔ r₃) where private module F = RawRing From module T = AlmostCommutativeRing To open MorphismDefinitions F.Carrier T.Carrier T._≈_ field ⟦_⟧ : Morphism +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_ *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_ -‿homo : Homomorphic₁ ⟦_⟧ F.-_ T.-_ 0-homo : Homomorphic₀ ⟦_⟧ F.0# T.0# 1-homo : Homomorphic₀ ⟦_⟧ F.1# T.1# -raw-almostCommutative⟶ : ∀ {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂) → AlmostCommutativeRing.rawRing R -Raw-AlmostCommutative⟶ R -raw-almostCommutative⟶ R = record { ⟦_⟧ = id ; +-homo = λ _ _ → refl ; *-homo = λ _ _ → refl ; -‿homo = λ _ → refl ; 0-homo = refl ; 1-homo = refl } where open AlmostCommutativeRing R Induced-equivalence : ∀ {c₁ c₂ ℓ₁ ℓ₂} {Coeff : RawRing c₁ ℓ₁} {R : AlmostCommutativeRing c₂ ℓ₂} → Coeff -Raw-AlmostCommutative⟶ R → Rel (RawRing.Carrier Coeff) ℓ₂ Induced-equivalence {R = R} morphism a b = ⟦ a ⟧ ≈ ⟦ b ⟧ where open AlmostCommutativeRing R open _-Raw-AlmostCommutative⟶_ morphism ------------------------------------------------------------------------ -- Conversions -- Commutative rings are almost commutative rings. fromCommutativeRing : ∀ {r₁ r₂} → CommutativeRing r₁ r₂ → AlmostCommutativeRing r₁ r₂ fromCommutativeRing CR = record { isAlmostCommutativeRing = record { isCommutativeSemiring = isCommutativeSemiring ; -‿cong = -‿cong ; -‿*-distribˡ = λ x y → sym (-‿distribˡ-* x y) ; -‿+-comm = ⁻¹-∙-comm } } where open CommutativeRing CR open import Algebra.Properties.Ring ring open import Algebra.Properties.AbelianGroup +-abelianGroup -- Commutative semirings can be viewed as almost commutative rings by -- using identity as the "almost negation". fromCommutativeSemiring : ∀ {r₁ r₂} → CommutativeSemiring r₁ r₂ → AlmostCommutativeRing _ _ fromCommutativeSemiring CS = record { -_ = id ; isAlmostCommutativeRing = record { isCommutativeSemiring = isCommutativeSemiring ; -‿cong = id ; -‿*-distribˡ = λ _ _ → refl ; -‿+-comm = λ _ _ → refl } } where open CommutativeSemiring CS