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 as concrete subcanonical sites, the former being a cohesive, dense subsite of the latter
  • category of smooth spaces, adjunction to diffeological spaces
• Cohesion:
  • local sites, locally connected sites and cohesive sites; also concrete sites
  • general cohesion

Material that has been upstreamed from here to mathlib so far includes delta-generated spaces, global sections of sheaves and adjoint triples. More PRs are on the way / currently waiting for review.

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 and / various papers; I have made an effort to include proper attribution in the module docstring of each file.