A manifold is a topological space M locally modelled on a model space H, i.e., the manifold is covered by open subsets on which there are local homeomorphisms (the charts) going to H. 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 manifold:

- 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 manifold 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.

`structure_groupoid H`

: a subset of local homeomorphisms of `H`

stable under composition, inverse
and restriction (ex: local diffeos)
`pregroupoid H`

: a subset of local homeomorphisms 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)
`continuous_groupoid H`

: the groupoid of all local homeomorphisms of `H`

`manifold H M`

: manifold 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 manifold modelled on
`H`

, require that all coordinate changes belong to `G`

. This is a type
class
`atlas H M`

: when `M`

is a manifold modelled on `H`

, the atlas of this manifold
structure, i.e., the set of charts
`structomorph G M M'`

: the set of diffeomorphisms between the manifolds M and M' for the
groupoid G. We avoid the word diffeomorphisms, keeping it for the
smooth category.

As a basic example, we give the instance
`instance manifold_model_space (H : Type*) [topological_space H] : manifold H H`

saying that a topological space is a manifold over itself, with the identity as unique chart. This
manifold structure is compatible with any groupoid.

The atlas in a manifold 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 `manifold_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 manifold, 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).

- members : set (local_homeomorph H H)
- comp : ∀ (e e' : local_homeomorph H H), e ∈ c.members → e' ∈ c.members → e.trans e' ∈ c.members
- inv : ∀ (e : local_homeomorph H H), e ∈ c.members → e.symm ∈ c.members
- id_mem : local_homeomorph.refl H ∈ c.members
- locality : ∀ (e : local_homeomorph H H), (∀ (x : H), x ∈ e.to_local_equiv.source → (∃ (s : set H), is_open s ∧ x ∈ s ∧ e.restr s ∈ c.members)) → e ∈ c.members
- eq_on_source : ∀ (e e' : local_homeomorph H H), e ∈ c.members → e' ≈ e → e' ∈ c.members

A structure groupoid is a set of local homeomorphisms of a topological space stable under composition and inverse. They appear in the definition of the smoothness class of a manifold.

@[instance]

- structure_groupoid.has_mem = {mem := λ (e : local_homeomorph H H) (G : structure_groupoid H), e ∈ G.members}

@[instance]

Partial order on the set of groupoids, given by inclusion of the members of the groupoid

- structure_groupoid.partial_order = partial_order.lift structure_groupoid.members structure_groupoid.partial_order._proof_1 (lattice.order_bot.to_partial_order (set (local_homeomorph H H)))

The trivial groupoid, containing only the identity (and maps with empty source, as this is necessary from the definition)

- id_groupoid H = {members := {local_homeomorph.refl H} ∪ {e : local_homeomorph H H | e.to_local_equiv.source = ∅}, comp := _, inv := _, id_mem := _, locality := _, eq_on_source := _}

@[instance]

Every structure groupoid contains the identity groupoid

- structure_groupoid.lattice.order_bot = {bot := id_groupoid H _inst_1, le := partial_order.le structure_groupoid.partial_order, lt := partial_order.lt structure_groupoid.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}

- property : (H → H) → set H → Prop
- comp : ∀ {f g : H → H} {u v : set H}, c.property f u → c.property g v → is_open (u ∩ f ⁻¹' v) → c.property (g ∘ f) (u ∩ f ⁻¹' v)
- id_mem : c.property id set.univ
- locality : ∀ {f : H → H} {u : set H}, is_open u → (∀ (x : H), x ∈ u → (∃ (v : set H), is_open v ∧ x ∈ v ∧ c.property f (u ∩ v))) → c.property f u
- congr : ∀ {f g : H → H} {u : set H}, is_open u → (∀ (x : H), x ∈ u → g x = f x) → c.property f u → c.property g u

To construct a groupoid, one may consider classes of local homeos 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.

Construct a groupoid of local homeos for which the map and its inverse have some property, from a pregroupoid asserting that this property is stable under composition.

- PG.groupoid = {members := {e : local_homeomorph H H | PG.property e.to_local_equiv.to_fun e.to_local_equiv.source ∧ PG.property e.to_local_equiv.inv_fun e.to_local_equiv.target}, comp := _, inv := _, id_mem := _, locality := _, eq_on_source := _}

theorem mem_groupoid_of_pregroupoid {H : Type u} [topological_space H] (PG : pregroupoid H) (e : local_homeomorph H H) :

e ∈ PG.groupoid ↔
PG.property
e.to_local_equiv.to_fun
e.to_local_equiv.source ∧
PG.property
e.to_local_equiv.inv_fun
e.to_local_equiv.target

theorem mem_pregroupoid_of_eq_on_source {H : Type u} [topological_space H] (PG : pregroupoid H) {e e' : local_homeomorph H H} :

e ≈ e' →
PG.property
e.to_local_equiv.to_fun
e.to_local_equiv.source →
PG.property
e'.to_local_equiv.to_fun
e'.to_local_equiv.source

The groupoid of all local homeomorphisms on a topological space H

@[instance]

Every structure groupoid is contained in the groupoid of all local homeomorphisms

- structure_groupoid.lattice.order_top = {top := continuous_groupoid H _inst_1, le := partial_order.le structure_groupoid.partial_order, lt := partial_order.lt structure_groupoid.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}

@[class]

structure manifold (H : Type u_4) [topological_space H] (M : Type u_5) [topological_space M] :

Type (max u_4 u_5)

- atlas : set (local_homeomorph M H)
- chart_at : M → local_homeomorph M H
- mem_chart_source : ∀ (x : M), x ∈ (manifold.chart_at H x).to_local_equiv.source
- chart_mem_atlas : ∀ (x : M), manifold.chart_at H x ∈ manifold.atlas H M

A manifold 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 chosing for each x a member `chart_at 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).

