Meta-properties section in Property pages

[prabau]

As we have remarked multiple times in the past, it would be a nice long-term goal if pi-base understood meta-properties of properties (like hereditary, hereditary for closed sets, preserved by finite products, etc, etc.) and was able to derive traits of spaces based on combinations of our current theorems and theorems involving meta-properties.

(See also for example this comment: #1057 (comment))

At one point, we had discussed the first steps we could take to enhance the pi-base data infrastructure to support some of this meta-information in a more organized fashion, even without the web engine deduction enhancements. But even that seems out of reach at the moment.

So a more modest goal for now could be to allow an optional "Meta-properties" section in Property pages, where it may make sense. I'd say certainly if it is useful in proofs of traits or theorems for now. But of course, it could be expanded a lot beyond that.

For an example, see at the bottom of https://topology.pi-base.org/properties/P000109 (monotonically normal).
(I added that section, as I needed to refer to the fact that "monotonically normal" is hereditary, as that was used in a few of the proofs of theorems.) One advantage of such a consolidation is that we can quote a reference proving the meta-property in just one place, and then refer to it multiple times from traits and theorems that use it.

Another example: https://topology.pi-base.org/properties/P000187 (W-space). See the Note at the end.

I'd be curious to see what people think about adding meta-property information in this fashion in general.

[yhx-12243]

Wow it's indeed a great idea I've waiting for a long time (after all, product, subspace, quotient, sum with finite, countably infinite, arbitrary ...), and it'll be a better database for it 👏
But maybe it is a vast project and maybe need many steps (My thought is that, in the later stage, for example, we may have:

• if A + B => C, A hereditary, B hereditary, and automatically C hereditary,
• We can also mark relationship between spaces. Take product as an example, we can mark S31 = S29^2, and auto deduce some property, e.g., KC, is not product-closed,
• e.g. We can mark T5 as hereditary version of T4 and deduce T663 from T661,

Anyway, this is only a very long-term planning and maybe hard to implement, that's totally OK 😀)

[GeoffreySangston]

A follow-up step which I think is also not too difficult would be to give meta-properties their own files, either just in the directory for that property, or also in a new top level directly parallel to spaces, properties, and theorems if ever that makes sense. Then when adding a meta-property to the description of a property, we add it as a link to that meta-property's file.

The reason for the claim that this is not too difficult is that I'm not presently suggesting any change about the pi-base logic. I'm just foreseeing an issue where some properties may have a lot of relevant meta-properties, and when that happens it may make the property file very long. This could make it unwieldy to include proper references and justifications for the meta-properties of that property.

It remains to be seen if this will be necessary.

[StevenClontz]

Something that seems be reasonably easy to implement on the software side is a simple tagging system. This could be used however the community feels is useful: we can tag spaces that require CH, properties that are hereditary, etc., and then get lists of things that are tagged. Maybe tags can have Markdown justifications, or that info can just go into the description.

[StevenClontz]

@prabau do we think this would be better as a Discussion thread than an Issue? I can't remember if we drew the line somewhere between Issues/Discussions for this particular project.

[prabau]

A follow-up step which I think is also not too difficult would be to give meta-properties their own files, either just in the directory for that property, or also in a new top level directly parallel to spaces, properties, and theorems if ever that makes sense. Then when adding a meta-property to the description of a property, we add it as a link to that meta-property's file.

The reason for the claim that this is not too difficult is that I'm not presently suggesting any change about the pi-base logic. I'm just foreseeing an issue where some properties may have a lot of relevant meta-properties, and when that happens it may make the property file very long. This could make it unwieldy to include proper references and justifications for the meta-properties of that property.

It remains to be seen if this will be necessary.

Actually, your proposal was exactly what we had discussed of doing, with the help of @Not-Abram. But it seems even that may be too much to implement right now? @StevenClontz

[prabau]

@prabau do we think this would be better as a Discussion thread than an Issue? I can't remember if we drew the line somewhere between Issues/Discussions for this particular project.

I initially thought of making this a Discussion. But then thought that Discussions are kind of ignored by most people and it would seem to get more attention as an issue? We can mention this tomorrow maybe, but I don't want to derail the meeting by rehashing this topic, as there are already a lot of other issues that I think should be discussed instead

The main thing is to get people's attention and then discuss how best to move forward. Maybe for the community meeting after the next one?

[StevenClontz]

But then thought that Discussions are kind of ignored by most people and it would seem to get more attention as an issue?

My thought as well - I'm happy with the norm that we don't care too much about Issue vs Discussion distinction for now. And agreed we have more to discuss this Friday, so I'll make a placeholder Jan community call thread with this on the agenda.

[StevenClontz]

Actually, your proposal was exactly what we had discussed of doing, with the help of @Not-Abram. But it seems even that may be too much to implement right now? @StevenClontz

Unfortunately, we kept ourselves busy enough with some smaller tasks - his senior project is also an honors thesis, so we have to move on now to finishing up a survey on research software engineering in mathematics and then start everyone's favorite part of research: writing.

[prabau]

We can also add this whole topic of Meta-properties as another item of discussion for the Jan zoom.

[Moniker1998]

The problem I see is to what extent we should provide proofs to meta-properties