Simple theorems for Artinian (P226)

[felixpernegger]

This solves the Artinian property for most spaces.

For the palestinian paper I didnt find a zbmath or DOI, so I just linked it directly.
The two papers I referenced dont appear to contain anything more useful.

If someone has any other ideas for simple theorem, this would be a good time.

The palestinian paper also mentions that there are Spectral + Artinian spaces which are not Noetherian (which is a little bit surprising since of course every Artinian ring is Noetherian), that would be a good space to add in my opinion.
EDIT: S166 already does this

[prabau]

I had a few suggestions for the first Artinian PR.
Should I write an easy PR for it, or just add a commit to this PR and we can discuss?

[felixpernegger]

I had a few suggestions for the first Artinian PR. Should I write an easy PR for it, or just add a commit to this PR and we can discuss?

Since I think it is good to encourage the easy label, making a PR would be a good idea in my opinion haha

[prabau]

I need to touch the same file P206. So how about I do a commit for that file here. And then I'll do a separate PR for the other files.

[felixpernegger]

yes sure

[prabau]

Wondering about an extension of T827. Can there be an infinite sober space that is Artinian?

[prabau]

For P226, Every nonempty collection of open/closed sets has a minimal/maximal element:
Minimal/maximal is with respect to inclusion. I assume that's kind of obvious and there is no need to say it, right?

[prabau]

Looking at the proof for T830 in the preview screen, in spite of what we talked about previously, wouldn't it be better in this case to rephrase T824 as [Artinian + T1 => finite] ?
That would match better with some of the other theorems here.

What do you think?

[prabau]

Not convinced it's worth to add the "finitely many open sets" property here.
But I am starting to see the advantage. :-)

[prabau]

Suddenly I can't refresh the artinian-theorems branch in preview mode.
It's maybe a problem with amazon?

[yhx-12243]

Suddenly I can't refresh the artinian-theorems branch in preview mode. It's maybe a problem with amazon?

Now you can. Because you added a contradiction then but you fixed just now.

[prabau]

Thanks for fixing the contradiction.

[prabau]

Another result: Artinian => separable.

We can even say that there is a finite set that is dense in $X$. Not sure if there is a property that matches this in pi-base.

Cannot be derived from other theorems. Do other theorems become redundant with this?

[prabau]

Also: [Artinian + T0 + not empty => has isolated point]

(As an aside, the set of isolated points is dense in $X$.)

Allows to derive that S200 (right ray topology on $\omega$ ) is not Artinian, which is still unknown with the other thms.

[felixpernegger]

Also: [Artinian + T0 + not empty => has isolated point]

(As an aside, the set of isolated points is dense in X .)

Allows to derive that S200 (right ray topology on ω ) is not Artinian, which is still unknown with the other thms.

This can be strengthened to Scattered (P51), right?

[prabau]

Yes! Then we don't need the nonempty hypothesis.

[felixpernegger]

Another result: Artinian => separable.

We can even say that there is a finite set that is dense in X . Not sure if there is a property that matches this in pi-base.

Cannot be derived from other theorems. Do other theorems become redundant with this?

Most likely some theorems are redundant now, but lets first collect all and then sort out I say.

[felixpernegger]

@prabau
I wont work on this anymore today, but do you have an idea how to enocde

1. Artinian + Hereditarily connected (sort of like cofinality, but in the other direction)
2. the fact that Artinian spaces have finitely many connected components

in a suitable way?

[prabau]

latex still has a problem.

[prabau]

@prabau I wont work on this anymore today, but do you have an idea how to enocde

1. Artinian + Hereditarily connected (sort of like cofinality, but in the other direction)

2. the fact that Artinian spaces have finitely many connected components

in a suitable way?

I need to give it some thought.

[prabau]

One thing I did notice. In an Artinian space discrete subsets must be finite.
Pi-base does not have a direct property for that, but at least all closed discrete sets must be finite, which is P21 (weakly countably compact = limit point compact).
So we get:
[ Artinian => weakly countably compact ]

This allows to derive two more space are not Artinian: S47 and S51 (Khalimski line).

---

Also we would have [Artinian => countable spread ].
That one does not give any additional traits.

Not sure if we need all these theorems actually. Like you said, we should at least determine which are redundant, and then which ones are useful for deriving currently unknown traits.

[prabau]

Suggested change

	- P000001: true
	- P000226: true
	- P000226: true
	- P000001: true

more parallel to T824

[Moniker1998]

You'd have to modify all of those then. @prabau Look at the page of Artinian

[prabau]

right. I want to see first which ones will remain after the cleanup

[Moniker1998]

All of them except for T824 have Artinian in the last place

[Moniker1998]

This theorem adds nothing new. It should be deleted. This is because totally disconnected already implies $T_1$.

[Moniker1998]

Should be modified after deletion of T828

[prabau]

