Documentation

TauCeti.Geometry.Manifold.VectorBundle.Cotangent.Prod

The cotangent bundle of a product #

The cotangent bundle of a product manifold is the product of the cotangent bundles:

T*(M × N) ≃ T*M × T*N

(TauCeti.CotangentBundle.prodDiffeomorph). A covector p at (x, y) goes to its restrictions to the two factors, the covectors p ∘ dι₁ at x and p ∘ dι₂ at y, where ι₁ = (·, y) and ι₂ = (x, ·) are the inclusions of the slices through (x, y). Conversely, covectors a at x and b at y go to a ∘ d pr₁ + b ∘ d pr₂ at (x, y). Both directions are stated through differentials of the product maps, so they do not depend on how the tangent spaces of a product are implemented.

The identification is a smooth diffeomorphism. Smoothness of the restriction map is the smoothness of pulling covectors back along a family of maps, TauCeti.CotangentBundle.contMDiffAt_mk_comp_mfderiv_uncurry, since the slice inclusion ι₁ depends on the point y of the second factor. The comparison of the Liouville and canonical symplectic forms of T*(M × N) with those of the factors is in TauCeti.Geometry.Symplectic.Cotangent.Bundle.Prod.

References #

source
noncomputable def TauCeti.CotangentBundle.prodDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_5} [TopologicalSpace H'] (J : ModelWithCorners 𝕜 F H') (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_7) [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] :
Diffeomorph ((I.prod J).prod (modelWithCornersSelf 𝕜 (E × F →L[𝕜] 𝕜))) ((I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] 𝕜))).prod (J.prod (modelWithCornersSelf 𝕜 (F →L[𝕜] 𝕜)))) (CotangentBundle (I.prod J) (M × N)) (CotangentBundle I M × CotangentBundle J N) ↑⊤

The cotangent bundle of a product is the product of the cotangent bundles. The smooth diffeomorphism T*(M × N) ≃ T*M × T*N restricting a covector p at (x, y) to the covectors p ∘ dι₁ at x and p ∘ dι₂ at y, for the slice inclusions ι₁ = (·, y) and ι₂ = (x, ·). Its inverse sends covectors a at x and b at y to a ∘ d pr₁ + b ∘ d pr₂.

