Vtyjkyuk

I will use letters such as $p$, $q$ for filters (or ultrafilters).

I want to ask about correspondence between iterated limit and $potimes q$-limit, but let me start by mentioning the relevant definitions and notation.
$requirebegingroupbegingroupnewcommandFlim[2]limlimits_#1to#2$

Tensor product. Let $p$ be a filter on a set $X$, $q$ be a filter on a set $Y$. Then the system
$$Asubseteq Xtimes Y; x; y; (x,y)in Ain qin p$$
is a filter on $Xtimes Y$. This filter is called tensor product or Fubini product of the filters $p$ and $q$ and denoted by $potimes q$.

If we denote $A_x=y; (x,y)in A$ the $x$-cut of the set $A$, then we can say more briefly
$$Ain potimes q Leftrightarrow x; A_xin qin p.$$
For people who are used to work with filter quantifiers¹ this can also be expressed as
beginalign*
Ain potimes q
&Leftrightarrow (forall_p x) A_xin q \
&Leftrightarrow (forall_p x) (forall_q y) (x,y)in A \
endalign*

It can be shown that if both $p$ and $q$ are ultrafilters, so is $potimes q$.

Limit along a filter. If $p$ is a filter on $X$, $T$ is a topological space and $fcolon Xto T$, then we say that $ell$ is $p$-limit of $f$ and write
$$Flim xp f(x)=ell$$
if for every neighborhood $U$ of $ell$ the preimage $f^-1[U]$ belongs to $p$, i.e.,
$$f^-1[U]=xin X; f(x)in Uin p.$$
This notion generalizes various types of limits. Some links to further references are given below.²

For the sake of simplicity, we will always assume that $T$ is Hausdorff, which gives us uniqueness of the $p$-limit.

An important property is that if $p$ is an ultrafilter and $T$ is compact, then the $p$-limit exists.

Correspondence. Let $fcolon Xtimes Yto T$, where $T$ is a compact Hausdorff topological space. Then for any two ultrafilters $p$ on $X$ and $q$ on $Y$, we have
$$Flim xp Flim yq f(x,y) = Flim(x,y)potimes q f(x,y)$$
in the sense the limit on the one side of the above equality exists, then so does the other one and the limits are equal to each other.

In fact, the above property characterizes the tensor product of ultrafilters. (In the sense that there exists unique ultrafilter on $Xtimes Y$ with the above properties. To see this it suffices to take $T=0,1$ with discrete topology and notice that $Flim xp chi_A(x)=1$ iff $Ain p$, so if we know limits of indicator functions, this uniquely determines the filter.)

If we only require $p$ and $q$ to be filters, then the existence of the iterated limit implies the existence of $potimes q$-limit. (But not conversely.) For this implication we can also omit the assumption that $T$ is compact.

When I searched for some references for this fact, I was able to find some places mentioning that
$$potimes q = Flim(x,y)potimes q (x,y)$$
for any $pinbeta X$, $qinbeta Y$; where we consider $X$, $Y$ endowed with the discrete topology and the ultrafilters are viewed as points of the Stone-Čech compactification. I found this claim for example as Lemma 11.2 in Hindman-Strauss: Algebra in the Stone-Čech Compactification (2nd edition). (The proof is left to the reader as an exercise.)

This is a special case of the above result if $f = e_Xtimes e_Y colon Xtimes Y to beta Xtimesbeta Y$ is product of embeddings into the corresponding compactifications. Maybe also the above result can be deduced from this, although I do not see an immediate way to show this.

Questions. I am interested both in references for this result and in a proof. (I have included my own proof as an answer, if there are alternative proofs or if my proof can be simplified, I'd be glad to learn about that.) It would also be nice to know whether some assumptions can be omitted. (But I do not think that it's possible to go too far beyond for what I have already mentioned - that in one direction you only need filters rather than ultrafilters and also the compactness assumption can be omitted.)
$endgroup$

¹See also this question and references there: References on filter quantifiers.

²For some references related to limit along filter (or filterbase) see Where has this common generalization of nets and filters been written down? or Basic facts about ultrafilters and convergence of a sequence along an ultrafilter.

$requirebegingroupbegingroupnewcommandFlim[2]limlimits_#1to#2$
Claim. Let $fcolon Xtimes Yto T$, where $T$ is a compact Hausdorff topological space and $ellin T$.
Let $p$ be an ultrafilter on $X$ and $q$ be an ultrafilter on $Y$.
Then we have
$$Flim xp Flim yq f(x,y) = ell qquadLeftrightarrowqquad Flim(x,y)potimes q f(x,y)=ell.$$

Proof. $boxedRightarrow$ For any fixed $xin X$ we have that the limit
$$Flim yq f(x,y) = g(x)$$
exists. And we also have $Flim xp g(x) = ell$.

If $U$ is a neighborhood of $ell$, then $g^-1[U]in p$. Now for each $xin g^-1[U]$, the set $U$ is also a neighborhood of $g(x)$. So from $Flim yp f(x,y) = g(x)$ we get for the $x$-section of $f^-1[U]$ that
begingather*
y; f(x,y)in U in q\
x; y; (x,y)in f^-1[U]in q supseteq g^-1[U]
endgather*
and, consequently, this set belongs to $p$.

So we get that
begingather*
x; y; (x,y)in f^-1[U]in q in p\
f^-1[U] in potimes q
endgather*
for every neighborhood of $ell$ and thus
$$Flim(x,y)potimes q f(x,y)=ell.$$

$boxedLeftarrow$ For every $x$ let us denote $g(x)=Flim yq f(x,y)$. (We know that this limit exists since, $q$ is an ultrafilter and $T$ is compact. For the same reasons we now that the limit $Flim xp g(x)$ exists.)

Let $U$ be a neighborhood of $ell$. Then we know that $f^-1[U] in potimes q$ which means that
$$A:=x; y; (x,y)in f^-1[U]in q in p.$$
Now let us fix $xin A$ and let us denote $f_x:=f(x,cdot)$, i.e, $f_x colon Yto T$ is the map given by $f_x(y)=f(x,y)$, i.e.,
$$f_xcolon y mapsto f(x,y).$$ Notice that $xin A$ means that
$$f_x^-1[U]=y; (x,y)in f^-1[U]in q$$
We know that
$$Flim yq f_x(y)=g(x).$$
Thus for every neighborhood $V$ of $g(x)$ we have
$$f_x^-1[V] = y; (x,y)in f_x^-1[V]in q.$$
Combining these two facts we get
$$f_x^-1[Ucap V] in q.$$
In particular, this implies that $U cap V$ is non-empty for every neighborhood $V$ of $g(x)$ and thus
$$g(x) in overline U.$$
From this we get that also $$Flim xp g(x)inoverline U.$$
Since we are working in a regular Hausdorff space and this is true for every neighborhood of $ell$, we finally get
$$ Flim xp Flim yq f(x,y) = Flim xp g(x) = ell.$$

You may notice that in the proof of implication $boxedRightarrow$ we only needed that $p$ a $q$ are filters and we also did not need compactness.

In the proof of $boxedLeftarrow$ we used both that $p$, $q$ are ultrafilters and $T$ is compact, since we needed existence of the limits $Flim yq f(x,y)$ and $Flim xp g(x)$.
$endgroup$