5 deleted 20 characters in body

In case anyone is interested, this is a rendition of the proof I was looking for, contained in the article pointed out by Andrej Bauer. (I'm not looking for upvotes; this is just to round out the discussion.)

The elegant proof of the implication I was after (see Martin Escardo's article) is perfectly constructive. So this answers completely my question: no choice is involved.

Major edit: In a previous version of this post, I had made a rash claim "above the fold" that the implication "$X$ is compact implies $\pi: X \times Y \to Y$ is a closed map for every space $Y$" seems to involve the axiom of choice. But Mike Shulman sent me an email which set me straight: if you do it right, AC is not required for this direction either.

Start with the following easy observation (which follows by playing around with complements): $\pi: X \times Y \to Y$ is a closed map precisely when the set

$$\{y \in Y: X \times \{y\} \subseteq U\}$$

is open whenever $U \subseteq X \times Y$ is open.

Now, suppose $\pi: X \times Y \to Y$ is a closed map for every $Y$. To show $X$ is compact, we show that $X$ belongs to any open cover of $X$ that is closed under finite unions. Let $\Sigma$ be such an open cover.

Construct a space $Y$ as follows: the points of $Y$ are open sets of $X$, and the open sets of $Y$ are subsets $W \subseteq Y$ such

• $W$ is upward-closed: if $U \in W$ and $U \subseteq V$ for $V \in Y$, then $V \in W$, and

• $\Sigma \cap W$ is nonempty (unless $W$ is empty).

It is straightforward to check this defines a topology on $Y$ (that the intersection of two opens $W$, $W'$ of $Y$ is again open uses the fact that $\Sigma$ is closed under finite unions).

Observe that if $U$ belongs to $\Sigma$ and $U' \subseteq U$, the principal upward-closed set $prin(U') = \{V \in Y: U' \subseteq V\}$ is open in $Y$.

Now consider the set $E = \{(x, U) \in X \times Y: x \in U\}$. Claim: this is open in $X \times Y$. Proof: for every $(x, U) \in E$, let $U' \in \Sigma$ the set $U \times prin(U)$ is an open set which contains $(x, U)$, and $U \times prin(U) \subseteq E$ because for every $(y, V) \in U \times prin(U)$, we have $y \in V$. Given $(x, U) \in E$, there exists $U' \in \Sigma$ containing $x$ (since $\Sigma$ is a cover), and then for $U'' = U \cap U'$, the set $U'' \times prin(U'')$ is an open that contains $(x, U)$, and this is included in $E$ because $y \in V$ for every $(y, V) \in U'' \times prin(U'')$.

By the open-set reformulation of the closed map condition, the set

$$\{V \in Y: X \times \{V\} \subseteq E\}$$

is open in $Y$, is nonempty (because $X$ belongs to it), and so this set intersects $\Sigma$ by definition of the topology of $Y$. Thus $X \times \{V\} \subseteq E$ for some $V \in \Sigma$. But then $V$ is all of $X$! So $X \in \Sigma$ for any open cover $\Sigma$ closed under finite unions; therefore $X$ is compact.

In case anyone is interested, this is a rendition of the proof I was looking for, contained in the article pointed out by Andrej Bauer. (I'm not looking for upvotes; this is just to round out the discussion.)

The elegant proof of the implication I was after (see Martin Escardo's article) is perfectly constructive. So this answers completely my question: no choice is involved.

Major edit: In a previous version of this post, I had made a rash claim "above the fold" that the implication "$X$ is compact implies $\pi: X \times Y \to Y$ is a closed map for every space $Y$" seems to involve the axiom of choice. But Mike Shulman sent me an email which set me straight: if you do it right, AC is not required for this direction either.

Start with the following easy observation (which follows by playing around with complements): $\pi: X \times Y \to Y$ is a closed map precisely when the set

$$\{y \in Y: X \times \{y\} \subseteq U\}$$

is open whenever $U \subseteq X \times Y$ is open.

Now, suppose $\pi: X \times Y \to Y$ is a closed map for every $Y$. To show $X$ is compact, we show that $X$ belongs to any open cover of $X$ that is closed under finite unions. Let $\Sigma$ be such an open cover.

Construct a space $Y$ as follows: the points of $Y$ are open sets of $X$, and the open sets of $Y$ are subsets $W \subseteq Y$ such

• $W$ is upward-closed: if $U \in W$ and $U \subseteq V$ for $V \in Y$, then $V \in W$, and

• $\Sigma \cap W$ is nonempty (unless $W$ is empty).

It is straightforward to check this defines a topology on $Y$ (that the intersection of two opens $W$, $W'$ of $Y$ is again open uses the fact that $\Sigma$ is closed under finite unions).

Observe that if $U$ belongs to $\Sigma$, \Sigma$and$U' \subseteq U$, the principal upward-closed set$prin(U) prin(U') = \{V \in Y: U' \subseteq V\}$is open in$Y$. Now consider the set$E = \{(x, U) \in X \times Y: x \in U\}$. Claim: this is open in$X \times Y$. Proof: for every$(x, U) \in E$, let$U' \in \Sigma$the set$U \times prin(U)$is an open set which contains$(x, U)$, and$U \times prin(U) \subseteq E$because for every$(y, V) \in U \times prin(U)$, we have$y \in V$. Given$(x, U) \in E$, there exists$U' \in \Sigma$containing$x$(since$\Sigma$is a cover), and then for$U'' = U \cap U'$, the set$U'' \times prin(U'')$is an open that contains$(x, U)$, and this is included in$E$because$y \in V$for every$(y, V) \in U'' \times prin(U'')$. By the open-set reformulation of the closed map condition, the set $$\{V \in Y: X \times \{V\} \subseteq E\}$$ is open in$Y$, is nonempty (because$X$belongs to it), and so this set intersects$\Sigma$by definition of the topology of$Y$. Thus$X \times \{V\} \subseteq E$for some$V \in \Sigma$. But then$V$is all of$X$! So$X \in \Sigma$for any open cover$\Sigma$closed under finite unions; therefore$X$is compact. 3 Updated the post with better information The elegant proof of the implication I was after (see Martin Escardo's article) is perfectly constructive. One thing that struck me while working through So this (which hadn't penetrated answers completely my consciousness before, although in hindsight it is perfectly obvious) question: no choice is involved. Major edit: In a previous version of this post, I had made a rash claim "above the fold" that the implication If$X$"$X$is compact , then for every space$Y$the projection implies$\pi: X \times Y \to Y$is a closed map (using traditional open cover definition of compactness) is non-constructive. In other words, as one works through the argument, one finds one has to choose an open cover for every space$Y\$" seems to satisfy a certain condition, and involve the axiom of choiceis unavoidable as far as I can tell.

Whereas the converse implication won't require choice at all. Thus, in a sense the closed-map formulation of compactness is stronger than the traditional oneBut Mike Shulman sent me an email which set me straight: if you do it implies the traditional finite subcover condition even in the absence of a choice principleright, AC is not required for this direction either.

2 rearranged a few words
1