The gauge-fixed vortex operator at a general field

This file continues TauCeti.Analysis.PDE.Vortex.Deformation, in the same coordinates: a field x = (A₁, A₂, p, q) represents a = i (A₁ ds + A₂ dt) and α = 2 (p + i q), and the coefficient metric |b|² + |δα|² / 4 on variations is the Euclidean metric. The infinitesimal gauge action d₀ = gaugeDirection x sends a real phase f to (-∂₁ f, -∂₂ f, -q f, p f), and its formal L² adjoint is

d₀* y = ∂₁ y₀ + ∂₂ y₁ + p y₃ - q y₂ (gaugeAdjoint).

The gauge-fixed operator L_x = d₀* ⊕ d₁ (gaugeFixedOperator) puts this gauge-fixing row in front of the three rows of linearizedEquation, and gaugeFixedAdjoint is its formal adjoint L_x* for the Euclidean metrics on fields and on ℝ ⊕ ℝ ⊕ ℂ. At the vacuum they are the operators vacuumOperator and vacuumAdjoint (gaugeFixedOperator_vacuumField, gaugeFixedAdjoint_vacuumField).

Main results

• gaugeAdjoint_gaugeDirection: d₀* d₀ f = -Δ f + (|α|² / 4) f pointwise, at every field.
• gaugeFixedOperator_gaugeFixedAdjoint: the pointwise Weitzenböck formula for L_x L_x* at every field, with the vortex defects equation x appearing explicitly. In complex notation, with φ = α / 2, η = (ξ, ζ), ∇ = d + a and the complex defect E = ∂bar_a α, it reads L_x L_x* (ξ, ζ) = (-Δ ξ + |φ|² ξ + i (conj ζ) E, -Δ_a ζ + (*iF_a + |φ|²) ζ + i E (conj ξ)).
• gaugeFixedOperator_gaugeFixedAdjoint_of_equation_eq_zero: at a point where the vortex equation holds, L_x L_x* = (-Δ + |φ|²) ⊕ (-Δ_a + 1 / 8 + |φ|² / 2). Both summands are nonnegative Schrödinger operators, which is how the cokernel of L_x is shown to vanish at a vortex.
• gaugeFixedAdjoint_gaugeFixedOperator: the pointwise Weitzenböck formula for L_x* L_x at every field. In complex notation, with κ = curvature x z and the holomorphic derivative ∂_a φ, it reads L_x* L_x (ξ, ζ) = ((-Δ + |φ|²) ξ + K ζ, (-Δ_a + κ + |φ|²) ζ + Kᵀ ξ), where the real matrix K is built from the components of 2 ∂_a φ; the defects ∂bar_a α do not enter.
• gaugeFixedAdjoint_gaugeFixedOperator_of_equation_eq_zero: at a point where the vortex equation holds, κ = |φ|² / 2 - 1 / 8 and 2 ∂_a φ = ∇₁ α, so the section potential is 3 |φ|² / 2 - 1 / 8 and K is multiplication by i conj (∇₁ α). Unlike L_x L_x*, this operator is not a sum of nonnegative Schrödinger operators, since the coupling K has no sign; small |∇₁ α| and |α| close to one suffice for it to be coercive.
• integral_mul_gaugeAdjoint and integral_inner_gaugeFixedOperator: the integration-by-parts identities ∫ f d₀* y = ∫ ⟪d₀ f, y⟫ and ∫ ⟪L_x y, η⟫ = ∫ ⟪y, L_x* η⟫, for C¹ data with one factor compactly supported and any additive Haar measure.

These are smooth differential expressions; no completed field space, Fredholm property or cokernel statement is asserted.

References

• A. Jaffe and C. H. Taubes, Vortices and Monopoles, Progress in Physics 2, Birkhäuser, 1980.
• C. H. Taubes, Arbitrary N-vortex solutions to the first order Ginzburg–Landau equations, Comm. Math. Phys. 72 (1980), 277--292.

