Constructively completely distributive lattices in presheaf categories
F. Marmolejo · 2007
An ordered set L is a sup lattice if and only if the down-segment embedding of L into its complete lattice of down-sets, ↓ :L → DL, has a left adjoint ∨ :DL → L. Since [3] a complete lattice has been said to be constructively completely distributive (CCD) if ∨ :DL → L has itself a left adjoint. In [4] there is a characterization of sup-lattices in terms of functors L :Cop → sup (sup the category of sup-lattices and sup-preserving arrows with respect to the base topos Set). We produce a similar characterization of CCD lattices in terms of fuctors L :Cop → ccd (ccd the category of ccd lattices and arrows that preserve both, suprema and infima). Since L takes values in ccd we have, for every f :B → C in C an adjoint string ∨ f a Lf a ∧ f . This characterization hinges on the (surprising) apperance of a right adjoint to ∧ f and on a condition called complete Frobenius reciprocity.