Orbifolds in Lean
This project started out with the goal to formalise some of the basic theory of orbifolds in Lean 4, but over time evolved into a sort of general staging ground for formalisation of various kinds of generalised differential geometry. Currently, the repository consists mostly of material on diffeological spaces and smooth spaces, but there are also formalisations of e.g. Frölicher spaces, cohesive topoi and various useful sites in the works. Current long-term goals include formalising the Cahiers topos with its differential cohesion, the quasitopos of concrete sheaves on any local site, and/or De-Rham cohomology of smooth spaces. Orbifolds will have to wait until there is enough material on higher category theory in mathlib to treat them properly; my hope is that the ongoing infinity-cosmos project will lay the groundwork for that.
Overview
The material currently featured in this repository includes:
- Diffeology:
- basics & lattice structure on diffeologies
- induced and coinduced diffeologies, inductions and subductions
- basic constructions (i.e. subspaces, quotient spaces, products, mapping spaces)
- D-topology, continuous diffeology
- internal tangent spaces
- diffeological manifolds & orbifolds
- reflexive diffeological spaces (i.e. Frölicher spaces)
- diffeological monoids, groups, rings and modules / vector spaces
- pointwise algebraic structure of mapping spaces
- category of diffeological spaces, limits & colimits in that category, cartesian-closedness and adjunctions to topological spaces & sets
- Smooth spaces:
- sites CartSp & EuclOp
- category of smooth spaces, adjunction to diffeological spaces
- Cohesion:
Other files that started out in this repository have also already made their way into mathlib, for example delta-generated spaces and global sections of sheaves.
References
The formalisation of diffeology here is based mostly on Patrick Iglesias-Zemmour's excellent book "Diffeology" and mathlib's formalisation of topology, since there are a lot of parallels to topology in the basic theory. Other files are mostly derived from the nlab or various shorter papers; I have made an effort to include proper attribution in the module docstring of each file.