This project aims to formalise some of the basic theory of orbifolds and other generalised smooth spaces in lean. A first goal is to develop the theory of diffeological spaces to a point where orbifolds can be defined and reasoned about as special diffeological spaces; after that the focus will probably shift more towards proving theorems about orbifolds, or maybe even building up a theory of Lie groupoids to the point where orbifolds can be defined in terms of them too.
So far this is mostly following Patrick Iglesias-Zemmour's book "Diffeology" - I will list more references here when I use them. The API is also in large parts adapted from mathlib's topology API, since there is a lot of similarities at least in the basic theory.
- Diffeological Spaces:
- Constructions:
- Diffeology generated by a family of functions
- Arbitrary joins and meets of diffeologies
- Pushforwards and pullbacks of diffeologies
- Subspace diffeologies
- Quotient diffeologies
- Binary product diffeologies
- Product diffeologies
- Binary coproduct diffeologies
- Coproduct diffeologies
- Mapping spaces
- D-topology
- Continuous diffeology
- Maps:
- Smooth maps
- Inductions & subductions
- Diffeomorphisms
- Types of diffeological spaces:
- Diffeological groups
- Diffeological vector spaces
- Diffeological manifolds
- Orbifolds as diffeological spaces
- Other spaces as diffeological spaces:
- Finite-dimensional vector spaces
- Normed or Banach spaces
- Manifolds, maybe ones with boundary & corners too
- Abstract nonsense:
- Category of diffeological spaces
- Completeness and Cocompleteness of that category
- Cartesian-closedness of that category
- Forgetful functor and related adjunctions
- D-topology functor and adjunction
- Category of smooth sets as sheaf topos on
CartSp - Diffeological spaces as a reflective subcategory of that
- Alternative characterisations via
EuclOpetc.
- Constructions: