Degree-one forms as sections of the bundle of fibrewise linear maps

A degree-one form with values in a vector bundle V assigns to each point an alternating map of one tangent vector. Mathlib's ContinuousAlternatingMap.ofSubsingleton identifies these with continuous linear maps TangentSpace I x →L[ℝ] V x, which are the fibres of the smooth bundle of fibrewise linear maps. This file shows that the identification preserves regularity, and packages it as a linear equivalence between smooth V-valued one-forms and smooth sections of that bundle.

For the trivial bundle V = Bundle.Trivial M ℝ the bundle of fibrewise linear maps is the cotangent bundle TauCeti.CotangentBundle I M, so smooth real one-forms are exactly smooth sections of the cotangent bundle. This is the comparison used to treat a covector field, such as the tautological one-form of a cotangent bundle, as a differential form to which the exterior derivative applies.

Main declarations

• TauCeti.mdifferentiableAt_ofSubsingleton_iff: a family of linear maps is differentiable at a point as a section of the linear-map bundle exactly when its degree-one form is.
• TauCeti.contMDiffAt_ofSubsingleton_iff, TauCeti.isSmoothBundleForm_ofSubsingleton_iff: a family of linear maps has C^n graph in the linear-map bundle, at a point or everywhere, exactly when the corresponding degree-one form does. More generally, a family of linear maps along a map b : N → M is C^n exactly when its family of degree-one forms is (TauCeti.contMDiffAt_sectionAlong_ofSubsingleton_iff).
• TauCeti.SmoothBundleForm.degreeOneEquiv: the linear equivalence between smooth degree-one forms and smooth sections of the bundle of fibrewise linear maps.
• TauCeti.SmoothBundleForm.tangentIdentity: the tangent-valued one-form sending a tangent vector to itself.
• TauCeti.isSmoothForm_ofSubsingleton_iff, TauCeti.SmoothForm.degreeOneEquiv: the same statements for fixed-coefficient forms. For F = ℝ the bundle of fibrewise linear maps is TauCeti.CotangentBundle I M, so these identify smooth real one-forms with smooth sections of the cotangent bundle.
• ContMDiff.contMDiff_totalSpaceMk_mvfderiv: the differential of a C^(n+1) function is a C^n section of the bundle of linear maps, through the exterior derivative of its 0-form.
• ContMDiff.contMDiff_totalSpaceMk_mvfderiv_uncurry: the differentials of a jointly C^(n+1) family of functions are jointly C^n.

theorem TauCeti.mdifferentiableAt_ofSubsingleton_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [IsManifold I 1 M] {α : (x : M) → TangentSpace I x →L[ℝ] V x} {x₀ : M} : (MDiffAt fun (x : M) => ⟨x, (ContinuousAlternatingMap.ofSubsingleton ℝ (TangentSpace I x) (V x) 0) (α x)⟩) x₀ ↔ (MDiffAt fun (x : M) => ⟨x, α x⟩) x₀

A bundle-valued one-form is differentiable exactly when the corresponding section of the bundle of continuous linear maps is differentiable.

theorem TauCeti.contMDiffAt_sectionAlong_ofSubsingleton_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [IsManifold I 1 M] {EN : Type u_6} {HN : Type u_7} {N : Type u_8} [NormedAddCommGroup EN] [NormedSpace ℝ EN] [TopologicalSpace HN] {J : ModelWithCorners ℝ EN HN} [TopologicalSpace N] [ChartedSpace HN N] {n : WithTop ℕ∞} {b : N → M} {α : (m : N) → TangentSpace I (b m) →L[ℝ] V (b m)} {m₀ : N} : ContMDiffAt J (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin 1]→L[ℝ] F))) n (fun (m : N) => ⟨b m, (ContinuousAlternatingMap.ofSubsingleton ℝ (TangentSpace I (b m)) (V (b m)) 0) (α m)⟩) m₀ ↔ ContMDiffAt J (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] F))) n (fun (m : N) => ⟨b m, α m⟩) m₀

A family of fibrewise linear maps along a map b : N → M is C^n at m₀ as a section of the bundle of linear maps TangentSpace I x →L[ℝ] V x along b exactly when the family of degree-one forms it defines is C^n at m₀ along b.

