nLab
canonical extension

Idea

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.

Definition

For distributive lattices

Given a distributive lattice $L$, its canonical extension $L^{\delta }$ is the downset lattice of the poset of prime filters of $L$, ordered by inclusion.

This construction extends to a functor

$$(-{)}^{\delta }:\mathrm{DistLattice}\to {\mathrm{DistLattice}}^{+}$$(-)^\delta : DistLattice \to DistLattice^+

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

$${\mathrm{DistLattice}}^{+}\stackrel{\stackrel{(-{)}^{\delta }}{\leftarrow }}{\hookrightarrow }\mathrm{DistLattice}.$$DistLattice^+ \stackrel{\overset{(-)^\delta}{\leftarrow}}{\hookrightarrow} DistLattice \,.

For Heyting algebras

The canonical extension $L^{\delta }$ of a distributive lattice $L$ is a complete and completely distributive lattice.

In particular the canonical extension is a Heyting algebra. If $L$ is itself already a Heyting algebra, then $e_L:L\to L^{\delta }$ preserves the Heyting implication. Also, canonical extension preserves homomorphisms of Heyting algebras. Hence it restricts to a functor

$$(-{)}^{\delta }:\mathrm{HeytingAlgebra}\to \mathrm{HeytingAlgebra}.$$(-)^\delta : HeytingAlgebra \to HeytingAlgebra \,.

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

$$(𝒜⊣𝒮):\mathrm{CoherentCat}\hookrightarrow \mathrm{CoherentHyperdoctrine}$$(\mathcal{A} \dashv \mathcal{S}) : CoherentCat \hookrightarrow CoherentHyperdoctrine

given by sending a coherent category $C$ to its self-indexing $c\mapsto C_{/c}$.

Since a coherent hyperdoctrine takes values in distributive lattices, we can apply canonical extension of distributive lattices termwise to get a functor

$$(-{)}^{\delta }:\mathrm{CoherentHyperdoctrine}\to \mathrm{CoherentHyperdoctrine}.$$(-)^\delta : CoherentHyperdoctrine \to CoherentHyperdoctrine \,.

Define then canonical extension of coherent categories to be the 2-functor induced from this under the above reflection:

$$(-{)}^{\delta }:\mathrm{CoherentCat}\stackrel{𝒮}{\to }\mathrm{CoherentHyperdoctrine}\stackrel{(-{)}^{\delta }}{\to }\mathrm{CoherentHyperdoctrine}\stackrel{𝒜}{\to }\mathrm{CoherentCat}.$$(-)^\delta : CoherentCat \stackrel{\mathcal{S}}{\to} CoherentHyperdoctrine \stackrel{(-)^\delta}{\to} CoherentHyperdoctrine \stackrel{\mathcal{A}}{\to} CoherentCat \,.

Under the restriction along the inclusion $\mathrm{DistLat}\hookrightarrow \mathrm{CoherentCat}$ this reproduces the canonical extension of distributive lattices: for $L$ a dsitributive lattice there is an equivalence

$$𝒜({𝒮}_L^{\delta })\simeq L^{\delta }.$$\mathcal{A}(\mathcal{S}_L^\delta) \simeq L^\delta \,.

(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 $\mathrm{HeytingCat}$ for the 2-category of Heyting categories, and $\mathrm{FirstOrderHyperdoctrine}$ 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

$$(𝒜⊣𝒮):\mathrm{HeyteingCat}\hookrightarrow \mathrm{FirstOrderHyperdoctrine}$$(\mathcal{A} \dashv \mathcal{S}) : HeyteingCat \hookrightarrow FirstOrderHyperdoctrine

This is (Coumans, prop. 19).

And the canonical extension of coherent categories accordingly restricts to a functor on Heyting categories

$$(-{)}^{\delta }:\mathrm{HeytingCat}\to \mathrm{HeytingCat}.$$(-)^\delta : HeytingCat \to HeytingCat \,.

Such that for $C$ a Heyting category, also the unit $C\to C^{\delta }$ is a morpjism of Heyting categories.

This is (Coumans, cor. 21).

Related concepts

• topos of types

References

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.

Reviews include

• Mai Gehrke, Jacob Vosmaer, A view of canonical extension (arXiv:1009.2803)

• Dion Coumans, Generalizing canonical extensions to the categorical setting, pdf, to appear in Annals of Pure and Applied Logic