Lattices.Free.Generation¶
Free generating sets¶
This is the Lattices.Free.Generation module of the agda-lattices library.
When does a family of elements of a free lattice generate a sublattice that is itself free, with the family as its free generating set? Freese, Ježek, and Nation (1995), Corollary 1.13, answers: exactly when no member lies below the join of finitely many other members, and no member lies above the meet of finitely many other members. For a finite family the condition quantifies over finitely many subfamilies, and each instance is a single decision of Whitman's procedure, so the criterion is decidable.
A family is a substitution σ from an index set I to the generators X
(Lattices.Free.Substitution), and "the sublattice
generated by the family is freely generated by it" means that the homomorphism
FL(I) → FL(X) the substitution induces is injective: it is then an isomorphism
of FL(I) onto its image, which is the sublattice generated by the family. The
module proves the following:
- Sufficiency (Corollary 1.12). If the family satisfies the condition, the
induced homomorphism reflects Whitman's order, hence is injective. The proof
is the book's: the images of the generators obey, inside the sublattice they
generate, the six rules of Whitman's procedure (Theorem 1.11), so an
inequality between images is derived by the same rules as the inequality
between the terms. Rules 2, 3, and 6 hold in all of
FL(X); rule 1 is the condition for a single other member; and rules 4 and 5, that each member is join prime and meet prime within the sublattice, are Lemma 1.3, which extends primality from joins of members to joins of arbitrary elements of the sublattice. - Necessity. If the induced homomorphism is injective, the condition holds,
because the generators of
FL(I)are join prime and meet prime. - The decision procedure (
freelyGenerates?), for an index set that is enumerated and has decidable equality. - Corollary 1.6(1): a free generator lies in the sublattice generated by a family only if it equals a member of the family. Through an embedding this decides when one free sublattice properly contains another.
Joins and meets of finite lists¶
The condition of Corollary 1.13 speaks of the join of a finite set of members,
and the set may be empty, while a free lattice on infinitely many generators has
no least element. So the statement "b lies below the join of the list G" is
a relation of its own, b ≤⋁ G, false for the empty list and
b ≤ʷ ⋁⁺ g gs for a list g ∷ gs; dually G ⋀≤ b. A member of
a list lies below its join (∈→≤⋁); the relation is closed
downward on the left (≤ʷ-≤⋁) and under joins on the left
(∨-≤⋁); and if every member of F lies below the join of G,
anything below the join of F does too (≤⋁-cover); dually
for meets (∈→⋀≤, ⋀≤-cover).
infix 4 _≤⋁_ _⋀≤_ _≤⋁_ : {X : Type χ} → LatTerm X → List (LatTerm X) → Type χ b ≤⋁ [] = ⊥ b ≤⋁ (g ∷ gs) = b ≤ʷ ⋁⁺ g gs _⋀≤_ : {X : Type χ} → List (LatTerm X) → LatTerm X → Type χ [] ⋀≤ b = ⊥ (g ∷ gs) ⋀≤ b = ⋀⁺ g gs ≤ʷ b ∈→≤⋁ : b ∈ G → b ≤⋁ G ∈→≤⋁ {G = []} () ∈→≤⋁ {G = _ ∷ _} b∈ = ⋁⁺-upper b∈ ≤ʷ-≤⋁ : b ≤ʷ c → c ≤⋁ G → b ≤⋁ G ≤ʷ-≤⋁ {G = []} _ () ≤ʷ-≤⋁ {G = _ ∷ _} p q = ≤ʷ-trans p q ∨-≤⋁ : u ≤⋁ G → v ≤⋁ G → u ∨̇ v ≤⋁ G ∨-≤⋁ {G = []} () _ ∨-≤⋁ {G = _ ∷ _} p q = ∨≤ p q ≤⋁-cover : b ≤⋁ F → (∀ {f} → f ∈ F → f ≤⋁ G) → b ≤⋁ G ≤⋁-cover {F = []} () _ ≤⋁-cover {F = _ ∷ _} {G = []} _ h = h (here refl) ≤⋁-cover {F = _ ∷ _} {G = _ ∷ _} p h = ≤ʷ-trans p (⋁⁺-least h) ∈→⋀≤ : b ∈ G → G ⋀≤ b ∈→⋀≤ {G = []} () ∈→⋀≤ {G = _ ∷ _} b∈ = ⋀⁺-lower b∈ ⋀≤-cover : F ⋀≤ b → (∀ {f} → f ∈ F → G ⋀≤ f) → G ⋀≤ b ⋀≤-cover {F = []} () _ ⋀≤-cover {F = _ ∷ _} {G = []} _ h = h (here refl) ⋀≤-cover {F = _ ∷ _} {G = _ ∷ _} p h = ≤ʷ-trans (⋀⁺-greatest h) p
The dual of a meet of a list is the join of the duals (dual-⋀⁺),
which is how a statement about meets of members becomes one about joins.
dual-⋀⁺ : (u : LatTerm X) (us : List (LatTerm X)) → dual (⋀⁺ u us) ≡ ⋁⁺ (dual u) (map dual us) dual-⋀⁺ u [] = refl dual-⋀⁺ u (w ∷ ws) = cong (dual u ∨̇_) (dual-⋀⁺ w ws)
The condition of Corollary 1.13¶
A family σ indexed by I satisfies the join condition
(JoinCondition) if a member σ i lies below the join of the
members indexed by a finite list Y only when i is in Y, and the meet
condition (MeetCondition) dually. It freely generates
(FreelyGenerates) if it satisfies both. Membership is that of
indices, so two indices with equal members violate the condition, as they must:
the homomorphism from FL(I) then identifies two generators. (Taking Y to be
the single index j gives the case σ i ≤ σ j, so the condition contains rule 1
of Whitman's procedure for the members.)
JoinCondition : {I : Type ι} {X : Type χ} → Sub I X → Type (ι ⊔ χ) JoinCondition {I = I} σ = ∀ {i : I} {Y : List I} → σ i ≤⋁ map σ Y → i ∈ Y MeetCondition : {I : Type ι} {X : Type χ} → Sub I X → Type (ι ⊔ χ) MeetCondition {I = I} σ = ∀ {i : I} {Y : List I} → map σ Y ⋀≤ σ i → i ∈ Y FreelyGenerates : {I : Type ι} {X : Type χ} → Sub I X → Type (ι ⊔ χ) FreelyGenerates σ = JoinCondition σ × MeetCondition σ
Lemma 1.3: primality spreads through the generated sublattice¶
Fix an element a of FL(X). Say that a is prime over a predicate P
(PrimeOn) if, whenever a lies below the join of a finite list
of elements satisfying P, it lies below one of them. Freese, Ježek, and Nation
(1995), Lemma 1.3, says that if a is prime over the generators of a lattice,
it is prime over the whole lattice. The proof grows the predicate one element at
a time and shows that primality survives adding the meet or the join of two
elements already present. Primality is antitone in the predicate
(PrimeOn-⊆).
module _ {X : Type χ} (a : LatTerm X) where PrimeOn : (LatTerm X → Type ℓ) → Type (χ ⊔ ℓ) PrimeOn P = ∀ {F} → All P F → a ≤⋁ F → Any (a ≤ʷ_) F PrimeOn-⊆ : {P : LatTerm X → Type ℓ} {Q : LatTerm X → Type ℓ′} → (∀ {e} → Q e → P e) → PrimeOn P → PrimeOn Q PrimeOn-⊆ Q⊆P pr qs = pr (All.map Q⊆P qs)
Both steps rewrite a list F of elements satisfying P or equal to a new element
t. squash w F ps replaces each occurrence of t in F by
w, using the proof ps to tell the occurrences apart; the result satisfies P
throughout when w does (squash-All). Each member of F
survives the replacement or is t, with w in its place
(squash-∈), so if t lies below w, every member of F lies
below the join of the result (squash-cover). And if a lies
below a member of the result, it lies below a member of F, or below w with
t a member of F (squash-Any).
module _ {P : LatTerm X → Type ℓ} {t : LatTerm X} where squash : (w : LatTerm X) (F : List (LatTerm X)) → All (λ e → P e ⊎ e ≡ t) F → List (LatTerm X) squash w [] [] = [] squash w (e ∷ F) (inj₁ _ ∷ ps) = e ∷ squash w F ps squash w (e ∷ F) (inj₂ _ ∷ ps) = w ∷ squash w F ps squash-All : (w : LatTerm X) → P w → (ps : All (λ e → P e ⊎ e ≡ t) F) → All P (squash w F ps) squash-All w pw [] = [] squash-All w pw (inj₁ pe ∷ ps) = pe ∷ squash-All w pw ps squash-All w pw (inj₂ _ ∷ ps) = pw ∷ squash-All w pw ps squash-∈ : (w : LatTerm X) (ps : All (λ e → P e ⊎ e ≡ t) F) → b ∈ F → b ∈ squash w F ps ⊎ (b ≡ t × w ∈ squash w F ps) squash-∈ w (inj₁ _ ∷ ps) (here refl) = inj₁ (here refl) squash-∈ w (inj₂ e≡t ∷ ps) (here refl) = inj₂ (e≡t , here refl) squash-∈ w (inj₁ _ ∷ ps) (there b∈) = ⊎-map there (map₂ there) (squash-∈ w ps b∈) squash-∈ w (inj₂ _ ∷ ps) (there b∈) = ⊎-map there (map₂ there) (squash-∈ w ps b∈) squash-cover : (w : LatTerm X) → t ≤ʷ w → (ps : All (λ e → P e ⊎ e ≡ t) F) → b ∈ F → b ≤⋁ squash w F ps squash-cover w t≤w ps b∈ = [ ∈→≤⋁ , (λ (b≡t , w∈) → ≤ʷ-≤⋁ (subst (_≤ʷ w) (sym b≡t) t≤w) (∈→≤⋁ w∈)) ]′ (squash-∈ w ps b∈) squash-Any : (w : LatTerm X) (ps : All (λ e → P e ⊎ e ≡ t) F) → Any (a ≤ʷ_) (squash w F ps) → Any (a ≤ʷ_) F ⊎ (a ≤ʷ w × t ∈ F) squash-Any w (inj₁ _ ∷ ps) (here p) = inj₁ (here p) squash-Any w (inj₂ e≡t ∷ ps) (here p) = inj₂ (p , here (sym e≡t)) squash-Any w (inj₁ _ ∷ ps) (there r) = ⊎-map there (map₂ there) (squash-Any w ps r) squash-Any w (inj₂ _ ∷ ps) (there r) = ⊎-map there (map₂ there) (squash-Any w ps r)
Adding a meet (∧-step). Suppose a is prime over P, the
elements u and v satisfy P, and a lies below the join of a list F of
elements satisfying P or equal to u ∧ v. Replacing u ∧ v by u only
raises the join, so primality over P puts a below a member of F, or below
u; likewise with v. If both answers are u and v, then a lies below
u ∧ v, which is a member of F. The two answers are combined by
meet-of-two.
meet-of-two : Any (a ≤ʷ_) F ⊎ (a ≤ʷ u × u ∧̇ v ∈ F) → Any (a ≤ʷ_) F ⊎ (a ≤ʷ v × u ∧̇ v ∈ F) → Any (a ≤ʷ_) F meet-of-two (inj₁ q) _ = q meet-of-two (inj₂ _) (inj₁ q) = q meet-of-two (inj₂ (a≤u , m∈)) (inj₂ (a≤v , _)) = Any.map (λ { refl → ≤∧ a≤u a≤v }) m∈ ∧-step : {P : LatTerm X → Type ℓ} → PrimeOn P → P u → P v → PrimeOn (λ e → P e ⊎ e ≡ u ∧̇ v) ∧-step {u = u} {v} pr pu pv ps a≤ = meet-of-two (squash-Any u ps (pr (squash-All u pu ps) (≤⋁-cover a≤ (squash-cover u ∧̇-lowerˡ ps)))) (squash-Any v ps (pr (squash-All v pv ps) (≤⋁-cover a≤ (squash-cover v ∧̇-lowerʳ ps))))
Adding a join (∨-step). Now replace u ∨ v in F by u in
one copy of the list and by v in another, and concatenate the copies. Every
member of F lies below the join of the result, u ∨ v because both u and v
are in it, so primality over P puts a below a member of one copy: a member of
F, or u or v, each of which lies below u ∨ v, a member of F
(squash-settle).
squash-settle : (a ≤ʷ w → a ≤ʷ t) → Any (a ≤ʷ_) F ⊎ (a ≤ʷ w × t ∈ F) → Any (a ≤ʷ_) F squash-settle f (inj₁ q) = q squash-settle f (inj₂ (a≤w , t∈)) = Any.map (λ { refl → f a≤w }) t∈ ∨-step : {P : LatTerm X → Type ℓ} → PrimeOn P → P u → P v → PrimeOn (λ e → P e ⊎ e ≡ u ∨̇ v) ∨-step {u = u} {v} pr pu pv {F} ps a≤ = [ squash-settle (λ a≤u → ≤ʷ-trans a≤u ∨̇-upperˡ) ∘ squash-Any u ps , squash-settle (λ a≤v → ≤ʷ-trans a≤v ∨̇-upperʳ) ∘ squash-Any v ps ]′ (Any.++⁻ (squash u F ps) (pr (All.++⁺ (squash-All u pu ps) (squash-All v pv ps)) (≤⋁-cover a≤ cover))) where both : List (LatTerm X) both = squash u F ps ++ squash v F ps cover : ∀ {f} → f ∈ F → f ≤⋁ both cover f∈ = [ (λ f∈u → ∈→≤⋁ (∈-++⁺ˡ f∈u)) , (λ (f≡ , u∈) → [ (λ f∈v → ∈→≤⋁ (∈-++⁺ʳ (squash u F ps) f∈v)) , (λ (_ , v∈) → subst (_≤⋁ both) (sym f≡) (∨-≤⋁ (∈→≤⋁ (∈-++⁺ˡ u∈)) (∈→≤⋁ (∈-++⁺ʳ (squash u F ps) v∈)))) ]′ (squash-∈ v ps f∈)) ]′ (squash-∈ u ps f∈)
The sublattice generated by a family. Fix a family σ. The elements in play
are the members σ j, together with a finite list L of further elements
(Pool). Adding the image t [ σ ] of a term t over I to the
list preserves primality of a (pool-extend), by induction on t: a
generator's image is a member already, and a meet or join is added by the two
steps above after its two sides have been added. Primality over the members alone
is the hypothesis of the lemma, read through the indices of the members
(pool-base). Together these give Lemma 1.3 in the form the free
generation argument uses (sublattice-join-prime): if a is prime
over the members, then a below the join of two elements of the generated
sublattice lies below one of them.
module _ {I : Type ι} {X : Type χ} (σ : Sub I X) (a : LatTerm X) where Pool : List (LatTerm X) → LatTerm X → Type (ι ⊔ χ) Pool L e = (Σ[ j ∈ I ] e ≡ σ j) ⊎ e ∈ L pool-extend : (t : LatTerm I) {L : List (LatTerm X)} → PrimeOn a (Pool L) → PrimeOn a (Pool (t [ σ ] ∷ L)) pool-extend (ℊ j) {L} pr = PrimeOn-⊆ a member pr where member : ∀ {e} → Pool (σ j ∷ L) e → Pool L e member (inj₁ g) = inj₁ g member (inj₂ (here refl)) = inj₁ (j , refl) member (inj₂ (there e∈)) = inj₂ e∈ pool-extend (u ∧̇ v) {L} pr = PrimeOn-⊆ a split (∧-step a (pool-extend v (pool-extend u pr)) (inj₂ (there (here refl))) (inj₂ (here refl))) where split : ∀ {e} → Pool ((u ∧̇ v) [ σ ] ∷ L) e → Pool (v [ σ ] ∷ u [ σ ] ∷ L) e ⊎ e ≡ u [ σ ] ∧̇ v [ σ ] split (inj₁ g) = inj₁ (inj₁ g) split (inj₂ (here refl)) = inj₂ refl split (inj₂ (there e∈)) = inj₁ (inj₂ (there (there e∈))) pool-extend (u ∨̇ v) {L} pr = PrimeOn-⊆ a split (∨-step a (pool-extend v (pool-extend u pr)) (inj₂ (there (here refl))) (inj₂ (here refl))) where split : ∀ {e} → Pool ((u ∨̇ v) [ σ ] ∷ L) e → Pool (v [ σ ] ∷ u [ σ ] ∷ L) e ⊎ e ≡ u [ σ ] ∨̇ v [ σ ] split (inj₁ g) = inj₁ (inj₁ g) split (inj₂ (here refl)) = inj₂ refl split (inj₂ (there e∈)) = inj₁ (inj₂ (there (there e∈)))
A list of members carries the list of their indices (indices),
whose image under σ is the list itself (indices-map).
indices : (F : List (LatTerm X)) → All (Pool []) F → List I indices [] [] = [] indices (_ ∷ F) (inj₁ (j , _) ∷ ps) = j ∷ indices F ps indices (_ ∷ F) (inj₂ () ∷ ps) indices-map : (F : List (LatTerm X)) (ps : All (Pool []) F) → map σ (indices F ps) ≡ F indices-map [] [] = refl indices-map (_ ∷ F) (inj₁ (j , refl) ∷ ps) = cong (σ j ∷_) (indices-map F ps) indices-map (_ ∷ F) (inj₂ () ∷ ps) pool-base : (∀ {Y : List I} → a ≤⋁ map σ Y → Any (λ j → a ≤ʷ σ j) Y) → PrimeOn a (Pool []) pool-base H {F} ps a≤ = subst (Any (a ≤ʷ_)) (indices-map F ps) (Any.map⁺ (H (subst (a ≤⋁_) (sym (indices-map F ps)) a≤))) sublattice-join-prime : (∀ {Y : List I} → a ≤⋁ map σ Y → Any (λ j → a ≤ʷ σ j) Y) → (u v : LatTerm I) → a ≤ʷ u [ σ ] ∨̇ v [ σ ] → a ≤ʷ u [ σ ] ⊎ a ≤ʷ v [ σ ] sublattice-join-prime H u v p = any-pair (pool-extend v (pool-extend u (pool-base H)) (inj₂ (there (here refl)) ∷ inj₂ (here refl) ∷ []) p) where any-pair : {P : LatTerm X → Type χ} {x y : LatTerm X} → Any P (x ∷ y ∷ []) → P x ⊎ P y any-pair (here q) = inj₁ q any-pair (there (here q)) = inj₂ q
Sufficiency: Corollary 1.12¶
Suppose σ freely generates. Each member σ i is prime over the members
(member-join-prime), since σ i below a join of members indexed
by Y puts i in Y. So by Lemma 1.3 each member is join prime in the
sublattice (join-prime). Meet primality
(meet-prime) is the same fact for the dual family
dual ∘ σ, whose join condition is the meet condition of σ
(MeetCondition→JoinConditionᵈ), read back through
dual-[] and the order reversal of
Lattices.Free.Duality.
module _ {I : Type ι} {X : Type χ} (σ : Sub I X) where MeetCondition→JoinConditionᵈ : MeetCondition σ → JoinCondition (dual ∘ σ) MeetCondition→JoinConditionᵈ mc {i} {[]} () MeetCondition→JoinConditionᵈ mc {i} {j ∷ js} p = mc {i} {j ∷ js} (dual-reflects (subst (dual (σ i) ≤ʷ_) (sym dual-meet) p)) where dual-meet : dual (⋀⁺ (σ j) (map σ js)) ≡ ⋁⁺ (dual (σ j)) (map (dual ∘ σ) js) dual-meet = trans (dual-⋀⁺ (σ j) (map σ js)) (cong (⋁⁺ (dual (σ j))) (sym (map-∘ js))) module Sufficiency (jc : JoinCondition σ) (mc : MeetCondition σ) where member-join-prime : (i : I) {Y : List I} → σ i ≤⋁ map σ Y → Any (λ j → σ i ≤ʷ σ j) Y member-join-prime i p = Any.map (λ { refl → ≤ʷ-refl }) (jc p) join-prime : (i : I) (u v : LatTerm I) → σ i ≤ʷ u [ σ ] ∨̇ v [ σ ] → σ i ≤ʷ u [ σ ] ⊎ σ i ≤ʷ v [ σ ] join-prime i = sublattice-join-prime σ (σ i) (member-join-prime i) meet-prime : (j : I) (u v : LatTerm I) → u [ σ ] ∧̇ v [ σ ] ≤ʷ σ j → u [ σ ] ≤ʷ σ j ⊎ v [ σ ] ≤ʷ σ j meet-prime j u v p = ⊎-map (back u) (back v) (sublattice-join-prime (dual ∘ σ) (dual (σ j)) Hᵈ (dual u) (dual v) pᵈ) where Hᵈ : ∀ {Y : List I} → dual (σ j) ≤⋁ map (dual ∘ σ) Y → Any (λ k → dual (σ j) ≤ʷ dual (σ k)) Y Hᵈ q = Any.map (λ { refl → ≤ʷ-refl }) (MeetCondition→JoinConditionᵈ mc q) pᵈ : dual (σ j) ≤ʷ dual u [ dual ∘ σ ] ∨̇ dual v [ dual ∘ σ ] pᵈ = subst (dual (σ j) ≤ʷ_) (cong₂ _∨̇_ (dual-[] u σ) (dual-[] v σ)) (dual-antitone p) back : (w : LatTerm I) → dual (σ j) ≤ʷ dual w [ dual ∘ σ ] → w [ σ ] ≤ʷ σ j back w q = dual-reflects (subst (dual (σ j) ≤ʷ_) (sym (dual-[] w σ)) q)
With the members prime in the sublattice, the images of the generators obey all
six rules of Whitman's procedure there, and the substitution reflects the order
([]-reflects), by the same recursion as the procedure itself. A
join on the left (rule 2) and a meet on the right (rule 3) split, since
substitution keeps the formal operations; two generators (rule 1) are compared by
the join condition for a single index; a generator below a join (rule 4) and a meet
below a generator (rule 5) are the primality of the members; and a meet below a
join (rule 6) is Whitman's condition in FL(X), the inversion
∧≤∨-inv, which applies because the images are themselves a formal
meet and a formal join.
[]-reflects : (s t : LatTerm I) → s [ σ ] ≤ʷ t [ σ ] → s ≤ʷ t []-reflects (s₁ ∨̇ s₂) t p = ∨≤ ([]-reflects s₁ t (proj₁ (∨≤-inv p))) ([]-reflects s₂ t (proj₂ (∨≤-inv p))) []-reflects (ℊ i) (t₁ ∧̇ t₂) p = ℊ≤∧ ([]-reflects (ℊ i) t₁ (proj₁ (≤∧-inv p))) ([]-reflects (ℊ i) t₂ (proj₂ (≤∧-inv p))) []-reflects (s₁ ∧̇ s₂) (t₁ ∧̇ t₂) p = ∧≤∧ ([]-reflects (s₁ ∧̇ s₂) t₁ (proj₁ (≤∧-inv p))) ([]-reflects (s₁ ∧̇ s₂) t₂ (proj₂ (≤∧-inv p))) []-reflects (ℊ i) (ℊ j) p = ℊ≤ℊ (single (jc {i} {j ∷ []} p)) where single : i ∈ j ∷ [] → i ≡ j single (here e) = e []-reflects (ℊ i) (t₁ ∨̇ t₂) p = [ (λ q → ℊ≤∨ˡ ([]-reflects (ℊ i) t₁ q)) , (λ q → ℊ≤∨ʳ ([]-reflects (ℊ i) t₂ q)) ]′ (join-prime i t₁ t₂ p) []-reflects (s₁ ∧̇ s₂) (ℊ j) p = [ (λ q → ∧ˡ≤ℊ ([]-reflects s₁ (ℊ j) q)) , (λ q → ∧ʳ≤ℊ ([]-reflects s₂ (ℊ j) q)) ]′ (meet-prime j s₁ s₂ p) []-reflects (s₁ ∧̇ s₂) (t₁ ∨̇ t₂) p = [ [ (λ q → ∧ˡ≤∨ ([]-reflects s₁ (t₁ ∨̇ t₂) q)) , (λ q → ∧ʳ≤∨ ([]-reflects s₂ (t₁ ∨̇ t₂) q)) ]′ , [ (λ q → ∧≤∨ˡ ([]-reflects (s₁ ∧̇ s₂) t₁ q)) , (λ q → ∧≤∨ʳ ([]-reflects (s₁ ∧̇ s₂) t₂ q)) ]′ ]′ (∧≤∨-inv p)
So a freely generating family induces an injective homomorphism
(freelyGenerates→injective), and FL(I) is a sublattice of
FL(X) by it (freelyGenerates→≤), in the sense of
Setoid.Subalgebras.Basic: an injective homomorphism, whose image is the
sublattice the family generates.
freelyGenerates→injective : FreelyGenerates σ → IsInjective (proj₁ (subst-hom σ)) freelyGenerates→injective (jc , mc) = reflects→injective σ ([]-reflects _ _) where open Sufficiency jc mc freelyGenerates→≤ : FreelyGenerates σ → proj₁ (FL I) IsSubalgebraOf proj₁ (FL X) freelyGenerates→≤ fg = subst-hom σ , freelyGenerates→injective fg
Necessity¶
Conversely, if the induced homomorphism is injective, σ freely generates
(injective→freelyGenerates). If σ i lies below the join of the
members indexed by j ∷ js, that join is the image of the join of the generators
ℊ j, ℊ k for k in js (⋁⁺-ℊ-[]), so by injectivity ℊ i
lies below the join of those generators in FL(I); a generator is join prime there
(rule 4), and two generators are comparable only when equal (rule 1), so i is in
the list. The meet condition is dual, with rule 5. With sufficiency this is
Corollary 1.13 (freelyGenerates⇔injective).
module _ {I : Type ι} {X : Type χ} (σ : Sub I X) where ⋁⁺-ℊ-[] : (j : I) (js : List I) → ⋁⁺ (ℊ j) (map ℊ js) [ σ ] ≡ ⋁⁺ (σ j) (map σ js) ⋁⁺-ℊ-[] j js = trans (⋁⁺-[] σ (ℊ j) (map ℊ js)) (cong (⋁⁺ (σ j)) (sym (map-∘ js))) ⋀⁺-ℊ-[] : (j : I) (js : List I) → ⋀⁺ (ℊ j) (map ℊ js) [ σ ] ≡ ⋀⁺ (σ j) (map σ js) ⋀⁺-ℊ-[] j js = trans (⋀⁺-[] σ (ℊ j) (map ℊ js)) (cong (⋀⁺ (σ j)) (sym (map-∘ js))) module _ (inj : IsInjective (proj₁ (subst-hom σ))) where injective→JoinCondition : JoinCondition σ injective→JoinCondition {i} {[]} () injective→JoinCondition {i} {j ∷ js} p = Any.map ℊ≤ℊ-inv (Any.map⁻ {f = ℊ} {xs = j ∷ js} (gen-⋁⁺-prime (injective→reflects σ {s = ℊ i} {t = ⋁⁺ (ℊ j) (map ℊ js)} inj (subst (σ i ≤ʷ_) (sym (⋁⁺-ℊ-[] j js)) p)))) injective→MeetCondition : MeetCondition σ injective→MeetCondition {i} {[]} () injective→MeetCondition {i} {j ∷ js} p = Any.map (sym ∘ ℊ≤ℊ-inv) (Any.map⁻ {f = ℊ} {xs = j ∷ js} (⋀⁺-gen-below (injective→reflects σ {s = ⋀⁺ (ℊ j) (map ℊ js)} {t = ℊ i} inj (subst (_≤ʷ σ i) (sym (⋀⁺-ℊ-[] j js)) p)))) injective→freelyGenerates : FreelyGenerates σ injective→freelyGenerates = injective→JoinCondition , injective→MeetCondition freelyGenerates⇔injective : FreelyGenerates σ ⇔ IsInjective (proj₁ (subst-hom σ)) freelyGenerates⇔injective = mk⇔ (freelyGenerates→injective σ) injective→freelyGenerates
Free generation depends only on the elements of the family, not on the terms
that name them: if σ i and τ i are equal in FL(X) for every i, and σ
freely generates, so does τ (freelyGenerates-resp). The
substitutions agree on every term up to equality ([]-congʳ), so
injectivity passes from one to the other. This lets a computation decide free
generation for a family of small terms and conclude it for equal but larger ones.
freelyGenerates-resp : {I : Type ι} {X : Type χ} {σ τ : Sub I X} → (∀ i → σ i ≈ʷ τ i) → FreelyGenerates σ → FreelyGenerates τ freelyGenerates-resp {σ = σ} {τ} e fg = injective→freelyGenerates τ λ {s} {t} p → freelyGenerates→injective σ fg (≈ʷ-trans ([]-congʳ s e) (≈ʷ-trans p (≈ʷ-sym ([]-congʳ t e))))
Restricting the index set¶
A subfamily of a freely generating family freely generates, provided its
index map is injective (freelyGenerates-reindex). The
join and meet conditions apply to the image of the finite index list;
injectivity then recovers membership in the original list. This includes
finite restrictions of a countable family, and inclusions of generators.
-- Free generation restricts along an injective map of indices. freelyGenerates-reindex : {I : Type ι} {J : Type κ} {X : Type χ} (σ : Sub I X) (f : J → I) → (∀ {i j} → f i ≡ f j → i ≡ j) → FreelyGenerates σ → FreelyGenerates (σ ∘ f) freelyGenerates-reindex σ f inj (jc , mc) = join , meet where -- Read the join comparison as one over the image list. join : JoinCondition (σ ∘ f) join {i} {Y} h = Any.map inj (Any.map⁻ {f = f} {xs = Y} (jc (subst (σ (f i) ≤⋁_) (map-∘ Y) h))) -- The same list transport proves the meet condition. meet : MeetCondition (σ ∘ f) meet {i} {Y} h = Any.map inj (Any.map⁻ {f = f} {xs = Y} (mc (subst (_⋀≤ σ (f i)) (map-∘ Y) h))) -- The canonical generators freely generate, by their join and meet primality. generators-free : {X : Type χ} → FreelyGenerates (ℊ {X = X}) generators-free = join , meet where -- A generator below a join of generators equals one of them. join : JoinCondition ℊ join {Y = []} () join {Y = j ∷ js} h = Any.map ℊ≤ℊ-inv (Any.map⁻ {f = ℊ} {xs = j ∷ js} (gen-⋁⁺-prime h)) -- Dually, a generator above a meet equals one of its meetands. meet : MeetCondition ℊ meet {Y = []} () meet {Y = j ∷ js} h = Any.map (sym ∘ ℊ≤ℊ-inv) (Any.map⁻ {f = ℊ} {xs = j ∷ js} (⋀⁺-gen-below h))
Deciding free generation¶
For an index set with decidable equality and a list enum of all its members, the
condition is decided by one decision of Whitman's order for each index and each
of the two halves (the module DecideBy, which takes the decision
procedure for the order as its last parameter). The members indexed by a
list not containing i all occur among the others, the indices different from
i (others), and the join over a sublist lies below the join over
the whole; so the join condition for i holds for every list exactly when σ i
does not lie below the join of the others
(others-join). When I has a single element, the list of others
is empty and the condition holds outright.
module DecideBy {I : Type ι} {X : Type χ} (_≟ᴵ_ : DecidableEquality I) (enum : List I) (complete : ∀ i → i ∈ enum) (_≤?_ : (s t : LatTerm X) → Dec (s ≤ʷ t)) where open DecMembership _≟ᴵ_ using ( _∈?_ ) others : I → List I others i = filter (λ j → ¬? (i ≟ᴵ j)) enum others-∌ : (i : I) → ¬ (i ∈ others i) others-∌ i i∈ = proj₂ (∈-filter⁻ (λ j → ¬? (i ≟ᴵ j)) {xs = enum} i∈) refl others-∋ : {i j : I} → ¬ (i ≡ j) → j ∈ others i others-∋ {i} {j} i≢j = ∈-filter⁺ (λ k → ¬? (i ≟ᴵ k)) (complete j) i≢j _≤⋁?_ : (b : LatTerm X) (G : List (LatTerm X)) → Dec (b ≤⋁ G) b ≤⋁? [] = no λ () b ≤⋁? (g ∷ gs) = b ≤? ⋁⁺ g gs _⋀≤?_ : (G : List (LatTerm X)) (b : LatTerm X) → Dec (G ⋀≤ b) [] ⋀≤? b = no λ () (g ∷ gs) ⋀≤? b = ⋀⁺ g gs ≤? b
If i is not in Y, every member indexed by Y is one of the others
(others-cover), so its join lies below the join of the others
and its meet above their meet.
module _ (σ : Sub I X) where others-cover : {i : I} {Y : List I} → ¬ (i ∈ Y) → ∀ {f} → f ∈ map σ Y → f ∈ map σ (others i) others-cover {i} {Y} i∉ f∈ = let (j , j∈ , f≡) = ∈-map⁻ σ f∈ in subst (_∈ map σ (others i)) (sym f≡) (∈-map⁺ σ (others-∋ (λ i≡j → i∉ (subst (_∈ Y) (sym i≡j) j∈)))) others-join : JoinCondition σ ⇔ All (λ i → ¬ (σ i ≤⋁ map σ (others i))) enum others-join = mk⇔ to from where to : JoinCondition σ → All (λ i → ¬ (σ i ≤⋁ map σ (others i))) enum to jc = tabulate λ {i} _ p → others-∌ i (jc p) from : All (λ i → ¬ (σ i ≤⋁ map σ (others i))) enum → JoinCondition σ from no-join {i} {Y} p = decidable-stable (i ∈? Y) λ i∉ → lookup no-join (complete i) (≤⋁-cover p λ f∈ → ∈→≤⋁ (others-cover i∉ f∈)) others-meet : MeetCondition σ ⇔ All (λ i → ¬ (map σ (others i) ⋀≤ σ i)) enum others-meet = mk⇔ to from where to : MeetCondition σ → All (λ i → ¬ (map σ (others i) ⋀≤ σ i)) enum to mc = tabulate λ {i} _ p → others-∌ i (mc p) from : All (λ i → ¬ (map σ (others i) ⋀≤ σ i)) enum → MeetCondition σ from no-meet {i} {Y} p = decidable-stable (i ∈? Y) λ i∉ → lookup no-meet (complete i) (⋀≤-cover p λ f∈ → ∈→⋀≤ (others-cover i∉ f∈)) joinCondition? : Dec (JoinCondition σ) joinCondition? = map′ (Equivalence.from others-join) (Equivalence.to others-join) (all? (λ i → ¬? (σ i ≤⋁? map σ (others i))) enum) meetCondition? : Dec (MeetCondition σ) meetCondition? = map′ (Equivalence.from others-meet) (Equivalence.to others-meet) (all? (λ i → ¬? (map σ (others i) ⋀≤? σ i)) enum) freelyGenerates? : Dec (FreelyGenerates σ) freelyGenerates? = joinCondition? ×-dec meetCondition?
Decide is the instance at Whitman's recursion
_≤ʷ?_ of Lattices.Free.Whitman, parameterized by the
decidable equality of generators as before, and Decideᵖ the
instance at the table _≤ᵖ?_ of
Lattices.Free.Whitman.Polynomial, for families whose members are large.
module Decide {ι χ : Level} {I : Type ι} {X : Type χ} (_≟ᴵ_ : DecidableEquality I) (enum : List I) (complete : ∀ i → i ∈ enum) (_≟_ : DecidableEquality X) = DecideBy _≟ᴵ_ enum complete (Decision._≤ʷ?_ _≟_) module Decideᵖ {ι χ : Level} {I : Type ι} {X : Type χ} (_≟ᴵ_ : DecidableEquality I) (enum : List I) (complete : ∀ i → i ∈ enum) (_≟_ : DecidableEquality X) = DecideBy _≟ᴵ_ enum complete (Decisionᵖ._≤ᵖ?_ _≟_)
Corollary 1.6: free generators are irreducible¶
A free generator ℊ i of FL(I) lies in the sublattice generated by a family
τ only if it equals a member of the family (generator-in-image):
if ℊ i equals the image t [ τ ] of a term, then by induction on t, a join
u ∨ v puts the generator below u or v (rule 4) and both above it (rule 2), so
it equals the image of u or of v; a meet is dual (rules 3 and 5); and a
generator ℊ j of the term gives the member τ j. This is Freese, Ježek, and
Nation (1995), Corollary 1.6(1), for free lattices: a generating set contains
the free generators.
Through an injective substitution σ the statement moves to the image: the
member σ i lies in the sublattice generated by a family expressed in the members,
ρ ⨟ σ for a family ρ in FL(I), only if ℊ i equals a member of ρ
(free-generator-in-image). So two freely generated sublattices
whose generators are related by ρ are equal only if each ℊ i is a member of
ρ; otherwise the containment is proper.
generator-in-image : {I : Type ι} {J : Type κ} (τ : Sub J I) (t : LatTerm J) {i : I} → ℊ i ≈ʷ t [ τ ] → Σ[ j ∈ J ] ℊ i ≈ʷ τ j generator-in-image τ (ℊ j) e = j , e generator-in-image τ (u ∨̇ v) (p , q) = [ (λ p' → generator-in-image τ u (p' , proj₁ (∨≤-inv q))) , (λ p' → generator-in-image τ v (p' , proj₂ (∨≤-inv q))) ]′ (ℊ≤∨-inv p) generator-in-image τ (u ∧̇ v) (p , q) = [ (λ q' → generator-in-image τ u (proj₁ (≤∧-inv p) , q')) , (λ q' → generator-in-image τ v (proj₂ (≤∧-inv p) , q')) ]′ (∧≤ℊ-inv q) free-generator-in-image : {I : Type ι} {J : Type κ} {X : Type χ} (σ : Sub I X) → IsInjective (proj₁ (subst-hom σ)) → (ρ : Sub J I) (t : LatTerm J) {i : I} → σ i ≈ʷ t [ ρ ⨟ σ ] → Σ[ j ∈ J ] ℊ i ≈ʷ ρ j free-generator-in-image σ inj ρ t {i} e = generator-in-image ρ t (inj {ℊ i} {t [ ρ ]} (subst (σ i ≈ʷ_) ([]-⨟ t ρ σ) e))