------------------------------------------------------------------------ -- The Agda standard library -- -- Some derivable properties of lattices ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Lattice.Bundles using (Lattice; Semilattice) module Algebra.Lattice.Properties.Lattice {l₁ l₂} (L : Lattice l₁ l₂) where import Algebra.Lattice.Properties.Semilattice as SemilatticeProperties open import Data.Product.Base using (_,_; swap) open Lattice L open import Algebra.Definitions _≈_ using (Idempotent; Congruent₂) open import Algebra.Structures _≈_ using (IsMagma; IsSemigroup; IsBand) open import Algebra.Lattice.Structures _≈_ using (IsLattice; IsSemilattice) open import Function.Base open import Relation.Binary.Reasoning.Setoid setoid open import Relation.Binary.Bundles using (Poset) import Relation.Binary.Lattice as R ------------------------------------------------------------------------ -- _∧_ is a semilattice ∧-idem : Idempotent _∧_ ∧-idem x = begin x ∧ x ≈⟨ ∧-congˡ (∨-absorbs-∧ _ _) ⟨ x ∧ (x ∨ x ∧ x) ≈⟨ ∧-absorbs-∨ _ _ ⟩ x ∎ ∧-isMagma : IsMagma _∧_ ∧-isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∧-cong } ∧-isSemigroup : IsSemigroup _∧_ ∧-isSemigroup = record { isMagma = ∧-isMagma ; assoc = ∧-assoc } ∧-isBand : IsBand _∧_ ∧-isBand = record { isSemigroup = ∧-isSemigroup ; idem = ∧-idem } ∧-isSemilattice : IsSemilattice _∧_ ∧-isSemilattice = record { isBand = ∧-isBand ; comm = ∧-comm } ∧-semilattice : Semilattice l₁ l₂ ∧-semilattice = record { isSemilattice = ∧-isSemilattice } open SemilatticeProperties ∧-semilattice public using ( ∧-isOrderTheoreticMeetSemilattice ; ∧-isOrderTheoreticJoinSemilattice ; ∧-orderTheoreticMeetSemilattice ; ∧-orderTheoreticJoinSemilattice ) ------------------------------------------------------------------------ -- _∨_ is a semilattice ∨-idem : Idempotent _∨_ ∨-idem x = begin x ∨ x ≈⟨ ∨-congˡ (∧-idem _) ⟨ x ∨ x ∧ x ≈⟨ ∨-absorbs-∧ _ _ ⟩ x ∎ ∨-isMagma : IsMagma _∨_ ∨-isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∨-cong } ∨-isSemigroup : IsSemigroup _∨_ ∨-isSemigroup = record { isMagma = ∨-isMagma ; assoc = ∨-assoc } ∨-isBand : IsBand _∨_ ∨-isBand = record { isSemigroup = ∨-isSemigroup ; idem = ∨-idem } ∨-isSemilattice : IsSemilattice _∨_ ∨-isSemilattice = record { isBand = ∨-isBand ; comm = ∨-comm } ∨-semilattice : Semilattice l₁ l₂ ∨-semilattice = record { isSemilattice = ∨-isSemilattice } open SemilatticeProperties ∨-semilattice public using () renaming ( ∧-isOrderTheoreticMeetSemilattice to ∨-isOrderTheoreticMeetSemilattice ; ∧-isOrderTheoreticJoinSemilattice to ∨-isOrderTheoreticJoinSemilattice ; ∧-orderTheoreticMeetSemilattice to ∨-orderTheoreticMeetSemilattice ; ∧-orderTheoreticJoinSemilattice to ∨-orderTheoreticJoinSemilattice ) ------------------------------------------------------------------------ -- The dual construction is also a lattice. ∧-∨-isLattice : IsLattice _∧_ _∨_ ∧-∨-isLattice = record { isEquivalence = isEquivalence ; ∨-comm = ∧-comm ; ∨-assoc = ∧-assoc ; ∨-cong = ∧-cong ; ∧-comm = ∨-comm ; ∧-assoc = ∨-assoc ; ∧-cong = ∨-cong ; absorptive = swap absorptive } ∧-∨-lattice : Lattice _ _ ∧-∨-lattice = record { isLattice = ∧-∨-isLattice } ------------------------------------------------------------------------ -- Every algebraic lattice can be turned into an order-theoretic one. open SemilatticeProperties ∧-semilattice public using (poset) open Poset poset using (_≤_; isPartialOrder) ∨-∧-isOrderTheoreticLattice : R.IsLattice _≈_ _≤_ _∨_ _∧_ ∨-∧-isOrderTheoreticLattice = record { isPartialOrder = isPartialOrder ; supremum = supremum ; infimum = infimum } where open R.MeetSemilattice ∧-orderTheoreticMeetSemilattice using (infimum) open R.JoinSemilattice ∨-orderTheoreticJoinSemilattice using (x≤x∨y; y≤x∨y; ∨-least) renaming (_≤_ to _≤′_) -- An alternative but equivalent interpretation of the order _≤_. sound : ∀ {x y} → x ≤′ y → x ≤ y sound {x} {y} y≈y∨x = sym $ begin x ∧ y ≈⟨ ∧-congˡ y≈y∨x ⟩ x ∧ (y ∨ x) ≈⟨ ∧-congˡ (∨-comm y x) ⟩ x ∧ (x ∨ y) ≈⟨ ∧-absorbs-∨ x y ⟩ x ∎ complete : ∀ {x y} → x ≤ y → x ≤′ y complete {x} {y} x≈x∧y = sym $ begin y ∨ x ≈⟨ ∨-congˡ x≈x∧y ⟩ y ∨ (x ∧ y) ≈⟨ ∨-congˡ (∧-comm x y) ⟩ y ∨ (y ∧ x) ≈⟨ ∨-absorbs-∧ y x ⟩ y ∎ supremum : R.Supremum _≤_ _∨_ supremum x y = sound (x≤x∨y x y) , sound (y≤x∨y x y) , λ z x≤z y≤z → sound (∨-least (complete x≤z) (complete y≤z)) ∨-∧-orderTheoreticLattice : R.Lattice _ _ _ ∨-∧-orderTheoreticLattice = record { isLattice = ∨-∧-isOrderTheoreticLattice }