@[reducible, inline]

abbrev SWGaugeGroup (M : Type u_1) [TopologicalSpace M] : Type u_1

The Seiberg–Witten gauge group $\mathcal{G} = C^\infty(M, S^1)$ on a manifold $M$.

def SWGaugeGroup.constEmb {M : Type u_1} [TopologicalSpace M] : Circle →* SWGaugeGroup M

The embedding $S^1 \hookrightarrow \mathcal{G}$ as constant maps; its image is the central stabilizer of reducible solutions.

def SWGaugeGroup.IsConstant {M : Type u_1} [TopologicalSpace M] (f : SWGaugeGroup M) : Prop

A gauge transformation $f \in \mathcal{G}$ is constant if $f \equiv z \in S^1$ everywhere.

structure ConcreteGaugeActionData {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] : Type (max 1 u_1)

Concrete data packaging the Seiberg–Witten setup on a $4$-manifold: spaces of connections, spinors, self-dual $2$-forms, the logarithmic derivative $f \mapsto f^{-1}df$, the Dirac operator, the self-dual curvature, Clifford multiplication, the traceless quadratic $\psi \otimes \psi^*$, and a perturbation $\mu$, together with the gauge-equivariance axioms.

• Connection : Type
• SpinorSection : Type
• NegativeSpinorSection : Type
• SelfDualTwoForm : Type
• instACGConn : AddCommGroup self.Connection
• instModConn : Module ℝ self.Connection
• instACGSpinor : AddCommGroup self.SpinorSection
• instModSpinor : Module ℝ self.SpinorSection
• instACGNeg : AddCommGroup self.NegativeSpinorSection
• instModNeg : Module ℝ self.NegativeSpinorSection
• instACGSD : AddCommGroup self.SelfDualTwoForm
• instModSD : Module ℝ self.SelfDualTwoForm
• instNontrivialSpinor : Nontrivial self.SpinorSection
• logDeriv : SWGaugeGroup M → self.Connection
• gaugeOnSpinor : SWGaugeGroup M → self.SpinorSection → self.SpinorSection
• supNormSq : self.SpinorSection → ℝ
• supNormSq_nonneg (ψ : self.SpinorSection) : 0 ≤ self.supNormSq ψ
• DiracOp : self.Connection → self.SpinorSection → self.NegativeSpinorSection
• selfDualCurvature : self.Connection → self.SelfDualTwoForm
• cliffordMap : self.SelfDualTwoForm → self.SpinorSection → self.SpinorSection
• tracelessQuadratic : self.SpinorSection → self.SpinorSection → self.SpinorSection
• perturbation : self.SelfDualTwoForm
• logDeriv_mul (f g : SWGaugeGroup M) : self.logDeriv (f * g) = self.logDeriv f + self.logDeriv g
• logDeriv_one : self.logDeriv 1 = 0
• logDeriv_const (z : Circle) : self.logDeriv (SWGaugeGroup.constEmb z) = 0
• gaugeOnSpinor_mul (f g : SWGaugeGroup M) (ψ : self.SpinorSection) : self.gaugeOnSpinor (f * g) ψ = self.gaugeOnSpinor f (self.gaugeOnSpinor g ψ)
• gaugeOnSpinor_one (ψ : self.SpinorSection) : self.gaugeOnSpinor 1 ψ = ψ
• gaugeOnSpinor_preserves_norm (f : SWGaugeGroup M) (ψ : self.SpinorSection) : self.supNormSq (self.gaugeOnSpinor f ψ) = self.supNormSq ψ
• gaugeOnNegSpinor : SWGaugeGroup M → self.NegativeSpinorSection → self.NegativeSpinorSection
• gaugeOnNegSpinor_zero (f : SWGaugeGroup M) : self.gaugeOnNegSpinor f 0 = 0
• DiracOp_gauge_equivariant (f : SWGaugeGroup M) (A : self.Connection) (ψ : self.SpinorSection) : self.DiracOp (A - 2 • self.logDeriv f) (self.gaugeOnSpinor f ψ) = self.gaugeOnNegSpinor f (self.DiracOp A ψ)
• selfDualCurvature_gauge_invariant (f : SWGaugeGroup M) (A : self.Connection) : self.selfDualCurvature (A - 2 • self.logDeriv f) = self.selfDualCurvature A
• tracelessQuadratic_gauge_invariant (f : SWGaugeGroup M) (ψ φ : self.SpinorSection) : self.tracelessQuadratic (self.gaugeOnSpinor f ψ) φ = self.tracelessQuadratic ψ φ

def ConcreteGaugeActionData.gaugeOnConnection {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] (ga : ConcreteGaugeActionData) (f : SWGaugeGroup M) (A : ga.Connection) : ga.Connection

The gauge action on a connection: $A \mapsto A - 2 f^{-1} df$.

def ConcreteGaugeActionData.gaugeAction {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] (ga : ConcreteGaugeActionData) (f : SWGaugeGroup M) (p : ga.Connection × ga.SpinorSection) : ga.Connection × ga.SpinorSection

The combined gauge action on pairs $(A, \psi) \mapsto (A - 2 df \cdot f^{-1}, f\psi)$.

def ConcreteGaugeActionData.IsSWSolution {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] (ga : ConcreteGaugeActionData) (A : ga.Connection) (ψ : ga.SpinorSection) : Prop

The (perturbed) Seiberg–Witten equations: $D_A \psi = 0$ and $F_A^+ \cdot \varphi = \sigma(\psi)\varphi - \mu \cdot \varphi$ for all spinors $\varphi$.

theorem gauge_action_preserves_solutions {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] (ga : ConcreteGaugeActionData) (f : SWGaugeGroup M) (A : ga.Connection) (ψ : ga.SpinorSection) (hsol : ga.IsSWSolution A ψ) : ga.IsSWSolution (ga.gaugeAction f (A, ψ)).1 (ga.gaugeAction f (A, ψ)).2

Proposition 1: the gauge action $(A, \psi) \mapsto (A - 2 df \cdot f^{-1}, f\psi)$ preserves the space of SW solutions (gauge invariance of the SW equations).