The Seiberg–Witten quadratic map in the trace-free self-adjoint endomorphisms

On a complex inner product space E of dimension two (a fibre of the positive half-spinor bundle), the quadratic endomorphism Q₀(ψ) = ψψ* - (‖ψ‖² / 2) Id and its polarization B(ψ, φ) = φψ* + ψφ* - Re⟪ψ, φ⟫ Id take values in the three-dimensional real space TauCeti.traceFreeSelfAdjoint E of trace-free self-adjoint endomorphisms; Q₀(ψ) is the trace-free part of ψψ*. Clifford multiplication identifies this space with the imaginary self-dual two-forms, so these are the values of the quadratic term of the curvature equation F_A⁺ = q(ψ) + η and of its derivative.

On that space the Hilbert–Schmidt pairing is tr (T* U) = tr (T U). This file computes the pairings of Q₀(ψ) and B(ψ, φ) with a trace-free endomorphism T: tr (Q₀(ψ) T) = ⟪ψ, T ψ⟫ and, for self-adjoint T, tr (B(ψ, φ) T) = 2 Re⟪T ψ, φ⟫. The first turns the curvature term ⟪C(F_A⁺) ψ, ψ⟫ of the Weitzenböck formula into a Hilbert–Schmidt pairing with Q₀(ψ); the second says that the formal adjoint of the derivative B(ψ, ·) of Q₀ is T ↦ 2 T ψ. In particular tr (Q₀(ψ)²) = ‖ψ‖⁴ / 2.

Main results

• quadraticEnd_eq_traceFreePart: Q₀(ψ) is the trace-free part of ψψ* in dimension two.
• quadraticEnd_mem_traceFreeSelfAdjoint, quadraticEndPolar_mem_traceFreeSelfAdjoint: Q₀(ψ) and B(ψ, φ) are trace-free self-adjoint in dimension two.
• trace_quadraticEnd_mul: tr (Q₀(ψ) T) = ⟪ψ, T ψ⟫ - (‖ψ‖² / 2) tr T; for trace-free T this is trace_quadraticEnd_mul_of_trace_eq_zero, tr (Q₀(ψ) T) = ⟪ψ, T ψ⟫.
• trace_quadraticEnd_mul_self: tr (Q₀(ψ)²) = ‖ψ‖⁴ / 2 in dimension two.
• trace_quadraticEndPolar_mul: tr (B(ψ, φ) T) = ⟪ψ, T φ⟫ + ⟪φ, T ψ⟫ - Re⟪ψ, φ⟫ tr T.
• trace_quadraticEndPolar_mul_of_mem_traceFreeSelfAdjoint: tr (B(ψ, φ) T) = 2 Re⟪T ψ, φ⟫ for trace-free self-adjoint T.

References

• J. W. Morgan, The Seiberg–Witten equations and applications to the topology of smooth four-manifolds, Mathematical Notes 44, Princeton University Press, 1996.

theorem TauCeti.SeibergWitten.quadraticEnd_eq_traceFreePart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (h₂ : Module.finrank ℂ E = 2) (ψ : E) : quadraticEnd ψ = (traceFreePart ℂ E) (((InnerProductSpace.rankOne ℂ) ψ) ψ)

In complex dimension two, Q₀(ψ) is the trace-free part of ψψ*.

theorem TauCeti.SeibergWitten.trace_quadraticEnd_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (ψ : E) (T : E →L[ℂ] E) : (LinearMap.trace ℂ E) (↑(quadraticEnd ψ) * ↑T) = inner ℂ ψ (T ψ) - ↑‖ψ‖ ^ 2 / 2 * (LinearMap.trace ℂ E) ↑T

The trace pairing of Q₀(ψ) with an endomorphism T: tr (Q₀(ψ) T) = ⟪ψ, T ψ⟫ - (‖ψ‖² / 2) tr T.

theorem TauCeti.SeibergWitten.trace_quadraticEnd_mul_of_trace_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {T : E →L[ℂ] E} (hT : (LinearMap.trace ℂ E) ↑T = 0) (ψ : E) : (LinearMap.trace ℂ E) (↑(quadraticEnd ψ) * ↑T) = inner ℂ ψ (T ψ)

Against a trace-free endomorphism T, Q₀(ψ) pairs as tr (Q₀(ψ) T) = ⟪ψ, T ψ⟫.

theorem TauCeti.SeibergWitten.trace_quadraticEnd_mul_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (h₂ : Module.finrank ℂ E = 2) (ψ : E) : (LinearMap.trace ℂ E) (↑(quadraticEnd ψ) * ↑(quadraticEnd ψ)) = ↑‖ψ‖ ^ 4 / 2

In complex dimension two, the Hilbert–Schmidt square of Q₀(ψ) is tr (Q₀(ψ)²) = ‖ψ‖⁴ / 2.

theorem TauCeti.SeibergWitten.trace_quadraticEndPolar_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (ψ φ : E) (T : E →L[ℂ] E) : (LinearMap.trace ℂ E) (↑((quadraticEndPolar ψ) φ) * ↑T) = inner ℂ ψ (T φ) + inner ℂ φ (T ψ) - ↑(inner ℂ ψ φ).re * (LinearMap.trace ℂ E) ↑T

The trace pairing of the polarization B(ψ, φ) with an endomorphism T: tr (B(ψ, φ) T) = ⟪ψ, T φ⟫ + ⟪φ, T ψ⟫ - Re⟪ψ, φ⟫ tr T.

theorem TauCeti.SeibergWitten.quadraticEnd_mem_traceFreeSelfAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [CompleteSpace E] (h₂ : Module.finrank ℂ E = 2) (ψ : E) : quadraticEnd ψ ∈ traceFreeSelfAdjoint E

In complex dimension two, Q₀(ψ) is a trace-free self-adjoint endomorphism.

theorem TauCeti.SeibergWitten.quadraticEndPolar_mem_traceFreeSelfAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [CompleteSpace E] (h₂ : Module.finrank ℂ E = 2) (ψ φ : E) : (quadraticEndPolar ψ) φ ∈ traceFreeSelfAdjoint E

In complex dimension two, the polarization B(ψ, φ) of Q₀ is a trace-free self-adjoint endomorphism.

theorem TauCeti.SeibergWitten.trace_quadraticEndPolar_mul_of_mem_traceFreeSelfAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [CompleteSpace E] {T : E →L[ℂ] E} (hT : T ∈ traceFreeSelfAdjoint E) (ψ φ : E) : (LinearMap.trace ℂ E) (↑((quadraticEndPolar ψ) φ) * ↑T) = 2 * ↑(inner ℂ (T ψ) φ).re

Against a trace-free self-adjoint T, the polarization of Q₀ pairs as tr (B(ψ, φ) T) = 2 Re⟪T ψ, φ⟫: the formal adjoint of the derivative B(ψ, ·) of Q₀ is T ↦ 2 T ψ.