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]

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]

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

[artemetra]

Sorry guys, had a few really busy days at work! Let me review.

[felixpernegger]

(Again I approve, but lets wait for @prabau to agree before merging)

[prabau]

@artemetra Please take a look at the comments above regarding T251, T823, T658. Since these changes are quite simple and fit well with the level of complexity of this PR (i.e., mostly immediate results), it would be good to deal with it at the same time. What do you think?

[prabau]

If you don't want to do this now, that's fine too, but please comment on this to mention your plan and not leave this pending.

FYI, there is also T189, T450. And possibly others.

[artemetra]

Got it, I'll look into these; if I find anything nontrivial, I think it's worth moving it into the second PR.

[artemetra]

T658 and T823 were using the same argument, so I generalized T658 to use Has finitely many open sets and deleted T823.

[artemetra]

Same thing here.

[artemetra]

I've looked for quite some time and couldn't find anything else to add so far tbh. I think we'll find more possible theorems/traits once we add the $\{\emptyset, \{p\}, X\}$ space.
@prabau fyi

[prabau]

T189: the refs section and lines 13-15 are not useful anymore. Can be removed.

[prabau]

@artemetra I took care of the comment above. Also removed the redundant indiscrete => compact and renumbered the theorems slightly so that the more basic results would have smaller theorem numbers (otherwise the deduction engine was ignoring them when deriving simple implications like finite => Noetherian for example).
Please review.

[artemetra]

LGTM. Shall we merge?

[felixpernegger]

I wanna say I am really happy that we have this property now. This is the last of a list of properties for pibase that I wished for for a long time. :)