Skip to content

Commit

Permalink
Add a few algebraic structures missing from the Algebra.Construct.Poi…
Browse files Browse the repository at this point in the history 
…ntwise (#2555)

* add a few algebraic structures missing from the Pointwise construct

* update CHANGELOG

* fix ws violation

* resolve conflicts
  • Loading branch information
@bsaul
bsaul authored Jan 19, 2025
1 parent a787006 commit 908e015
Show file tree
Hide file tree
Showing 2 changed files with 132 additions and 2 deletions.
29 changes: 29 additions & 0 deletions CHANGELOG.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,3 +26,32 @@ New modules

Additions to existing modules
-----------------------------

* In `Algebra.Construct.Pointwise`:
```agda
isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# →
IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0# →
IsSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0# →
IsCommutativeSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1# →
IsCommutativeSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isIdempotentSemiring : IsIdempotentSemiring _≈_ _+_ _*_ 0# 1# →
IsIdempotentSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isKleeneAlgebra : IsKleeneAlgebra _≈_ _+_ _*_ _⋆ 0# 1# →
IsKleeneAlgebra (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ _⋆) (lift₀ 0#) (lift₀ 1#)
isQuasiring : IsQuasiring _≈_ _+_ _*_ 0# 1# →
IsQuasiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1# →
IsCommutativeRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
commutativeMonoid : CommutativeMonoid c ℓ → CommutativeMonoid (a ⊔ c) (a ⊔ ℓ)
nearSemiring : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ)
semiringWithoutOne : SemiringWithoutOne c ℓ → SemiringWithoutOne (a ⊔ c) (a ⊔ ℓ)
commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne c ℓ → CommutativeSemiringWithoutOne (a ⊔ c) (a ⊔ ℓ)
commutativeSemiring : CommutativeSemiring c ℓ → CommutativeSemiring (a ⊔ c) (a ⊔ ℓ)
idempotentSemiring : IdempotentSemiring c ℓ → IdempotentSemiring (a ⊔ c) (a ⊔ ℓ)
kleeneAlgebra : KleeneAlgebra c ℓ → KleeneAlgebra (a ⊔ c) (a ⊔ ℓ)
quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
```
105 changes: 103 additions & 2 deletions src/Algebra/Construct/Pointwise.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,15 +22,14 @@ open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)


private

variable
c ℓ : Level
C : Set c
_≈_ : Rel C ℓ
ε 0# 1# : C
_⁻¹ -_ : Op₁ C
_⁻¹ -_ _⋆ : Op₁ C
_∙_ _+_ _*_ : Op₂ C

lift₀ : C → A → C
Expand Down Expand Up @@ -121,6 +120,36 @@ isAbelianGroup isAbelianGroup = record
}
where module M = IsAbelianGroup isAbelianGroup

isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# →
IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isNearSemiring isNearSemiring = record
{ +-isMonoid = isMonoid M.+-isMonoid
; *-cong = λ g h _ → M.*-cong (g _) (h _)
; *-assoc = λ f g h _ → M.*-assoc (f _) (g _) (h _)
; distribʳ = λ f g h _ → M.distribʳ (f _) (g _) (h _)
; zeroˡ = λ f _ → M.zeroˡ (f _)
}
where module M = IsNearSemiring isNearSemiring

isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0# →
IsSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isSemiringWithoutOne isSemiringWithoutOne = record
{ +-isCommutativeMonoid = isCommutativeMonoid M.+-isCommutativeMonoid
; *-cong = λ g h _ → M.*-cong (g _) (h _)
; *-assoc = λ f g h _ → M.*-assoc (f _) (g _) (h _)
; distrib = (λ f g h _ → M.distribˡ (f _) (g _) (h _)) , (λ f g h _ → M.distribʳ (f _) (g _) (h _))
; zero = (λ f _ → M.zeroˡ (f _)) , (λ f _ → M.zeroʳ (f _))
}
where module M = IsSemiringWithoutOne isSemiringWithoutOne

isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0# →
IsCommutativeSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isCommutativeSemiringWithoutOne isCommutativeSemiringWithoutOne = record
{ isSemiringWithoutOne = isSemiringWithoutOne M.isSemiringWithoutOne
; *-comm = λ f g _ → M.*-comm (f _) (g _)
}
where module M = IsCommutativeSemiringWithoutOne isCommutativeSemiringWithoutOne

isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1# →
IsSemiringWithoutAnnihilatingZero (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZero = record
Expand All @@ -140,6 +169,44 @@ isSemiring isSemiring = record
}
where module M = IsSemiring isSemiring

isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1# →
IsCommutativeSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isCommutativeSemiring isCommutativeSemiring = record
{ isSemiring = isSemiring M.isSemiring
; *-comm = λ f g _ → M.*-comm (f _) (g _)
}
where module M = IsCommutativeSemiring isCommutativeSemiring

isIdempotentSemiring : IsIdempotentSemiring _≈_ _+_ _*_ 0# 1# →
IsIdempotentSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isIdempotentSemiring isIdempotentSemiring = record
{ isSemiring = isSemiring M.isSemiring
; +-idem = λ f _ → M.+-idem (f _)
}
where module M = IsIdempotentSemiring isIdempotentSemiring

