Hamiltonian perturbation data on the pair of pants

The pair-of-pants product of Hamiltonian Floer theory counts solutions of the perturbed Cauchy–Riemann equation (du - X_K)^{0,1} = 0 on the thrice-punctured sphere S = ℂ ∖ {0, 1}, with positive (input) cylindrical ends at 0 and 1 and a negative (output) cylindrical end at ∞. The perturbation is a one-form K on S with values in smooth functions on the target manifold M, which must equal H_q(t) dt in the end coordinates (s, t) of each end q far out on the end, where H_q is the period-one Hamiltonian attached to that end.

This file constructs such a perturbation from any three smooth period-one Hamiltonians, TauCeti.Floer.pairOfPantsPerturbation: on the end q it is β(±s) H_q(t) dt for a smooth cutoff β vanishing for ±s ≤ 1 and equal to 1 for ±s ≥ 2, and it vanishes off the three ends. Its value at w is a real covector on ℂ, so the ds and dt components of its pullback along an end lift φ are its values on φ'(z) and φ'(z) i. The results are:

• TauCeti.Floer.contMDiffAt_pairOfPantsPerturbation: the perturbation is smooth on S × M.
• TauCeti.Floer.pairOfPantsPerturbation_add: the perturbation is additive in the end Hamiltonians.
• TauCeti.Floer.pairOfPantsPerturbation_add_const: adding functions c_q of time to the end Hamiltonians adds the perturbation of the target-independent Hamiltonians c_q, which does not depend on the target point (TauCeti.Floer.pairOfPantsPerturbation_const_target).
• TauCeti.Floer.contDiffAt_pairOfPantsPerturbation_prod: for a vector space target and Cⁿ Hamiltonians, the perturbation is Cⁿ jointly in the domain and target points.
• TauCeti.Floer.pairOfPantsPerturbation_cylindricalEndLift_of_pos: on the part ±s > 0 of the end q its pullback is the continuation datum β(±s - 1) H_q(t) dt.
• TauCeti.Floer.pairOfPantsPerturbation_cylindricalEndLift: on the part ±s ≥ 2 of the end q its pullback is H_q(t) dt, that is K_s = 0 and K_t = H_q(t).
• TauCeti.Floer.pairOfPantsPerturbation_eq_smul_endAngularForm: on the part ±s ≥ 2 of the end q the perturbation itself is H_q(t) dt_q, in terms of the angular form of the end.
• TauCeti.Floer.pairOfPantsEndComponent H q v: the component of the pullback along the tangent vector v of the cylinder, in the end coordinates of the end q, so that K_s and K_t are its components along v = 1 and v = i; TauCeti.Floer.pairOfPantsEndComponent_of_pos computes them on the part ±s > 0 of the end, and TauCeti.Floer.pairOfPantsEndComponent_I_of_two_le gives K_t = H_q(t) where ±s ≥ 2.
• TauCeti.Floer.exists_cylindricalEndLift_of_pairOfPantsPerturbation_ne_zero: it is supported in the parts ±s > 1 of the three ends, so it vanishes off the ends; TauCeti.Floer.pairOfPantsPerturbation_eq_zero_of_forall_le states this in end coordinates.

The angular coordinate t of an end is defined only modulo 1, which is why the Hamiltonians are required to have period one: smoothness across the ray where the angular coordinate jumps is TauCeti.ThricePuncturedSphere.Puncture.contMDiffAt_comp_im_endCoord.

References

• M. Schwarz, Cohomology operations from S¹-cobordisms in Floer homology, PhD thesis, ETH Zürich (1995), on perturbation data for the pair-of-pants product.
• P. Seidel, Fukaya categories and Picard–Lefschetz theory, EMS (2008), on perturbation one-forms on punctured surfaces that agree with H dt on the ends.

noncomputable def TauCeti.Floer.pairOfPantsPerturbation {M : Type u_1} (H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ) (w : ℂ) (x : M) : ℂ →L[ℝ] ℝ

The Hamiltonian perturbation one-form on the pair of pants given by period-one Hamiltonians H q on its three ends. At w ∈ ℂ and x ∈ M it is the covector ∑ q, β(±s_q(w)) H_q(t_q(w), x) dt_q, where (s_q, t_q) are the coordinates of the end q, the sign is that of the end, and β is the smooth transition from 0 on (-∞, 1] to 1 on [2, ∞).

theorem TauCeti.Floer.pairOfPantsPerturbation_def {M : Type u_1} (H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ) (w : ℂ) (x : M) : pairOfPantsPerturbation H w x = ∑ q : ThricePuncturedSphere.Puncture, ((q.endSign * (q.endCoord w).re - 1).smoothTransition * H q (q.endCoord w).im x) • q.endAngularForm w