noncomputable def TauCeti.Vortex.gaugeAdjoint (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : ℝ

The formal L² adjoint d₀* of the infinitesimal gauge action gaugeDirection x, applied to a variation y: d₀* y = ∂₁ y₀ + ∂₂ y₁ + p y₃ - q y₂. See integral_mul_gaugeAdjoint.

noncomputable def TauCeti.Vortex.gaugeFixedOperator (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : EuclideanSpace ℝ (Fin 4)

The gauge-fixed linearization L_x = d₀* ⊕ d₁ of the vortex equation at the field x: the gauge-fixing row gaugeAdjoint x y followed by the three rows of linearizedEquation x y.

noncomputable def TauCeti.Vortex.gaugeFixedAdjoint (x η : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : EuclideanSpace ℝ (Fin 4)

The formal L² adjoint L_x* of gaugeFixedOperator x, for the Euclidean metrics on the coordinates of variations and of ℝ ⊕ ℝ ⊕ ℂ. See integral_inner_gaugeFixedOperator.

@[simp]

theorem TauCeti.Vortex.gaugeAdjoint_def (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : gaugeAdjoint x y z = (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 0) z) 1 + (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 1) z) Complex.I + (x z).ofLp 2 * (y z).ofLp 3 - (x z).ofLp 3 * (y z).ofLp 2

The defining formula of d₀*.

@[simp]

theorem TauCeti.Vortex.gaugeFixedOperator_apply_zero (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (gaugeFixedOperator x y z).ofLp 0 = gaugeAdjoint x y z

The gauge-fixing row of L_x.

@[simp]

theorem TauCeti.Vortex.gaugeFixedOperator_apply_one (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (gaugeFixedOperator x y z).ofLp 1 = (linearizedEquation x y z).ofLp 0

The curvature row of L_x.

@[simp]

theorem TauCeti.Vortex.gaugeFixedOperator_apply_two (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (gaugeFixedOperator x y z).ofLp 2 = (linearizedEquation x y z).ofLp 1

The real ∂bar row of L_x.

@[simp]

theorem TauCeti.Vortex.gaugeFixedOperator_apply_three (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (gaugeFixedOperator x y z).ofLp 3 = (linearizedEquation x y z).ofLp 2

The imaginary ∂bar row of L_x.

@[simp]

theorem TauCeti.Vortex.gaugeFixedAdjoint_apply_zero (x η : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (gaugeFixedAdjoint x η z).ofLp 0 = -(fderiv ℝ (fun (w : ℂ) => (η w).ofLp 0) z) 1 - (fderiv ℝ (fun (w : ℂ) => (η w).ofLp 1) z) Complex.I + (x z).ofLp 2 * (η z).ofLp 3 - (x z).ofLp 3 * (η z).ofLp 2

The first connection component of L_x*.

@[simp]

theorem TauCeti.Vortex.gaugeFixedAdjoint_apply_one (x η : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (gaugeFixedAdjoint x η z).ofLp 1 = -(fderiv ℝ (fun (w : ℂ) => (η w).ofLp 0) z) Complex.I + (fderiv ℝ (fun (w : ℂ) => (η w).ofLp 1) z) 1 - (x z).ofLp 2 * (η z).ofLp 2 - (x z).ofLp 3 * (η z).ofLp 3

The second connection component of L_x*.

@[simp]

theorem TauCeti.Vortex.gaugeFixedAdjoint_apply_two (x η : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (gaugeFixedAdjoint x η z).ofLp 2 = -(fderiv ℝ (fun (w : ℂ) => (η w).ofLp 2) z) 1 - (fderiv ℝ (fun (w : ℂ) => (η w).ofLp 3) z) Complex.I - (x z).ofLp 1 * (η z).ofLp 2 + (x z).ofLp 0 * (η z).ofLp 3 - (x z).ofLp 3 * (η z).ofLp 0 + (x z).ofLp 2 * (η z).ofLp 1

The real section component of L_x*.

@[simp]

theorem TauCeti.Vortex.gaugeFixedAdjoint_apply_three (x η : ℂ → EuclideanSpace ℝ (Fin 4)) (z : ℂ) : (gaugeFixedAdjoint x η z).ofLp 3 = -(fderiv ℝ (fun (w : ℂ) => (η w).ofLp 3) z) 1 + (fderiv ℝ (fun (w : ℂ) => (η w).ofLp 2) z) Complex.I - (x z).ofLp 0 * (η z).ofLp 2 - (x z).ofLp 1 * (η z).ofLp 3 + (x z).ofLp 2 * (η z).ofLp 0 + (x z).ofLp 3 * (η z).ofLp 1

The imaginary section component of L_x*.

theorem TauCeti.Vortex.gaugeAdjoint_add (x : ℂ → EuclideanSpace ℝ (Fin 4)) {y v : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hy : DifferentiableAt ℝ y z) (hv : DifferentiableAt ℝ v z) : gaugeAdjoint x (y + v) z = gaugeAdjoint x y z + gaugeAdjoint x v z

d₀* preserves addition of variations differentiable at the point.

theorem TauCeti.Vortex.gaugeAdjoint_smul (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (t : ℝ) (z : ℂ) : gaugeAdjoint x (t • y) z = t * gaugeAdjoint x y z

d₀* commutes with real scalar multiplication of variations.

theorem TauCeti.Vortex.gaugeFixedOperator_add (x : ℂ → EuclideanSpace ℝ (Fin 4)) {y v : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hy : DifferentiableAt ℝ y z) (hv : DifferentiableAt ℝ v z) : gaugeFixedOperator x (y + v) z = gaugeFixedOperator x y z + gaugeFixedOperator x v z

L_x preserves addition of variations differentiable at the point.

theorem TauCeti.Vortex.gaugeFixedOperator_congr_nhds (x : ℂ → EuclideanSpace ℝ (Fin 4)) {y v : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (h : y =ᶠ[nhds z] v) : gaugeFixedOperator x y z = gaugeFixedOperator x v z

L_x y at a point depends only on the germ of the variation y there.

theorem TauCeti.Vortex.gaugeFixedOperator_smul (x y : ℂ → EuclideanSpace ℝ (Fin 4)) (t : ℝ) (z : ℂ) : gaugeFixedOperator x (t • y) z = t • gaugeFixedOperator x y z

L_x commutes with real scalar multiplication of variations.

@[simp]

theorem TauCeti.Vortex.gaugeFixedOperator_zero (x : ℂ → EuclideanSpace ℝ (Fin 4)) : gaugeFixedOperator x 0 = 0

L_x sends the zero variation to zero.

theorem TauCeti.Vortex.gaugeFixedAdjoint_add (x : ℂ → EuclideanSpace ℝ (Fin 4)) {η ν : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hη : DifferentiableAt ℝ η z) (hν : DifferentiableAt ℝ ν z) : gaugeFixedAdjoint x (η + ν) z = gaugeFixedAdjoint x η z + gaugeFixedAdjoint x ν z

L_x* preserves addition of arguments differentiable at the point.

theorem TauCeti.Vortex.gaugeFixedAdjoint_smul (x η : ℂ → EuclideanSpace ℝ (Fin 4)) (t : ℝ) (z : ℂ) : gaugeFixedAdjoint x (t • η) z = t • gaugeFixedAdjoint x η z

L_x* commutes with real scalar multiplication.

def TauCeti.Vortex.gaugeFixedAdjointSymbol (d : ℂ →L[ℝ] ℝ) (v : EuclideanSpace ℝ (Fin 4)) : EuclideanSpace ℝ (Fin 4)

The principal symbol of the gauge-fixed vortex adjoint, acting on a real covector and a target field value. It is independent of the vortex coefficients.

theorem TauCeti.Vortex.gaugeFixedAdjointSymbol_def (d : ℂ →L[ℝ] ℝ) (v : EuclideanSpace ℝ (Fin 4)) : gaugeFixedAdjointSymbol d v = !₂[-d 1 * v.ofLp 0 - d Complex.I * v.ofLp 1, -d Complex.I * v.ofLp 0 + d 1 * v.ofLp 1, -d 1 * v.ofLp 2 - d Complex.I * v.ofLp 3, -d 1 * v.ofLp 3 + d Complex.I * v.ofLp 2]

Coordinate formula for the principal symbol of the adjoint.

@[simp]

theorem TauCeti.Vortex.gaugeFixedAdjointSymbol_apply_zero (d : ℂ →L[ℝ] ℝ) (v : EuclideanSpace ℝ (Fin 4)) : (gaugeFixedAdjointSymbol d v).ofLp 0 = -d 1 * v.ofLp 0 - d Complex.I * v.ofLp 1

The first connection component of the adjoint symbol.

@[simp]

theorem TauCeti.Vortex.gaugeFixedAdjointSymbol_apply_one (d : ℂ →L[ℝ] ℝ) (v : EuclideanSpace ℝ (Fin 4)) : (gaugeFixedAdjointSymbol d v).ofLp 1 = -d Complex.I * v.ofLp 0 + d 1 * v.ofLp 1

The second connection component of the adjoint symbol.

@[simp]

theorem TauCeti.Vortex.gaugeFixedAdjointSymbol_apply_two (d : ℂ →L[ℝ] ℝ) (v : EuclideanSpace ℝ (Fin 4)) : (gaugeFixedAdjointSymbol d v).ofLp 2 = -d 1 * v.ofLp 2 - d Complex.I * v.ofLp 3

The real section component of the adjoint symbol.

@[simp]

theorem TauCeti.Vortex.gaugeFixedAdjointSymbol_apply_three (d : ℂ →L[ℝ] ℝ) (v : EuclideanSpace ℝ (Fin 4)) : (gaugeFixedAdjointSymbol d v).ofLp 3 = -d 1 * v.ofLp 3 + d Complex.I * v.ofLp 2

The imaginary section component of the adjoint symbol.

theorem TauCeti.Vortex.norm_sq_gaugeFixedAdjointSymbol (d : ℂ →L[ℝ] ℝ) (v : EuclideanSpace ℝ (Fin 4)) : ‖gaugeFixedAdjointSymbol d v‖ ^ 2 = ‖d‖ ^ 2 * ‖v‖ ^ 2

The adjoint symbol preserves squared norms up to the squared covector norm.

@[simp]

theorem TauCeti.Vortex.gaugeFixedAdjointSymbol_smul_left (r : ℝ) (d : ℂ →L[ℝ] ℝ) (v : EuclideanSpace ℝ (Fin 4)) : gaugeFixedAdjointSymbol (r • d) v = r • gaugeFixedAdjointSymbol d v

The adjoint symbol commutes with real scaling of the covector.

@[simp]

theorem TauCeti.Vortex.gaugeFixedAdjointSymbol_smul_right (d : ℂ →L[ℝ] ℝ) (r : ℝ) (v : EuclideanSpace ℝ (Fin 4)) : gaugeFixedAdjointSymbol d (r • v) = r • gaugeFixedAdjointSymbol d v

The adjoint symbol commutes with real scaling of the field value.

theorem TauCeti.Vortex.gaugeFixedAdjoint_fun_smul (x : ℂ → EuclideanSpace ℝ (Fin 4)) {η : ℂ → EuclideanSpace ℝ (Fin 4)} {w : ℂ → ℝ} {z : ℂ} (hw : DifferentiableAt ℝ w z) (hη : DifferentiableAt ℝ η z) : gaugeFixedAdjoint x (fun (t : ℂ) => w t • η t) z = w z • gaugeFixedAdjoint x η z + gaugeFixedAdjointSymbol (fderiv ℝ w z) (η z)

The adjoint's Leibniz rule for a real weight, with its exact symbol commutator.

theorem TauCeti.Vortex.gaugeAdjoint_gaugeDirection (x : ℂ → EuclideanSpace ℝ (Fin 4)) {f : ℂ → ℝ} {z : ℂ} (hf : ContDiffAt ℝ 2 f z) : gaugeAdjoint x (gaugeDirection x f) z = -Laplacian.laplacian f z + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * f z

The gauge Laplacian: at every field, d₀* d₀ f = -Δ f + (|α|² / 4) f, where |α|² / 4 = p² + q². No regularity of the field is needed.

theorem TauCeti.Vortex.gaugeFixedOperator_gaugeFixedAdjoint {x η : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hx : DifferentiableAt ℝ x z) (hη : ContDiffAt ℝ 2 η z) : gaugeFixedOperator x (gaugeFixedAdjoint x η) z = !₂[-Laplacian.laplacian (fun (w : ℂ) => (η w).ofLp 0) z + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (η z).ofLp 0 - (η z).ofLp 2 * (equation x z).ofLp 2 + (η z).ofLp 3 * (equation x z).ofLp 1, -Laplacian.laplacian (fun (w : ℂ) => (η w).ofLp 1) z + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (η z).ofLp 1 + (η z).ofLp 2 * (equation x z).ofLp 1 + (η z).ofLp 3 * (equation x z).ofLp 2, -Laplacian.laplacian (fun (w : ℂ) => (η w).ofLp 2) z + ((equation x z).ofLp 0 + 1 / 8 + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) / 2 + (x z).ofLp 0 ^ 2 + (x z).ofLp 1 ^ 2) * (η z).ofLp 2 + ((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 0) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 1) z) Complex.I) * (η z).ofLp 3 + 2 * ((x z).ofLp 0 * (fderiv ℝ (fun (w : ℂ) => (η w).ofLp 3) z) 1 + (x z).ofLp 1 * (fderiv ℝ (fun (w : ℂ) => (η w).ofLp 3) z) Complex.I) - (equation x z).ofLp 2 * (η z).ofLp 0 + (equation x z).ofLp 1 * (η z).ofLp 1, -Laplacian.laplacian (fun (w : ℂ) => (η w).ofLp 3) z + ((equation x z).ofLp 0 + 1 / 8 + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) / 2 + (x z).ofLp 0 ^ 2 + (x z).ofLp 1 ^ 2) * (η z).ofLp 3 - ((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 0) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 1) z) Complex.I) * (η z).ofLp 2 - 2 * ((x z).ofLp 0 * (fderiv ℝ (fun (w : ℂ) => (η w).ofLp 2) z) 1 + (x z).ofLp 1 * (fderiv ℝ (fun (w : ℂ) => (η w).ofLp 2) z) Complex.I) + (equation x z).ofLp 1 * (η z).ofLp 0 + (equation x z).ofLp 2 * (η z).ofLp 1]

The Weitzenböck formula for L_x L_x* at an arbitrary field, with the vortex defects E = equation x z displayed. With P = p² + q² = |α|² / 4, the connection part is (-Δ + P) η plus defect couplings, while the section part is -Δ_a ζ + (E₀ + 1 / 8 + P / 2) ζ plus defect couplings, where -Δ_a is the covariant Laplacian of ζ = η₂ + i η₃ for ∇ = d + a and E₀ + 1 / 8 - P / 2 = *iF_a. In real coordinates -Δ_a ζ = -Δ ζ - i (∂₁ A₁ + ∂₂ A₂) ζ - 2 i (A₁ ∂₁ ζ + A₂ ∂₂ ζ) + |A|² ζ.

theorem TauCeti.Vortex.gaugeFixedOperator_gaugeFixedAdjoint_of_equation_eq_zero {x η : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hx : DifferentiableAt ℝ x z) (hη : ContDiffAt ℝ 2 η z) (hsol : equation x z = 0) : gaugeFixedOperator x (gaugeFixedAdjoint x η) z = !₂[-Laplacian.laplacian (fun (w : ℂ) => (η w).ofLp 0) z + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (η z).ofLp 0, -Laplacian.laplacian (fun (w : ℂ) => (η w).ofLp 1) z + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (η z).ofLp 1, -Laplacian.laplacian (fun (w : ℂ) => (η w).ofLp 2) z + (1 / 8 + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) / 2 + (x z).ofLp 0 ^ 2 + (x z).ofLp 1 ^ 2) * (η z).ofLp 2 + ((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 0) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 1) z) Complex.I) * (η z).ofLp 3 + 2 * ((x z).ofLp 0 * (fderiv ℝ (fun (w : ℂ) => (η w).ofLp 3) z) 1 + (x z).ofLp 1 * (fderiv ℝ (fun (w : ℂ) => (η w).ofLp 3) z) Complex.I), -Laplacian.laplacian (fun (w : ℂ) => (η w).ofLp 3) z + (1 / 8 + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) / 2 + (x z).ofLp 0 ^ 2 + (x z).ofLp 1 ^ 2) * (η z).ofLp 3 - ((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 0) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 1) z) Complex.I) * (η z).ofLp 2 - 2 * ((x z).ofLp 0 * (fderiv ℝ (fun (w : ℂ) => (η w).ofLp 2) z) 1 + (x z).ofLp 1 * (fderiv ℝ (fun (w : ℂ) => (η w).ofLp 2) z) Complex.I)]

