Pulling back Hamiltonian perturbation data along changes of domain coordinates

A Riemann surface with cylindrical ends, such as the pair of pants, carries no single global coordinate: its perturbation datum K = K_s ds + K_t dt and the inhomogeneous Floer equation are written in an affine chart on the compact part and in the cylinder coordinates (s, t) on each end. This file records how the coordinate objects of TauCeti.Geometry.Symplectic.Floer.Energy change under a change of domain coordinates φ : ℝ × ℝ → ℝ × ℝ.

The pullback φ^*K of the Hamiltonian-valued one-form K evaluates K at φ w on the pushed tangent vector dφ_w v, so its components are (φ^*K)_s = (∂_s φ)₁ K_s ∘ φ + (∂_s φ)₂ K_t ∘ φ and (φ^*K)_t = (∂_t φ)₁ K_s ∘ φ + (∂_t φ)₂ K_t ∘ φ (TauCeti.Floer.perturbationPullback). Then, for the reparametrized map u ∘ φ:

• the perturbed derivative d(u ∘ φ) - X_{φ^*K} is (du - X_K) ∘ dφ;
• the Floer energy density is multiplied by the Jacobian determinant det dφ;
• the curvature R_{φ^*K} is det dφ times R_K ∘ φ, so that R_K ds ∧ dt is a well-defined Hamiltonian-valued two-form; the second derivatives of φ cancel by the symmetry of d²φ;
• when dφ is complex linear (a holomorphic change of coordinates, such as the exponential cylinder coordinates on the ends of a punctured sphere), solutions of the Floer equation (du - X_K)^{0,1} = 0 pull back to solutions.

With the change of variables formula, the energy and the integrated curvature over a region are the same computed in either coordinate system, for an injective orientation-preserving φ. These are the identities that let the rectangle energy identity TauCeti.SymplecticForm.integral_floerEnergyDensity be applied chart by chart on a punctured domain.

Main definitions

• TauCeti.Floer.perturbationPullback: the pullback φ^*K of a perturbation datum, evaluated on a tangent vector.

Main results

• TauCeti.Floer.perturbationPullback_comp: pullback is compatible with composition of coordinate changes.
• TauCeti.Floer.fderiv_perturbationPullback_sub_fderiv_perturbationPullback: the domain-derivative part ∂_s K_t - ∂_t K_s of the curvature scales by det dφ, for any target.
• TauCeti.Floer.perturbationPullback_realChart: the pullback of a datum on ℂ along a holomorphic map f evaluates the datum at f w on f'(w) v.
• TauCeti.Floer.differentiableAt_domain_of_differentiableAt, TauCeti.Floer.differentiableAt_target_of_differentiableAt: a datum on ℂ that is differentiable jointly in the domain and target points is differentiable in each of them, in real coordinates.
• TauCeti.SymplecticForm.perturbedFDeriv_perturbationPullback: the perturbed derivative of the reparametrized map is the original one precomposed with dφ.
• TauCeti.SymplecticForm.floerEnergyDensity_perturbationPullback: the energy density scales by det dφ.
• TauCeti.SymplecticForm.hamiltonianCurvature_perturbationPullback: the curvature scales by det dφ.
• TauCeti.SymplecticForm.isComplexLinearMap_perturbedFDeriv_perturbationPullback: holomorphic changes of coordinates preserve the Floer equation.
• TauCeti.SymplecticForm.integral_floerEnergyDensity_image, TauCeti.SymplecticForm.integral_hamiltonianCurvature_image and TauCeti.SymplecticForm.integral_abs_hamiltonianCurvature_image: the integrated energy and curvature are invariant under injective orientation-preserving changes of coordinates, and the integrated absolute curvature under all injective ones.
• TauCeti.SymplecticForm.lintegral_enorm_hamiltonianCurvature_image: the same invariance of the integrated absolute curvature as a lower Lebesgue integral, along arbitrary maps.

References

