left-adjoint to join in a Heyting algebra Define a Heyting algebra to be a bounded lattice $L$ with an operation $\to : L^{op}\times L \to L$ such that for any $x, a, b \in L$ we have $x\wedge a \leqslant b$ iff $x \leqslant a \to b$.  Thinking of $L$ as a category, this says $-\wedge a$ is left-adjoint to $a\to -$. Since $\wedge$ is the product and $\vee$ the coproduct on $L$, we get the distributivity law
$$ a\wedge(b\vee c) = (a\wedge b)\vee (a \wedge c)$$
by abstract nonsense (left adjoints preserve colimits).  This question is about proving the other distributivity law
$$ a \vee (b \wedge c) = (a \vee b) \wedge (a \vee c).$$
If we knew that $a \vee -$ was a right adjoint then this would be immediate as right adjoints preserve limits.  Is it true that in a Heyting algebra, $a \vee -$ is always a right adjoint?  If so, what is its left adjoint?
If not, I'm interested in counterexamples or characterisations of those Heyting algebras in which it is true.  I don't see this in the obvious sources (ncatlab, wiki) which deal with the second distributivity law by appealing to standard results about duality in distributive lattices or leaving it as an exercise.

 A: You probably know this already, but distributivity of $\vee$ over $\wedge$ in a lattice follows easily from distributivity of $\wedge$ over $\vee$:
\begin{align*}
(a\vee b)\wedge (a\vee c) &= ((a\vee b)\wedge a)\vee ((a\vee b)\wedge c)\\
&= a \vee ((a\wedge c)\vee (b\wedge c))\\
&= (a \vee (a \wedge c)) \vee (b \wedge c)\\
&= a \vee (b\wedge c).
\end{align*}
So if you know that $a\wedge -$ is a left adjoint, you actually get both distributive laws "for free".
To answer your actual question, $a\vee -$ is not always a right adjoint. For a counterexample, you just need to find a Heyting algebra in which $a\vee -$ fails to preserve some infinite meets. In his answer to this MathOverflow question, Andreas Blass gives a nice example: Consider the Heyting algebra of open subsets of $\mathbb{R}$. Let $a = \mathbb{R}\setminus \{0\}$, and let $b_n = (-\frac{1}{n},\frac{1}{n})$ for all $n\in \mathbb{N}^+$. Then $a\vee \left(\bigwedge_{n\in \mathbb{N}^+} b_n\right) = a$ but $\bigwedge_{n\in \mathbb{N}^+} (a\vee b_n) = \mathbb{R}$.
On the other hand, in a finite Heyting algebra, all meets are finite, so $a\lor -$ always preserves all meets. The existence of a left adjoint then follows by the adjoint functor theorem for posets. It is defined by $$L(x) = \bigwedge \{c\mid x\leq a\lor c\}.$$
Of course, verifying that this construction works requires you to know that $\vee$ distributes over $\wedge$. So this is not a route to proving the second distributive law, even in finite Heyting algebras.
