Subbundles spanned by smooth local frames, and subbundle inclusions #
Let π β π' be a normed field extension, and let E be a C^n bundle over a π-manifold
B, with compatible π- and π'-vector bundle structures on the same atlas and model fibre
F. Let V assign to every point x a π'-subspace V x of the fibre E x. A continuous
local frame X of V on an open
set U gives the local trivialization TauCeti.IsSubbundleFrameOn.trivialization of V, which
sends a vector of V y to its coordinates in the basis X Β· y; with the subspace topology, these
trivializations make V a topological vector bundle. This file shows that when the sections
X i are C^n, the coordinate changes between such trivializations are C^n. This is the
compatibility condition for the trivializations of C^n local frames to form a C^n vector
bundle structure on V, a C^n subbundle of E. When V has C^n local frames of a fixed
finite size near every point (TauCeti.HasLocalContMDiffSubbundleFrames), the atlas of all their
trivializations is such a structure
(TauCeti.HasLocalContMDiffSubbundleFrames.contMDiffVectorBundle). The distributions of a
manifold (TauCeti.IsContMDiffDistribution.contMDiffVectorBundle) and conormal bundles
(TauCeti.CotangentBundle.conormalContMDiffVectorBundle) are instances.
Read in a trivialization of E near a point yβ, a C^n frame X becomes a C^n family of
injective operators A_X y : (π')α΅ βL[π'] F, namely c β¦ β i, c i β’ X i y
(TauCeti.IsSubbundleFrameOn.contMDiffAt_trivOperator). Such a family has C^n left inverses
near yβ (ContMDiffAt.exists_contMDiffAt_leftInverse), and the coordinate change from the frame
X to a second frame Y is L_Y y β A_X y for a π'-linear left inverse L_Y y of
A_Y y. All smoothness is over the ground field π. The finite-frame coordinate argument uses
IsRCLikeNormedField π' for HahnβBanach splitting; it requires no finite rank of the ambient
fibre. In particular it applies to complex subbundles of real-smooth complex vector bundles
without assuming an ambient global trivialization. The native subspace topology, frame
trivializations and coordinate changes are unchanged.
Conversely, whenever a family of subspaces V x β E (f x) along f : B' β B carries a C^n
vector bundle structure with finite-dimensional model fibre F' inside a finite-dimensional model
fibre F and its canonical inclusion into TotalSpace F E is C^n, that inclusion has the
immersion normal form: over the same base B with no boundarylessness hypothesis
(TauCeti.isImmersion_totalSpace_subbundle, TauCeti.isSmoothEmbedding_totalSpace_subbundle), and
along an embedding f : B' β B of a boundaryless manifold B' into an arbitrary manifold B
(TauCeti.isImmersion_lift_totalSpace_subbundle,
TauCeti.isSmoothEmbedding_lift_totalSpace_subbundle). In bundle trivializations the fibrewise
inclusion is a C^n family of split injections A x : F' βL[π] F; adjoining a fixed complement
Q produces a local C^n trivialization diffeomorphism straightening V to F' Γ {0}.
Main results #
TauCeti.IsSubbundleFrameOn.contMDiffAt_trivOperator:C^nsections ofE, read in a trivialization ofE, form aC^nfamily of operators.TauCeti.IsSubbundleFrameOn.contMDiffOn_coordChangeL: the coordinate changes between the trivializations of twoC^nlocal frames ofVareC^non the intersection of their domains.TauCeti.HasLocalContMDiffSubbundleFrames.contMDiffVectorBundle: smooth local frame criterion: a family of subspaces withC^nlocal frames of a fixed finite size near every point is aC^nsubbundle ofE.TauCeti.exists_isSubbundleFrameOn_map_synthesisMap: aC^nfamily of orthogonal projections of a coefficient space, synthesized againstC^nlinearly independent sections, givesC^nlocal frames of the image subspaces.Bundle.Trivialization.exists_isSubbundleFrameOn_map_symmβ: the ranges of aC^nfamily of operators of constant rank on the model fibre, read through a trivialization, haveC^nlocal frames.TauCeti.IsSubbundleFrameOn.contMDiffAt_totalSpace_subbundle: the canonical inclusion of a frame-trivializedC^nsubbundle intoTotalSpace F EisC^n.TauCeti.isImmersion_totalSpace_subbundle,TauCeti.isSmoothEmbedding_totalSpace_subbundle: aC^nvector subbundle overBwhose canonical inclusion intoTotalSpace F EisC^nis immersed (and, with the subspace topology,C^n-embedded) inTotalSpace F E.TauCeti.isImmersion_lift_totalSpace_subbundle,TauCeti.isSmoothEmbedding_lift_totalSpace_subbundle: the same for aC^nsubbundle off *α΅ Elifted intoTotalSpace F Ealong an embeddingf : B' β Bof a boundaryless manifoldB'.
References #
- J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Lemma 10.32 and Proposition 10.34.
A family of sections X i of E that are C^n at y, read in the trivialization of E at
any point yβ whose base set contains y, is an operator c β¦ β i, c i β’ X i depending C^n
over π on the base point at y, retaining its π'-linear coefficients.
Coordinate changes between C^n local frames are C^n. If X and Y are local frames
of V on open sets U and U' whose sections are C^n, then the coordinate change from the
trivialization of X to that of Y is a C^n family of π'-linear operators over the ground
field π on U β© U'. The finite frame may span a subspace of an infinite-dimensional ambient
fibre.
The canonical inclusion of a frame-trivialized subbundle is C^n. At any point p in the
domain U of a C^n local frame X whose trivialization belongs to the bundle atlas of V, the
canonical inclusion (x, v) β¦ (x, βv) from TotalSpace (ΞΉ β π') (fun x β¦ V x) into
TotalSpace F E is C^n over the ground field π, with its original scalar structures.
Every point of the base has an open neighbourhood carrying a local frame of the family of
π'-subspaces V, indexed by ΞΉ, whose members are C^n sections of E over the ground field
π. Over β or β, when ΞΉ is finite and E is a C^n vector bundle, such a family, with the
subspace topology, is a C^n vector bundle with model fibre ΞΉ β π', a C^n subbundle of E
(TauCeti.HasLocalContMDiffSubbundleFrames.contMDiffVectorBundle). With π' = β and π = β
this covers complex subbundles of real-smooth complex vector bundles.
Instances For
Unfolding TauCeti.HasLocalContMDiffSubbundleFrames.
C^n local frames are in particular continuous local frames.
C^n local frames are C^m local frames for every m β€ n.
A family of subspaces with C^n 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 C^n 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 C^n local frames of
V on open sets.
A family of subspaces with C^n 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 over π' with model fibre ΞΉ β π'.
Smooth local frame criterion for subbundles. If E is a C^n vector bundle over the
ground field π and the family of π'-subspaces V has C^n local frames indexed by a finite
type ΞΉ near every point, then V, with the subspace topology of the total space of E and the
atlas of hV.fiberBundle, is a C^n vector bundle with model fibre ΞΉ β π': a C^n subbundle
of E. Its π-vector bundle structure is the restriction of scalars of hV.vectorBundle.
The canonical inclusion (x, v) β¦ (x, βv) of a subbundle given by C^n local frames into
the total space of E is C^n over the ground field.
A C^n map into the total space of E with values in a subbundle given by C^n local frames
is C^n as a map into the subbundle. The frame coordinates are recovered from the ambient vector
by a C^n left inverse of the frame (ContMDiffAt.exists_contMDiffAt_leftInverse).
Local frames from smooth orthogonal projections. Let Ξ΅ be a C^n family of sections of
E, linearly independent at every point of an open set Uβ, and let W y be subspaces of the
coefficient space β^d whose orthogonal projections are C^n on Uβ. Near a point xβ β Uβ
where W xβ has dimension r, the images of the W y under the synthesis maps
c β¦ β i, c i β’ Ξ΅ i y have a C^n local frame of size r: project a basis of W xβ onto the
nearby W y and synthesize.
Local frames from a smooth family of operators of constant rank. Let e be a
trivialization of E in its atlas and let A y be operators on the model fibre F, depending
C^n on y in an open subset Uβ of the base set of e, all of rank r. Read through e, their
ranges are subspaces of the fibres E y; near every point of Uβ these have a C^n local frame
of size r.
If V is a C^n vector subbundle of E over B whose canonical inclusion into
TotalSpace F E is C^n, that inclusion is a C^n immersion at every point. Neither B nor its
model need be boundaryless or finite-dimensional.
If V is a C^n vector subbundle of E over B whose canonical inclusion into
TotalSpace F E is C^n, that inclusion is a C^n immersion. Neither B nor its model need be
boundaryless or finite-dimensional.
With the subspace topology subbundleTopology, a C^n vector subbundle V of E over B
whose canonical inclusion into TotalSpace F E is C^n is C^n-smoothly embedded in
TotalSpace F E.
Along a topological embedding f : B' β B of a boundaryless manifold B' that is a C^n
immersion at p.proj, a C^n vector subbundle V of f *α΅ E whose canonical inclusion into
TotalSpace F E is C^n is a C^n immersion at p. The ambient manifold B need not be
boundaryless.
Along a C^n smooth embedding f : B' β B of a boundaryless manifold B', a C^n vector
subbundle V of f *α΅ E whose canonical inclusion into TotalSpace F E is C^n is a C^n
immersion into TotalSpace F E. The ambient manifold B need not be boundaryless.
Along a C^n smooth embedding f : B' β B of a boundaryless manifold B', a C^n vector
subbundle V over B' whose canonical inclusion (x, v) β¦ (f x, v) into TotalSpace F E is
C^n and a topological embedding is C^n-smoothly embedded in TotalSpace F E.