The defining equation of the perturbation: the cutoff-weighted sum over the three ends of H_q(t_q(w), x) dt_q.

theorem TauCeti.Floer.pairOfPantsPerturbation_add {M : Type u_1} (H G : ThricePuncturedSphere.Puncture → ℝ → M → ℝ) (w : ℂ) (x : M) : pairOfPantsPerturbation (fun (q : ThricePuncturedSphere.Puncture) (t : ℝ) (y : M) => H q t y + G q t y) w x = pairOfPantsPerturbation H w x + pairOfPantsPerturbation G w x

The pair-of-pants perturbation is additive in the end Hamiltonians.

theorem TauCeti.Floer.pairOfPantsPerturbation_add_const {M : Type u_1} (H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ) (c : ThricePuncturedSphere.Puncture → ℝ → ℝ) (w : ℂ) (x : M) : pairOfPantsPerturbation (fun (q : ThricePuncturedSphere.Puncture) (t : ℝ) (y : M) => H q t y + c q t) w x = pairOfPantsPerturbation H w x + pairOfPantsPerturbation (fun (q : ThricePuncturedSphere.Puncture) (t : ℝ) (x : M) => c q t) w x

Normalizing the end Hamiltonians. Adding functions c_q of time to the end Hamiltonians adds the pair-of-pants perturbation of the target-independent Hamiltonians c_q.

theorem TauCeti.Floer.pairOfPantsPerturbation_const_target {M : Type u_1} (c : ThricePuncturedSphere.Puncture → ℝ → ℝ) (w : ℂ) (x y : M) : pairOfPantsPerturbation (fun (q : ThricePuncturedSphere.Puncture) (t : ℝ) (x : M) => c q t) w x = pairOfPantsPerturbation (fun (q : ThricePuncturedSphere.Puncture) (t : ℝ) (x : M) => c q t) w y

The pair-of-pants perturbation of target-independent Hamiltonians does not depend on the target point.

theorem TauCeti.Floer.one_lt_endSign_mul_re_endCoord {q : ThricePuncturedSphere.Puncture} {w : ℂ} (h : (q.endSign * (q.endCoord w).re - 1).smoothTransition ≠ 0) : 1 < q.endSign * (q.endCoord w).re ∧ w ≠ q.endCenter

Where the cutoff of the end q is nonzero, the point lies on the part ±s > 1 of that end, and in particular it is not the center of the end.

theorem TauCeti.Floer.exists_cylindricalEndLift_of_pairOfPantsPerturbation_ne_zero {M : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ} {w : ℂ} {x : M} (h : pairOfPantsPerturbation H w x ≠ 0) : ∃ (q : ThricePuncturedSphere.Puncture) (z : ℂ), 1 < q.endSign * z.re ∧ q.cylindricalEndLift z = w

The perturbation is supported in the parts ±s > 1 of the three ends.

theorem TauCeti.Floer.pairOfPantsPerturbation_eq_zero_of_forall_le {M : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ} {w : ℂ} (h : ∀ (q : ThricePuncturedSphere.Puncture), q.endSign * (q.endCoord w).re ≤ 1) (x : M) : pairOfPantsPerturbation H w x = 0

The perturbation vanishes at every point where the signed longitudinal coordinate of every end is at most 1.

theorem TauCeti.Floer.pairOfPantsPerturbation_single {M : Type u_1} (q : ThricePuncturedSphere.Puncture) (G : ℝ → M → ℝ) (w : ℂ) (x : M) : pairOfPantsPerturbation (Pi.single q G) w x = ((q.endSign * (q.endCoord w).re - 1).smoothTransition * G (q.endCoord w).im x) • q.endAngularForm w

The pair-of-pants datum of a single end is the summand of that end.

theorem TauCeti.Floer.pairOfPantsPerturbation_endCenter {M : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ} (q : ThricePuncturedSphere.Puncture) (x : M) : pairOfPantsPerturbation H q.endCenter x = 0

The perturbation vanishes at the center of every end. The centers are the punctures 0 and 1, where every signed longitudinal coordinate is at most 0.

@[simp]

theorem TauCeti.Floer.smoothTransition_endCoord_cylindricalEndLift_eq_zero {q r : ThricePuncturedSphere.Puncture} (hrq : r ≠ q) {z : ℂ} (hz : 0 < q.endSign * z.re) : (r.endSign * (r.endCoord (q.cylindricalEndLift z)).re - 1).smoothTransition = 0

On the part ±s > 0 of the end q, the cutoff of every other end r vanishes, since the parts ±s > 0 of distinct ends are disjoint.

