The vacuum vortex operator on the Sobolev scale

The gauge-fixed linearization L₀ of the vortex equations at the vacuum (TauCeti.Vortex.vacuumOperator) is a first-order operator with constant real coefficients acting on fields x = (b₁, b₂, p, q). This file extends L₀ and its formal adjoint L₀* to fields whose four components are complex tempered distributions on ℂ, so that they act on Mathlib's L² Sobolev spaces H^s (TemperedDistribution.MemSobolev s 2) for every real s. The complex components are the complexification of the real fields: the coefficients of L₀ are real, and real fields are the ones whose components are real distributions. A field lies in H^s when each of its components does.

The Weitzenböck identities L₀* L₀ = L₀ L₀* = -Δ + 1 / 4 continue to hold on tempered distributions. With the resolvent (-Δ + 1 / 4)⁻¹ of the Laplacian on tempered distributions (TemperedDistribution.laplacianResolvent), they show that L₀ and L₀* are continuous linear automorphisms of the space of tempered fields, with inverses L₀⁻¹ = L₀* (-Δ + 1 / 4)⁻¹ and (L₀*)⁻¹ = L₀ (-Δ + 1 / 4)⁻¹. On the Sobolev scale, L₀ maps H^s to H^{s-1}, since it has order one, while L₀⁻¹ maps H^{s-1} back to H^s, since the resolvent gains two derivatives and L₀* loses one. Hence L₀ : H^s → H^{s-1} is bijective for every s, in particular H^k → H^{k-1} for every integer k, and a tempered field x lies in H^s exactly when L₀ x lies in H^{s-1}. On Schwartz fields the tempered operators agree with vacuumOperator and vacuumAdjoint.

Main declarations

• TauCeti.Vortex.temperedVacuumOperator and TauCeti.Vortex.temperedVacuumAdjoint: L₀ and L₀* on fields of tempered distributions, characterized by their component formulas.
• TauCeti.Vortex.temperedVacuumOperator_toTemperedDistribution and TauCeti.Vortex.temperedVacuumAdjoint_toTemperedDistribution: they extend vacuumOperator and vacuumAdjoint from Schwartz fields.
• TauCeti.Vortex.temperedVacuumAdjoint_temperedVacuumOperator and TauCeti.Vortex.temperedVacuumOperator_temperedVacuumAdjoint: the Weitzenböck identities L₀* L₀ = L₀ L₀* = -Δ + 1 / 4.
• TauCeti.Vortex.temperedVacuumOperatorEquiv and TauCeti.Vortex.temperedVacuumAdjointEquiv: L₀ and L₀* as continuous linear automorphisms of the tempered fields, with inverses given by TauCeti.Vortex.temperedVacuumOperatorEquiv_symm_apply and TauCeti.Vortex.temperedVacuumAdjointEquiv_symm_apply.
• TauCeti.Vortex.memSobolev_temperedVacuumOperator and TauCeti.Vortex.memSobolev_temperedVacuumOperatorEquiv_symm: L₀ : H^s → H^{s-1} and L₀⁻¹ : H^s → H^{s+1}.
• TauCeti.Vortex.memSobolev_temperedVacuumOperator_iff: x ∈ H^s if and only if L₀ x ∈ H^{s-1}; with the automorphism this is the bijectivity of L₀ : H^s → H^{s-1}. The same statements for L₀* are TauCeti.Vortex.memSobolev_temperedVacuumAdjoint, TauCeti.Vortex.memSobolev_temperedVacuumAdjointEquiv_symm and TauCeti.Vortex.memSobolev_temperedVacuumAdjoint_iff.

References

• C. H. Taubes, SW ⇒ Gr: from the Seiberg–Witten equations to pseudo-holomorphic curves, J. Amer. Math. Soc. 9 (1996), 845--918.
• M. Taylor, Partial Differential Equations I, Chapter 4, §1 (the Sobolev spaces H^s).

noncomputable def TauCeti.Vortex.temperedVacuumOperator : (Fin 4 → TemperedDistribution ℂ ℂ) →L[ℂ] Fin 4 → TemperedDistribution ℂ ℂ

The vacuum operator L₀ on fields x = (b₁, b₂, p, q) of complex tempered distributions on ℂ, producing (G, C, H₁, H₂); see the component formulas temperedVacuumOperator_apply_zero through temperedVacuumOperator_apply_three. On Schwartz fields it is vacuumOperator (temperedVacuumOperator_toTemperedDistribution).

