Changing the coordinates of a bundle homomorphism #
ContinuousLinearMap.inCoordinates_eq_coordChangeL_comp changes both preferred
trivializations used to read a continuous semilinear map between vector-bundle fibres.
The source and target bundles may have different bases. This formula permits regularity
proved in coordinates centred at a point to be transported to fixed trivializations.
The corresponding range-transport theorem identifies the subspaces in different
charts, as required for quotient-bundle coordinate changes.
ContinuousLinearMap.inCoordinates_inverse reads the inverse of a fibre map in coordinates
as the inverse of its coordinate expression, which reduces smoothness of fibrewise inverses
to smoothness of inversion of continuous linear maps.
ContinuousLinearMap.inCoordinates_eq_conjContinuousAlgEquiv reads an endomorphism of a fibre
in coordinates as its conjugate by the fibre equivalence of the trivialization, an algebra
isomorphism, so that coordinate expressions of algebraic expressions in fibre endomorphisms are
the same algebraic expressions in their coordinate expressions.
ContinuousLinearMap.isInvertible_inCoordinates_iff reads invertibility of a fibre map
off its coordinate expression, ContinuousLinearMap.inCoordinates_comp reads a composite
of fibre maps as the composite of their coordinate expressions, and
ContinuousLinearMap.inCoordinates_id and ContinuousLinearMap.inCoordinates_smul read the
identity map and scalar multiples in a compatible target vector-bundle structure, and
ContinuousLinearMap.inCoordinates_finset_sum reads finite sums of fibre maps.
ContinuousLinearMap.mem_ker_inCoordinates_iff, ContinuousLinearMap.mem_range_inCoordinates_iff
and ContinuousLinearMap.finrank_range_inCoordinates read the kernel, the range and the rank of
a fibre map off its coordinate expression, and ContinuousLinearMap.range_inCoordinates
identifies the coordinate range with the trivialized range.
VectorBundleCore.localTriv_coordChangeL and
VectorBundleCore.trivializationAt_coordChangeL identify transitions between actual
trivializations with their core coordinate-change maps, and
VectorBundleCore.coordChange_self_eq_id states the self-transition as an operator identity.
The fibre instances VectorBundleCore.isTopologicalAddGroupFiber and
VectorBundleCore.continuousSMulFiber make Mathlib's Hom bundle between two cores available.
VectorBundleCore.inChartCoordinates expresses a fibre map between two cores in an arbitrary
pair of source and target charts, not only the preferred charts of base points, and
VectorBundleCore.inChartCoordinates_comp composes these expressions through any intermediate
chart containing the base point.
On the common domain of the two charts, VectorBundleCore.inChartCoordinates_eq_localTriv_comp
reads the chart expression through the local trivializations of the two cores.
The construction follows Mathlib's ContinuousLinearMap.inCoordinates and
Bundle.Trivialization.comp_continuousLinearEquivAt_eq_coord_change.
A transition between core trivializations is the core coordinate-change map.
Preferred core trivializations use their selected core coordinate-change maps.
The transition from a chart to itself is the identity operator; the operator form of
VectorBundleCore.coordChange_self.
The fibres of a vector bundle core are topological additive groups, as is the model fibre. This makes the Hom bundle between two cores available.
Scalar multiplication on the fibres of a vector bundle core is continuous.
The expression of a fibre map ϕ over x in the source chart i and the target chart
j. Unlike ContinuousLinearMap.inCoordinates, the charts need not be preferred charts of
base points.
Instances For
The chart expression of a fibre map is its composite with the transitions from the source chart and to the target chart.
On the common domain of a source chart and a target chart, reading a fibre map through the local trivializations of those charts gives its chart expression.
In the preferred charts the coordinate expression of a fibre map is the map itself.
Coordinate expressions of a composite compose through any intermediate chart containing the base point.
Changing the source and target trivializations pre- and post-composes the coordinate operator with the corresponding bundle transitions. All four trivializations must contain their respective fibre base points.
Changing tangent or bundle coordinates transports an operator range by the target coordinate change. The source coordinate change is surjective and leaves the range unchanged.
In a preferred trivialization whose base set contains x, the identity on V x reads as the
identity on the model fibre F.
inCoordinates commutes with scalar multiplication by any c : 𝕜'' from a compatible
VectorBundle 𝕜'' F' W structure. Both sides vanish when y is outside the base set of the
target trivialization.
The inverse of a continuous linear map between fibres reads as the inverse of its coordinate
expression. No invertibility is assumed: both sides vanish when the map is not invertible, and
also when x or y lies outside the base set of the respective trivialization.
In trivializations whose base sets contain the two fibre base points, a continuous linear map between fibres is invertible exactly when its coordinate expression is.
In a preferred trivialization whose base set contains x, reading an endomorphism of V x
in coordinates is conjugation by the fibre equivalence of the trivialization, an algebra
isomorphism (V x →L[𝕜] V x) ≃A[𝕜] (F →L[𝕜] F).
In trivializations whose base sets contain the two fibre base points, a model vector lies in the kernel of the coordinate expression of a fibre map exactly when the corresponding fibre vector lies in the kernel of the map.
In trivializations whose base sets contain the two fibre base points, a model vector lies in the range of the coordinate expression of a fibre map exactly when the corresponding fibre vector lies in the range of the map.
In trivializations whose base sets contain the two fibre base points, the range of the coordinate expression of a fibre map is the image of its range under the trivialization of the target bundle at the target base point.
In trivializations whose base sets contain the two fibre base points, the coordinate expression of a fibre map has the rank of the map.
The coordinate expression of a composite is the composite of the coordinate expressions, provided the trivialization of the middle bundle contains the middle fibre base point.
The coordinate expression of a finite sum of fibre maps is the sum of their coordinate expressions.