Skip to content

Remove duplication in Ring-like structures #1684

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MatthewDaggitt merged 6 commits into from
Jan 18, 2022
Merged

Remove duplication in Ring-like structures #1684

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
1da1bec
Deduplicate IsNearSemiring
Taneb Jan 11, 2022
36d7133
Deduplicate IsSemiringWithoutOne
Taneb Jan 11, 2022
96993e1
Deduplicate IsSemiringWithoutAnnihilatingZero
Taneb Jan 11, 2022
6dd1d63
Deduplicate IsRing
Taneb Jan 11, 2022
33f511e
Add migration structures to Algebra.Structures.Biased
Taneb Jan 14, 2022
06f71a8
Update changelog
Taneb Jan 14, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`
Expand Down
9 changes: 7 additions & 2 deletions src/Algebra/Construct/DirectProduct.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
Expand Down Expand Up @@ -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
}
Expand Down
8 changes: 5 additions & 3 deletions src/Algebra/Construct/Subst/Equality.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
12 changes: 9 additions & 3 deletions src/Algebra/Lattice/Properties/BooleanAlgebra.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
}
Expand Down
4 changes: 3 additions & 1 deletion src/Algebra/Morphism/RingMonomorphism.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
119 changes: 90 additions & 29 deletions src/Algebra/Structures.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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# *

Expand All @@ -278,32 +279,62 @@ 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
; isCommutativeMagma to +-isCommutativeMagma
; 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

Expand All @@ -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
Expand Down Expand Up @@ -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ˡ +
Expand All @@ -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
)


Expand All @@ -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
}
Expand Down Expand Up @@ -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# *

Expand Down Expand Up @@ -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# *
Expand All @@ -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
}

Expand Down
Loading