theorem TauCeti.contMDiffAt_ofSubsingleton_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [IsManifold I 1 M] {n : WithTop ℕ∞} {α : (x : M) → TangentSpace I x →L[ℝ] V x} {x₀ : M} : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin 1]→L[ℝ] F))) n (fun (x : M) => ⟨x, (ContinuousAlternatingMap.ofSubsingleton ℝ (TangentSpace I x) (V x) 0) (α x)⟩) x₀ ↔ ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] F))) n (fun (x : M) => ⟨x, α x⟩) x₀

A family of fibrewise linear maps is C^n at x₀ as a section of the bundle of linear maps TangentSpace I x →L[ℝ] V x exactly when the degree-one form it defines is C^n at x₀.

theorem TauCeti.isSmoothBundleForm_ofSubsingleton_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [IsManifold I 1 M] {n : WithTop ℕ∞} {α : (x : M) → TangentSpace I x →L[ℝ] V x} : (IsSmoothBundleForm I F V n fun (x : M) => (ContinuousAlternatingMap.ofSubsingleton ℝ (TangentSpace I x) (V x) 0) (α x)) ↔ ContMDiff I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] F))) n fun (x : M) => ⟨x, α x⟩

A family of fibrewise linear maps is a C^n section of the bundle of linear maps TangentSpace I x →L[ℝ] V x exactly when the degree-one form it defines is C^n.

noncomputable def TauCeti.SmoothBundleForm.degreeOneEquiv {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [IsManifold I 1 M] : SmoothBundleForm I F V 1 ≃ₗ[ℝ] ContMDiffSection I (E →L[ℝ] F) ↑⊤ fun (x : M) => TangentSpace I x →L[ℝ] V x

Smooth V-valued degree-one forms are smooth sections of the bundle of fibrewise linear maps TangentSpace I x →L[ℝ] V x, through ContinuousAlternatingMap.ofSubsingleton on each fibre.

@[simp]

theorem TauCeti.SmoothBundleForm.degreeOneEquiv_apply_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [IsManifold I 1 M] (φ : SmoothBundleForm I F V 1) (x : M) (v : TangentSpace I x) : ((degreeOneEquiv φ) x) v = (↑φ x) fun (x : Fin 1) => v

The section of a smooth degree-one form evaluates a tangent vector as the form does.

@[simp]

theorem TauCeti.SmoothBundleForm.degreeOneEquiv_symm_apply_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [IsManifold I 1 M] (s : ContMDiffSection I (E →L[ℝ] F) ↑⊤ fun (x : M) => TangentSpace I x →L[ℝ] V x) (x : M) (v : Fin 1 → TangentSpace I x) : (↑(degreeOneEquiv.symm s) x) v = (s x) (v 0)

The degree-one form of a smooth section evaluates a single tangent vector as the section does.

noncomputable def TauCeti.SmoothBundleForm.tangentIdentity {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] : SmoothBundleForm I E (TangentSpace I) 1

The canonical tangent-valued one-form: the identity on every tangent fibre.

@[simp]

theorem TauCeti.SmoothBundleForm.tangentIdentity_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (x : M) (v : Fin 1 → TangentSpace I x) : (↑tangentIdentity x) v = v 0

The tangent identity one-form evaluates to its sole tangent-vector argument.

theorem TauCeti.isSmoothForm_ofSubsingleton_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {n : WithTop ℕ∞} {α : (x : M) → TangentSpace I x →L[ℝ] F} : (IsSmoothForm I n fun (x : M) => (ContinuousAlternatingMap.ofSubsingleton ℝ (TangentSpace I x) F 0) (α x)) ↔ ContMDiff I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] F))) n fun (x : M) => ⟨x, α x⟩

A family of linear functionals TangentSpace I x →L[ℝ] F is a C^n section of the bundle of linear maps exactly when the fixed-coefficient degree-one form it defines is C^n. For F = ℝ the total space of this bundle is TauCeti.CotangentBundle I M.

theorem ContMDiff.contMDiff_totalSpaceMk_mvfderiv {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 2 M] {n : WithTop ℕ∞} {f : M → F} (hf : ContMDiff I (modelWithCornersSelf ℝ F) (n + 1) f) : ContMDiff I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] F))) n fun (x : M) => ⟨x, d% f x⟩

The differential of a C^(n+1) function is a C^n covector field: x ↦ df_x is a C^n section of the bundle of linear maps TangentSpace I x →L[ℝ] F, which is the cotangent bundle when F = ℝ.

