Local primitives of closed 1-forms and their covering space #
A function g is a primitive of a 1-form φ on an open set U (TauCeti.IsPrimitiveOn) when
it is differentiable there with d g = φ. By the Poincaré lemma
(TauCeti.exists_mextDeriv_eq_nhds) a closed C^r 1-form (1 ≤ r) has a C^r primitive near
every point (TauCeti.exists_contMDiff_isPrimitiveOn), and two primitives on a common open set
differ by a locally constant function.
Pairs (x, a) of a point and a value, with the topology generated by the graphs
{(y, g y) | y ∈ U} of the primitives g of φ on open sets U, make up the space
TauCeti.PrimitiveSpace φ.
For closed φ the projection to the point is a covering map
(TauCeti.PrimitiveSpace.isCoveringMap_proj): over an open set carrying a primitive g, the sheets
are the graphs of the translates g + c. Translating the value is a continuous map of this space
over M (TauCeti.PrimitiveSpace.translate).
This covering space is the integration theory of closed 1-forms along continuous paths: a lift of
a path is a primitive of the form along the path, and its monodromy is the integral. It gives the
exactness of closed 1-forms on simply connected manifolds and the period homomorphism of a closed
1-form on the fundamental group.
Main declarations #
TauCeti.IsPrimitiveOn φ g U:gis a primitive ofφon the open setU.TauCeti.IsPrimitiveOn.mpullback: composing with a differentiable map gives a primitive of the pulled back form.IsLocalDiffeomorphAt.isPrimitiveOn_comp_localInverse: conversely, a primitive of a form pulled back along a local diffeomorphism descends along its local inverse.TauCeti.PrimitiveSpace φ: the space of points and values with the topology of local primitives.TauCeti.PrimitiveSpace.isCoveringMap_proj: its projection is a covering map whenφis closed.TauCeti.PrimitiveSpace.exists_isPrimitiveOn_eventually_value_eq: near each parameter, a continuous map intoPrimitiveSpace φruns along the graph of a translate of a local primitive.
References #
- John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 11, section Conservative Covector Fields.
- Allen Hatcher, Algebraic Topology, Section 1.3 (covering spaces and the lifting criterion).
Local primitives #
g is a primitive of the 1-form φ on the open set U: it is differentiable on U and
its differential agrees with φ there.
- isOpen : IsOpen U
- mdifferentiableOn : MDiff[U] g
- mextDeriv_eq (y : M) : y ∈ U → mextDeriv (RoughForm.ofFunction I g) y = φ y
Instances For
A differentiable function whose differential is φ is a primitive of φ on the whole space.
The sum of primitives of φ and ψ is a primitive of φ + ψ on the intersection.
A scalar multiple of a primitive of φ is a primitive of the scalar multiple of φ.
Near a point of its domain, the chart expression of a locally exact one-form is the ordinary derivative of its local primitive, read as an alternating map of one vector.
The derivative of a locally exact one-form in a preferred chart is the second derivative of its primitive, followed by the identification of linear maps with degree-one alternating maps. No critical-point assumption is needed for this coordinate formula.
Composing a primitive g of θ on U with a map f that is differentiable on an open set
W gives a primitive of the pullback of θ along f on W ∩ f ⁻¹' U.
Composing a primitive g of θ on U with a differentiable map f gives a primitive of the
pullback of θ along f on the preimage of U.
Primitives descend along a local inverse. If π is a C^n local diffeomorphism at x
(n ≠ 0) and g is a primitive of the pullback π^* θ on V, then g ∘ s is a primitive of
θ on s.source ∩ s ⁻¹' V, for the local inverse s of π near x.
The set where two primitives of the same 1-form agree is open: their difference has zero
differential, so it is locally constant.
Two primitives of the same one-form differ near a common point by their difference at that point. No connectedness of their domains is required.
The covering space of local primitives #
Pairs of a point and a value, with the topology generated by the graphs of the primitives of
φ on open sets.
Instances For
The point underlying an element of PrimitiveSpace φ.
Instances For
The value underlying an element of PrimitiveSpace φ.
Instances For
The graph of a function, as a map into PrimitiveSpace φ.
Instances For
Elements of PrimitiveSpace φ are determined by their point and value.
Every element of PrimitiveSpace φ lies on the graph of the constant function at its
value.
The graph of a primitive on an open set is continuous there.
A map into PrimitiveSpace φ which, near a parameter t, runs along the graph of a primitive
g on an open set containing the point at t, is continuous at t.
Translation of the value by c, as a map of PrimitiveSpace φ over M.
Instances For
Translation of the value is continuous: it carries the graph of a primitive g to the graph
of the primitive g + c.
By the Poincaré lemma, a closed C^r 1-form has a C^r primitive near every point.
Projecting PrimitiveSpace φ to the point is a covering map when φ is closed. Over an open
set U carrying a primitive g, the sheets are the graphs of the translates g + c.
Lifts run along local primitives. Near each parameter t, a continuous map Γ into
PrimitiveSpace φ, for a closed C^r form φ (1 ≤ r), runs along the graph of a translate
g + c of a C^r primitive g of φ on an open set U containing the point at t.