The Weitzenböck formula at a vortex: where the vortex equation holds, L_x L_x* = (-Δ + P) ⊕ (-Δ_a + 1 / 8 + P / 2) with P = p² + q² = |α|² / 4. The section part is displayed in real coordinates as in gaugeFixedOperator_gaugeFixedAdjoint.

theorem TauCeti.Vortex.gaugeFixedAdjoint_gaugeFixedOperator {x y : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hx : DifferentiableAt ℝ x z) (hy : ContDiffAt ℝ 2 y z) : gaugeFixedAdjoint x (gaugeFixedOperator x y) z = !₂[-Laplacian.laplacian (fun (w : ℂ) => (y w).ofLp 0) z + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (y z).ofLp 0 + ((x z).ofLp 0 * (x z).ofLp 2 + (x z).ofLp 1 * (x z).ofLp 3 - (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) Complex.I + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) 1) * (y z).ofLp 2 - ((x z).ofLp 1 * (x z).ofLp 2 - (x z).ofLp 0 * (x z).ofLp 3 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) Complex.I) * (y z).ofLp 3, -Laplacian.laplacian (fun (w : ℂ) => (y w).ofLp 1) z + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (y z).ofLp 1 + ((x z).ofLp 1 * (x z).ofLp 2 - (x z).ofLp 0 * (x z).ofLp 3 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) Complex.I) * (y z).ofLp 2 + ((x z).ofLp 0 * (x z).ofLp 2 + (x z).ofLp 1 * (x z).ofLp 3 - (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) Complex.I + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) 1) * (y z).ofLp 3, -Laplacian.laplacian (fun (w : ℂ) => (y w).ofLp 2) z + (curvature x z + (x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2 + (x z).ofLp 0 ^ 2 + (x z).ofLp 1 ^ 2) * (y z).ofLp 2 + ((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 0) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 1) z) Complex.I) * (y z).ofLp 3 + 2 * ((x z).ofLp 0 * (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 3) z) 1 + (x z).ofLp 1 * (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 3) z) Complex.I) + ((x z).ofLp 0 * (x z).ofLp 2 + (x z).ofLp 1 * (x z).ofLp 3 - (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) Complex.I + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) 1) * (y z).ofLp 0 + ((x z).ofLp 1 * (x z).ofLp 2 - (x z).ofLp 0 * (x z).ofLp 3 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) Complex.I) * (y z).ofLp 1, -Laplacian.laplacian (fun (w : ℂ) => (y w).ofLp 3) z + (curvature x z + (x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2 + (x z).ofLp 0 ^ 2 + (x z).ofLp 1 ^ 2) * (y z).ofLp 3 - ((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 0) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 1) z) Complex.I) * (y z).ofLp 2 - 2 * ((x z).ofLp 0 * (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 2) z) 1 + (x z).ofLp 1 * (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 2) z) Complex.I) - ((x z).ofLp 1 * (x z).ofLp 2 - (x z).ofLp 0 * (x z).ofLp 3 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) Complex.I) * (y z).ofLp 0 + ((x z).ofLp 0 * (x z).ofLp 2 + (x z).ofLp 1 * (x z).ofLp 3 - (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 2) z) Complex.I + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 3) z) 1) * (y z).ofLp 1]

