diff --git a/src/Algebra/Ordered.agda b/src/Algebra/Ordered.agda index 69e726aec0..5d2c9c96e7 100644 --- a/src/Algebra/Ordered.agda +++ b/src/Algebra/Ordered.agda @@ -12,3 +12,4 @@ module Algebra.Ordered where open import Algebra.Ordered.Structures public open import Algebra.Ordered.Bundles public +open import Algebra.Ordered.Residuated public diff --git a/src/Algebra/Ordered/Residuated.agda b/src/Algebra/Ordered/Residuated.agda new file mode 100644 index 0000000000..c888ab0984 --- /dev/null +++ b/src/Algebra/Ordered/Residuated.agda @@ -0,0 +1,457 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Residuated pomonoids and lattices +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary.Core using (Rel) + +module Algebra.Ordered.Residuated where + +open import Algebra.Core using (Op₂) +open import Algebra.Bundles using (Monoid; Semiring) +open import Algebra.Ordered.Bundles +open import Data.Product using (proj₁; proj₂; swap) +open import Function using (flip) +open import Level using (suc; _⊔_) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions +open import Relation.Binary.Lattice.Definitions using (Supremum) +open import Relation.Binary.Lattice.Bundles +import Relation.Binary.Reasoning.PartialOrder as PosetReasoning + +------------------------------------------------------------------------ +-- Structures + +module _ + {a ℓ₁ ℓ₂} {A : Set a} -- The underlying set + (_≈_ : Rel A ℓ₁) -- The underlying equality + (_≤_ : Rel A ℓ₂) -- The partial order + where + + -- FIXME: the definition of these structures should probably go into + -- a separate module parametrized by _≈_ and _≤_, at which point + -- these should go to the top. But until it's clear where these + -- should go, I'll keep this as is. + + open import Algebra.Definitions _≈_ + open import Algebra.Ordered.Structures _≈_ _≤_ + open import Algebra.Structures _≈_ using (IsMonoid; IsSemiring) + open import Relation.Binary.Structures _≈_ using (IsPartialOrder) + open import Relation.Binary.Lattice.Structures _≈_ _≤_ + + -- Residuated pomonoids + -- + -- TODO: should this remain here, in a separate module, or go into + -- Algebra.Ordered.Structures? + + record IsRightResiduatedPomonoid + (_∙_ : Op₂ A) -- The monoid multiplication + (_\\_ : Op₂ A) -- The right residual + (ε : A) -- The monoid unit + : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + + field + isPartialOrder : IsPartialOrder _≤_ + ∙-mono₁ : ∀ z → Monotonic₁ _≤_ _≤_ (_∙ z) + assoc : Associative _∙_ + identity : Identity ε _∙_ + adjoint : ∀ {z} → Adjoint _≤_ _≤_ (z ∙_) (z \\_) + + open IsPartialOrder isPartialOrder public using (refl) + + unit : ∀ {x y} → y ≤ (x \\ (x ∙ y)) + unit = proj₁ adjoint refl + + counit : ∀ {x y} → (x ∙ (x \\ y)) ≤ y + counit = proj₂ adjoint refl + + open PosetReasoning (record { isPartialOrder = isPartialOrder }) + + ∙-mono₂ : ∀ z → Monotonic₁ _≤_ _≤_ (z ∙_) + ∙-mono₂ z {x} {x′} x≤x′ = proj₂ adjoint (begin + x ≤⟨ x≤x′ ⟩ + x′ ≤⟨ unit ⟩ + z \\ (z ∙ x′) ∎) + + ∙-mono : Monotonic₂ _≤_ _≤_ _≤_ _∙_ + ∙-mono {x} {x′} {y} {y′} x≤x′ y≤y′ = begin + x ∙ y ≤⟨ ∙-mono₁ y x≤x′ ⟩ + x′ ∙ y ≤⟨ ∙-mono₂ x′ y≤y′ ⟩ + x′ ∙ y′ ∎ + + isPomonoid : IsPomonoid _∙_ ε + isPomonoid = record + { isPosemigroup = record + { isPomagma = record + { isPartialOrder = isPartialOrder + ; mono = ∙-mono + } + ; assoc = assoc + } + ; identity = identity + } + + open IsPomonoid isPomonoid public hiding + ( isPartialOrder + ; refl + ; mono + ; assoc + ; identity + ) + + \\-anti₁ : ∀ z → Antitonic₁ _≤_ _≤_ (_\\ z) + \\-anti₁ z {x} {x′} x≥x′ = proj₁ adjoint (begin + x′ ∙ (x \\ z) ≤⟨ ∙-mono₁ _ x≥x′ ⟩ + x ∙ (x \\ z) ≤⟨ counit ⟩ + z ∎) + + \\-mono₂ : ∀ z → Monotonic₁ _≤_ _≤_ (z \\_) + \\-mono₂ z {x} {x′} x≤x′ = proj₁ adjoint (begin + z ∙ (z \\ x) ≤⟨ counit ⟩ + x ≤⟨ x≤x′ ⟩ + x′ ∎) + + \\-mono : AntitonicMonotonic _≤_ _≤_ _≤_ _\\_ + \\-mono {x} {x′} {y} {y′} x≥x′ y≤y′ = begin + x \\ y ≤⟨ \\-anti₁ y x≥x′ ⟩ + x′ \\ y ≤⟨ \\-mono₂ x′ y≤y′ ⟩ + x′ \\ y′ ∎ + + record IsResiduatedPomonoid (_∙_ : Op₂ A) -- The monoid multiplication + (_//_ : Op₂ A) -- The left residual + (_\\_ : Op₂ A) -- The right residual + (ε : A) -- The monoid unit + : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isPartialOrder : IsPartialOrder _≤_ + assoc : Associative _∙_ + identity : Identity ε _∙_ + ∙-//-adjoint : ∀ {z} → Adjoint _≤_ _≤_ (_∙ z) (_// z) + ∙-\\-adjoint : ∀ {z} → Adjoint _≤_ _≤_ (z ∙_) (z \\_) + + open IsPartialOrder isPartialOrder public using (refl) + + ∙-//-unit : ∀ {x y} → y ≤ ((y ∙ x) // x) + ∙-//-unit = proj₁ ∙-//-adjoint refl + + open PosetReasoning (record { isPartialOrder = isPartialOrder }) + + ∙-mono₁ : ∀ z → Monotonic₁ _≤_ _≤_ (_∙ z) + ∙-mono₁ z {x} {x′} x≤x′ = proj₂ ∙-//-adjoint (begin + x ≤⟨ x≤x′ ⟩ + x′ ≤⟨ ∙-//-unit ⟩ + (x′ ∙ z) // z ∎) + + isRightResiduatedPomonoid : IsRightResiduatedPomonoid _∙_ _\\_ ε + isRightResiduatedPomonoid = record + { isPartialOrder = isPartialOrder + ; ∙-mono₁ = ∙-mono₁ + ; assoc = assoc + ; identity = identity + ; adjoint = ∙-\\-adjoint + } + + open IsRightResiduatedPomonoid isRightResiduatedPomonoid public + renaming + ( unit to ∙-\\-unit + ; counit to ∙-\\-counit + ) + hiding + ( isPartialOrder + ; refl + ; ∙-mono₁ + ; assoc + ; identity + ; adjoint + ) + + isLeftResiduatedPomonoid : IsRightResiduatedPomonoid (flip _∙_) (flip _//_) ε + isLeftResiduatedPomonoid = record + { isPartialOrder = isPartialOrder + ; ∙-mono₁ = ∙-mono₂ + ; assoc = λ x y z → Eq.sym (assoc z y x) + ; identity = swap identity + ; adjoint = ∙-//-adjoint + } + + open IsRightResiduatedPomonoid isLeftResiduatedPomonoid public + using () renaming + ( counit to ∙-//-counit + ; \\-anti₁ to //-anti₂ + ; \\-mono₂ to //-mono₁ + ; \\-mono to //-mono + ) + + ------------------------------------------------------------------------ + -- Residuated lattices + + -- Residuated semilattices + -- + -- NOTE: We're only treating the join-case here, the meet-case is + -- analogous. + -- + -- TODO: should these definitions remain here, in a separate module in + -- the Algebra.Ordered hiararchy, or go into + -- Relation.Binary.Lattice.Structures? + + record IsRightResiduatedSemilattice + (∨ : Op₂ A) -- The join operation. + (∙ : Op₂ A) -- The monoid multiplication. + (\\ : Op₂ A) -- The right residual. + (ε : A) -- The monoid unit. + : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + + field + isRightResiduatedPomonoid : IsRightResiduatedPomonoid ∙ \\ ε + supremum : Supremum _≤_ ∨ + + open IsRightResiduatedPomonoid isRightResiduatedPomonoid public + + isJoinSemilattice : IsJoinSemilattice ∨ + isJoinSemilattice = record + { isPartialOrder = isPartialOrder + ; supremum = supremum + } + + record IsResiduatedSemilattice + (∨ : Op₂ A) -- The join operation. + (∙ : Op₂ A) -- The monoid multiplication. + (// : Op₂ A) -- The left residual. + (\\ : Op₂ A) -- The right residual. + (ε : A) -- The monoid unit. + : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + + field + isResiduatedPomonoid : IsResiduatedPomonoid ∙ // \\ ε + supremum : Supremum _≤_ ∨ + + open IsResiduatedPomonoid isResiduatedPomonoid public + + isRightResiduatedSemilattice : IsRightResiduatedSemilattice ∨ ∙ \\ ε + isRightResiduatedSemilattice = record + { isRightResiduatedPomonoid = isRightResiduatedPomonoid + ; supremum = supremum + } + + isLeftResiduatedSemilattice + : IsRightResiduatedSemilattice ∨ (flip ∙) (flip //) ε + isLeftResiduatedSemilattice = record + { isRightResiduatedPomonoid = isLeftResiduatedPomonoid + ; supremum = supremum + } + + open IsRightResiduatedSemilattice isRightResiduatedSemilattice public + using (isJoinSemilattice) + + -- Residuated bounded semilattices + + record IsResiduatedBoundedSemilattice + (∨ : Op₂ A) -- The join operation. + (∙ : Op₂ A) -- The monoid multiplication. + (// : Op₂ A) -- The left residual. + (\\ : Op₂ A) -- The right residual. + (⊥ : A) -- The lattice minimum. + (ε : A) -- The monoid unit. + : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + + field + isResiduatedPomonoid : IsResiduatedPomonoid ∙ // \\ ε + supremum : Supremum _≤_ ∨ + minimum : Minimum _≤_ ⊥ + + open IsResiduatedPomonoid isResiduatedPomonoid public + + isResiduatedSemilattice : IsResiduatedSemilattice ∨ ∙ // \\ ε + isResiduatedSemilattice = record + { isResiduatedPomonoid = isResiduatedPomonoid + ; supremum = supremum + } + open IsResiduatedSemilattice isResiduatedSemilattice public using + ( isJoinSemilattice + ; isRightResiduatedSemilattice + ; isLeftResiduatedSemilattice + ) + + isBoundedJoinSemilattice : IsBoundedJoinSemilattice ∨ ⊥ + isBoundedJoinSemilattice = record + { isJoinSemilattice = isJoinSemilattice + ; minimum = minimum + } + +------------------------------------------------------------------------ +-- Bundles +-- +-- FIXME: should these go into a separate module? If so, where? + +-- Residuated pomonoids + +record RightResiduatedPomonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _≤_ + infixl 7 _∙_ + infixl 6 _\\_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ -- The underlying equality. + _≤_ : Rel Carrier ℓ₂ -- The partial order. + _∙_ : Op₂ Carrier -- The monoid multiplication. + _\\_ : Op₂ Carrier -- The right residual. + ε : Carrier -- The monoid unit. + isRightResiduatedPomonoid : IsRightResiduatedPomonoid _≈_ _≤_ _∙_ _\\_ ε + + open IsRightResiduatedPomonoid isRightResiduatedPomonoid public + + pomonoid : Pomonoid c ℓ₁ ℓ₂ + pomonoid = record { isPomonoid = isPomonoid } + + open Pomonoid pomonoid public using + ( preorder + ; poset + ; magma + ; promagma + ; pomagma + ; semigroup + ; prosemigroup + ; posemigroup + ; monoid + ; promonoid + ) + +record ResiduatedPomonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _≤_ + infixl 7 _∙_ + infixl 6 _//_ _\\_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ -- The underlying equality. + _≤_ : Rel Carrier ℓ₂ -- The partial order. + _∙_ : Op₂ Carrier -- The monoid multiplication. + _//_ : Op₂ Carrier -- The left residual. + _\\_ : Op₂ Carrier -- The right residual. + ε : Carrier -- The monoid unit. + isResiduatedPomonoid : IsResiduatedPomonoid _≈_ _≤_ _∙_ _//_ _\\_ ε + + open IsResiduatedPomonoid isResiduatedPomonoid public + + leftResiduatedPomonoid : RightResiduatedPomonoid c ℓ₁ ℓ₂ + leftResiduatedPomonoid = record + { isRightResiduatedPomonoid = isLeftResiduatedPomonoid } + + rightResiduatedPomonoid : RightResiduatedPomonoid c ℓ₁ ℓ₂ + rightResiduatedPomonoid = record + { isRightResiduatedPomonoid = isRightResiduatedPomonoid } + + open RightResiduatedPomonoid rightResiduatedPomonoid public + using (preorder; poset; pomonoid; semigroup; monoid) + +-- Residuated semilattices + +record RightResiduatedSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _≤_ + infixr 6 _∨_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ -- The underlying equality. + _≤_ : Rel Carrier ℓ₂ -- The partial order. + _∨_ : Op₂ Carrier -- The join operation. + _∙_ : Op₂ Carrier -- The monoid multiplication. + _\\_ : Op₂ Carrier -- The right residual. + ε : Carrier -- The monoid unit. + isRightResiduatedSemilattice + : IsRightResiduatedSemilattice _≈_ _≤_ _∨_ _∙_ _\\_ ε + + open IsRightResiduatedSemilattice isRightResiduatedSemilattice public + + rightResiduatedPomonoid : RightResiduatedPomonoid c ℓ₁ ℓ₂ + rightResiduatedPomonoid = record + { isRightResiduatedPomonoid = isRightResiduatedPomonoid } + + open RightResiduatedPomonoid public + using (preorder; poset; pomonoid; semigroup; monoid) + + joinSemilattice : JoinSemilattice c ℓ₁ ℓ₂ + joinSemilattice = record { isJoinSemilattice = isJoinSemilattice } + +record ResiduatedSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _≤_ + infixr 6 _∨_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ -- The underlying equality. + _≤_ : Rel Carrier ℓ₂ -- The partial order. + _∨_ : Op₂ Carrier -- The join operation. + _∙_ : Op₂ Carrier -- The monoid multiplication. + _//_ : Op₂ Carrier -- The left residual. + _\\_ : Op₂ Carrier -- The right residual. + ε : Carrier -- The monoid unit. + isResiduatedSemilattice + : IsResiduatedSemilattice _≈_ _≤_ _∨_ _∙_ _//_ _\\_ ε + + open IsResiduatedSemilattice isResiduatedSemilattice public + + residuatedPomonoid : ResiduatedPomonoid c ℓ₁ ℓ₂ + residuatedPomonoid = record { isResiduatedPomonoid = isResiduatedPomonoid } + + open ResiduatedPomonoid residuatedPomonoid public using + ( leftResiduatedPomonoid + ; rightResiduatedPomonoid + ; preorder + ; poset + ; pomonoid + ; semigroup + ; monoid + ) + + leftResiduatedSemilattice : RightResiduatedSemilattice c ℓ₁ ℓ₂ + leftResiduatedSemilattice = record + { isRightResiduatedSemilattice = isLeftResiduatedSemilattice } + + rightResiduatedSemilattice : RightResiduatedSemilattice c ℓ₁ ℓ₂ + rightResiduatedSemilattice = record + { isRightResiduatedSemilattice = isRightResiduatedSemilattice } + + open RightResiduatedSemilattice rightResiduatedSemilattice public + using (joinSemilattice) + +-- Residuated bounded semilattices + +record ResiduatedBoundedSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈_ _≤_ + infixr 6 _∨_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ -- The underlying equality. + _≤_ : Rel Carrier ℓ₂ -- The partial order. + _∨_ : Op₂ Carrier -- The join operation. + _∙_ : Op₂ Carrier -- The monoid multiplication. + _//_ : Op₂ Carrier -- The left residual. + _\\_ : Op₂ Carrier -- The right residual. + ⊥ : Carrier -- The lattice minimum. + ε : Carrier -- The monoid unit. + isResiduatedBoundedSemilattice + : IsResiduatedBoundedSemilattice _≈_ _≤_ _∨_ _∙_ _//_ _\\_ ⊥ ε + + open IsResiduatedBoundedSemilattice isResiduatedBoundedSemilattice public + + residuatedSemilattice : ResiduatedSemilattice c ℓ₁ ℓ₂ + residuatedSemilattice = record + { isResiduatedSemilattice = isResiduatedSemilattice } + + open ResiduatedSemilattice residuatedSemilattice public using + ( preorder + ; poset + ; pomonoid + ; rightResiduatedPomonoid + ; leftResiduatedPomonoid + ; joinSemilattice + ; leftResiduatedSemilattice + ; rightResiduatedSemilattice + ; semigroup + ; monoid + ) + + boundedJoinSemilattice : BoundedJoinSemilattice c ℓ₁ ℓ₂ + boundedJoinSemilattice = record + { isBoundedJoinSemilattice = isBoundedJoinSemilattice } diff --git a/src/Algebra/Properties/ResiduatedPomonoid.agda b/src/Algebra/Properties/ResiduatedPomonoid.agda new file mode 100644 index 0000000000..231927858d --- /dev/null +++ b/src/Algebra/Properties/ResiduatedPomonoid.agda @@ -0,0 +1,35 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of right-residuated partially ordered monoids +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Ordered.Residuated using (ResiduatedPomonoid) + +module Algebra.Properties.ResiduatedPomonoid + {a ℓ₁ ℓ₂} (rp : ResiduatedPomonoid a ℓ₁ ℓ₂) + where + +import Algebra.Properties.RightResiduatedPomonoid as RightResiduatedPomonoid + +open ResiduatedPomonoid rp + +open RightResiduatedPomonoid rightResiduatedPomonoid public + renaming + ( unit-ε to \\-unit-ε + ; isGaloisConnection to ∙-\\-isGaloisConnection + ; galoisConnection to ∙-\\-galoisConnection + ) + +open RightResiduatedPomonoid leftResiduatedPomonoid public + using () renaming + ( \\-cong to //-cong + ; ∙-\\-assoc to //-∙-assoc + ; \\-∙-assoc to ∙-//-assoc + ; \\-identityˡ to //-identityʳ + ; unit-ε to //-unit-ε + ; isGaloisConnection to ∙-//-isGaloisConnection + ; galoisConnection to ∙-//-galoisConnection + ) diff --git a/src/Algebra/Properties/RightResiduatedPomonoid.agda b/src/Algebra/Properties/RightResiduatedPomonoid.agda new file mode 100644 index 0000000000..f5836d2e6c --- /dev/null +++ b/src/Algebra/Properties/RightResiduatedPomonoid.agda @@ -0,0 +1,111 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of right-residuated partially ordered monoids +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Ordered.Residuated + +module Algebra.Properties.RightResiduatedPomonoid + {a ℓ₁ ℓ₂} (rrp : RightResiduatedPomonoid a ℓ₁ ℓ₂) + where + +open import Algebra.Definitions using (Congruent₂; Commutative) +import Algebra.Construct.Flip.Op as FlipOp +open import Data.Product using (_,_; proj₁; proj₂) +open import Function.Base using (flip) +open import Function.GaloisConnection +import Relation.Binary.Reasoning.PartialOrder as PosetReasoning +open import Relation.Binary.Consequences using (mono₂⇒cong₂) +open import Relation.Binary.Definitions using (Adjoint) + +open RightResiduatedPomonoid rrp +open PosetReasoning (record { isPartialOrder = isPartialOrder }) + + +------------------------------------------------------------------------------ +-- Useful (in)equations. + +\\-cong : Congruent₂ _≈_ _\\_ +\\-cong x≈y u≈v = + antisym (\\-mono (reflexive (Eq.sym x≈y)) (reflexive u≈v)) + (\\-mono (reflexive x≈y) (reflexive (Eq.sym u≈v))) + +∙-\\-assoc : ∀ {x y z} → ((x ∙ y) \\ z) ≈ (y \\ (x \\ z)) +∙-\\-assoc {x} {y} {z} = antisym + (proj₁ adjoint (proj₁ adjoint (begin + x ∙ (y ∙ ((x ∙ y) \\ z)) ≈⟨ Eq.sym (assoc x y _) ⟩ + (x ∙ y) ∙ ((x ∙ y) \\ z) ≤⟨ counit ⟩ + z ∎))) + (proj₁ adjoint (begin + (x ∙ y) ∙ (y \\ (x \\ z)) ≈⟨ assoc x y _ ⟩ + x ∙ (y ∙ (y \\ (x \\ z))) ≤⟨ ∙-mono₂ x counit ⟩ + x ∙ (x \\ z) ≤⟨ counit ⟩ + z ∎)) + +\\-∙-assoc : ∀ {x y z} → ((x \\ y) ∙ z) ≤ (x \\ (y ∙ z)) +\\-∙-assoc {x} {y} {z} = proj₁ adjoint (begin + x ∙ ((x \\ y) ∙ z) ≈⟨ Eq.sym (assoc x (x \\ y) z) ⟩ + (x ∙ (x \\ y)) ∙ z ≤⟨ ∙-mono₁ z counit ⟩ + y ∙ z ∎) + +unit-ε : ∀ {x} → ε ≤ (x \\ x) +unit-ε {x} = begin + ε ≤⟨ unit ⟩ + x \\ (x ∙ ε) ≈⟨ \\-cong Eq.refl (identityʳ x) ⟩ + x \\ x ∎ + +\\-identityˡ : ∀ {x} → (ε \\ x) ≈ x +\\-identityˡ {x} = antisym + (begin + ε \\ x ≈⟨ Eq.sym (identityˡ (ε \\ x)) ⟩ + ε ∙ (ε \\ x) ≤⟨ counit ⟩ + x ∎) + (proj₁ adjoint (begin + ε ∙ x ≈⟨ identityˡ x ⟩ + x ∎)) + +------------------------------------------------------------------------------ +-- The operations of a residuated pomonoid form a Galois connection + +isGaloisConnection : ∀ z → IsGaloisConnection _≈_ _≈_ _≤_ _≤_ (z ∙_) (z \\_) +isGaloisConnection z = record + { ≤₁-isPartialOrder = isPartialOrder + ; ≤₂-isPartialOrder = isPartialOrder + ; left-mono = ∙-mono₂ z + ; right-mono = \\-mono₂ z + ; adjoint = adjoint + } + +galoisConnection : ∀ z → GaloisConnection a a ℓ₁ ℓ₁ ℓ₂ ℓ₂ +galoisConnection z = record { isGaloisConnection = isGaloisConnection z } + +------------------------------------------------------------------------------ +-- If the underlying monoid is commutative, _\\_ is also a left residual + +module _ (∙-comm : Commutative _≈_ _∙_) where + + ∙-comm-\\-left-residual : ∀ {z} → Adjoint _≤_ _≤_ (_∙ z) (z \\_) + ∙-comm-\\-left-residual {z} {x} {y} = + (λ x∙z≤y → + proj₁ adjoint (begin + z ∙ x ≤⟨ reflexive (∙-comm z x) ⟩ + x ∙ z ≤⟨ x∙z≤y ⟩ + y ∎)) , + (λ x≤z\\y → + begin + x ∙ z ≤⟨ reflexive (∙-comm x z) ⟩ + z ∙ x ≤⟨ proj₂ adjoint x≤z\\y ⟩ + y ∎) + + ∙-comm-isLeftResiduatedPomonoid : + IsRightResiduatedPomonoid _≈_ _≤_ (flip _∙_) _\\_ ε + ∙-comm-isLeftResiduatedPomonoid = record + { isPartialOrder = isPartialOrder + ; ∙-mono₁ = ∙-mono₂ + ; assoc = FlipOp.associative _≈_ _∙_ Eq.sym assoc + ; identity = FlipOp.identity _≈_ _∙_ identity + ; adjoint = ∙-comm-\\-left-residual + } diff --git a/src/Function/GaloisConnection.agda b/src/Function/GaloisConnection.agda new file mode 100644 index 0000000000..dfa5913f5a --- /dev/null +++ b/src/Function/GaloisConnection.agda @@ -0,0 +1,137 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Galois connections +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Function.GaloisConnection where + +open import Data.Product using (proj₁; proj₂; _,_) +open import Level using (suc; _⊔_) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions +open import Relation.Binary.Structures using (IsPartialOrder) +open import Relation.Binary.Bundles using (Poset) +import Relation.Binary.Reasoning.PartialOrder as PosetReasoning +open import Relation.Binary.Lattice.Definitions using (Infimum; Supremum) + + +------------------------------------------------------------------------ +-- Galois connections + +record IsGaloisConnection {a b ℓ₁₁ ℓ₁₂ ℓ₂₁ ℓ₂₂} {A : Set a} {B : Set b} + (≈₁ : Rel A ℓ₁₁) (≈₂ : Rel B ℓ₁₂) + (≤₁ : Rel A ℓ₂₁) (≤₂ : Rel B ℓ₂₂) + (f : A → B) (g : B → A) + : Set (a ⊔ b ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂) where + field + ≤₁-isPartialOrder : IsPartialOrder ≈₁ ≤₁ + ≤₂-isPartialOrder : IsPartialOrder ≈₂ ≤₂ + left-mono : Monotonic₁ ≤₁ ≤₂ f + right-mono : Monotonic₁ ≤₂ ≤₁ g + adjoint : Adjoint ≤₁ ≤₂ f g + + open IsPartialOrder ≤₁-isPartialOrder public using () renaming + ( isEquivalence to ≈₁-isEquivalence + ; isPreorder to ≤₁-isPreorder + ; reflexive to ≤₁-reflexive + ; refl to ≤₁-refl + ; trans to ≤₁-trans + ; antisym to ≤₁-antisym + ; ≤-resp-≈ to ≤₁-resp-≈₁ + ; module Eq to Eq₁ + ) + + open IsPartialOrder ≤₂-isPartialOrder public using () renaming + ( isEquivalence to ≈₂-isEquivalence + ; isPreorder to ≤₂-isPreorder + ; reflexive to ≤₂-reflexive + ; refl to ≤₂-refl + ; trans to ≤₂-trans + ; antisym to ≤₂-antisym + ; ≤-resp-≈ to ≤₂-resp-≈₂ + ; module Eq to Eq₂ + ) + + unit : ∀ {x} → ≤₁ x (g (f x)) + unit = proj₁ adjoint ≤₂-refl + + counit : ∀ {x} → ≤₂ (f (g x)) x + counit = proj₂ adjoint ≤₁-refl + + -- Left adjoints preserve colimits (suprema, minima). + + ⊥-pres : ∀ {⊥₁ ⊥₂} → Minimum ≤₁ ⊥₁ → Minimum ≤₂ ⊥₂ → ≈₂ (f ⊥₁) ⊥₂ + ⊥-pres minimum₁ minimum₂ = + ≤₂-antisym (proj₂ adjoint (minimum₁ (g _))) (minimum₂ (f _)) + + ∨-pres : ∀ {_∨₁_ _∨₂_} → Supremum ≤₁ _∨₁_ → Supremum ≤₂ _∨₂_ → + ∀ x y → ≈₂ (f (x ∨₁ y)) (f x ∨₂ f y) + ∨-pres {_∨₁_} {_∨₂_} supremum₁ supremum₂ x y = + let (x≤x∨y , y≤x∨y , least₁) = supremum₁ x y + (fx≤fx∨fy , fy≤fx∨fy , least₂) = supremum₂ (f x) (f y) + in ≤₂-antisym (proj₂ adjoint (least₁ (g (f x ∨₂ f y)) + (begin + x ≤⟨ unit ⟩ + g (f x) ≤⟨ right-mono fx≤fx∨fy ⟩ + g (f x ∨₂ f y) ∎) + (begin + y ≤⟨ unit ⟩ + g (f y) ≤⟨ right-mono fy≤fx∨fy ⟩ + g (f x ∨₂ f y) ∎))) + (least₂ (f (x ∨₁ y)) (left-mono x≤x∨y) + (left-mono y≤x∨y)) + where open PosetReasoning (record { isPartialOrder = ≤₁-isPartialOrder }) + + + -- Right adjoints preserve limits (infima, maxima). + + ⊤-pres : ∀ {⊤₁ ⊤₂} → Maximum ≤₁ ⊤₁ → Maximum ≤₂ ⊤₂ → ≈₁ (g ⊤₂) ⊤₁ + ⊤-pres maximum₁ maximum₂ = + ≤₁-antisym (maximum₁ (g _)) (proj₁ adjoint (maximum₂ (f _))) + + ∧-pres : ∀ {_∧₁_ _∧₂_} → Infimum ≤₁ _∧₁_ → Infimum ≤₂ _∧₂_ → + ∀ x y → ≈₁ (g (x ∧₂ y)) (g x ∧₁ g y) + ∧-pres {_∧₁_} {_∧₂_} infimum₁ infimum₂ x y = + let (gx∧gy≤gx , gx∧gy≤gy , greatest₁) = infimum₁ (g x) (g y) + (x∧y≤x , x∧y≤y , greatest₂) = infimum₂ x y + in ≤₁-antisym (greatest₁ (g (x ∧₂ y)) (right-mono x∧y≤x) + (right-mono x∧y≤y)) + (proj₁ adjoint (greatest₂ (f (g x ∧₁ g y)) + (begin + f (g x ∧₁ g y) ≤⟨ left-mono gx∧gy≤gx ⟩ + f (g x) ≤⟨ counit ⟩ + x ∎) + (begin + f (g x ∧₁ g y) ≤⟨ left-mono gx∧gy≤gy ⟩ + f (g y) ≤⟨ counit ⟩ + y ∎))) + where open PosetReasoning (record { isPartialOrder = ≤₂-isPartialOrder }) + +record GaloisConnection a b ℓ₁₁ ℓ₁₂ ℓ₂₁ ℓ₂₂ + : Set (suc (a ⊔ b ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where + infix 4 _≈₁_ _≈₂_ _≤₁_ _≤₂_ + field + Carrier₁ : Set a + Carrier₂ : Set b + _≈₁_ : Rel Carrier₁ ℓ₁₁ + _≈₂_ : Rel Carrier₂ ℓ₁₂ + _≤₁_ : Rel Carrier₁ ℓ₂₁ + _≤₂_ : Rel Carrier₂ ℓ₂₂ + left : Carrier₁ → Carrier₂ + right : Carrier₂ → Carrier₁ + isGaloisConnection : IsGaloisConnection _≈₁_ _≈₂_ _≤₁_ _≤₂_ left right + + open IsGaloisConnection isGaloisConnection public + + ≤₁-poset : Poset a ℓ₁₁ ℓ₂₁ + ≤₁-poset = record { isPartialOrder = ≤₁-isPartialOrder } + + open Poset ≤₁-poset public using () renaming (preorder to ≤₁-preorder) + + ≤₂-poset : Poset b ℓ₁₂ ℓ₂₂ + ≤₂-poset = record { isPartialOrder = ≤₂-isPartialOrder } + + open Poset ≤₂-poset public using () renaming (preorder to ≤₂-preorder) diff --git a/src/Relation/Binary/Lattice/Properties/ResiduatedBoundedSemilattice.agda b/src/Relation/Binary/Lattice/Properties/ResiduatedBoundedSemilattice.agda new file mode 100644 index 0000000000..714b790a5c --- /dev/null +++ b/src/Relation/Binary/Lattice/Properties/ResiduatedBoundedSemilattice.agda @@ -0,0 +1,57 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of residuated bounded semilattices +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Ordered.Residuated using (ResiduatedBoundedSemilattice) + +module Relation.Binary.Lattice.Properties.ResiduatedBoundedSemilattice + {a ℓ₁ ℓ₂} (rbsl : ResiduatedBoundedSemilattice a ℓ₁ ℓ₂) + where + +open ResiduatedBoundedSemilattice rbsl + +open import Algebra.Definitions _≈_ using (LeftZero; RightZero; Zero) +open import Algebra.Ordered.Structures using (IsPosemiring) +open import Algebra.Ordered.Bundles using (Posemiring) +import Algebra.Properties.RightResiduatedPomonoid as RightResiduatedPomonoid +open import Data.Product using (_,_) +open import Function.GaloisConnection using (GaloisConnection) +open import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice + boundedJoinSemilattice using (isCommutativePomonoid) +open import Relation.Binary.Lattice.Properties.ResiduatedSemilattice + residuatedSemilattice using (∙-∨-distrib) + +open RightResiduatedPomonoid leftResiduatedPomonoid using () + renaming (galoisConnection to ∙-//-galoisConnection) +open RightResiduatedPomonoid rightResiduatedPomonoid using () + renaming (galoisConnection to ∙-\\-galoisConnection) + +-- Every residuated bounded lattice induces an (idempotent) posemiring. + +zeroˡ : LeftZero ⊥ _∙_ +zeroˡ x = ⊥-pres minimum minimum + where open GaloisConnection (∙-//-galoisConnection x) + +zeroʳ : RightZero ⊥ _∙_ +zeroʳ x = ⊥-pres minimum minimum + where open GaloisConnection (∙-\\-galoisConnection x) + +zero : Zero ⊥ _∙_ +zero = zeroˡ , zeroʳ + +isPosemiring : IsPosemiring _≈_ _≤_ _∨_ _∙_ ⊥ ε +isPosemiring = record + { +-isCommutativePomonoid = isCommutativePomonoid + ; *-mono = ∙-mono + ; *-assoc = assoc + ; *-identity = identity + ; distrib = ∙-∨-distrib + ; zero = zero + } + +posemiring : Posemiring a ℓ₁ ℓ₂ +posemiring = record { isPosemiring = isPosemiring } diff --git a/src/Relation/Binary/Lattice/Properties/ResiduatedSemilattice.agda b/src/Relation/Binary/Lattice/Properties/ResiduatedSemilattice.agda new file mode 100644 index 0000000000..a53ef0edad --- /dev/null +++ b/src/Relation/Binary/Lattice/Properties/ResiduatedSemilattice.agda @@ -0,0 +1,27 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of residuated semilattices +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Ordered.Residuated using (ResiduatedSemilattice) + +module Relation.Binary.Lattice.Properties.ResiduatedSemilattice + {a ℓ₁ ℓ₂} (rsl : ResiduatedSemilattice a ℓ₁ ℓ₂) + where + +open ResiduatedSemilattice rsl + +open import Algebra.Definitions _≈_ using (_DistributesOver_) +open import Data.Product using (_,_) +import Relation.Binary.Lattice.Properties.RightResiduatedSemilattice + as RightResiduatedSemilattice + +open RightResiduatedSemilattice rightResiduatedSemilattice +open RightResiduatedSemilattice leftResiduatedSemilattice public + using () renaming (∙-∨-distribˡ to ∙-∨-distribʳ) + +∙-∨-distrib : _∙_ DistributesOver _∨_ +∙-∨-distrib = ∙-∨-distribˡ , ∙-∨-distribʳ diff --git a/src/Relation/Binary/Lattice/Properties/RightResiduatedSemilattice.agda b/src/Relation/Binary/Lattice/Properties/RightResiduatedSemilattice.agda new file mode 100644 index 0000000000..8275d462f3 --- /dev/null +++ b/src/Relation/Binary/Lattice/Properties/RightResiduatedSemilattice.agda @@ -0,0 +1,25 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of right-residuated semilattices +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Ordered.Residuated using (RightResiduatedSemilattice) + +module Relation.Binary.Lattice.Properties.RightResiduatedSemilattice + {a ℓ₁ ℓ₂} (rrsl : RightResiduatedSemilattice a ℓ₁ ℓ₂) + where + +open RightResiduatedSemilattice rrsl + +open import Algebra.Definitions _≈_ using (_DistributesOverˡ_) +import Algebra.Properties.RightResiduatedPomonoid as RightResiduatedPomonoid +open import Function.GaloisConnection using (GaloisConnection) + +open RightResiduatedPomonoid rightResiduatedPomonoid + +∙-∨-distribˡ : _∙_ DistributesOverˡ _∨_ +∙-∨-distribˡ x y z = ∨-pres supremum supremum y z + where open GaloisConnection (galoisConnection x)