Weak dual with discrete topology

Stream: Is there code for X?

[Adam Topaz]

Do we have a version of docs#weak_dual where both the field and vector space are discrete?

[Kalle Kytölä]

I'm not sure I understand what you are asking...

docs#weak_dual currently assumes [comm_semiring 𝕜] [topological_space 𝕜] [has_continuous_add 𝕜] [has_continuous_const_smul 𝕜 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] . I don't think these type classes rule out discrete topology on the field and the vector space, right? There might not be any API about the discrete case specifically, though, and I'm not sure the instances of these type classes are there for discrete fields and vector spaces. :thinking:

[Adam Topaz]

If $k$ is a field (with the discrete topology) and $V$ is a vector space over $k$, again with the discrete topology, I would like the dual $Hom_k(V,k)$ endowed with the topology induced by the inclusion of $Hom_k(V,k)$ into $k^V$ with the product topology.

[Adam Topaz]

I'm fairly sure this should (topologically) agree with the weak dual where both $V$ and $k$ are discrete.

[Adam Topaz]

To un-xy the question, I'm interested in this because there is a well behaved duality between subspaces of V and closed subspaces of the dual, with this given topology.

[Adam Topaz]

In lean there is an issue with just using weak_dual because I would have to individually give k and V the discrete topology (via a local instance or alias or whatever). But I think this is a sufficiently common case that it might deserve its own name without the additional typeclass gymnastics.

[Kalle Kytölä]

Adam Topaz said:

I'm fairly sure this should (topologically) agree with the weak dual where both $V$ and $k$ are discrete.

So I think the weak_dual should be a type in this case which has a topology --- if the field and the vector space have instances of the discrete topology, and if the (trivial) has_continuous_add 𝕜etc. have also been instantiated. (And I think it should indeed be almost by definition that the topology you want agrees with the topology on weak_dual, as you say.)

But I see you'd like to do that without the instances (typeclass gymnastics, in technical terms :gymnastics:)... I do not have a lot of experience to comment on that design decision.

[Kalle Kytölä]

Do we have discrete topology instances on (common) discrete fields, and if not, would it be a terrible idea?

I can believe that automatically equipping vector spaces over discrete fields with discrete topology can be more problematic. But at some point one would anyway have to tell Lean (either explicitly with type class instances or implicitly by using a synonym of weak_dual meant for this purpose) that the intended topology on the vector space is discrete, right?

Again, these are just naive questions --- I don't know which ways would work well for your purpose.