theorem TauCeti.Floer.pairOfPantsPerturbation_cylindricalEndLift_of_pos {M : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ} {q : ThricePuncturedSphere.Puncture} (hH : Function.Periodic (H q) 1) {z : ℂ} (hz : 0 < q.endSign * z.re) (x : M) (v : ℂ) : (pairOfPantsPerturbation H (q.cylindricalEndLift z) x) (deriv q.cylindricalEndLift z * v) = v.im * ((q.endSign * z.re - 1).smoothTransition * H q z.im x)

The perturbation on an end. On the part ±s > 0 of the end q, the pullback of the perturbation along the end lift φ is the continuation datum β(±s - 1) H_q(t) dt: it sends a tangent vector v of the cylinder to Im v · β(±s - 1) H_q(t).

theorem TauCeti.Floer.pairOfPantsPerturbation_cylindricalEndLift {M : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ} {q : ThricePuncturedSphere.Puncture} (hH : Function.Periodic (H q) 1) {z : ℂ} (hz : 2 ≤ q.endSign * z.re) (x : M) (v : ℂ) : (pairOfPantsPerturbation H (q.cylindricalEndLift z) x) (deriv q.cylindricalEndLift z * v) = v.im * H q z.im x

The perturbation is H_q(t) dt far out on each end. On the part ±s ≥ 2 of the end q, the pullback of the perturbation along the end lift φ sends a tangent vector v of the cylinder to Im v · H_q(t): its ds component (v = 1) vanishes and its dt component (v = i) is H_q(t).

theorem TauCeti.Floer.pairOfPantsPerturbation_eq_smul_endAngularForm {M : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ} {r : ThricePuncturedSphere.Puncture} {w : ℂ} (hw : 2 ≤ r.endSign * (r.endCoord w).re) (x : M) : pairOfPantsPerturbation H w x = H r (r.endCoord w).im x • r.endAngularForm w

The perturbation is H_r(t_r) dt_r far out on each end. At a point w of the part ±s ≥ 2 of the end r, the perturbation is the angular form of r scaled by the Hamiltonian H_r at the angular coordinate of w.

noncomputable def TauCeti.Floer.pairOfPantsEndComponent {M : Type u_1} (H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ) (q : ThricePuncturedSphere.Puncture) (v : ℂ) (z : ℝ × ℝ) (x : M) : ℝ

The component of the pair-of-pants perturbation along the tangent vector v of the cylinder, in the end coordinates z = (s, t) of the end q: the pullback of the perturbation along the end lift φ, evaluated at the point s + i t on v. The components K_s and K_t of the pulled-back datum K_s ds + K_t dt are those along v = 1 and v = i.

theorem TauCeti.Floer.pairOfPantsEndComponent_def {M : Type u_1} (H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ) (q : ThricePuncturedSphere.Puncture) (v : ℂ) (z : ℝ × ℝ) (x : M) : pairOfPantsEndComponent H q v z x = (pairOfPantsPerturbation H (q.cylindricalEndLift { re := z.1, im := z.2 }) x) (deriv q.cylindricalEndLift { re := z.1, im := z.2 } * v)

theorem TauCeti.Floer.pairOfPantsEndComponent_of_pos {M : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ} {q : ThricePuncturedSphere.Puncture} (hH : Function.Periodic (H q) 1) {z : ℝ × ℝ} (hz : 0 < q.endSign * z.1) (v : ℂ) (x : M) : pairOfPantsEndComponent H q v z x = v.im * ((q.endSign * z.1 - 1).smoothTransition * H q z.2 x)

On the part ±s > 0 of the end q, the component of the perturbation along v is Im v · β(±s - 1) H_q(t).

theorem TauCeti.Floer.pairOfPantsEndComponent_one_of_pos {M : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ} {q : ThricePuncturedSphere.Puncture} (hH : Function.Periodic (H q) 1) {z : ℝ × ℝ} (hz : 0 < q.endSign * z.1) (x : M) : pairOfPantsEndComponent H q 1 z x = 0

On the part ±s > 0 of the end q, the ds component of the perturbation vanishes.

theorem TauCeti.Floer.pairOfPantsEndComponent_I_of_pos {M : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ} {q : ThricePuncturedSphere.Puncture} (hH : Function.Periodic (H q) 1) {z : ℝ × ℝ} (hz : 0 < q.endSign * z.1) (x : M) : pairOfPantsEndComponent H q Complex.I z x = (q.endSign * z.1 - 1).smoothTransition * H q z.2 x

On the part ±s > 0 of the end q, the dt component of the perturbation is β(±s - 1) H_q(t).