The Weitzenböck formula for L_x* L_x at an arbitrary field. With P = p² + q² = |α|² / 4 and κ = curvature x z, so that F_a = i κ ds ∧ dt, the connection part is (-Δ + P) ξ and the section part is -Δ_a ζ + (κ + P) ζ, with the covariant Laplacian -Δ_a of ζ = y₂ + i y₃ displayed in real coordinates as in gaugeFixedOperator_gaugeFixedAdjoint. The two parts are coupled at order zero through the real coefficients d + i c = ∇₁ φ - i ∇₂ φ of the holomorphic derivative 2 ∂_a φ of φ = α / 2, and the defects ∂bar_a α do not appear.

theorem TauCeti.Vortex.gaugeFixedAdjoint_gaugeFixedOperator_of_equation_eq_zero {x y : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hx : DifferentiableAt ℝ x z) (hy : ContDiffAt ℝ 2 y z) (hsol : equation x z = 0) : gaugeFixedAdjoint x (gaugeFixedOperator x y) z = !₂[-Laplacian.laplacian (fun (w : ℂ) => (y w).ofLp 0) z + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (y z).ofLp 0 + (covariantDerivative x z 1).im * (y z).ofLp 2 - (covariantDerivative x z 1).re * (y z).ofLp 3, -Laplacian.laplacian (fun (w : ℂ) => (y w).ofLp 1) z + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (y z).ofLp 1 + (covariantDerivative x z 1).re * (y z).ofLp 2 + (covariantDerivative x z 1).im * (y z).ofLp 3, -Laplacian.laplacian (fun (w : ℂ) => (y w).ofLp 2) z + (3 * ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) / 2 - 1 / 8 + (x z).ofLp 0 ^ 2 + (x z).ofLp 1 ^ 2) * (y z).ofLp 2 + ((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 0) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 1) z) Complex.I) * (y z).ofLp 3 + 2 * ((x z).ofLp 0 * (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 3) z) 1 + (x z).ofLp 1 * (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 3) z) Complex.I) + (covariantDerivative x z 1).im * (y z).ofLp 0 + (covariantDerivative x z 1).re * (y z).ofLp 1, -Laplacian.laplacian (fun (w : ℂ) => (y w).ofLp 3) z + (3 * ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) / 2 - 1 / 8 + (x z).ofLp 0 ^ 2 + (x z).ofLp 1 ^ 2) * (y z).ofLp 3 - ((fderiv ℝ (fun (w : ℂ) => (x w).ofLp 0) z) 1 + (fderiv ℝ (fun (w : ℂ) => (x w).ofLp 1) z) Complex.I) * (y z).ofLp 2 - 2 * ((x z).ofLp 0 * (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 2) z) 1 + (x z).ofLp 1 * (fderiv ℝ (fun (w : ℂ) => (y w).ofLp 2) z) Complex.I) - (covariantDerivative x z 1).re * (y z).ofLp 0 + (covariantDerivative x z 1).im * (y z).ofLp 1]

