I have a variation of the subspace problem related to having `Pointed`

be a requirement on `Topological`

. I know this has come up before. But it seems fairly solvable in mathcomp 2. I have forgotten if there's a good reason to require Pointed. But I'm definitely finding good reason to separate them. I volunteer to go through and figure out which lemmas do/don't need it.

In my work today, I wanted to take a `A : set X`

and build a `Type`

which represents the subspace. We have `subspace A`

, but the intention of the this topology was to gain the "local" topological behaviors of the subspace while preserving all the algebraic ones (which has certainly proven useful in the measure theory world). But global properties often fail, and many definitions don't work at all because `forall x : subspace A`

just means `forall x : X`

. So when I only care about topological properties, I'd rather just use `weak_topologicalType (projT1 _ A)`

. (I can go into more detail on my use case if it's helpful)

Only problem is, weak_topologicalType needs a `Pointed`

, which causes a bit of havoc. So `A`

has to be nonempty, which causes one set of issues. But even if we know A is non-empty one must construct the PointedType directly. It's doable (I do it in cantor.v), but verbose and terrible. It's also dangerous because it's badly non-canonical, and exposing these types in lemma statements risks lots of weird incompatibilities with other people building different instances.

Hi Zachary, the only reason for making them pointed is because rings are nontrivial... If we finally make the separation in mathcomp we can finally propagate

Why is there a dependency? If we separate them on our side, we would build an instance of the basic Topology. But rings are pointed, so HB should infer the instance of PointedTopology.

Is there a non-forgertful inheritance I'm missing?

I'll explain on Tuesday when I'm back from vacations

Last updated: Jun 25 2024 at 18:02 UTC