diff --git a/CHANGELOG.md b/CHANGELOG.md index 3bd1282042..9bf1538b4a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -322,6 +322,22 @@ Non-backwards compatible changes * The contents of `Function.Strict` is now re-exported by `Function`. +### Changes to ring structures + +* Several ring-like structures now have the multiplicative structure defined by + its laws rather than as a substructure, to avoid repeated proofs that the + underlying relation is an equivalence. These are: + * `IsNearSemiring` + * `IsSemiringWithoutOne` + * `IsSemiringWithoutAnnihilatingZero` + * `IsRing` +* To aid with migration, structures matching the old style ones have been added + to `Algebra.Structures.Biased`, with conversionFunctions: + * `IsNearSemiring*` and `isNearSemiring*` + * `IsSemiringWithoutOne*` and `isSemiringWithoutOne*` + * `IsSemiringWithoutAnnihilatingZero*` and `isSemiringWithoutAnnihilatingZero*` + * `IsRing*` and `isRing*` + ### Other * The first two arguments of `m≡n⇒m-n≡0` (now `i≡j⇒i-j≡0`) in `Data.Integer.Base` diff --git a/src/Algebra/Construct/DirectProduct.agda b/src/Algebra/Construct/DirectProduct.agda index 145bd066b7..b2f63c7925 100644 --- a/src/Algebra/Construct/DirectProduct.agda +++ b/src/Algebra/Construct/DirectProduct.agda @@ -172,7 +172,10 @@ semiringWithoutAnnihilatingZero R S = record { +-isCommutativeMonoid = CommutativeMonoid.isCommutativeMonoid (commutativeMonoid R.+-commutativeMonoid S.+-commutativeMonoid) - ; *-isMonoid = Monoid.isMonoid (monoid R.*-monoid S.*-monoid) + ; *-cong = zip R.*-cong S.*-cong + ; *-assoc = λ x y z → (R.*-assoc , S.*-assoc) <*> x <*> y <*> z + ; *-identity = (R.*-identityˡ , S.*-identityˡ <*>_) + , (R.*-identityʳ , S.*-identityʳ <*>_) ; distrib = (λ x y z → (R.distribˡ , S.distribˡ) <*> x <*> y <*> z) , (λ x y z → (R.distribʳ , S.distribʳ) <*> x <*> y <*> z) } @@ -208,7 +211,9 @@ ring R S = record { -_ = uncurry (λ x y → R.-_ x , S.-_ y) ; isRing = record { +-isAbelianGroup = AbelianGroup.isAbelianGroup A - ; *-isMonoid = Semiring.*-isMonoid Semi + ; *-cong = Semiring.*-cong Semi + ; *-assoc = Semiring.*-assoc Semi + ; *-identity = Semiring.*-identity Semi ; distrib = Semiring.distrib Semi ; zero = Semiring.zero Semi } diff --git a/src/Algebra/Construct/Subst/Equality.agda b/src/Algebra/Construct/Subst/Equality.agda index a8dda52c87..0998888152 100644 --- a/src/Algebra/Construct/Subst/Equality.agda +++ b/src/Algebra/Construct/Subst/Equality.agda @@ -126,9 +126,10 @@ isAbelianGroup S = record isNearSemiring : ∀ {+ * 0#} → IsNearSemiring ≈₁ + * 0# → IsNearSemiring ≈₂ + * 0# -isNearSemiring S = record +isNearSemiring {* = *} S = record { +-isMonoid = isMonoid S.+-isMonoid - ; *-isSemigroup = isSemigroup S.*-isSemigroup + ; *-cong = cong₂ S.*-cong + ; *-assoc = assoc {*} S.*-assoc ; distribʳ = λ x y z → to (S.distribʳ x y z) ; zeroˡ = to ∘ S.zeroˡ } where module S = IsNearSemiring S @@ -137,7 +138,8 @@ isSemiringWithoutOne : ∀ {+ * 0#} → IsSemiringWithoutOne ≈₁ + * 0# → IsSemiringWithoutOne ≈₂ + * 0# isSemiringWithoutOne {+} {*} S = record { +-isCommutativeMonoid = isCommutativeMonoid S.+-isCommutativeMonoid - ; *-isSemigroup = isSemigroup S.*-isSemigroup + ; *-cong = cong₂ S.*-cong + ; *-assoc = assoc {*} S.*-assoc ; distrib = distrib {*} {+} S.distrib ; zero = Prod.map (to ∘_) (to ∘_) S.zero } where module S = IsSemiringWithoutOne S diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda index 3c8717a217..1aa1be5945 100644 --- a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda +++ b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda @@ -136,7 +136,9 @@ open DistribLatticeProperties distributiveLattice public ∨-∧-isSemiring = record { isSemiringWithoutAnnihilatingZero = record { +-isCommutativeMonoid = ∨-⊥-isCommutativeMonoid - ; *-isMonoid = ∧-⊤-isMonoid + ; *-cong = ∧-cong + ; *-assoc = ∧-assoc + ; *-identity = ∧-identity ; distrib = ∧-∨-distrib } ; zero = ∧-zero @@ -146,7 +148,9 @@ open DistribLatticeProperties distributiveLattice public ∧-∨-isSemiring = record { isSemiringWithoutAnnihilatingZero = record { +-isCommutativeMonoid = ∧-⊤-isCommutativeMonoid - ; *-isMonoid = ∨-⊥-isMonoid + ; *-cong = ∨-cong + ; *-assoc = ∨-assoc + ; *-identity = ∨-identity ; distrib = ∨-∧-distrib } ; zero = ∨-zero @@ -514,7 +518,9 @@ module XorRing ⊕-∧-isRing : IsRing _⊕_ _∧_ id ⊥ ⊤ ⊕-∧-isRing = record { +-isAbelianGroup = ⊕-⊥-isAbelianGroup - ; *-isMonoid = ∧-⊤-isMonoid + ; *-cong = ∧-cong + ; *-assoc = ∧-assoc + ; *-identity = ∧-identity ; distrib = ∧-distrib-⊕ ; zero = ∧-zero } diff --git a/src/Algebra/Morphism/RingMonomorphism.agda b/src/Algebra/Morphism/RingMonomorphism.agda index 8cb93067c0..4e26fe02f1 100644 --- a/src/Algebra/Morphism/RingMonomorphism.agda +++ b/src/Algebra/Morphism/RingMonomorphism.agda @@ -146,7 +146,9 @@ module _ (+-isGroup : IsGroup _≈₂_ _⊕_ 0#₂ ⊝_) isRing : IsRing _≈₂_ _⊕_ _⊛_ ⊝_ 0#₂ 1#₂ → IsRing _≈₁_ _+_ _*_ -_ 0# 1# isRing isRing = record { +-isAbelianGroup = isAbelianGroup R.+-isAbelianGroup - ; *-isMonoid = *-isMonoid R.*-isMonoid + ; *-cong = *-cong R.*-isMagma + ; *-assoc = *-assoc R.*-isMagma R.*-assoc + ; *-identity = *-identity R.*-isMagma R.*-identity ; distrib = distrib R.+-isGroup R.*-isMagma R.distrib ; zero = zero R.+-isGroup R.*-isMagma R.zero } where module R = IsRing isRing diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 1c0dd7a93a..631f24a45d 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -260,7 +260,8 @@ record IsAbelianGroup (∙ : Op₂ A) record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where field +-isMonoid : IsMonoid + 0# - *-isSemigroup : IsSemigroup * + *-cong : Congruent₂ * + *-assoc : Associative * distribʳ : * DistributesOverʳ + zeroˡ : LeftZero 0# * @@ -278,25 +279,36 @@ record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where ; isSemigroup to +-isSemigroup ) - open IsSemigroup *-isSemigroup public + *-isMagma : IsMagma * + *-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = *-cong + } + + *-isSemigroup : IsSemigroup * + *-isSemigroup = record + { isMagma = *-isMagma + ; assoc = *-assoc + } + + open IsMagma *-isMagma public using () renaming - ( assoc to *-assoc - ; ∙-cong to *-cong - ; ∙-congˡ to *-congˡ + ( ∙-congˡ to *-congˡ ; ∙-congʳ to *-congʳ - ; isMagma to *-isMagma ) record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where field +-isCommutativeMonoid : IsCommutativeMonoid + 0# - *-isSemigroup : IsSemigroup * + *-cong : Congruent₂ * + *-assoc : Associative * distrib : * DistributesOver + zero : Zero 0# * - open IsCommutativeMonoid +-isCommutativeMonoid public using () + open IsCommutativeMonoid +-isCommutativeMonoid public + using (isEquivalence) renaming ( comm to +-comm ; isMonoid to +-isMonoid @@ -304,6 +316,25 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where ; isCommutativeSemigroup to +-isCommutativeSemigroup ) + *-isMagma : IsMagma * + *-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = *-cong + } + + *-isSemigroup : IsSemigroup * + *-isSemigroup = record + { isMagma = *-isMagma + ; assoc = *-assoc + } + + open IsMagma *-isMagma public + using () + renaming + ( ∙-congˡ to *-congˡ + ; ∙-congʳ to *-congʳ + ) + zeroˡ : LeftZero 0# * zeroˡ = proj₁ zero @@ -313,15 +344,12 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where isNearSemiring : IsNearSemiring + * 0# isNearSemiring = record { +-isMonoid = +-isMonoid - ; *-isSemigroup = *-isSemigroup + ; *-cong = *-cong + ; *-assoc = *-assoc ; distribʳ = proj₂ distrib ; zeroˡ = zeroˡ } - open IsNearSemiring isNearSemiring public - hiding (+-isMonoid; zeroˡ; *-isSemigroup) - - record IsCommutativeSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where field @@ -349,7 +377,9 @@ record IsSemiringWithoutAnnihilatingZero (+ * : Op₂ A) -- Note that these structures do have an additive unit, but this -- unit does not necessarily annihilate multiplication. +-isCommutativeMonoid : IsCommutativeMonoid + 0# - *-isMonoid : IsMonoid * 1# + *-cong : Congruent₂ * + *-assoc : Associative * + *-identity : Identity 1# * distrib : * DistributesOver + distribˡ : * DistributesOverˡ + @@ -376,18 +406,31 @@ record IsSemiringWithoutAnnihilatingZero (+ * : Op₂ A) ; isCommutativeSemigroup to +-isCommutativeSemigroup ) + *-isMagma : IsMagma * + *-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = *-cong + } + + *-isSemigroup : IsSemigroup * + *-isSemigroup = record + { isMagma = *-isMagma + ; assoc = *-assoc + } + + *-isMonoid : IsMonoid * 1# + *-isMonoid = record + { isSemigroup = *-isSemigroup + ; identity = *-identity + } + open IsMonoid *-isMonoid public using () renaming - ( assoc to *-assoc - ; ∙-cong to *-cong - ; ∙-congˡ to *-congˡ + ( ∙-congˡ to *-congˡ ; ∙-congʳ to *-congʳ - ; identity to *-identity ; identityˡ to *-identityˡ ; identityʳ to *-identityʳ - ; isMagma to *-isMagma - ; isSemigroup to *-isSemigroup ) @@ -403,7 +446,8 @@ record IsSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where isSemiringWithoutOne : IsSemiringWithoutOne + * 0# isSemiringWithoutOne = record { +-isCommutativeMonoid = +-isCommutativeMonoid - ; *-isSemigroup = *-isSemigroup + ; *-cong = *-cong + ; *-assoc = *-assoc ; distrib = distrib ; zero = zero } @@ -459,7 +503,9 @@ record IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where field +-isAbelianGroup : IsAbelianGroup + 0# -_ - *-isMonoid : IsMonoid * 1# + *-cong : Congruent₂ * + *-assoc : Associative * + *-identity : Identity 1# * distrib : * DistributesOver + zero : Zero 0# * @@ -489,18 +535,31 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where ; isGroup to +-isGroup ) + *-isMagma : IsMagma * + *-isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = *-cong + } + + *-isSemigroup : IsSemigroup * + *-isSemigroup = record + { isMagma = *-isMagma + ; assoc = *-assoc + } + + *-isMonoid : IsMonoid * 1# + *-isMonoid = record + { isSemigroup = *-isSemigroup + ; identity = *-identity + } + open IsMonoid *-isMonoid public using () renaming - ( assoc to *-assoc - ; ∙-cong to *-cong - ; ∙-congˡ to *-congˡ + ( ∙-congˡ to *-congˡ ; ∙-congʳ to *-congʳ - ; identity to *-identity ; identityˡ to *-identityˡ ; identityʳ to *-identityʳ - ; isMagma to *-isMagma - ; isSemigroup to *-isSemigroup ) zeroˡ : LeftZero 0# * @@ -513,7 +572,9 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where : IsSemiringWithoutAnnihilatingZero + * 0# 1# isSemiringWithoutAnnihilatingZero = record { +-isCommutativeMonoid = +-isCommutativeMonoid - ; *-isMonoid = *-isMonoid + ; *-cong = *-cong + ; *-assoc = *-assoc + ; *-identity = *-identity ; distrib = distrib } diff --git a/src/Algebra/Structures/Biased.agda b/src/Algebra/Structures/Biased.agda index 6f4b092fdb..dfe0f7fd71 100644 --- a/src/Algebra/Structures/Biased.agda +++ b/src/Algebra/Structures/Biased.agda @@ -61,6 +61,70 @@ record IsCommutativeMonoidʳ (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where open IsCommutativeMonoidʳ public using () renaming (isCommutativeMonoid to isCommutativeMonoidʳ) +------------------------------------------------------------------------ +-- IsSemiringWithoutOne + +record IsSemiringWithoutOne* (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where + field + +-isCommutativeMonoid : IsCommutativeMonoid + 0# + *-isSemigroup : IsSemigroup * + distrib : * DistributesOver + + zero : Zero 0# * + + isSemiringWithoutOne : IsSemiringWithoutOne + * 0# + isSemiringWithoutOne = record + { +-isCommutativeMonoid = +-isCommutativeMonoid + ; *-cong = ∙-cong + ; *-assoc = assoc + ; distrib = distrib + ; zero = zero + } where open IsSemigroup *-isSemigroup + +open IsSemiringWithoutOne* public + using () renaming (isSemiringWithoutOne to isSemiringWithoutOne*) + +------------------------------------------------------------------------ +-- IsNearSemiring + +record IsNearSemiring* (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where + field + +-isMonoid : IsMonoid + 0# + *-isSemigroup : IsSemigroup * + distribʳ : * DistributesOverʳ + + zeroˡ : LeftZero 0# * + + isNearSemiring : IsNearSemiring + * 0# + isNearSemiring = record + { +-isMonoid = +-isMonoid + ; *-cong = ∙-cong + ; *-assoc = assoc + ; distribʳ = distribʳ + ; zeroˡ = zeroˡ + } where open IsSemigroup *-isSemigroup + +open IsNearSemiring* public + using () renaming (isNearSemiring to isNearSemiring*) + +------------------------------------------------------------------------ +-- IsSemiringWithoutAnnihilatingZero + +record IsSemiringWithoutAnnihilatingZero* (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where + field + +-isCommutativeMonoid : IsCommutativeMonoid + 0# + *-isMonoid : IsMonoid * 1# + distrib : * DistributesOver + + + isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# + isSemiringWithoutAnnihilatingZero = record + { +-isCommutativeMonoid = +-isCommutativeMonoid + ; *-cong = ∙-cong + ; *-assoc = assoc + ; *-identity = identity + ; distrib = distrib + } where open IsMonoid *-isMonoid + +open IsSemiringWithoutAnnihilatingZero* public + using () renaming (isSemiringWithoutAnnihilatingZero to isSemiringWithoutAnnihilatingZero*) ------------------------------------------------------------------------ -- IsCommutativeSemiring @@ -77,7 +141,9 @@ record IsCommutativeSemiringˡ (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) whe { isSemiring = record { isSemiringWithoutAnnihilatingZero = record { +-isCommutativeMonoid = +-isCommutativeMonoid - ; *-isMonoid = *.isMonoid + ; *-cong = *.∙-cong + ; *-assoc = *.assoc + ; *-identity = *.identity ; distrib = comm+distrʳ⇒distr +.setoid +.∙-cong *.comm distribʳ } ; zero = comm+zeˡ⇒ze +.setoid *.comm zeroˡ @@ -104,7 +170,9 @@ record IsCommutativeSemiringʳ (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) whe { isSemiring = record { isSemiringWithoutAnnihilatingZero = record { +-isCommutativeMonoid = +-isCommutativeMonoid - ; *-isMonoid = *.isMonoid + ; *-cong = *.∙-cong + ; *-assoc = *.assoc + ; *-identity = *.identity ; distrib = comm+distrˡ⇒distr +.setoid +.∙-cong *.comm distribˡ } ; zero = comm+zeʳ⇒ze +.setoid *.comm zeroʳ @@ -150,10 +218,32 @@ record IsRingWithoutAnnihilatingZero (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) isRing : IsRing + * -_ 0# 1# isRing = record { +-isAbelianGroup = +-isAbelianGroup - ; *-isMonoid = *-isMonoid + ; *-cong = *.∙-cong + ; *-assoc = *.assoc + ; *-identity = *.identity ; distrib = distrib ; zero = zero } open IsRingWithoutAnnihilatingZero public using () renaming (isRing to isRingWithoutAnnihilatingZero) + +record IsRing* (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where + field + +-isAbelianGroup : IsAbelianGroup + 0# -_ + *-isMonoid : IsMonoid * 1# + distrib : * DistributesOver + + zero : Zero 0# * + + isRing : IsRing + * -_ 0# 1# + isRing = record + { +-isAbelianGroup = +-isAbelianGroup + ; *-cong = ∙-cong + ; *-assoc = assoc + ; *-identity = identity + ; distrib = distrib + ; zero = zero + } where open IsMonoid *-isMonoid + +open IsRing* public + using () renaming (isRing to isRing*) diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda index e8801d3e3b..5463a23045 100644 --- a/src/Data/Bool/Properties.agda +++ b/src/Data/Bool/Properties.agda @@ -506,7 +506,9 @@ true