The rank-one quadratic endomorphism of the Seiberg–Witten equations

For a vector ψ of a complex inner product space E, set Q₀(ψ) = ψψ* - (‖ψ‖² / 2) Id, where ψψ* is InnerProductSpace.rankOne ℂ ψ ψ, the map v ↦ ⟪ψ, v⟫ ψ. When E has complex dimension two (a fibre of the positive half-spinor bundle of a Spinᶜ four-manifold), Q₀(ψ) is the trace-free part of ψψ*, and the Seiberg–Witten curvature equation reads C(F_A⁺) = Q₀(ψ), where C is Clifford multiplication by self-dual two-forms.

This file proves the pointwise algebra and calculus of Q₀ needed by the nonlinear analysis of the equations. The map Q₀ is real-quadratic but not complex-linear, so its polarization and its derivative are only real-linear.

Main definitions

• TauCeti.SeibergWitten.quadraticEnd ψ: the endomorphism Q₀(ψ) = ψψ* - (‖ψ‖² / 2) Id.
• TauCeti.SeibergWitten.quadraticEndPolar: its real polarization B(ψ, φ) = φψ* + ψφ* - Re⟪ψ, φ⟫ Id, as a continuous real-bilinear map.

Main results

• trace_quadraticEnd: Q₀(ψ) is trace free when E has complex dimension two.
• isSelfAdjoint_quadraticEnd: Q₀(ψ) is self-adjoint.
• quadraticEnd_apply_self: Q₀(ψ) ψ = (‖ψ‖² / 2) ψ.
• quadraticEnd_smul, quadraticEnd_smul_of_norm_eq_one: Q₀(c ψ) = |c|² Q₀(ψ); in particular Q₀ is invariant under unit phases.
• quadraticEnd_add: Q₀(ψ + φ) = Q₀(ψ) + Q₀(φ) + B(ψ, φ).
• trace_quadraticEndPolar, isSelfAdjoint_quadraticEndPolar: like Q₀(ψ), every B(ψ, φ) is trace free in complex dimension two and self-adjoint.
• norm_quadraticEnd_apply, norm_quadraticEnd: Q₀(ψ) is ‖ψ‖² / 2 times an isometry, so its operator norm is ‖ψ‖² / 2; in particular Q₀(ψ) = 0 only for ψ = 0.
• norm_quadraticEndPolar_le, norm_quadraticEnd_sub_le: ‖B(ψ, φ)‖ ≤ ‖ψ‖ ‖φ‖ and ‖Q₀(ψ) - Q₀(φ)‖ ≤ ‖ψ - φ‖ (‖ψ‖ + ‖φ‖) / 2.
• hasFDerivAt_quadraticEnd: the real Fréchet derivative of Q₀ at ψ is B(ψ, ·), that is DQ₀|_ψ (φ) = φψ* + ψφ* - Re⟪ψ, φ⟫ Id.
• quadraticEndPolar_smul_self: B(ψ, c ψ) = 2 Re(c) Q₀(ψ), so the derivative kills the infinitesimal gauge directions ξ ψ with ξ imaginary.

References

• C. H. Taubes, The Seiberg–Witten and Gromov invariants, Math. Res. Lett. 2 (1995).
• J. W. Morgan, The Seiberg–Witten equations and applications to the topology of smooth four-manifolds, Mathematical Notes 44, Princeton University Press, 1996.

noncomputable def TauCeti.SeibergWitten.quadraticEnd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : E) : E →L[ℂ] E

The rank-one quadratic endomorphism Q₀(ψ) = ψψ* - (‖ψ‖² / 2) Id of a complex inner product space. In complex dimension two this is the trace-free part of ψψ*.

theorem TauCeti.SeibergWitten.quadraticEnd_def {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : E) : quadraticEnd ψ = ((InnerProductSpace.rankOne ℂ) ψ) ψ - (↑‖ψ‖ ^ 2 / 2) • ContinuousLinearMap.id ℂ E

Unfolding lemma for quadraticEnd.

@[simp]

theorem TauCeti.SeibergWitten.quadraticEnd_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ v : E) : (quadraticEnd ψ) v = inner ℂ ψ v • ψ - (↑‖ψ‖ ^ 2 / 2) • v

Q₀(ψ) v = ⟪ψ, v⟫ ψ - (‖ψ‖² / 2) v.

@[simp]

