Lattices.Free.Membership¶
Membership in a finitely generated sublattice of a free lattice¶
This is the Lattices.Free.Membership module of the agda-lattices library.
A finitely generated sublattice of a free lattice FL(Y) is the image of a
homomorphism σ : FL(n) → FL(Y), which is substitution by
σ : Sub (Fin n) Y (Lattices.Free.Substitution). Whether an element w
of FL(Y) lies in it is decidable, when the equality of Y is
(inImage?). The decision is the least preimage: the
homomorphism is lower bounded, so the elements a of FL(n) whose images lie
above w have a least one β(w) when there are any, and then w lies in the
image exactly when β(w) is sent to w (inImage⇔β): if
a [ σ ] = w, then β(w) ≤ a, so w ≤ β(w) [ σ ] ≤ a [ σ ] = w. And there are
elements above w exactly when w lies below the image of the top of
FL(n) (leastAbove⇔below-top), for n ≥ 1, where FL(n) has
a top (Lattices.Free.Extrema). Together, w lies in the image exactly
when w ≤ σ(x₁ ∨ ⋯ ∨ xₙ) and β(w) [ σ ] = w (inImage⇔).
The image is all of FL(Y) exactly when every generator is one of the images
σ i (onto⇔generators-are-images, by Corollary 1.6), and
for finitely many generators it is not all of FL(Y) exactly when some
generator is none of them (not-onto⇔missed-generator).
Freese, Ježek, and Nation (1995) obtain the lower bound β of a
homomorphism from a finitely generated lattice to FL(Y) from Theorem 2.6 and
Lemma 2.7, with D(FL(Y)) = FL(Y) (Corollary 2.11), and compute it by
Corollary 2.8, which defines β(w) exactly for w ≤ σ(1). This module takes
it from Kostinsky's Lemma 3.1 instead, leastAbove? of
Lattices.Free.Bounded, which computes β(w) by recursion on w, or
reports that no image lies above w.
The image of a substitution¶
InImage w says that w is the image of an element of
FL(n). With the equality of Y decided, leastAbove?
returns the least preimage above w, or that there is none
(NoneAbove). If w is an image, the least preimage β
exists and its image lies below that of every preimage above w
(least-image), hence below w, and above w by definition:
β is sent to w (inImage⇔β). The decision
(inImage?) asks leastAbove? for β and then
decides β [ σ ] ≤ʷ w by Whitman's procedure.
module _ {n : ℕ} {Y : Type υ} (σ : Sub (Fin n) Y) where -- w lies in the sublattice generated by σ, the image of FL(n) under σ. InImage : LatTerm Y → Type υ InImage w = Σ[ a ∈ LatTerm (Fin n) ] a [ σ ] ≈ʷ w -- The image of the least preimage above w lies below every image above w. least-image : ∀ {w} (β : LeastAbove σ w) → ∀ a → w ≤ʷ a [ σ ] → LeastAbove.elt β [ σ ] ≤ʷ a [ σ ] least-image β a p = []-mono σ (LeastAbove.least β a p) module _ {n : ℕ} {Y : Type υ} (_≟ʸ_ : DecidableEquality Y) (σ : Sub (Fin n) Y) where open Decision _≟ʸ_ using ( _≤ʷ?_ ) private -- The least preimage above w, when some image lies above w. least-from : ∀ {w} a → w ≤ʷ a [ σ ] → LeastAbove σ w ⊎ NoneAbove σ w → LeastAbove σ w least-from a p (inj₁ β) = β least-from a p (inj₂ none) = ⊥-elim (none a p) -- The least preimage above w, given an image above w. β-above : ∀ {w} a → w ≤ʷ a [ σ ] → LeastAbove σ w β-above {w} a p = least-from a p (leastAbove? _≟ʸ_ σ w) -- w lies in the image exactly when the least preimage above it exists and is sent to w. inImage⇔β : ∀ {w} → InImage σ w ⇔ (Σ[ β ∈ LeastAbove σ w ] LeastAbove.elt β [ σ ] ≈ʷ w) inImage⇔β {w} = mk⇔ to from where to : InImage σ w → Σ[ β ∈ LeastAbove σ w ] LeastAbove.elt β [ σ ] ≈ʷ w to (a , e₁ , e₂) = β-above a e₂ , ≤ʷ-trans (least-image σ (β-above a e₂) a e₂) e₁ , LeastAbove.above (β-above a e₂) from : Σ[ β ∈ LeastAbove σ w ] LeastAbove.elt β [ σ ] ≈ʷ w → InImage σ w from (β , e) = LeastAbove.elt β , e private -- Decide membership from the answer of leastAbove?. decide : ∀ {w} → LeastAbove σ w ⊎ NoneAbove σ w → Dec (InImage σ w) decide (inj₂ none) = no λ (a , _ , e) → none a e decide {w} (inj₁ β) = map′ (λ p → LeastAbove.elt β , p , LeastAbove.above β) (λ (a , e₁ , e₂) → ≤ʷ-trans (least-image σ β a e₂) e₁) (LeastAbove.elt β [ σ ] ≤ʷ? w) -- Membership in a finitely generated sublattice of FL(Y) is decidable. inImage? : ∀ w → Dec (InImage σ w) inImage? w = decide (leastAbove? _≟ʸ_ σ w)
Corollary 2.8: where the least preimage exists¶
Let ⊤ be a top element of FL(n), which exists exactly when n ≥ 1
(Lattices.Free.Extrema): the join x₁ ∨ ⋯ ∨ xₙ of the generators, or
anything equal to it. A least preimage above w exists exactly when w lies
below ⊤ [ σ ] (leastAbove⇔below-top): every preimage lies
below ⊤, so its image below ⊤ [ σ ]; and ⊤ is itself a preimage above
such a w. So w lies in the image exactly when w ≤ ⊤ [ σ ] and the least
preimage it then has is sent to w (inImage⇔), the form of
the criterion with the two conditions apart.
module _ ((⊤₁ , ⊤₂) : TopOf (FL (Fin n))) where -- The image of the top. image-of-top : LatTerm Y image-of-top = ⊤₁ [ σ ] -- A least preimage above w exists exactly when w lies below the image of the top. leastAbove⇔below-top : ∀ {w} → LeastAbove σ w ⇔ w ≤ʷ image-of-top leastAbove⇔below-top {w} = mk⇔ to (β-above ⊤₁) where to : LeastAbove σ w → w ≤ʷ image-of-top to β = ≤ʷ-trans (LeastAbove.above β) ([]-mono σ (≤→≤ʷ (⊤₂ (LeastAbove.elt β)))) -- w is in the image exactly when it is below the image of the top and its -- least preimage is sent to it. inImage⇔ : ∀ {w} → InImage σ w ⇔ (Σ[ p ∈ w ≤ʷ image-of-top ] LeastAbove.elt (β-above ⊤₁ p) [ σ ] ≈ʷ w) inImage⇔ {w} = mk⇔ to from where to : InImage σ w → Σ[ p ∈ w ≤ʷ image-of-top ] LeastAbove.elt (β-above ⊤₁ p) [ σ ] ≈ʷ w to (a , e₁ , e₂) = p , ≤ʷ-trans (least-image σ (β-above ⊤₁ p) a e₂) e₁ , LeastAbove.above (β-above ⊤₁ p) where p : w ≤ʷ image-of-top p = Equivalence.to leastAbove⇔below-top (β-above a e₂) from : Σ[ p ∈ w ≤ʷ image-of-top ] LeastAbove.elt (β-above ⊤₁ p) [ σ ] ≈ʷ w → InImage σ w from (p , e) = LeastAbove.elt (β-above ⊤₁ p) , e
Onto exactly when every generator is an image¶
The image of σ is all of FL(Y) exactly when it contains every generator
(onto⇔generators): the image is closed under the
operations, so it contains every term once it contains the generators. By
Corollary 1.6 a generator lies in the image only when it is one of the images
σ i (generator-in-image of Lattices.Free.Generation),
so σ is onto exactly when every generator is one of the σ i
(onto⇔generators-are-images). With finitely many generators
the condition is decidable, so σ fails to be onto exactly when some generator
is none of the images (not-onto⇔missed-generator); for a
self-embedding of FL(n) this says that it is proper exactly when it misses a
generator.
module _ {n : ℕ} {Y : Type υ} (σ : Sub (Fin n) Y) where -- The image is everything exactly when it contains every generator. onto⇔generators : (∀ w → InImage σ w) ⇔ (∀ y → InImage σ (ℊ y)) onto⇔generators = mk⇔ (λ onto y → onto (ℊ y)) from where from : (∀ y → InImage σ (ℊ y)) → ∀ w → InImage σ w from gens (ℊ y) = gens y from gens (u ∧̇ v) = let (a , e) = from gens u ; (b , f) = from gens v in a ∧̇ b , ∧̇-cong e f from gens (u ∨̇ v) = let (a , e) = from gens u ; (b , f) = from gens v in a ∨̇ b , ∨̇-cong e f -- Corollary 1.6: the image is everything exactly when every generator is one of -- the images. onto⇔generators-are-images : (∀ w → InImage σ w) ⇔ (∀ y → Σ[ i ∈ Fin n ] ℊ y ≈ʷ σ i) onto⇔generators-are-images = mk⇔ to from where to : (∀ w → InImage σ w) → ∀ y → Σ[ i ∈ Fin n ] ℊ y ≈ʷ σ i to onto y = let (a , e) = onto (ℊ y) in generator-in-image σ a (≈ʷ-sym e) from : (∀ y → Σ[ i ∈ Fin n ] ℊ y ≈ʷ σ i) → ∀ w → InImage σ w from images = Equivalence.from onto⇔generators λ y → let (i , e) = images y in ℊ i , ≈ʷ-sym e module _ {n m : ℕ} (σ : Sub (Fin n) (Fin m)) where open Decision (_≟_ {m}) using ( _≈ʷ?_ ) -- The image is not everything exactly when some generator is none of the images. not-onto⇔missed-generator : (¬ (∀ w → InImage σ w)) ⇔ (Σ[ y ∈ Fin m ] ∀ i → ¬ (ℊ y ≈ʷ σ i)) not-onto⇔missed-generator = mk⇔ to from where images : ∀ y → Dec (Σ[ i ∈ Fin n ] ℊ y ≈ʷ σ i) images y = any? λ i → ℊ y ≈ʷ? σ i to : ¬ (∀ w → InImage σ w) → Σ[ y ∈ Fin m ] ∀ i → ¬ (ℊ y ≈ʷ σ i) to not-onto = let (y , ¬image) = ¬∀⟶∃¬ m _ images λ all → not-onto (Equivalence.from (onto⇔generators-are-images σ) all) in y , λ i e → ¬image (i , e) from : Σ[ y ∈ Fin m ] (∀ i → ¬ (ℊ y ≈ʷ σ i)) → ¬ (∀ w → InImage σ w) from (y , missed) onto = let (i , e) = Equivalence.to (onto⇔generators-are-images σ) onto y in missed i e
Examples¶
In FL(3) on x, y, z, the sublattice generated by x ∨ y and z
contains (x ∨ y) ∧ z and z ∨ (x ∨ y), and contains neither x nor
x ∨ z, each decided by inImage? and read off by
from-yes or from-no.
private x y z : LatTerm (Fin 3) x = ℊ 0F y = ℊ 1F z = ℊ 2F -- The pair x ∨ y, z. τ : Sub (Fin 2) (Fin 3) τ 0F = x ∨̇ y τ 1F = z -- (x ∨ y) ∧ z and z ∨ (x ∨ y) lie in ⟨x ∨ y, z⟩. meet-in : InImage τ ((x ∨̇ y) ∧̇ z) meet-in = from-yes (inImage? _≟_ τ ((x ∨̇ y) ∧̇ z)) join-in : InImage τ (z ∨̇ (x ∨̇ y)) join-in = from-yes (inImage? _≟_ τ (z ∨̇ (x ∨̇ y))) -- x and x ∨ z do not. x-out : ¬ InImage τ x x-out = from-no (inImage? _≟_ τ x) x∨z-out : ¬ InImage τ (x ∨̇ z) x∨z-out = from-no (inImage? _≟_ τ (x ∨̇ z))