Tangent bundles #
This file defines the tangent bundle as a smooth vector bundle.
Let M
be a smooth manifold with corners with model I
on (E, H)
. We define the tangent bundle
of M
using the VectorBundleCore
construction indexed by the charts of M
with fibers E
.
Given two charts i, j : PartialHomeomorph M H
, the coordinate change between i
and j
at a point x : M
is the derivative of the composite
I.symm i.symm j I
E -----> H -----> M --> H --> E
within the set range I ⊆ E
at I (i x) : E
.
This defines a smooth vector bundle TangentBundle
with fibers TangentSpace
.
Main definitions #
TangentSpace I M x
is the fiber of the tangent bundle atx : M
, which is defined to beE
.TangentBundle I M
is the total space ofTangentSpace I M
, proven to be a smooth vector bundle.
Auxiliary lemma for tangent spaces: the derivative of a coordinate change between two charts is smooth on its source.
Let M
be a smooth manifold with corners with model I
on (E, H)
.
Then VectorBundleCore I M
is the vector bundle core for the tangent bundle over M
.
It is indexed by the atlas of M
, with fiber E
and its change of coordinates from the chart i
to the chart j
at point x : M
is the derivative of the composite
I.symm i.symm j I
E -----> H -----> M --> H --> E
within the set range I ⊆ E
at I (i x) : E
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
In a manifold M
, given two preferred charts indexed by x y : M
, tangentCoordChange I x y
is the family of derivatives of the corresponding change-of-coordinates map. It takes junk values
outside the intersection of the sources of the two charts.
Note that this definition takes advantage of the fact that tangentBundleCore
has the same base
sets as the preferred charts of the base manifold.
Equations
- tangentCoordChange I x y = (tangentBundleCore I M).coordChange (achart H x) (achart H y)
Instances For
The tangent space at a point of the manifold M
. It is just E
. We could use instead
(tangentBundleCore I M).to_topological_vector_bundle_core.fiber x
, but we use E
to help the
kernel.
Equations
- TangentSpace I _x = E
Instances For
Equations
Equations
Equations
- ⋯ = ⋯
The tangent bundle to a smooth manifold, as a Sigma type. Defined in terms of
Bundle.TotalSpace
to be able to put a suitable topology on it.
Equations
- TangentBundle I M = Bundle.TotalSpace E (TangentSpace I)
Instances For
Equations
- instModuleTangentSpace I x = inferInstanceAs (Module 𝕜 E)
Equations
- instInhabitedTangentSpace I x = { default := 0 }
Equations
- instTopologicalSpaceTangentBundle I M = (tangentBundleCore I M).toTopologicalSpace
Equations
- TangentSpace.fiberBundle I M = (tangentBundleCore I M).fiberBundle
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The tangent bundle to the model space #
In the tangent bundle to the model space, the charts are just the canonical identification
between a product type and a sigma type, a.k.a. TotalSpace.toProd
.
The canonical identification between the tangent bundle to the model space and the product, as a homeomorphism
Equations
- tangentBundleModelSpaceHomeomorph H I = { toEquiv := Bundle.TotalSpace.toProd H E, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
The map in_coordinates
for the tangent bundle is trivial on the model spaces
When ϕ x
is a continuous linear map that changes vectors in charts around f x
to vectors
in charts around g x
, inTangentCoordinates I I' f g ϕ x₀ x
is a coordinate change of
this continuous linear map that makes sense from charts around f x₀
to charts around g x₀
by composing it with appropriate coordinate changes.
Note that the type of ϕ
is more accurately
Π x : N, TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)
.
We are unfolding TangentSpace
in this type so that Lean recognizes that the type of ϕ
doesn't
actually depend on f
or g
.
This is the underlying function of the trivializations of the hom of (pullbacks of) tangent spaces.
Equations
- inTangentCoordinates I I' f g ϕ x₀ x = ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (f x₀) (f x) (g x₀) (g x) (ϕ x)
Instances For
Equations
- ⋯ = ⋯