/usr/share/agda-stdlib/Algebra/RingSolver/AlmostCommutativeRing.agda is in agda-stdlib 0.7-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Commutative semirings with some additional structure ("almost"
-- commutative rings), used by the ring solver
------------------------------------------------------------------------
module Algebra.RingSolver.AlmostCommutativeRing where
open import Relation.Binary
open import Algebra
open import Algebra.Structures
open import Algebra.FunctionProperties
import Algebra.Morphism as Morphism
open import Function
open import Level
------------------------------------------------------------------------
-- Definitions
record IsAlmostCommutativeRing
{a ℓ} {A : Set a} (_≈_ : Rel A ℓ)
(_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
field
isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#
-‿cong : -_ Preserves _≈_ ⟶ _≈_
-‿*-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 ( setoid
; +-semigroup; +-monoid; +-commutativeMonoid
; *-semigroup; *-monoid; *-commutativeMonoid
; semiring
)
rawRing : RawRing _
rawRing = record
{ _+_ = _+_
; _*_ = _*_
; -_ = -_
; 0# = 0#
; 1# = 1#
}
------------------------------------------------------------------------
-- Homomorphisms
record _-Raw-AlmostCommutative⟶_
{r₁ r₂ r₃}
(From : RawRing r₁)
(To : AlmostCommutativeRing r₂ r₃) : Set (r₁ ⊔ r₂ ⊔ r₃) where
private
module F = RawRing From
module T = AlmostCommutativeRing To
open Morphism.Definitions 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
-- A homomorphism induces a notion of equivalence on the raw ring.
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 _ _
fromCommutativeRing CR = record
{ isAlmostCommutativeRing = record
{ isCommutativeSemiring = isCommutativeSemiring
; -‿cong = -‿cong
; -‿*-distribˡ = -‿*-distribˡ
; -‿+-comm = ⁻¹-∙-comm
}
}
where
open CommutativeRing CR
import Algebra.Props.Ring as R; open R ring
import Algebra.Props.AbelianGroup as AG; open AG +-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
|