theorem TauCeti.SeibergWitten.quadraticEnd_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : quadraticEnd 0 = 0

Q₀(0) = 0.

theorem TauCeti.SeibergWitten.quadraticEnd_apply_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : E) : (quadraticEnd ψ) ψ = (↑‖ψ‖ ^ 2 / 2) • ψ

ψ is an eigenvector of Q₀(ψ) with eigenvalue ‖ψ‖² / 2.

theorem TauCeti.SeibergWitten.quadraticEnd_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (c : ℂ) (ψ : E) : quadraticEnd (c • ψ) = ‖c‖ ^ 2 • quadraticEnd ψ

Q₀ is homogeneous of degree two for the real structure: Q₀(c ψ) = |c|² Q₀(ψ).

theorem TauCeti.SeibergWitten.quadraticEnd_smul_of_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {u : ℂ} (hu : ‖u‖ = 1) (ψ : E) : quadraticEnd (u • ψ) = quadraticEnd ψ

Q₀ is invariant under unit phases: Q₀(u ψ) = Q₀(ψ) when |u| = 1.

@[simp]

theorem TauCeti.SeibergWitten.quadraticEnd_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : E) : quadraticEnd (-ψ) = quadraticEnd ψ

Q₀(-ψ) = Q₀(ψ).

theorem TauCeti.SeibergWitten.trace_quadraticEnd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (h₂ : Module.finrank ℂ E = 2) (ψ : E) : (LinearMap.trace ℂ E) ↑(quadraticEnd ψ) = 0

In complex dimension two, Q₀(ψ) is trace free.

theorem TauCeti.SeibergWitten.isSelfAdjoint_quadraticEnd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (ψ : E) : IsSelfAdjoint (quadraticEnd ψ)

Q₀(ψ) is self-adjoint.

theorem TauCeti.SeibergWitten.norm_quadraticEnd_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ v : E) : ‖(quadraticEnd ψ) v‖ = ‖ψ‖ ^ 2 / 2 * ‖v‖

Q₀(ψ) scales the norm of every vector by exactly ‖ψ‖² / 2: for ψ ≠ 0 it is ‖ψ‖² / 2 times the reflection fixing ψ and negating its orthogonal complement.

theorem TauCeti.SeibergWitten.norm_quadraticEnd_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : E) : ‖quadraticEnd ψ‖ ≤ ‖ψ‖ ^ 2 / 2

The operator norm of Q₀(ψ) is at most ‖ψ‖² / 2.

@[simp]

theorem TauCeti.SeibergWitten.norm_quadraticEnd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : E) : ‖quadraticEnd ψ‖ = ‖ψ‖ ^ 2 / 2

The operator norm of Q₀(ψ) is ‖ψ‖² / 2.

@[simp]

theorem TauCeti.SeibergWitten.quadraticEnd_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : E} : quadraticEnd ψ = 0 ↔ ψ = 0

Q₀(ψ) vanishes exactly when ψ does.

noncomputable def TauCeti.SeibergWitten.quadraticEndPolar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : E →L[ℝ] E →L[ℝ] E →L[ℂ] E

The real polarization B(ψ, φ) = φψ* + ψφ* - Re⟪ψ, φ⟫ Id of Q₀, as a continuous real-bilinear map. It satisfies Q₀(ψ + φ) = Q₀(ψ) + Q₀(φ) + B(ψ, φ) and is the real Fréchet derivative of Q₀ at ψ.

theorem TauCeti.SeibergWitten.quadraticEndPolar_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ φ : E) : (quadraticEndPolar ψ) φ = ((InnerProductSpace.rankOne ℂ) φ) ψ + ((InnerProductSpace.rankOne ℂ) ψ) φ - ↑(inner ℂ ψ φ).re • ContinuousLinearMap.id ℂ E

Unfolding lemma for quadraticEndPolar.

@[simp]

theorem TauCeti.SeibergWitten.quadraticEndPolar_apply_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ φ v : E) : ((quadraticEndPolar ψ) φ) v = inner ℂ ψ v • φ + inner ℂ φ v • ψ - ↑(inner ℂ ψ φ).re • v

B(ψ, φ) v = ⟪ψ, v⟫ φ + ⟪φ, v⟫ ψ - Re⟪ψ, φ⟫ v.

