Lattices.Free.Bounded¶
Homomorphisms between free lattices are bounded¶
This is the Lattices.Free.Bounded module of the agda-lattices library.
Kostinsky's Lemma 3.1 ("Projective lattices and bounded homomorphisms",
Pacific J. Math. 40 (1972), p. 115) says that a homomorphism f from a
lattice generated by a set X into a free lattice FL(Y) is upper bounded as
soon as, for each b ∈ FL(Y), only finitely many generators x ∈ X have
f x ≤ b, and lower bounded under the dual condition; his Corollary 3.2 reads
it for a homomorphism between free lattices, and for a finite X both
conditions hold outright. So every homomorphism FL(n) → FL(Y) is bounded,
which is the content of Freese, Ježek, and Nation (1995), Corollary 2.16,
for the homomorphisms the easy direction of Kostinsky's theorem needs: an
embedding of a finitely generated lattice into FL(Y), composed with an
epimorphism from FL(n) onto it (Lattices.Kostinsky).
A homomorphism FL(n) → FL(Y) is substitution by a σ : Sub (Fin n) Y
(Lattices.Free.Substitution). This module proves, for every term c over
Y, that the set {a ∈ FL(n) : a [ σ ] ≤ c} either has a greatest element or
is empty (greatestBelow?), and dually that {a : c ≤ a [ σ ]}
either has a least element or is empty (leastAbove?). The
proof is Kostinsky's, by recursion on c, with the set
{x ∈ Fin n : σ x ≤ c} listed by Whitman's decision procedure, which is where
decidable equality on Y enters. It collects, for each c, a finite list of
candidates whose images lie below c and whose join lies above every a with
a [ σ ] ≤ c: for a generator y, the generators of FL(n) sent below y,
which by rules 2 and 5 of Whitman's procedure bound every such a; for a meet
c₁ ∧ c₂, the meet of the two joins of candidates, when both exist, by rule 3;
and for a join c₁ ∨ c₂, the candidates of both joinands together with the
generators sent below the join, where rule 6, Whitman's condition in FL(Y),
sends a meet a₁ ∧ a₂ below c₁ ∨ c₂ to one of the four smaller problems.
The greatest element is the join of the candidates, when there are any. The
least element above c is read off the greatest element below dual c for the
dual substitution (Lattices.Free.Duality).
Greatest preimages below, and least preimages above¶
Fix σ : Sub (Fin n) Y. GreatestBelow σ c is a term of
FL(n) whose image lies below c and which lies above every term whose image
does; NoneBelow σ c says that no image lies below c.
LeastAbove σ c and NoneAbove σ c are the duals.
For an epimorphism onto a sublattice of FL(Y) these are the greatest and least
preimages of the elements of the sublattice, read in FL(Y) (Kostinsky's
Note 2.4).
module _ {n : ℕ} {Y : Type υ} (σ : Sub (Fin n) Y) where -- The greatest a with a [ σ ] ≤ c. record GreatestBelow (c : LatTerm Y) : Type υ where field elt : LatTerm (Fin n) below : elt [ σ ] ≤ʷ c greatest : ∀ a → a [ σ ] ≤ʷ c → a ≤ʷ elt -- No image lies below c. NoneBelow : LatTerm Y → Type υ NoneBelow c = ∀ a → ¬ (a [ σ ] ≤ʷ c) -- The least a with c ≤ a [ σ ]. record LeastAbove (c : LatTerm Y) : Type υ where field elt : LatTerm (Fin n) above : c ≤ʷ elt [ σ ] least : ∀ a → c ≤ʷ a [ σ ] → elt ≤ʷ a -- No image lies above c. NoneAbove : LatTerm Y → Type υ NoneAbove c = ∀ a → ¬ (c ≤ʷ a [ σ ])
Below the join of a list¶
a ≤⋁ʷ cs says that a lies below the join of the list cs,
and has no inhabitant for the empty list, as _≤⋁_ of
Lattices.Generation has none; it is an inductive family, so that the list
is an index Agda infers. A member lies below the join; the relation is closed
under joins on the left, and a meet lies below whatever one of its meetands
does; and it grows with the list.
module _ {n : ℕ} where infix 4 _≤⋁ʷ_ -- a lies below the join of cs; no inhabitant for the empty list. data _≤⋁ʷ_ (a : LatTerm (Fin n)) : List (LatTerm (Fin n)) → Type where ≤⋁⁺ : {d : LatTerm (Fin n)} {ds : List (LatTerm (Fin n))} → a ≤ʷ ⋁⁺ d ds → a ≤⋁ʷ (d ∷ ds) -- Nothing lies below the join of the empty list. ≤⋁ʷ-[] : ∀ {a} → ¬ (a ≤⋁ʷ []) ≤⋁ʷ-[] () -- Below the join of a nonempty list, as an inequality. ≤⋁ʷ-∷ : ∀ {a d ds} → a ≤⋁ʷ (d ∷ ds) → a ≤ʷ ⋁⁺ d ds ≤⋁ʷ-∷ (≤⋁⁺ p) = p -- A member lies below the join. ∈→≤⋁ʷ : ∀ {a cs} → a ∈ cs → a ≤⋁ʷ cs ∈→≤⋁ʷ {cs = d ∷ ds} a∈ = ≤⋁⁺ (⋁⁺-upper {w = d} {ws = ds} a∈) -- The relation is closed under joins on the left. ∨-≤⋁ʷ : ∀ {a b cs} → a ≤⋁ʷ cs → b ≤⋁ʷ cs → a ∨̇ b ≤⋁ʷ cs ∨-≤⋁ʷ (≤⋁⁺ p) (≤⋁⁺ q) = ≤⋁⁺ (∨≤ p q) -- A meet lies below whatever one of its meetands does. ∧ˡ-≤⋁ʷ : ∀ {a b cs} → a ≤⋁ʷ cs → a ∧̇ b ≤⋁ʷ cs ∧ˡ-≤⋁ʷ (≤⋁⁺ p) = ≤⋁⁺ (∧ˡ≤ p) ∧ʳ-≤⋁ʷ : ∀ {a b cs} → b ≤⋁ʷ cs → a ∧̇ b ≤⋁ʷ cs ∧ʳ-≤⋁ʷ (≤⋁⁺ p) = ≤⋁⁺ (∧ʳ≤ p) -- The relation grows with the list, on either side of a concatenation. ≤⋁ʷ-++ˡ : ∀ {a cs ds} → a ≤⋁ʷ cs → a ≤⋁ʷ (cs ++ ds) ≤⋁ʷ-++ˡ {ds = ds} (≤⋁⁺ {d} {ds'} p) = ≤⋁⁺ (≤ʷ-trans p (⋁⁺-least {w = d} {ws = ds'} λ u∈ → ⋁⁺-upper {w = d} {ws = ds' ++ ds} (∈-++⁺ˡ u∈))) ≤⋁ʷ-++ʳ : ∀ {a} cs {ds} → a ≤⋁ʷ ds → a ≤⋁ʷ (cs ++ ds) ≤⋁ʷ-++ʳ [] p = p ≤⋁ʷ-++ʳ (c ∷ cs) (≤⋁⁺ {e} {es} p) = ≤⋁⁺ (≤ʷ-trans p (⋁⁺-least {w = e} {ws = es} λ u∈ → ⋁⁺-upper {w = c} {ws = cs ++ e ∷ es} (∈-++⁺ʳ (c ∷ cs) u∈)))
The candidates¶
Fix a decision procedure for the equality of Y, so that Whitman's procedure
decides the order of FL(Y), and a substitution σ. The generators of
FL(n) sent below c form the list gens-below c, by a
filter over allFin n, and cands c is the list of candidates
described above. Two facts are proved about it: every candidate's image lies
below c (cands-below), and every a whose image lies below
c lies below the join of the candidates (cands-complete).
The second is the induction of Kostinsky's proof, on c and, for each c, on
a: the clause for a meet a₁ ∧ a₂ below a generator uses rule 5, the clause
for a meet below a join uses rule 6, Whitman's condition in FL(Y), and the
other clauses split the term by rules 2 and 3. The joins of candidate lists
substitute to joins of images (⋁⁺-[]-≤), so the join of the
candidates for c has its image below c.
module _ {n : ℕ} {Y : Type υ} (_≟ʸ_ : DecidableEquality Y) (σ : Sub (Fin n) Y) where open Decision _≟ʸ_ using ( _≤ʷ?_ ) -- The generators of FL(n) whose image lies below c. gens-below : LatTerm Y → List (Fin n) gens-below c = filter (λ x → σ x ≤ʷ? c) (allFin n) ∈-gens⁺ : ∀ {x c} → σ x ≤ʷ c → x ∈ gens-below c ∈-gens⁺ {x} {c} p = ∈-filter⁺ (λ x → σ x ≤ʷ? c) {xs = allFin n} (∈-allFin x) p ∈-gens⁻ : ∀ {x c} → x ∈ gens-below c → σ x ≤ʷ c ∈-gens⁻ {c = c} x∈ = proj₂ (∈-filter⁻ (λ x → σ x ≤ʷ? c) {xs = allFin n} x∈) -- The images of generators sent below c lie below c. gens-all′ : ∀ {c} (xs : List (Fin n)) → All (λ x → σ x ≤ʷ c) xs → All (λ a → a [ σ ] ≤ʷ c) (map ℊ xs) gens-all′ [] [] = [] gens-all′ (x ∷ xs) (p ∷ ps) = p ∷ gens-all′ xs ps gens-all : ∀ c → All (λ a → a [ σ ] ≤ʷ c) (map ℊ (gens-below c)) gens-all c = gens-all′ (gens-below c) (All.tabulate {xs = gens-below c} λ {x} x∈ → ∈-gens⁻ {x} {c} x∈) -- The join of a list of terms whose images lie below c has its image below c. ⋁⁺-[]-≤ : ∀ {c d ds} → All (λ a → a [ σ ] ≤ʷ c) (d ∷ ds) → ⋁⁺ d ds [ σ ] ≤ʷ c ⋁⁺-[]-≤ {ds = []} (p ∷ []) = p ⋁⁺-[]-≤ {ds = _ ∷ _} (p ∷ ps) = ∨≤ p (⋁⁺-[]-≤ ps) -- The candidates for a meet: the meet of the two joins, when both lists are nonempty. meet-cands : List (LatTerm (Fin n)) → List (LatTerm (Fin n)) → List (LatTerm (Fin n)) meet-cands [] _ = [] meet-cands (_ ∷ _) [] = [] meet-cands (d ∷ ds) (e ∷ es) = (⋁⁺ d ds ∧̇ ⋁⁺ e es) ∷ [] -- The candidates: terms with image below c whose join bounds every such term. cands : LatTerm Y → List (LatTerm (Fin n)) cands (ℊ y) = map ℊ (gens-below (ℊ y)) cands (c₁ ∧̇ c₂) = meet-cands (cands c₁) (cands c₂) cands (c₁ ∨̇ c₂) = cands c₁ ++ cands c₂ ++ map ℊ (gens-below (c₁ ∨̇ c₂)) -- The candidates of a meet lie below it. meet-cands-below : ∀ {c₁ c₂ cs ds} → All (λ a → a [ σ ] ≤ʷ c₁) cs → All (λ a → a [ σ ] ≤ʷ c₂) ds → All (λ a → a [ σ ] ≤ʷ c₁ ∧̇ c₂) (meet-cands cs ds) meet-cands-below {cs = []} _ _ = [] meet-cands-below {cs = _ ∷ _} _ [] = [] meet-cands-below {cs = _ ∷ _} ps@(_ ∷ _) qs@(_ ∷ _) = ≤∧ (∧ˡ≤ (⋁⁺-[]-≤ ps)) (∧ʳ≤ (⋁⁺-[]-≤ qs)) ∷ [] -- Every candidate's image lies below c. cands-below : ∀ c → All (λ a → a [ σ ] ≤ʷ c) (cands c) cands-below (ℊ y) = gens-all (ℊ y) cands-below (c₁ ∧̇ c₂) = meet-cands-below (cands-below c₁) (cands-below c₂) cands-below (c₁ ∨̇ c₂) = ++⁺ (All.map ≤∨ˡ (cands-below c₁)) (++⁺ (All.map ≤∨ʳ (cands-below c₂)) (gens-all (c₁ ∨̇ c₂))) -- Below both joins of candidates means below the candidate for the meet. meet-complete : ∀ {a cs ds} → a ≤⋁ʷ cs → a ≤⋁ʷ ds → a ≤⋁ʷ meet-cands cs ds meet-complete (≤⋁⁺ p) (≤⋁⁺ q) = ≤⋁⁺ (≤∧ p q) -- Every a with a [ σ ] ≤ c lies below the join of the candidates for c. cands-complete : ∀ c a → a [ σ ] ≤ʷ c → a ≤⋁ʷ cands c cands-complete (ℊ y) (ℊ x) p = ∈→≤⋁ʷ (∈-map⁺ ℊ (∈-gens⁺ p)) cands-complete (ℊ y) (a₁ ∨̇ a₂) p = let (p₁ , p₂) = ∨≤-inv p in ∨-≤⋁ʷ (cands-complete (ℊ y) a₁ p₁) (cands-complete (ℊ y) a₂ p₂) cands-complete (ℊ y) (a₁ ∧̇ a₂) p = [ (λ p₁ → ∧ˡ-≤⋁ʷ (cands-complete (ℊ y) a₁ p₁)) , (λ p₂ → ∧ʳ-≤⋁ʷ (cands-complete (ℊ y) a₂ p₂)) ]′ (∧≤ℊ-inv p) cands-complete (c₁ ∧̇ c₂) a p = let (p₁ , p₂) = ≤∧-inv p in meet-complete (cands-complete c₁ a p₁) (cands-complete c₂ a p₂) cands-complete (c₁ ∨̇ c₂) (ℊ x) p = ∈→≤⋁ʷ (∈-++⁺ʳ (cands c₁) (∈-++⁺ʳ (cands c₂) (∈-map⁺ ℊ (∈-gens⁺ p)))) cands-complete (c₁ ∨̇ c₂) (a₁ ∨̇ a₂) p = let (p₁ , p₂) = ∨≤-inv p in ∨-≤⋁ʷ (cands-complete (c₁ ∨̇ c₂) a₁ p₁) (cands-complete (c₁ ∨̇ c₂) a₂ p₂) cands-complete (c₁ ∨̇ c₂) (a₁ ∧̇ a₂) p = [ [ (λ q → ∧ˡ-≤⋁ʷ (cands-complete (c₁ ∨̇ c₂) a₁ q)) , (λ q → ∧ʳ-≤⋁ʷ (cands-complete (c₁ ∨̇ c₂) a₂ q)) ]′ , [ (λ q → ≤⋁ʷ-++ˡ (cands-complete c₁ (a₁ ∧̇ a₂) q)) , (λ q → ≤⋁ʷ-++ʳ (cands c₁) (≤⋁ʷ-++ˡ (cands-complete c₂ (a₁ ∧̇ a₂) q))) ]′ ]′ (∧≤∨-inv p)
Kostinsky's Lemma 3.1¶
With the candidates in hand, the dichotomy is immediate: an empty candidate
list says that nothing maps below c, and a nonempty one has its join as the
greatest element.
-- From a candidate list to the dichotomy. fromCands : (c : LatTerm Y) (cs : List (LatTerm (Fin n))) → All (λ a → a [ σ ] ≤ʷ c) cs → (∀ a → a [ σ ] ≤ʷ c → a ≤⋁ʷ cs) → GreatestBelow σ c ⊎ NoneBelow σ c fromCands c [] _ compl = inj₂ λ a p → ≤⋁ʷ-[] (compl a p) fromCands c (d ∷ ds) ps compl = inj₁ (record { elt = ⋁⁺ d ds ; below = ⋁⁺-[]-≤ ps ; greatest = λ a p → ≤⋁ʷ-∷ (compl a p) }) -- Lemma 3.1 (1): below each c there is a greatest image, or none. greatestBelow? : (c : LatTerm Y) → GreatestBelow σ c ⊎ NoneBelow σ c greatestBelow? c = fromCands c (cands c) (cands-below c) (cands-complete c)
The dual¶
The least image above c is the dual of the greatest image below dual c
under the dual substitution dual ∘ σ, since c ≤ a [ σ ] exactly when
dual a [ dual ∘ σ ] ≤ dual c (dual-[] of
Lattices.Free.Substitution with the antitone, order-reflecting
dual).
module _ {n : ℕ} {Y : Type υ} (_≟ʸ_ : DecidableEquality Y) (σ : Sub (Fin n) Y) where private σᵈ : Sub (Fin n) Y σᵈ = dual ∘ σ -- c ≤ a [ σ ] exactly when dual a [ σᵈ ] ≤ dual c. flip : ∀ a {c} → c ≤ʷ a [ σ ] → dual a [ σᵈ ] ≤ʷ dual c flip a p = subst (_≤ʷ dual _) (dual-[] a σ) (dual-antitone p) unflip : ∀ a {c} → dual a [ σᵈ ] ≤ʷ dual c → c ≤ʷ a [ σ ] unflip a p = dual-reflects (subst (_≤ʷ dual _) (sym (dual-[] a σ)) p) -- The dichotomy for the dual substitution at dual c gives the dichotomy at c. fromDual : (c : LatTerm Y) → GreatestBelow σᵈ (dual c) ⊎ NoneBelow σᵈ (dual c) → LeastAbove σ c ⊎ NoneAbove σ c fromDual c (inj₂ none) = inj₂ λ a p → none (dual a) (flip a p) fromDual c (inj₁ gb) = inj₁ (record { elt = dual elt ; above = unflip (dual elt) (subst (λ u → u [ σᵈ ] ≤ʷ dual c) (sym (dual-involutive elt)) below) ; least = λ a p → subst (dual elt ≤ʷ_) (dual-involutive a) (dual-antitone (greatest (dual a) (flip a p))) }) where open GreatestBelow gb -- Lemma 3.1 (2): above each c there is a least image, or none. leastAbove? : (c : LatTerm Y) → LeastAbove σ c ⊎ NoneAbove σ c leastAbove? c = fromDual c (greatestBelow? _≟ʸ_ σᵈ (dual c))
The module checks in well under a second of its own.