Naming of SecondCountableTopology

Stream: mathlib4

[Josha Dekker]

I'm trying to automatically generate names for topological spaces to facilitate in tracking the progress of Mathlib on the results in pi-base, but I'm a bit confused about why SecondCountableTopology and FirstCountableTopology are not named SecondCountableSpace and FirstCountableSpace instead, what logic am I missing, so that I can adapt my code for this?

[Yury G. Kudryashov]

Usually, the answer is "for historical reasons" a.k.a. someone chose these names several years ago. Also, there are no other topology- related terms in the names.

[Yury G. Kudryashov]

Also, some names are in the TopologicalSpace namespace, others aren't.

[Josha Dekker]

Okay, thank you! Let me drop a poll here to see if people want to see the name changed to SecondCountableSpace? I’ll make a PR if there is sufficiently much support

[Josha Dekker]

/poll Change the name to SecondCountableTopology?
Yes
No

[Jireh Loreaux]

Personally, I would prefer dropping the Space suffix on these. E.g., SecondCountable, Metrizable (that one could even come out of the TopologicalSpace namespace), etc.

[Josha Dekker]

/poll Drop the -Topology/Space suffix on the above mentioned topological properties
Yes
No

[Sébastien Gouëzel]

I'd rather add a prefix Is for uniformity with the rest of mathlib, but keep Spaceto distinguish properties of the space from properties of sets. For instance, IsCompact vs. IsCompactSpace.

[Jireh Loreaux]

I think this shows that we really need to decide under what conditions the Is prefix applies.

[Kevin Buzzard]

What are the arguments against "Is iff a Prop"?

[Adam Topaz]

That doesn’t make sense in category theory

[Richard Osborn]

I believe most of the counter examples are in the category theory files (Faithful, IsLimit, IsLeftAdjoint). I think the argument is that Full being a Type and Faithful being a Prop is largely an implementation detail, so it would be weird to have Full and IsFaithful.

[Adam Topaz]

Well, in my opinion the reason is that Prop genuinely should mean something different when doing category theory. Since talking about, e.g. equality of objects is incompatible with the language of category theory, if you want to state some property involving objects, you need to include data which (usually) pins down some objects up to isomorphism. IsLimit and IsLeftAdjoint are good examples of this. When we start doing higher category theory in earnest, the situation will only get worse

[Adam Topaz]

Arguably Full could be made a prop since it’s a property about morphisms, not objects

[Antoine Chambert-Loir]

Why can't docs#CategoryTheory.Limits.IsLimit be a Prop?

[Antoine Chambert-Loir]

I rephrase: presently, docs#CategoryTheory.Limits.IsLimit contains the lifts implied by the universal property of a limit, so it contains data, but why couldn't there be a Prop-version that merely asserts the universal property?

[Markus Himmel]

That would be slightly strange, as it would mean that you care about the specific maps going out of the cone point (these are part of the cone), but not about those going into the cone point (which are part of IsLimit). Of course, we do have the case where you care about neither maps, nor the cone point: docs#CategoryTheory.Limits.HasLimit

[Adam Topaz]

Antoine, you’re right, IsLimit could indeed be phrased as a prop with this philosophy. But there are situations where you may want explicit control over the lift morphism, and for those having it as part of the data is convenient. If no control is needed then HasLimit is the way to go as Markus mentioned. (I admit, this issue is orthogonal to the situation of the comment I made above, so IsLeftAdjoint is a better example in that case.)