Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
Your change seems right to me.
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.
Okay, thanks.
I have now also added the equivalent characterization in terms of complementary open subsets. here.
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.
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 have also added the statement and proof that irreducible closed subsets are in bijection to the frame homomorphisms to the point, here.
There has been some discussion of this statement at sober space comment 16 and following. Perhaps it should be continued here.
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.
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.
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$),
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).
1 to 13 of 13