noncomputable def TauCeti.Vortex.temperedVacuumAdjoint : (Fin 4 → TemperedDistribution ℂ ℂ) →L[ℂ] Fin 4 → TemperedDistribution ℂ ℂ

The formal adjoint L₀* of the vacuum operator on fields of complex tempered distributions on ℂ; see the component formulas temperedVacuumAdjoint_apply_zero through temperedVacuumAdjoint_apply_three. On Schwartz fields it is vacuumAdjoint (temperedVacuumAdjoint_toTemperedDistribution).

@[simp]

theorem TauCeti.Vortex.temperedVacuumOperator_apply_zero (x : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumOperator x 0 = LineDeriv.lineDerivOp 1 (x 0) + LineDeriv.lineDerivOp Complex.I (x 1) + (1 / 2) • x 3

The gauge component G = ∂₁ b₁ + ∂₂ b₂ + q / 2 of L₀.

@[simp]

theorem TauCeti.Vortex.temperedVacuumOperator_apply_one (x : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumOperator x 1 = LineDeriv.lineDerivOp Complex.I (x 0) - LineDeriv.lineDerivOp 1 (x 1) + (1 / 2) • x 2

The curvature component C = ∂₂ b₁ - ∂₁ b₂ + p / 2 of L₀.

@[simp]

theorem TauCeti.Vortex.temperedVacuumOperator_apply_two (x : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumOperator x 2 = LineDeriv.lineDerivOp 1 (x 2) - LineDeriv.lineDerivOp Complex.I (x 3) - (1 / 2) • x 1

The first ∂bar component H₁ = ∂₁ p - ∂₂ q - b₂ / 2 of L₀.

@[simp]

theorem TauCeti.Vortex.temperedVacuumOperator_apply_three (x : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumOperator x 3 = LineDeriv.lineDerivOp Complex.I (x 2) + LineDeriv.lineDerivOp 1 (x 3) + (1 / 2) • x 0

The second ∂bar component H₂ = ∂₂ p + ∂₁ q + b₁ / 2 of L₀.

@[simp]

theorem TauCeti.Vortex.temperedVacuumAdjoint_apply_zero (y : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumAdjoint y 0 = -LineDeriv.lineDerivOp 1 (y 0) - LineDeriv.lineDerivOp Complex.I (y 1) + (1 / 2) • y 3

The b₁ component -∂₁ G - ∂₂ C + H₂ / 2 of L₀* (G, C, H₁, H₂).

@[simp]

theorem TauCeti.Vortex.temperedVacuumAdjoint_apply_one (y : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumAdjoint y 1 = -LineDeriv.lineDerivOp Complex.I (y 0) + LineDeriv.lineDerivOp 1 (y 1) - (1 / 2) • y 2

The b₂ component -∂₂ G + ∂₁ C - H₁ / 2 of L₀* (G, C, H₁, H₂).

@[simp]

theorem TauCeti.Vortex.temperedVacuumAdjoint_apply_two (y : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumAdjoint y 2 = -LineDeriv.lineDerivOp 1 (y 2) - LineDeriv.lineDerivOp Complex.I (y 3) + (1 / 2) • y 1

The p component -∂₁ H₁ - ∂₂ H₂ + C / 2 of L₀* (G, C, H₁, H₂).

@[simp]

theorem TauCeti.Vortex.temperedVacuumAdjoint_apply_three (y : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumAdjoint y 3 = LineDeriv.lineDerivOp Complex.I (y 2) - LineDeriv.lineDerivOp 1 (y 3) + (1 / 2) • y 0

The q component ∂₂ H₁ - ∂₁ H₂ + G / 2 of L₀* (G, C, H₁, H₂).

Agreement with the vacuum operator on Schwartz fields

theorem TauCeti.Vortex.temperedVacuumOperator_toTemperedDistribution (x : SchwartzMap ℂ (EuclideanSpace ℝ (Fin 4))) : (temperedVacuumOperator fun (i : Fin 4) => (SchwartzMap.toTemperedDistributionCLM ℂ ℂ MeasureTheory.volume) ((SchwartzMap.postcompCLM (Complex.ofRealCLM ∘SL EuclideanSpace.proj i)) x)) = fun (i : Fin 4) => (SchwartzMap.toTemperedDistributionCLM ℂ ℂ MeasureTheory.volume) ((SchwartzMap.postcompCLM (Complex.ofRealCLM ∘SL EuclideanSpace.proj i)) (vacuumOperator x))

temperedVacuumOperator extends vacuumOperator: on the components of a real Schwartz field x, viewed as complex tempered distributions, it gives the components of vacuumOperator x.

theorem TauCeti.Vortex.temperedVacuumAdjoint_toTemperedDistribution (y : SchwartzMap ℂ (EuclideanSpace ℝ (Fin 4))) : (temperedVacuumAdjoint fun (i : Fin 4) => (SchwartzMap.toTemperedDistributionCLM ℂ ℂ MeasureTheory.volume) ((SchwartzMap.postcompCLM (Complex.ofRealCLM ∘SL EuclideanSpace.proj i)) y)) = fun (i : Fin 4) => (SchwartzMap.toTemperedDistributionCLM ℂ ℂ MeasureTheory.volume) ((SchwartzMap.postcompCLM (Complex.ofRealCLM ∘SL EuclideanSpace.proj i)) (vacuumAdjoint y))

temperedVacuumAdjoint extends vacuumAdjoint: on the components of a real Schwartz field y, viewed as complex tempered distributions, it gives the components of vacuumAdjoint y.

The Weitzenböck identities

theorem TauCeti.Vortex.temperedVacuumAdjoint_temperedVacuumOperator (x : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumAdjoint (temperedVacuumOperator x) = fun (i : Fin 4) => -Laplacian.laplacian (x i) + (1 / 4) • x i

The Weitzenböck identity at the vacuum on tempered fields: L₀* L₀ = -Δ + 1 / 4.

theorem TauCeti.Vortex.temperedVacuumOperator_temperedVacuumAdjoint (y : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumOperator (temperedVacuumAdjoint y) = fun (i : Fin 4) => -Laplacian.laplacian (y i) + (1 / 4) • y i

The reverse Weitzenböck identity at the vacuum on tempered fields: L₀ L₀* = -Δ + 1 / 4.

The inverses of the vacuum operator and its adjoint

theorem TauCeti.Vortex.temperedVacuumOperator_injective : Function.Injective ⇑temperedVacuumOperator

The vacuum operator has trivial kernel on tempered fields.

theorem TauCeti.Vortex.temperedVacuumAdjoint_injective : Function.Injective ⇑temperedVacuumAdjoint

The adjoint of the vacuum operator has trivial kernel on tempered fields.

noncomputable def TauCeti.Vortex.temperedVacuumOperatorEquiv : (Fin 4 → TemperedDistribution ℂ ℂ) ≃L[ℂ] Fin 4 → TemperedDistribution ℂ ℂ

The vacuum operator is invertible on tempered fields: L₀ as a continuous linear automorphism of the fields of tempered distributions. Its inverse is L₀⁻¹ = L₀* (-Δ + 1 / 4)⁻¹ (temperedVacuumOperatorEquiv_symm_apply).

noncomputable def TauCeti.Vortex.temperedVacuumAdjointEquiv : (Fin 4 → TemperedDistribution ℂ ℂ) ≃L[ℂ] Fin 4 → TemperedDistribution ℂ ℂ

The adjoint of the vacuum operator is invertible on tempered fields: L₀* as a continuous linear automorphism of the fields of tempered distributions. Its inverse is (L₀*)⁻¹ = L₀ (-Δ + 1 / 4)⁻¹ (temperedVacuumAdjointEquiv_symm_apply).

@[simp]

theorem TauCeti.Vortex.coe_temperedVacuumOperatorEquiv : ⇑temperedVacuumOperatorEquiv = ⇑temperedVacuumOperator

@[simp]

theorem TauCeti.Vortex.coe_temperedVacuumAdjointEquiv : ⇑temperedVacuumAdjointEquiv = ⇑temperedVacuumAdjoint

theorem TauCeti.Vortex.temperedVacuumOperatorEquiv_symm_apply (y : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumOperatorEquiv.symm y = temperedVacuumAdjoint fun (i : Fin 4) => (TemperedDistribution.laplacianResolvent ℂ (1 / 4)) (y i)

The inverse of the vacuum operator on tempered fields is L₀⁻¹ = L₀* (-Δ + 1 / 4)⁻¹.

theorem TauCeti.Vortex.temperedVacuumAdjointEquiv_symm_apply (y : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumAdjointEquiv.symm y = temperedVacuumOperator fun (i : Fin 4) => (TemperedDistribution.laplacianResolvent ℂ (1 / 4)) (y i)

The inverse of the adjoint of the vacuum operator on tempered fields is (L₀*)⁻¹ = L₀ (-Δ + 1 / 4)⁻¹.

@[simp]

theorem TauCeti.Vortex.temperedVacuumOperator_temperedVacuumOperatorEquiv_symm (y : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumOperator (temperedVacuumOperatorEquiv.symm y) = y

@[simp]

theorem TauCeti.Vortex.temperedVacuumOperatorEquiv_symm_temperedVacuumOperator (x : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumOperatorEquiv.symm (temperedVacuumOperator x) = x

@[simp]

theorem TauCeti.Vortex.temperedVacuumAdjoint_temperedVacuumAdjointEquiv_symm (y : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumAdjoint (temperedVacuumAdjointEquiv.symm y) = y

@[simp]

theorem TauCeti.Vortex.temperedVacuumAdjointEquiv_symm_temperedVacuumAdjoint (x : Fin 4 → TemperedDistribution ℂ ℂ) : temperedVacuumAdjointEquiv.symm (temperedVacuumAdjoint x) = x

The Sobolev scale

theorem TauCeti.Vortex.memSobolev_temperedVacuumOperator {x : Fin 4 → TemperedDistribution ℂ ℂ} {s : ℝ} (hx : ∀ (i : Fin 4), TemperedDistribution.MemSobolev s 2 (x i)) (i : Fin 4) : TemperedDistribution.MemSobolev (s - 1) 2 (temperedVacuumOperator x i)

The vacuum operator has order one: L₀ maps H^s to H^{s-1}.

theorem TauCeti.Vortex.memSobolev_temperedVacuumAdjoint {y : Fin 4 → TemperedDistribution ℂ ℂ} {s : ℝ} (hy : ∀ (i : Fin 4), TemperedDistribution.MemSobolev s 2 (y i)) (i : Fin 4) : TemperedDistribution.MemSobolev (s - 1) 2 (temperedVacuumAdjoint y i)

The adjoint of the vacuum operator has order one: L₀* maps H^s to H^{s-1}.

theorem TauCeti.Vortex.memSobolev_temperedVacuumOperatorEquiv_symm {y : Fin 4 → TemperedDistribution ℂ ℂ} {s : ℝ} (hy : ∀ (i : Fin 4), TemperedDistribution.MemSobolev s 2 (y i)) (i : Fin 4) : TemperedDistribution.MemSobolev (s + 1) 2 (temperedVacuumOperatorEquiv.symm y i)

The inverse of the vacuum operator gains one derivative: L₀⁻¹ maps H^s to H^{s+1}.

theorem TauCeti.Vortex.memSobolev_temperedVacuumAdjointEquiv_symm {y : Fin 4 → TemperedDistribution ℂ ℂ} {s : ℝ} (hy : ∀ (i : Fin 4), TemperedDistribution.MemSobolev s 2 (y i)) (i : Fin 4) : TemperedDistribution.MemSobolev (s + 1) 2 (temperedVacuumAdjointEquiv.symm y i)

The inverse of the adjoint of the vacuum operator gains one derivative: (L₀*)⁻¹ maps H^s to H^{s+1}.

theorem TauCeti.Vortex.memSobolev_temperedVacuumOperator_iff {x : Fin 4 → TemperedDistribution ℂ ℂ} {s : ℝ} : (∀ (i : Fin 4), TemperedDistribution.MemSobolev (s - 1) 2 (temperedVacuumOperator x i)) ↔ ∀ (i : Fin 4), TemperedDistribution.MemSobolev s 2 (x i)

The vacuum operator restricts to a bijection H^s → H^{s-1}: a tempered field x lies in H^s if and only if L₀ x lies in H^{s-1}. Since L₀ is bijective on tempered fields (temperedVacuumOperatorEquiv), it restricts to a bijection from H^s onto H^{s-1}, for every real s.

theorem TauCeti.Vortex.memSobolev_temperedVacuumAdjoint_iff {y : Fin 4 → TemperedDistribution ℂ ℂ} {s : ℝ} : (∀ (i : Fin 4), TemperedDistribution.MemSobolev (s - 1) 2 (temperedVacuumAdjoint y i)) ↔ ∀ (i : Fin 4), TemperedDistribution.MemSobolev s 2 (y i)

The adjoint of the vacuum operator restricts to a bijection H^s → H^{s-1}: a tempered field y lies in H^s if and only if L₀* y lies in H^{s-1}. Since L₀* is bijective on tempered fields (temperedVacuumAdjointEquiv), it restricts to a bijection from H^s onto H^{s-1}, for every real s.