Finite topology property + simple theorems

[artemetra]

Initial PR for #1800.
Defines Finite topology and shows finite topology => Artinian and Noetherian, needs more work

[artemetra]

@prabau I did what you mentioned, however I don't think this PR is useful as-is currently, and I suggest at least adding a space that has finite topology but isn't finite or indiscrete; and replacing (deleting?) the finite => Artinian and finite => Noetherian theorems.

[artemetra]

I added a couple more pretty simple theorems and it seems like the property has been established for all spaces now. The above comment still holds, tho.

[prabau]

Suggested change

	The cardinality of the topology on $(X, \tau)$ is finite, i.e. $|\tau| < \infty$.
	$X$ has finitely many open sets.

simpler

[prabau]

T911 is not needed here. Since indiscrete spaces are Artinian and Noetherian (already known in pi-base), the theorem will be a direct consequence of the second PR.
see #1803 (comment)

[prabau]

T909, T910: we don't want to introduce theorems showing that finite topology implies Artinian and Noetherian. Instead the existing corresponding theorems for finite spaces should be modified (T198, T825).

(When we generalize theorems we usually try to modify the less general theorem in place, except in some cases where we want to preserve the previous less general result for didactic reasons. Here, Artinian and Noetherian are not very basic properties, so it's fine to modify the results directly.)

[prabau]

I changed the name from Finite topology to Has a finite topology to make the discussion easier.
Now deciding between (1) Has a finite topology and (2) Has finitely many open sets.

I like (2). But the reason I had suggested the shorter name (1) was that a shorter name makes things easier to grasp when used in theorems. Long property names that are basically a description of the meaning seem harder to handle in that context.

But maybe (2) is not that bad after all. So why don't we do the following: change the name to (2) and see how we feel about it after the second PR.

Note: we do not need an "alias" in this case. Aliases are meant to be terminology commonly used in the literature, so that someone looking for the property under that name would be able to more easily find the property in pi-base. Since the current property usually does not appear in the literature and certainly not with a well-known name, aliases serve no purpose here. So bottom line: don't add Has a finite topology as an alias.

@StevenClontz fyi

[prabau]

@artemetra T912: I find this a little cryptic maybe. Can you explain here in words what the reasoning is?

Wait, I think I get it:
Kol(X) is finite, and is equal to X since X is T0. So X is finite.

[prabau]

T911 indiscrete => finite topology.
Thinking some more about it, we can keep this. But we can and should remove T251 indiscrete => compact then.
Not sure if other results involving indiscrete can be cleaned up further. I have not looked at it.

[felixpernegger]

We can improve T823

[prabau]

and remove T658 at the same time. There must be more cleanup of that kind lying around. Not sure we want to do it all necessarily in this PR. But maybe ok if it's kind of trivial.

[felixpernegger]

@artemetra I think once you apply all the suggestions we are ready to merge

[felixpernegger]

Also, I fixed a small typo and indendation error and applied it directly, I hope you mind

[prabau]

@artemetra I think once you apply all the suggestions we are ready to merge

@felixpernegger You often say exactly the same thing, and often something comes up after the suggestions are applied. Would be good to first have the suggestion applied and then analyze the results further. As there may be further suggestions that have not been given yet. (Sorry for the rant)

[prabau]

Suggested change

	aliases:
	- Has a finite topology

per #1803 (comment)

[prabau]

Suggested change

	Follows from the Kolmogorov quotient being finite.
	$\text{Kol}(X)$ is finite, and is equal to $X$ since $X$ is {P1}. So $X$ is finite.

#1803 (comment)

[prabau]

@artemetra There were several further suggestions in the discussion above that need to be applied, regarding T909, T910, and other related theorems. Still working on it, I assume?

[prabau]

need more work (ensures that the PR does not get prematurely approved and merged)

[felixpernegger]

@artemetra I think once you apply all the suggestions we are ready to merge

@felixpernegger You often say exactly the same thing, and often something comes up after the suggestions are applied. Would be good to first have the suggestion applied and then analyze the results further. As there may be further suggestions that have not been given yet. (Sorry for the rant)

I have been making PRs in this repo for ~8 months now (and in that timespan almost the majority of all PRs were made by me) as well reviewed many others. I think am I qualified to make judgement calls.
It is not necessary at every single PR for you to give the final approval to go ahead, especially if you have shared suggestions already (which were implemented). You don't do the same in other PRs as well.

[prabau]

@artemetra I think once you apply all the suggestions we are ready to merge

@felixpernegger You often say exactly the same thing, and often something comes up after the suggestions are applied. Would be good to first have the suggestion applied and then analyze the results further. As there may be further suggestions that have not been given yet. (Sorry for the rant)

I have been making PRs in this repo for ~8 months now (and in that timespan almost the majority of all PRs were made by me) as well reviewed many others. I think am I qualified to make judgement calls. It is not necessary at every single PR for you to give the final approval to go ahead, especially if you have shared suggestions already (which were implemented). You don't do the same in other PRs as well.

Of course not. But for this particular PR there were several things that still needed to be applied. And the PR should not have been approved without further changes and discussion.

[prabau]

@felixpernegger I guess for next time, if I have further pending comments, I should say it up front. Sometimes I don't say it so that the discussion can be focused on one thing at a time. My bad.

[felixpernegger]

@felixpernegger I guess for next time, if I have further pending comments, I should say it up front. Sometimes I don't say it so that the discussion can be focused on one thing at a time. My bad.

Good idea, no worries