Lattices.Generation¶
Free generation in a lattice satisfying Whitman's condition¶
This is the Lattices.Generation module of the agda-lattices library.
Freese, Ježek, and Nation (1995), Corollary 1.12, characterizes the
generating sets of a lattice satisfying (W) that generate it freely: a lattice
L satisfying (W) and generated by X is free on X if and only if, for
x ∈ X and a finite subset Y ⊆ X, x ≤ ⋁Y implies x ∈ Y, and dually
⋀Y ≤ x implies x ∈ Y. Lattices.Free.Generation proves the special
case Corollary 1.13, for families inside a free lattice FL(X), by Whitman's
procedure in FL(X) itself. This module proves the corollary for a family
η : I → L in an arbitrary lattice L satisfying (W), in the form "the
homomorphism FL(I) → L that η induces is injective", whose image is the
sublattice the family generates. Jónsson and Kiefer's theorem
(Lattices.Breadth) applies it to three elements of a lattice with (W).
The module proves the following:
- The join condition and the meet condition for a family of elements of any lattice, stated with joins and meets of finite lists.
- Sufficiency. If
Lsatisfies (W) and the family satisfies both conditions, the induced homomorphism reflects the order (reflects), so it is injective andFL(I)is a sublattice ofLby it. The proof is the book's: the members obey, in the sublattice they generate, the six rules of Whitman's procedure, so an inequality between values of terms is derived by the same rules as the inequality between the terms. Rules 2 and 3 hold in every lattice, rule 6 is (W) inL, rule 1 is the join condition for a single index, and rules 4 and 5, that each member is join prime and meet prime in the generated sublattice, are Freese, Ježek, and Nation (1995), Lemma 2.83 (1). That lemma is proved here by a dichotomy: every element of the sublattice lies above the memberη ior below the join of finitely many members other thanη i. - Necessity. If the induced homomorphism is injective, the family
satisfies both conditions, in any lattice, because the generators of
FL(I)are join prime and meet prime. - The conditions from one bound per index: if for each index
isome elementrlies above every other member and not aboveη i, the join condition holds, and dually. For a finite family this is how the conditions are checked; Jónsson and Kiefer's theorem uses it with three indices.
The case analysis of sufficiency splits on the sums that (W) and the
dichotomy return, and on the decidable equality of the indices; it decides no
inequality of L, which need not be decidable.
Joins and meets of finite lists¶
Fix a lattice 𝑳, with the meet order of
Lattice-Order. A lattice need not have a least element, so the
join of a list is defined for a nonempty list b ∷ bs only
(⋁⁺), nested to the right as the term-level
⋁⁺ of Lattices.Free.Canonical.Basic is; dually
⋀⁺. "a lies below the join of the list G" is a relation
of its own, a ≤⋁ G, false for the empty list, as in
Lattices.Free.Generation, here an inductive family so that the list is
an index Agda can infer; dually G ⋀≤ a. A member of a
list lies below its join (⋁⁺-upper), the join lies below
every upper bound of the members (⋁⁺-least), and dually.
module _ (𝑳 : Lattice α ρ) where open Lattice-Op 𝑳 using ( _∧_ ; _∨_ ) open Lattice-Order 𝑳 using ( _≤_ ; ≤-refl ; ≤-trans ; ∧-greatest ; ∧-lowerˡ ; ∧-lowerʳ ; ∨-least ; ∨-upperˡ ; ∨-upperʳ ) private L : Type α L = 𝕌[ proj₁ 𝑳 ] -- The join and the meet of a nonempty list. ⋁⁺ ⋀⁺ : L → List L → L ⋁⁺ a [] = a ⋁⁺ a (b ∷ bs) = a ∨ ⋁⁺ b bs ⋀⁺ a [] = a ⋀⁺ a (b ∷ bs) = a ∧ ⋀⁺ b bs infix 4 _≤⋁_ _⋀≤_ -- a lies below the join of a list; false for the empty list. data _≤⋁_ (a : L) : List L → Type (α ⊔ ρ) where ≤⋁⁺ : {b : L} {bs : List L} → a ≤ ⋁⁺ b bs → a ≤⋁ (b ∷ bs) -- The meet of a list lies below a; false for the empty list. data _⋀≤_ : List L → L → Type (α ⊔ ρ) where ⋀⁺≤ : {a b : L} {bs : List L} → ⋀⁺ b bs ≤ a → (b ∷ bs) ⋀≤ a -- A member of a list lies below its join. ⋁⁺-upper : {a b : L} {bs : List L} → a ∈ (b ∷ bs) → a ≤ ⋁⁺ b bs ⋁⁺-upper {bs = []} (here refl) = ≤-refl ⋁⁺-upper {bs = _ ∷ _} (here refl) = ∨-upperˡ ⋁⁺-upper {bs = _ ∷ _} (there a∈) = ≤-trans (⋁⁺-upper a∈) ∨-upperʳ -- The join of a list lies below every upper bound of its members. ⋁⁺-least : {b c : L} {bs : List L} → (∀ {a} → a ∈ (b ∷ bs) → a ≤ c) → ⋁⁺ b bs ≤ c ⋁⁺-least {bs = []} f = f (here refl) ⋁⁺-least {bs = _ ∷ _} f = ∨-least (f (here refl)) (⋁⁺-least λ a∈ → f (there a∈)) -- The meet of a list lies below each member. ⋀⁺-lower : {a b : L} {bs : List L} → a ∈ (b ∷ bs) → ⋀⁺ b bs ≤ a ⋀⁺-lower {bs = []} (here refl) = ≤-refl ⋀⁺-lower {bs = _ ∷ _} (here refl) = ∧-lowerˡ ⋀⁺-lower {bs = _ ∷ _} (there a∈) = ≤-trans ∧-lowerʳ (⋀⁺-lower a∈) -- The meet of a list lies above every lower bound of its members. ⋀⁺-greatest : {b c : L} {bs : List L} → (∀ {a} → a ∈ (b ∷ bs) → c ≤ a) → c ≤ ⋀⁺ b bs ⋀⁺-greatest {bs = []} f = f (here refl) ⋀⁺-greatest {bs = _ ∷ _} f = ∧-greatest (f (here refl)) (⋀⁺-greatest λ a∈ → f (there a∈))
The relation _≤⋁_ is closed downward on the left
(≤-≤⋁) and under joins on the left (∨-≤⋁),
and it grows with the list (≤⋁-⊆: if every member of F is
a member of G, a join over F lies below the join over G). An upper bound
of the members of G bounds everything below their join
(≤⋁-elim), and a list with an element below its join is
nonempty (≤⋁-nonempty). A member lies below the join
(∈→≤⋁), and so does the join of a nonempty list of members
(⋁⁺-≤⋁). The dual facts hold for
_⋀≤_.
-- ≤⋁ is closed downward, under joins, and along an inclusion of lists. ≤-≤⋁ : {a c : L} {G : List L} → a ≤ c → c ≤⋁ G → a ≤⋁ G ≤-≤⋁ p (≤⋁⁺ q) = ≤⋁⁺ (≤-trans p q) ∨-≤⋁ : {a c : L} {G : List L} → a ≤⋁ G → c ≤⋁ G → a ∨ c ≤⋁ G ∨-≤⋁ (≤⋁⁺ p) (≤⋁⁺ q) = ≤⋁⁺ (∨-least p q) ≤⋁-⊆ : {a : L} {F G : List L} → a ≤⋁ F → (∀ {f} → f ∈ F → f ∈ G) → a ≤⋁ G ≤⋁-⊆ {G = []} (≤⋁⁺ _) h with h (here refl) ... | () ≤⋁-⊆ {G = _ ∷ _} (≤⋁⁺ p) h = ≤⋁⁺ (≤-trans p (⋁⁺-least λ f∈ → ⋁⁺-upper (h f∈))) -- A member lies below the join, and so does the join of a list of members. ∈→≤⋁ : {a : L} {G : List L} → a ∈ G → a ≤⋁ G ∈→≤⋁ {G = _ ∷ _} a∈ = ≤⋁⁺ (⋁⁺-upper a∈) ⋁⁺-≤⋁ : {b : L} {bs G : List L} → (∀ {f} → f ∈ (b ∷ bs) → f ∈ G) → ⋁⁺ b bs ≤⋁ G ⋁⁺-≤⋁ {G = []} h with h (here refl) ... | () ⋁⁺-≤⋁ {G = _ ∷ _} h = ≤⋁⁺ (⋁⁺-least λ f∈ → ⋁⁺-upper (h f∈)) -- An upper bound of the members bounds what lies below their join. ≤⋁-elim : {a c : L} {G : List L} → a ≤⋁ G → (∀ {f} → f ∈ G → f ≤ c) → a ≤ c ≤⋁-elim (≤⋁⁺ p) h = ≤-trans p (⋁⁺-least h) -- A list with an element below its join has a member. ≤⋁-nonempty : {a : L} {G : List L} → a ≤⋁ G → Σ[ g ∈ L ] g ∈ G ≤⋁-nonempty {G = g ∷ _} (≤⋁⁺ _) = g , here refl -- The dual facts for ⋀≤. ⋀≤-≤ : {a c : L} {G : List L} → G ⋀≤ c → c ≤ a → G ⋀≤ a ⋀≤-≤ (⋀⁺≤ p) q = ⋀⁺≤ (≤-trans p q) ∧-⋀≤ : {a c : L} {G : List L} → G ⋀≤ a → G ⋀≤ c → G ⋀≤ a ∧ c ∧-⋀≤ (⋀⁺≤ p) (⋀⁺≤ q) = ⋀⁺≤ (∧-greatest p q) ⋀≤-⊆ : {a : L} {F G : List L} → F ⋀≤ a → (∀ {f} → f ∈ F → f ∈ G) → G ⋀≤ a ⋀≤-⊆ {G = []} (⋀⁺≤ _) h with h (here refl) ... | () ⋀≤-⊆ {G = _ ∷ _} (⋀⁺≤ p) h = ⋀⁺≤ (≤-trans (⋀⁺-greatest λ f∈ → ⋀⁺-lower (h f∈)) p) ⋀≤-elim : {a c : L} {G : List L} → G ⋀≤ a → (∀ {f} → f ∈ G → c ≤ f) → c ≤ a ⋀≤-elim (⋀⁺≤ p) h = ≤-trans (⋀⁺-greatest h) p
The conditions of Corollary 1.12¶
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. These are the
conditions of Lattices.Free.Generation read in an arbitrary lattice: at
L = FL(X) the meet order is Whitman's order, and the two definitions agree.
module _ {I : Type ι} (η : I → L) where JoinCondition : Type (α ⊔ ρ ⊔ ι) JoinCondition = ∀ {i : I} {Y : List I} → η i ≤⋁ map η Y → i ∈ Y MeetCondition : Type (α ⊔ ρ ⊔ ι) MeetCondition = ∀ {i : I} {Y : List I} → map η Y ⋀≤ η i → i ∈ Y FreelyGenerates : Type (α ⊔ ρ ⊔ ι) FreelyGenerates = JoinCondition × MeetCondition
Two list facts serve the rest of the module: an inclusion of index lists
gives an inclusion of the lists of members (map-⊆), and an
index outside two lists is outside their concatenation
(∉-++).
-- An inclusion of index lists gives an inclusion of member lists. map-⊆ : {J K : List I} → (∀ {j} → j ∈ J → j ∈ K) → ∀ {f} → f ∈ map η J → f ∈ map η K map-⊆ h f∈ = let (j , j∈ , f≡) = ∈-map⁻ η f∈ in subst (_∈ _) (sym f≡) (∈-map⁺ η (h j∈)) -- An index outside two lists is outside their concatenation. ∉-++ : {i : I} {J K : List I} → ¬ (i ∈ J) → ¬ (i ∈ K) → ¬ (i ∈ J ++ K) ∉-++ {J = J} i∉J i∉K i∈ = [ i∉J , i∉K ]′ (∈-++⁻ J i∈)
Lemma 2.83 (1): the members are prime in the generated sublattice¶
Fix an index i. An element a is beneath others of i
(BeneathOthers) if it lies below the join of the members
indexed by some finite list not containing i; dually a is above others
(AboveOthers). Both properties are closed under joins and
meets of two elements that have them (beneath-∨,
above-∧), by concatenating the lists, and under going down
(beneath-≤) or up (above-≤).
-- a lies below a join of members other than η i. BeneathOthers : I → L → Type (α ⊔ ρ ⊔ ι) BeneathOthers i a = Σ[ J ∈ List I ] (¬ (i ∈ J) × a ≤⋁ map η J) -- a lies above a meet of members other than η i. AboveOthers : I → L → Type (α ⊔ ρ ⊔ ι) AboveOthers i a = Σ[ J ∈ List I ] (¬ (i ∈ J) × map η J ⋀≤ a) beneath-≤ : {i : I} {a c : L} → a ≤ c → BeneathOthers i c → BeneathOthers i a beneath-≤ p (J , i∉ , q) = J , i∉ , ≤-≤⋁ p q beneath-∨ : {i : I} {a c : L} → BeneathOthers i a → BeneathOthers i c → BeneathOthers i (a ∨ c) beneath-∨ {i} (J , i∉J , p) (K , i∉K , q) = J ++ K , ∉-++ i∉J i∉K , ∨-≤⋁ (≤⋁-⊆ p (map-⊆ ∈-++⁺ˡ)) (≤⋁-⊆ q (map-⊆ (∈-++⁺ʳ J))) above-≤ : {i : I} {a c : L} → a ≤ c → AboveOthers i a → AboveOthers i c above-≤ p (J , i∉ , q) = J , i∉ , ⋀≤-≤ q p above-∧ : {i : I} {a c : L} → AboveOthers i a → AboveOthers i c → AboveOthers i (a ∧ c) above-∧ {i} (J , i∉J , p) (K , i∉K , q) = J ++ K , ∉-++ i∉J i∉K , ∧-⋀≤ (⋀≤-⊆ p (map-⊆ ∈-++⁺ˡ)) (⋀≤-⊆ q (map-⊆ (∈-++⁺ʳ J)))
The dichotomy (above-or-beneath) says that every element of
the sublattice the family generates lies above η i or is beneath others of
i, by induction on a term naming it. A generator ℊ j is η i itself when
j is i, and otherwise lies below the join of the one-element list [ j ];
a meet lies above η i when both meetands do, and is beneath others as soon as
one meetand is; a join lies above η i as soon as one joinand does, and is
beneath others when both are. The dual (below-or-above) puts
every element below η i or above others. Only the equality of indices is
decided, never an inequality of the lattice.
module _ (_≟_ : DecidableEquality I) where open Evaluation 𝑳 using ( ⟦_⟧ ) -- A one-element list of another index. single-∉ : {i j : I} → ¬ (i ≡ j) → ¬ (i ∈ j ∷ []) single-∉ i≢j (here i≡j) = i≢j i≡j -- Every element of the generated sublattice is above η i or beneath others. above-or-beneath : (i : I) (w : LatTerm I) → η i ≤ ⟦ w ⟧ η ⊎ BeneathOthers i (⟦ w ⟧ η) above-or-beneath i (ℊ j) with i ≟ j ... | yes refl = inj₁ ≤-refl ... | no i≢j = inj₂ (j ∷ [] , single-∉ i≢j , ≤⋁⁺ ≤-refl) above-or-beneath i (u ∧̇ v) with above-or-beneath i u | above-or-beneath i v ... | inj₁ p | inj₁ q = inj₁ (∧-greatest p q) ... | inj₂ p | _ = inj₂ (beneath-≤ ∧-lowerˡ p) ... | inj₁ _ | inj₂ q = inj₂ (beneath-≤ ∧-lowerʳ q) above-or-beneath i (u ∨̇ v) with above-or-beneath i u | above-or-beneath i v ... | inj₁ p | _ = inj₁ (≤-trans p ∨-upperˡ) ... | inj₂ _ | inj₁ q = inj₁ (≤-trans q ∨-upperʳ) ... | inj₂ p | inj₂ q = inj₂ (beneath-∨ p q) -- Dually, every element is below η i or above others. below-or-above : (i : I) (w : LatTerm I) → ⟦ w ⟧ η ≤ η i ⊎ AboveOthers i (⟦ w ⟧ η) below-or-above i (ℊ j) with i ≟ j ... | yes refl = inj₁ ≤-refl ... | no i≢j = inj₂ (j ∷ [] , single-∉ i≢j , ⋀⁺≤ ≤-refl) below-or-above i (u ∧̇ v) with below-or-above i u | below-or-above i v ... | inj₁ p | _ = inj₁ (≤-trans ∧-lowerˡ p) ... | inj₂ _ | inj₁ q = inj₁ (≤-trans ∧-lowerʳ q) ... | inj₂ p | inj₂ q = inj₂ (above-∧ p q) below-or-above i (u ∨̇ v) with below-or-above i u | below-or-above i v ... | inj₁ p | inj₁ q = inj₁ (∨-least p q) ... | inj₂ p | _ = inj₂ (above-≤ ∨-upperˡ p) ... | inj₁ _ | inj₂ q = inj₂ (above-≤ ∨-upperʳ q)
Under the join condition, η i is join prime in the generated sublattice
(join-prime), which is Lemma 2.83 (1). If η i lies below
⟦ u ⟧ ∨ ⟦ v ⟧, split on the two dichotomies: either one of them puts η i
below ⟦ u ⟧ or ⟦ v ⟧, or both joinands are beneath others of i, and then
so is the join, and η i lies below a join of members indexed by a list not
containing i, against the join condition. Meet primality under the meet
condition is the dual (meet-prime).
-- Lemma 2.83 (1): under the join condition, η i is join prime in the sublattice. join-prime : JoinCondition → (i : I) (u v : LatTerm I) → η i ≤ ⟦ u ⟧ η ∨ ⟦ v ⟧ η → η i ≤ ⟦ u ⟧ η ⊎ η i ≤ ⟦ v ⟧ η join-prime jc i u v p with above-or-beneath i u | above-or-beneath i v ... | inj₁ q | _ = inj₁ q ... | inj₂ _ | inj₁ q = inj₂ q ... | inj₂ q | inj₂ r = let (J , i∉ , u∨v≤) = beneath-∨ q r in ⊥-elim (i∉ (jc (≤-≤⋁ p u∨v≤))) -- Dually, under the meet condition, η i is meet prime in the sublattice. meet-prime : MeetCondition → (i : I) (u v : LatTerm I) → ⟦ u ⟧ η ∧ ⟦ v ⟧ η ≤ η i → ⟦ u ⟧ η ≤ η i ⊎ ⟦ v ⟧ η ≤ η i meet-prime mc i u v p with below-or-above i u | below-or-above i v ... | inj₁ q | _ = inj₁ q ... | inj₂ _ | inj₁ q = inj₂ q ... | inj₂ q | inj₂ r = let (J , i∉ , ≤u∧v) = above-∧ q r in ⊥-elim (i∉ (mc (⋀≤-≤ ≤u∧v p)))
Sufficiency¶
With the members prime in the sublattice, the homomorphism the family induces
reflects the order (reflects), by the recursion of Whitman's
procedure, clause for clause as []-reflects of
Lattices.Free.Generation. A join on the left (rule 2) and a meet on the
right (rule 3) split, since evaluation sends the formal operations to those of
𝑳; two generators (rule 1) are compared by the join condition
for the one-element list; 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 (W) in 𝑳, each of whose four alternatives is a
smaller pair.
module _ (W : SatisfiesW 𝑳) (jc : JoinCondition) (mc : MeetCondition) where -- Corollary 1.12, sufficiency: the induced homomorphism reflects the order. reflects : (s t : LatTerm I) → ⟦ s ⟧ η ≤ ⟦ t ⟧ η → s ≤ʷ t reflects (s₁ ∨̇ s₂) t p = ∨≤ (reflects s₁ t (≤-trans ∨-upperˡ p)) (reflects s₂ t (≤-trans ∨-upperʳ p)) reflects (ℊ i) (t₁ ∧̇ t₂) p = ℊ≤∧ (reflects (ℊ i) t₁ (≤-trans p ∧-lowerˡ)) (reflects (ℊ i) t₂ (≤-trans p ∧-lowerʳ)) reflects (s₁ ∧̇ s₂) (t₁ ∧̇ t₂) p = ∧≤∧ (reflects (s₁ ∧̇ s₂) t₁ (≤-trans p ∧-lowerˡ)) (reflects (s₁ ∧̇ s₂) t₂ (≤-trans p ∧-lowerʳ)) 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 jc i t₁ t₂ p) reflects (s₁ ∧̇ s₂) (ℊ j) p = [ (λ q → ∧ˡ≤ℊ (reflects s₁ (ℊ j) q)) , (λ q → ∧ʳ≤ℊ (reflects s₂ (ℊ j) q)) ]′ (meet-prime mc 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)) ]′ ]′ (W (⟦ s₁ ⟧ η) (⟦ s₂ ⟧ η) (⟦ t₁ ⟧ η) (⟦ t₂ ⟧ η) p)
So a freely generating family in a lattice with (W) induces an injective
homomorphism (freelyGenerates→injective), and FL(I) is a
sublattice of 𝑳 by it (freelyGenerates→≤), in
the sense of Setoid.Subalgebras.Basic (the relation
Embeds of Lattices.Nation is the same relation, read on
lattices).
-- Corollary 1.12, sufficiency: the induced homomorphism is injective. freelyGenerates→injective : SatisfiesW 𝑳 → FreelyGenerates → IsInjective (proj₁ (FL-extend-hom 𝑳 η)) freelyGenerates→injective W (jc , mc) {s} {t} e = reflects W jc mc s t (≤-reflexive e) , reflects W jc mc t s (≤-reflexive (sym≈ e)) where open Lattice-Order 𝑳 using ( ≤-reflexive ) open Setoid 𝔻[ proj₁ 𝑳 ] using () renaming ( sym to sym≈ ) -- FL(I) is a sublattice of 𝑳, by the homomorphism the family induces. freelyGenerates→≤ : SatisfiesW 𝑳 → FreelyGenerates → proj₁ (FL I) IsSubalgebraOf proj₁ 𝑳 freelyGenerates→≤ W fg = FL-extend-hom 𝑳 η , freelyGenerates→injective W fg
Necessity¶
Conversely, in any lattice, if the induced homomorphism is injective, the family
freely generates (injective→freelyGenerates). If η i lies
below the join of the members indexed by j ∷ js, that join is the value of
the term-level join of the generators ℊ j, ℊ k for k in js
(⟦⋁̇⁺⟧); so the value of ℊ i ∧̇ (that join) equals the value
of ℊ i, by injectivity the two terms are equal in FL(I), and ℊ i lies
below the join of the generators there. A generator is join prime in FL(I)
(rule 4) and comparable with another generator only when equal (rule 1), so
i is in the list. The meet condition is dual. With sufficiency this is
Corollary 1.12 (freelyGenerates⇔injective).
-- The value of a term-level join (meet) of generators is the join (meet) of members. ⟦⋁̇⁺⟧ : (j : I) (js : List I) → Evaluation.⟦_⟧ 𝑳 (⋁̇⁺ (ℊ j) (map ℊ js)) η ≡ ⋁⁺ (η j) (map η js) ⟦⋁̇⁺⟧ j [] = refl ⟦⋁̇⁺⟧ j (k ∷ ks) = cong (η j ∨_) (⟦⋁̇⁺⟧ k ks) ⟦⋀̇⁺⟧ : (j : I) (js : List I) → Evaluation.⟦_⟧ 𝑳 (⋀̇⁺ (ℊ j) (map ℊ js)) η ≡ ⋀⁺ (η j) (map η js) ⟦⋀̇⁺⟧ j [] = refl ⟦⋀̇⁺⟧ j (k ∷ ks) = cong (η j ∧_) (⟦⋀̇⁺⟧ k ks) module _ (inj : IsInjective (proj₁ (FL-extend-hom 𝑳 η))) where -- Corollary 1.12, necessity: the join condition. injective→JoinCondition : JoinCondition injective→JoinCondition {i} {[]} () injective→JoinCondition {i} {j ∷ js} (≤⋁⁺ p) = Any.map ℊ≤ℊ-inv (Any.map⁻ {f = ℊ} {xs = j ∷ js} (gen-⋁⁺-prime (≤ʷ-trans (proj₂ (inj {ℊ i ∧̇ t} {ℊ i} (subst (λ a → η i ∧ a ≈ η i) (sym (⟦⋁̇⁺⟧ j js)) p))) ∧̇-lowerʳ))) where open Setoid 𝔻[ proj₁ 𝑳 ] using ( _≈_ ) t : LatTerm I t = ⋁̇⁺ (ℊ j) (map ℊ js) -- Corollary 1.12, necessity: the meet condition. injective→MeetCondition : MeetCondition injective→MeetCondition {i} {[]} () injective→MeetCondition {i} {j ∷ js} (⋀⁺≤ p) = Any.map (λ e → sym (ℊ≤ℊ-inv e)) (Any.map⁻ {f = ℊ} {xs = j ∷ js} (⋀⁺-gen-below (≤ʷ-trans (proj₂ (inj {t ∧̇ ℊ i} {t} (subst (λ a → a ∧ η i ≈ a) (sym (⟦⋀̇⁺⟧ j js)) p))) ∧̇-lowerʳ))) where open Setoid 𝔻[ proj₁ 𝑳 ] using ( _≈_ ) t : LatTerm I t = ⋀̇⁺ (ℊ j) (map ℊ js) injective→freelyGenerates : FreelyGenerates injective→freelyGenerates = injective→JoinCondition , injective→MeetCondition -- Corollary 1.12: in a lattice with (W), free generation is injectivity. freelyGenerates⇔injective : DecidableEquality I → SatisfiesW 𝑳 → FreelyGenerates ⇔ IsInjective (proj₁ (FL-extend-hom 𝑳 η)) freelyGenerates⇔injective _≟_ W = mk⇔ (freelyGenerates→injective _≟_ W) injective→freelyGenerates
The conditions from one bound per index¶
To check the join condition it suffices, for each index i, to have an
element r above every other member and not above η i
(bound→JoinCondition): if η i lies below the join of the
members indexed by Y and i is not in Y, every member indexed by Y is
another member, so lies below r, and so does η i. The hypothesis "every
other member lies below r" is stated as follows: for each index j, either
j is i or η j ≤ r. Membership of i in Y is
decided, so a refutation of i ∉ Y gives i ∈ Y. The meet condition is dual
(bound→MeetCondition).
module _ (_≟_ : DecidableEquality I) where open DecMembership _≟_ using ( _∈?_ ) -- The join condition from one upper bound of the others per index. bound→JoinCondition : (∀ i → Σ[ r ∈ L ] ((∀ j → j ≡ i ⊎ η j ≤ r) × ¬ (η i ≤ r))) → JoinCondition bound→JoinCondition bound {i} {Y} p = decidable-stable (i ∈? Y) λ i∉ → let (r , others≤r , ≰r) = bound i in ≰r (≤⋁-elim p λ f∈ → let (j , j∈ , f≡) = ∈-map⁻ η f∈ in subst (_≤ r) (sym f≡) ([ (λ j≡i → ⊥-elim (i∉ (subst (_∈ Y) j≡i j∈))) , (λ q → q) ]′ (others≤r j))) -- The meet condition from one lower bound of the others per index. bound→MeetCondition : (∀ i → Σ[ m ∈ L ] ((∀ j → j ≡ i ⊎ m ≤ η j) × ¬ (m ≤ η i))) → MeetCondition bound→MeetCondition bound {i} {Y} p = decidable-stable (i ∈? Y) λ i∉ → let (m , m≤others , ≰m) = bound i in ≰m (⋀≤-elim p λ f∈ → let (j , j∈ , f≡) = ∈-map⁻ η f∈ in subst (m ≤_) (sym f≡) ([ (λ j≡i → ⊥-elim (i∉ (subst (_∈ Y) j≡i j∈))) , (λ q → q) ]′ (m≤others j)))