Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have re-written the content at differentiable manifold, trying to make it look a little nicer. Also gave topological manifold some minimum of content.
I have expanded the Examples-section at differentiable manifold: here.
I’m adding material which defines and gives examples for manifolds as etalé spaces in the sense that they can be locally modeled on subsets of Euclidean space with a structure sheaf of appropriate functions. This may answer Zoran’s concern in etalé map.
It seems this definition is also fairly easy to formalize in a proof assistant once you get something else to do the hard work of capturing “etalé”.
I’m adding material which defines and gives examples for manifolds as etalé spaces in the sense that they can be locally modeled on subsets of Euclidean space with a structure sheaf of appropriate functions. This may answer Zoran’s concern in etalé map.
It seems this definition is also fairly easy to formalize in a proof assistant once you get something else to do the hard work of capturing “etalé”.
Thanks for the addition.
Regarding formalizations of manifolds via one of étale maps:
Around here we have been talking about a formalization of differential geometry where one assumes a modal operator (the “infinitesimal shape modality”) which allows one to say “formally etale morphism”.
Then for a group object, a good definition of “manifold locally modeled on ” – or “-manifold”, for short, is: is a -manifold if it admits a “-atlas”, namely a correspondence of morphisms
such that
both morphisms are formally étale
the morphism is in addition a covering (an epimorphism in the topos/type-theoretic sense).
The page geometry of physics – manifolds and orbifolds is meant to eventually talk about this in detail, though at the moment it contains just some minimum (here).
But Felix Wellen has been busy formalizing this definition in modal type theory and exploring differential geometry using it. His stuff is collected at thesis Wellen (schreiber). If you’d like to see more, that would be the page to explore. Or of course we could talk about it.
Of course, this may or may not be relevant for what you are after. Just mentioning it for completeness.
I think this is very relevant indeed, thank you Urs. A nice achievement of this shape modality is that it captures the intuition that a manifold should be a kind of “homogeneous space”; instead of the transition maps being taken from a fixed Lie group, they are taken from . So once the homotopy pullback formulation of étale morphism is formalized, one is just a few steps away from having a synthetic formalization of ’smooth manifold’. And thanks for linking to Wellen, I’m liking his HoTT-inspired use of Agda. And I see he obtains G-structures in a very nice way at the end of the talk slides there; I will have to read this thesis and would love to discuss.
1 to 9 of 9