Locally orderable spaces are radial

[prabau]

New theorem: Locally orderable => radial.

Plus some metaproperties for Radial. I added "not preserved by products" because it was not initially obvious, and could be surprising to some.

This theorem allows to derive two more spaces are radial: S40 (altered long ray) and S196 (long circle),
and two more spaces are not locally orderable: S109 (Novak space) and S110 (strong ultrafilter topology).

[prabau]

One could shorten the proof of the thm by just saying Radial is a "local property" (which is being proved as part of the theorem here) and using LOTS => radial. I just went with this longer way.

[yhx-12243]

Looks T774~T777 seem to be preserved by #1426?

[prabau]

good point. I'll change the number.

[prabau]

The metaprop that Radial (P172) is a "local property" is simple enough, so there should be no need to justify it with a mathse post or a reference to some book/paper.

Based on that, one could just shorten the justification of the theorem to the following:

This follows from the fact that {P172} is a "local" property,
and {P133} spaces are {P172}
[(Explore)](https://topology.pi-base.org/spaces?q=LOTS%2B%7ERadial).

Would that be preferable?

[Moniker1998]

@prabau to me, yes

[Moniker1998]

@prabau actually, why the quotation marks?

[prabau]

because we have not defined what it means. It could mean different things in general. In this case, it's referring to what is spelled out as one of the meta-properties, but I did not feel like repeating all that. If that's too terse, we may as well give more details about the proof.

Note: @StevenClontz has suggested that in the future there will be some kind of dictionary of often used terms in pi-base. If that happens, we can better define what we mean and have links to suitable definitions.

[felixpernegger]

A property being "local" is a well defined notion (at least in Algebra(ic Geometry) and apparently also in topology), so the quotes are not necessary.

A rather rudimentary formalisation of this in Lean would be

def IsLocal.{u} (P : (X : Type u) → TopologicalSpace X → Prop) : Prop :=
  ∀ (X : Type u) [i : TopologicalSpace X], P X i ↔ ∀ x : X, ∃ s ∈ 𝓝 x, P s instTopologicalSpaceSubtype

:)

[yhx-12243]

π-base wiki Conventions and Style has already specify how local properties means.

[felixpernegger]

π-base wiki Conventions and Style has already specify how local properties means.

Technically this only says given a property P, what (weakly) locally P means, but not the notion of a property being (weakly) local. Probably should be added.

[felixpernegger]

Having: "This property is (weakly?) local." might be useful as a metaproperty in general actually

[Moniker1998]

π-base wiki Conventions and Style has already specify how local properties means.

yes, and since this property is hereditary there should be no confusion

[Moniker1998]

@yhx-12243 @prabau
I think wiki should be updated on the whole "closed under unions" thing we discussed with countable extent and what not.
Also, we would just use that radial spaces are closed under open unions, basically. So we can just skip all the local thing.
Alternatively, we could introduce the local thing on the wiki and here.

@prabau
FYI, if you are introducing a non-standard meta-property, that's not on the wiki, I think it's a good practice to discuss that with others, so it can be filled in the wiki etc. Right now there seems to be no convention on what to do in this situation, good place to discuss this.

[prabau]

Yes, feel free to open an issue to discuss this further, so we can have the discussion in one place for the future if this does not get resolved now. We'll need feedback from @StevenClontz.

And as already discussed, my take is that saying "radial spaces are closed under open unions" does not make much sense semantically. But I know what you are trying to say.

Also, as mentioned by @yhx-12243 there are various versions of "local properties", including a weak one. I know it's the same in this case due to hereditariness. But a casual user of pi-base should be able to make sense of what they read without having to dig information in an obscure associated wiki. That's why I prefer to spell things out clearly in the meta-properties, even if it's more verbose. And again, as already mentioned, we would not have to do that if there was an extra layer of common terminology/glossary that we could link directly to.

[StevenClontz]

I haven't thought enough about the math.

Ideally, these definitions would be in the pi-base/data repo and subject to all the peer review / pull request workflows any other content would be subject to. But that requires time to work on the infrastructure I don't have. (I'm writing a grant proposal due in about a week or so that would change this...)

However, what do we think about using https://github.com/pi-base/data/wiki to track this information for now, and linking to there? We already do this somewhat at https://github.com/pi-base/data/wiki/Conventions-and-Style We can add a note to the top of a page like https://github.com/pi-base/data/wiki/Definitions reminding folks that edits should not be made without an appropriate discussion as part of an Issue or PR.

Does that clear up the input needed from me? Another iron in the fire: I'm hoping to start having regular https://mathbases.org/ community calls, and on alternate weeks the intent is to provide a virtual space for projects like ours to hop into breakout rooms to discuss business and/or onboard new contributors. I'll share more when that progresses...

[prabau]

Thinking about it some more. Maybe it's easier than I thought.

Suppose P is some property that applies to topological spaces. From P there are various "derived properties":

