Periods of closed 1-forms on the first singular homology group #
A closed C¹ 1-form φ on a manifold M can be integrated along every singular 1-simplex,
read as a continuous path (TauCeti.pathClassIntegral), and hence along every singular
1-chain. The integral is additive under concatenation of paths, so it vanishes on the boundaries
of singular 2-simplices and descends to a homomorphism TauCeti.homologyPeriodHom φ from the
first singular homology group H₁(M; ℤ) to the coefficients.
Unlike the period homomorphism TauCeti.periodHom φ x on the fundamental group, it needs no base
point, and it recovers the periods on loops at every base point: the period homomorphism factors
as π₁(M, x) → H₁(M; ℤ) → F through the Hurewicz map (TauCeti.homologyPeriodHom_hurewicz₁).
For a path-connected manifold, where the Hurewicz map identifies H₁(M; ℤ) with the
abelianization of π₁(M, x), this determines homologyPeriodHom φ
(TauCeti.homologyPeriodHom_hurewiczHomologyAddEquiv). The periods are natural: the periods of
the pullback f^* θ along a C² map f are those of θ composed with the induced map
f_* : H₁(M; ℤ) → H₁(M'; ℤ) (TauCeti.homologyPeriodHom_singularHomologyMap).
For smooth real forms the homomorphism only depends on the de Rham class, and it determines the
class, with no connectedness assumption: TauCeti.deRhamCohomology.homologyPeriod is an injective
linear map from H¹_dR(M) to the homomorphisms H₁(M; ℤ) → ℝ. A closed form with vanishing periods
has a primitive on each path component, the integral from a base point of the component
(TauCeti.exists_mextDeriv_eq_of_homologyPeriodHom_eq_zero, for any coefficients).
The singular chains are those of TopCat.of M in TopCat.{0}, so M and the coefficients live
in Type.
Main declarations #
TauCeti.homologyPeriodHom φ: the integral of a closedC¹1-form on singular1-cycles, as a homomorphism fromH₁(M; ℤ)to the coefficients.TauCeti.homologyPeriodHom_homologyπ: its value on the class of a cycleΣ nᵢ σᵢisΣ nᵢ ∫_{σᵢ} φ.TauCeti.homologyPeriodHom_hurewicz₁: the period of a loop is the value on its Hurewicz class.TauCeti.homologyPeriodHom_mextDeriv: exact forms have vanishing periods, for any coefficients.TauCeti.IsPrimitiveOn.eventually_exists_path_pathClassIntegral_eq_sub: near a point where a closed1-form has a primitiveg, paths from the point integrate the form to the change ofg.TauCeti.exists_mextDeriv_eq_of_homologyPeriodHom_eq_zero: a closed1-form whose periods onH₁(M; ℤ)vanish is exact.TauCeti.homologyPeriodHom_singularHomologyMap: naturality of the periods under pullback.TauCeti.mem_exactForms_one_iff_homologyPeriodHom_eq_zero: a closed smooth real1-form is exact exactly when its periods onH₁(M; ℤ)vanish.TauCeti.deRhamCohomology.homologyPeriod: the periods of de Rham classes onH₁(M; ℤ), an injective linear map.
References #
- M. Farber, Topology of Closed One-Forms, Section 1.1 (the homomorphism of periods
H₁(M; ℤ) → ℝ). - Allen Hatcher, Algebraic Topology, Theorem 2A.1.
The period homomorphism on singular homology of a 1-form φ: the integral of φ on
singular 1-cycles of M, as a homomorphism from H₁(M; ℤ) to the coefficients. A singular
1-simplex is integrated as the continuous path it traces (TauCeti.pathClassIntegral). It is
meaningful for closed C¹ forms, and 0 otherwise.
Instances For
The period on the class of a cycle, given in the explicit description H₁ of the first
homology group.
The period on the homology class of a cycle Σ nᵢ σᵢ is Σ nᵢ ∫_{σᵢ} φ.
The period on the homology class of a loop is the integral along the loop.
The periods factor through H₁(M; ℤ): the period of a loop class g at any base point is
the value of homologyPeriodHom φ on the Hurewicz class of g.
On a path-connected manifold, homologyPeriodHom φ is the period homomorphism at x
transported along the Hurewicz isomorphism from the abelianization of π₁(M, x).
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 a 1-form which is not a closed C¹ form are 0 by convention.
The periods of the zero form vanish.
Stokes' theorem on singular 1-chains. The integral of dψ along a singular 1-chain is
the evaluation of the 0-form ψ on its boundary.
Naturality under pullback #
Naturality of the periods on singular homology. For a closed C¹ form θ and a C²
map f, the period of θ on the image f_* c of a class c ∈ H₁(M; ℤ) is the period of the
pullback f^* θ on c.
Periods of de Rham classes on singular homology #
Exact forms have vanishing periods on singular homology. The periods of the exterior
derivative of a C² function vanish.
Exact smooth real 1-forms have vanishing periods on singular homology.
Paths along a local primitive. If g is a primitive of a closed C¹ 1-form φ on an
open set containing x, then every point y near x is joined to x by a path along which the
integral of φ is g y - g x.
Forms with vanishing periods on singular homology are exact. A closed C^r 1-form
(1 ≤ r) whose periods on H₁(M; ℤ) vanish is the exterior derivative of a C^r function.
Periods on singular homology detect exactness. A closed smooth real 1-form is exact
exactly when its periods on H₁(M; ℤ) vanish.
The periods of a de Rham class on singular homology in degree one: the homomorphism
homologyPeriodHom of any closed form representing it, as a linear map from H¹_dR(M) to the
homomorphisms H₁(M; ℤ) → ℝ.
Instances For
The periods on singular homology of the class of a closed form are those of the form.
The periods of a de Rham class on the Hurewicz class of a loop class g are its periods
on g.
De Rham classes of degree one are determined by their periods on singular homology.