theorem TauCeti.Floer.pairOfPantsEndComponent_I_of_two_le {M : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ} {q : ThricePuncturedSphere.Puncture} (hH : Function.Periodic (H q) 1) {z : ℝ × ℝ} (hz : 2 ≤ q.endSign * z.1) : pairOfPantsEndComponent H q Complex.I z = H q z.2

On the part ±s ≥ 2 of the end q, where the cutoff is 1, the dt component of the perturbation is H_q(t).

theorem TauCeti.Floer.eventuallyEq_pairOfPantsEndComponent {M : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ} {q : ThricePuncturedSphere.Puncture} (hH : Function.Periodic (H q) 1) {z : ℝ × ℝ} (hz : 0 < q.endSign * z.1) : (pairOfPantsEndComponent H q 1 =ᶠ[nhds z] fun (x : ℝ × ℝ) (x_1 : M) => 0) ∧ pairOfPantsEndComponent H q Complex.I =ᶠ[nhds z] fun (w : ℝ × ℝ) (x : M) => (q.endSign * w.1 - 1).smoothTransition * H q w.2 x

Near a point of the part ±s > 0 of the end q, the components of the perturbation are those of the continuation datum β(±s - 1) H_q(t) dt.

theorem TauCeti.Floer.contMDiffAt_smoothTransition_endCoord_comp {F : Type u_4} {G' : Type u_5} {N : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace G'] {I' : ModelWithCorners ℝ F G'} [TopologicalSpace N] [ChartedSpace G' N] {n : WithTop ℕ∞} [ENat.LEInfty n] (q : ThricePuncturedSphere.Puncture) (c : ℝ) {f : N → ℂ} {y₀ : N} (hf : ContMDiffAt I' (modelWithCornersSelf ℝ ℂ) n f y₀) (hq : f y₀ ≠ q.endCenter) : ContMDiffAt I' (modelWithCornersSelf ℝ ℝ) n (fun (y : N) => (q.endSign * (q.endCoord (f y)).re - c).smoothTransition) y₀

Away from the center of the end q, the shifted cutoff β(±s_q - c) is C^n along a C^n family f of points of ℂ.

theorem TauCeti.Floer.contMDiffAt_smoothTransition_endCoord {M : Type u_1} {E : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace G] {I : ModelWithCorners ℝ E G} [TopologicalSpace M] [ChartedSpace G M] {n : ℕ∞} (q : ThricePuncturedSphere.Puncture) (c : ℝ) {w : ℂ} (hw : w ≠ q.endCenter) (x : M) : ContMDiffAt ((modelWithCornersSelf ℝ ℂ).prod I) (modelWithCornersSelf ℝ ℝ) (↑n) (fun (p : ℂ × M) => (q.endSign * (q.endCoord p.1).re - c).smoothTransition) (w, x)

Away from the center of the end q, the shifted cutoff β(±s_q - c) is C^n as a function on ℂ × M which ignores the point of M.

theorem TauCeti.Floer.contMDiffAt_pairOfPantsPerturbation {M : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → M → ℝ} {E : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace G] {I : ModelWithCorners ℝ E G} [TopologicalSpace M] [ChartedSpace G M] {n : ℕ∞} (hH : ∀ (q : ThricePuncturedSphere.Puncture), Function.Periodic (H q) 1) (hHs : ∀ (q : ThricePuncturedSphere.Puncture), ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) (modelWithCornersSelf ℝ ℝ) (↑n) (Function.uncurry (H q))) (w : ThricePuncturedSphere) (x : M) : ContMDiffAt ((modelWithCornersSelf ℝ ℂ).prod I) (modelWithCornersSelf ℝ (ℂ →L[ℝ] ℝ)) (↑n) (fun (p : ℂ × M) => pairOfPantsPerturbation H p.1 p.2) (↑w, x)

The perturbation is smooth. For Hamiltonians of period one which are C^n on ℝ × M, the perturbation is C^n on S × M, where S = ℂ ∖ {0, 1} is the thrice-punctured sphere.

theorem TauCeti.Floer.contDiffAt_pairOfPantsPerturbation_prod {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] {H : ThricePuncturedSphere.Puncture → ℝ → V → ℝ} {n : ℕ∞} (hH : ∀ (q : ThricePuncturedSphere.Puncture), Function.Periodic (H q) 1) (hHs : ∀ (q : ThricePuncturedSphere.Puncture), ContDiff ℝ (↑n) (Function.uncurry (H q))) {w : ℂ} (hw : w ≠ 0 ∧ w ≠ 1) (x : V) : ContDiffAt ℝ (↑n) (fun (p : ℂ × V) => pairOfPantsPerturbation H p.1 p.2) (w, x)

The perturbation is Cⁿ jointly in the domain point of S and the target point, for Cⁿ Hamiltonians.