Topic: Topological vector spaces
Sebastien Gouezel (May 24 2019 at 11:53):
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 (May 24 2019 at 13:00):
@Sebastien Gouezel We didn't use anything about topological modules.
Sebastien Gouezel (May 24 2019 at 13:01):
OK, thanks. I will have to do it, then :(
Kevin Buzzard (May 24 2019 at 13:30):
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.
Last updated: May 12 2021 at 07:17 UTC