Continuous sections of vector bundles and partitions of unity #
This file develops the arithmetic of continuous sections of a topological vector bundle and uses it to glue local sections along a partition of unity.
A section s : Π x, E x is continuous when x ↦ TotalSpace.mk' F x (s x) is continuous.
Over the base set of a trivialization e, this is equivalent to continuity of the coordinate
function x ↦ (e ⟨x, s x⟩).2 (Bundle.Trivialization.continuousAt_section_iff and
Bundle.Trivialization.continuousOn_section_iff), with no atlas or linearity assumption on e.
Sums, finite sums, scalar multiples by continuous functions and locally finite sums of continuous
sections are continuous (ContinuousAt.add_section, ContinuousAt.smul_section,
ContinuousAt.sum_section, Continuous.finsum_section_of_locallyFinite; for global scalar
multiples use Continuous.smul_totalSpace), and a function with
closed support inside an open set multiplies a section continuous on that set into a globally
continuous section (ContinuousOn.smul_section_of_tsupport).
A linear trivialization reconstructs a section from arbitrary model coordinates by
Bundle.Trivialization.sectionFromCoordinates, with the two coordinate inverse laws on its base
set. This construction is purely topological and requires no manifold structure.
The main result, TauCeti.exists_continuous_section_forall_mem_convex_of_local, is the bundle form
of exists_continuous_forall_mem_convex_of_local: over a normal paracompact base, if convex
fibrewise conditions can be met by sections that are continuous near each point, then they are met
by a single global continuous section. This is how continuous fibre metrics, and other
fibrewise-convex structures on bundles over paracompact bases, are constructed.
The statements and proofs are the continuous counterparts of Mathlib's smooth section API
ContMDiffWithinAt.add_section, ContMDiffOn.smul_section_of_tsupport and
exists_contMDiffSection_forall_mem_convex_of_local.
Within the base set of a trivialization e, a section is continuous at a point within a set
exactly when its coordinate function read in e is.
Within the base set of a trivialization e, a section is continuous at a point exactly when
its coordinate function read in e is.
On a subset of the base set of a trivialization e, a section is continuous exactly when its
coordinate function read in e is.
The sum of two sections continuous at a point within a set is continuous there.
The sum of two sections continuous at a point is continuous there.
The sum of two sections continuous on a set is continuous on it.
The sum of two continuous sections is continuous.
The product of a scalar function and a section, both continuous at a point within a set, is continuous there.
The product of a scalar function and a section, both continuous at a point, is continuous there.
The product of a scalar function and a section, both continuous on a set, is continuous on it.
The product f • s of a continuous scalar function f and a section s is continuous as soon
as s is continuous on an open set containing the closed support of f. This is the vector
bundle analogue of continuous_of_tsupport.
A finite sum of sections continuous at a point is continuous there.
The sum of a locally finite family of continuous sections is continuous.
The section with constant coordinates v in a linear trivialization e is continuous on the
base set of e.
Let E be a real vector bundle over a normal paracompact space and t x ⊆ E x a family of
convex sets. If near each point some section, continuous there, lies in t, then a single
continuous global section lies in t everywhere. This is the vector bundle version of
exists_continuous_forall_mem_convex_of_local.
Reconstruct a section from its model coordinates in a chosen frame.
Instances For
Evaluate the reconstructed section through the native inverse frame map.
Reading the reconstructed section in the same frame recovers the model field.
Reconstructing the coordinates of a section recovers it on the frame domain.