The Weitzenböck formula for L_x* L_x at a vortex. Where the vortex equation holds, the curvature is κ = P / 2 - 1 / 8 and ∂bar_a α = 0, so the section potential is 3 P / 2 - 1 / 8 and the coupling coefficients are the components of ∇₁ α (covariantDerivative x z 1). With P = p² + q² = |α|² / 4, in complex notation L_x* L_x (ξ, ζ) = ((-Δ + P) ξ + K ζ, (-Δ_a + 3 P / 2 - 1 / 8) ζ + Kᵀ ξ), where K is the real 2 × 2 matrix of multiplication by i conj (∇₁ α). At the vacuum, P = 1 / 4 and ∇α = 0, this is L₀* L₀ = -Δ + 1 / 4.

theorem TauCeti.Vortex.gaugeFixedOperator_vacuumField (y : SchwartzMap ℂ (EuclideanSpace ℝ (Fin 4))) (z : ℂ) : gaugeFixedOperator vacuumField (⇑y) z = (vacuumOperator y) z

At the vacuum, the gauge-fixed operator is vacuumOperator.

theorem TauCeti.Vortex.gaugeFixedAdjoint_vacuumField (η : SchwartzMap ℂ (EuclideanSpace ℝ (Fin 4))) (z : ℂ) : gaugeFixedAdjoint vacuumField (⇑η) z = (vacuumAdjoint η) z

