While we are at it, I would like to remark that the notion of completely primer filter is not only a better constructive rendering of that of irreducible closed set, as stated in this page, but also it is conceptually more primitive: a completely prime filter corresponds directly to a global point of the frame of open sets of the topological space, seen as a locale. Independently of not being amenable for constructive reasoning, I always felt that the notion of irreducible closed set is artificial. The notion of completely prime filter is much more natural: a completely prime filter is the open neighbourhood filter of a point which may or may not exist (it exists when the space is sober, by definition of sobriety).

]]>Another characterization of irreducible spaces: an open subspace is dense iff inhabited. (Or equivalently, the intersection of any finite number of inhabited open subspaces is inhabited.)

This should be more tractable constructively. A typical space should have lots of reducible closed subspaces, formed by taking the union of two closed subspaces $F_1$ and $F_2$, so long as neither is contained in the other. But constructively, there's no guarantee that this union will be closed. Of course, you can look at $Cl(F_1 \cup F_2)$, but then there's no guarantee that it's reducible in the sense that it's the union of two proper closed subsets.

But with the dense open subset criterion, $A \coloneqq Cl(F_1 \cup F_2)$ works. Specifically, if each $F_i$ has a point in the exterior of the other, then $A$ is reducible in the sense that it has an inhabited open subspace (in fact at least two, of the form $G_i = A \cap Ext(F_i)$) that is not dense in $A$ (in the strong sense that there is a point in the exterior of the relative closure of this $G_i$),

]]>Followup to #6: At Wikipedia/EN: Hyperconnected space, we see that irreducibility is (like compactness) actually an inherent property of a space (rather than of a space embedded as a subspace in some ambient space): a subspace is irreducible iff it's irreducibly closed within itself.

]]>By the way, my exactly-three idea in #5 is wrong. ($F$ may have proper closed subsets besides the empty one.)

ETA: I've replaced that comment with a counterexample.

]]>There has been some discussion of this statement at sober space comment 16 and following. Perhaps it should be continued here.

]]>I have also added the statement and proof that irreducible closed subsets are in bijection to the frame homomorphisms to the point, here.

]]>There is a MO question in which ‘irreducible’ is defined for any subspace, not just closed ones. In that case, rather than looking for exactly-two, the elegant thing seems to be a binary/nullary pair that can be generalized to any finite number: if an irreducible subspace is contained in the union of a finite collection of closed subspaces, then it is already contained in one of them.

]]>~~I think that there's really an exactly-~~*three* thing going on (which seems slightly less than elegant given how many things are exactly-two). A subspace $F$ (of a given topological space $X$) is irreducibly closed iff there are exactly three ways to write it as a union of closed subspaces (of $X$) contained in $F$, which then must necessarily be $\emptyset \cup F$, $F \cup \emptyset$, and $F \cup F$. (Incidentally, you don't have to state up front that $F$ is closed; that follows.)

Counterexample: Sierpiński space.

]]>Okay, thanks.

I have now also added the equivalent characterization in terms of complementary open subsets. here.

]]>The word ‘inhabited’ certainly needed to be changed to ‘proper’, but I think that there should still be an ‘exactly two’ aspect. But I guess that I don't see how that would work.

]]>Your change seems right to me.

]]>The definition that used to be at *irreducible closed subspace* seemed wrong to me. It seemed to fail to impose the condition that the two summands of the union are required to be proper subsets. (The same issue is at *sober topological space*.)
Anyway, I changed it. But (Toby should) please check if I am missing something.