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 partial homeomorphisms stable under composition and inverse, to which the change of coordinates should belong.
Main definitions #
StructureGroupoid H
: a subset of partial homeomorphisms ofH
stable under composition, inverse and restriction (ex: partial diffeomorphisms).continuousGroupoid H
: the groupoid of all partial homeomorphisms ofH
.ChartedSpace H M
: charted space structure onM
modelled onH
, given by an atlas of partial homeomorphisms fromM
toH
whose sources coverM
. This is a type class.HasGroupoid M G
: whenG
is a structure groupoid onH
andM
is a charted space modelled onH
, require that all coordinate changes belong toG
. This is a type class.atlas H M
: whenM
is a charted space modelled onH
, the atlas of this charted space structure, i.e., the set of charts.G.maximalAtlas M
: whenM
is a charted space modelled onH
and admittingG
as a structure groupoid, one can consider all the partial homeomorphisms fromM
toH
such that changing coordinate from any chart to them belongs toG
. This is a larger atlas, called the maximal atlas (for the groupoidG
).Structomorph G M M'
: the type of diffeomorphisms between the charted spacesM
andM'
for the groupoidG
. We avoid the word diffeomorphism, keeping it for the smooth category.
As a basic example, we give the instance
instance chartedSpaceSelf (H : Type*) [TopologicalSpace H] : ChartedSpace 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 partial maps ofH
stable under composition and restriction, but not inverse (ex: smooth maps)Pregroupoid.groupoid
: 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)chartAt H x
is a preferred chart atx : M
whenM
has a charted space structure modelled onH
.G.compatible he he'
states that, for any two chartse
ande'
in the atlas, the composition ofe.symm
ande'
belongs to the groupoidG
whenM
admitsG
as a structure groupoid.G.compatible_of_mem_maximalAtlas he he'
states that, for any two chartse
ande'
in the maximal atlas associated to the groupoidG
, the composition ofe.symm
ande'
belongs to theG
ifM
admitsG
as a structure groupoid.ChartedSpaceCore.toChartedSpace
: consider a space without a topology, but endowed with a set of charts (which are partial equivs) for which the change of coordinates are partial homeos. Then one can construct a topology on the space for which the charts become partial 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 ChartedSpaceCore
making it possible to construct a topology out of a set of
partial 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 partial homeomorphisms with ≫ₕ
, and the
composition of partial equivs with ≫
.
Equations
- Manifold.«term_≫ₕ_» = Lean.ParserDescr.trailingNode `Manifold.term_≫ₕ_ 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ₕ ") (Lean.ParserDescr.cat `term 100))
Instances For
Equations
- Manifold.«term_≫_» = Lean.ParserDescr.trailingNode `Manifold.term_≫_ 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ ") (Lean.ParserDescr.cat `term 100))
Instances For
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 ClosedUnderRestriction
for groupoids
which have the restriction property.
The only nontrivial requirement is locality: if a partial 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 partial 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 partial 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
Membership
instance, writing e ∈ G
instead of e ∈ G.members
.
A structure groupoid is a set of partial homeomorphisms of a topological space stable under composition and inverse. They appear in the definition of the smoothness class of a manifold.
- members : Set (PartialHomeomorph H H)
Members of the structure groupoid are partial homeomorphisms.
- trans' : ∀ (e e' : PartialHomeomorph H H), e ∈ self.members → e' ∈ self.members → e.trans e' ∈ self.members
Structure groupoids are stable under composition.
- symm' : ∀ e ∈ self.members, e.symm ∈ self.members
Structure groupoids are stable under inverse.
- id_mem' : PartialHomeomorph.refl H ∈ self.members
The identity morphism lies in the structure groupoid.
- locality' : ∀ (e : PartialHomeomorph H H), (∀ x ∈ e.source, ∃ (s : Set H), IsOpen s ∧ x ∈ s ∧ e.restr s ∈ self.members) → e ∈ self.members
Let
e
be a partial homeomorphism. If for everyx ∈ e.source
, the restriction of e to some open set aroundx
lies in the groupoid, thene
lies in the groupoid. - mem_of_eqOnSource' : ∀ (e e' : PartialHomeomorph H H), e ∈ self.members → e' ≈ e → e' ∈ self.members
Membership in a structure groupoid respects the equivalence of partial homeomorphisms.
Instances For
Structure groupoids are stable under composition.
Structure groupoids are stable under inverse.
The identity morphism lies in the structure groupoid.
Let e
be a partial homeomorphism. If for every x ∈ e.source
, the restriction of e to some
open set around x
lies in the groupoid, then e
lies in the groupoid.
Membership in a structure groupoid respects the equivalence of partial homeomorphisms.
Equations
- instMembershipPartialHomeomorphStructureGroupoid = { mem := fun (G : StructureGroupoid H) (e : PartialHomeomorph H H) => e ∈ G.members }
Equations
- instSetLikeStructureGroupoidPartialHomeomorph H = { coe := fun (s : StructureGroupoid H) => s.members, coe_injective' := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Partial order on the set of groupoids, given by inclusion of the members of the groupoid.
Equations
- StructureGroupoid.partialOrder = PartialOrder.lift StructureGroupoid.members ⋯
The trivial groupoid, containing only the identity (and maps with empty source, as this is necessary from the definition).
Equations
- idGroupoid H = { members := {PartialHomeomorph.refl H} ∪ {e : PartialHomeomorph H H | e.source = ∅}, trans' := ⋯, symm' := ⋯, id_mem' := ⋯, locality' := ⋯, mem_of_eqOnSource' := ⋯ }
Instances For
Every structure groupoid contains the identity groupoid.
Equations
- instStructureGroupoidOrderBot = OrderBot.mk ⋯
Equations
- instInhabitedStructureGroupoid = { default := idGroupoid H }
To construct a groupoid, one may consider classes of partial homeomorphisms such that
both the function and its inverse have some property. If this property is stable under composition,
one gets a groupoid. Pregroupoid
bundles the properties needed for this construction, with the
groupoid of smooth functions with smooth inverses as an application.
Property describing membership in this groupoid: the pregroupoid "contains" all functions
H → H
having the pregroupoid property on somes : Set H
- comp : ∀ {f g : H → H} {u v : Set H}, self.property f u → self.property g v → IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → self.property (g ∘ f) (u ∩ f ⁻¹' v)
The pregroupoid property is stable under composition
- id_mem : self.property id Set.univ
Pregroupoids contain the identity map (on
univ
) - locality : ∀ {f : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, ∃ (v : Set H), IsOpen v ∧ x ∈ v ∧ self.property f (u ∩ v)) → self.property f u
The pregroupoid property is "local", in the sense that
f
has the pregroupoid property onu
iff its restriction to each open subset ofu
has it
Instances For
The pregroupoid property is stable under composition
Pregroupoids contain the identity map (on univ
)
The pregroupoid property is "local", in the sense that f
has the pregroupoid property on u
iff its restriction to each open subset of u
has it
Construct a groupoid of partial homeos for which the map and its inverse have some property, from a pregroupoid asserting that this property is stable under composition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pregroupoid of all partial maps on a topological space H
.
Equations
- continuousPregroupoid H = { property := fun (x : H → H) (x : Set H) => True, comp := ⋯, id_mem := trivial, locality := ⋯, congr := ⋯ }
Instances For
Equations
- instInhabitedPregroupoid H = { default := continuousPregroupoid H }
The groupoid of all partial homeomorphisms on a topological space H
.
Equations
- continuousGroupoid H = (continuousPregroupoid H).groupoid
Instances For
Every structure groupoid is contained in the groupoid of all partial homeomorphisms.
Equations
- instStructureGroupoidOrderTop = OrderTop.mk ⋯
Equations
- instCompleteLatticeStructureGroupoid = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
A groupoid is closed under restriction if it contains all restrictions of its element local homeomorphisms to open subsets of the source.
- closedUnderRestriction : ∀ {e : PartialHomeomorph H H}, e ∈ G → ∀ (s : Set H), IsOpen s → e.restr s ∈ G
Instances
The trivial restriction-closed groupoid, containing only partial homeomorphisms equivalent to the restriction of the identity to the various open subsets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The trivial restriction-closed groupoid is indeed ClosedUnderRestriction
.
Equations
- ⋯ = ⋯
A groupoid is closed under restriction if and only if it contains the trivial restriction-closed groupoid.
The groupoid of all partial homeomorphisms on a topological space H
is closed under restriction.
Equations
- ⋯ = ⋯
Charted spaces #
A charted space is a topological space endowed with an atlas, i.e., a set of local
homeomorphisms taking value in a model space H
, called charts, such that the domains of the charts
cover the whole space. We express the covering property by choosing for each x
a member
chartAt x
of the atlas containing x
in its source: in the smooth case, this is convenient to
construct the tangent bundle in an efficient way.
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 over ℝ^(2n)
.
- atlas : Set (PartialHomeomorph M H)
The atlas of charts in the
ChartedSpace
. - chartAt : M → PartialHomeomorph M H
The preferred chart at each point in the charted space.
- mem_chart_source : ∀ (x : M), x ∈ (ChartedSpace.chartAt x).source
- chart_mem_atlas : ∀ (x : M), ChartedSpace.chartAt x ∈ ChartedSpace.atlas
Instances
The atlas of charts in a ChartedSpace
.
Instances For
The preferred chart at a point x
in a charted space M
.
Equations
- chartAt H x = ChartedSpace.chartAt x
Instances For
An empty type is a charted space over any topological space.
Equations
- ChartedSpace.empty H M = { atlas := ∅, chartAt := fun (x : M) => ⋯.elim, mem_chart_source := ⋯, chart_mem_atlas := ⋯ }
Instances For
Any space is a ChartedSpace
modelled over itself, by just using the identity chart.
Equations
- chartedSpaceSelf H = { atlas := {PartialHomeomorph.refl H}, chartAt := fun (x : H) => PartialHomeomorph.refl H, mem_chart_source := ⋯, chart_mem_atlas := ⋯ }
In the trivial ChartedSpace
structure of a space modelled over itself through the identity,
the atlas members are just the identity.
In the model space, chartAt
is always the identity.
achart H x
is the chart at x
, considered as an element of the atlas.
Especially useful for working with BasicSmoothVectorBundleCore
.
Instances For
If a topological space admits an atlas with locally compact charts, then the space itself is locally compact.
If a topological space admits an atlas with locally connected charts, then the space itself is locally connected.
If M
is modelled on H'
and H'
is itself modelled on H
, then we can consider M
as being
modelled on H
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- instTopologicalSpaceModelProd H H' = instTopologicalSpaceProd
Equations
- instTopologicalSpaceModelPi = Pi.topologicalSpace
The product of two charted spaces is naturally a charted space, with the canonical construction of the atlas of product maps.
Equations
- One or more equations did not get rendered due to their size.
The product of a finite family of charted spaces is naturally a charted space, with the canonical construction of the atlas of finite product maps.
Equations
- One or more equations did not get rendered due to their size.
Constructing a topology from an atlas #
Sometimes, one may want to construct a charted space structure on a space which does not yet
have a topological structure, where the topology would come from the charts. For this, one needs
charts that are only partial equivalences, and continuity properties for their composition.
This is formalised in ChartedSpaceCore
.
- atlas : Set (PartialEquiv M H)
An atlas of charts, which are only
PartialEquiv
s - chartAt : M → PartialEquiv M H
The preferred chart at each point
- mem_chart_source : ∀ (x : M), x ∈ (self.chartAt x).source
- chart_mem_atlas : ∀ (x : M), self.chartAt x ∈ self.atlas
- open_source : ∀ (e e' : PartialEquiv M H), e ∈ self.atlas → e' ∈ self.atlas → IsOpen (e.symm.trans e').source
- continuousOn_toFun : ∀ (e e' : PartialEquiv M H), e ∈ self.atlas → e' ∈ self.atlas → ContinuousOn (↑(e.symm.trans e')) (e.symm.trans e').source
Instances For
Topology generated by a set of charts on a Type.
Equations
Instances For
An element of the atlas in a charted space without topology becomes a partial homeomorphism
for the topology constructed from this atlas. The PartialHomeomorph
version is given in this
definition.
Equations
- c.partialHomeomorph e he = { toPartialEquiv := e, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }
Instances For
Given a charted space without topology, endow it with a genuine charted space structure with respect to the topology constructed from the atlas.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Charted space with a given structure groupoid #
A charted space has an atlas in a groupoid G
if the change of coordinates belong to the
groupoid.
Instances
Reformulate in the StructureGroupoid
namespace the compatibility condition of charts in a
charted space admitting a structure groupoid, to make it more easily accessible with dot
notation.
The trivial charted space structure on the model space is compatible with any groupoid.
Equations
- ⋯ = ⋯
Any charted space structure is compatible with the groupoid of all partial homeomorphisms.
Equations
- ⋯ = ⋯
If G
is closed under restriction, the transition function between
the restriction of two charts e
and e'
lies in G
.
Given a charted space admitting a structure groupoid, the maximal atlas associated to this structure groupoid is the set of all charts that are compatible with the atlas, i.e., such that changing coordinates with an atlas member gives an element of the groupoid.
Equations
- StructureGroupoid.maximalAtlas M G = {e : PartialHomeomorph M H | ∀ e' ∈ atlas H M, e.symm.trans e' ∈ G ∧ e'.symm.trans e ∈ G}
Instances For
The elements of the atlas belong to the maximal atlas for any structure groupoid.
Changing coordinates between two elements of the maximal atlas gives rise to an element of the structure groupoid.
The maximal atlas of a structure groupoid is stable under equivalence.
In the model space, the identity is in any maximal atlas.
In the model space, any element of the groupoid is in the maximal atlas.
If a single partial homeomorphism e
from a space α
into H
has source covering the whole
space α
, then that partial homeomorphism induces an H
-charted space structure on α
.
(This condition is equivalent to e
being an open embedding of α
into H
; see
OpenEmbedding.singletonChartedSpace
.)
Equations
- e.singletonChartedSpace h = { atlas := {e}, chartAt := fun (x : α) => e, mem_chart_source := ⋯, chart_mem_atlas := ⋯ }
Instances For
Given a partial homeomorphism e
from a space α
into H
, if its source covers the whole
space α
, then the induced charted space structure on α
is HasGroupoid G
for any structure
groupoid G
which is closed under restrictions.
An open embedding of α
into H
induces an H
-charted space structure on α
.
See PartialHomeomorph.singletonChartedSpace
.
Equations
- h.singletonChartedSpace = (OpenEmbedding.toPartialHomeomorph f h).singletonChartedSpace ⋯
Instances For
An open subset of a charted space is naturally a charted space.
If s
is a non-empty open subset of M
, every chart of s
is the restriction
of some chart on M
.
If t
is a non-empty open subset of H
,
every chart of t
is the restriction of some chart on H
.
If a groupoid G
is ClosedUnderRestriction
, then an open subset of a space which is
HasGroupoid G
is naturally HasGroupoid G
.
Equations
- ⋯ = ⋯
Restricting a chart of M
to an open subset s
yields a chart in the maximal atlas of s
.
NB. We cannot deduce membership in atlas H s
in general: by definition, this atlas contains
precisely the restriction of each preferred chart at x ∈ s
--- whereas atlas H M
can contain more charts than these.
Structomorphisms #
A G
-diffeomorphism between two charted spaces is a homeomorphism which, when read in the
charts, belongs to G
. We avoid the word diffeomorph as it is too related to the smooth category,
and use structomorph instead.
- toFun : M → M'
- invFun : M' → M
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- continuous_toFun : Continuous self.toFun
- continuous_invFun : Continuous self.invFun
- mem_groupoid : ∀ (c : PartialHomeomorph M H) (c' : PartialHomeomorph M' H), c ∈ atlas H M → c' ∈ atlas H M' → c.symm.trans (self.toPartialHomeomorph.trans c') ∈ G
Instances For
The identity is a diffeomorphism of any charted space, for any groupoid.
Equations
- Structomorph.refl M = { toHomeomorph := Homeomorph.refl M, mem_groupoid := ⋯ }
Instances For
The inverse of a structomorphism is a structomorphism.
Equations
- e.symm = { toHomeomorph := e.symm, mem_groupoid := ⋯ }
Instances For
The composition of structomorphisms is a structomorphism.
Equations
- e.trans e' = { toHomeomorph := e.trans e'.toHomeomorph, mem_groupoid := ⋯ }
Instances For
Restricting a chart to its source s ⊆ M
yields a chart in the maximal atlas of s
.
Each chart of a charted space is a structomorphism between its source and target.
Equations
- One or more equations did not get rendered due to their size.