The cotangent relation of a map

A differentiable map f : M → N pulls a covector at f x back to a covector at x. It need not induce a map from T*M to T*N: the transpose of its differential need not be invertible. TauCeti.CotangentBundle.cotangentRel I J f records instead the relation between (x, p) and (f x, q) given by p = q ∘ df_x.

The relation of the identity is equality, and the relation of a composite is exactly the composite of the relations. For diffeomorphisms it is the graph of the existing cotangent lift Diffeomorph.cotangent. Under TauCeti.CotangentBundle.prodDiffeomorph, the cotangent relation of a product map Prod.map i₁ i₂ splits into the cotangent relations of its factors (TauCeti.CotangentBundle.cotangentRel_prodMap_iff). For constant maps, all target covectors over the constant value are related to the zero source covector; this illustrates why a relation is necessary for general maps.

The definition uses Mathlib's mfderiv, with its usual zero value at points where the map is not differentiable. The composition and product theorems assume differentiability only at the source point (and its image, for composition). No finite-dimensionality or boundaryless assumptions are needed.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer, 2013, Chapter 11 (pullback of covectors).

def TauCeti.CotangentBundle.cotangentRel {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_6} [TopologicalSpace H'] (J : ModelWithCorners 𝕜 F H') {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] (f : M → N) (z : CotangentBundle I M) (w : CotangentBundle J N) : Prop

The cotangent relation of f relates a source covector p to a target covector q when their base points lie over f and p is the pullback of q by the differential. At nondifferentiable points this uses the usual zero convention for mfderiv.

theorem TauCeti.CotangentBundle.cotangentRel_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_6} [TopologicalSpace H'] (J : ModelWithCorners 𝕜 F H') {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] (f : M → N) (z : CotangentBundle I M) (w : CotangentBundle J N) : cotangentRel I J f z w ↔ f z.proj = w.proj ∧ z.snd = w.snd ∘SL mfderiv% f z.proj

A pair belongs to the cotangent relation precisely when it lies over the map and the source covector is the pullback of the target covector.

@[simp]

theorem TauCeti.CotangentBundle.cotangentRel_mk_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_6} [TopologicalSpace H'] (J : ModelWithCorners 𝕜 F H') {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] (f : M → N) (x : M) (p : TangentSpace I x →L[𝕜] 𝕜) (q : TangentSpace J (f x) →L[𝕜] 𝕜) : cotangentRel I J f ⟨x, p⟩ ⟨f x, q⟩ ↔ p = q ∘SL mfderiv% f x

For covectors with the prescribed base points, membership is equality with the linear pullback.

theorem TauCeti.CotangentBundle.cotangentRel_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} {z : CotangentBundle I M} {w : CotangentBundle J N} (h : cotangentRel I J f z w) : f z.proj = w.proj

Related cotangent vectors lie over the graph of the base map.

theorem TauCeti.CotangentBundle.cotangentRel_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_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} {z : CotangentBundle I M} {w : CotangentBundle J N} (h : cotangentRel I J f z w) (v : TangentSpace I z.proj) : z.snd v = w.snd ((mfderiv% f z.proj) v)

Related covectors have the same pairing with a tangent vector and its image.

@[simp]

theorem TauCeti.CotangentBundle.cotangentRel_id_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] (z w : CotangentBundle I M) : cotangentRel I I id z w ↔ z = w

The cotangent relation of the identity map is the diagonal.

theorem TauCeti.CotangentBundle.cotangentRel_comp_iff {𝕜 : 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_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_6} [TopologicalSpace H'] (J : ModelWithCorners 𝕜 F H') {H'' : Type u_7} [TopologicalSpace H''] (K : ModelWithCorners 𝕜 G H'') {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace H'' P] {f : M → N} {g : N → P} (z : CotangentBundle I M) (u : CotangentBundle K P) (hf : MDiffAt f z.proj) (hg : MDiffAt g (f z.proj)) : cotangentRel I K (g ∘ f) z u ↔ Relation.Comp (cotangentRel I J f) (cotangentRel J K g) z u