isKleeneAlgebra : IsKleeneAlgebra _≈_ _+_ _*_ _⋆ 0# 1# →
IsKleeneAlgebra (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ _⋆) (lift₀ 0#) (lift₀ 1#)
isKleeneAlgebra isKleeneAlgebra = record
{ isIdempotentSemiring = isIdempotentSemiring M.isIdempotentSemiring
; starExpansive = (λ f _ → M.starExpansiveˡ (f _)) , λ f _ → M.starExpansiveʳ (f _)
; starDestructive = (λ f g h i _ → M.starDestructiveˡ (f _) (g _) (h _) (i _))
, (λ f g h i _ → M.starDestructiveʳ (f _) (g _) (h _) (i _))
}
where module M = IsKleeneAlgebra isKleeneAlgebra

isQuasiring : IsQuasiring _≈_ _+_ _*_ 0# 1# →
IsQuasiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isQuasiring isQuasiring = record
{ +-isMonoid = isMonoid M.+-isMonoid
; *-cong = λ g h _ → M.*-cong (g _) (h _)
; *-assoc = λ f g h _ → M.*-assoc (f _) (g _) (h _)
; *-identity = (λ f _ → M.*-identityˡ (f _)) , λ f _ → M.*-identityʳ (f _)
; distrib = (λ f g h _ → M.distribˡ (f _) (g _) (h _)) , λ f g h _ → M.distribʳ (f _) (g _) (h _)
; zero = (λ f _ → M.zeroˡ (f _)) , λ f _ → M.zeroʳ (f _)
}
where module M = IsQuasiring isQuasiring

isRing : IsRing _≈_ _+_ _*_ -_ 0# 1# →
IsRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
isRing isRing = record
Expand All @@ -151,6 +218,13 @@ isRing isRing = record
}
where module M = IsRing isRing

isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1# →
IsCommutativeRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
isCommutativeRing isCommutativeRing = record
{ isRing = isRing M.isRing
; *-comm = λ f g _ → M.*-comm (f _) (g _)
}
where module M = IsCommutativeRing isCommutativeRing

------------------------------------------------------------------------
-- Bundles
Expand All @@ -170,15 +244,42 @@ commutativeSemigroup m = record { isCommutativeSemigroup = isCommutativeSemigrou
monoid : Monoid c ℓ → Monoid (a ⊔ c) (a ⊔ ℓ)
monoid m = record { isMonoid = isMonoid (Monoid.isMonoid m) }

commutativeMonoid : CommutativeMonoid c ℓ → CommutativeMonoid (a ⊔ c) (a ⊔ ℓ)
commutativeMonoid m = record { isCommutativeMonoid = isCommutativeMonoid (CommutativeMonoid.isCommutativeMonoid m) }

group : Group c ℓ → Group (a ⊔ c) (a ⊔ ℓ)
group m = record { isGroup = isGroup (Group.isGroup m) }

abelianGroup : AbelianGroup c ℓ → AbelianGroup (a ⊔ c) (a ⊔ ℓ)
abelianGroup m = record { isAbelianGroup = isAbelianGroup (AbelianGroup.isAbelianGroup m) }

nearSemiring : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ)
nearSemiring m = record { isNearSemiring = isNearSemiring (NearSemiring.isNearSemiring m) }

semiringWithoutOne : SemiringWithoutOne c ℓ → SemiringWithoutOne (a ⊔ c) (a ⊔ ℓ)
semiringWithoutOne m = record { isSemiringWithoutOne = isSemiringWithoutOne (SemiringWithoutOne.isSemiringWithoutOne m) }

commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne c ℓ → CommutativeSemiringWithoutOne (a ⊔ c) (a ⊔ ℓ)
commutativeSemiringWithoutOne m = record
{ isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne (CommutativeSemiringWithoutOne.isCommutativeSemiringWithoutOne m) }

semiring : Semiring c ℓ → Semiring (a ⊔ c) (a ⊔ ℓ)
semiring m = record { isSemiring = isSemiring (Semiring.isSemiring m) }

commutativeSemiring : CommutativeSemiring c ℓ → CommutativeSemiring (a ⊔ c) (a ⊔ ℓ)
commutativeSemiring m = record { isCommutativeSemiring = isCommutativeSemiring (CommutativeSemiring.isCommutativeSemiring m) }

idempotentSemiring : IdempotentSemiring c ℓ → IdempotentSemiring (a ⊔ c) (a ⊔ ℓ)
idempotentSemiring m = record { isIdempotentSemiring = isIdempotentSemiring (IdempotentSemiring.isIdempotentSemiring m) }

kleeneAlgebra : KleeneAlgebra c ℓ → KleeneAlgebra (a ⊔ c) (a ⊔ ℓ)
kleeneAlgebra m = record { isKleeneAlgebra = isKleeneAlgebra (KleeneAlgebra.isKleeneAlgebra m) }

quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
quasiring m = record { isQuasiring = isQuasiring (Quasiring.isQuasiring m) }

ring : Ring c ℓ → Ring (a ⊔ c) (a ⊔ ℓ)
ring m = record { isRing = isRing (Ring.isRing m) }

commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
commutativeRing m = record { isCommutativeRing = isCommutativeRing (CommutativeRing.isCommutativeRing m) }

0 comments on commit 908e015

Please sign in to comment.