mathlib
mathlib copied to clipboard
leanprover-community
feat(geometry/manifold/*): transferring geometrical structures through homeomorphisms and open embeddings
This is just the part of the code that was before part of the PR on GLn and that was removed because the strategy changed, but that can still be useful in other situations.
It mainly proves that if X is a topological space and a monoid, M is a topological monoid, and f: X \to M is both an open embedding and a homomorphism, then multiplication in X is continuous.
This PR also contains some definitions to transfer smooth structures through homomorphisms.
I am not really sure that these lemmas are generally useful. If they do join the library, I think it should be in more generality: a general open embedding (rather than a homeomorphism) for the manifold constructions, a general function satisfying inducing (rather than an open embedding) for the topology/algebra constructions. I also think that, if both kept, they should be in separate PRs.