theorem TauCeti.SeibergWitten.quadraticEndPolar_comm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ φ : E) : (quadraticEndPolar ψ) φ = (quadraticEndPolar φ) ψ

The polarization of Q₀ is symmetric.

@[simp]

theorem TauCeti.SeibergWitten.quadraticEndPolar_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : E) : (quadraticEndPolar ψ) ψ = 2 • quadraticEnd ψ

The polarization of Q₀ restricts on the diagonal to 2 Q₀.

theorem TauCeti.SeibergWitten.quadraticEnd_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ φ : E) : quadraticEnd (ψ + φ) = quadraticEnd ψ + quadraticEnd φ + (quadraticEndPolar ψ) φ

Real polarization of Q₀: Q₀(ψ + φ) = Q₀(ψ) + Q₀(φ) + B(ψ, φ).

theorem TauCeti.SeibergWitten.trace_quadraticEndPolar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (h₂ : Module.finrank ℂ E = 2) (ψ φ : E) : (LinearMap.trace ℂ E) ↑((quadraticEndPolar ψ) φ) = 0

In complex dimension two, the polarization B(ψ, φ) of Q₀ is trace free.

theorem TauCeti.SeibergWitten.isSelfAdjoint_quadraticEndPolar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (ψ φ : E) : IsSelfAdjoint ((quadraticEndPolar ψ) φ)

The polarization B(ψ, φ) of Q₀ is self-adjoint.

@[simp]

theorem TauCeti.SeibergWitten.quadraticEndPolar_I_smul_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : E) : (quadraticEndPolar ψ) (Complex.I • ψ) = 0

B(ψ, i ψ) = 0: the derivative of Q₀ vanishes along the infinitesimal phase direction i ψ.

theorem TauCeti.SeibergWitten.quadraticEndPolar_smul_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (c : ℂ) (ψ : E) : (quadraticEndPolar ψ) (c • ψ) = (2 * c.re) • quadraticEnd ψ

B(ψ, c ψ) = 2 Re(c) Q₀(ψ). In particular B(ψ, ξ ψ) = 0 for imaginary ξ: the derivative of Q₀ vanishes along the infinitesimal phase directions.

theorem TauCeti.SeibergWitten.quadraticEndPolar_sub_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ φ : E) : (quadraticEndPolar (ψ - φ)) (ψ + φ) = 2 • (quadraticEnd ψ - quadraticEnd φ)

B(ψ - φ, ψ + φ) = 2 (Q₀(ψ) - Q₀(φ)).

theorem TauCeti.SeibergWitten.norm_quadraticEndPolar_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ φ : E) : ‖(quadraticEndPolar ψ) φ‖ ≤ ‖ψ‖ * ‖φ‖

The polarization of Q₀ satisfies ‖B(ψ, φ)‖ ≤ ‖ψ‖ ‖φ‖.

theorem TauCeti.SeibergWitten.norm_quadraticEnd_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ φ : E) : ‖quadraticEnd ψ - quadraticEnd φ‖ ≤ ‖ψ - φ‖ * (‖ψ‖ + ‖φ‖) / 2

Q₀ is locally Lipschitz: ‖Q₀(ψ) - Q₀(φ)‖ ≤ ‖ψ - φ‖ (‖ψ‖ + ‖φ‖) / 2.

theorem TauCeti.SeibergWitten.hasStrictFDerivAt_quadraticEnd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : E) : HasStrictFDerivAt quadraticEnd (quadraticEndPolar ψ) ψ

The real Fréchet derivative of Q₀ at ψ is B(ψ, ·), that is DQ₀|_ψ (φ) = φψ* + ψφ* - Re⟪ψ, φ⟫ Id; this holds in the strict sense.

theorem TauCeti.SeibergWitten.hasFDerivAt_quadraticEnd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : E) : HasFDerivAt quadraticEnd (quadraticEndPolar ψ) ψ

The real Fréchet derivative of Q₀ at ψ is B(ψ, ·).

theorem TauCeti.SeibergWitten.fderiv_quadraticEnd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ : E) : fderiv ℝ quadraticEnd ψ = quadraticEndPolar ψ

The real Fréchet derivative of Q₀ at ψ is B(ψ, ·).

theorem TauCeti.SeibergWitten.contDiff_quadraticEnd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {n : WithTop ℕ∞} : ContDiff ℝ n quadraticEnd

Q₀ is a smooth map of the underlying real vector space.