At the vacuum, the formal adjoint of the gauge-fixed operator is vacuumAdjoint.

theorem TauCeti.Vortex.continuous_gaugeAdjoint {x y : ℂ → EuclideanSpace ℝ (Fin 4)} (hx : Continuous x) (hy : ContDiff ℝ 1 y) : Continuous (gaugeAdjoint x y)

d₀* y is continuous for a continuous field and a C¹ variation.

theorem TauCeti.Vortex.contDiff_gaugeFixedAdjoint {x y : ℂ → EuclideanSpace ℝ (Fin 4)} {n : WithTop ℕ∞} (hx : ContDiff ℝ n x) (hy : ContDiff ℝ (n + 1) y) : ContDiff ℝ n (gaugeFixedAdjoint x y)

The formal adjoint is Cⁿ when the background is Cⁿ and the argument is Cⁿ⁺¹.

theorem TauCeti.Vortex.continuous_gaugeFixedAdjoint {x y : ℂ → EuclideanSpace ℝ (Fin 4)} (hx : Continuous x) (hy : ContDiff ℝ 1 y) : Continuous (gaugeFixedAdjoint x y)

L_x* y is continuous for a continuous field and a C¹ argument.

theorem TauCeti.Vortex.hasCompactSupport_gaugeFixedAdjoint {x y : ℂ → EuclideanSpace ℝ (Fin 4)} (hy : HasCompactSupport y) : HasCompactSupport (gaugeFixedAdjoint x y)