• D. McDuff and D. Salamon, J-holomorphic curves and symplectic topology, Section 8.1, on Hamiltonian perturbations as one-forms on the domain, their curvature two-form and the energy identity.
• P. Seidel, Fukaya categories and Picard–Lefschetz theory, Section 8, on perturbation data on surfaces with strip-like ends.

noncomputable def TauCeti.Floer.perturbationPullback {X : Type u_1} (φ : ℝ × ℝ → ℝ × ℝ) (Ks Kt : ℝ × ℝ → X → ℝ) (v w : ℝ × ℝ) (x : X) : ℝ

The pullback φ^*K of the perturbation one-form K = K_s ds + K_t dt along a change of domain coordinates φ, evaluated on the tangent vector v at w and the target point x: it is K at φ w evaluated on dφ_w v. Its ds and dt components are perturbationPullback φ Ks Kt stdComplexLineReal and perturbationPullback φ Ks Kt stdComplexLineImag.

theorem TauCeti.Floer.perturbationPullback_apply {X : Type u_1} (φ : ℝ × ℝ → ℝ × ℝ) (Ks Kt : ℝ × ℝ → X → ℝ) (v w : ℝ × ℝ) (x : X) : perturbationPullback φ Ks Kt v w x = ((fderiv ℝ φ w) v).1 * Ks (φ w) x + ((fderiv ℝ φ w) v).2 * Kt (φ w) x

@[simp]

theorem TauCeti.Floer.perturbationPullback_zero {X : Type u_1} (φ : ℝ × ℝ → ℝ × ℝ) (v : ℝ × ℝ) : perturbationPullback φ (fun (x : ℝ × ℝ) (x_1 : X) => 0) (fun (x : ℝ × ℝ) (x_1 : X) => 0) v = fun (x : ℝ × ℝ) (x_1 : X) => 0

The pullback of the zero perturbation along any change of coordinates is zero.

@[simp]

theorem TauCeti.Floer.perturbationPullback_id_stdComplexLineReal {X : Type u_1} (Ks Kt : ℝ × ℝ → X → ℝ) : perturbationPullback id Ks Kt stdComplexLineReal = Ks

The ds component of the pullback along the identity is K_s.

@[simp]

theorem TauCeti.Floer.perturbationPullback_id_stdComplexLineImag {X : Type u_1} (Ks Kt : ℝ × ℝ → X → ℝ) : perturbationPullback id Ks Kt stdComplexLineImag = Kt

The dt component of the pullback along the identity is K_t.

theorem TauCeti.Floer.perturbationPullback_comp {X : Type u_1} {φ ψ : ℝ × ℝ → ℝ × ℝ} (Ks Kt : ℝ × ℝ → X → ℝ) {w : ℝ × ℝ} (hφ : DifferentiableAt ℝ φ (ψ w)) (hψ : DifferentiableAt ℝ ψ w) (v : ℝ × ℝ) : perturbationPullback (φ ∘ ψ) Ks Kt v w = perturbationPullback ψ (perturbationPullback φ Ks Kt stdComplexLineReal) (perturbationPullback φ Ks Kt stdComplexLineImag) v w

Pulling back along a composite φ ∘ ψ is pulling back along φ and then along ψ, at points where both changes of coordinates are differentiable.

theorem TauCeti.Floer.fderiv_perturbationPullback_apply {X : Type u_1} {φ : ℝ × ℝ → ℝ × ℝ} {Ks Kt : ℝ × ℝ → X → ℝ} {w : ℝ × ℝ} {x : X} (hφ : DifferentiableAt ℝ (fderiv ℝ φ) w) (hφ' : DifferentiableAt ℝ φ w) (hKs : DifferentiableAt ℝ (fun (z : ℝ × ℝ) => Ks z x) (φ w)) (hKt : DifferentiableAt ℝ (fun (z : ℝ × ℝ) => Kt z x) (φ w)) (v e : ℝ × ℝ) : (fderiv ℝ (fun (w' : ℝ × ℝ) => perturbationPullback φ Ks Kt v w' x) w) e = (((fderiv ℝ (fderiv ℝ φ) w) e) v).1 * Ks (φ w) x + ((fderiv ℝ φ w) v).1 * (fderiv ℝ (fun (z : ℝ × ℝ) => Ks z x) (φ w)) ((fderiv ℝ φ w) e) + ((((fderiv ℝ (fderiv ℝ φ) w) e) v).2 * Kt (φ w) x + ((fderiv ℝ φ w) v).2 * (fderiv ℝ (fun (z : ℝ × ℝ) => Kt z x) (φ w)) ((fderiv ℝ φ w) e))

