Lattices.Prime¶
Prime generators¶
This is the Lattices.Prime module of the agda-lattices library.
Freese, Ježek, and Nation (1995), Section I.2, proves the basic facts about
the generators of a free lattice in a lattice L generated by a set X, under
one condition on X:
(†)
⋀S ≤ ⋁TimpliesS ∩ T ≠ ∅, for all finite subsetsSandTofX,
which holds in every relatively free lattice of a nontrivial variety (Lemma
1.2); in the trivial variety the relatively free lattice has one element, and
(†) fails for any two disjoint nonempty sets. The sets S and
T are nonempty, as in Lemma 1.4 (3): a lattice need not have an empty meet
or join, and where it has both, as FL(X) has for a finite nonempty X, the
empty meet is the top ⋁X, and (†) fails for S = ∅ and T = X. This
module proves those facts for any lattice of the Setoid tree, generated by an
assignment η : X → L in the sense of Lattices.Kostinsky (the
homomorphism FL(X) → L it induces is onto), as follows:
- Lemma 1.3: if an element
alies below a join of finitely many generators only when it lies below one of them (condition (‡)), thenais join prime. - Lemma 1.4: (1) a join prime element is the meet of a finite nonempty
set of generators, and (2) dually; under (†), (3) the meet of a finite
nonempty set of generators is join prime and its join is meet prime, and
(4) if
Xis the disjoint union ofYandZ, thenLis the disjoint union of the filter generated byYand the ideal generated byZ. - The general clauses of Corollary 1.5: under (†) every generator is join prime and meet prime, and two generators are comparable only when equal; conversely, every element both join prime and meet prime is a generator, by Lemma 1.4 (1) and (2).
- Corollary 1.6: under (†), (1) every generating family of
Lcontains the generators, and (2) every automorphism ofLis induced by a permutation ofX.
Lattices.Free.Prime reads them in FL(X), where Lemma 1.2 supplies (†).
The book's proofs of Lemma 1.4 (1) and (3) split X into the generators
above a and the rest, which a constructive proof cannot do without deciding
the order of L. The proofs here split nothing: (1) is an induction on a term
naming a, and Lemma 1.3, which gives (3), is an induction on a term that
carries, instead of the book's family of finite sets, an element whose joins
with generators are already known to behave. Nothing here assumes decidable
equality of the generators or a decided order.
A meet prime element of L is a join prime element of its dual lattice,
IsJoinPrime (dualLattice 𝑳), as in
Lattices.Bounded.Covers (FL-gen-primeᵈ), and the meet
halves of the results are their join halves read in the dual: the dual is
generated by the same assignment, and (†) is self-dual.
Homomorphisms and terms¶
A homomorphism of lattices commutes with the evaluation of lattice terms
(hom-⟦⟧), by induction on the term, from its compatibility
with the two operations (Lattices.Semidistributive).
module _ (𝓚@(𝑲 , _) : Lattice αᴷ ρᴷ) (𝓜@(𝑴 , _) : Lattice αᴹ ρᴹ) (h : hom 𝑲 𝑴) where open Evaluation 𝓚 using () renaming ( ⟦_⟧ to ⟦_⟧ᴷ ) open Evaluation 𝓜 using ( ⟦_⟧ ) open Lattice-Op 𝓜 using ( ∧-cong ; ∨-cong ) open Setoid 𝔻[ 𝑴 ] using ( _≈_ ) renaming ( refl to ≈refl ; trans to ≈trans ) -- A homomorphism commutes with the evaluation of lattice terms. hom-⟦⟧ : {X : Type χ} (t : LatTerm X) (η : X → 𝕌[ 𝑲 ]) → h .proj₁ ⟨$⟩ ⟦ t ⟧ᴷ η ≈ ⟦ t ⟧ (λ x → h .proj₁ ⟨$⟩ η x) hom-⟦⟧ (ℊ x) η = ≈refl hom-⟦⟧ (s ∧̇ t) η = ≈trans (hom-preserves-∧ 𝓚 𝓜 h (⟦ s ⟧ᴷ η) (⟦ t ⟧ᴷ η)) (∧-cong (hom-⟦⟧ s η) (hom-⟦⟧ t η)) hom-⟦⟧ (s ∨̇ t) η = ≈trans (hom-preserves-∨ 𝓚 𝓜 h (⟦ s ⟧ᴷ η) (⟦ t ⟧ᴷ η)) (∨-cong (hom-⟦⟧ s η) (hom-⟦⟧ t η))
Conditions (†) and (‡)¶
Fix a lattice 𝑳 and an assignment η of its
elements to the generators. A finite nonempty set of generators is a list
s ∷ ss, and its meet and join are those of the nonempty lists of
Lattices.Generation. Condition (†) (Satisfies†) says
that a meet of generators lies below a join of generators only when a generator
occurs in both lists, the intersection being witnessed. Condition (‡) at an
element a (Satisfies‡) says that a lies below a join of
generators only when it lies below one of them.
module _ (𝓛@(𝑳 , _) : Lattice α ρ) {X : Type χ} (η : X → 𝕌[ 𝑳 ]) where open Lattice-Op 𝓛 using ( _∧_ ; _∨_ ; ∨-cong ) open Lattice-Order 𝓛 using ( _≤_ ; ≤-refl ; ≤-trans ; ≤-antisym ; ≤-reflexive ; ≤-respʳ-≈ ; ∧-greatest ; ∧-lowerˡ ; ∧-lowerʳ ; ∨-least ; ∨-upperˡ ; ∨-upperʳ ) open Setoid 𝔻[ 𝑳 ] using ( _≈_ ) renaming ( sym to ≈sym ; trans to ≈trans ) open Evaluation 𝓛 using ( ⟦_⟧ ) private L : Type α L = 𝕌[ 𝑳 ] infix 4 _⋀≤ᴸ_ _≤⋁ᴸ_ _⋀≤ᴸ_ : List L → L → Type (α ⊔ ρ) _⋀≤ᴸ_ = _⋀≤_ 𝓛 _≤⋁ᴸ_ : L → List L → Type (α ⊔ ρ) _≤⋁ᴸ_ = _≤⋁_ 𝓛 -- Condition (†): a meet of generators lies below a join of generators only when they share one. Satisfies† : Type (ρ ⊔ χ) Satisfies† = (s : X) (ss : List X) (t : X) (ts : List X) → ⋀⁺ 𝓛 (η s) (map η ss) ≤ ⋁⁺ 𝓛 (η t) (map η ts) → Σ[ x ∈ X ] (x ∈ s ∷ ss × x ∈ t ∷ ts) -- Condition (‡) at a: a lies below a join of generators only when below one of them. Satisfies‡ : L → Type (ρ ⊔ χ) Satisfies‡ a = (g : X) (gs : List X) → a ≤ ⋁⁺ 𝓛 (η g) (map η gs) → Any (λ x → a ≤ η x) (g ∷ gs)
Four order facts about joins serve the proofs below: a join is monotone in each
argument (∨-monoˡ, ∨-monoʳ), commutative
(∨-swap), and associative (∨-assoc), each as
one inequality. The bounds of the join of a list (upper,
least) and the inclusions of a list of generators in a
concatenation (map-++ˡ, map-++ʳ) restate
lemmas of Lattices.Generation with the lists explicit, since Agda cannot
infer a list from its image under map η.
private -- A join is monotone in its left argument. ∨-monoˡ : ∀ {b b′ c} → b ≤ b′ → b ∨ c ≤ b′ ∨ c ∨-monoˡ p = ∨-least (≤-trans p ∨-upperˡ) ∨-upperʳ -- A join is monotone in its right argument. ∨-monoʳ : ∀ {b c c′} → c ≤ c′ → b ∨ c ≤ b ∨ c′ ∨-monoʳ p = ∨-least ∨-upperˡ (≤-trans p ∨-upperʳ) -- A join is commutative. ∨-swap : ∀ {b c} → b ∨ c ≤ c ∨ b ∨-swap = ∨-least ∨-upperʳ ∨-upperˡ -- A join is associative. ∨-assoc : ∀ {b c d} → (b ∨ c) ∨ d ≤ b ∨ (c ∨ d) ∨-assoc = ∨-least (∨-least ∨-upperˡ (≤-trans ∨-upperˡ ∨-upperʳ)) (≤-trans ∨-upperʳ ∨-upperʳ) -- A member of a nonempty list lies below its join. upper : ∀ b bs {f} → f ∈ b ∷ bs → f ≤ ⋁⁺ 𝓛 b bs upper b bs = ⋁⁺-upper 𝓛 {b = b} {bs = bs} -- The join of a nonempty list lies below every upper bound of its members. least : ∀ b bs {c} → (∀ {f} → f ∈ b ∷ bs → f ≤ c) → ⋁⁺ 𝓛 b bs ≤ c least b bs = ⋁⁺-least 𝓛 {b = b} {bs = bs} -- The generators of the first list are generators of the concatenation. map-++ˡ : ∀ gs hs {f} → f ∈ map η gs → f ∈ map η (gs ++ hs) map-++ˡ gs hs = map-⊆ 𝓛 η {J = gs} {K = gs ++ hs} ∈-++⁺ˡ -- The generators of the second list are generators of the concatenation. map-++ʳ : ∀ gs hs {f} → f ∈ map η hs → f ∈ map η (gs ++ hs) map-++ʳ gs hs = map-⊆ 𝓛 η {J = hs} {K = gs ++ hs} (∈-++⁺ʳ gs)
Lemma 1.3: primality from the generators¶
Assume η generates 𝓛: every element b is the
value of a term term b (term-≈), the
preimage the surjection supplies. Fix an element a satisfying (‡).
An element r is good (Good) if a lies below the join
of r with finitely many generators only when it lies below r or below one of
the generators; (‡) says that the join of a nonempty list of generators is good
for its head (good-ℊ), and a good element stays good when
generators are joined to it (good-⋁), since the two lists of
generators concatenate.
The induction (below-∨) proves, for every term t and good
r, that a ≤ ⟦ t ⟧ ∨ r puts a below ⟦ t ⟧ or below r. A generator is
(‡) applied to r and the one generator. A meet t₁ ∧ t₂ lies below each
meetand, so a lies below r or below both meetands. A join t₁ ∨ t₂ is
the case that needs goodness: t₂ ∨ r is good, by the induction at t₂
against the good element r ∨ ⋁G for each list G of generators, so the
induction at t₁ against t₂ ∨ r puts a below t₁, or below t₂ ∨ r, and
then the induction at t₂ against r finishes. Every call is at a subterm,
so the recursion is structural; it is the book's induction over the family of
sets on which (‡) holds, with the family folded into goodness.
So every value of a term is good (good-term), and a is join
prime (‡→joinPrime), which is Lemma 1.3 for binary joins;
the list form follows by joinPrime-list of
Lattices.Bounded.Covers.
module _ (onto : IsSurjective (FL-extend 𝓛 η)) where -- A term naming each element. term : L → LatTerm X term = SurjInv (FL-extend 𝓛 η) onto -- The term names the element. term-≈ : ∀ b → ⟦ term b ⟧ η ≈ b term-≈ b = SurjInvIsInverseʳ (FL-extend 𝓛 η) onto module _ {a : L} (H : Satisfies‡ a) where -- r is good: a below r joined with generators lies below r or below one of them. Good : L → Type (ρ ⊔ χ) Good r = (gs : List X) → a ≤ ⋁⁺ 𝓛 r (map η gs) → a ≤ r ⊎ Any (λ x → a ≤ η x) gs -- A generator is good, by (‡). good-ℊ : ∀ g → Good (η g) good-ℊ g gs p = Any.toSum (H g gs p) -- A good element stays good when generators are joined to it. good-⋁ : ∀ {r} → Good r → ∀ gs → Good (⋁⁺ 𝓛 r (map η gs)) good-⋁ {r} good gs hs p = [ (λ q → inj₁ (≤-trans q (upper r (map η gs) (here refl)))) , (λ q → [ inj₁ ∘ below-⋁ , inj₂ ]′ (Any.++⁻ gs q)) ]′ (good (gs ++ hs) (≤-trans p regroup)) where regroup : ⋁⁺ 𝓛 (⋁⁺ 𝓛 r (map η gs)) (map η hs) ≤ ⋁⁺ 𝓛 r (map η (gs ++ hs)) regroup = least (⋁⁺ 𝓛 r (map η gs)) (map η hs) λ { (here refl) → least r (map η gs) λ { (here refl) → upper r (map η (gs ++ hs)) (here refl) ; (there f∈) → upper r (map η (gs ++ hs)) (there (map-++ˡ gs hs f∈)) } ; (there f∈) → upper r (map η (gs ++ hs)) (there (map-++ʳ gs hs f∈)) } below-⋁ : Any (λ x → a ≤ η x) gs → a ≤ ⋁⁺ 𝓛 r (map η gs) below-⋁ q = let (x , x∈ , a≤) = find q in ≤-trans a≤ (upper r (map η gs) (there (∈-map⁺ η x∈))) -- The induction of Lemma 1.3: below t ∨ r with r good, a lies below t or below r. below-∨ : (t : LatTerm X) {r : L} → Good r → a ≤ ⟦ t ⟧ η ∨ r → a ≤ ⟦ t ⟧ η ⊎ a ≤ r below-∨ (ℊ x) good p = [ inj₂ , (λ { (here q) → inj₁ q ; (there ()) }) ]′ (good (x ∷ []) (≤-trans p ∨-swap)) below-∨ (t₁ ∧̇ t₂) {r} good p = both (below-∨ t₁ good (≤-trans p (∨-monoˡ ∧-lowerˡ))) (below-∨ t₂ good (≤-trans p (∨-monoˡ ∧-lowerʳ))) where both : a ≤ ⟦ t₁ ⟧ η ⊎ a ≤ r → a ≤ ⟦ t₂ ⟧ η ⊎ a ≤ r → a ≤ ⟦ t₁ ∧̇ t₂ ⟧ η ⊎ a ≤ r both (inj₁ q₁) (inj₁ q₂) = inj₁ (∧-greatest q₁ q₂) both (inj₂ q) _ = inj₂ q both (inj₁ _) (inj₂ q) = inj₂ q below-∨ (t₁ ∨̇ t₂) {r} good p = [ (λ q → inj₁ (≤-trans q ∨-upperˡ)) , (λ q → [ (λ q₂ → inj₁ (≤-trans q₂ ∨-upperʳ)) , inj₂ ]′ (below-∨ t₂ good q)) ]′ (below-∨ t₁ good₂ (≤-trans p ∨-assoc)) where regroup : ∀ gs → ⋁⁺ 𝓛 (⟦ t₂ ⟧ η ∨ r) (map η gs) ≤ ⟦ t₂ ⟧ η ∨ ⋁⁺ 𝓛 r (map η gs) regroup gs = least (⟦ t₂ ⟧ η ∨ r) (map η gs) λ { (here refl) → ∨-monoʳ (upper r (map η gs) (here refl)) ; (there f∈) → ≤-trans (upper r (map η gs) (there f∈)) ∨-upperʳ } -- t₂ ∨ r is good. good₂ : Good (⟦ t₂ ⟧ η ∨ r) good₂ gs q = [ (λ q₂ → inj₁ (≤-trans q₂ ∨-upperˡ)) , (λ q′ → [ (λ q″ → inj₁ (≤-trans q″ ∨-upperʳ)) , inj₂ ]′ (good gs q′)) ]′ (below-∨ t₂ (good-⋁ good gs) (≤-trans q (regroup gs))) -- The value of every term is good. good-term : (u : LatTerm X) → Good (⟦ u ⟧ η) good-term u [] p = inj₁ p good-term u (g ∷ gs) p = [ inj₁ , inj₂ ∘ H g gs ]′ (below-∨ u (good-⋁ (good-ℊ g) gs) p) -- Lemma 1.3: an element satisfying (‡) is join prime. ‡→joinPrime : IsJoinPrime 𝓛 a ‡→joinPrime {b} {c} p = ⊎-map (≤-respʳ-≈ (term-≈ b)) (≤-respʳ-≈ (term-≈ c)) (below-∨ (term b) (good-term (term c)) (≤-respʳ-≈ (∨-cong (≈sym (term-≈ b)) (≈sym (term-≈ c))) p))
Lemma 1.4 (1): join prime elements are meets of generators¶
A join prime element a below the value of a term lies below the meet of a
finite nonempty list of generators each above a, and that meet lies below the
term (meet-of-generators): a generator is its own list; for a
join, primality chooses the joinand above a; for a meet, the two lists
concatenate. At a term naming a this is Lemma 1.4 (1)
(joinPrime→meet): a lies below the meet, which lies below
a. The book splits the generators into those above a and the others; the
induction chooses, through the primality of a, only the generators it meets.
-- Below a term, a join prime element lies below a meet of generators above it. meet-of-generators : ∀ {a} → IsJoinPrime 𝓛 a → (t : LatTerm X) → a ≤ ⟦ t ⟧ η → Σ[ S ∈ List X ] (All (λ x → a ≤ η x) S × map η S ⋀≤ᴸ ⟦ t ⟧ η) meet-of-generators jp (ℊ x) p = x ∷ [] , p ∷ [] , ⋀⁺≤ ≤-refl meet-of-generators jp (t₁ ∨̇ t₂) p = [ (λ q → let (S , A , m) = meet-of-generators jp t₁ q in S , A , ⋀≤-≤ 𝓛 m ∨-upperˡ) , (λ q → let (S , A , m) = meet-of-generators jp t₂ q in S , A , ⋀≤-≤ 𝓛 m ∨-upperʳ) ]′ (jp p) meet-of-generators {a} jp (t₁ ∧̇ t₂) p = let (S₁ , A₁ , m₁) = meet-of-generators jp t₁ (≤-trans p ∧-lowerˡ) (S₂ , A₂ , m₂) = meet-of-generators jp t₂ (≤-trans p ∧-lowerʳ) in S₁ ++ S₂ , All.++⁺ A₁ A₂ , ∧-⋀≤ 𝓛 (⋀≤-⊆ 𝓛 m₁ (map-++ˡ S₁ S₂)) (⋀≤-⊆ 𝓛 m₂ (map-++ʳ S₁ S₂)) -- Lemma 1.4 (1): a join prime element is the meet of a finite nonempty set of generators. joinPrime→meet : ∀ {a} → IsJoinPrime 𝓛 a → Σ[ s ∈ X ] Σ[ ss ∈ List X ] a ≈ ⋀⁺ 𝓛 (η s) (map η ss) joinPrime→meet {a} jp = from (meet-of-generators jp (term a) (≤-reflexive (≈sym (term-≈ a)))) where from : Σ[ S ∈ List X ] (All (λ x → a ≤ η x) S × map η S ⋀≤ᴸ ⟦ term a ⟧ η) → Σ[ s ∈ X ] Σ[ ss ∈ List X ] a ≈ ⋀⁺ 𝓛 (η s) (map η ss) from (s ∷ ss , A , ⋀⁺≤ m) = s , ss , ≤-antisym (⋀⁺-greatest 𝓛 above) (≤-respʳ-≈ (term-≈ a) m) where above : ∀ {f} → f ∈ η s ∷ map η ss → a ≤ f above f∈ = let (x , x∈ , f≡) = ∈-map⁻ η {xs = s ∷ ss} f∈ in subst (a ≤_) (sym f≡) (All.lookup A x∈)
Lemma 1.4 (3): meets of generators are join prime¶
Under (†), the meet of a finite nonempty list of generators satisfies (‡)
(†→‡): if it lies below a join of generators, (†) names a
generator in both lists, and the meet lies below it. So it is join prime, by
Lemma 1.3 (meet-joinPrime), the book's argument. The other
half of (3), that the join is meet prime, is the dual, below.
-- Under (†), the meet of a finite nonempty set of generators satisfies (‡). †→‡ : Satisfies† → ∀ s ss → Satisfies‡ (⋀⁺ 𝓛 (η s) (map η ss)) †→‡ dag s ss g gs p = let (x , x∈S , x∈T) = dag s ss g gs p in Any.map (λ x≡ → subst (λ y → ⋀⁺ 𝓛 (η s) (map η ss) ≤ η y) x≡ (⋀⁺-lower 𝓛 (∈-map⁺ η x∈S))) x∈T -- Lemma 1.4 (3), join half: under (†), the meet of a finite nonempty set of generators is join prime. meet-joinPrime : Satisfies† → ∀ s ss → IsJoinPrime 𝓛 (⋀⁺ 𝓛 (η s) (map η ss)) meet-joinPrime dag s ss = ‡→joinPrime (†→‡ dag s ss)
Lemma 1.4 (4): the filter and the ideal¶
A set of generators is a predicate P on X. The filter generated by P
(GeneratedFilter P) is the set of elements above the meet of
some finite nonempty list of generators satisfying P. Dually, the ideal
generated by P (GeneratedIdeal P) is the set of elements
below the join of some finite nonempty list of generators satisfying P,
which is the book's description of a generated ideal on p. 9. The lists are
nonempty because the list relations _⋀≤_ and
_≤⋁_ of Lattices.Generation are false for the empty
list. The filter is closed upward (filter-≤) and under meets
(filter-∧), by concatenating the lists, and contains the
generators satisfying P (filter-ℊ); the ideal dually.
-- The filter generated by the generators satisfying P. GeneratedFilter : Pred X ℓ₁ → Pred L (α ⊔ ρ ⊔ χ ⊔ ℓ₁) GeneratedFilter P b = Σ[ S ∈ List X ] (All P S × map η S ⋀≤ᴸ b) -- The ideal generated by the generators satisfying P. GeneratedIdeal : Pred X ℓ₁ → Pred L (α ⊔ ρ ⊔ χ ⊔ ℓ₁) GeneratedIdeal P b = Σ[ T ∈ List X ] (All P T × b ≤⋁ᴸ map η T) module _ {P : Pred X ℓ₁} where -- The filter is closed upward. filter-≤ : ∀ {b c} → GeneratedFilter P b → b ≤ c → GeneratedFilter P c filter-≤ (S , A , m) p = S , A , ⋀≤-≤ 𝓛 m p -- The filter is closed under meets. filter-∧ : ∀ {b c} → GeneratedFilter P b → GeneratedFilter P c → GeneratedFilter P (b ∧ c) filter-∧ (S , A , m) (S′ , A′ , m′) = S ++ S′ , All.++⁺ A A′ , ∧-⋀≤ 𝓛 (⋀≤-⊆ 𝓛 m (map-++ˡ S S′)) (⋀≤-⊆ 𝓛 m′ (map-++ʳ S S′)) -- The filter contains the generators satisfying P. filter-ℊ : ∀ {x} → P x → GeneratedFilter P (η x) filter-ℊ {x} px = x ∷ [] , px ∷ [] , ⋀⁺≤ ≤-refl -- The ideal is closed downward. ideal-≤ : ∀ {b c} → b ≤ c → GeneratedIdeal P c → GeneratedIdeal P b ideal-≤ p (T , A , n) = T , A , ≤-≤⋁ 𝓛 p n -- The ideal is closed under joins. ideal-∨ : ∀ {b c} → GeneratedIdeal P b → GeneratedIdeal P c → GeneratedIdeal P (b ∨ c) ideal-∨ (T , A , n) (T′ , A′ , n′) = T ++ T′ , All.++⁺ A A′ , ∨-≤⋁ 𝓛 (≤⋁-⊆ 𝓛 n (map-++ˡ T T′)) (≤⋁-⊆ 𝓛 n′ (map-++ʳ T T′)) -- The ideal contains the generators satisfying P. ideal-ℊ : ∀ {x} → P x → GeneratedIdeal P (η x) ideal-ℊ {x} px = x ∷ [] , px ∷ [] , ≤⋁⁺ ≤-refl
Let X be the disjoint union of Y and Z: every generator satisfies Y or
Z (cover, the case split the induction needs), and none
satisfies both (apart). Every value of a term lies in the
filter generated by Y or in the ideal generated by Z
(filter-or-ideal-term), by the induction of the book's proof:
a join is in the filter as soon as a joinand is, and in the ideal when both
are; a meet dually. If η generates 𝓛, so does
every element (filter-or-ideal). Under (†) no element lies
in both (filter-ideal-disjoint): an element of both lies
above a meet of generators in Y and below a join of generators in Z, and
(†) names a generator in both lists. Together these are Lemma 1.4 (4)
(partition).
module _ (Y : Pred X ℓ₁) (Z : Pred X ℓ₂) (cover : ∀ x → Y x ⊎ Z x) where -- Every value of a term lies in the filter generated by Y or in the ideal generated by Z. filter-or-ideal-term : (t : LatTerm X) → GeneratedFilter Y (⟦ t ⟧ η) ⊎ GeneratedIdeal Z (⟦ t ⟧ η) filter-or-ideal-term (ℊ x) = ⊎-map filter-ℊ ideal-ℊ (cover x) filter-or-ideal-term (t₁ ∨̇ t₂) = join (filter-or-ideal-term t₁) (filter-or-ideal-term t₂) where join : GeneratedFilter Y (⟦ t₁ ⟧ η) ⊎ GeneratedIdeal Z (⟦ t₁ ⟧ η) → GeneratedFilter Y (⟦ t₂ ⟧ η) ⊎ GeneratedIdeal Z (⟦ t₂ ⟧ η) → GeneratedFilter Y (⟦ t₁ ∨̇ t₂ ⟧ η) ⊎ GeneratedIdeal Z (⟦ t₁ ∨̇ t₂ ⟧ η) join (inj₁ f) _ = inj₁ (filter-≤ f ∨-upperˡ) join (inj₂ _) (inj₁ f) = inj₁ (filter-≤ f ∨-upperʳ) join (inj₂ i) (inj₂ i′) = inj₂ (ideal-∨ i i′) filter-or-ideal-term (t₁ ∧̇ t₂) = meet (filter-or-ideal-term t₁) (filter-or-ideal-term t₂) where meet : GeneratedFilter Y (⟦ t₁ ⟧ η) ⊎ GeneratedIdeal Z (⟦ t₁ ⟧ η) → GeneratedFilter Y (⟦ t₂ ⟧ η) ⊎ GeneratedIdeal Z (⟦ t₂ ⟧ η) → GeneratedFilter Y (⟦ t₁ ∧̇ t₂ ⟧ η) ⊎ GeneratedIdeal Z (⟦ t₁ ∧̇ t₂ ⟧ η) meet (inj₂ i) _ = inj₂ (ideal-≤ ∧-lowerˡ i) meet (inj₁ _) (inj₂ i) = inj₂ (ideal-≤ ∧-lowerʳ i) meet (inj₁ f) (inj₁ f′) = inj₁ (filter-∧ f f′) -- Every element lies in the filter generated by Y or in the ideal generated by Z. filter-or-ideal : IsSurjective (FL-extend 𝓛 η) → ∀ b → GeneratedFilter Y b ⊎ GeneratedIdeal Z b filter-or-ideal onto b = ⊎-map (λ f → filter-≤ f (≤-reflexive (term-≈ onto b))) (ideal-≤ (≤-reflexive (≈sym (term-≈ onto b)))) (filter-or-ideal-term (term onto b)) -- Under (†), no element lies in both, when no generator satisfies Y and Z. filter-ideal-disjoint : Satisfies† → (∀ {x} → Y x → Z x → ⊥) → ∀ {b} → GeneratedFilter Y b → GeneratedIdeal Z b → ⊥ filter-ideal-disjoint dag apart (s ∷ ss , AY , ⋀⁺≤ m) (t ∷ ts , AZ , ≤⋁⁺ n) = let (x , x∈S , x∈T) = dag s ss t ts (≤-trans m n) in apart (All.lookup AY x∈S) (All.lookup AZ x∈T) -- Lemma 1.4 (4): L is the disjoint union of the filter generated by Y and the ideal generated by Z. partition : IsSurjective (FL-extend 𝓛 η) → Satisfies† → (∀ {x} → Y x → Z x → ⊥) → ∀ b → (GeneratedFilter Y b ⊎ GeneratedIdeal Z b) × (GeneratedFilter Y b → GeneratedIdeal Z b → ⊥) partition onto dag apart b = filter-or-ideal onto b , filter-ideal-disjoint dag apart
Corollary 1.5 in general: comparable generators are equal¶
Under (†) a generator below another is that generator
(generator-≤→≡): (†) for the two one-element lists names a
generator equal to both. So η is injective up to the equality
of 𝓛 (generator-injective).
-- Under (†), comparable generators are equal. generator-≤→≡ : Satisfies† → ∀ {x y} → η x ≤ η y → x ≡ y generator-≤→≡ dag {x} {y} p with dag x [] y [] p ... | _ , here z≡x , here z≡y = trans (sym z≡x) z≡y -- Under (†), the assignment is injective. generator-injective : Satisfies† → ∀ {x y} → η x ≈ η y → x ≡ y generator-injective dag = (generator-≤→≡ dag) ∘ ≤-reflexive
Duality¶
The dual lattice has the carrier, the equality and the generators of
𝓛, with the two operations exchanged. A term t evaluates in
the dual, at its dual term, to its value in 𝓛
(⟦dual⟧), so η generates the dual if it
generates 𝓛 (onto-dual). The meet of a list in
the dual is its join in 𝓛, and conversely
(⋀⁺ᵈ≡⋁⁺, ⋁⁺ᵈ≡⋀⁺), by induction on the list,
since the operations agree by definition. So (†) holds in the dual if it holds
in 𝓛 (†-dual), with the two lists exchanged.
Meet primality, join primality in the dual, unfolds to b ∧ c ≤ a implying
b ≤ a or c ≤ a (joinPrimeᵈ→meetPrime).
module _ (𝓛@(𝑳 , _) : Lattice α ρ) {X : Type χ} (η : X → 𝕌[ 𝑳 ]) where open Lattice-Op 𝓛 using ( _∧_ ; _∨_ ) open Lattice-Order 𝓛 using ( _≤_ ) open Setoid 𝔻[ 𝑳 ] using ( _≈_ ; reflexive ) renaming ( sym to ≈sym ; trans to ≈trans ) open Evaluation 𝓛 using ( ⟦_⟧ ) open Evaluation (dualLattice 𝓛) using () renaming ( ⟦_⟧ to ⟦_⟧ᵈ ) open LatticeDual 𝓛 using ( ≤ᵈ-flip ; ≤ᵈ-unflip ) private L : Type α L = 𝕌[ 𝑳 ] -- A dual term evaluates in the dual lattice to the value of the term. ⟦dual⟧ : (t : LatTerm X) → ⟦ dual t ⟧ᵈ η ≡ ⟦ t ⟧ η ⟦dual⟧ (ℊ x) = refl ⟦dual⟧ (s ∧̇ t) = cong₂ _∧_ (⟦dual⟧ s) (⟦dual⟧ t) ⟦dual⟧ (s ∨̇ t) = cong₂ _∨_ (⟦dual⟧ s) (⟦dual⟧ t) -- An assignment generating 𝓛 generates its dual. onto-dual : IsSurjective (FL-extend 𝓛 η) → IsSurjective (FL-extend (dualLattice 𝓛) η) onto-dual onto {b} = eq (dual (term 𝓛 η onto b)) (≈sym (≈trans (reflexive (⟦dual⟧ (term 𝓛 η onto b))) (term-≈ 𝓛 η onto b))) -- The meet of a list in the dual is its join in 𝓛. ⋀⁺ᵈ≡⋁⁺ : ∀ b bs → ⋀⁺ (dualLattice 𝓛) b bs ≡ ⋁⁺ 𝓛 b bs ⋀⁺ᵈ≡⋁⁺ b [] = refl ⋀⁺ᵈ≡⋁⁺ b (c ∷ cs) = cong (b ∨_) (⋀⁺ᵈ≡⋁⁺ c cs) -- The join of a list in the dual is its meet in 𝓛. ⋁⁺ᵈ≡⋀⁺ : ∀ b bs → ⋁⁺ (dualLattice 𝓛) b bs ≡ ⋀⁺ 𝓛 b bs ⋁⁺ᵈ≡⋀⁺ b [] = refl ⋁⁺ᵈ≡⋀⁺ b (c ∷ cs) = cong (b ∧_) (⋁⁺ᵈ≡⋀⁺ c cs) -- (†) holds in the dual if it holds in 𝓛. †-dual : Satisfies† 𝓛 η → Satisfies† (dualLattice 𝓛) η †-dual dag s ss t ts p = x , x∈S , x∈T where open Relation.Binary.PropositionalEquality using ( subst₂ ) ξ : Σ[ x ∈ X ] (x ∈ t ∷ ts × x ∈ s ∷ ss) ξ = dag t ts s ss ( subst₂ _≤_ (⋁⁺ᵈ≡⋀⁺ (η t) (map η ts)) (⋀⁺ᵈ≡⋁⁺ (η s) (map η ss)) (≤ᵈ-flip p) ) x : X x = ξ .proj₁ x∈T : x ∈ t ∷ ts x∈T = ξ .proj₂ .proj₁ x∈S : x ∈ s ∷ ss x∈S = ξ .proj₂ .proj₂ -- Meet primality, read in the order of 𝓛. joinPrimeᵈ→meetPrime : ∀ {a} → IsJoinPrime (dualLattice 𝓛) a → ∀ {b c} → b ∧ c ≤ a → b ≤ a ⊎ c ≤ a joinPrimeᵈ→meetPrime mp p = ⊎-map ≤ᵈ-flip ≤ᵈ-flip (mp (≤ᵈ-unflip p))
Lemma 1.4 (2) and (3), the dual halves¶
Lemma 1.4 (2) is (1) in the dual (meetPrime→join): a meet
prime element is the join of a finite nonempty set of generators. The second
half of (3) is the first half in the dual (join-meetPrime):
under (†) the join of a finite nonempty set of generators is meet prime.
prime-meets-joins states (3) whole. At one generator, (3) says
that every generator is join prime and meet prime
(generator-joinPrime, generator-meetPrime),
which with generator-≤→≡ is Corollary 1.5 read in
𝓛.
module _ (onto : IsSurjective (FL-extend 𝓛 η)) where -- Lemma 1.4 (2): a meet prime element is the join of a finite nonempty set of -- generators. meetPrime→join : ∀ {a} → IsJoinPrime (dualLattice 𝓛) a → Σ[ s ∈ X ] Σ[ ss ∈ List X ] a ≈ ⋁⁺ 𝓛 (η s) (map η ss) meetPrime→join {a} mp = s , ss , subst (_ ≈_) (⋀⁺ᵈ≡⋁⁺ (η s) (map η ss)) e where ξ : Σ[ s ∈ X ] Σ[ ss ∈ List X ] a ≈ ⋀⁺ (dualLattice 𝓛) (η s) (map η ss) ξ = joinPrime→meet (dualLattice 𝓛) η (onto-dual onto) mp s : X s = ξ .proj₁ ss : List X ss = ξ .proj₂ .proj₁ e : a ≈ ⋀⁺ (dualLattice 𝓛) (η s) (map η ss) e = ξ .proj₂ .proj₂ -- Lemma 1.4 (3), meet half: under (†), the join of a finite nonempty set of -- generators is meet prime. join-meetPrime : Satisfies† 𝓛 η → ∀ s ss → IsJoinPrime (dualLattice 𝓛) (⋁⁺ 𝓛 (η s) (map η ss)) join-meetPrime dag s ss = subst (IsJoinPrime (dualLattice 𝓛)) (⋀⁺ᵈ≡⋁⁺ (η s) (map η ss)) (meet-joinPrime (dualLattice 𝓛) η (onto-dual onto) (†-dual dag) s ss) -- Lemma 1.4 (3): under (†), meets of generators are join prime and joins of -- generators meet prime. prime-meets-joins : Satisfies† 𝓛 η → ∀ s ss → IsJoinPrime 𝓛 (⋀⁺ 𝓛 (η s) (map η ss)) × IsJoinPrime (dualLattice 𝓛) (⋁⁺ 𝓛 (η s) (map η ss)) prime-meets-joins dag s ss = meet-joinPrime 𝓛 η onto dag s ss , join-meetPrime dag s ss -- Under (†), every generator is join prime. generator-joinPrime : Satisfies† 𝓛 η → ∀ x → IsJoinPrime 𝓛 (η x) generator-joinPrime dag x = meet-joinPrime 𝓛 η onto dag x [] -- Under (†), every generator is meet prime. generator-meetPrime : Satisfies† 𝓛 η → ∀ x → IsJoinPrime (dualLattice 𝓛) (η x) generator-meetPrime dag x = join-meetPrime dag x []
The generators are the doubly prime elements¶
Under (†) the converse holds too: an element both join prime and meet prime
is a generator (doublyPrime→generator). By Lemma 1.4 (1) and
(2) it is a meet ⋀S and a join ⋁T of generators, so ⋀S ≤ ⋁T, (†) names
a generator x in both, and ⋀S ≤ x ≤ ⋁T, which pins the element to x.
So the generators are exactly the elements that are join prime and meet prime
(doublyPrime⇔generator), up to the equality of
𝓛; primality respects that equality (D-resp
of Lattices.Bounded.Covers at rank 0).
open Lattice-Order 𝓛 using ( ≤-trans ; ≤-antisym ; ≤-reflexive ) -- Under (†), an element both join prime and meet prime is a generator. doublyPrime→generator : Satisfies† 𝓛 η → ∀ {a} → IsJoinPrime 𝓛 a → IsJoinPrime (dualLattice 𝓛) a → Σ[ x ∈ X ] a ≈ η x doublyPrime→generator dag {a} jp mp = let (s , ss , a≈⋀) = joinPrime→meet 𝓛 η onto jp (t , ts , a≈⋁) = meetPrime→join mp (x , x∈S , x∈T) = dag s ss t ts (≤-trans (≤-reflexive (≈sym a≈⋀)) (≤-reflexive a≈⋁)) in x , ≤-antisym (≤-trans (≤-reflexive a≈⋀) (⋀⁺-lower 𝓛 (∈-map⁺ η x∈S))) (≤-trans (⋁⁺-upper 𝓛 (∈-map⁺ η x∈T)) (≤-reflexive (≈sym a≈⋁))) -- Under (†), the generators are exactly the elements both join prime and meet prime. doublyPrime⇔generator : Satisfies† 𝓛 η → ∀ a → (IsJoinPrime 𝓛 a × IsJoinPrime (dualLattice 𝓛) a) ⇔ (Σ[ x ∈ X ] a ≈ η x) doublyPrime⇔generator dag a = mk⇔ (λ (jp , mp) → doublyPrime→generator dag jp mp) from where from : Σ[ x ∈ X ] a ≈ η x → IsJoinPrime 𝓛 a × IsJoinPrime (dualLattice 𝓛) a from (x , e) = D-resp 𝓛 zero (≈sym e) (generator-joinPrime dag x) , D-resp (dualLattice 𝓛) zero (≈sym e) (generator-meetPrime dag x)
Corollary 1.6 (1): generating sets contain the generators¶
An element that is join prime and meet prime, and lies in the sublattice
generated by a family κ, equals a member of the family
(prime-in-sublattice), by induction on a term naming it: if it
equals a join, it lies below a joinand by primality and above it, so it equals
the joinand; a meet is dual. This is the book's proof: a generator is join
irreducible and meet irreducible. So, under (†), every family generating
𝓛 contains the generators (generators-in-family),
Corollary 1.6 (1), with a set Y given as a family.
module _ {J : Type ι} (κ : J → L) where open Lattice-Order 𝓛 using ( ≤-trans ; ≤-antisym ; ≤-reflexive ; ∨-upperˡ ; ∨-upperʳ ; ∧-lowerˡ ; ∧-lowerʳ ) -- A doubly prime element of the sublattice generated by κ is a member of κ. prime-in-sublattice : ∀ {a} → IsJoinPrime 𝓛 a → IsJoinPrime (dualLattice 𝓛) a → (u : LatTerm J) → a ≈ ⟦ u ⟧ κ → Σ[ j ∈ J ] a ≈ κ j prime-in-sublattice jp mp (ℊ j) e = j , e prime-in-sublattice jp mp (u₁ ∨̇ u₂) e = [ (λ q → prime-in-sublattice jp mp u₁ (≤-antisym q (≤-trans ∨-upperˡ (≤-reflexive (≈sym e))))) , (λ q → prime-in-sublattice jp mp u₂ (≤-antisym q (≤-trans ∨-upperʳ (≤-reflexive (≈sym e))))) ]′ (jp (≤-reflexive e)) prime-in-sublattice jp mp (u₁ ∧̇ u₂) e = [ (λ q → prime-in-sublattice jp mp u₁ (≤-antisym (≤-trans (≤-reflexive e) ∧-lowerˡ) q)) , (λ q → prime-in-sublattice jp mp u₂ (≤-antisym (≤-trans (≤-reflexive e) ∧-lowerʳ) q)) ]′ (joinPrimeᵈ→meetPrime mp (≤-reflexive (≈sym e))) module _ (onto : IsSurjective (FL-extend 𝓛 η)) (dag : Satisfies† 𝓛 η) where -- Corollary 1.6 (1): under (†), every family generating 𝓛 contains the -- generators. generators-in-family : {J : Type ι} (κ : J → L) → IsSurjective (FL-extend 𝓛 κ) → ∀ x → Σ[ j ∈ J ] η x ≈ κ j generators-in-family κ onto-κ x = prime-in-sublattice κ (generator-joinPrime onto dag x) (generator-meetPrime onto dag x) (term 𝓛 κ onto-κ (η x)) (≈sym (term-≈ 𝓛 κ onto-κ (η x)))
Corollary 1.6 (2): automorphisms are permutations of the generators¶
An automorphism of 𝓛 is an isomorphism φ of 𝓛
with itself (Setoid.Homomorphisms.Isomorphisms). It carries the
generators to a generating family (automorphism-generates):
an element b is φ of φ⁻¹ b, and φ⁻¹ b is the value of a term, so b
is the value of the same term at the images of the generators. By Corollary
1.6 (1) every generator is the image under φ of a generator
(preimage), and every image of a generator is a generator, by
the same applied to φ⁻¹. These two maps X → X are mutually inverse, by
the injectivity of η under (†) and of φ, so φ permutes the
generators (automorphism-permutation), Corollary 1.6 (2).
φ is then induced by the permutation: its value at the value of a term is
the value of the term at the permuted generators
(automorphism-induced).
private -- The map of an automorphism. ap : 𝑳 ≅ 𝑳 → L → L ap φ b = _≅_.to φ .proj₁ ⟨$⟩ b -- An automorphism carries the generators to a generating family. automorphism-generates : (φ : 𝑳 ≅ 𝑳) → IsSurjective (FL-extend 𝓛 (ap φ ∘ η)) automorphism-generates φ {b} = eq t (≈trans (≈sym (_≅_.to∼from φ b)) (≈trans (Func.cong (_≅_.to φ .proj₁) (≈sym (term-≈ 𝓛 η onto b′))) (hom-⟦⟧ 𝓛 𝓛 (_≅_.to φ) t η))) where b′ : L b′ = ap (≅-sym φ) b t : LatTerm X t = term 𝓛 η onto b′ -- Every generator is the image of a generator under an automorphism. preimage : (φ : 𝑳 ≅ 𝑳) → ∀ x → Σ[ y ∈ X ] η x ≈ ap φ (η y) preimage φ = generators-in-family (ap φ ∘ η) (automorphism-generates φ) -- Corollary 1.6 (2): under (†), every automorphism of 𝓛 is induced by a -- permutation of X. automorphism-permutation : (φ : 𝑳 ≅ 𝑳) → Σ[ π ∈ X ↔ X ] (∀ x → ap φ (η x) ≈ η (Inverse.to π x)) automorphism-permutation φ = mk↔ₛ′ π π⁻¹ π-π⁻¹ π⁻¹-π , φ-π where π π⁻¹ : X → X π x = preimage (≅-sym φ) x .proj₁ π⁻¹ x = preimage φ x .proj₁ -- φ sends each generator to its image under π. φ-π : ∀ x → ap φ (η x) ≈ η (π x) φ-π x = ≈trans (Func.cong (_≅_.to φ .proj₁) (preimage (≅-sym φ) x .proj₂)) (_≅_.to∼from φ (η (π x))) π-π⁻¹ : ∀ y → π (π⁻¹ y) ≡ y π-π⁻¹ y = generator-injective 𝓛 η dag (≈trans (≈sym (φ-π (π⁻¹ y))) (≈sym (preimage φ y .proj₂))) π⁻¹-π : ∀ x → π⁻¹ (π x) ≡ x π⁻¹-π x = generator-injective 𝓛 η dag (≅toInjective φ (≈trans (≈sym (preimage φ (π x) .proj₂)) (≈sym (φ-π x)))) -- An automorphism sends the value of a term to its value at the permuted generators. automorphism-induced : (φ : 𝑳 ≅ 𝑳) (t : LatTerm X) → ap φ (⟦ t ⟧ η) ≈ ⟦ t ⟧ (η ∘ (automorphism-permutation φ .proj₁ .Inverse.to)) automorphism-induced φ t = ≈trans (hom-⟦⟧ 𝓛 𝓛 (_≅_.to φ) t η) (⟦⟧-cong t (automorphism-permutation φ .proj₂)) where open Evaluation 𝓛 using ( ⟦⟧-cong )
The statements of Lemmas 1.3 and 1.4¶
Each of the two lemmas is one definition whose type is the statement, with its
proof beside it, built from the names above; Lattices.Free.FJN lists them
with the rest of Chapter I. A statement quantifies over the levels of the
lattice and of the generators, so it is a type in Setω, and a statement in
several parts is a record with one field per part, in the book's order. "L
is generated by X" is read as in the rest of the module: an assignment
η : X → L whose extension FL(X) → L is onto. The finite sets of the book
are lists, and a finite set that a meet or join is taken of is nonempty, as
the book's Lemma 1.4 (3) says and as a lattice without bounds requires.
FJN-1·3 is Lemma 1.3: if a ≤ ⋁S implies a ≤ s for some
s ∈ S, for every finite nonempty S ⊆ X (condition (‡) at a), then the
same holds for every finite nonempty S ⊆ L, that is, a is join prime;
join primality for two joinands gives it for every finite nonempty set.
FJN-1·4 is Lemma 1.4: (1) a join prime element is ⋀S and
(2) a meet prime element is ⋁S, for some finite nonempty S ⊆ X; and if X
satisfies (†), then (3) for every finite nonempty S ⊆ X, ⋀S is join prime
and ⋁S is meet prime, and (4) if X is the disjoint union of Y and Z,
then every element lies in the filter generated by Y or in the ideal
generated by Z, and in not both. A subset of X is a predicate, and "the
disjoint union" is the two hypotheses that every generator satisfies Y or
Z and none satisfies both. Meet primality is join primality in the dual
lattice.
-- FJN Lemma 1.3: an element prime over the generators is join prime. FJN-1·3 : Setω FJN-1·3 = ∀ {α ρ χ} (𝓛 : Lattice α ρ) {X : Type χ} (η : X → 𝕌[ 𝓛 .proj₁ ]) → IsSurjective (FL-extend 𝓛 η) → ∀ {a} → Satisfies‡ 𝓛 η a → IsJoinPrime 𝓛 a fjn-1·3 : FJN-1·3 fjn-1·3 𝓛 η onto H = ‡→joinPrime 𝓛 η onto H -- FJN Lemma 1.4: the prime elements of a generated lattice, and under (†) -- the primality of meets and joins of generators and the partition. record FJN-1·4 : Setω where field part-1 : ∀ {α ρ χ} (𝓛 : Lattice α ρ) {X : Type χ} (η : X → 𝕌[ 𝓛 .proj₁ ]) → IsSurjective (FL-extend 𝓛 η) → let open Setoid 𝔻[ 𝓛 .proj₁ ] using ( _≈_ ) in ∀ {a} → IsJoinPrime 𝓛 a → Σ[ s ∈ X ] Σ[ ss ∈ List X ] a ≈ ⋀⁺ 𝓛 (η s) (map η ss) part-2 : ∀ {α ρ χ} (𝓛 : Lattice α ρ) {X : Type χ} (η : X → 𝕌[ 𝓛 .proj₁ ]) → IsSurjective (FL-extend 𝓛 η) → let open Setoid 𝔻[ 𝓛 .proj₁ ] using ( _≈_ ) in ∀ {a} → IsJoinPrime (dualLattice 𝓛) a → Σ[ s ∈ X ] Σ[ ss ∈ List X ] a ≈ ⋁⁺ 𝓛 (η s) (map η ss) part-3 : ∀ {α ρ χ} (𝓛 : Lattice α ρ) {X : Type χ} (η : X → 𝕌[ 𝓛 .proj₁ ]) → IsSurjective (FL-extend 𝓛 η) → Satisfies† 𝓛 η → ∀ s ss → IsJoinPrime 𝓛 (⋀⁺ 𝓛 (η s) (map η ss)) × IsJoinPrime (dualLattice 𝓛) (⋁⁺ 𝓛 (η s) (map η ss)) part-4 : ∀ {α ρ χ ℓ₁ ℓ₂} (𝓛 : Lattice α ρ) {X : Type χ} (η : X → 𝕌[ 𝓛 .proj₁ ]) → IsSurjective (FL-extend 𝓛 η) → Satisfies† 𝓛 η → (Y : Pred X ℓ₁) (Z : Pred X ℓ₂) → (∀ x → Y x ⊎ Z x) → (∀ {x} → Y x → Z x → ⊥) → ∀ b → (GeneratedFilter 𝓛 η Y b ⊎ GeneratedIdeal 𝓛 η Z b) × (GeneratedFilter 𝓛 η Y b → GeneratedIdeal 𝓛 η Z b → ⊥) fjn-1·4 : FJN-1·4 fjn-1·4 = record { part-1 = λ 𝓛 η onto → joinPrime→meet 𝓛 η onto ; part-2 = λ 𝓛 η onto → meetPrime→join 𝓛 η onto ; part-3 = λ 𝓛 η onto dag → prime-meets-joins 𝓛 η onto dag ; part-4 = λ 𝓛 η onto dag Y Z cover apart → partition 𝓛 η Y Z cover onto dag apart }