Topological vector spaces

Stream: maths

[Sebastien Gouezel]

I will need to refactor things a little bit for manifolds, as the tangent space has a canonical topology but not a canonical norm (and I don't want to impose a norm, otherwise when I change the norm the space of bounded linear maps will change, i.e., the definition of the derivative would depend on the choice of norm). This means that the good setting for the tangent space is a topological vector space, of which normed space will be a special case.

This is not hard to introduce, but as some of you have played a lot with topological rings in the perfectoid project I don't want to duplicate what has already been done. Are there already topological modules over a topological ring, either in mathlib or in the wild?

[Johan Commelin]

@Sebastien Gouezel We didn't use anything about topological modules.

[Sebastien Gouezel]

OK, thanks. I will have to do it, then :(

[Kevin Buzzard]

Yes, sorry about that! In the book by Bosch Guentzer Remmert on foundations of rigid geometry they spend their entire life thinking about topological modules, but we never got onto sheaves of modules, we only did sheaves of rings, so we needed no topological modules at all.