How can one prove Tychonoff's theorem using ultrafilters?

Tychonoff's theorem, as a reminder, says that the product of a possibly infinite number of compact spaces is compact (a compact space being a space every open cover of which has a finite subcover; this is sometimes called quasi-compactness, as in the Stacks Project).

Interlude: the typical way of proving Tychonoff's theorem

If one proves the Alexander subbase theorem (that, given a subbase $S$ of a topological space $X$, $X$ is compact whenever all open coverings of $X$ that are subsets of $S$ have finite subcoverings), it is not hard to prove Tychonoff's theorem. To do so, let us set the $X$ and $S$ needed for applying the Alexander subbase theorem: let our topological space $X$ be $\Pi_n X_n$,¹ the product space of infinitely many $X_n$, and let our subbase $S$ be the set of inverse images of open sets under the projections $\pi_n: X → X_n$. Then let $\mathcal{O} \subseteq S$ be an open covering of $S$.

It is then clear that every element of $\mathcal{O}$ will be a product of all but one of the $X_n$ with an open set from the remaining $X_n$. Then either some of the elements of $\mathcal{O}$ will completely cover one of the $X_n$ and thus have a finite subcovering that includes all of $X$, or we will be able to find an element of $X_n$ that $\mathcal{O}$ does not cover by taking the product of the closed sets that $\mathcal{O}$ leaves uncovered in each $X_n$, basically as illustrated below:

And to prove the Alexander subbase lemma, in turn, is not hard to do using Zorn's lemma: without further ado, let $\mathcal{O}$ be a maximally coarse open covering of $X$ with no finite subcovering; then $\mathcal{O}$ must be a subset of $S$², but all open coverings that are subsets of $S$ have finite subcoverings by hypothesis, hence there is no maximally coarse open covering of $X$ with no finite subcovering, hence all open coverings of $X$ have finite subcoverings and $X$ is compact.

What about proving it using the ultrafilter lemma?

I have heard that Tychonoff's theorem is actually a quite straightforward consequence of basic theorems on ultrafilters. Proving it this way would have two advantages: the conceptual advantage of linking it to the ultrafilter-based understanding of compactness (useful elsewhere, e.g. in Stone-Čech compactification) and the axiomatic advantage of using the ultrafilter lemma instead of the more powerful Zorn's lemma. (But I'm much more interested in the conceptual advantage.)

But I have not as yet figured out how to formulate the right ultrafilter-based understanding of compactness for this task. Speaking vaguely, the approach of saying that quasi-compact spaces are those all of whose "ultrafilters" (in some sense) are principal does not seem to be getting me anywhere (I can show that products of non-principal ultrafilters extend to non-principal ultrafilters, but that's just affirming the consequent).

Hence, to restate my question: what am I missing? What is the right ultrafilter-based conception of compactness? And how does it apply to proving Tychonoff's theorem?

---

¹Where the $n$ are elements of a not necessarily countable indexed set $I$.

² How do we prove this? Suppose, for a contradiction, that $\mathcal{O}\not\subseteq S$. Then there exists $O_1 \not\in S$; since $S$ is a subbase $O_1$ is the intersection of a finite number $n$ of $S_1,…S_n \in S$. Then we have $n$ coarsenings of $\mathcal{O}$ achieved by replacing $O_1$ with $S_1$, $S_2$, … $S_n$. All $n$ coarsenings (by maximality of $\mathcal{O}$) must have finite subcoverings, and we can take the union of these $n$ finite subcoverings and replace the $S_i$ with $O_1$ to get a finite subcovering of $\mathcal{O}$, contradiction. (It's very similar, for some reason, to a technique I used here, in footnote 2…)