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.

[prabau]

Again, I advocate for a "Finitely many open sets" property. With it, none of this is awkward.

Not sure about it one way or the other yet. I think it should be discussed in an issue.

[Moniker1998]

Not sure about it one way or the other yet. I think it should be discussed in an issue.

No it definitely shouldn't be added.

Once we establish that Artinian + R_0 is equivalent to partition + compact, the only interesting Artinian spaces are not non-R_0 ones. And of course, Kolmogorov quotient makes it so that those are T_0 but not T_1 spaces. Now I think that almost all of such spaces look like something of the form $\kappa$ with topology consisting of rays $[0, \alpha]$ for $\alpha\in \kappa$, or their finite disjoint unions. I was wrong about my previous assesment, if you have a tree (well-ordered one), that should also be Artinian. Maybe all $T_0$ but no $T_1$ spaces are (well-ordered) trees. They aren't all trees.

We could try proving that connected + Artinian + T_0 implies Toronto, this would essentially show my claim.

I don't see how interesting would it be to introduce "has finite amount of open sets". Seems very non-interesting and useless to us.

[felixpernegger]

I dont agre its useless.

Essentially we already have

R_0 =T_1 without T_0
R_1 = T_2 without T_1
Partition Topology = Discrete without T_0

(to be precise, Kolmogorov quotient).

Therefore at least the idea that this might be useful (though not interesting, similar to T_0), is not absurd to suggest.

Most properties are preserved by Kolmogorov quotient, but some are not and for the most common properties having a second version (i.e. Kolmogorov quotient has the property) may be convenient.

[prabau]

One of the cardinality functions discussed in Hodel's chapter of Handbook of set-theoretic topology and also in Juhasz is $o(X)=$ number of open sets. In that sense, it may later on be useful to introduce other related properties like $o(X)$ at most something, etc. So it does not seem completely unreasonable to have "finite number of open sets".

In any case, we should not introduce it right now in this PR.

[prabau]

Also, as mentioned multiple times in the past, it would be really nice to enhance the deduction engine of pi-base so that it would understand Kolmogorov quotients and be able to automatically combine that with existing theorems. That would allow to simplify or remove quite a few theorems as redundant.

Unfortunately, @StevenClontz mentioned there are no development resources to work on that non-trivial enhancement.

[prabau]

@felixpernegger can you take a look at the other suggestions I made?
Then we can move this out of draft and finish it.

[prabau]

approved. Leaving it to @Moniker1998 to merge in case he wants to take a last look.

[Moniker1998]

@prabau were the indexing of theorems changed?

[prabau]

I think the indexing was changed for some of the theorems at some point. In the final result in preview mode, all theorems related to Artinian are consecutive, from T823 to T832.

[Moniker1998]

I was skeptical at keeping T824.

Logically, all of the deductions make it redundant. But it's used in the proofs of those theorems which make it redundant. So we would have to shove it inside one of these theorems anyway. @prabau

I'm guessing you want to keep it this way? Alternatively we would shove it in T830.

[prabau]

Felix wanted to keep it because the proofs of several of the other theorems were using T824 explicitly. But now this has been changed to "Explore" links ("let pi-base do the work"). So the argument to keep T824 is a lot weaker and I am not necessarily against removing T824.

@Moniker1998 Is T824 deducible by just removing it?
We can have a commit that removes it and see how things look. And further change if we don't like it.

[Moniker1998]

@prabau It's deducible. You have Artinian + T_1 then Artinian + R_0 then compact + partition.
Partition follows from Artinian then Alexandroff and Alexandroff + R_0 then partition.
None of these implications use it. And then compact + partition + T_1 then finite.

The only place where T824 is cited is T830 which I've seen. And for T830 we basically need to prove something like T824 anyway. So the benefit is only for pi-base to have one less theorem, it essentially is the same amount of work.

[prabau]

I have cloned this branch to a new branch artinian-theorems-trim with T824 removed. So we can see the result and compare side by side.

[prabau]

[Moniker1998]

@prabau interesting, so it even takes some other route than me.

[prabau]

The "Explore" links for T827 and T829 also become quite long.

@felixpernegger @Moniker1998 how does it look to you?

[Moniker1998]

@felixpernegger @Moniker1998 how does it look to you?

@prabau you mean on which branch? The Felix's one? It looks short with T824.
Should we keep it for that reason?

[prabau]

Yes. Comparing the two branches, the derivations in artinian-theorems-trim look quite a bit more involved. In the interest of simplicity, I prefer to keep what's in artinian-theorems, even if there is some redundancy.