# mathlibdocumentation

geometry.manifold.basic_smooth_bundle

# Basic smooth bundles #

In general, a smooth bundle is a bundle over a smooth manifold, whose fiber is a manifold, and for which the coordinate changes are smooth. In this definition, there are charts involved at several places: in the manifold structure of the base, in the manifold structure of the fibers, and in the local trivializations. This makes it a complicated object in general. There is however a specific situation where things are much simpler: when the fiber is a vector space (no need for charts for the fibers), and when the local trivializations of the bundle and the charts of the base coincide. Then everything is expressed in terms of the charts of the base, making for a much simpler overall structure, which is easier to manipulate formally.

Most vector bundles that naturally occur in differential geometry are of this form: the tangent bundle, the cotangent bundle, differential forms (used to define de Rham cohomology) and the bundle of Riemannian metrics. Therefore, it is worth defining a specific constructor for this kind of bundle, that we call basic smooth bundles.

A basic smooth bundle is thus a smooth bundle over a smooth manifold whose fiber is a vector space, and which is trivial in the coordinate charts of the base. (We recall that in our notion of manifold there is a distinguished atlas, which does not need to be maximal: we require the triviality above this specific atlas). It can be constructed from a basic smooth bundled core, defined below, specifying the changes in the fiber when one goes from one coordinate chart to another one. We do not require that this changes in fiber are linear, but only diffeomorphisms.

## Main definitions #

• basic_smooth_bundle_core I M F: assuming that M is a smooth manifold over the model with corners I on (𝕜, E, H), and F is a normed vector space over 𝕜, this structure registers, for each pair of charts of M, a smooth change of coordinates on F. This is the core structure from which one will build a smooth bundle with fiber F over M.

Let Z be a basic smooth bundle core over M with fiber F. We define Z.to_topological_fiber_bundle_core, the (topological) fiber bundle core associated to Z. From it, we get a space Z.to_topological_fiber_bundle_core.total_space (which as a Type is just Σ (x : M), F), with the fiber bundle topology. It inherits a manifold structure (where the charts are in bijection with the charts of the basis). We show that this manifold is smooth.

Then we use this machinery to construct the tangent bundle of a smooth manifold.

• tangent_bundle_core I M: the basic smooth bundle core associated to a smooth manifold M over a model with corners I.
• tangent_bundle I M : the total space of tangent_bundle_core I M. It is itself a smooth manifold over the model with corners I.tangent, the product of I and the trivial model with corners on E.
• tangent_space I x : the tangent space to M at x
• tangent_bundle.proj I M: the projection from the tangent bundle to the base manifold

## Implementation notes #

In the definition of a basic smooth bundle core, we do not require that the coordinate changes of the fibers are linear map, only that they are diffeomorphisms. Therefore, the fibers of the resulting fiber bundle do not inherit a vector space structure (as an algebraic object) in general. As the fiber, as a type, is just F, one can still always register the vector space structure, but it does not make sense to do so (i.e., it will not lead to any useful theorem) unless this structure is canonical, i.e., the coordinate changes are linear maps.

For instance, we register the vector space structure on the fibers of the tangent bundle. However, we do not register the normed space structure coming from that of F (as it is not canonical, and we also want to keep the possibility to add a Riemannian structure on the manifold later on without having two competing normed space instances on the tangent spaces).

We require F to be a normed space, and not just a topological vector space, as we want to talk about smooth functions on F. The notion of derivative requires a norm to be defined.

## TODO #

construct the cotangent bundle, and the bundles of differential forms. They should follow functorially from the description of the tangent bundle as a basic smooth bundle.

## Tags #

Smooth fiber bundle, vector bundle, tangent space, tangent bundle

