Zachary Stone (Dec 29 2023 at 02:26): Zachary Stone (Dec 29 2023 at 02:26):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.
Cyril Cohen (Dec 29 2023 at 18:36):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
Zachary Stone (Dec 29 2023 at 18:42):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?
Cyril Cohen (Dec 30 2023 at 21:27):I'll explain on Tuesday when I'm back from vacations
Last updated: Oct 13 2024 at 01:02 UTC