Lattices.Free.FJN¶

The results of Freese, Ježek, and Nation, one statement each¶

This is the Lattices.Free.FJN module of the agda-lattices library.

The library proves the results of Freese, Ježek, and Nation (1995) (FJN) under descriptive names, and a theorem is often spread over several of them. This module gathers, for each result of the book's Chapter I that the library proves in full, and for Lemma 9.13, one definition whose type is the statement and one proof of it, and re-exports them in the book's order. The library's results from other chapters (Theorem 5.1 and Corollary 5.2 in Lattices.Projective, say) keep their descriptive names only. It proves nothing itself: each statement and its proof live in the module that proves the result, built from the names there, and the table below names that module.

The conventions are as follows:

Names. A result with a standard name takes it: Theorem 1.11, Whitman's solution of the word problem, is WhitmansTheorem, with its proof whitmans-theorem. Every other result is named by its number in the book: FJN-1·19 is the statement of Theorem 1.19 and fjn-1·19 its proof. The separator is the middle dot ·, since Agda reserves . for qualified names. The book itself calls three results "Whitman's theorem" (1.11, 1.22 and 1.28) and two "Jónsson and Kiefer's" (1.21 and 1.30), so only Theorem 1.11 takes a name.
The form of a statement. A statement quantifies over the levels of the generators and the lattices it speaks of, so it is a type in Setω; one that quantifies over nothing (1.23, 1.28, 1.29) is a type at level zero. A result in several parts is a record with one field per part, part-1, part-2, and so on, in the order the book gives them: for example FJN-1·4.part-3 fjn-1·4 is Lemma 1.4 (3).
The reading. Each statement says what the book says, in the generality of the library: FL(X) for any type X of generators, a lattice generated by X as an assignment X → L whose extension FL(X) → L is onto, or every lattice, each with the setoid equality of agda-algebras. The library's terms are binary where the book's are n-ary, and its (W) is the binary form, equivalent in every lattice. Decidable equality on the generators is assumed only where a computation needs it. Where a statement differs from the book's otherwise, the prose above it in its module says so, and the table says so in short.

FJN	Name	Statement	Module
Lemma 1.2	`FJN-1·2`	the generators of `FL(X)` satisfy (†): `⋀S ≤ ⋁T` implies `S ∩ T ≠ ∅` (in `FL(X)`; the book, in every nontrivial variety)	Lattices.Free.Prime
Lemma 1.3	`FJN-1·3`	in a lattice generated by `X`, an element prime over the finite joins of generators is join prime	Lattices.Prime
Lemma 1.4	`FJN-1·4`	in a lattice generated by `X`: (1) join prime elements are meets, (2) meet prime elements are joins, of finitely many generators; under (†), (3) such meets are join prime and such joins meet prime, (4) a partition of `X` partitions the lattice into a filter and an ideal	Lattices.Prime
Corollary 1.5	`FJN-1·5`	in `FL(X)`: (1) meets of generators are join prime and joins meet prime, (2) every generator is both, (3) comparable generators are equal (the book, in every nontrivial variety)	Lattices.Free.Prime
Corollary 1.6	`FJN-1·6`	for a lattice generated by `X` with (†): (1) every generating set contains `X`, (2) every automorphism is induced by a permutation of `X`; (3) the automorphism group of `FL(X)` is the symmetric group on `X`	Lattices.Free.Prime
Theorem 1.8	`FJN-1·8`	`FL(X)` satisfies (W)	Lattices.Free.Semidistributive
Corollary 1.9	`FJN-1·9`	(1) every sublattice of a free lattice satisfies (W); (2) in a lattice with (W) no element is both a proper join and a proper meet	Lattices.Nation
Theorem 1.11	`WhitmansTheorem`	(1) to (6) Whitman's six rules, as equivalences in `FL(X)`; (7) they decide its order; (8) that order is the order of all lattices	Lattices.Free.Universal
Corollary 1.12	`FJN-1·12`	in a lattice with (W), a family freely generates the sublattice it generates exactly when it satisfies the join and meet conditions	Lattices.Generation
Corollary 1.13	`FJN-1·13`	a family in `FL(X)` freely generates exactly when it satisfies the join and meet conditions	Lattices.Free.Generation
Theorem 1.17	`FJN-1·17`	every element of `FL(X)` has a term of least rank, unique up to commutativity	Lattices.Free.Canonical.LeastRank
Theorem 1.18	`FJN-1·18`	a term has least rank exactly when it satisfies the four conditions	Lattices.Free.Canonical.LeastRank
Theorem 1.19	`FJN-1·19`	(1) the canonical joinands refine every join representation; (2) they are the unique minimal join representation	Lattices.Free.Embedding
Theorem 1.20	`FJN-1·20`	a join irreducible `u` with an element strictly below it is a canonical joinand of `w` exactly when some `a` has `w = u ∨ a` and `v ∨ a < w` for all `v < u` (the book omits the hypothesis, without which the theorem fails at the least element of `FL(X)` for finite `X`)	Lattices.Free.Canonical.JoinIrreducible
Theorem 1.21	`FJN-1·21`	(1) free lattices are semidistributive; (2) (SD∨) is equivalent to its form for finite joins; (3) dually under (SD∧)	Lattices.Free.Semidistributive
Theorem 1.23	`FJN-1·23`	the polynomial `f₁` has no fixed point in `FL(3)`	Lattices.Free.FixedPointFree
Theorem 1.28	`FJN-1·28`	`FL(ω)` is a sublattice of `FL(3)`	Lattices.Free.Countable
Lemma 1.29	`FJN-1·29`	the five non-inequalities between the generators of `FL(3)` and the chains of the proof of Theorem 1.28	Lattices.Free.WhitmanChains
Theorem 1.30	`FJN-1·30`	a lattice with (W) and elements `a₁, a₂, a₃, v` as in (1) to (3) contains `FL(3)`	Lattices.Breadth
Corollary 1.31	`FJN-1·31`	(1) finite lattices with (W) have breadth at most 4; (2) they are 4-distributive and (3) not every lattice is; (4) so are finite sublattices of free lattices	Lattices.Breadth
Lemma 9.13	`FJN-9·13`	an embedding of free lattices sends a canonical joinand that is not a generator to a canonical joinand of the image	Lattices.Free.Embedding

