The groupoid of C^n
, fiberwise-linear maps #
This file contains preliminaries for the definition of a C^n
vector bundle: an associated
StructureGroupoid
, the groupoid of contMDiffFiberwiseLinear
functions.
The groupoid of C^n
, fiberwise-linear maps #
For B
a topological space and F
a 𝕜
-normed space, a map from U : Set B
to F ≃L[𝕜] F
determines an open partial homeomorphism from B × F
to itself by its action fiberwise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of FiberwiseLinear.openPartialHomeomorph
.
For B
a topological space and F
a 𝕜
-normed space, a map from U : Set B
to F ≃L[𝕜] F
determines an open partial homeomorphism from B × F
to itself by its action fiberwise.
Instances For
Compute the composition of two open partial homeomorphisms induced by fiberwise linear equivalences.
Alias of FiberwiseLinear.trans_openPartialHomeomorph_apply
.
Compute the composition of two open partial homeomorphisms induced by fiberwise linear equivalences.
Compute the source of the composition of two open partial homeomorphisms induced by fiberwise linear equivalences.
Alias of FiberwiseLinear.source_trans_openPartialHomeomorph
.
Compute the source of the composition of two open partial homeomorphisms induced by fiberwise linear equivalences.
Compute the target of the composition of two open partial homeomorphisms induced by fiberwise linear equivalences.
Alias of FiberwiseLinear.target_trans_openPartialHomeomorph
.
Compute the target of the composition of two open partial homeomorphisms induced by fiberwise linear equivalences.
Let e
be an open partial 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-C^n
fiberwise
linear open partial 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-C^n
fiberwise linear open partial homeomorphism.
Let e
be an open partial 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-C^n
fiberwise linear open partial homeomorphism. Then e
itself
is equal to some bi-C^n
fiberwise linear open partial homeomorphism.
This is the key mathematical point of the locality
condition in the construction of the
StructureGroupoid
of bi-C^n
fiberwise linear open partial homeomorphisms. The proof is by
gluing together the various bi-C^n
fiberwise linear open partial 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 contMDiffFiberwiseLinear
.
For B
a manifold and F
a normed space, the groupoid on B × F
consisting of local
homeomorphisms which are bi-C^n
and fiberwise linear, and induce the identity on B
.
When a (topological) vector bundle is C^n
, then the composition of charts associated
to the vector bundle belong to this groupoid.
Equations
- One or more equations did not get rendered due to their size.