------------------------------------------------------------------------
-- The Agda standard library
--
-- Flipping the arguments of a binary operation preserves many of its
-- algebraic properties.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Construct.Flip.Op where
open import Algebra.Core
open import Algebra.Bundles
import Algebra.Definitions as Def
import Algebra.Structures as Str
import Algebra.Consequences.Setoid as Consequences
import Data.Product as Prod
import Data.Sum as Sum
open import Function.Base using (flip)
open import Level using (Level)
open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_)
open import Relation.Binary.Definitions using (Symmetric)
private
variable
a ℓ : Level
A : Set a
≈ : Rel A ℓ
ε : A
⁻¹ : Op₁ A
∙ : Op₂ A
------------------------------------------------------------------------
-- Properties
preserves₂ : (∼ ≈ ≋ : Rel A ℓ) →
∙ Preserves₂ ∼ ⟶ ≈ ⟶ ≋ → (flip ∙) Preserves₂ ≈ ⟶ ∼ ⟶ ≋
preserves₂ _ _ _ pres = flip pres
module ∙-Properties (≈ : Rel A ℓ) (∙ : Op₂ A) where
open Def ≈
associative : Symmetric ≈ → Associative ∙ → Associative (flip ∙)
associative sym assoc x y z = sym (assoc z y x)
identity : Identity ε ∙ → Identity ε (flip ∙)
identity id = Prod.swap id
commutative : Commutative ∙ → Commutative (flip ∙)
commutative comm = flip comm
selective : Selective ∙ → Selective (flip ∙)
selective sel x y = Sum.swap (sel y x)
idempotent : Idempotent ∙ → Idempotent (flip ∙)
idempotent idem = idem
inverse : Inverse ε ⁻¹ ∙ → Inverse ε ⁻¹ (flip ∙)
inverse inv = Prod.swap inv
zero : Zero ε ∙ → Zero ε (flip ∙)
zero zer = Prod.swap zer
module *-Properties (≈ : Rel A ℓ) (* + : Op₂ A) where
open Def ≈
distributes : * DistributesOver + → (flip *) DistributesOver +
distributes distrib = Prod.swap distrib
------------------------------------------------------------------------
-- Structures
module _ {≈ : Rel A ℓ} {∙ : Op₂ A} where
open Def ≈
open Str ≈
open ∙-Properties ≈ ∙
isMagma : IsMagma ∙ → IsMagma (flip ∙)
isMagma m = record
{ isEquivalence = isEquivalence
; ∙-cong = preserves₂ ≈ ≈ ≈ ∙-cong
}
where open IsMagma m
isSelectiveMagma : IsSelectiveMagma ∙ → IsSelectiveMagma (flip ∙)
isSelectiveMagma m = record
{ isMagma = isMagma m.isMagma
; sel = selective m.sel
}
where module m = IsSelectiveMagma m
isCommutativeMagma : IsCommutativeMagma ∙ → IsCommutativeMagma (flip ∙)
isCommutativeMagma m = record
{ isMagma = isMagma m.isMagma
; comm = commutative m.comm
}
where module m = IsCommutativeMagma m
isSemigroup : IsSemigroup ∙ → IsSemigroup (flip ∙)
isSemigroup s = record
{ isMagma = isMagma s.isMagma
; assoc = associative s.sym s.assoc
}
where module s = IsSemigroup s
isBand : IsBand ∙ → IsBand (flip ∙)
isBand b = record
{ isSemigroup = isSemigroup b.isSemigroup
; idem = b.idem
}
where module b = IsBand b
isCommutativeSemigroup : IsCommutativeSemigroup ∙ →
IsCommutativeSemigroup (flip ∙)
isCommutativeSemigroup s = record
{ isSemigroup = isSemigroup s.isSemigroup
; comm = commutative s.comm
}
where module s = IsCommutativeSemigroup s
isUnitalMagma : IsUnitalMagma ∙ ε → IsUnitalMagma (flip ∙) ε
isUnitalMagma m = record
{ isMagma = isMagma m.isMagma
; identity = identity m.identity
}
where module m = IsUnitalMagma m
isMonoid : IsMonoid ∙ ε → IsMonoid (flip ∙) ε
isMonoid m = record
{ isSemigroup = isSemigroup m.isSemigroup
; identity = identity m.identity
}
where module m = IsMonoid m
isCommutativeMonoid : IsCommutativeMonoid ∙ ε →
IsCommutativeMonoid (flip ∙) ε
isCommutativeMonoid m = record
{ isMonoid = isMonoid m.isMonoid
; comm = commutative m.comm
}
where module m = IsCommutativeMonoid m
isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ∙ ε →
IsIdempotentCommutativeMonoid (flip ∙) ε
isIdempotentCommutativeMonoid m = record
{ isCommutativeMonoid = isCommutativeMonoid m.isCommutativeMonoid
; idem = idempotent m.idem
}
where module m = IsIdempotentCommutativeMonoid m
isInvertibleMagma : IsInvertibleMagma ∙ ε ⁻¹ →
IsInvertibleMagma (flip ∙) ε ⁻¹
isInvertibleMagma m = record
{ isMagma = isMagma m.isMagma
; inverse = inverse m.inverse
; ⁻¹-cong = m.⁻¹-cong
}
where module m = IsInvertibleMagma m
isInvertibleUnitalMagma : IsInvertibleUnitalMagma ∙ ε ⁻¹ →
IsInvertibleUnitalMagma (flip ∙) ε ⁻¹
isInvertibleUnitalMagma m = record
{ isInvertibleMagma = isInvertibleMagma m.isInvertibleMagma
; identity = identity m.identity
}
where module m = IsInvertibleUnitalMagma m
isGroup : IsGroup ∙ ε ⁻¹ → IsGroup (flip ∙) ε ⁻¹
isGroup g = record
{ isMonoid = isMonoid g.isMonoid
; inverse = inverse g.inverse
; ⁻¹-cong = g.⁻¹-cong
}
where module g = IsGroup g
isAbelianGroup : IsAbelianGroup ∙ ε ⁻¹ → IsAbelianGroup (flip ∙) ε ⁻¹
isAbelianGroup g = record
{ isGroup = isGroup g.isGroup
; comm = commutative g.comm
}
where module g = IsAbelianGroup g
module _ {≈ : Rel A ℓ} {+ * : Op₂ A} {0# 1# : A} where
open Str ≈
open ∙-Properties ≈ *
open *-Properties ≈ * +
isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# →
IsSemiringWithoutAnnihilatingZero + (flip *) 0# 1#
isSemiringWithoutAnnihilatingZero r = record
{ +-isCommutativeMonoid = r.+-isCommutativeMonoid
; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
; *-assoc = associative r.sym r.*-assoc
; *-identity = identity r.*-identity
; distrib = distributes r.distrib
}
where module r = IsSemiringWithoutAnnihilatingZero r
isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1#
isSemiring r = record
{ isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero r.isSemiringWithoutAnnihilatingZero
; zero = zero r.zero
}
where module r = IsSemiring r
isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# →
IsCommutativeSemiring + (flip *) 0# 1#
isCommutativeSemiring r = record
{ isSemiring = isSemiring r.isSemiring
; *-comm = commutative r.*-comm
}
where module r = IsCommutativeSemiring r
isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring + * 0# 1# →
IsCancellativeCommutativeSemiring + (flip *) 0# 1#
isCancellativeCommutativeSemiring r = record
{ isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring
; *-cancelˡ-nonZero = Consequences.comm∧almostCancelˡ⇒almostCancelʳ r.setoid r.*-comm r.*-cancelˡ-nonZero
}
where module r = IsCancellativeCommutativeSemiring r
isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# →
IsIdempotentSemiring + (flip *) 0# 1#
isIdempotentSemiring r = record
{ isSemiring = isSemiring r.isSemiring
; +-idem = r.+-idem
}
where module r = IsIdempotentSemiring r
isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1#
isQuasiring r = record
{ +-isMonoid = r.+-isMonoid
; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
; *-assoc = associative r.sym r.*-assoc
; *-identity = identity r.*-identity
; distrib = distributes r.distrib
; zero = zero r.zero
}
where module r = IsQuasiring r
module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# : A} where
open Str ≈
open ∙-Properties ≈ *
open *-Properties ≈ * +
isRingWithoutOne : IsRingWithoutOne + * - 0# → IsRingWithoutOne + (flip *) - 0#
isRingWithoutOne r = record
{ +-isAbelianGroup = r.+-isAbelianGroup
; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
; *-assoc = associative r.sym r.*-assoc
; distrib = distributes r.distrib
}
where module r = IsRingWithoutOne r
module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where
open Str ≈
open ∙-Properties ≈ *
open *-Properties ≈ * +
isNonAssociativeRing : IsNonAssociativeRing + * - 0# 1# →
IsNonAssociativeRing + (flip *) - 0# 1#
isNonAssociativeRing r = record
{ +-isAbelianGroup = r.+-isAbelianGroup
; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
; *-identity = identity r.*-identity
; distrib = distributes r.distrib
; zero = zero r.zero
}
where module r = IsNonAssociativeRing r
isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# -
isNearring r = record
{ isQuasiring = isQuasiring r.isQuasiring
; +-inverse = r.+-inverse
; ⁻¹-cong = r.⁻¹-cong
}
where module r = IsNearring r
isRing : IsRing + * - 0# 1# → IsRing + (flip *) - 0# 1#
isRing r = record
{ +-isAbelianGroup = r.+-isAbelianGroup
; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
; *-assoc = associative r.sym r.*-assoc
; *-identity = identity r.*-identity
; distrib = distributes r.distrib
}
where module r = IsRing r
isCommutativeRing : IsCommutativeRing + * - 0# 1# →
IsCommutativeRing + (flip *) - 0# 1#
isCommutativeRing r = record
{ isRing = isRing r.isRing
; *-comm = commutative r.*-comm
}
where module r = IsCommutativeRing r
------------------------------------------------------------------------
-- Bundles
magma : Magma a ℓ → Magma a ℓ
magma m = record { isMagma = isMagma m.isMagma }
where module m = Magma m
commutativeMagma : CommutativeMagma a ℓ → CommutativeMagma a ℓ
commutativeMagma m = record
{ isCommutativeMagma = isCommutativeMagma m.isCommutativeMagma
}
where module m = CommutativeMagma m
selectiveMagma : SelectiveMagma a ℓ → SelectiveMagma a ℓ
selectiveMagma m = record
{ isSelectiveMagma = isSelectiveMagma m.isSelectiveMagma
}
where module m = SelectiveMagma m
semigroup : Semigroup a ℓ → Semigroup a ℓ
semigroup s = record { isSemigroup = isSemigroup s.isSemigroup }
where module s = Semigroup s
band : Band a ℓ → Band a ℓ
band b = record { isBand = isBand b.isBand }
where module b = Band b
commutativeSemigroup : CommutativeSemigroup a ℓ → CommutativeSemigroup a ℓ
commutativeSemigroup s = record
{ isCommutativeSemigroup = isCommutativeSemigroup s.isCommutativeSemigroup
}
where module s = CommutativeSemigroup s
unitalMagma : UnitalMagma a ℓ → UnitalMagma a ℓ
unitalMagma m = record
{ isUnitalMagma = isUnitalMagma m.isUnitalMagma
}
where module m = UnitalMagma m
monoid : Monoid a ℓ → Monoid a ℓ
monoid m = record { isMonoid = isMonoid m.isMonoid }
where module m = Monoid m
commutativeMonoid : CommutativeMonoid a ℓ → CommutativeMonoid a ℓ
commutativeMonoid m = record
{ isCommutativeMonoid = isCommutativeMonoid m.isCommutativeMonoid
}
where module m = CommutativeMonoid m
idempotentCommutativeMonoid : IdempotentCommutativeMonoid a ℓ →
IdempotentCommutativeMonoid a ℓ
idempotentCommutativeMonoid m = record
{ isIdempotentCommutativeMonoid =
isIdempotentCommutativeMonoid m.isIdempotentCommutativeMonoid
}
where module m = IdempotentCommutativeMonoid m
invertibleMagma : InvertibleMagma a ℓ → InvertibleMagma a ℓ
invertibleMagma m = record
{ isInvertibleMagma = isInvertibleMagma m.isInvertibleMagma
}
where module m = InvertibleMagma m
invertibleUnitalMagma : InvertibleUnitalMagma a ℓ → InvertibleUnitalMagma a ℓ
invertibleUnitalMagma m = record
{ isInvertibleUnitalMagma = isInvertibleUnitalMagma m.isInvertibleUnitalMagma
}
where module m = InvertibleUnitalMagma m
group : Group a ℓ → Group a ℓ
group g = record { isGroup = isGroup g.isGroup }
where module g = Group g
abelianGroup : AbelianGroup a ℓ → AbelianGroup a ℓ
abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup }
where module g = AbelianGroup g
semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ →
SemiringWithoutAnnihilatingZero a ℓ
semiringWithoutAnnihilatingZero r = record
{ isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero r.isSemiringWithoutAnnihilatingZero }
where module r = SemiringWithoutAnnihilatingZero r
semiring : Semiring a ℓ → Semiring a ℓ
semiring r = record { isSemiring = isSemiring r.isSemiring }
where module r = Semiring r
commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ
commutativeSemiring r = record
{ isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring }
where module r = CommutativeSemiring r
cancellativeCommutativeSemiring : CancellativeCommutativeSemiring a ℓ →
CancellativeCommutativeSemiring a ℓ
cancellativeCommutativeSemiring r = record
{ isCancellativeCommutativeSemiring = isCancellativeCommutativeSemiring r.isCancellativeCommutativeSemiring }
where module r = CancellativeCommutativeSemiring r
idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ
idempotentSemiring r = record
{ isIdempotentSemiring = isIdempotentSemiring r.isIdempotentSemiring }
where module r = IdempotentSemiring r
quasiring : Quasiring a ℓ → Quasiring a ℓ
quasiring r = record { isQuasiring = isQuasiring r.isQuasiring }
where module r = Quasiring r
ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ
ringWithoutOne r = record { isRingWithoutOne = isRingWithoutOne r.isRingWithoutOne }
where module r = RingWithoutOne r
nonAssociativeRing : NonAssociativeRing a ℓ → NonAssociativeRing a ℓ
nonAssociativeRing r = record
{ isNonAssociativeRing = isNonAssociativeRing r.isNonAssociativeRing }
where module r = NonAssociativeRing r
nearring : Nearring a ℓ → Nearring a ℓ
nearring r = record { isNearring = isNearring r.isNearring }
where module r = Nearring r
ring : Ring a ℓ → Ring a ℓ
ring r = record { isRing = isRing r.isRing }
where module r = Ring r
commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ
commutativeRing r = record { isCommutativeRing = isCommutativeRing r.isCommutativeRing }
where module r = CommutativeRing r
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4