The other results of Chapter I are not stated here, since the library does not prove them in full: Theorem 1.1 (Day's doubling), Corollary 1.7, Theorem 1.10, Corollary 1.14, Lemmas 1.15 and 1.16 (the second is proved for the n-ary terms of the canonical-form modules, not for arbitrary terms), Theorem 1.22, the last claim of Example 1.24 (its chain has no join; the strictness of the chain is ascending-strict), Theorems 1.26 (which the book states without proof) and 1.27, and Corollary 1.32. Nor are the results of Chapter II, which the library proves only in part where it proves them (Theorem 2.6 and Lemma 2.7 for a homomorphism from FL(n) onto a lattice with a decided order in Lattices.Bounded.Preimage, and the clause D(FL(X)) = FL(X) of Corollary 2.11 in Lattices.Bounded.Covers).

The module is not in the barrel Lattices.Free, since it imports Lattices.Prime, Lattices.Nation, Lattices.Generation and Lattices.Breadth, which the barrel does not.

{-# OPTIONS --without-K --exact-split --safe #-}

module Lattices.Free.FJN where

open import Lattices.Free.Prime                 public
  using ( FJN-1·2 ; fjn-1·2 )
open import Lattices.Prime                      public
  using ( FJN-1·3 ; fjn-1·3 ; FJN-1·4 ; module FJN-1·4 ; fjn-1·4 )
open import Lattices.Free.Prime                 public
  using  ( FJN-1·5 ; module FJN-1·5 ; fjn-1·5
         ; FJN-1·6 ; module FJN-1·6 ; fjn-1·6 )
open import Lattices.Free.Semidistributive      public
  using ( FJN-1·8 ; fjn-1·8 )
open import Lattices.Nation                     public
  using ( FJN-1·9 ; module FJN-1·9 ; fjn-1·9 )
open import Lattices.Free.Universal             public
  using ( WhitmansTheorem ; module WhitmansTheorem ; whitmans-theorem )
open import Lattices.Generation                 public
  using ( FJN-1·12 ; fjn-1·12 )
open import Lattices.Free.Generation            public
  using ( FJN-1·13 ; fjn-1·13 )
open import Lattices.Free.Canonical.LeastRank   public
  using ( FJN-1·17 ; fjn-1·17 ; FJN-1·18 ; fjn-1·18 )
open import Lattices.Free.Embedding             public
  using ( FJN-1·19 ; module FJN-1·19 ; fjn-1·19 )
open import Lattices.Free.Canonical.JoinIrreducible public
  using ( FJN-1·20 ; fjn-1·20 )
open import Lattices.Free.Semidistributive      public
  using ( FJN-1·21 ; module FJN-1·21 ; fjn-1·21 )
open import Lattices.Free.FixedPointFree        public
  using ( FJN-1·23 ; fjn-1·23 )
open import Lattices.Free.Countable             public
  using ( FJN-1·28 ; fjn-1·28 )
open import Lattices.Free.WhitmanChains         public
  using ( FJN-1·29 ; module FJN-1·29 ; fjn-1·29 )
open import Lattices.Breadth                    public
  using ( FJN-1·30 ; fjn-1·30 ; FJN-1·31 ; module FJN-1·31 ; fjn-1·31 )
open import Lattices.Free.Embedding             public
  using ( FJN-9·13 ; fjn-9·13 )