• X is locally P = each point has a nbhd base, each member of which satisfies P.
• X is weakly locally P = each point has a nbhd satisfying P.
• various other variants, open nbhds, open nbhds within other nbhds such that ..., etc (it can get pretty involved, see for example the discussion in Property Suggestion: Fundamental group properties #1576 and the various links there, for locally simply connected and related properties)

The first two above are the common cases. So assuming the terminology for these two cases is understood, isn't what we want to say the following:

"If $X$ is weakly locally radial, then $X$ is radial."

So what is the best way to express this in a meta-property?

[prabau]

However, what do we think about using https://github.com/pi-base/data/wiki to track this information for now, and linking to there? We already do this somewhat at https://github.com/pi-base/data/wiki/Conventions-and-Style We can add a note to the top of a page like https://github.com/pi-base/data/wiki/Definitions reminding folks that edits should not be made without an appropriate discussion as part of an Issue or PR.

That's fine to do that. But the issue is: what can we show on a particular pi-base web page to indicate what is meant by some particular terminology, understandable by a casual user of pi-base? e.g., if we talk about "weakly locally ABC" without defining it, in a meta-property for example, how can we indicate the precise meaning of it?

Would linking to the wiki from a pi-base page be possible?

[Moniker1998]

The first two above are the common cases. So assuming the terminology for these two cases is understood, isn't what we want to say the following:
"If X is locally radial, then X is radial."

@prabau I think we actually want to say that X is weakly locally radial. Maybe it's better to use the union of open sets property (however you would like to phrase it).

(the locally radial adds unnecessary complexity - we'll probably rarely be using "locally" in this sense)

[prabau]

Like you said before, because radial is hereditary, the derived properties "locally radial" and "weakly locally radial" are equivalent. The wiki (https://github.com/pi-base/data/wiki/Conventions-and-Style#local-properties) mentions that in such a case we would name the property with the shorter form "locally radial". That's if we had to introduce this as a property name.

I agree though that it would make more sense for the meta-property to state "weakly locally radial" as a hypothesis.
And I also agree that it seems too complicated for casual users.

Again, what's wrong with the original suggestion (more verbose, but clear):
"A space that is locally {P172} (every point has a neighborhood with the property) has the property."

or maybe (too long?)
"A space that satisfies the property (weakly) locally (every point has a neighborhood with the property) also satisfies the property."

or without mentioning the word "local" ?
"A space in which each point has a neighborhood with the property also satisfies the property."

or shorter ?
"If each point has a neighborhood with the property, $X$ also satisfies the property."
"If each point has a neighborhood with the property, $X$ also has the property."

I am not opposed to union of open sets either, if we can phrase it properly. My above formulation was in terms of nbhds, not open nbhds, which was intentional, and maybe preferable in general (e.g., "locally compact" with open nbhds usually does not work).

[StevenClontz]

Would linking to the wiki from a pi-base page be possible?

Yes, that's what I had in mind. pi-Base pages are just markdown, and thus support links to arbitrary URLs (like we do sometimes to preprints/fulltexts). So we could do something like:

Meta-Properties

• This property is weakly local

and not have to spell out everything in every file in the database.

[StevenClontz]

Long-term, maybe we need to support arbitrary "pages" in the pi-Base software. So when there's a shared concern used by multiple different objects/properties/theorems, we can write up something on a "page" and link to it. (And these "pages" would be subject to the same peer review as the rest of our data, so we can count on them being as curated as anything else in the database.)

[prabau]

Would linking to the wiki from a pi-base page be possible?

Yes, that's what I had in mind. pi-Base pages are just markdown, and thus support links to arbitrary URLs (like we do sometimes to preprints/fulltexts). So we could do something like:

Meta-Properties

• This property is weakly local

and not have to spell out everything in every file in the database.

That could be a good solution for now. We could have a "glossary page" somewhere on the wiki, for now. And we could link directly into it.
Ideally we could link directly to a particular definition in the glossary. Not sure how to do that, but it should not be hard with some sort of anchoring tags?

[prabau]

Separately from the use of a glossary page in the wiki:
For what to use for the radial meta-property, I still think it will be easier for now to go with my simpler suggestion above. Let me do the change and then we can discuss further if we agree to that, or do some more general meta stuff. (We can always change things later after the PR is merged.)
Both meta-property and the theorem are simpler now.

[Moniker1998]

@prabau I think this meta-property is fine, but if we're going to go with it then it needs to be on the wiki. Also the other property we've added.

[prabau]

Added this one to the wiki. We can add other ones as we start using them, so we'll have more context to decide the best phrasing.

[StevenClontz]

Not sure how to do that, but it should not be hard with some sort of anchoring tags?

example: https://github.com/pi-base/data/wiki/Conventions-and-Style#meta-properties

[Moniker1998]

Added this one to the wiki. We can add other ones as we start using them, so we'll have more context to decide the best phrasing.

@prabau I mean the one we've already used for the countable extent

[prabau]

added