Relative Poincaré primitives by fiber scaling

On a product E × N, scale only the normal coordinate: H((q, p), t) = (q, t • p). Integrating the time contraction of H*ω gives fiberwisePoincareHomotopy ω. This form vanishes as a full ambient tensor at every (q, 0), even if ω does not. For a closed form on an open convex set stable under this scaling, its exterior derivative is ω - r*ω, where r(q, p) = (q, 0). Thus vanishing of the restriction of ω to the zero section suffices to obtain a primitive vanishing there. This is the local product construction used to compare symplectic forms relative to a submanifold.

All positive degrees and Banach coefficient spaces are allowed. The base and normal spaces need not be finite-dimensional or complete. Regularity and closedness are required only on the specified set, which may be an adapted coordinate box.

References

• A. Cannas da Silva, Lectures on Symplectic Geometry, Springer, 2001, §6 (the relative Poincaré lemma).
• R. Bott and L. W. Tu, Differential Forms in Algebraic Topology, GTM 82, §4 (integration along a homotopy).

noncomputable def TauCeti.fiberwisePoincareHomotopy {E : Type u_1} {N : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} (ω : E × N → (E × N) [⋀^Fin (k + 1)]→L[ℝ] F) : E × N → (E × N) [⋀^Fin k]→L[ℝ] F

Integrate the time contraction of the pullback by (q, p, t) ↦ (q, t • p). This relative Poincaré operator fixes the base and contracts the normal coordinate.

theorem TauCeti.fiberwisePoincareHomotopy_apply {E : Type u_1} {N : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} (ω : E × N → (E × N) [⋀^Fin (k + 1)]→L[ℝ] F) (x : E × N) : fiberwisePoincareHomotopy ω x = ∫ (t : ℝ) in 0..1, ((ω (x.1, t • x.2)).curryLeft (0, x.2)).compContinuousLinearMap ((ContinuousLinearMap.id ℝ E).prodMap (t • ContinuousLinearMap.id ℝ N))

The relative primitive evaluated as an integral of ambient alternating tensors. The remaining arguments are transformed by (v, w) ↦ (v, t • w).

@[simp]

theorem TauCeti.fiberwisePoincareHomotopy_zeroSection {E : Type u_1} {N : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} (ω : E × N → (E × N) [⋀^Fin (k + 1)]→L[ℝ] F) (q : E) : fiberwisePoincareHomotopy ω (q, 0) = 0

The relative Poincaré operator vanishes on the zero section as a full ambient tensor.

