Equality of conatural numbers

[fredrik-bakke]

No description provided.

[fredrik-bakke]

I've started formalizing the alternative definition of the conaturals as the type of decreasing binary sequences alongside this, and I am wondering what name to use for it, what label to give the type, and in which namespace it should be placed. In Martín's formalizations, he calls it the "generic convergent sequence" and gives it the label ℕ∞ but that is already taken by our coinductive definition. I'm tempted to place the formalization of this alternative definition in set-theory, but am not sure if that is a good idea given that the conaturals are placed in elementary-number-theory. I suppose I prefer "decreasing binary sequences" over "generic convergent sequence", as the former leaves room for the equivalent "increasing binary sequences". Opinions or any input is appreciated!

[EgbertRijke]

We could consider reserving the infinity notation for things that are defined by adding a point at infinity, such as the one-point compactification. In that case the name for the conatural numbers would have to change to something like conat or conatural-number, which would make sense because as it is defined it is the dual to the natural numbers. I like decreasing-boolean-sequence-ℕ for the type of decreasing boolean sequence. We already have some sequence-ℕ definitions for sequences indexed by the natural numbers (as opposed to sequences indexed by the integers), so boolean-sequence-ℕ would be a sequence of booleans, and decreasing-boolean-sequence-ℕ would be a decreasing such sequence.

[EgbertRijke]

One more thought: If we would define one-point compactifications by specification, then we could prove that the conatural numbers is a one-point compactification of the natural numbers, justifying that the name can stay as it is.

[fredrik-bakke]

What do you mean by specification?

[EgbertRijke]

A specification of X is saying what it means to be an X, instead of defining an instance of an X.

The specification of one point compactification is its universal property, whereas "the" one point compactification would be an operation returning one point compactifications

[fredrik-bakke]

Right right. Thanks for clarifying!

[EgbertRijke]

All that was to say that I'm happy to keep the name ℕ∞ for the conatural numbers. So no need to change anything.

[fredrik-bakke]

This has got me thinking about what the universal property should be... Perhaps something like the following:

• An extension f : X ↪ X∞ equipped with a point ∞ ∈ X∞ is a one-point compactification of X if the double complement of the image of f is full, and ∞ ∈ X∞ satisfies some pointed compactness condition.

[fredrik-bakke]

In TypeTopology, Martín defines a limit point to be an element whose isolatedness implies WLPO. I would have hoped for something that is "model agnostic" to the natural numbers, so I think the following should work:

• An extension f : X ↪ X∞ equipped with a point ∞ ∈ X∞ is a one-point compactification of X if X∞ is compact, and the isolatedness of ∞ ∈ X∞ implies that X is compact.

[fredrik-bakke]

Aaand you need something to ensure uniqueness of ∞ of course. Perhaps "if x is not equal to ∞ then it is in the image of f."

[EgbertRijke]

The n-lab page has a more traditional approach to the universal property of one-point compactification:

https://ncatlab.org/nlab/show/one-point+compactification

[fredrik-bakke]

Aha, so do you have certain definitions in mind for the notions of "locally compact", "Hausdorff" and "closed subspace"?
I suppose closed subspace should be double negation stable, and Hausdorff should mean that the diagonal X -> X x X is double negation stable? I'm less sure about local compactness.

[fredrik-bakke]

I suppose this kind of stuff really ought to be in a type-topology namespace...

[fredrik-bakke]

Ah, so a Hausdorff type is really just a type whose equality is double negation stable, huh?

[EgbertRijke]

I suppose this kind of stuff really ought to be in a type-topology namespace...

Or in a condensed-mathematics namespace.

I don't have any concrete proposals for definitions of Hausdorff types or locally compact types right now, but it would be interesting to explore.

[fredrik-bakke]

If I dare ask, how is this condensed mathematics?

[fredrik-bakke]

To my very limited understanding reading up this afternoon, in the "traditional" interpretation of types as topological spaces, "closed" means double negation stable. Although, of course, as you and I both know, double negation is but one mode of logic.

[EgbertRijke]

If I dare ask, how is this condensed mathematics?

If I recall correctly, this sort of thing comes up in Reid Barton's interpretation of condensed mathematics.

[EgbertRijke]

To my very limited understanding reading up this afternoon, in the "traditional" interpretation of types as topological spaces, "closed" means double negation stable. Although, of course, as you and I both know, double negation is but one mode of logic.

Original, I meant "traditional" as in the way you'd learn about it in a standard textbook on topology. When people say traditional mathematics, it usually refers to mathematics in the standard curriculum and not really this kind of fancy stuff:)