The cotangent relation of a composite equals relational composition. In particular, every related pair factors through a covector at the intermediate base point.

@[simp]

theorem TauCeti.CotangentBundle.cotangentRel_zeroSection {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_6} [TopologicalSpace H'] (J : ModelWithCorners 𝕜 F H') {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] (f : M → N) (x : M) : cotangentRel I J f (Bundle.zeroSection (E →L[𝕜] 𝕜) (fun (x : M) => TangentSpace I x →L[𝕜] 𝕜) x) (Bundle.zeroSection (F →L[𝕜] 𝕜) (fun (x : N) => TangentSpace J x →L[𝕜] 𝕜) (f x))

The zero sections of the source and target are related over every base point.

@[simp]

theorem TauCeti.CotangentBundle.cotangentRel_const_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_6} [TopologicalSpace H'] (J : ModelWithCorners 𝕜 F H') {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] (y : N) (z : CotangentBundle I M) (w : CotangentBundle J N) : cotangentRel I J (fun (x : M) => y) z w ↔ y = w.proj ∧ z.snd = 0

A constant map relates exactly zero source covectors to arbitrary target covectors over its value.

@[simp]

theorem TauCeti.CotangentBundle.cotangentRel_diffeomorph_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_6} [TopologicalSpace H'] (J : ModelWithCorners 𝕜 F H') {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (h : Diffeomorph I J M N ↑⊤) (z : CotangentBundle I M) (w : CotangentBundle J N) : cotangentRel I J (⇑h) z w ↔ h.cotangent z = w

For a diffeomorphism, the cotangent relation is the graph of its cotangent lift.

theorem TauCeti.CotangentBundle.cotangentRel_prodMap_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E₁ : Type u_11} {E₂ : Type u_12} {F₁ : Type u_13} {F₂ : Type u_14} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] {H₁ : Type u_15} {H₂ : Type u_16} {G₁ : Type u_17} {G₂ : Type u_18} [TopologicalSpace H₁] [TopologicalSpace H₂] [TopologicalSpace G₁] [TopologicalSpace G₂] {I₁ : ModelWithCorners 𝕜 E₁ H₁} {I₂ : ModelWithCorners 𝕜 E₂ H₂} {J₁ : ModelWithCorners 𝕜 F₁ G₁} {J₂ : ModelWithCorners 𝕜 F₂ G₂} {M₁ : Type u_19} {M₂ : Type u_20} {Q₁ : Type u_21} {Q₂ : Type u_22} [TopologicalSpace M₁] [ChartedSpace H₁ M₁] [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [TopologicalSpace Q₁] [ChartedSpace G₁ Q₁] [TopologicalSpace Q₂] [ChartedSpace G₂ Q₂] [IsManifold I₁ 2 M₁] [IsManifold I₂ 2 M₂] [IsManifold J₁ 2 Q₁] [IsManifold J₂ 2 Q₂] {i₁ : Q₁ → M₁} {i₂ : Q₂ → M₂} (z : CotangentBundle (J₁.prod J₂) (Q₁ × Q₂)) (w : CotangentBundle (I₁.prod I₂) (M₁ × M₂)) (hi₁ : MDiffAt i₁ z.proj.1) (hi₂ : MDiffAt i₂ z.proj.2) : cotangentRel (J₁.prod J₂) (I₁.prod I₂) (Prod.map i₁ i₂) z w ↔ cotangentRel J₁ I₁ i₁ ((prodDiffeomorph J₁ J₂ Q₁ Q₂) z).1 ((prodDiffeomorph I₁ I₂ M₁ M₂) w).1 ∧ cotangentRel J₂ I₂ i₂ ((prodDiffeomorph J₁ J₂ Q₁ Q₂) z).2 ((prodDiffeomorph I₁ I₂ M₁ M₂) w).2

The cotangent relation of a product map splits under prodDiffeomorph. Assuming i₁ and i₂ are differentiable at the two components of z.proj, Prod.map i₁ i₂ relates z to w if and only if i₁ and i₂ relate the corresponding factors of prodDiffeomorph z and prodDiffeomorph w.