theorem TauCeti.fiberwisePoincareHomotopy_congr {E : Type u_1} {N : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {x : E × N} {ω₁ ω₂ : E × N → (E × N) [⋀^Fin (k + 1)]→L[ℝ] F} (h : Set.EqOn ω₁ ω₂ (segment ℝ (x.1, 0) x)) : fiberwisePoincareHomotopy ω₁ x = fiberwisePoincareHomotopy ω₂ x

The relative Poincaré operator at x only depends on the form along the segment from (x.1, 0) to x.

@[simp]

theorem TauCeti.fiberwisePoincareHomotopy_zero {E : Type u_1} {N : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} : fiberwisePoincareHomotopy 0 = 0

The relative Poincaré operator of the zero form is zero.

theorem TauCeti.fiberwisePoincareHomotopy_smul {E : Type u_1} {N : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} (c : ℝ) (ω : E × N → (E × N) [⋀^Fin (k + 1)]→L[ℝ] F) : fiberwisePoincareHomotopy (c • ω) = c • fiberwisePoincareHomotopy ω

The relative Poincaré operator commutes with real scalar multiplication of forms.

theorem TauCeti.fiberwisePoincareHomotopy_add_apply {E : Type u_1} {N : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {x : E × N} {ω₁ ω₂ : E × N → (E × N) [⋀^Fin (k + 1)]→L[ℝ] F} (h₁ : ContinuousOn ω₁ (segment ℝ (x.1, 0) x)) (h₂ : ContinuousOn ω₂ (segment ℝ (x.1, 0) x)) : fiberwisePoincareHomotopy (ω₁ + ω₂) x = fiberwisePoincareHomotopy ω₁ x + fiberwisePoincareHomotopy ω₂ x

The relative Poincaré operator is additive on forms that are continuous along the segment from (x.1, 0) to x.

theorem Convex.contDiffOn_fiberwisePoincareHomotopy {E : Type u_1} {N : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {s : Set (E × N)} (hs : Convex ℝ s) (hsu : UniqueDiffOn ℝ s) {r : ℕ∞} {ω : E × N → (E × N) [⋀^Fin (k + 1)]→L[ℝ] F} (hω : ContDiffOn ℝ (↑r) ω s) (hscale : ∀ x ∈ s, ∀ t ∈ Set.Icc 0 1, (x.1, t • x.2) ∈ s) : ContDiffOn ℝ (↑r) (TauCeti.fiberwisePoincareHomotopy ω) s

Fiberwise Poincaré integration preserves regularity on a convex set stable under scaling the normal coordinate.

theorem Convex.extDeriv_fiberwisePoincareHomotopy {E : Type u_1} {N : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [CompleteSpace F] {s : Set (E × N)} (hs : Convex ℝ s) (hso : IsOpen s) {ω : E × N → (E × N) [⋀^Fin (k + 1)]→L[ℝ] F} (hω : ContDiffOn ℝ 1 ω s) (hscale : ∀ x ∈ s, ∀ t ∈ Set.Icc 0 1, (x.1, t • x.2) ∈ s) (hclosed : ∀ x ∈ s, extDeriv ω x = 0) {x : E × N} (hx : x ∈ s) : extDeriv (TauCeti.fiberwisePoincareHomotopy ω) x = ω x - (ω (x.1, 0)).compContinuousLinearMap ((ContinuousLinearMap.id ℝ E).prodMap 0)

The relative Poincaré identity for a closed form: dKω = ω - r*ω, where r(q, p) = (q, 0). Only the tangential restriction of ω occurs in the correction term.

theorem Convex.extDeriv_fiberwisePoincareHomotopy_eq {E : Type u_1} {N : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [CompleteSpace F] {s : Set (E × N)} (hs : Convex ℝ s) (hso : IsOpen s) {ω : E × N → (E × N) [⋀^Fin (k + 1)]→L[ℝ] F} (hω : ContDiffOn ℝ 1 ω s) (hscale : ∀ x ∈ s, ∀ t ∈ Set.Icc 0 1, (x.1, t • x.2) ∈ s) (hclosed : ∀ x ∈ s, extDeriv ω x = 0) (hzero : ∀ (q : E), (q, 0) ∈ s → (ω (q, 0)).compContinuousLinearMap (ContinuousLinearMap.inl ℝ E N) = 0) {x : E × N} (hx : x ∈ s) : extDeriv (TauCeti.fiberwisePoincareHomotopy ω) x = ω x

If the tangential restriction to the zero section vanishes, fiber scaling gives a primitive whose exterior derivative is the original closed form. No ambient vanishing of the original form on the zero section is required.

theorem Convex.exists_contDiffOn_relative_primitive {E : Type u_1} {N : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [CompleteSpace F] {s : Set (E × N)} (hs : Convex ℝ s) (hso : IsOpen s) {r : ℕ∞} (hr : 1 ≤ r) {ω : E × N → (E × N) [⋀^Fin (k + 1)]→L[ℝ] F} (hω : ContDiffOn ℝ (↑r) ω s) (hscale : ∀ x ∈ s, ∀ t ∈ Set.Icc 0 1, (x.1, t • x.2) ∈ s) (hclosed : ∀ x ∈ s, extDeriv ω x = 0) (hzero : ∀ (q : E), (q, 0) ∈ s → (ω (q, 0)).compContinuousLinearMap (ContinuousLinearMap.inl ℝ E N) = 0) : ∃ (β : E × N → (E × N) [⋀^Fin k]→L[ℝ] F), ContDiffOn ℝ (↑r) β s ∧ (∀ (q : E), β (q, 0) = 0) ∧ ∀ x ∈ s, extDeriv β x = ω x

The relative Poincaré lemma on an adapted convex neighborhood. A closed form of positive degree whose restriction to the zero section vanishes has a primitive of the same regularity, vanishing there as a full ambient tensor. The neighborhood must be stable under scaling the normal coordinate towards zero.