@[instance]

Any space is a manifold modelled over itself, by just using the identity chart

- manifold_model_space H = {atlas := {local_homeomorph.refl H}, chart_at := λ (x : H), local_homeomorph.refl H, mem_chart_source := _, chart_mem_atlas := _}

@[simp]

In the trivial manifold structure of a space modelled over itself through the identity, the atlas members are just the identity

@[simp]

In the model space, chart_at is always the identity

- atlas : set (local_equiv M H)
- chart_at : M → local_equiv M H
- mem_chart_source : ∀ (x : M), x ∈ (c.chart_at x).source
- chart_mem_atlas : ∀ (x : M), c.chart_at x ∈ c.atlas
- open_source : ∀ (e e' : local_equiv M H), e ∈ c.atlas → e' ∈ c.atlas → is_open (e.symm.trans e').source
- continuous_to_fun : ∀ (e e' : local_equiv M H), e ∈ c.atlas → e' ∈ c.atlas → continuous_on (e.symm.trans e').to_fun (e.symm.trans e').source

Sometimes, one may want to construct a manifold 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 local equivs, and continuity properties for their composition.
This is formalised in `manifold_core`

.

def manifold_core.to_topological_space {H : Type u} {M : Type u_1} [topological_space H] :

manifold_core H M → topological_space M

Topology generated by a set of charts on a Type.

- c.to_topological_space = topological_space.generate_from (⋃ (e : local_equiv M H) (he : e ∈ c.atlas) (s : set H) (s_open : is_open s), {e.to_fun ⁻¹' s ∩ e.source})

theorem manifold_core.open_source' {H : Type u} {M : Type u_1} [topological_space H] (c : manifold_core H M) {e : local_equiv M H} :

theorem manifold_core.open_target {H : Type u} {M : Type u_1} [topological_space H] (c : manifold_core H M) {e : local_equiv M H} :

def manifold_core.local_homeomorph {H : Type u} {M : Type u_1} [topological_space H] (c : manifold_core H M) (e : local_equiv M H) :

- c.local_homeomorph e he = {to_local_equiv := {to_fun := e.to_fun, inv_fun := e.inv_fun, source := e.source, target := e.target, map_source := _, map_target := _, left_inv := _, right_inv := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}

def manifold_core.to_manifold {H : Type u} {M : Type u_1} [topological_space H] (c : manifold_core H M) :

manifold H M

- c.to_manifold = {atlas := ⋃ (e : local_equiv M H) (he : e ∈ c.atlas), {c.local_homeomorph e he}, chart_at := λ (x : M), c.local_homeomorph (c.chart_at x) _, mem_chart_source := _, chart_mem_atlas := _}

@[class]

structure has_groupoid {H : Type u_4} [topological_space H] (M : Type u_5) [topological_space M] [manifold H M] :

structure_groupoid H → Prop

- compatible : ∀ {e e' : local_homeomorph M H}, e ∈ manifold.atlas H M → e' ∈ manifold.atlas H M → e.symm.trans e' ∈ G

A manifold has an atlas in a groupoid G if the change of coordinates belong to the groupoid

theorem has_groupoid_of_le {H : Type u} {M : Type u_1} [topological_space H] [topological_space M] [manifold H M] {G₁ G₂ : structure_groupoid H} :

theorem has_groupoid_of_pregroupoid {H : Type u} {M : Type u_1} [topological_space H] [topological_space M] [manifold H M] (PG : pregroupoid H) :

(∀ {e e' : local_homeomorph M H},
e ∈ manifold.atlas H M →
e' ∈ manifold.atlas H M →
PG.property
(e.symm.trans
e').to_local_equiv.to_fun
(e.symm.trans
e').to_local_equiv.source) →
has_groupoid M PG.groupoid

@[instance]

def has_groupoid_model_space (H : Type u_1) [topological_space H] (G : structure_groupoid H) :

has_groupoid H G

The trivial manifold structure on the model space is compatible with any groupoid

- _ = _

@[instance]

def has_groupoid_continuous_groupoid {H : Type u} {M : Type u_1} [topological_space H] [topological_space M] [manifold H M] :

Any manifold structure is compatible with the groupoid of all local homeomorphisms

structure structomorph {H : Type u} [topological_space H] (G : structure_groupoid H) (M : Type u_4) (M' : Type u_5) [topological_space M] [topological_space M'] [manifold H M] [manifold H M'] :

Type (max u_4 u_5)

- to_homeomorph : M ≃ₜ M'
- to_fun_mem_groupoid : ∀ (c_1 : local_homeomorph M H) (c' : local_homeomorph M' H), c_1 ∈ manifold.atlas H M → c' ∈ manifold.atlas H M' → c_1.symm.trans (c.to_homeomorph.to_local_homeomorph.trans c') ∈ G

A G-diffeomorphism between two manifolds 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.

def structomorph.refl {H : Type u} [topological_space H] {G : structure_groupoid H} (M : Type u_1) [topological_space M] [manifold H M] [has_groupoid M G] :

structomorph G M M

The identity is a diffeomorphism of any manifold, for any groupoid.

- structomorph.refl M = {to_homeomorph := {to_equiv := (homeomorph.refl M).to_equiv, continuous_to_fun := _, continuous_inv_fun := _}, to_fun_mem_groupoid := _}

def structomorph.symm {H : Type u} {M : Type u_1} {M' : Type u_2} [topological_space H] [topological_space M] [manifold H M] [topological_space M'] {G : structure_groupoid H} [manifold H M'] :

structomorph G M M' → structomorph G M' M

The inverse of a structomorphism is a structomorphism

- e.symm = {to_homeomorph := {to_equiv := e.to_homeomorph.symm.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}, to_fun_mem_groupoid := _}

def structomorph.trans {H : Type u} {M : Type u_1} {M' : Type u_2} {M'' : Type u_3} [topological_space H] [topological_space M] [manifold H M] [topological_space M'] [topological_space M''] {G : structure_groupoid H} [manifold H M'] [manifold H M''] :

The composition of structomorphisms is a structomorphism

- e.trans e' = {to_homeomorph := {to_equiv := (e.to_homeomorph.trans e'.to_homeomorph).to_equiv, continuous_to_fun := _, continuous_inv_fun := _}, to_fun_mem_groupoid := _}