# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeMay 6th 2017
• (edited May 6th 2017)

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.

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeJun 11th 2017

I have expanded the Examples-section at differentiable manifold: here.

• CommentRowNumber3.
• CommentAuthorJames Francese
• CommentTimeMar 18th 2019

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é”.

• CommentRowNumber4.
• CommentAuthorJames Francese
• CommentTimeMar 18th 2019

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é”.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeMar 18th 2019
• (edited Mar 18th 2019)

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 $\Im,$ (the “infinitesimal shape modality”) which allows one to say “formally etale morphism”.

Then for $V$ a group object, a good definition of “manifold locally modeled on $V$” – or “$V$-manifold”, for short, is: $X$ is a $V$-manifold if it admits a “$V$-atlas”, namely a correspondence of morphisms

$\array{ && U \\ & \swarrow && \searrow \\ V && && X }$

such that

1. both morphisms are formally étale

2. the morphism $U \to X$ 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.

• CommentRowNumber6.
• CommentAuthorJames Francese
• CommentTimeMar 20th 2019

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 $V$. 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.

• CommentRowNumber7.
• CommentAuthorJames Francese
• CommentTimeSep 13th 2019

Added some comments on manifolds regarded as topological spaces with particular structure sheaf, and added detail to the basic example of $\mathbf{R}P^n$ as a locally ringed space. Fixed several typos.

1. typos

Anonymous