The formal adjoint preserves compact support, with no regularity assumption on the field.

theorem TauCeti.Vortex.contDiff_gaugeFixedOperator {x y : ℂ → EuclideanSpace ℝ (Fin 4)} {n : WithTop ℕ∞} (hx : ContDiff ℝ n x) (hy : ContDiff ℝ (n + 1) y) : ContDiff ℝ n (gaugeFixedOperator x y)

The gauge-fixed operator is Cⁿ when the background is Cⁿ and the argument is Cⁿ⁺¹.

theorem TauCeti.Vortex.continuous_gaugeFixedOperator {x y : ℂ → EuclideanSpace ℝ (Fin 4)} (hx : Continuous x) (hy : ContDiff ℝ 1 y) : Continuous (gaugeFixedOperator x y)

L_x y is continuous for a continuous field and a C¹ argument.

theorem TauCeti.Vortex.integral_mul_gaugeAdjoint {μ : MeasureTheory.Measure ℂ} [μ.IsAddHaarMeasure] {x y : ℂ → EuclideanSpace ℝ (Fin 4)} {f : ℂ → ℝ} (hx : Continuous x) (hy : ContDiff ℝ 1 y) (hf : ContDiff ℝ 1 f) (hfc : HasCompactSupport f) : ∫ (z : ℂ), f z * gaugeAdjoint x y z ∂μ = ∫ (z : ℂ), inner ℝ (gaugeDirection x f z) (y z) ∂μ

d₀* is the formal adjoint of the infinitesimal gauge action: ∫ f d₀* y = ∫ ⟪d₀ f, y⟫ for a continuous field x, a C¹ variation y and a compactly supported C¹ phase f.

theorem TauCeti.Vortex.integral_inner_gaugeFixedOperator {μ : MeasureTheory.Measure ℂ} [μ.IsAddHaarMeasure] {x y η : ℂ → EuclideanSpace ℝ (Fin 4)} (hx : Continuous x) (hy : ContDiff ℝ 1 y) (hyc : HasCompactSupport y) (hη : ContDiff ℝ 1 η) : ∫ (z : ℂ), inner ℝ (gaugeFixedOperator x y z) (η z) ∂μ = ∫ (z : ℂ), inner ℝ (y z) (gaugeFixedAdjoint x η z) ∂μ

L_x* is the formal adjoint of the gauge-fixed operator: ∫ ⟪L_x y, η⟫ = ∫ ⟪y, L_x* η⟫ for a continuous field x, a compactly supported C¹ variation y and a C¹ field η.