Charted spaces

A smooth manifold is a topological space M locally modelled on a euclidean space (or a euclidean half-space for manifolds with boundaries, or an infinite dimensional vector space for more general notions of manifolds), i.e., the manifold is covered by open subsets on which there are local homeomorphisms (the charts) going to a model space H, and the changes of charts should be smooth maps.

In this file, we introduce a general framework describing these notions, where the model space is an arbitrary topological space. We avoid the word manifold, which should be reserved for the situation where the model space is a (subset of a) vector space, and use the terminology charted space instead.

If the changes of charts satisfy some additional property (for instance if they are smooth), then M inherits additional structure (it makes sense to talk about smooth manifolds). There are therefore two different ingredients in a charted space:

• the set of charts, which is data
• the fact that changes of charts belong to some group (in fact groupoid), which is additional Prop.

We separate these two parts in the definition: the charted space structure is just the set of charts, and then the different smoothness requirements (smooth manifold, orientable manifold, contact manifold, and so on) are additional properties of these charts. These properties are formalized through the notion of structure groupoid, i.e., a set of local homeomorphisms stable under composition and inverse, to which the change of coordinates should belong.

Main definitions

• structure_groupoid H : a subset of local homeomorphisms of H stable under composition, inverse and restriction (ex: local diffeos).
• continuous_groupoid H : the groupoid of all local homeomorphisms of H
• charted_space H M : charted space structure on M modelled on H, given by an atlas of local homeomorphisms from M to H whose sources cover M. This is a type class.
• has_groupoid M G : when G is a structure groupoid on H and M is a charted space modelled on H, require that all coordinate changes belong to G. This is a type class.
• atlas H M : when M is a charted space modelled on H, the atlas of this charted space structure, i.e., the set of charts.
• G.maximal_atlas M : when M is a charted space modelled on H and admitting G as a structure groupoid, one can consider all the local homeomorphisms from M to H such that changing coordinate from any chart to them belongs to G. This is a larger atlas, called the maximal atlas (for the groupoid G).
• structomorph G M M' : the type of diffeomorphisms between the charted spaces M and M' for the groupoid G. We avoid the word diffeomorphism, keeping it for the smooth category.

As a basic example, we give the instance instance charted_space_model_space (H : Type*) [topological_space H] : charted_space H H saying that a topological space is a charted space over itself, with the identity as unique chart. This charted space structure is compatible with any groupoid.

Additional useful definitions:

• pregroupoid H : a subset of local mas of H stable under composition and restriction, but not inverse (ex: smooth maps)
• groupoid_of_pregroupoid : construct a groupoid from a pregroupoid, by requiring that a map and its inverse both belong to the pregroupoid (ex: construct diffeos from smooth maps)
• chart_at H x is a preferred chart at x : M when M has a charted space structure modelled on H.
• G.compatible he he' states that, for any two charts e and e' in the atlas, the composition of e.symm and e' belongs to the groupoid G when M admits G as a structure groupoid.
• G.compatible_of_mem_maximal_atlas he he' states that, for any two charts e and e' in the maximal atlas associated to the groupoid G, the composition of e.symm and e' belongs to the G if M admits G as a structure groupoid.
• charted_space_core.to_charted_space: consider a space without a topology, but endowed with a set of charts (which are local equivs) for which the change of coordinates are local homeos. Then one can construct a topology on the space for which the charts become local homeos, defining a genuine charted space structure.

Implementation notes

The atlas in a charted space is not a maximal atlas in general: the notion of maximality depends on the groupoid one considers, and changing groupoids changes the maximal atlas. With the current formalization, it makes sense first to choose the atlas, and then to ask whether this precise atlas defines a smooth manifold, an orientable manifold, and so on. A consequence is that structomorphisms between M and M' do not induce a bijection between the atlases of M and M': the definition is only that, read in charts, the structomorphism locally belongs to the groupoid under consideration. (This is equivalent to inducing a bijection between elements of the maximal atlas). A consequence is that the invariance under structomorphisms of properties defined in terms of the atlas is not obvious in general, and could require some work in theory (amounting to the fact that these properties only depend on the maximal atlas, for instance). In practice, this does not create any real difficulty.

We use the letter H for the model space thinking of the case of manifolds with boundary, where the model space is a half space.

Manifolds are sometimes defined as topological spaces with an atlas of local diffeomorphisms, and sometimes as spaces with an atlas from which a topology is deduced. We use the former approach: otherwise, there would be an instance from manifolds to topological spaces, which means that any instance search for topological spaces would try to find manifold structures involving a yet unknown model space, leading to problems. However, we also introduce the latter approach, through a structure charted_space_core making it possible to construct a topology out of a set of local equivs with compatibility conditions (but we do not register it as an instance).

In the definition of a charted space, the model space is written as an explicit parameter as there can be several model spaces for a given topological space. For instance, a complex manifold (modelled over ℂ^n) will also be seen sometimes as a real manifold modelled over ℝ^(2n).

Notations

In the locale manifold, we denote the composition of local homeomorphisms with ≫ₕ, and the composition of local equivs with ≫.

Structure groupoids

One could add to the definition of a structure groupoid the fact that the restriction of an element of the groupoid to any open set still belongs to the groupoid. (This is in Kobayashi-Nomizu.) I am not sure I want this, for instance on H × E where E is a vector space, and the groupoid is made of functions respecting the fibers and linear in the fibers (so that a charted space over this groupoid is naturally a vector bundle) I prefer that the members of the groupoid are always defined on sets of the form s × E. There is a typeclass closed_under_restriction for groupoids which have the restriction property.

The only nontrivial requirement is locality: if a local homeomorphism belongs to the groupoid around each point in its domain of definition, then it belongs to the groupoid. Without this requirement, the composition of structomorphisms does not have to be a structomorphism. Note that this implies that a local homeomorphism with empty source belongs to any structure groupoid, as it trivially satisfies this condition.

There is also a technical point, related to the fact that a local homeomorphism is by definition a global map which is a homeomorphism when restricted to its source subset (and its values outside of the source are not relevant). Therefore, we also require that being a member of the groupoid only depends on the values on the source.

We use primes in the structure names as we will reformulate them below (without primes) using a has_mem instance, writing e ∈ G instead of e ∈ G.members.

Charted spaces

Constructing a topology from an atlas

Charted space with a given structure groupoid

Structomorphisms