The domain derivative of a component of the pullback φ^*K, by the product and chain rules: the second derivative of φ falls on the coefficient and the first derivative of φ on K.

theorem TauCeti.Floer.fderiv_perturbationPullback_sub_fderiv_perturbationPullback {X : Type u_1} {φ : ℝ × ℝ → ℝ × ℝ} {Ks Kt : ℝ × ℝ → X → ℝ} {w : ℝ × ℝ} {x : X} (hφ : ContDiffAt ℝ 2 φ w) (hKs : DifferentiableAt ℝ (fun (z : ℝ × ℝ) => Ks z x) (φ w)) (hKt : DifferentiableAt ℝ (fun (z : ℝ × ℝ) => Kt z x) (φ w)) : (fderiv ℝ (fun (w' : ℝ × ℝ) => perturbationPullback φ Ks Kt stdComplexLineImag w' x) w) stdComplexLineReal - (fderiv ℝ (fun (w' : ℝ × ℝ) => perturbationPullback φ Ks Kt stdComplexLineReal w' x) w) stdComplexLineImag = (fderiv ℝ φ w).det * ((fderiv ℝ (fun (z : ℝ × ℝ) => Kt z x) (φ w)) stdComplexLineReal - (fderiv ℝ (fun (z : ℝ × ℝ) => Ks z x) (φ w)) stdComplexLineImag)

The domain part of the curvature is a two-form. For a C² change of coordinates φ, the exterior derivative ∂_s (φ^*K)_t - ∂_t (φ^*K)_s of the pulled-back datum at a fixed target point is the Jacobian determinant of φ times ∂_s K_t - ∂_t K_s at φ w. The terms involving second derivatives of φ cancel by the symmetry of d²φ. No structure on the target is involved.

Holomorphic changes of coordinates

theorem TauCeti.Floer.perturbationPullback_realChart {X : Type u_1} (P : ℂ → X → ℂ →L[ℝ] ℝ) {f : ℂ → ℂ} {f' : ℂ} {w : ℝ × ℝ} (hf : HasDerivAt f f' (Complex.equivRealProdCLM.symm w)) (v : ℝ × ℝ) (x : X) : perturbationPullback (Complex.realChart f) (fun (z : ℝ × ℝ) (x : X) => (P (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : X) => (P (Complex.equivRealProdCLM.symm z) x) Complex.I) v w x = (P (f (Complex.equivRealProdCLM.symm w)) x) (f' * Complex.equivRealProdCLM.symm v)

The pullback along a holomorphic map f of a datum P on ℂ, written in the real coordinates through its values on 1 and i, evaluates P at the image point f w on the image f'(w) v of the tangent vector.

theorem TauCeti.Floer.differentiableAt_domain_of_differentiableAt {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {P : ℂ → X → ℂ →L[ℝ] ℝ} {w : ℝ × ℝ} {x : X} (hP : DifferentiableAt ℝ (fun (p : ℂ × X) => P p.1 p.2) (Complex.equivRealProdCLM.symm w, x)) (v : ℂ) : DifferentiableAt ℝ (fun (z : ℝ × ℝ) => (P (Complex.equivRealProdCLM.symm z) x) v) w

If a datum P on ℂ is differentiable jointly in the domain and target points, then, in the real coordinates, its value on a fixed tangent vector is differentiable in the domain point.

theorem TauCeti.Floer.differentiableAt_target_of_differentiableAt {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {P : ℂ → X → ℂ →L[ℝ] ℝ} {w : ℝ × ℝ} {x : X} (hP : DifferentiableAt ℝ (fun (p : ℂ × X) => P p.1 p.2) (Complex.equivRealProdCLM.symm w, x)) (v : ℂ) : DifferentiableAt ℝ (fun (y : X) => (P (Complex.equivRealProdCLM.symm w) y) v) x

If a datum P on ℂ is differentiable jointly in the domain and target points, then, in the real coordinates, its value on a fixed tangent vector is differentiable in the target point.

theorem TauCeti.SymplecticForm.hamiltonianVectorField_perturbationPullback {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {φ : ℝ × ℝ → ℝ × ℝ} {Ks Kt : ℝ × ℝ → V → ℝ} {w : ℝ × ℝ} {x : V} (ω : SymplecticForm V) (hKs : DifferentiableAt ℝ (Ks (φ w)) x) (hKt : DifferentiableAt ℝ (Kt (φ w)) x) (v : ℝ × ℝ) : ω.hamiltonianVectorField (Floer.perturbationPullback φ Ks Kt v w) x = ((fderiv ℝ φ w) v).1 • ω.hamiltonianVectorField (Ks (φ w)) x + ((fderiv ℝ φ w) v).2 • ω.hamiltonianVectorField (Kt (φ w)) x

The Hamiltonian vector field of a component of the pullback φ^*K is the corresponding combination of the Hamiltonian vector fields of K_s and K_t at φ w.

theorem TauCeti.SymplecticForm.perturbedFDeriv_perturbationPullback {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {φ : ℝ × ℝ → ℝ × ℝ} {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {w : ℝ × ℝ} (ω : SymplecticForm V) (hφ : DifferentiableAt ℝ φ w) (hu : DifferentiableAt ℝ u (φ w)) (hKs : DifferentiableAt ℝ (Ks (φ w)) (u (φ w))) (hKt : DifferentiableAt ℝ (Kt (φ w)) (u (φ w))) : ω.perturbedFDeriv (Floer.perturbationPullback φ Ks Kt stdComplexLineReal) (Floer.perturbationPullback φ Ks Kt stdComplexLineImag) (u ∘ φ) w = ω.perturbedFDeriv Ks Kt u (φ w) ∘SL fderiv ℝ φ w

Naturality of the perturbed derivative. The perturbed derivative of the reparametrized map u ∘ φ for the pulled-back datum φ^*K is (du - X_K) ∘ dφ.

theorem TauCeti.SymplecticForm.floerEnergyDensity_perturbationPullback {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {φ : ℝ × ℝ → ℝ × ℝ} {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {w : ℝ × ℝ} (ω : SymplecticForm V) (hφ : DifferentiableAt ℝ φ w) (hu : DifferentiableAt ℝ u (φ w)) (hKs : DifferentiableAt ℝ (Ks (φ w)) (u (φ w))) (hKt : DifferentiableAt ℝ (Kt (φ w)) (u (φ w))) : ω.floerEnergyDensity (Floer.perturbationPullback φ Ks Kt stdComplexLineReal) (Floer.perturbationPullback φ Ks Kt stdComplexLineImag) (u ∘ φ) w = (fderiv ℝ φ w).det * ω.floerEnergyDensity Ks Kt u (φ w)

The energy density is a two-form. The Floer energy density of u ∘ φ for the pulled-back datum φ^*K is the Jacobian determinant of φ times the energy density of u for K at φ w.

theorem TauCeti.SymplecticForm.hamiltonianCurvature_perturbationPullback {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {φ : ℝ × ℝ → ℝ × ℝ} {Ks Kt : ℝ × ℝ → V → ℝ} {w : ℝ × ℝ} {x : V} (ω : SymplecticForm V) (hφ : ContDiffAt ℝ 2 φ w) (hKs : DifferentiableAt ℝ (fun (z : ℝ × ℝ) => Ks z x) (φ w)) (hKt : DifferentiableAt ℝ (fun (z : ℝ × ℝ) => Kt z x) (φ w)) : ω.hamiltonianCurvature (Floer.perturbationPullback φ Ks Kt stdComplexLineReal) (Floer.perturbationPullback φ Ks Kt stdComplexLineImag) w x = (fderiv ℝ φ w).det * ω.hamiltonianCurvature Ks Kt (φ w) x

The curvature is a two-form. For a C² change of coordinates φ, the curvature of the pulled-back datum φ^*K is the Jacobian determinant of φ times the curvature of K at φ w. The terms involving second derivatives of φ cancel by the symmetry of d²φ.

theorem TauCeti.SymplecticForm.isComplexLinearMap_perturbedFDeriv_perturbationPullback {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {φ : ℝ × ℝ → ℝ × ℝ} {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {w : ℝ × ℝ} (ω : SymplecticForm V) {J : AlmostComplexStructure V} (hφ : DifferentiableAt ℝ φ w) (hu : DifferentiableAt ℝ u (φ w)) (hKs : DifferentiableAt ℝ (Ks (φ w)) (u (φ w))) (hKt : DifferentiableAt ℝ (Kt (φ w)) (u (φ w))) (hφJ : IsComplexLinearMap (AlmostComplexStructure.product ℝ) (AlmostComplexStructure.product ℝ) ↑(fderiv ℝ φ w)) (h : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J ↑(ω.perturbedFDeriv Ks Kt u (φ w))) : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J ↑(ω.perturbedFDeriv (Floer.perturbationPullback φ Ks Kt stdComplexLineReal) (Floer.perturbationPullback φ Ks Kt stdComplexLineImag) (u ∘ φ) w)

Holomorphic changes of coordinates preserve the Floer equation. If dφ is complex linear at w and u solves (du - X_K)^{0,1} = 0 at φ w, then u ∘ φ solves the Floer equation for the pulled-back datum φ^*K at w.

theorem TauCeti.SymplecticForm.integral_floerEnergyDensity_image {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {φ : ℝ × ℝ → ℝ × ℝ} {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {s : Set (ℝ × ℝ)} (ω : SymplecticForm V) (hs : MeasurableSet s) (hinj : Set.InjOn φ s) (hφ : ∀ w ∈ s, DifferentiableAt ℝ φ w) (hdet : ∀ w ∈ s, 0 ≤ (fderiv ℝ φ w).det) (hu : ∀ w ∈ s, DifferentiableAt ℝ u (φ w)) (hKs : ∀ w ∈ s, DifferentiableAt ℝ (Ks (φ w)) (u (φ w))) (hKt : ∀ w ∈ s, DifferentiableAt ℝ (Kt (φ w)) (u (φ w))) : ∫ (z : ℝ × ℝ) in φ '' s, ω.floerEnergyDensity Ks Kt u z = ∫ (w : ℝ × ℝ) in s, ω.floerEnergyDensity (Floer.perturbationPullback φ Ks Kt stdComplexLineReal) (Floer.perturbationPullback φ Ks Kt stdComplexLineImag) (u ∘ φ) w

Invariance of the energy under changes of coordinates. For a change of coordinates φ that is injective and orientation preserving on a measurable set s, the energy of u for K over φ '' s is the energy of u ∘ φ for φ^*K over s.

theorem TauCeti.SymplecticForm.integral_hamiltonianCurvature_image {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {φ : ℝ × ℝ → ℝ × ℝ} {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {s : Set (ℝ × ℝ)} (ω : SymplecticForm V) (hs : MeasurableSet s) (hinj : Set.InjOn φ s) (hφ : ∀ w ∈ s, ContDiffAt ℝ 2 φ w) (hdet : ∀ w ∈ s, 0 ≤ (fderiv ℝ φ w).det) (hKs : ∀ w ∈ s, DifferentiableAt ℝ (fun (z : ℝ × ℝ) => Ks z (u (φ w))) (φ w)) (hKt : ∀ w ∈ s, DifferentiableAt ℝ (fun (z : ℝ × ℝ) => Kt z (u (φ w))) (φ w)) : ∫ (z : ℝ × ℝ) in φ '' s, ω.hamiltonianCurvature Ks Kt z (u z) = ∫ (w : ℝ × ℝ) in s, ω.hamiltonianCurvature (Floer.perturbationPullback φ Ks Kt stdComplexLineReal) (Floer.perturbationPullback φ Ks Kt stdComplexLineImag) w (u (φ w))

Invariance of the integrated curvature under changes of coordinates. For a C² change of coordinates φ that is injective and orientation preserving on a measurable set s, the integral of the curvature R_K(u) over φ '' s is the integral of R_{φ^*K}(u ∘ φ) over s.

theorem TauCeti.SymplecticForm.integral_abs_hamiltonianCurvature_image {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {φ : ℝ × ℝ → ℝ × ℝ} {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {s : Set (ℝ × ℝ)} (ω : SymplecticForm V) (hs : MeasurableSet s) (hinj : Set.InjOn φ s) (hφ : ∀ w ∈ s, ContDiffAt ℝ 2 φ w) (hKs : ∀ w ∈ s, DifferentiableAt ℝ (fun (z : ℝ × ℝ) => Ks z (u (φ w))) (φ w)) (hKt : ∀ w ∈ s, DifferentiableAt ℝ (fun (z : ℝ × ℝ) => Kt z (u (φ w))) (φ w)) : ∫ (z : ℝ × ℝ) in φ '' s, |ω.hamiltonianCurvature Ks Kt z (u z)| = ∫ (w : ℝ × ℝ) in s, |ω.hamiltonianCurvature (Floer.perturbationPullback φ Ks Kt stdComplexLineReal) (Floer.perturbationPullback φ Ks Kt stdComplexLineImag) w (u (φ w))|

Invariance of the curvature allowance under changes of coordinates. For a C² change of coordinates φ that is injective on a measurable set s, the integral of |R_K(u)| over φ '' s is the integral of |R_{φ^*K}(u ∘ φ)| over s. No orientation hypothesis is needed, since both sides are absolute values. Curvature bounds used in energy estimates may therefore be computed in any chart.

theorem TauCeti.SymplecticForm.lintegral_enorm_hamiltonianCurvature_image {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {φ : ℝ × ℝ → ℝ × ℝ} {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {s : Set (ℝ × ℝ)} (ω : SymplecticForm V) (hs : MeasurableSet s) (hinj : Set.InjOn φ s) (hφ : ∀ w ∈ s, ContDiffAt ℝ 2 φ w) (hKs : ∀ w ∈ s, DifferentiableAt ℝ (fun (z : ℝ × ℝ) => Ks z (u (φ w))) (φ w)) (hKt : ∀ w ∈ s, DifferentiableAt ℝ (fun (z : ℝ × ℝ) => Kt z (u (φ w))) (φ w)) : ∫⁻ (z : ℝ × ℝ) in φ '' s, ‖ω.hamiltonianCurvature Ks Kt z (u z)‖ₑ = ∫⁻ (w : ℝ × ℝ) in s, ‖ω.hamiltonianCurvature (Floer.perturbationPullback φ Ks Kt stdComplexLineReal) (Floer.perturbationPullback φ Ks Kt stdComplexLineImag) w (u (φ w))‖ₑ

Invariance of the curvature allowance as a lower integral. For a C² change of coordinates φ that is injective on a measurable set s, the lower Lebesgue integral of |R_K(u)| over φ '' s is that of |R_{φ^*K}(u ∘ φ)| over s. Unlike TauCeti.SymplecticForm.integral_abs_hamiltonianCurvature_image, no integrability or measurability of the integrands is needed, so curvature allowances along arbitrary maps u may be computed in any chart.