Conormal covectors of a map

For a map i : Q → M, the conormal set TauCeti.CotangentBundle.conormal J I i is the set of covectors p ∈ T*_{i q} M annihilating the tangent image di_q (T_q Q), for some q : Q. For an embedded submanifold Q ⊆ M this is the conormal bundle N*Q as a subset of T*M. Its fibre over q is the annihilator TauCeti.CotangentBundle.conormalSpace J I i q of the tangent image; when di_q is injective and M is finite-dimensional it has dimension dim M - dim Q (TauCeti.CotangentBundle.finrank_add_finrank_conormalSpace), so that N*Q has the dimension of M.

A covector is conormal exactly when the cotangent relation of i (TauCeti.CotangentBundle.cotangentRel) relates it to a zero covector of T*Q. Through the composition law of these relations, conormal sets are independent of the parametrization (TauCeti.CotangentBundle.conormal_comp_diffeomorph) and are carried to each other by cotangent lifts of diffeomorphisms (TauCeti.CotangentBundle.image_cotangent_conormal).

The two extreme examples are the conormal set of the identity, which is the zero section (TauCeti.CotangentBundle.conormal_id), and that of a constant map, which is the whole fibre over its value (TauCeti.CotangentBundle.conormal_const).

As for TauCeti.CotangentBundle.cotangentRel, the differential is Mathlib's mfderiv, which is 0 where i is not differentiable.

References

• A. Cannas da Silva, Lectures on Symplectic Geometry, Lecture Notes in Mathematics 1764, Springer, 2001, Section 3.3.
• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Chapter 11.

The conormal fibre

noncomputable def TauCeti.CotangentBundle.conormalSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] (J : ModelWithCorners 𝕜 F H') (I : ModelWithCorners 𝕜 E H) (i : Q → M) (q : Q) : Submodule 𝕜 (TangentSpace I (i q) →L[𝕜] 𝕜)

The conormal space of i : Q → M at q: the covectors at i q which annihilate the tangent image di_q (T_q Q), that is, the polar StrongDual.polarSubmodule of that image.

@[simp]

theorem TauCeti.CotangentBundle.mem_conormalSpace_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] {i : Q → M} {q : Q} {p : TangentSpace I (i q) →L[𝕜] 𝕜} : p ∈ conormalSpace J I i q ↔ p ∘SL mfderiv% i q = 0

A covector at i q is conormal at q when it vanishes on the image of di_q.

theorem TauCeti.CotangentBundle.finrank_add_finrank_conormalSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] {i : Q → M} {q : Q} (hi : Function.Injective ⇑(mfderiv% i q)) : Module.finrank 𝕜 F + Module.finrank 𝕜 ↥(conormalSpace J I i q) = Module.finrank 𝕜 E

The dimension of the conormal space. If M is finite-dimensional and the differential of i at q is injective, then dim Q + dim (conormalSpace J I i q) = dim M.

The conormal set

def TauCeti.CotangentBundle.conormal {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {H' : Type u_7} [TopologicalSpace H'] {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] (J : ModelWithCorners 𝕜 F H') (I : ModelWithCorners 𝕜 E H) (i : Q → M) : Set (CotangentBundle I M)

The conormal set of a map i : Q → M: the covectors of M at points i q which annihilate the tangent image di_q (T_q Q). For an embedded submanifold this is its conormal bundle N*Q ⊆ T*M.

theorem TauCeti.CotangentBundle.mem_conormal_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] {i : Q → M} {w : CotangentBundle I M} : w ∈ conormal J I i ↔ ∃ (q : Q), i q = w.proj ∧ w.snd ∘SL mfderiv% i q = 0

A covector is conormal to i when it lies over some i q and vanishes on the image of di_q.

theorem TauCeti.CotangentBundle.mem_conormal_iff_exists_cotangentRel {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] {i : Q → M} {w : CotangentBundle I M} : w ∈ conormal J I i ↔ ∃ (q : Q), cotangentRel J I i (Bundle.zeroSection (F →L[𝕜] 𝕜) (fun (q : Q) => TangentSpace J q →L[𝕜] 𝕜) q) w

A covector is conormal to i exactly when the cotangent relation of i relates a zero covector of T*Q to it.

theorem TauCeti.CotangentBundle.mk_mem_conormal_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] {i : Q → M} (hi : Function.Injective i) (q : Q) (p : TangentSpace I (i q) →L[𝕜] 𝕜) : ⟨i q, p⟩ ∈ conormal J I i ↔ p ∈ conormalSpace J I i q

