Local frames in a vector bundle #

Let V → M be a finite rank smooth vector bundle with standard fiber F. A family of sections s i of V → M is called a C^k local frame on a set U ⊆ M iff each section s i is C^k on U, and the section values s i x form a basis for each x ∈ U. We define a predicate IsLocalFrame for a collection of sections to be a local frame on a set, and define basic notions (such as the coefficients of a section w.r.t. a local frame, and checking the smoothness of t via its coefficients in a local frame).

Given a basis b for F and a local trivialisation e for V, we construct a smooth local frame on V w.r.t. e and b, i.e. a collection of sections sᵢ of V which is smooth on e.baseSet such that {sᵢ x} is a basis of V x for each x ∈ e.baseSet. Any section s of e can be uniquely written as s = ∑ i, f^i sᵢ near x, and s is smooth at x iff the functions f^i are.

In this file, we prove the latter statement for finite-rank bundles (with coefficients in a complete field). In Mathlib/Geometry/Manifold/VectorBundle/OrthonormalFrame.lean (#26221), we will prove the same for real vector bundles of any rank which admit a C^n bundle metric. This includes bundles of finite rank, modelled on a Hilbert space or on a Banach space which has smooth partitions of unity.

We will use this to construct local extensions of a vector to a section which is smooth on the trivialisation domain.

Main definitions and results #

IsLocalFrameOn: a family of sections s i of V → M is called a C^k local frame on a set U ⊆ M iff each section s i is C^k on U, and the section values s i x form a basis for each x ∈ U

Suppose {sᵢ} is a local frame on U, and hs : IsLocalFrameOn s U.

IsLocalFrameOn.toBasisAt hs: for each x ∈ U, the vectors sᵢ x form a basis of F
IsLocalFrameOn.coeff hs describes the coefficient of sections of V w.r.t. {sᵢ}. hs.coeff i is a linear map from sections of V to functions M → 𝕜.
IsLocalFrameOn.eventually_eq_sum_coeff_smul hs: for a local frame {sᵢ} near x, for each section t we have t = ∑ i, (hs.coeff i t) • sᵢ.
IsLocalFrameOn.coeff_sum_eq hs t hx proves that t x = ∑ i, (hs.coeff i t) x • sᵢ x, provided that hx : x ∈ U.
IsLocalFrameOn.coeff_congr hs: the coefficient hs.coeff i of t in the local frame {sᵢ} only depends on t at x.
IsLocalFrameOn.eq_iff_coeff hs: two sections t and t' are equal at x if and only if their coefficients at x w.r.t. {sᵢ} agree.
IsLocalFrameOn.contMDiffOn_of_coeff hs: a section t is C^k on U if each coefficient hs.coeff i t is C^k on U
IsLocalFrameOn.contMDiffAt_of_coeff hs: a section t is C^k at x ∈ U if all of its frame coefficients are
IsLocalFrameOn.contMDiffOn_off_coeff hs: a section t is C^k on an open set t ⊆ U ff all of its frame coefficients are
MDifferentiable versions of the previous three statements

In the following lemmas, let e be a compatible local trivialisation of V, and b a basis of the model fiber F.

Trivialization.basisAt e b: for each x ∈ e.baseSet, return the basis of V x induced by e and b
e.localFrame b: the local frame on V induced by e and b. Use e.localFrame b i to access the i-th section in that frame.
e.contMDiffOn_localFrame_baseSet: each section e.localFrame b i is smooth on e.baseSet

TODO #

Strengthen the proof of smoothness in terms of the local frame coefficients.

IsLocalFrameOn.contMDiffOn_coeff hs: if t is a C^k section, each coefficient hs.coeff i t is C^k on U
IsLocalFrameOn.contMDiffAt_iff_coeff hs: a section t is C^k at x ∈ U iff all of its frame coefficients are
IsLocalFrameOn.contMDiffOn_iff_coeff hs: a section t is C^k on an open set t ⊆ U iff all of its frame coefficients are
a MDifferentiable version of each of these

Implementation notes #

Local frames use the junk value pattern: they are defined on all of M, but their value is only meaningful on the set on which they are a local frame.

Tags #

vector bundle, local frame, smoothness