Canonical extension provides an algebraic formulation of duality theory and a tool to derive representation theorems. It may be regarded as an algebraic formulation of Stone duality (see Gehrke-Vosmaer, p. 5).
Originally (Jonsson-Tarski) is was formulated for Boolean algebras with operators, but the notion was later generalized to distributive lattices and even to arbitrary posets.
For distributive lattices
Given a distributive lattice , its canonical extension is the downset lattice of the poset of prime filters of , ordered by inclusion.
This construction extends to a functor
from the category of distributive lattices to that of completely distributive algebraic lattices. This is left adjoint to the corresponding forgetful functor, exhibiting completely distributive algebraic lattices as a reflective subcategory of the distributive lattices
For Heyting algebras
The canonical extension of a distributive lattice is a complete and completely distributive lattice.
In particular the canonical extension is a Heyting algebra. If is itself already a Heyting algebra, then preserves the Heyting implication. Also, canonical extension preserves homomorphisms of Heyting algebras. Hence it restricts to a functor
For coherent categories
A distributive lattice is a cogerent (0,1)-category. One may therefore ask if there is a generalization of canonical extension to general coherent categories.
The following is considered in (Coumans).
By the discussion at coherent category and coherent hyperdoctrine, we have a reflective sub-2-category embedding
given by sending a coherent category to its self-indexing .
Since a coherent hyperdoctrine takes values in distributive lattices, we can apply canonical extension of distributive lattices termwise to get a functor
Define then canonical extension of coherent categories to be the 2-functor induced from this under the above reflection:
Under the restriction along the inclusion this reproduces the canonical extension of distributive lattices: for a dsitributive lattice there is an equivalence
(This is (Coumans, prop 12)).
For Heyting categories
There is also a joint generalization of canonical extension for Heyting algebras (here) and for coherent categories (here).
Write for the 2-category of Heyting categories, and for the 2-category of first-order hyperdoctrines (which are, in particular, hyperdoctrines with values in Heyting algebras).
Then the above restricts to a reflective sub-2-category inclusion
This is (Coumans, prop. 19).
And the canonical extension of coherent categories accordingly restricts to a functor on Heyting categories
Such that for a Heyting category, also the unit is a morpjism of Heyting categories.
This is (Coumans, cor. 21).
The study of canonical extensions originates in the articles
- B. Jónsson, Alfred Tarski, Boolean algebras with operators, I, Amer. J. Math. 73 (1951), 891–939.
- Dion Coumans, Generalizing canonical extensions to the categorical setting, pdf, to appear in Annals of Pure and Applied Logic