nLab
canonical extension

Contents

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 LL, its canonical extension L δL^\delta is the downset lattice of the poset of prime filters of LL, ordered by inclusion.

This construction extends to a functor

() δ:DistLatticeDistLattice + (-)^\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

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

For Heyting algebras

The canonical extension L δL^\delta of a distributive lattice LL is a complete and completely distributive lattice.

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

() δ:HeytingAlgebraHeytingAlgebra. (-)^\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

(𝒜𝒮):CoherentCatCoherentHyperdoctrine (\mathcal{A} \dashv \mathcal{S}) : CoherentCat \hookrightarrow CoherentHyperdoctrine

given by sending a coherent category CC to its self-indexing cC /cc \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

() δ:CoherentHyperdoctrineCoherentHyperdoctrine. (-)^\delta : CoherentHyperdoctrine \to CoherentHyperdoctrine \,.

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

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

Under the restriction along the inclusion DistLatCoherentCatDistLat \hookrightarrow CoherentCat this reproduces the canonical extension of distributive lattices: for LL a dsitributive lattice there is an equivalence

𝒜(𝒮 L δ)L δ. \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 HeytingCatHeytingCat for the 2-category of Heyting categories, and FirstOrderHyperdoctrineFirstOrderHyperdoctrine 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

(𝒜𝒮):HeyteingCatFirstOrderHyperdoctrine (\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

() δ:HeytingCatHeytingCat. (-)^\delta : HeytingCat \to HeytingCat \,.

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

This is (Coumans, cor. 21).

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

Revised on July 24, 2012 04:00:16 by Zoran Škoda (190.26.78.124)