Suggested change

	For $x \in X$, let $U_x\subseteq X$ be its minimal open neighborhood, this is well-defined by {T824}.
	Let $U_z$ be a minimal member of the collection $\{U_x\mid x \in X\}$.
	Suppose $U_z$ contains $y \neq z$. Then by {P1} it follows $U_y \subsetneq U_z$, contradiction.
	Therefore $X$ has an isolated point. Since both {P1} and {P226} are hereditary, the assertion follows.
	Let $A$ be a nonempty subset of $X$.
	Let $U$ be a minimal open set in $X$ with $U\cap A\ne\emptyset$.
	The set $U\cap A$ cannot contain two distinct points;
	otherwise, by the {P1} property there would be an open set $V$ in $X$ containing one point and not the other.
	Then $U\cap V$ would be a strictly smaller open set that meets $A$, which is not possible.
	Thus, the element of $U\cap A$ is isolated in $A$.

We cannot use T824 here. The proposed change is more direct.

[Moniker1998]

@prabau why did you delete this and added it after?

[prabau]

It's because a commit (yours I think) happened on that file right before I clicked to add my comment the first time. And because it touched the same lines, for some reason my change did not appear in the "Files changed" tab.
So I redid it on top of your change, and now it shows up.

[Moniker1998]

What's the purpose of announcing you are proving some kind of claim? Just delete that part.

[Moniker1998]

@prabau oh okay you mean the one which fixed TeX by yhx. Yeah, yours were still old. But that commit is irrelevant if you're rewriting it anyway.

[prabau]

you are right. Modifying it.

[Moniker1998]

This proof could be modified to show that an Artinian space has a dense finite subset. Also it shows hereditarily separable since those spaces are hereditarily separable.
If you take $\omega_1$ with topology by $[\alpha, \omega_1)$ then it should be Artinian but not have a countable network. So this is pretty strong.

In fact Artinian is equivalent to hereditarily finitely dense i.e. every $Y\subseteq X$ has a finite dense subset.

[prabau]

For dense finite subset, see #1575 (comment). I don't see a property in pi-base for that. Not worth introducing at the moment, but could potentially be useful in the future.

Hereditarily separable is a good idea. I'll modify my suggested change below.

[Moniker1998]

@prabau what? I mean it should be added as equivalent characterization for this space. Just like how we have hereditarily compact for Noetherian.

Edit: Oh you mean the proof? I meant we could show something stronger just for people who want to view the proof. Not that we modify the theorem.

[prabau]

I see what you mean. I'll leave my suggested change alone then. And then Felix can applied it and it can be further changed afterwards?

Or what do you think would be the best way to do this? (I also wanted to change a few more files from the previous PR, not touched yet in this PR)

[Moniker1998]

Honestly I was thinking that maybe editing suggestions is not a good idea, but then again someone will go and approve a PR prematurely. So it's lesser of the two evils. I think we should just focus on the readme first (maybe it's in the paper by the Polish authors). Then modify everything and if it doesn't fit we'll just resolve these things.

[prabau]

converted to draft, until things settle down
(It was one of @StevenClontz guidelines if I remember correctly: while things are being worked on, move it to draft to avoid premature approval.)

[prabau]

Suggested change

	Consider the collection of closed sets $\{\operatorname{cl}(C)\mid C\subseteq X\text{ is countable}\}$ and let $\operatorname{cl}(D)$ be a maximal element thereof. Suppose $\operatorname{cl}(D) \neq X$, then choose some $x \in X \setminus \operatorname{cl}(D)$ and we get $\operatorname{cl}(D)\subsetneq \operatorname{cl}(D\cup \{x\})$, contradiction.
	Let $C$ be a maximal separable closed set in $X$.
	If $C\ne X$ with $x\in X\setminus C$, the set $C\cup\overline{\{x\}}$ would be a strictly larger separable closed set, which is not possible.
	So $X=C$ is separable.

more direct

[Moniker1998]

Actually I think we should modify the read me and put in an equivalent characterization of Noetherian. And then cite that. Or something like this. Actually most of these theorems follow from that characterization.

[Moniker1998]

See my comment under this file.

[Moniker1998]

@felixpernegger @prabau

So the question here is, the articles mentioned already are most likely one of the very few places in which this property is discussed (the peak of the cream if you will). As such we might not be able to find an equivalent characterization:

$X$ is Artinian iff for every $Y\subseteq X$ there is finite $F\subseteq Y$ dense in $Y$

As such, maybe we should add this to pi-base without comment? This is an easy to show equivalence. What do you think?

Alternatively we could try playing around with mathse and try to show it there somehow and then add it as reference. But I don't know how we'd do that.

Edit: On the other hand, the cited paper does not prove the equivalences either. So might as well pack it all into a math.se question where someone is proving (either by self-answered question or not) that all of these are equivalent.

[prabau]

I think that equivalence is worth adding as an equivalent characterization. And it's kind of straightforward, so I don't think we need an explicit proof. But if someone wants to post a question on mathse, I am sure someone out there will give an answer, which is easy. I don't want to ask or answer myself.

[Moniker1998]

I think that equivalence is worth adding as an equivalent characterization. And it's kind of straightforward, so I don't think we need an explicit proof. But if someone wants to post a question on mathse, I am sure someone out there will give an answer, which is easy. I don't want to ask or answer myself.

I'll write a self-answer.

Also notice "minimal" vs "minimum" element.

[Moniker1998]

@felixpernegger

Add this post https://math.stackexchange.com/questions/5117935/equivalent-definitions-of-an-artinian-space as another reference to README, add an equivalent definition for Artinian space, and then we will continue with this PR.