Subbundles spanned by continuous local frames #
Let E be a topological vector bundle over B with model fibre F, and let V assign to every
point x a subspace V x of the fibre E x. The total space of V, the pairs (x, v) with
v ∈ V x, carries the topology of a subspace of the total space of E
(TauCeti.subbundleTopology). This file shows that over ℝ or ℂ a continuous local frame of
V gives a local trivialization of V for this topology, and that the coordinate changes between
two such trivializations are continuous. For a family of subspaces with a continuous local frame of
a fixed size near every point (TauCeti.HasLocalSubbundleFrames), these are the data and the two
axioms of a topological vector bundle structure, a subbundle of E
(TauCeti.HasLocalSubbundleFrames.vectorBundle), whose atlas consists of the trivializations of
all continuous local frames. TauCeti.IsContMDiffDistribution.vectorBundle assembles the same
data for the distributions of a manifold, keeping only C^n frames in its atlas so that the
result is also a C^n vector bundle.
A continuous local frame X of V on a set U (TauCeti.IsSubbundleFrameOn F V X U) is a
family of sections of E, continuous on U, whose values form a basis of V y at each point
y ∈ U (TauCeti.IsSubbundleFrameOn.basis). The trivialization
TauCeti.IsSubbundleFrameOn.trivialization sends a vector of V y to its coordinates in that
basis. The substance is that these coordinates depend continuously on the vector in the subspace
topology. Read in a trivialization of E near y₀, the frame becomes a continuous family of
injective operators A y : 𝕜ᵏ →L[𝕜] F; an injective operator out of a finite-dimensional space
has a continuous left inverse, and left inverses can be chosen continuously in families
(ContinuousAt.exists_continuousAt_leftInverse). The same argument shows that the coordinate
changes between two frames are continuous.
Over a general nontrivially normed field a finite-dimensional subspace of the model space need
not be complemented, which is why the scalars are ℝ or ℂ (IsRCLikeNormedField 𝕜); the model
fibre F is an arbitrary normed space and the base an arbitrary topological space. The subspace
topology and the algebraic API of frames (TauCeti.IsSubbundleFrameOn.basis) only need a semiring
of scalars.
The model fibre F of E cannot be recovered from V, so the subspace topology is not an
instance; install it with letI := TauCeti.subbundleTopology F V.
Main definitions #
TauCeti.subbundleTopology: the subspace topology on the total space of a family of subspaces of the fibres of a bundle.TauCeti.IsSubbundleFrameOn F V X U: the sectionsX iform a continuous local frame ofVonU.TauCeti.IsSubbundleFrameOn.basis: the basis of a fibre ofVgiven by a local frame.TauCeti.IsSubbundleFrameOn.trivialization: the local trivialization ofVgiven by a local frame on an open set.TauCeti.HasLocalSubbundleFrames F ι V: every point has an open neighbourhood with a continuous local frame ofVindexed byι.TauCeti.HasLocalSubbundleFrames.fiberBundle: the resulting fibre bundle structure onV.
Main results #
TauCeti.isEmbedding_totalSpace_subbundle: the total space ofVis a subspace of the total space ofE.TauCeti.isInducing_totalSpaceMk_subbundle: each fibreV xcarries the topology induced from the total space ofV.TauCeti.IsSubbundleFrameOn.continuousOn_coordChangeL: the coordinate changes between the trivializations of two local frames are continuous on the overlap.TauCeti.vectorBundle_of_forall_mem_trivializationAtlas: a fibre bundle structure on a family of subspaces whose atlas consists of local frame trivializations is a topological vector bundle.TauCeti.HasLocalSubbundleFrames.vectorBundle: a family of subspaces with continuous local frames of a fixed finite size near every point is a topological vector bundle.Bundle.Trivialization.isSubbundleFrameOn_symm_comp: a continuous family of injective operators into the model fibre, read through a linear trivialization, is a local frame of the subspaces corresponding to its ranges.Bundle.Trivialization.continuousAt_symm_subbundle: a vector given by a trivialization ofV, read in a trivialization ofE, depends continuously on the base point.
References #
- J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 10 (the local frame criterion for smooth subbundles, Lemma 10.32, of which this is the continuous counterpart).
The total space of a family V of subspaces of the fibres of E, the pairs (x, v) with
v ∈ V x, carries the topology of a subspace of the total space of E. The model-fibre parameter
F' of Bundle.TotalSpace plays no role. Since F cannot be recovered from V, this is not an
instance; install it with letI.
Instances For
The total space of a family of subspaces of the fibres of E is embedded in the total space
of E.
The projection of the total space of a family of subspaces of the fibres of E is
continuous.
Each subspace V x, with the topology induced from the fibre E x, carries the topology
induced from the total space of V.
The sections X i of E form a continuous local frame of the family of subspaces V on the
set U: each X i is continuous on U as a map into the total space of E, and at every point
x of U the values X i x form a basis of V x.
- continuousOn (i : ι) : ContinuousOn (fun (x : B) => Bundle.TotalSpace.mk' F x (X i x)) U
Each member of the frame is a continuous section on
U. The values of the frame at a point of
Uare linearly independent.The values of the frame at a point of
Uspan the subspaceVthere.
Instances For
A local frame of V on U is a local frame of V on every subset of U.
Every member of a local frame of V on U takes values in V on U.
The subspaces of a family with a local frame indexed by ι have dimension card ι.
At a point y of U, a local frame of V on U is a basis of the subspace V y.
Instances For
At a point y of U, the vector of V y with coordinates c in the frame X is the
combination ∑ i, c i • X i y.
Every point of the base has an open neighbourhood carrying a continuous local frame of the
family of subspaces V, indexed by ι. Over ℝ or ℂ, when ι is finite, such a family,
with the subspace topology, is a vector bundle with model fibre ι → 𝕜
(TauCeti.HasLocalSubbundleFrames.vectorBundle): a subbundle of E.
Instances For
Unfolding TauCeti.HasLocalSubbundleFrames.
The subspaces of a family with local frames indexed by ι all have dimension card ι.
The frame X near y, read in the trivialization of E at y₀, as an operator from
coordinates to the model fibre.
Instances For
The operator trivOperator 𝕜 F X y₀ y is the finite sum over the frame of the frame vectors
read in the trivialization of E at y₀, each scaled by its coordinate.
Over the base set of the trivialization at y₀, the operator trivOperator 𝕜 F X y₀ y sends
coordinates to the corresponding combination of the frame, read in that trivialization.
A family of sections X i of E that are continuous at y₀, read in the trivialization of
E at y₀, is an operator c ↦ ∑ i, c i • X i depending continuously on the base point at
y₀.
At a point y₀ of U, the frame read in the trivialization of E at y₀ is injective on
coordinates.
The local trivialization of a family of subspaces V given by a local frame X on an open
set U: over U, a vector of V y is sent to its coordinates in the frame. The total space of
V carries the subspace topology TauCeti.subbundleTopology. Only finiteness of the index type
is required; no enumeration is chosen as part of the trivialization.
Instances For
Over U, the frame trivialization sends a vector to its coordinates in the frame.
Over U, the inverse of the frame trivialization sends coordinates to the corresponding
combination of the frame.
The frame trivialization is fibrewise linear.
The coordinate changes between the trivializations of two local frames of V are continuous
on the intersection of their domains.
Local frame criterion for subbundles, atlas form. A fibre bundle structure on a family of
subspaces V, for the subspace topology of the total space of E, each of whose trivializations
is the trivialization of a continuous local frame of V on an open set, is a topological vector
bundle with model fibre ι → 𝕜: the frame trivializations are linear, with continuous coordinate
changes.
A family of subspaces with continuous local frames indexed by a finite type ι near every
point is a fibre bundle with fibre ι → 𝕜, the topology of its total space being that of a
subspace of the total space of E. Its trivializations are those of all continuous local frames
of V on open sets (TauCeti.IsSubbundleFrameOn.trivialization). Use this definition as a local
instance; it chooses a local frame near every point.
Instances For
The trivializations of hV.fiberBundle are the trivializations of the continuous local frames
of V on open sets.
Local frame criterion for subbundles. A family of subspaces with continuous local frames
indexed by a finite type ι near every point, with the subspace topology of the total space of
E and the atlas of hV.fiberBundle, is a topological vector bundle with model fibre ι → 𝕜.
A vector e'.symm x v given by a trivialization e' of a family V of subspaces of the
fibres of E, read in a trivialization g of E, depends continuously on the base point near a
point of both base sets, provided the total space of V maps continuously into that of E.
Read in a linear trivialization e, a continuous family of injective operators κ x whose
ranges correspond to the subspaces V x gives a continuous local frame of V: the images under
e.symm x of the values of κ x on a basis.