Integrals of closed 1-forms along continuous paths, and periods #
A closed C¹ 1-form φ can be integrated along every continuous path, and the integral only
depends on the homotopy class of the path relative to its endpoints. The integral along a path
γ from x to y is TauCeti.pathClassIntegral φ γ. It is computed by lifting γ to the
covering space TauCeti.PrimitiveSpace φ of local primitives: a lift is a primitive of φ along
the path, and the integral is the change of its value (TauCeti.pathClassIntegral_mk_eq_sub).
Equivalently, the monodromy of the covering along γ translates values by the integral
(TauCeti.PrimitiveSpace.value_monodromy), which gives homotopy invariance for free.
The integral is additive under concatenation (TauCeti.pathClassIntegral_trans), linear in the
form (TauCeti.pathClassIntegral_smul_add_smul), equal to the endpoint difference of a primitive
for exact forms (TauCeti.pathClassIntegral_mextDeriv_ofFunction), and equal to the line integral
TauCeti.pathIntegral along C¹ curves (TauCeti.pathClassIntegral_mk_eq_pathIntegral).
On loops at x it is the period homomorphism TauCeti.periodHom φ x from the fundamental
group to the coefficients. For smooth real closed forms it only depends on the de Rham class, and on
a connected manifold a closed form is exact exactly when all its periods vanish
(TauCeti.mem_exactForms_one_iff_periodHom_eq_zero). Hence the periods give an injective linear
map TauCeti.deRhamCohomology.period from H¹_dR(M) to the homomorphisms π₁(M, x) → ℝ.
Periods are natural under pullback: the integral of f^* θ along γ is the integral of θ along
f ∘ γ (TauCeti.pathClassIntegral_mpullback), so the periods of f^* θ at x are those of θ
at f x composed with f_* : π₁(M, x) → π₁(M', f x) (TauCeti.periodHom_mpullback,
TauCeti.deRhamCohomology.period_map). Consequently, for a smooth map f from a connected
manifold, f^* θ is exact exactly when the periods of θ vanish on the image of f_*
(TauCeti.mpullback_mem_exactForms_one_iff_periodHom_map_eq_zero). For a covering map this image
is the subgroup of loops lifting to loops, so this decides which covers make a closed form exact.
Main declarations #
TauCeti.pathClassIntegral φ γ: the integral of a closedC¹1-form along a homotopy class of paths.TauCeti.periodHom φ x: the period homomorphism ofφon the fundamental group atx.TauCeti.mem_exactForms_one_iff_periodHom_eq_zero: a closed smooth real1-form on a connected manifold is exact exactly when its periods vanish.TauCeti.deRhamCohomology.period: the periods of de Rham classes in degree one, an injective linear map on a connected manifold.TauCeti.pathClassIntegral_mpullback,TauCeti.periodHom_mpullback,TauCeti.deRhamCohomology.period_map: naturality of integrals and periods under pullback.TauCeti.mpullback_mem_exactForms_one_iff_periodHom_map_eq_zero: the pullback of a closed form along a smooth map from a connected manifold is exact exactly when the periods vanish on the image of the fundamental group.
References #
- John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 11, section Conservative Covector Fields, and Chapter 17.
- Allen Hatcher, Algebraic Topology, Section 1.3 (path lifting and monodromy).
- M. Farber, Topology of Closed One-Forms, Section 1.1 (the homomorphism of periods).
The integral of a closed C¹ 1-form φ along a homotopy class γ of paths from x to y:
the value at the end of the lift of γ to the covering space of local primitives of φ which
starts at x with value 0. It is 0 when φ is not a closed C¹ form.
Instances For
The integral of a form which is not a closed C¹ form is 0 by convention.
Integration along a lift. If Γ is a continuous lift of the path γ to the covering space
of local primitives of a closed C¹ form φ, then the integral of φ along γ is the change of
the value of Γ.
Integration inside the domain of a primitive. The integral of a closed C¹ form along a
path inside an open set U is the difference of the values at the endpoints of any primitive of
the form on U.
The monodromy of the covering space of local primitives along γ translates values by the
integral of φ along γ.
The integral along a constant path vanishes.
Casting the endpoints of a path class does not change the integral.
The integral along a concatenation of paths is the sum of the integrals.
The integral along the reversed path is the negative of the integral.
The fundamental theorem of calculus for path classes. The integral of the differential of
a C² function along a path class is the difference of the values of the function at the
endpoints.
The fundamental theorem of calculus for path classes, for a C² form ψ of degree zero:
the integral of dψ along a path class is the difference of the values of ψ at the
endpoints.
Path classes of smooth curves. The integral of a closed C¹ form along the class of a
path which follows a C¹ curve c is the line integral along c.
Paths which agree pointwise have the same integral, even when their endpoints are written differently.
Linearity in the form #
Integration along path classes is linear in the closed C¹ form.
Integration along path classes is additive in the closed C¹ form.
The integral of the zero form vanishes.
Integration along path classes commutes with real scalar multiplication of the form.
The period homomorphism #
The period homomorphism of a 1-form φ at x: the integral of φ along loops at x,
as a homomorphism from the fundamental group to the coefficients. It is meaningful for closed
C¹ forms, and 0 otherwise.
Instances For
The periods of a sum of closed C¹ forms are the sums of their periods.
The periods of a real multiple of a form are the multiples of its periods.
The periods of the zero form vanish.
The period of a closed C¹ form along the class of a C¹ loop is its line integral.
Naturality under pullback #
Naturality of path class integrals. The integral of the pullback of a closed C¹ form θ
along a C² map f over a path class γ is the integral of θ over the image of γ.
Naturality of periods. The periods of the pullback of a closed C¹ form θ along a C²
map f are the periods of θ composed with the induced map of fundamental groups.
Periods of smooth real forms and de Rham cohomology #
Exact smooth real 1-forms have vanishing periods.
Periods detect exactness. A closed smooth real 1-form on a connected manifold is exact
exactly when all its periods at a base point x₀ vanish.
Exactness of pullbacks. The pullback of a closed smooth real 1-form θ along a smooth
map f from a connected manifold is exact exactly when the periods of θ vanish on the image of
the fundamental group under f. For a covering map, this says that θ becomes exact on the cover
exactly when its periods vanish on the loops which lift to loops.
The periods of a de Rham class in degree one: the period homomorphism of any closed form
representing it, as a linear map from H¹_dR(M) to the homomorphisms from the fundamental group
at x to ℝ.
Instances For
The periods of the class of a closed form are the periods of the form.
De Rham classes of degree one are determined by their periods on a connected manifold.
Naturality of periods of de Rham classes. The periods of the pullback of a class along a
smooth map f are the periods of the class composed with the induced map of fundamental groups.