Lattices.Free.Prime¶
The generators of a free lattice¶
This is the Lattices.Free.Prime module of the agda-lattices library.
Lattices.Prime proves Lemmas 1.3 and 1.4 and Corollary 1.6 of Freese,
Ježek, and Nation (1995) for any lattice generated by a set satisfying
condition (†). This module reads them in the free lattice FL(X), for any
type X of generators, as follows:
- Lemma 1.2 in
FL(X): the generators satisfy (†) (FL-satisfies†). The book mapsFL(X)onto the two-element lattice, sending one of the two disjoint sets to1, which decides membership in a set of generators; here Whitman's condition along two lists (W-listof Lattices.Free.Canonical.Basic) and the primality of the generators (rules 4 and 5) find the shared generator, with no decision.FL(X)is generated byX(FL-onto). - Corollary 1.5 in
FL(X): the meet of a finite nonempty set of generators is join prime and its join is meet prime (FL-prime-meets-joins). Its other two clauses are in the library already: every generator is join prime and meet prime (FL-gen-primeandFL-gen-primeᵈof Lattices.Bounded.Covers), and two comparable generators are equal (ℊ≤ℊ-invof Lattices.Free.Whitman). - Lemma 1.4 in
FL(X): its join prime elements are the meets of finite nonempty sets of generators, its meet prime elements the joins (FL-joinPrime→meet,FL-meetPrime→join), so its generators are exactly its elements both join prime and meet prime (FL-doublyPrime⇔generator), and a partition of the generators partitionsFL(X)into a filter and an ideal (FL-partition). - Corollary 1.6 in
FL(X): every generating family contains the generators (FL-generators-in-family; the stronger form for any family,generator-in-image, is in Lattices.Free.Generation), and every automorphism is induced by a permutation ofX(FL-automorphism-permutation). Conversely every permutation ofXinduces an automorphism (permutation-automorphism), and the two passages are mutually inverse (permutation-of-automorphism,automorphism-of-permutation) and respect composition (permutation-automorphism-∘): the automorphism group ofFL(X)is the symmetric group onX, the book's last sentence of the corollary.
Lemma 1.2: the generators satisfy (†)¶
The meet and join of FL X are the formal ones by definition, so
the meet and join of a list in FL X are the term-level ones
of Lattices.Free.Canonical.Basic (FL-⋀⁺,
FL-⋁⁺), by induction on the list. If the meet of the
generators in s ∷ ss lies below the join of those in t ∷ ts, Whitman's
condition along the two lists (W-list) puts a meetand ℊ x
below the join, or the meet below a joinand ℊ y; in the first case ℊ x is
below a joinand by rule 4, in the second a meetand is below ℊ y by rule 5,
and two comparable generators are equal by rule 1. So a generator occurs in
both lists (FL-satisfies†), which is Lemma 1.2 for FL(X).
Every element of FL(X) is the value of itself (FL-onto), so
X generates FL(X).
module _ {X : Type χ} where open Setoid 𝔻[ FL X .proj₁ ] using ( reflexive ) -- The meet of a list in FL X is its term-level meet. FL-⋀⁺ : ∀ b bs → ⋀⁺ (FL X) b bs ≡ ⋀̇⁺ b bs FL-⋀⁺ b [] = refl FL-⋀⁺ b (c ∷ cs) = cong (b ∧̇_) (FL-⋀⁺ c cs) -- The join of a list in FL X is its term-level join. FL-⋁⁺ : ∀ b bs → ⋁⁺ (FL X) b bs ≡ ⋁̇⁺ b bs FL-⋁⁺ b [] = refl FL-⋁⁺ b (c ∷ cs) = cong (b ∨̇_) (FL-⋁⁺ c cs) -- Lemma 1.2: in FL(X), a meet of generators lies below a join of generators -- only when they share one. FL-satisfies† : Satisfies† (FL X) ℊ FL-satisfies† s ss t ts p = shared (W-list (map ℊ ss) (map ℊ ts) ( subst₂ _≤ʷ_ (FL-⋀⁺ (ℊ s) (map ℊ ss)) (FL-⋁⁺ (ℊ t) (map ℊ ts)) (≤→≤ʷ p)) ) where -- A meetand below the join, or the meet below a joinand, names a shared generator. shared : Any.Any (_≤ʷ ⋁̇⁺ (ℊ t) (map ℊ ts)) (ℊ s ∷ map ℊ ss) ⊎ Any.Any (⋀̇⁺ (ℊ s) (map ℊ ss) ≤ʷ_) (ℊ t ∷ map ℊ ts) → Σ[ x ∈ X ] (x ∈ s ∷ ss × x ∈ t ∷ ts) shared (inj₁ meetand) = let (x , x∈S , x≤) = find (Any.map⁻ meetand) in x , x∈S , Any.map ℊ≤ℊ-inv (Any.map⁻ (gen-⋁⁺-prime x≤)) shared (inj₂ joinand) = let (y , y∈T , ≤y) = find (Any.map⁻ joinand) in y , Any.map (λ e → sym (ℊ≤ℊ-inv e)) (Any.map⁻ (⋀⁺-gen-below ≤y)) , y∈T -- X generates FL(X): every element is the value of itself. FL-onto : IsSurjective (FL-extend (FL X) ℊ) FL-onto {b} = eq b (reflexive (sym (⟦⟧-ℊ b)))
Corollary 1.5 and Lemma 1.4 in FL(X)¶
The general statements of Lattices.Prime at 𝑳 = FL X and
η = ℊ, with the meets and joins of lists read as terms.
-- Corollary 1.5: in FL(X), meets of generators are join prime and joins of -- generators meet prime. FL-prime-meets-joins : ∀ s ss → IsJoinPrime (FL X) (⋀̇⁺ (ℊ s) (map ℊ ss)) × IsJoinPrime (dualLattice (FL X)) (⋁̇⁺ (ℊ s) (map ℊ ss)) FL-prime-meets-joins s ss = let (jp , mp) = prime-meets-joins (FL X) ℊ FL-onto FL-satisfies† s ss in subst (IsJoinPrime (FL X)) (FL-⋀⁺ (ℊ s) (map ℊ ss)) jp , subst (IsJoinPrime (dualLattice (FL X))) (FL-⋁⁺ (ℊ s) (map ℊ ss)) mp -- Lemma 1.4 (1) in FL(X): a join prime element is a meet of finitely many generators. FL-joinPrime→meet : ∀ {w} → IsJoinPrime (FL X) w → Σ[ s ∈ X ] Σ[ ss ∈ List X ] w ≈ʷ ⋀̇⁺ (ℊ s) (map ℊ ss) FL-joinPrime→meet jp = let (s , ss , e) = joinPrime→meet (FL X) ℊ FL-onto jp in s , ss , subst (_ ≈ʷ_) (FL-⋀⁺ (ℊ s) (map ℊ ss)) e -- Lemma 1.4 (2) in FL(X): a meet prime element is a join of finitely many generators. FL-meetPrime→join : ∀ {w} → IsJoinPrime (dualLattice (FL X)) w → Σ[ s ∈ X ] Σ[ ss ∈ List X ] w ≈ʷ ⋁̇⁺ (ℊ s) (map ℊ ss) FL-meetPrime→join mp = let (s , ss , e) = meetPrime→join (FL X) ℊ FL-onto mp in s , ss , subst (_ ≈ʷ_) (FL-⋁⁺ (ℊ s) (map ℊ ss)) e -- In FL(X), the generators are exactly the elements both join prime and meet prime. FL-doublyPrime⇔generator : ∀ w → (IsJoinPrime (FL X) w × IsJoinPrime (dualLattice (FL X)) w) ⇔ (Σ[ x ∈ X ] w ≈ʷ ℊ x) FL-doublyPrime⇔generator = doublyPrime⇔generator (FL X) ℊ FL-onto FL-satisfies† -- Lemma 1.4 (4) in FL(X): a partition of X partitions FL(X) into a filter and an ideal. FL-partition : (Y : Pred X ℓ₁) (Z : Pred X ℓ₂) → (∀ x → Y x ⊎ Z x) → (∀ {x} → Y x → Z x → ⊥) → ∀ w → (GeneratedFilter (FL X) ℊ Y w ⊎ GeneratedIdeal (FL X) ℊ Z w) × (GeneratedFilter (FL X) ℊ Y w → GeneratedIdeal (FL X) ℊ Z w → ⊥) FL-partition Y Z cover apart = partition (FL X) ℊ Y Z cover FL-onto FL-satisfies† apart
Corollary 1.6 in FL(X)¶
Every family generating FL(X) contains the generators
(FL-generators-in-family), and every automorphism φ of
FL(X) permutes them (FL-automorphism-permutation), with
φ(t) the substitution of the permutation in t
(FL-automorphism-induced): a homomorphism of free lattices is
the substitution of its values at the generators (hom-induced
of Lattices.Free.Substitution). This is automorphism-induced
of Lattices.Prime read in FL(X); deriving it from that statement, through
the evaluation of terms in FL(X), cost 7 s of conversion checking, and this
proof costs nothing measurable.
open Inverse -- Corollary 1.6 (1) in FL(X): every generating family contains the generators. FL-generators-in-family : {J : Type ι} (κ : J → LatTerm X) → IsSurjective (FL-extend (FL X) κ) → ∀ x → Σ[ j ∈ J ] ℊ x ≈ʷ κ j FL-generators-in-family = generators-in-family (FL X) ℊ FL-onto FL-satisfies† -- Corollary 1.6 (2) in FL(X): every automorphism is induced by a permutation of X. FL-automorphism-permutation : (φ : FL X .proj₁ ≅ FL X .proj₁) → Σ[ π ∈ X ↔ X ] (∀ x → _≅_.to φ .proj₁ ⟨$⟩ ℊ x ≈ʷ ℊ (to π x)) FL-automorphism-permutation = automorphism-permutation (FL X) ℊ FL-onto FL-satisfies† -- An automorphism of FL(X) is the substitution of its permutation. FL-automorphism-induced : (φ : FL X .proj₁ ≅ FL X .proj₁) (t : LatTerm X) → _≅_.to φ .proj₁ ⟨$⟩ t ≈ʷ t [ ℊ ∘ to (FL-automorphism-permutation φ .proj₁) ] FL-automorphism-induced φ t = ≈ʷ-trans (hom-induced (_≅_.to φ) t) ([]-congʳ t (FL-automorphism-permutation φ .proj₂)) where π : X ↔ X π = FL-automorphism-permutation φ .proj₁
The automorphism group is the symmetric group¶
A permutation π of X induces the automorphism of FL(X) that substitutes
π for the generators (permutation-automorphism), with the
substitution of π⁻¹ as its inverse: substituting one and then the other is
substituting the composite ([]-⨟), which fixes every
generator. The permutation of this automorphism is π
(permutation-of-automorphism), since the automorphism sends
ℊ x to ℊ (π x) and generators are equal only when their indices are. The
automorphism of the permutation of φ agrees with φ
(automorphism-of-permutation), by
FL-automorphism-induced. And the automorphism of a composite
permutation is the composite of the automorphisms
(permutation-automorphism-∘), by []-⨟. So
φ ↦ π is a bijection of the automorphisms of FL(X), up to the equality of
FL(X), onto the permutations of X, which respects composition.
private -- Substituting two maps of generators that compose to the identity fixes a term. inverse-[] : (f g : X → X) → (∀ x → f (g x) ≡ x) → ∀ t → t [ ℊ ∘ g ] [ ℊ ∘ f ] ≈ʷ t inverse-[] f g fg t = subst (_≈ʷ t) ([]-⨟ t (ℊ ∘ g) (ℊ ∘ f)) (≈ʷ-trans ([]-congʳ t {σ = (ℊ ∘ g) ⨟ (ℊ ∘ f)} {τ = ℊ} (λ x → reflexive (cong ℊ (fg x)))) (reflexive ([]-ℊ t))) -- A permutation of X induces an automorphism of FL(X). permutation-automorphism : X ↔ X → FL X .proj₁ ≅ FL X .proj₁ permutation-automorphism π = mkiso (subst-hom (ℊ ∘ to π)) (subst-hom (ℊ ∘ from π)) (inverse-[] (to π) (from π) (strictlyInverseˡ π)) (inverse-[] (from π) (to π) (strictlyInverseʳ π)) -- The permutation of the automorphism of π is π. permutation-of-automorphism : (π : X ↔ X) (x : X) → to (FL-automorphism-permutation (permutation-automorphism π) .proj₁) x ≡ to π x permutation-of-automorphism π x = sym (ℊ-injective (FL-automorphism-permutation (permutation-automorphism π) .proj₂ x)) -- The automorphism of the permutation of φ agrees with φ. automorphism-of-permutation : (φ : FL X .proj₁ ≅ FL X .proj₁) (t : LatTerm X) → _≅_.to (permutation-automorphism (FL-automorphism-permutation φ .proj₁)) .proj₁ ⟨$⟩ t ≈ʷ _≅_.to φ .proj₁ ⟨$⟩ t automorphism-of-permutation = ≈ʷ-sym ∘₂ FL-automorphism-induced -- The automorphism of a composite permutation is the composite of the automorphisms. permutation-automorphism-∘ : (π σ : X ↔ X) (t : LatTerm X) → _≅_.to (permutation-automorphism (π ↔-∘ σ)) .proj₁ ⟨$⟩ t ≡ _≅_.to (permutation-automorphism π) .proj₁ ⟨$⟩ (_≅_.to (permutation-automorphism σ) .proj₁ ⟨$⟩ t) permutation-automorphism-∘ π σ t = []-⨟ t (ℊ ∘ to σ) (ℊ ∘ to π)
The statements of Lemma 1.2 and Corollaries 1.5 and 1.6¶
Each of the three results 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 generators and the lattices it speaks of, so it is a type in Setω, and a
statement in several parts is a record with one field per part, in the order
the book gives them. The order of FL(X) is _≤ʷ_ and its
equality _≈ʷ_, by Whitman's theorem
(WhitmansTheorem of Lattices.Free.Universal).
FJN-1·2 is Lemma 1.2: the generators of FL(X) satisfy (†),
⋀S ≤ ⋁T implies that S and T share a generator, for finite nonempty
S, T ⊆ X, given as lists. The book states it for the relatively free
lattice of any nontrivial variety; the library has FL(X) alone. The sets
are nonempty because a meet or join of lattice terms is; read with the empty
meet as a top, (†) would fail in FL(X) for finite nonempty X.
FJN-1·5 is Corollary 1.5 in FL(X), again not in every
relatively free lattice: (1) for a finite nonempty S ⊆ X, ⋀S is join prime
and ⋁S is meet prime; (2) every generator is join prime and meet prime; (3)
x ≤ y for generators implies x = y. Meet primality is join primality in
the dual lattice, as in Lattices.Bounded.Covers.
FJN-1·6 is Corollary 1.6. Its parts (1) and (2) are for any
lattice L generated by X (FL-extend onto) with (†): (1)
every generating set of L, given as a family κ, contains X, up to the
equality of L; (2) every automorphism of L is induced by a permutation of
X. Its last sentence, part (3), is stated for FL(X) and not for every
relatively free lattice: the automorphism group of FL(X) is isomorphic to the
symmetric group on X, by the map P that sends a permutation to the
substitution it induces. P π is π on the generators, P sends a composite
to the composite, every automorphism is some P π, and P π and P σ agree
only when π and σ do; equality of automorphisms is agreement at every
element, in the equality of FL(X).
-- FJN Lemma 1.2, in FL(X): the generators satisfy condition (†). FJN-1·2 : Setω FJN-1·2 = ∀ {χ} {X : Type χ} → Satisfies† (FL X) ℊ fjn-1·2 : FJN-1·2 fjn-1·2 = FL-satisfies† -- FJN Corollary 1.5, in FL(X): meets and joins of generators are prime, and -- comparable generators are equal. record FJN-1·5 : Setω where field part-1 : ∀ {χ} {X : Type χ} (s : X) (ss : List X) → IsJoinPrime (FL X) (⋀̇⁺ (ℊ s) (map ℊ ss)) × IsJoinPrime (dualLattice (FL X)) (⋁̇⁺ (ℊ s) (map ℊ ss)) part-2 : ∀ {χ} {X : Type χ} (x : X) → IsJoinPrime (FL X) (ℊ x) × IsJoinPrime (dualLattice (FL X)) (ℊ x) part-3 : ∀ {χ} {X : Type χ} {x y : X} → ℊ x ≤ʷ ℊ y → x ≡ y fjn-1·5 : FJN-1·5 fjn-1·5 = record { part-1 = FL-prime-meets-joins ; part-2 = λ x → FL-prime-meets-joins x [] ; part-3 = ℊ≤ℊ-inv } -- FJN Corollary 1.6: generating sets contain the generators, automorphisms -- permute them, and the automorphism group of FL(X) is the symmetric group. record FJN-1·6 : Setω where field part-1 : ∀ {α ρ χ ι} (𝓛 : Lattice α ρ) {X : Type χ} (η : X → 𝕌[ 𝓛 .proj₁ ]) → IsSurjective (FL-extend 𝓛 η) → Satisfies† 𝓛 η → {J : Type ι} (κ : J → 𝕌[ 𝓛 .proj₁ ]) → IsSurjective (FL-extend 𝓛 κ) → let open Setoid 𝔻[ 𝓛 .proj₁ ] using ( _≈_ ) in ∀ x → Σ[ j ∈ J ] η x ≈ κ j part-2 : ∀ {α ρ χ} (𝓛 : Lattice α ρ) {X : Type χ} (η : X → 𝕌[ 𝓛 .proj₁ ]) → IsSurjective (FL-extend 𝓛 η) → Satisfies† 𝓛 η → let open Setoid 𝔻[ 𝓛 .proj₁ ] using ( _≈_ ) in (φ : 𝓛 .proj₁ ≅ 𝓛 .proj₁) → Σ[ π ∈ X ↔ X ] (∀ x → _≅_.to φ .proj₁ ⟨$⟩ η x ≈ η (Inverse.to π x)) part-3 : ∀ {χ} {X : Type χ} → let ap : FL X .proj₁ ≅ FL X .proj₁ → LatTerm X → LatTerm X ap φ t = _≅_.to φ .proj₁ ⟨$⟩ t in Σ[ P ∈ (X ↔ X → FL X .proj₁ ≅ FL X .proj₁) ] (∀ π x → ap (P π) (ℊ x) ≈ʷ ℊ (Inverse.to π x)) × (∀ π σ t → ap (P (π ↔-∘ σ)) t ≈ʷ ap (P π) (ap (P σ) t)) × (∀ φ → Σ[ π ∈ X ↔ X ] (∀ t → ap (P π) t ≈ʷ ap φ t)) × (∀ π σ → (∀ t → ap (P π) t ≈ʷ ap (P σ) t) → ∀ x → Inverse.to π x ≡ Inverse.to σ x) fjn-1·6 : FJN-1·6 fjn-1·6 = record { part-1 = λ 𝓛 η onto dag κ → generators-in-family 𝓛 η onto dag κ ; part-2 = automorphism-permutation ; part-3 = permutation-automorphism , (λ π x → ≈ʷ-refl) , (λ π σ t → Setoid.reflexive 𝔻[ FL _ .proj₁ ] (permutation-automorphism-∘ π σ t)) , (λ φ → FL-automorphism-permutation φ .proj₁ , automorphism-of-permutation φ) , (λ π σ e x → ℊ-injective (e (ℊ x))) }