The conormal vector subbundle of a map #
For a map i : Q → M between manifolds, the conormal fibres
TauCeti.CotangentBundle.conormalSpace J I i q ⊆ T*_{i q} M form a family of subspaces of the
pulled-back cotangent bundle i *ᵖ T*M. Their total space carries the subspace topology
TauCeti.CotangentBundle.instTopologicalSpaceTotalSpaceConormalSpace from i *ᵖ T*M, and
TauCeti.CotangentBundle.conormalInclusion sends (q, p) to (i q, p) ∈ T*M, with image
TauCeti.CotangentBundle.conormal J I i; it is a topological embedding whenever i is
(TauCeti.CotangentBundle.isEmbedding_conormalInclusion).
Over ℝ or ℂ, when M has dimension finrank 𝕜 F + k, i is C^m (n + 1 ≤ m), and di_q is
injective at every q : Q, the conormal spaces admit C^n local frames
(TauCeti.CotangentBundle.exists_isConormalFrameOn): near q₀ : Q, for a fixed complement
B : (Fin k → 𝕜) →L[𝕜] E to the coordinate differential A q₀, the projections
(A q).quotientRangeCoordinate B vanish on range (A q) and pull back through the tangent chart at
i q₀ to a C^n local basis of conormalSpace J I i. By the smooth local frame criterion
TauCeti.HasLocalContMDiffSubbundleFrames.contMDiffVectorBundle
(hasLocalContMDiffSubbundleFrames_conormalSpace), this makes conormalSpace J I i a C^n vector
bundle of rank k over Q (conormalFiberBundle, conormalVectorBundle,
conormalContMDiffVectorBundle) with C^n canonical inclusion into T*M
(contMDiff_conormalInclusion) and model dimension dim M (finrank_conormalBundleModel), without
assuming Q or M boundaryless. When Q is boundaryless and i is a C^m smooth embedding
(n + 1 ≤ m), TauCeti.isSmoothEmbedding_lift_totalSpace_subbundle shows conormalInclusion is a
C^n smooth embedding (isSmoothEmbedding_conormalInclusion). Point, full-manifold, product, and
slice examples are in Conormal.Basic and Conormal.Prod.
Main definitions and results #
TauCeti.CotangentBundle.conormalInclusion,range_conormalInclusion,isEmbedding_conormalInclusion: canonical map(q, p) ↦ (i q, p)intoT*M, with rangeconormal J I i, topological embedding wheniis.TauCeti.CotangentBundle.instTopologicalSpaceTotalSpaceConormalSpace: subspace topology fromi *ᵖ T*Mon the total space ofconormalSpace J I i.TauCeti.CotangentBundle.IsConormalFrameOn,exists_isConormalFrameOn:C^nlocal frames ofconormalSpace J I i, their pointwisebasisandtrivialization, and local existence without shrinking across finite orders.TauCeti.CotangentBundle.hasLocalContMDiffSubbundleFrames_conormalSpace: the conormal spaces haveC^nlocal frames of sizeknear every point.TauCeti.CotangentBundle.conormalFiberBundle,conormalVectorBundle,conormalContMDiffVectorBundle,contMDiff_conormalInclusion,isSmoothEmbedding_conormalInclusion:C^nvector subbundle structure andC^nsmooth embedding intoT*M.
References #
- A. Cannas da Silva, Lectures on Symplectic Geometry, LNM 1764, Springer, 2001, Section 3.3.
- J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., GTM 218, Springer, 2013, Lemma 10.32 and Proposition 11.27.
Canonical inclusion into the ambient cotangent bundle #
The canonical map from the total space of the conormal spaces of i : Q → M into T*M,
sending (q, p) with p ∈ conormalSpace J I i q to (i q, p). The model-fibre parameter P of
Bundle.TotalSpace plays no role.
Instances For
conormalInclusion sends the zero covector in the conormal space over q to the zero covector
in T*M over i q.
Every covector in the image of conormalInclusion annihilates the differential of i at its
base point in Q.
The image of conormalInclusion in T*M is the conormal set conormal J I i.
When i : Q → M is injective, conormalInclusion is injective.
Subbundle topology #
The total space of the conormal spaces of i : Q → M carries the subspace topology
(TauCeti.subbundleTopology) of the pulled-back cotangent bundle i *ᵖ T*M. The model-fibre
parameter P of Bundle.TotalSpace plays no role.
The bundle projection of the conormal spaces is continuous.
The canonical map conormalInclusion into T*M is continuous.
Along a topological embedding i : Q → M, conormalInclusion is a topological embedding of the
total space of conormalSpace J I i into T*M.
Local frames and C^n vector subbundle structure #
A family of covectors X j q ∈ T*_{i q} M over q : Q is a C^n local frame of
conormalSpace J I i on U ⊆ Q when each lift q ↦ (i q, X j q) into T*M is C^n on U and,
at every q ∈ U, the covectors X j q form a basis of conormalSpace J I i q.
- contMDiffOn_lift (j : ι) : ContMDiffOn J (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))) n (fun (q : Q) => ⟨i q, X j q⟩) U
Each lifted covector section
q ↦ (i q, X j q)isC^nonU. At every point of
U, the frame covectors are linearly independent.- span_eq {q : Q} (hq : q ∈ U) : Submodule.span 𝕜 (Set.range fun (x : ι) => X x q) = conormalSpace J I i q
At every point of
U, the frame covectors spanconormalSpace J I i q.
Instances For
Restricting a C^n local conormal frame to a subset preserves the frame property.
Lowering the regularity order preserves a local conormal frame.
Every C^n local conormal frame is a continuous local subbundle frame of
conormalSpace J I i inside the pulled-back cotangent bundle i *ᵖ T*M.
At a point q ∈ U, a local conormal frame X on U forms a basis of
conormalSpace J I i q.
Instances For
Coercing the j-th element of hX.basis hq into T*_{i q} M recovers X j q.
At q ∈ U, the conormal covector with coordinates c in hX.basis hq is the linear
combination ∑ j, c j • X j q.
On an open set U, each member of a C^n local conormal frame along ic : C^n⟮J, Q; I, M⟯ is
a C^n section of the pulled-back cotangent bundle ic *ᵖ T*M.
The local trivialization of conormalSpace J I ic over U determined by a local conormal
frame X along ic : C^n⟮J, Q; I, M⟯.
Instances For
hX.trivialization ic hU is the subbundle frame trivialization
hX.isSubbundleFrameOn.trivialization hU inside the pulled-back cotangent bundle ic *ᵖ T*M.
The base set of hX.trivialization ic hU is U.
Over U, the conormal frame trivialization sends a covector to its coordinates in the basis
hX.basis hp.
Over U, the partial-homeomorphism inverse of the conormal frame trivialization sends
(q, c) to (q, (hX.basis hz).equivFun.symm c).
Over U, the fibrewise inverse of the conormal frame trivialization sends coordinates c to
(hX.basis hq).equivFun.symm c.
The conormal frame trivialization is fibrewise linear.
Existence of C^n local conormal frames. When M has dimension finrank 𝕜 F + k, i is
C^m with n + 1 ≤ m, and mfderiv J I i q is injective at every q : Q, every point q₀ : Q
has an open neighbourhood U carrying a C^n local frame of conormalSpace J I i indexed by
Fin k. Smooth and analytic orders (∞, ω) are included without shrinking per finite order.
For a C^m map i : Q → M with n + 1 ≤ m, injective differentials, and ambient dimension
finrank 𝕜 F + k = finrank 𝕜 E, the conormal spaces conormalSpace J I i have C^n local frames
of size k near every point, as a family of subspaces of the pulled-back cotangent bundle
i *ᵖ T*M.
For a C^m map i : Q → M with n + 1 ≤ m, injective differentials, and ambient dimension
finrank 𝕜 F + k = finrank 𝕜 E, the conormal spaces conormalSpace J I i form a fibre bundle over
Q with model fibre Fin k → 𝕜, carrying the subspace topology from i *ᵖ T*M
(TauCeti.HasLocalContMDiffSubbundleFrames.fiberBundle). Install this definition locally with
letI.
Instances For
The trivializations of conormalFiberBundle are the trivializations associated with C^n local
conormal frames on open subsets of Q.
The conormal bundle is a topological vector bundle. Its local frame trivializations are linear with continuous coordinate changes.
The conormal bundle is a C^n vector bundle. On C^m manifolds with n + 1 ≤ m, the
conormal spaces have C^n local frames, so the smooth local frame criterion
TauCeti.HasLocalContMDiffSubbundleFrames.contMDiffVectorBundle applies.
The canonical inclusion conormalInclusion of the conormal bundle into T*M is C^n.
Dimension of the conormal bundle model. When finrank 𝕜 F + k = finrank 𝕜 E, the model
space F × (Fin k → 𝕜) of the conormal bundle has the same dimension as M.
The conormal bundle of an embedded submanifold is smoothly embedded in T*M. For a C^m
smooth embedding i : Q → M (n + 1 ≤ m) of a boundaryless manifold Q into a finite-dimensional
manifold M with finrank 𝕜 F + k = finrank 𝕜 E, the canonical inclusion conormalInclusion is a
C^n smooth embedding of TotalSpace (Fin k → 𝕜) (fun q ↦ conormalSpace J I i q) into
CotangentBundle I M. The ambient manifold M need not be boundaryless.