Lattices.Semidistributive¶
Semidistributivity and Whitman's condition¶
This is the Lattices.Semidistributive module of the agda-lattices library.
A lattice is join semidistributive (SD∨) if a ∨ b = a ∨ c implies
a ∨ b = a ∨ (b ∧ c), meet semidistributive (SD∧) if the dual implication
holds, and semidistributive if it is both. It satisfies Whitman's condition
(W) if s₁ ∧ s₂ ≤ t₁ ∨ t₂ implies s₁ ≤ t₁ ∨ t₂, or s₂ ≤ t₁ ∨ t₂, or
s₁ ∧ s₂ ≤ t₁, or s₁ ∧ s₂ ≤ t₂. The conditions are independent of
distributivity and of each other. Every distributive lattice is
semidistributive, yet the product of two three-element chains fails (W), since its
middle element is both a join of two smaller elements and a meet of two larger
ones (see W-irreducible below); and the five-element modular
lattice M₃ satisfies (W) and neither semidistributive law. What ties the three
together is the free lattice. Free lattices satisfy (W) (Freese, Ježek, and Nation
(1995), Theorem 1.8) and are semidistributive (Theorem 1.21, due to Jónsson and
Kiefer), and all three conditions are universal sentences, so every sublattice of
a free lattice satisfies them too. Conversely, Nation's theorem (Theorem 5.55)
says that a finite lattice is a sublattice of a free lattice if and only if it
is semidistributive and satisfies (W). Nation's proof is deep and is not
formalized here; this module supplies the three conditions it speaks of.
The module defines the predicates IsJoinSemidistributive,
IsMeetSemidistributive, IsSemidistributive,
and SatisfiesW on an arbitrary Lattice, stated
with the meet order of Classical.Properties.Lattice; proves the second half
of Corollary 1.9 of the book (in a lattice satisfying (W) every element is join
irreducible or meet irreducible); and proves that each condition passes to
sublattices and along isomorphisms. The free lattice FL X is
shown to satisfy the conditions in
Lattices.Free.Semidistributive.
The three conditions¶
Fix a lattice 𝑳, with the curried operations of
Lattice-Op and the meet order a ≤ b, meaning a ∧ b ≈ a, of
Lattice-Order. The two semidistributive laws are stated as
implications between equations, exactly as in Freese, Ježek, and Nation
(1995), Section I.3, and their conjunction is semidistributivity. Whitman's
condition is stated for binary meets and joins, with its four disjuncts grouped
in the order of ∧≤∨-inv, the inversion of the sixth of Whitman's
rules in Lattices.Free.Whitman: first the two meetands
below the join, then the meet below the two joinands. The book states (W) for
meets and joins of any finite number of elements; the binary form implies the
general one by induction on the numbers of meetands and joinands, and the two are
equivalent. All four predicates quantify their variables explicitly, so that a
proof can be applied to the elements it is about, and a decision procedure can
sweep them.
module _ (𝑳 : Lattice α ρ) where open Lattice-Op 𝑳 using ( _∧_ ; _∨_ ) open Lattice-Order 𝑳 using ( _≤_ ) open Setoid 𝔻[ proj₁ 𝑳 ] using ( _≈_ ) IsJoinSemidistributive : Type (α ⊔ ρ) IsJoinSemidistributive = ∀ a b c → a ∨ b ≈ a ∨ c → a ∨ b ≈ a ∨ (b ∧ c) IsMeetSemidistributive : Type (α ⊔ ρ) IsMeetSemidistributive = ∀ a b c → a ∧ b ≈ a ∧ c → a ∧ b ≈ a ∧ (b ∨ c) IsSemidistributive : Type (α ⊔ ρ) IsSemidistributive = IsJoinSemidistributive × IsMeetSemidistributive SatisfiesW : Type (α ⊔ ρ) SatisfiesW = ∀ s₁ s₂ t₁ t₂ → s₁ ∧ s₂ ≤ t₁ ∨ t₂ → (s₁ ≤ t₁ ∨ t₂ ⊎ s₂ ≤ t₁ ∨ t₂) ⊎ (s₁ ∧ s₂ ≤ t₁ ⊎ s₁ ∧ s₂ ≤ t₂)
Whitman's condition forbids doubly reducible elements¶
The second half of Freese, Ježek, and Nation (1995), Corollary 1.9, says that
in a lattice satisfying (W) every element is join irreducible or meet irreducible.
Read constructively, W-irreducible says that if a is written
both as a join b ∨ c and as a meet d ∧ e, then one of the four decompositions
is trivial: a equals one of the meetands, or one of the joinands. The proof
applies (W) to d ∧ e ≤ b ∨ c, which holds since both sides equal a. A
meetand below b ∨ c = a equals a, since a = d ∧ e lies below it; and if
d ∧ e = a lies below a joinand, the joinand equals a, since a = b ∨ c lies
above it.
module _ (W : SatisfiesW) where open Lattice-Order 𝑳 using ( ≤-antisym ; ≤-respˡ-≈ ; ≤-respʳ-≈ ; ≤-reflexive ; ∧-lowerˡ ; ∧-lowerʳ ; ∨-upperˡ ; ∨-upperʳ ) open Setoid 𝔻[ proj₁ 𝑳 ] using ( sym ; trans ) W-irreducible : ∀ {a b c d e} → a ≈ b ∨ c → a ≈ d ∧ e → (a ≈ d ⊎ a ≈ e) ⊎ (a ≈ b ⊎ a ≈ c) W-irreducible {a} {b} {c} {d} {e} a≈b∨c a≈d∧e = ⊎-map (⊎-map (λ d≤ → ≤-antisym (below ∧-lowerˡ) (≤-respʳ-≈ (sym a≈b∨c) d≤)) (λ e≤ → ≤-antisym (below ∧-lowerʳ) (≤-respʳ-≈ (sym a≈b∨c) e≤))) (⊎-map (λ ≤b → ≤-antisym (≤-respˡ-≈ (sym a≈d∧e) ≤b) (above ∨-upperˡ)) (λ ≤c → ≤-antisym (≤-respˡ-≈ (sym a≈d∧e) ≤c) (above ∨-upperʳ))) (W d e b c (≤-reflexive (trans (sym a≈d∧e) a≈b∨c))) where below : ∀ {x} → d ∧ e ≤ x → a ≤ x below = ≤-respˡ-≈ (sym a≈d∧e) above : ∀ {x} → x ≤ b ∨ c → x ≤ a above = ≤-respʳ-≈ (sym a≈b∨c)
Homomorphisms and the order¶
A homomorphism of lattices is a homomorphism of the underlying algebras over
Sig-Lattice, so it commutes with the curried meet and join
(hom-preserves-∧, hom-preserves-∨): its
compatibility with an operation symbol, applied at the argument tuple
pair x y, followed by interp-cong at the two argument
positions. It is therefore monotone for the meet order
(hom-preserves-≤), and an injective homomorphism also
reflects the order (hom-reflects-≤): if h x ≤ h y, then
h (x ∧ y) ≈ h x ∧ h y ≈ h x, so x ∧ y ≈ x by injectivity. These four lemmas
carry each condition from a lattice to its sublattices. The two lattices are
explicit arguments, since neither is determined by the type of a homomorphism
between their underlying algebras.
module _ (𝑲 : Lattice α ρᵃ) (𝑳 : Lattice β ρᵇ) where open Lattice-Op 𝑲 using () renaming ( _∧_ to _∧ᴷ_ ; _∨_ to _∨ᴷ_ ) open Lattice-Order 𝑲 using () renaming ( _≤_ to _≤ᴷ_ ) open Lattice-Op 𝑳 using ( _∧_ ; _∨_ ) open Lattice-Order 𝑳 using ( _≤_ ) open Setoid 𝔻[ proj₁ 𝑳 ] using ( _≈_ ; refl ; sym ; trans ) module _ (h : hom (proj₁ 𝑲) (proj₁ 𝑳)) where private f : 𝕌[ proj₁ 𝑲 ] → 𝕌[ proj₁ 𝑳 ] f = proj₁ h ⟨$⟩_ hom-preserves-∧ : ∀ x y → f (x ∧ᴷ y) ≈ f x ∧ f y hom-preserves-∧ x y = trans (IsHom.compatible (proj₂ h) {∧-Op} {pair x y}) (interp-cong (proj₁ 𝑳) ∧-Op λ { 0F → refl ; 1F → refl }) hom-preserves-∨ : ∀ x y → f (x ∨ᴷ y) ≈ f x ∨ f y hom-preserves-∨ x y = trans (IsHom.compatible (proj₂ h) {∨-Op} {pair x y}) (interp-cong (proj₁ 𝑳) ∨-Op λ { 0F → refl ; 1F → refl }) hom-preserves-≤ : ∀ {x y} → x ≤ᴷ y → f x ≤ f y hom-preserves-≤ {x} {y} x≤y = trans (sym (hom-preserves-∧ x y)) (cong (proj₁ h) x≤y) hom-reflects-≤ : IsInjective (proj₁ h) → ∀ {x y} → f x ≤ f y → x ≤ᴷ y hom-reflects-≤ inj {x} {y} fx≤fy = inj (trans (hom-preserves-∧ x y) fx≤fy)
Sublattices¶
A sublattice of 𝑳 is a lattice 𝑲 whose underlying
algebra is a subalgebra of that of 𝑳, that is, one with an injective
homomorphism into it (Setoid.Subalgebras.Basic). Each condition passes to
sublattices, which is the content of the remark after Theorem 1.8 in Freese,
Ježek, and Nation (1995): none of them refers to anything but the operations,
the equality, and universally quantified elements. The proofs follow the names of
the invariance lemmas of Setoid.Varieties.Properties (⊧-S-invar
for an identity): move the hypothesis into 𝑳 along the
homomorphism h, apply the condition there, and move the conclusion
back by injectivity, rewriting h past the operations with the lemmas above.
For the join semidistributive law, an equation a ∨ b ≈ a ∨ c in 𝑲
becomes h a ∨ h b ≈ h a ∨ h c in 𝑳, and the conclusion
h a ∨ h b ≈ h a ∨ (h b ∧ h c) there is the image of the conclusion in
𝑲. The meet semidistributive law is the dual, and
semidistributivity is the pair.
module _ (sub : proj₁ 𝑲 IsSubalgebraOf proj₁ 𝑳) where private h : hom (proj₁ 𝑲) (proj₁ 𝑳) h = proj₁ sub f : 𝕌[ proj₁ 𝑲 ] → 𝕌[ proj₁ 𝑳 ] f = proj₁ h ⟨$⟩_ open SetoidReasoning 𝔻[ proj₁ 𝑳 ] open Lattice-Op 𝑳 using ( ∧-cong ; ∨-cong ) IsJoinSemidistributive-S-invar : IsJoinSemidistributive 𝑳 → IsJoinSemidistributive 𝑲 IsJoinSemidistributive-S-invar sd a b c e = proj₂ sub (begin f (a ∨ᴷ b) ≈⟨ hom-preserves-∨ h a b ⟩ f a ∨ f b ≈⟨ sd (f a) (f b) (f c) fe ⟩ f a ∨ (f b ∧ f c) ≈˘⟨ ∨-cong refl (hom-preserves-∧ h b c) ⟩ f a ∨ f (b ∧ᴷ c) ≈˘⟨ hom-preserves-∨ h a (b ∧ᴷ c) ⟩ f (a ∨ᴷ (b ∧ᴷ c)) ∎) where fe : f a ∨ f b ≈ f a ∨ f c fe = trans (sym (hom-preserves-∨ h a b)) (trans (cong (proj₁ h) e) (hom-preserves-∨ h a c)) IsMeetSemidistributive-S-invar : IsMeetSemidistributive 𝑳 → IsMeetSemidistributive 𝑲 IsMeetSemidistributive-S-invar sd a b c e = proj₂ sub (begin f (a ∧ᴷ b) ≈⟨ hom-preserves-∧ h a b ⟩ f a ∧ f b ≈⟨ sd (f a) (f b) (f c) fe ⟩ f a ∧ (f b ∨ f c) ≈˘⟨ ∧-cong refl (hom-preserves-∨ h b c) ⟩ f a ∧ f (b ∨ᴷ c) ≈˘⟨ hom-preserves-∧ h a (b ∨ᴷ c) ⟩ f (a ∧ᴷ (b ∨ᴷ c)) ∎) where fe : f a ∧ f b ≈ f a ∧ f c fe = trans (sym (hom-preserves-∧ h a b)) (trans (cong (proj₁ h) e) (hom-preserves-∧ h a c)) IsSemidistributive-S-invar : IsSemidistributive 𝑳 → IsSemidistributive 𝑲 IsSemidistributive-S-invar (sd∨ , sd∧) = IsJoinSemidistributive-S-invar sd∨ , IsMeetSemidistributive-S-invar sd∧
For Whitman's condition, the hypothesis s₁ ∧ s₂ ≤ t₁ ∨ t₂ in 𝑲
goes to 𝑳 by monotonicity, and each of the four disjuncts that
(W) returns there comes back by hom-reflects-≤, after h is
moved back inside the meet on the left (reflect-∧ˡ) or the
join on the right (reflect-∨ʳ).
private reflect-∨ʳ : ∀ {x y z} → f x ≤ f y ∨ f z → x ≤ᴷ y ∨ᴷ z reflect-∨ʳ {x} {y} {z} p = hom-reflects-≤ h (proj₂ sub) (≤-respʳ-≈ (sym (hom-preserves-∨ h y z)) p) where open Lattice-Order 𝑳 using ( ≤-respʳ-≈ ) reflect-∧ˡ : ∀ {x y z} → f x ∧ f y ≤ f z → x ∧ᴷ y ≤ᴷ z reflect-∧ˡ {x} {y} {z} p = hom-reflects-≤ h (proj₂ sub) (≤-respˡ-≈ (sym (hom-preserves-∧ h x y)) p) where open Lattice-Order 𝑳 using ( ≤-respˡ-≈ ) SatisfiesW-S-invar : SatisfiesW 𝑳 → SatisfiesW 𝑲 SatisfiesW-S-invar W s₁ s₂ t₁ t₂ p = ⊎-map (⊎-map reflect-∨ʳ reflect-∨ʳ) (⊎-map reflect-∧ˡ reflect-∧ˡ) (W (f s₁) (f s₂) (f t₁) (f t₂) fp) where open Lattice-Order 𝑳 using ( ≤-respˡ-≈ ; ≤-respʳ-≈ ) fp : f s₁ ∧ f s₂ ≤ f t₁ ∨ f t₂ fp = ≤-respʳ-≈ (hom-preserves-∨ h t₁ t₂) (≤-respˡ-≈ (hom-preserves-∧ h s₁ s₂) (hom-preserves-≤ h p))
Isomorphic lattices¶
An isomorphism is in particular an injective homomorphism (≅→≤
of Setoid.Subalgebras.Properties), so each condition is invariant under
isomorphism as a special case of the sublattice lemmas, applied to the inverse:
if 𝑲 ≅ 𝑳 and 𝑲 satisfies a condition, then 𝑳,
being isomorphic to a sublattice of 𝑲, satisfies it too. The
direction of the lemmas follows ⊧-I-invar of
Setoid.Varieties.Properties: from the left-hand side of the isomorphism to
the right.
module _ (𝑲 : Lattice α ρᵃ) (𝑳 : Lattice β ρᵇ) (φ : proj₁ 𝑲 ≅ proj₁ 𝑳) where private sub : proj₁ 𝑳 IsSubalgebraOf proj₁ 𝑲 sub = ≅→≤ (≅-sym φ) IsJoinSemidistributive-I-invar : IsJoinSemidistributive 𝑲 → IsJoinSemidistributive 𝑳 IsJoinSemidistributive-I-invar = IsJoinSemidistributive-S-invar 𝑳 𝑲 sub IsMeetSemidistributive-I-invar : IsMeetSemidistributive 𝑲 → IsMeetSemidistributive 𝑳 IsMeetSemidistributive-I-invar = IsMeetSemidistributive-S-invar 𝑳 𝑲 sub IsSemidistributive-I-invar : IsSemidistributive 𝑲 → IsSemidistributive 𝑳 IsSemidistributive-I-invar = IsSemidistributive-S-invar 𝑳 𝑲 sub SatisfiesW-I-invar : SatisfiesW 𝑲 → SatisfiesW 𝑳 SatisfiesW-I-invar = SatisfiesW-S-invar 𝑳 𝑲 sub
Deciding the conditions in a finite lattice¶
In a finite lattice with decidable equality the three conditions are decidable, by
a sweep over the elements: triples for the semidistributive laws, quadruples for
(W). The lattice's carrier is given as a FiniteAlgebra of
Setoid.Algebras.Finite, a surjective enumeration enum : Fin card → 𝕌
together with a decision procedure _≟_ for ≈, and the meet order
inherits a decision procedure from it, since x ≤ y is the equation
x ∧ y ≈ x (_≤?_). Each condition is a universal statement
about an instance SD∨-at a b c, SD∧-at a b c,
or W-at s₁ s₂ t₁ t₂ that is decidable and respects ≈ in each
argument (SD∨-resp, SD∧-resp,
W-resp, each a rewriting by the congruence of the operations).
So all³? and all⁴? of Setoid.Algebras.Finite
decide them: the sweep runs over the enumerated elements, and the surjectivity of
the enumeration carries a positive verdict to every element. The answers have
the predicates themselves as their types, so in a concrete lattice from-yes or
from-no of a decision is a proof of the condition or of its negation, obtained
by evaluation; Lattices.Examples.M3 and
Lattices.Examples.N5 are worked examples. A lattice with n
enumerated elements costs n³ instances for each semidistributive law and n⁴
for (W).
module _ (𝑳 : Lattice α ρ) (𝑭 : FiniteAlgebra (proj₁ 𝑳)) where open FiniteAlgebra 𝑭 using ( _≟_ ) open Lattice-Op 𝑳 using ( _∧_ ; _∨_ ; ∧-cong ; ∨-cong ) open Lattice-Order 𝑳 using ( _≤_ ; ≤-respˡ-≈ ; ≤-respʳ-≈ ) open Setoid 𝔻[ proj₁ 𝑳 ] using ( _≈_ ; sym ; trans ) open SetoidReasoning 𝔻[ proj₁ 𝑳 ] private infix 4 _≤?_ _≤?_ : ∀ x y → Dec (x ≤ y) x ≤? y = (x ∧ y) ≟ x ≤-resp : ∀ {x x' y y'} → x ≈ x' → y ≈ y' → x ≤ y → x' ≤ y' ≤-resp x≈ y≈ p = ≤-respʳ-≈ y≈ (≤-respˡ-≈ x≈ p) SD∨-at SD∧-at : 𝕌[ proj₁ 𝑳 ] → 𝕌[ proj₁ 𝑳 ] → 𝕌[ proj₁ 𝑳 ] → Type ρ SD∨-at a b c = a ∨ b ≈ a ∨ c → a ∨ b ≈ a ∨ (b ∧ c) SD∧-at a b c = a ∧ b ≈ a ∧ c → a ∧ b ≈ a ∧ (b ∨ c) W-at : 𝕌[ proj₁ 𝑳 ] → 𝕌[ proj₁ 𝑳 ] → 𝕌[ proj₁ 𝑳 ] → 𝕌[ proj₁ 𝑳 ] → Type ρ W-at s₁ s₂ t₁ t₂ = s₁ ∧ s₂ ≤ t₁ ∨ t₂ → (s₁ ≤ t₁ ∨ t₂ ⊎ s₂ ≤ t₁ ∨ t₂) ⊎ (s₁ ∧ s₂ ≤ t₁ ⊎ s₁ ∧ s₂ ≤ t₂) SD∨-resp : ∀ {a a' b b' c c'} → a ≈ a' → b ≈ b' → c ≈ c' → SD∨-at a b c → SD∨-at a' b' c' SD∨-resp {a} {a'} {b} {b'} {c} {c'} a≈ b≈ c≈ h e' = begin a' ∨ b' ≈˘⟨ ∨-cong a≈ b≈ ⟩ a ∨ b ≈⟨ h (trans (∨-cong a≈ b≈) (trans e' (sym (∨-cong a≈ c≈)))) ⟩ a ∨ (b ∧ c) ≈⟨ ∨-cong a≈ (∧-cong b≈ c≈) ⟩ a' ∨ (b' ∧ c') ∎ SD∧-resp : ∀ {a a' b b' c c'} → a ≈ a' → b ≈ b' → c ≈ c' → SD∧-at a b c → SD∧-at a' b' c' SD∧-resp {a} {a'} {b} {b'} {c} {c'} a≈ b≈ c≈ h e' = begin a' ∧ b' ≈˘⟨ ∧-cong a≈ b≈ ⟩ a ∧ b ≈⟨ h (trans (∧-cong a≈ b≈) (trans e' (sym (∧-cong a≈ c≈)))) ⟩ a ∧ (b ∨ c) ≈⟨ ∧-cong a≈ (∨-cong b≈ c≈) ⟩ a' ∧ (b' ∨ c') ∎ W-resp : ∀ {s₁ s₁' s₂ s₂' t₁ t₁' t₂ t₂'} → s₁ ≈ s₁' → s₂ ≈ s₂' → t₁ ≈ t₁' → t₂ ≈ t₂' → W-at s₁ s₂ t₁ t₂ → W-at s₁' s₂' t₁' t₂' W-resp {s₁} {s₁'} {s₂} {s₂'} {t₁} {t₁'} {t₂} {t₂'} s₁≈ s₂≈ t₁≈ t₂≈ h p' = ⊎-map (⊎-map (≤-resp s₁≈ t≈) (≤-resp s₂≈ t≈)) (⊎-map (≤-resp s≈ t₁≈) (≤-resp s≈ t₂≈)) (h (≤-resp (sym s≈) (sym t≈) p')) where s≈ : s₁ ∧ s₂ ≈ s₁' ∧ s₂' s≈ = ∧-cong s₁≈ s₂≈ t≈ : t₁ ∨ t₂ ≈ t₁' ∨ t₂' t≈ = ∨-cong t₁≈ t₂≈ isJoinSemidistributive? : Dec (IsJoinSemidistributive 𝑳) isJoinSemidistributive? = all³? 𝑭 SD∨-at SD∨-resp λ a b c → (a ∨ b) ≟ (a ∨ c) →-dec (a ∨ b) ≟ (a ∨ (b ∧ c)) isMeetSemidistributive? : Dec (IsMeetSemidistributive 𝑳) isMeetSemidistributive? = all³? 𝑭 SD∧-at SD∧-resp λ a b c → (a ∧ b) ≟ (a ∧ c) →-dec (a ∧ b) ≟ (a ∧ (b ∨ c)) isSemidistributive? : Dec (IsSemidistributive 𝑳) isSemidistributive? = isJoinSemidistributive? ×-dec isMeetSemidistributive? satisfiesW? : Dec (SatisfiesW 𝑳) satisfiesW? = all⁴? 𝑭 W-at W-resp λ s₁ s₂ t₁ t₂ → s₁ ∧ s₂ ≤? t₁ ∨ t₂ →-dec ((s₁ ≤? t₁ ∨ t₂ ⊎-dec s₂ ≤? t₁ ∨ t₂) ⊎-dec (s₁ ∧ s₂ ≤? t₁ ⊎-dec s₁ ∧ s₂ ≤? t₂))