Refine category of RealSet

[mkoeppe]

we should put it in a suitable subcategory of TopologicalSpaces.

[gh-mjungmath]

Possibly a good idea to consider: ​https://trac.sagemath.org/ticket/30832#comment:6.

[mkoeppe]

New commits:

​4b09685

RealSet: Put it in a suitable subcategory of TopologicalSpaces()

[gh-mjungmath]

I personally don't like adding RealSet to TopologicalSpaces. Imo the difference between RealSet and OpenInterval should be exactly that: seeing them as sets or manifolds (i.e. top. spaces).

Then a forgetful functor would also make more sense.

[mkoeppe]

A RealSet instance is a union of finitely many (possibly degenerate) intervals, so it is always a topological subspace of the real line, but not always a manifold. It would belong to the category of manifolds with corners of mixed dimension, but I think it's a long way until we have implemented that.

[tscrim]

I think this is good. As Matthias said, they are naturally topological spaces from the subspace topology. The only question I have is why is ambient() a @staticmethod? I feel like it should be a normal method because the ambient space is associated with the instance rather than as a constructor function (cf. open_closed).

@gh-mjungmath I don't understand what you mean by forgetful functor. These are parents, and have nothing to do with functors. For example, there is a forgetful functor from Rings -> Sets, and applying that functor to ZZ still obtains ZZ. It still has all of the behavior of an object in Sets, but there is no reason to actually forget about the ring structure.

[mkoeppe]

Replying to tscrim:

The only question I have is why is ambient() a @staticmethod? I feel like it should be a normal method

OK, I'll make this change.

[git]

Branch pushed to git repo; I updated commit sha1. New commits:

​46eed0e

RealSet.ambient: Change to a normal method

[mkoeppe]

Replying to tscrim:

I don't understand what you mean by forgetful functor. These are parents, and have nothing to do with functors. For example, there is a forgetful functor from Rings -> Sets, and applying that functor to ZZ still obtains ZZ. It still has all of the behavior of an object in Sets, but there is no reason to actually forget about the ring structure.

I think the idea would be that after applying the functor to the parent, asking for example for the homset would give a different answer.

[tscrim]

Replying to mkoeppe:

Replying to tscrim:

I don't understand what you mean by forgetful functor. These are parents, and have nothing to do with functors. For example, there is a forgetful functor from Rings -> Sets, and applying that functor to ZZ still obtains ZZ. It still has all of the behavior of an object in Sets, but there is no reason to actually forget about the ring structure.

I think the idea would be that after applying the functor to the parent, asking for example for the homset would give a different answer.

IMO, it is better to pass that category information to the homset construction (which you can do) if you want to consider morphisms in a weaker category. This way you have less proliferation of "equal" parents and dealing with elements that maybe shouldn't have the additional structure. In this example, should you be able to add two integers that are in the ZZ as a Sets object? Plus, the category you want for the morphisms is a property of the morphism, not the parent.

[tscrim]

Thanks for the change.

[mkoeppe]

Thanks!

[gh-mjungmath]

Replying to tscrim:

I think this is good. As Matthias said, they are naturally topological spaces from the subspace topology.

Just because it comes with a natural topology doesn't mean it is the topology the user wants.

If you argument like that, every set must be seen in the category of topological spaces, because every set is endowed with a topology.

@gh-mjungmath I don't understand what you mean by forgetful functor. These are parents, and have nothing to do with functors. For example, there is a forgetful functor from Rings -> Sets, and applying that functor to ZZ still obtains ZZ. It still has all of the behavior of an object in Sets, but there is no reason to actually forget about the ring structure.

IMO, it is better to pass that category information to the homset construction (which you can do) if you want to consider morphisms in a weaker category. This way you have less proliferation of "equal" parents and dealing with elements that maybe shouldn't have the additional structure. In this example, should you be able to add two integers that are in the ZZ as a Sets object? Plus, the category you want for the morphisms is a property of the morphism, not the parent.

Then I don't understand why we even have a forgetful functor if it technically just represents the identity functor...

[gh-mjungmath]

But I agree, for structures like rings, groups etc. this approach makes total sense. Though, I still don't understand why ForgetfulFunctor was introduced in the first place.

But for manifolds, things are slightly different. It would be good to have a functor that forgets about the topological structure, for example to impose another one. Like I said, I don't like the idea of enforcing a preferred topology on a set if we see it just as set (what we clearly do with RealSet as the name indicates).

[mkoeppe]

Replying to gh-mjungmath:

Replying to tscrim:

I think this is good. As Matthias said, they are naturally topological spaces from the subspace topology.

Just because it comes with a natural topology doesn't mean it is the topology the user wants.

RealSet provides constructors for certain subsets of the reals. The "set" of real numbers comes with a distinguished topology, which is reflected by the names of the RealSet constructors for intervals such as open, closed.

In #31881 (RealSet: Extend constructors so that they can build manifold objects) I plan to add a category keyword argument. Then also the rather specialized use case that a subset of the real numbers is to be treated merely as a set can be achieved by passing category=Sets() to the constructors.

[gh-mjungmath]

Replying to mkoeppe:

RealSet provides constructors for certain subsets of the reals. The "set" of real numbers comes with a distinguished topology, which is reflected by the names of the RealSet constructors for intervals such as open, closed.

Good point!

In #31881 (RealSet: Extend constructors so that they can build manifold objects) I plan to add a category keyword argument. Then also the rather specialized use case that a subset of the real numbers is to be treated merely as a set can be achieved by passing category=Sets() to the constructors.

+1

[tscrim]

Just because it acts as the identity on parents, doesn't mean it is the identity functor. Be very careful with confusing abstract and concrete mathematics. If I said ZZ the set is the same as ZZ the ring, would you agree or disagree? Or would you be like Bill Clinton and state "That depends on what the definition of 'is' is."? The forgetful functor does carry some information, and that is the category you obtain at the end. It could also be used as a base class when you do have some more canonical implementations, but currently it doesn't seem to be used.

By being in the category of topological spaces, you are stating there is a preferred topology. This is akin to the WithBasis category saying there is a distinguished basis. This is why TopologicalSpaces is constructed as a functor construction category.

For the manifold code, while it is dynamic, each manifold is not meant to be treated as something that can change. So if you go from differentiable to topological, you are actually constructing a different object because the maximal atlas is different. We just may not have provided enough information yet to see that difference.

[git]

Branch pushed to git repo; I updated commit sha1 and set ticket back to needs_review. New commits:

​5b8ceca	InternalRealInterval, RealSet: Add _latex_ methods
​69ca854	RealSet._repr_: Use unicode cup sign instead of +
​dbdfc06	InternalRealInterval, RealSet: Remove extra whitespace in latex, add documentation
​7f56338	PiecewiseFunction: Adjust doctests for changed RealSet repr
​8abdc8b	src/sage/functions/piecewise.py: Add coding header
​5b0f85d	Merge #31880

[mkoeppe]

Merged to resolve merge conflict