Products of curves are totally real in the symmetric power

Let α be a Hausdorff complex curve, so that its n-th symmetric power Sym α n is a complex manifold for its elementary-symmetric charts (TauCeti.isManifold_symChartedSpace). Given real curves γ₁, …, γₙ in α, immersed at parameters t₁, …, tₙ whose points γᵢ(tᵢ) are pairwise distinct, the map

Γ : ℝⁿ → Sym α n, (s₁, …, sₙ) ↦ {γ₁(s₁), …, γₙ(sₙ)}

is an immersion at (t₁, …, tₙ) in every chart of Sym α n, and its tangent space there is a maximal totally real subspace of the complex coordinate space: it meets its image under multiplication by i only in 0, and spans with it. When γᵢ locally parametrizes the i-th attaching curve αᵢ of a Heegaard diagram, Γ locally parametrizes the torus T_α = α₁ × ⋯ × αₙ (TauCeti.Sym.pi, TauCeti.Sym.ofFn_mem_pi), whose points are always such tuples of distinct points because attaching curves are pairwise disjoint. Thus, after supplying those local parametrizations, the result gives the tangent-space criterion needed for the tori in the holomorphic-disk boundary conditions of Ozsváth–Szabó. Their embedded, closed-torus result is TauCeti.Sym.piHomeomorph.

Main declarations

• TauCeti.differentiableAt_symChartAt_ofFn: the product of the curves, read in a chart of the symmetric power, is real-differentiable.
• TauCeti.fderiv_symChartAt_ofFn_injective: it is an immersion.
• TauCeti.isMaximalTotallyReal_range_fderiv_symChartAt_ofFn: its tangent space is maximal totally real.

References

• P. Ozsváth and Z. Szabó, Holomorphic disks and topological invariants for closed three-manifolds, Ann. of Math. 159 (2004), arXiv:math/0101206, §2.

Products of curves in the symmetric power

theorem TauCeti.differentiableAt_symChartAt_ofFn {α : Type u_1} [TopologicalSpace α] [T2Space α] [ChartedSpace ℂ α] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 α] {n : ℕ} {γ : Fin n → ℝ → α} {t₀ : Fin n → ℝ} {v : Fin n → ℂ} (hinj : Function.Injective fun (i : Fin n) => γ i (t₀ i)) (hγ : ∀ (i : Fin n), ContinuousAt (γ i) (t₀ i)) (hv : ∀ (i : Fin n), HasDerivAt (fun (t : ℝ) => ↑(chartAt ℂ (γ i (t₀ i))) (γ i t)) (v i) (t₀ i)) (s : Sym α n) (hs : (Sym.ofFn fun (i : Fin n) => γ i (t₀ i)) ∈ (symChartAt s).source) : DifferentiableAt ℝ (fun (t : Fin n → ℝ) => ↑(symChartAt s) (Sym.ofFn fun (i : Fin n) => γ i (t i))) t₀

The product of real curves in a complex curve, read in a chart of the symmetric power, is real-differentiable at a parameter where the curves are differentiable and pass through pairwise distinct points.

theorem TauCeti.fderiv_symChartAt_ofFn_injective {α : Type u_1} [TopologicalSpace α] [T2Space α] [ChartedSpace ℂ α] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 α] {n : ℕ} {γ : Fin n → ℝ → α} {t₀ : Fin n → ℝ} {v : Fin n → ℂ} (hinj : Function.Injective fun (i : Fin n) => γ i (t₀ i)) (hγ : ∀ (i : Fin n), ContinuousAt (γ i) (t₀ i)) (hv : ∀ (i : Fin n), HasDerivAt (fun (t : ℝ) => ↑(chartAt ℂ (γ i (t₀ i))) (γ i t)) (v i) (t₀ i)) (hv0 : ∀ (i : Fin n), v i ≠ 0) (s : Sym α n) (hs : (Sym.ofFn fun (i : Fin n) => γ i (t₀ i)) ∈ (symChartAt s).source) : Function.Injective ⇑(fderiv ℝ (fun (t : Fin n → ℝ) => ↑(symChartAt s) (Sym.ofFn fun (i : Fin n) => γ i (t i))) t₀)

The product of immersed curves is an immersion into the symmetric power. If real curves γ i in a complex curve have nonzero velocity at t₀ i and pass there through pairwise distinct points, then t ↦ {γ₁(t₁), …, γₙ(tₙ)}, read in any chart of the symmetric power, has injective derivative at t₀.

theorem TauCeti.isMaximalTotallyReal_range_fderiv_symChartAt_ofFn {α : Type u_1} [TopologicalSpace α] [T2Space α] [ChartedSpace ℂ α] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 α] {n : ℕ} {γ : Fin n → ℝ → α} {t₀ : Fin n → ℝ} {v : Fin n → ℂ} (hinj : Function.Injective fun (i : Fin n) => γ i (t₀ i)) (hγ : ∀ (i : Fin n), ContinuousAt (γ i) (t₀ i)) (hv : ∀ (i : Fin n), HasDerivAt (fun (t : ℝ) => ↑(chartAt ℂ (γ i (t₀ i))) (γ i t)) (v i) (t₀ i)) (hv0 : ∀ (i : Fin n), v i ≠ 0) (s : Sym α n) (hs : (Sym.ofFn fun (i : Fin n) => γ i (t₀ i)) ∈ (symChartAt s).source) : IsMaximalTotallyReal (AlmostComplexStructure.ofComplexModule (Fin n → ℂ)).toLinearMap (↑(fderiv ℝ (fun (t : Fin n → ℝ) => ↑(symChartAt s) (Sym.ofFn fun (i : Fin n) => γ i (t i))) t₀)).range

Products of immersed curves are maximal totally real in the symmetric power. If real curves γ i in a complex curve have nonzero velocity at t₀ i and pass there through pairwise distinct points, then in every chart of the symmetric power the tangent space of t ↦ {γ₁(t₁), …, γₙ(tₙ)} at t₀ is a maximal totally real subspace of Fin n → ℂ: it is complementary to its image under multiplication by i. Applied to local parametrizations of pairwise disjoint attaching curves, this supplies the required tangent-space criterion for the corresponding torus in Sym^g(Σ).