Community Meeting July 21 4pm Eastern

[StevenClontz]

This is the Friday of Summer Topology Conference, but we do not conflict with any talks/sessions.

Agenda:

• Spaces that rely on more than ZFC, e.g. https://topology.pi-base.org/spaces/S000147
  • Decision: mark e.g. additional_axioms: CH, and stop using ambiguous_construction throughout
• Handling equivalent properties, e.g. P70 and P71.
• Revisit the removal of deprecated theorems
  • Condensing some equivalent properties involving Menger-like principles #347 (comment)
  • Decision: okay to have some equivalent properties/theorems. But also okay to combine/delete if duplication isn't helpful (check Math.SE and MO for references first)
• Considering spaces as special properties.
  • (punt for now)
• Issues with non-optimal deducations
  • Decision Steven will sync with James on this topic as well as new web interface bugs

[ccaruvana]

As discussed in https://github.com/orgs/pi-base/discussions/320, we may want to check in on how to represent special constructions that rely on independent but consistent axioms like CH. Currently we have Space 147, Luzin sets, that rely on more than ZFC to exist. Perhaps we can add some sort of special alert tag to appear in the search feature.

[StevenClontz]

It would be interesting to consider whether it'd make sense to refactor pi-Base someday to remove spaces as a separate concept, and just "tag" the properties that are satisfiied by only one space up to homeomorphism.

Then the "traits" of a space can use the same infrastructure as theorems as they are space => property pairs.

I don't think a human wants to really think about managing our content like this, but maybe the distinction of spaces vs properties can just be syntatic sugar used for data entry.

[StevenClontz]

Put another way: I don't think I ever actually want a space => property theorem (and definitely it doesn't need a name like T123456), but there are plenty of properites => space theorems that would be useful to have in the pi-Base.

[prabau]

Item for the agenda: revisit the removal of deprecated theorems, given mathse/mo search for usage with the "url:" syntax.

[StevenClontz]

I believe out of the regulars just @lyengulalp is at the summer topology conference, so let's plan for those of us available to sync up on Friday at Clontz.org/zoom at 4pm Eastern.

[prabau]

Minor item: an illustration that the chain of deductions are not always optimal. Compare these two:

• https://topology.pi-base.org/spaces/S000022/properties/P000011 goes from T5 to regular in 4 steps
• https://topology.pi-base.org/spaces/S000039/properties/P000011 goes from LOTS to regular in 7 steps, but could really be 5