theorem ContMDiff.contMDiff_totalSpaceMk_mvfderiv_uncurry {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {E' : Type u_6} {H' : Type u_7} {N : Type u_8} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {n : WithTop ℕ∞} {f : N → M → F} (hf : ContMDiff (J.prod I) (modelWithCornersSelf ℝ F) (n + 1) (Function.uncurry f)) : ContMDiff (J.prod I) (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] F))) n fun (q : N × M) => ⟨q.2, d% (f q.1) q.2⟩

The differential of a jointly C^(n+1) family is jointly C^n. For a family of functions f : N → M → F which is jointly C^(n+1) on N × M, the differentials (p, x) ↦ d(f p)_x form a C^n map into the bundle of linear maps TangentSpace I x →L[ℝ] F, lying over the projection N × M → M. For N = ℝ this is the regularity in time and space of the differential of a time-dependent function.

noncomputable def TauCeti.SmoothForm.degreeOneEquiv {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] : SmoothForm I M F 1 ≃ₗ[ℝ] ContMDiffSection I (E →L[ℝ] F) ↑⊤ fun (x : M) => TangentSpace I x →L[ℝ] F

Smooth F-valued one-forms are smooth sections of the bundle of linear maps TangentSpace I x →L[ℝ] F, through ContinuousAlternatingMap.ofSubsingleton on each fibre. For F = ℝ these are the smooth sections of TauCeti.CotangentBundle I M. This is SmoothBundleForm.degreeOneEquiv for the trivial bundle Bundle.Trivial M F.

theorem TauCeti.SmoothForm.degreeOneEquiv_apply_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] (φ : SmoothForm I M F 1) (x : M) (v : TangentSpace I x) : ((degreeOneEquiv φ) x) v = (↑φ x) fun (x : Fin 1) => v

The section of a smooth one-form evaluates a tangent vector as the form does.

@[simp]

theorem TauCeti.SmoothForm.degreeOneEquiv_apply_apply_vec {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] (φ : SmoothForm I M F 1) (x : M) (v : TangentSpace I x) : ((degreeOneEquiv φ) x) v = (↑φ x) ![v]

The section of a smooth one-form evaluates a tangent vector v as the form evaluates the one-element family ![v].

theorem TauCeti.SmoothForm.contMDiffAt_sectionAlong_degreeOneEquiv_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {EN : Type u_6} {HN : Type u_7} {N : Type u_8} [NormedAddCommGroup EN] [NormedSpace ℝ EN] [TopologicalSpace HN] {J : ModelWithCorners ℝ EN HN} [TopologicalSpace N] [ChartedSpace HN N] {n : WithTop ℕ∞} {b : N → M} {α : N → SmoothForm I M F 1} {m₀ : N} : ContMDiffAt J (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] F))) n (fun (m : N) => ⟨b m, (degreeOneEquiv (α m)) (b m)⟩) m₀ ↔ ContMDiffAt J (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin 1]→L[ℝ] F))) n (fun (m : N) => ⟨b m, ↑(α m) (b m)⟩) m₀

A family of smooth one-forms α m, evaluated along a map b : N → M, is C^n at m₀ as a section of the bundle of linear maps exactly when it is C^n as a section of the bundle of alternating maps.

@[simp]

theorem TauCeti.SmoothForm.apply_neg_vec {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] (φ : SmoothForm I M F 1) (x : M) (v : TangentSpace I x) : (↑φ x) ![-v] = -(↑φ x) ![v]

A smooth one-form sends the one-element family ![-v] to minus its value on ![v].

theorem TauCeti.SmoothForm.degreeOneEquiv_coe_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] (φ : SmoothForm I M F 1) (x : M) (v : TangentSpace I x) : ↑((degreeOneEquiv φ) x) v = (↑φ x) ![v]

The section of a smooth one-form, read as a linear map, evaluates a tangent vector v as the form evaluates the one-element family ![v].

theorem TauCeti.SmoothForm.degreeOneEquiv_coe_eq_zero_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : SmoothForm I M F 1} {x : M} : ↑((degreeOneEquiv φ) x) = 0 ↔ ↑φ x = 0

The section of a smooth one-form, read as a linear map, vanishes at x exactly when the form vanishes at x.

@[simp]

theorem TauCeti.SmoothForm.degreeOneEquiv_symm_apply_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] (s : ContMDiffSection I (E →L[ℝ] F) ↑⊤ fun (x : M) => TangentSpace I x →L[ℝ] F) (x : M) (v : Fin 1 → TangentSpace I x) : (↑(degreeOneEquiv.symm s) x) v = (s x) (v 0)

The one-form of a smooth section evaluates a single tangent vector as the section does.