structure basic_smooth_bundle_core {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (M : Type u_4) [ M] (F : Type u_5) [normed_group F] [ F] :
Type (max u_3 u_4 u_5)

Core structure used to create a smooth bundle above M (a manifold over the model with corner I) with fiber the normed vector space F over 𝕜, which is trivial in the chart domains of M. This structure registers the changes in the fibers when one changes coordinate charts in the base. We do not require the change of coordinates of the fibers to be linear, only smooth. Therefore, the fibers of the resulting bundle will not inherit a canonical vector space structure in general.

def trivial_basic_smooth_bundle_core {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (M : Type u_4) [ M] (F : Type u_5) [normed_group F] [ F] :

The trivial basic smooth bundle core, in which all the changes of coordinates are the identity.

Equations
@[instance]
def basic_smooth_bundle_core.inhabited {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] :
Equations
def basic_smooth_bundle_core.to_topological_fiber_bundle_core {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] (Z : F) :
F

Fiber bundle core associated to a basic smooth bundle core

Equations
@[simp]
theorem basic_smooth_bundle_core.base_set {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] (Z : F) (i : (atlas H M)) :
def basic_smooth_bundle_core.chart {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] (Z : F) {e : H} (he : e M) :

Local chart for the total space of a basic smooth bundle

Equations
@[simp]
theorem basic_smooth_bundle_core.chart_source {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] (Z : F) (e : H) (he : e M) :
@[simp]
theorem basic_smooth_bundle_core.chart_target {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] (Z : F) (e : H) (he : e M) :
@[instance]
def basic_smooth_bundle_core.to_charted_space {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] (Z : F) :

The total space of a basic smooth bundle is endowed with a charted space structure, where the charts are in bijection with the charts of the basis.

Equations
theorem basic_smooth_bundle_core.mem_atlas_iff {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] (Z : F)  :
∃ (e : H) (he : e M), f = Z.chart he
@[simp]
theorem basic_smooth_bundle_core.mem_chart_source_iff {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] (Z : F) (p q : Z.to_topological_fiber_bundle_core.total_space) :
@[simp]
theorem basic_smooth_bundle_core.mem_chart_target_iff {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] (Z : F) (p : H × F)  :
@[simp]
theorem basic_smooth_bundle_core.coe_chart_at_fst {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] (Z : F) (p q : Z.to_topological_fiber_bundle_core.total_space) :
((chart_at F) q) p).fst = (chart_at H q.fst) p.fst
@[simp]
theorem basic_smooth_bundle_core.coe_chart_at_symm_fst {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] (Z : F) (p : H × F)  :
(((chart_at F) q).symm) p).fst = ((chart_at H q.fst).symm) p.fst
@[instance]
def basic_smooth_bundle_core.to_smooth_manifold {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {F : Type u_5} [normed_group F] [ F] (Z : F) :

Smooth manifold structure on the total space of a basic smooth bundle

def tangent_bundle_core {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (M : Type u_4) [ M]  :

Basic smooth bundle core version of the tangent bundle of a smooth manifold M modelled over a model with corners I on (E, H). The fibers are equal to E, and the coordinate change in the fiber corresponds to the derivative of the coordinate change in M.

Equations
@[nolint]
def tangent_space {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] (x : M) :
Type u_2

The tangent space at a point of the manifold M. It is just E. We could use instead (tangent_bundle_core I M).to_topological_fiber_bundle_core.fiber x, but we use E to help the kernel.

Equations
• = E
@[nolint]
def tangent_bundle {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (M : Type u_4) [ M]  :
Type (max u_4 u_2)

The tangent bundle to a smooth manifold, as a plain type. We could use (tangent_bundle_core I M).to_topological_fiber_bundle_core.total_space, but instead we use the (definitionally equal) Σ (x : M), tangent_space I x, to make sure that rcasing an element of the tangent bundle gives a second component in the tangent space.

Equations
• = Σ (x : M),
def tangent_bundle.proj {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (M : Type u_4) [ M]  :
→ M

The projection from the tangent bundle of a smooth manifold to the manifold. As the tangent bundle is represented internally as a sigma type, the notation p.1 also works for the projection of the point p.

Equations
• = λ (p : M), p.fst
@[simp]
theorem tangent_bundle.proj_apply {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] (x : M) (v : x) :
x, v⟩ = x
@[instance]
def tangent_bundle.topological_space {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (M : Type u_4) [ M]  :
Equations
@[instance]
def tangent_bundle.charted_space {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (M : Type u_4) [ M]  :
Equations
@[instance]
def tangent_bundle.smooth_manifold_with_corners {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (M : Type u_4) [ M]  :
@[instance]
def tangent_space.has_continuous_smul {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] (x : M) :
x)
@[instance]
def tangent_space.topological_space {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] (x : M) :
Equations
@[instance]
def tangent_space.add_comm_group {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] (x : M) :
Equations
@[instance]
def tangent_space.topological_add_group {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] (x : M) :
@[instance]
def tangent_space.module {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] (x : M) :
x)
Equations
@[instance]
def tangent_space.inhabited {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] (x : M) :
Equations
theorem tangent_bundle_proj_continuous {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (M : Type u_4) [ M]  :

The tangent bundle projection on the basis is a continuous map.

theorem tangent_bundle_proj_open {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (M : Type u_4) [ M]  :

The tangent bundle projection on the basis is an open map.

@[simp]
theorem tangent_bundle_model_space_chart_at {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (p : H) :

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. equiv.sigma_equiv_prod.

@[simp]
theorem tangent_bundle_model_space_coe_chart_at {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (p : H) :
@[simp]
theorem tangent_bundle_model_space_coe_chart_at_symm {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_3} (I : H) (p : H) :
((chart_at E) p).symm) = E).symm)
def tangent_bundle_model_space_homeomorph {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] (H : Type u_3) (I : H) :

The canonical identification between the tangent bundle to the model space and the product, as a homeomorphism

Equations
@[simp]
theorem tangent_bundle_model_space_homeomorph_coe {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] (H : Type u_3) (I : H) :
@[simp]
theorem tangent_bundle_model_space_homeomorph_coe_symm {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] (H : Type u_3) (I : H) :
= E).symm)