For an injective map i, a covector at i q is conormal to i exactly when it lies in the conormal space at q.

theorem TauCeti.CotangentBundle.mk_mem_conormal {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] {i : Q → M} {q : Q} {p : TangentSpace I (i q) →L[𝕜] 𝕜} (hp : p ∈ conormalSpace J I i q) : ⟨i q, p⟩ ∈ conormal J I i

The covectors of the conormal space at q are conormal to i.

@[simp]

theorem TauCeti.CotangentBundle.zeroSection_mem_conormal {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] (i : Q → M) (q : Q) : Bundle.zeroSection (E →L[𝕜] 𝕜) (fun (x : M) => TangentSpace I x →L[𝕜] 𝕜) (i q) ∈ conormal J I i

The zero covector at every point i q is conormal to i.

@[simp]

theorem TauCeti.CotangentBundle.proj_image_conormal {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] (i : Q → M) : Bundle.TotalSpace.proj '' conormal J I i = Set.range i

The conormal set of i lies over the image of i, and covers all of it.

Examples

theorem TauCeti.CotangentBundle.conormal_eq_range_zeroSection {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] {i : Q → M} (hi : Function.Surjective i) (hdi : ∀ (q : Q), Function.Surjective ⇑(mfderiv% i q)) : conormal J I i = Set.range (Bundle.zeroSection (E →L[𝕜] 𝕜) fun (x : M) => TangentSpace I x →L[𝕜] 𝕜)

The conormal set of a submersive surjection is the zero section. If i is surjective with surjective differentials, then only zero covectors annihilate its tangent images.

@[simp]

theorem TauCeti.CotangentBundle.conormal_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_6} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] : conormal I I id = Set.range (Bundle.zeroSection (E →L[𝕜] 𝕜) fun (x : M) => TangentSpace I x →L[𝕜] 𝕜)

The conormal set of M itself is the zero section.

@[simp]

theorem TauCeti.CotangentBundle.conormal_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] (J : ModelWithCorners 𝕜 F H') {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] [Nonempty Q] (y : M) : (conormal J I fun (x : Q) => y) = Bundle.TotalSpace.proj ⁻¹' {y}

The conormal set of a point is its whole cotangent fibre. A constant map from a nonempty source has zero differential, so every covector over its value is conormal.

Reparametrization and transport

theorem TauCeti.CotangentBundle.conormal_comp_of_surjective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {H'' : Type u_8} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 G H''} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] {P : Type u_12} [TopologicalSpace P] [ChartedSpace H'' P] {g : P → Q} {i : Q → M} (hg : MDiff g) (hi : MDiff i) (hsurj : Function.Surjective g) (hdg : ∀ (p : P), Function.Surjective ⇑(mfderiv% g p)) : conormal K I (i ∘ g) = conormal J I i

Precomposing i : Q → M with a differentiable surjection g : P → Q whose differentials are surjective does not change its conormal set.

theorem TauCeti.CotangentBundle.conormal_comp_diffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {H'' : Type u_8} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 G H''} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] {P : Type u_12} [TopologicalSpace P] [ChartedSpace H'' P] [IsManifold J 2 Q] [IsManifold K 2 P] (φ : Diffeomorph K J P Q ↑⊤) {i : Q → M} (hi : MDiff i) : conormal K I (i ∘ ⇑φ) = conormal J I i

The conormal set does not depend on the parametrization. Precomposing a differentiable map with a diffeomorphism of its source does not change its conormal set.

theorem TauCeti.CotangentBundle.image_cotangent_conormal {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E₂ : Type u_5} [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {H₂ : Type u_9} [TopologicalSpace H₂] {I₂ : ModelWithCorners 𝕜 E₂ H₂} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {Q : Type u_11} [TopologicalSpace Q] [ChartedSpace H' Q] {M₂ : Type u_13} [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [IsManifold I 2 M] [IsManifold I₂ 2 M₂] (h : Diffeomorph I I₂ M M₂ ↑⊤) {i : Q → M} (hi : MDiff i) : ⇑h.cotangent '' conormal J I i = conormal J I₂ (⇑h ∘ i)

Cotangent lifts carry conormal sets to conormal sets. For a diffeomorphism h : M → M₂, the cotangent lift of h maps the conormal set of a differentiable map i onto the conormal set of h ∘ i.