Instances For
    source
    @[simp]
    theorem TauCeti.CotangentBundle.proj_prodDiffeomorph_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (z : CotangentBundle (I.prod J) (M × N)) :
    ((prodDiffeomorph I J M N) z).1.proj = z.proj.1

    The first component of prodDiffeomorph z lies over the first component of the base point of z.

    source
    @[simp]
    theorem TauCeti.CotangentBundle.proj_prodDiffeomorph_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (z : CotangentBundle (I.prod J) (M × N)) :
    ((prodDiffeomorph I J M N) z).2.proj = z.proj.2

    The second component of prodDiffeomorph z lies over the second component of the base point of z.

    source
    theorem TauCeti.CotangentBundle.prodDiffeomorph_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (z : CotangentBundle (I.prod J) (M × N)) :
    ((prodDiffeomorph I J M N) z).1 = ⟨z.proj.1, z.snd ∘SL (mfderiv% fun (x : M) => (x, z.proj.2)) z.proj.1⟩

    The first component of prodDiffeomorph z is the restriction of z along the horizontal slice through z.proj.

    source
    theorem TauCeti.CotangentBundle.prodDiffeomorph_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (z : CotangentBundle (I.prod J) (M × N)) :
    ((prodDiffeomorph I J M N) z).2 = ⟨z.proj.2, z.snd ∘SL (mfderiv% fun (y : N) => (z.proj.1, y)) z.proj.2⟩

    The second component of prodDiffeomorph z is the restriction of z along the vertical slice through z.proj.

    source
    @[simp]
    theorem TauCeti.CotangentBundle.prodDiffeomorph_fst_snd_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (z : CotangentBundle (I.prod J) (M × N)) (v : TangentSpace I ((prodDiffeomorph I J M N) z).1.proj) :
    ((prodDiffeomorph I J M N) z).1.snd v = z.snd (((mfderiv% fun (x : M) => (x, z.proj.2)) z.proj.1) v)

    The first component of prodDiffeomorph z evaluates a tangent vector v of M as z evaluates its image under the differential of the slice inclusion x ↦ (x, y).

    source
    @[simp]
    theorem TauCeti.CotangentBundle.prodDiffeomorph_snd_snd_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (z : CotangentBundle (I.prod J) (M × N)) (v : TangentSpace J ((prodDiffeomorph I J M N) z).2.proj) :
    ((prodDiffeomorph I J M N) z).2.snd v = z.snd (((mfderiv% fun (y : N) => (z.proj.1, y)) z.proj.2) v)

    The second component of prodDiffeomorph z evaluates a tangent vector v of N as z evaluates its image under the differential of the slice inclusion y ↦ (x, y).

    source
    @[simp]
    theorem TauCeti.CotangentBundle.proj_prodDiffeomorph_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (w : CotangentBundle I M × CotangentBundle J N) :
    ((prodDiffeomorph I J M N).symm w).proj = (w.1.proj, w.2.proj)

    The inverse of prodDiffeomorph lies over the pair of base points.

    source
    @[simp]
    theorem TauCeti.CotangentBundle.prodDiffeomorph_symm_snd_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (w : CotangentBundle I M × CotangentBundle J N) (v : TangentSpace (I.prod J) ((prodDiffeomorph I J M N).symm w).proj) :
    ((prodDiffeomorph I J M N).symm w).snd v = w.1.snd ((mfderiv% Prod.fst (w.1.proj, w.2.proj)) v) + w.2.snd ((mfderiv% Prod.snd (w.1.proj, w.2.proj)) v)

    The inverse of prodDiffeomorph combines covectors a at x and b at y into the covector a ∘ d pr₁ + b ∘ d pr₂ at (x, y).

    source
    theorem TauCeti.CotangentBundle.snd_apply_eq_prodDiffeomorph_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (z : CotangentBundle (I.prod J) (M × N)) (v : TangentSpace (I.prod J) z.proj) :
    z.snd v = ((prodDiffeomorph I J M N) z).1.snd ((mfderiv% Prod.fst z.proj) v) + ((prodDiffeomorph I J M N) z).2.snd ((mfderiv% Prod.snd z.proj) v)

    prodDiffeomorph preserves the pairing of covectors with tangent vectors: a covector z on M × N evaluates a tangent vector v as the sum of its two restrictions evaluated on the components d pr₁ v and d pr₂ v.

    source
    @[simp]
    theorem TauCeti.CotangentBundle.prodDiffeomorph_zeroSection {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (p : M × N) :
    (prodDiffeomorph I J M N) (Bundle.zeroSection (E × F →L[𝕜] 𝕜) (fun (z : M × N) => TangentSpace (I.prod J) z →L[𝕜] 𝕜) p) = (Bundle.zeroSection (E →L[𝕜] 𝕜) (fun (x : M) => TangentSpace I x →L[𝕜] 𝕜) p.1, Bundle.zeroSection (F →L[𝕜] 𝕜) (fun (y : N) => TangentSpace J y →L[𝕜] 𝕜) p.2)

    prodDiffeomorph sends the zero covector at p = (x, y) to the pair of zero covectors at x and y.

    source
    @[simp]
    theorem TauCeti.CotangentBundle.prodDiffeomorph_symm_zeroSection {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (x : M) (y : N) :
    (prodDiffeomorph I J M N).symm (Bundle.zeroSection (E →L[𝕜] 𝕜) (fun (x : M) => TangentSpace I x →L[𝕜] 𝕜) x, Bundle.zeroSection (F →L[𝕜] 𝕜) (fun (y : N) => TangentSpace J y →L[𝕜] 𝕜) y) = Bundle.zeroSection (E × F →L[𝕜] 𝕜) (fun (z : M × N) => TangentSpace (I.prod J) z →L[𝕜] 𝕜) (x, y)

    The inverse of prodDiffeomorph combines the zero covectors at x and y into the zero covector at (x, y).