The projection of a fibre bundle is a submersion

For a fibre bundle V with model fibre F over a manifold B modelled on IB, the total space carries the charts (trivializationAt F V b) ≫ (chartAt HB b × id), modelled on IB.prod 𝓘(𝕜, F). In such a chart and the chart chartAt HB b of the base, the bundle projection is the first projection (u, v) ↦ u. Hence the projection is a submersion in the sense of Manifold.IsSubmersion, with the model fibre F as a complement. Smoothness of the projection, Mathlib's Bundle.contMDiff_proj, is recovered from this by Manifold.IsSubmersion.contMDiff.

The same chart computation identifies the derivative of the projection: composed with the derivative of the inverse of a preferred chart of the total space, it is the derivative of the inverse base chart applied to the first coordinate (Bundle.mfderiv_proj_comp_mfderivWithin_extChartAt_symm). This is how forms built from the derivative of the projection, such as the Liouville form of a cotangent bundle, are computed in charts. In particular the derivative of the projection is surjective at every point (Bundle.mfderiv_proj_surjective). A self-map of the total space covering the identity of the base commutes with the derivative of the projection (Bundle.mfderiv_proj_comp_mfderiv_of_proj_eq), and the derivative of a section is a right inverse of the derivative of the projection, hence injective (Bundle.mfderiv_injective_of_proj_comp_eq_id).

No linear structure on the fibres is used, and the regularity order n is arbitrary.

theorem Bundle.fst_mem_extChartAt_target {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {EB : Type u_4} {HB : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] (p : TotalSpace F V) {y : EB × F} (hy : y ∈ (extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) p).target) : y.1 ∈ (extChartAt IB p.proj).target

A point of the target of a preferred chart of the total space has its first coordinate in the target of the corresponding chart of the base.

theorem Bundle.proj_extChartAt_symm {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {EB : Type u_4} {HB : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] (p : TotalSpace F V) {y : EB × F} (hy : y ∈ (extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) p).target) : (↑(extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) p).symm y).proj = ↑(extChartAt IB p.proj).symm y.1

Read through the inverse of a preferred chart of the total space, the bundle projection is the inverse of the base chart applied to the first coordinate.

theorem Bundle.isSubmersionOfComplement_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {EB : Type u_4} {HB : Type u_5} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] [IsManifold IB n B] [IsManifold (IB.prod (modelWithCornersSelf 𝕜 F)) n (TotalSpace F V)] : Manifold.IsSubmersionOfComplement F (IB.prod (modelWithCornersSelf 𝕜 F)) IB n TotalSpace.proj

The projection of a fibre bundle is a submersion, with the model fibre as complement: in the preferred charts of the total space and of the base, it is the first projection.

theorem Bundle.isSubmersion_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {EB : Type u_4} {HB : Type u_5} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] [IsManifold IB n B] [IsManifold (IB.prod (modelWithCornersSelf 𝕜 F)) n (TotalSpace F V)] : Manifold.IsSubmersion (IB.prod (modelWithCornersSelf 𝕜 F)) IB n TotalSpace.proj

The projection of a fibre bundle is a submersion.

theorem Bundle.mfderiv_proj_comp_mfderivWithin_extChartAt_symm {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {EB : Type u_4} {HB : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] [IsManifold IB 1 B] [IsManifold (IB.prod (modelWithCornersSelf 𝕜 F)) 1 (TotalSpace F V)] (p : TotalSpace F V) {y : EB × F} (hy : y ∈ (extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) p).target) : mfderiv% TotalSpace.proj (↑(extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) p).symm y) ∘SL mfderiv[Set.range ↑(IB.prod (modelWithCornersSelf 𝕜 F))] ↑(extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) p).symm y = mfderiv[Set.range ↑IB] ↑(extChartAt IB p.proj).symm y.1 ∘SL ContinuousLinearMap.fst 𝕜 EB F

The derivative of the bundle projection in a preferred chart. Composed with the derivative of the inverse of a preferred chart of the total space, the derivative of the projection is the derivative of the inverse base chart applied to the first coordinate.

theorem Bundle.mfderiv_proj {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {EB : Type u_4} {HB : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] [IsManifold IB 1 B] [IsManifold (IB.prod (modelWithCornersSelf 𝕜 F)) 1 (TotalSpace F V)] (p : TotalSpace F V) : mfderiv% TotalSpace.proj p = ContinuousLinearMap.fst 𝕜 EB F

The derivative of the bundle projection is the first projection. Tangent vectors at a point p of the total space are read in the preferred chart at p, as pairs of a base and a fibre coordinate, and tangent vectors of the base in the chart at p.proj; in these coordinates the derivative of the projection keeps the base coordinate.

theorem Bundle.mfderiv_proj_surjective {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {EB : Type u_4} {HB : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] [IsManifold IB 1 B] [IsManifold (IB.prod (modelWithCornersSelf 𝕜 F)) 1 (TotalSpace F V)] (p : TotalSpace F V) : Function.Surjective ⇑(mfderiv% TotalSpace.proj p)

The derivative of the projection of a fibre bundle is surjective at every point of the total space: every tangent vector of the base lifts to a tangent vector of the total space.

theorem Bundle.mfderiv_proj_comp_mfderiv_of_proj_eq {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {EB : Type u_4} {HB : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] {g : TotalSpace F V → TotalSpace F V} {z : TotalSpace F V} (hg : MDiffAt g z) (hproj : ∀ (p : TotalSpace F V), (g p).proj = p.proj) : mfderiv% TotalSpace.proj (g z) ∘SL mfderiv% g z = mfderiv% TotalSpace.proj z

A self-map g of the total space covering the identity of the base commutes with the derivative of the projection: dπ_{g z} ∘ dg_z = dπ_z.

theorem Bundle.mfderiv_proj_comp_mfderiv_of_proj_comp_eq_id {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {EB : Type u_4} {HB : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] {s : B → TotalSpace F V} {b : B} (hs : MDiffAt s b) (hπs : TotalSpace.proj ∘ s = id) : mfderiv% TotalSpace.proj (s b) ∘SL mfderiv% s b = ContinuousLinearMap.id 𝕜 (TangentSpace IB b)

The derivative of a section s of the bundle (π ∘ s = id) is a right inverse of the derivative of the projection: dπ_{s b} ∘ ds_b = id.

theorem Bundle.mfderiv_injective_of_proj_comp_eq_id {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {EB : Type u_4} {HB : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] {s : B → TotalSpace F V} {b : B} (hs : MDiffAt s b) (hπs : TotalSpace.proj ∘ s = id) : Function.Injective ⇑(mfderiv% s b)

A section s of the bundle (π ∘ s = id) has injective derivative at every point where it is differentiable.