Exactness of 1-forms through line integrals

A closed 1-form on a connected manifold is exact as soon as its integral along every smooth loop at a base point vanishes (TauCeti.exists_mextDeriv_eq_of_forall_pathIntegral_eq_zero). Together with the vanishing of the integrals of exact forms around closed curves, this characterizes the vanishing of de Rham classes in degree one (TauCeti.deRhamCohomology.mk_eq_zero_iff_forall_pathIntegral_eq_zero), which is how line integrals detect H¹_dR.

The primitive is the integral from the base point x₀: f y = ∫_γ φ along a smooth curve γ from x₀ to y. Smooth curves joining two points exist on a connected manifold (TauCeti.exists_contMDiff_curve), and the value does not depend on the curve, because two such curves concatenate, the second reversed, to a smooth loop at x₀. Near each point the closed form has a primitive by the Poincaré lemma (TauCeti.exists_mextDeriv_eq_nhds), and integrating along short curves shows that f differs from it by a constant. Hence f is smooth with df = φ. The Poincaré lemma is where finite dimensionality, the Hausdorff property and completeness of the coefficient space are used. Manifolds with boundary or corners are included.

Main declarations

• TauCeti.exists_local_primitive_pathIntegral_eq_add_sub: near a point x, a closed form φ has a function g, C^r at x with dg x = φ x, such that extending a curve from the base point to x by short curves changes its line integral by the increment of g.
• TauCeti.exists_mextDeriv_eq_of_forall_pathIntegral_eq_zero: a closed 1-form whose integrals along smooth loops at a base point vanish is exact.
• TauCeti.mem_exactForms_one_iff_forall_pathIntegral_eq_zero: a closed smooth real 1-form is exact exactly when its integrals along smooth loops at a base point vanish.
• TauCeti.deRhamCohomology.mk_eq_zero_iff_forall_pathIntegral_eq_zero: the same criterion for the vanishing of a de Rham class in degree one.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 11, section Conservative Covector Fields, and Chapter 17.

theorem TauCeti.pathIntegral_eq_of_forall_pathIntegral_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : RoughForm I M F 1} (hφ : IsSmoothForm I 0 φ) {x₀ y : M} (h : ∀ (γ : ℝ → M), ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ → γ 0 = x₀ → γ 1 = x₀ → pathIntegral φ γ 0 1 = 0) {γ γ' : ℝ → M} (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ) (hγ₀ : ∀ t ≤ 0, γ t = x₀) (hγ₁ : ∀ (t : ℝ), 1 ≤ t → γ t = y) (hγ' : ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ') (hγ'₀ : ∀ t ≤ 0, γ' t = x₀) (hγ'₁ : ∀ (t : ℝ), 1 ≤ t → γ' t = y) : pathIntegral φ γ 0 1 = pathIntegral φ γ' 0 1

If the integrals of φ along smooth loops at x₀ vanish, then two smooth curves from x₀ to y, constant on (-∞, 0] and on [1, ∞), have the same line integral: the first followed by the reversed second is a smooth loop at x₀.

theorem TauCeti.exists_local_primitive_pathIntegral_eq_add_sub {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] {r : ℕ∞} (hr : 1 ≤ r) {φ : RoughForm I M F 1} (hφ : IsSmoothForm I (↑r) φ) {x₀ x : M} (hclosed : ∀ᶠ (y : M) in nhds x, mextDeriv φ y = 0) {γ : ℝ → M} (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ) (hγ₀ : ∀ t ≤ 0, γ t = x₀) (hγ₁ : ∀ (t : ℝ), 1 ≤ t → γ t = x) : ∃ (g : M → F), ContMDiffAt I (modelWithCornersSelf ℝ F) (↑r) g x ∧ mextDeriv (RoughForm.ofFunction I g) x = φ x ∧ ∀ᶠ (y : M) in nhds x, ∃ (δ : ℝ → M), ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) δ ∧ (∀ t ≤ 0, δ t = x₀) ∧ (∀ (t : ℝ), 1 ≤ t → δ t = y) ∧ pathIntegral φ δ 0 1 = pathIntegral φ γ 0 1 + (g y - g x)

Local primitives extend line integrals. Let φ be a C^r 1-form (1 ≤ r) closed near x, and γ a smooth curve from x₀ to x, constant on (-∞, 0] and on [1, ∞). Then there is a function g, C^r at x with dg x = φ x, such that every y near x is reached from x₀ by a smooth curve δ, γ followed by a short curve from x to y, with ∫_δ φ = ∫_γ φ + g y - g x.

theorem TauCeti.exists_mextDeriv_eq_of_forall_pathIntegral_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] [PreconnectedSpace M] {r : ℕ∞} (hr : 1 ≤ r) {φ : RoughForm I M F 1} (hφ : IsSmoothForm I (↑r) φ) (hclosed : mextDeriv φ = 0) (x₀ : M) (h : ∀ (γ : ℝ → M), ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ → γ 0 = x₀ → γ 1 = x₀ → pathIntegral φ γ 0 1 = 0) : ∃ (ψ : RoughForm I M F 0), IsSmoothForm I (↑r) ψ ∧ mextDeriv ψ = φ

Line integrals detect exactness. On a preconnected manifold, a closed C^r 1-form (1 ≤ r) whose integral along every smooth loop at a base point x₀ vanishes is the exterior derivative of a C^r function. The primitive is the integral along smooth curves from x₀.

theorem TauCeti.mem_exactForms_one_iff_forall_pathIntegral_eq_zero {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] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] [PreconnectedSpace M] {φ : SmoothForm I M ℝ 1} (hφ : φ ∈ closedForms I M 1) (x₀ : M) : φ ∈ exactForms I M 1 ↔ ∀ (γ : ℝ → M), ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ → γ 0 = x₀ → γ 1 = x₀ → pathIntegral (↑φ) γ 0 1 = 0

A closed smooth real 1-form on a preconnected manifold is exact exactly when its integral along every smooth loop at a base point x₀ vanishes.

theorem TauCeti.deRhamCohomology.mk_eq_zero_iff_forall_pathIntegral_eq_zero {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] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] [PreconnectedSpace M] (φ : ↥(closedForms I M 1)) (x₀ : M) : (mk I 1) φ = 0 ↔ ∀ (γ : ℝ → M), ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ → γ 0 = x₀ → γ 1 = x₀ → pathIntegral (↑↑φ) γ 0 1 = 0

A de Rham class of degree one on a preconnected manifold vanishes exactly when the integrals of a representative along all smooth loops at a base point x₀ vanish.