The groupoid of smooth, fiberwise-linear maps #
This file contains preliminaries for the definition of a smooth vector bundle: an associated
StructureGroupoid
, the groupoid of smoothFiberwiseLinear
functions.
The groupoid of smooth, fiberwise-linear maps #
For B
a topological space and F
a 𝕜
-normed space, a map from U : Set B
to F ≃L[𝕜] F
determines a local homeomorphism from B × F
to itself by its action fiberwise.
Instances For
Compute the composition of two local homeomorphisms induced by fiberwise linear equivalences.
Compute the source of the composition of two local homeomorphisms induced by fiberwise linear equivalences.
Compute the target of the composition of two local homeomorphisms induced by fiberwise linear equivalences.
Let e
be a local homeomorphism of B × F
. Suppose that at every point p
in the source of
e
, there is some neighbourhood s
of p
on which e
is equal to a bi-smooth fiberwise linear
local homeomorphism.
Then the source of e
is of the form U ×ˢ univ
, for some set U
in B
, and, at any point x
in
U
, admits a neighbourhood u
of x
such that e
is equal on u ×ˢ univ
to some bi-smooth
fiberwise linear local homeomorphism.
Let e
be a local homeomorphism of B × F
whose source is U ×ˢ univ
, for some set U
in
B
, and which, at any point x
in U
, admits a neighbourhood u
of x
such that e
is equal on
u ×ˢ univ
to some bi-smooth fiberwise linear local homeomorphism. Then e
itself is equal to
some bi-smooth fiberwise linear local homeomorphism.
This is the key mathematical point of the locality
condition in the construction of the
StructureGroupoid
of bi-smooth fiberwise linear local homeomorphisms. The proof is by gluing
together the various bi-smooth fiberwise linear local homeomorphism which exist locally.
The U
in the conclusion is the same U
as in the hypothesis. We state it like this, because this
is exactly what we need for smoothFiberwiseLinear
.
For B
a manifold and F
a normed space, the groupoid on B × F
consisting of local
homeomorphisms which are bi-smooth and fiberwise linear, and induce the identity on B
.
When a (topological) vector bundle is smooth, then the composition of charts associated
to the vector bundle belong to this groupoid.