structure IntersectionForm : Type

The intersection form of a 4-manifold: a symmetric bilinear form on $H^2(X;\mathbb{Z})$ described abstractly by its rank $b_2$, the splitting $b_2 = b_2^+ + b_2^-$ into positive and negative subspaces, signature $\sigma = b_2^+ - b_2^-$, parity (even/odd), and the explicit bilinear form.

• b₂ : ℕ
• b₂_plus : ℕ
• b₂_minus : ℕ
• rank_decomp : self.b₂ = self.b₂_plus + self.b₂_minus
• signature : ℤ
• signature_eq : self.signature = ↑self.b₂_plus - ↑self.b₂_minus
• isEven : Bool
• bilinForm : (Fin self.b₂ → ℤ) → (Fin self.b₂ → ℤ) → ℤ

class Has4ManifoldTopology (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] : Type

Typeclass recording the topology of a compact simply-connected 4-manifold $M$: its intersection form $Q$ and Euler characteristic $\chi = 2 + b_2$.

• Q : IntersectionForm
• euler : ℤ
• euler_eq : euler M = 2 + ↑(Q M).b₂

def IntersectionForm.IsPositiveDefinite (Q : IntersectionForm) : Prop

$Q$ is positive definite, i.e. $b_2^- = 0$.

def IntersectionForm.IsNegativeDefinite (Q : IntersectionForm) : Prop

$Q$ is negative definite, i.e. $b_2^+ = 0$.

def IntersectionForm.IsDefinite (Q : IntersectionForm) : Prop

$Q$ is definite if it is either positive definite or negative definite.

def IntersectionForm.IsDiagonal (Q : IntersectionForm) : Prop

$Q$ is (potentially) diagonalisable in the sense that its parity is odd.

theorem posdef_signature_eq_b₂ (Q : IntersectionForm) (hdef : Q.IsPositiveDefinite) : Q.signature = ↑Q.b₂

For a positive-definite intersection form, the signature equals the rank: $\sigma = b_2$.

theorem negdef_signature_eq_neg_b₂ (Q : IntersectionForm) (hdef : Q.IsNegativeDefinite) : Q.signature = -↑Q.b₂

For a negative-definite intersection form, the signature is minus the rank: $\sigma = -b_2$.

class IsCompactSimplyConnected4Manifold (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] : Prop

Typeclass for a compact (simply connected) 4-manifold $M$.

• compact : CompactSpace M

class AreHomeomorphic4Manifolds (M₁ : Type u_1) (M₂ : Type u_2) [TopologicalSpace M₁] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M₁] [TopologicalSpace M₂] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M₂] [htop₁ : Has4ManifoldTopology M₁] [htop₂ : Has4ManifoldTopology M₂] : Prop

Two 4-manifolds have the same homeomorphism type (à la Freedman) if their intersection forms agree in rank, signature, and parity.

• b₂_eq : (Has4ManifoldTopology.Q M₁).b₂ = (Has4ManifoldTopology.Q M₂).b₂
• signature_eq : (Has4ManifoldTopology.Q M₁).signature = (Has4ManifoldTopology.Q M₂).signature
• parity_eq : (Has4ManifoldTopology.Q M₁).isEven = (Has4ManifoldTopology.Q M₂).isEven

structure SpinCStructure (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 (max 1 u_2) u_3)

Abstract data for a $\mathrm{Spin}^c$-structure $S$ on a 4-manifold $M$: positive and negative spinor bundle sections $\Gamma(S^\pm)$, the determinant line $L$ with $c_1(L)$, Clifford multiplication $\gamma$ acting between $S^\pm$ and on 2-forms (with the $(\pm 1)$-eigenspace decomposition under Hodge $*$), and a Hermitian inner product on $S^+$.

• SectionsPlus : Type
• SectionsMinus : Type
• instACGPlus : AddCommGroup self.SectionsPlus
• instModPlus : Module ℝ self.SectionsPlus
• instACGMinus : AddCommGroup self.SectionsMinus
• instModMinus : Module ℝ self.SectionsMinus
• nontrivial_plus : Nontrivial self.SectionsPlus
• c₁_L : ℤ
• Q_eval : ℤ → ℤ
• c₁_pair : ℤ → ℤ
• metric_pairing : Ω1 → Ω1 → ℝ
• γ_plus_to_minus : Ω1 → self.SectionsPlus → self.SectionsMinus
• γ_minus_to_plus : Ω1 → self.SectionsMinus → self.SectionsPlus
• γ_on_2forms : Ω2 → self.SectionsPlus → self.SectionsPlus
• γ_on_2forms_minus : Ω2 → self.SectionsMinus → self.SectionsMinus
• hodge_star : Ω2 → Ω2
• hodge_star_invol (α : Ω2) : self.hodge_star (self.hodge_star α) = α
• hodge_clifford_plus (α : Ω2) (ψ : self.SectionsPlus) : self.γ_on_2forms (self.hodge_star α) ψ = self.γ_on_2forms α ψ
• hodge_clifford_minus (α : Ω2) (ψ : self.SectionsMinus) : self.γ_on_2forms_minus (self.hodge_star α) ψ = -self.γ_on_2forms_minus α ψ
• gamma_anticomm (u v : Ω1) (ψ : self.SectionsPlus) : self.γ_minus_to_plus u (self.γ_plus_to_minus v ψ) + self.γ_minus_to_plus v (self.γ_plus_to_minus u ψ) = (-2 * self.metric_pairing u v) • ψ
• hermitianInnerPlus : self.SectionsPlus → self.SectionsPlus → ℝ
• normSqPlus : self.SectionsPlus → ℝ
• normSq_nonneg (ψ : self.SectionsPlus) : 0 ≤ self.normSqPlus ψ
• normSq_zero_iff (ψ : self.SectionsPlus) : self.normSqPlus ψ = 0 ↔ ψ = 0
• hermitian_norm_compat (ψ : self.SectionsPlus) : self.hermitianInnerPlus ψ ψ = self.normSqPlus ψ
• hermitian_smul_left (c : ℝ) (ψ φ : self.SectionsPlus) : self.hermitianInnerPlus (c • ψ) φ = c * self.hermitianInnerPlus ψ φ

noncomputable def SpinCStructure.tracelessQuadratic {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] (spinc : SpinCStructure M Ω1 Ω2) (ψ φ : spinc.SectionsPlus) : spinc.SectionsPlus

The traceless quadratic form $(\psi^* \otimes \varphi)_0 = \langle \psi, \varphi\rangle \cdot \psi

• \tfrac{1}{2}|\psi|^2 \cdot \varphi$, appearing on the right-hand side of the curvature equation $\gamma(F_A^+) = (\psi^* \otimes \psi)_0$ in the Seiberg-Witten equations.

structure DiracOperator {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] (spinc : SpinCStructure M Ω1 Ω2) : Type u_2

Data of a Dirac operator $D_A = \sum_i \gamma(e^i)\nabla^A_{e_i}$ for a Spin-c structure: a local frame $(e_i)$, covariant derivatives $\nabla^A_{e_i}$ on $S^\pm$, $\mathbb{R}$-linearity of Clifford multiplication, and the $L^2$ adjoint relation between $D_A^+ : \Gamma(S^+) \to \Gamma(S^-)$ and $D_A^- : \Gamma(S^-) \to \Gamma(S^+)$.

• frame : Fin 4 → Ω1
• conn_plus : Fin 4 → spinc.SectionsPlus →ₗ[ℝ] spinc.SectionsPlus
• conn_minus : Fin 4 → spinc.SectionsMinus →ₗ[ℝ] spinc.SectionsMinus
• γ_linear (ω : Ω1) : IsLinearMap ℝ (spinc.γ_plus_to_minus ω)
• γ_linear_minus (ω : Ω1) : IsLinearMap ℝ (spinc.γ_minus_to_plus ω)
• L2pairingPlus : spinc.SectionsPlus → spinc.SectionsPlus → ℝ
• L2pairingMinus : spinc.SectionsMinus → spinc.SectionsMinus → ℝ
• adjoint_relation (ψ : spinc.SectionsPlus) (φ : spinc.SectionsMinus) : self.L2pairingMinus (∑ i : Fin 4, spinc.γ_plus_to_minus (self.frame i) ((self.conn_plus i) ψ)) φ = self.L2pairingPlus ψ (∑ i : Fin 4, spinc.γ_minus_to_plus (self.frame i) ((self.conn_minus i) φ))

def dirac_sum {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] {spinc : SpinCStructure M Ω1 Ω2} (D : DiracOperator spinc) (ψ : spinc.SectionsPlus) : spinc.SectionsMinus

The local Dirac sum $D_A \psi = \sum_{i=1}^4 \gamma(e^i)\nabla^A_{e_i}\psi \in \Gamma(S^-)$.

def dirac_sum_adjoint {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] {spinc : SpinCStructure M Ω1 Ω2} (D : DiracOperator spinc) (φ : spinc.SectionsMinus) : spinc.SectionsPlus

The local adjoint Dirac sum $D_A^- \varphi = \sum_i \gamma(e^i)\nabla^A_{e_i}\varphi \in \Gamma(S^+)$ for $\varphi \in \Gamma(S^-)$.

def DiracOperator.D_plus {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] {spinc : SpinCStructure M Ω1 Ω2} (D : DiracOperator spinc) : spinc.SectionsPlus → spinc.SectionsMinus

The positive-chirality Dirac operator $D_A^+ : \Gamma(S^+) \to \Gamma(S^-)$.

def DiracOperator.D_minus {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] {spinc : SpinCStructure M Ω1 Ω2} (D : DiracOperator spinc) : spinc.SectionsMinus → spinc.SectionsPlus

The negative-chirality Dirac operator $D_A^- : \Gamma(S^-) \to \Gamma(S^+)$, the $L^2$ adjoint of $D_A^+$.

structure SWSolution {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] (spinc : SpinCStructure M Ω1 Ω2) : Type (max u_2 u_3)

A formal Seiberg-Witten solution: bundles together a Dirac operator $D_A$, a positive spinor $\psi \in \Gamma(S^+)$, the self-dual curvature $F_A^+ \in \Omega^{2,+}$, and the analytic data (Weitzenböck and Bochner identities) needed for the a priori bounds: $\langle D_A^2 \psi, \psi\rangle = \langle \nabla^*\nabla\psi, \psi\rangle + \tfrac{s}{4}|\psi|^2 + \tfrac{1}{2}\langle \gamma(F_A^+)\psi, \psi\rangle$, together with $D_A\psi = 0$ on the kernel.

• dirac : DiracOperator spinc
• ψ : spinc.SectionsPlus
• F_A_plus : Ω2
• supNormSq : ℝ
• supNormSq_nonneg : 0 ≤ self.supNormSq
• supNormSq_eq : self.supNormSq = spinc.normSqPlus self.ψ
• scalarCurvatureVal : ℝ
• laplacianTerm : ℝ
• covDerivNormSq : ℝ
• laplacianTerm_nonneg : 0 ≤ self.laplacianTerm
• covDerivNormSq_nonneg : 0 ≤ self.covDerivNormSq
• connLapInnerProd : ℝ
• cliffordInnerProd : ℝ
• diracSqInnerProd : ℝ
• integration_by_parts_eq : self.connLapInnerProd = self.laplacianTerm + self.covDerivNormSq
• curvature_eq_applied : spinc.γ_on_2forms self.F_A_plus self.ψ = spinc.tracelessQuadratic self.ψ self.ψ
• clifford_inner_from_gamma : self.cliffordInnerProd = spinc.hermitianInnerPlus (spinc.γ_on_2forms self.F_A_plus self.ψ) self.ψ
• clifford_quadratic_eq : self.cliffordInnerProd = 1 / 2 * self.supNormSq ^ 2
• diracSq_diagonal_eq_connLap : ℝ
• diracSq_offdiagonal_eq_curvature : ℝ
• diagonal_eq : self.diracSq_diagonal_eq_connLap = self.connLapInnerProd
• offdiagonal_eq : self.diracSq_offdiagonal_eq_curvature = self.scalarCurvatureVal / 4 * self.supNormSq + 1 / 2 * self.cliffordInnerProd
• diracSq_split : self.diracSqInnerProd = self.diracSq_diagonal_eq_connLap + self.diracSq_offdiagonal_eq_curvature
• dirac_kernel : self.diracSqInnerProd = 0

theorem SWSolution.weitzenbock_decomp {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] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) : sol.diracSqInnerProd = sol.connLapInnerProd + sol.scalarCurvatureVal / 4 * sol.supNormSq + 1 / 2 * sol.cliffordInnerProd

The Weitzenböck decomposition for a Seiberg-Witten solution: $\langle D_A^2 \psi, \psi\rangle = \langle \nabla^*\nabla\psi, \psi\rangle + \tfrac{s}{4}|\psi|^2 + \tfrac{1}{2}\langle \gamma(F_A^+)\psi, \psi\rangle$.

theorem SWSolution.weitzenbock_eq {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] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) : 0 = sol.connLapInnerProd + sol.scalarCurvatureVal / 4 * sol.supNormSq + 1 / 2 * sol.cliffordInnerProd

Weitzenböck identity in the Dirac kernel: when $D_A \psi = 0$, $0 = \langle \nabla^*\nabla\psi, \psi\rangle + \tfrac{s}{4}|\psi|^2

• \tfrac{1}{2}\langle \gamma(F_A^+)\psi, \psi\rangle$.

theorem SWSolution.bochner_eq {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] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) : sol.laplacianTerm + sol.covDerivNormSq + sol.scalarCurvatureVal / 4 * sol.supNormSq + 1 / 4 * sol.supNormSq ^ 2 = 0

Bochner-type identity obtained from the Weitzenböck identity together with the curvature equation and integration by parts: $\tfrac{1}{2}\Delta|\psi|^2 + |\nabla\psi|^2 + \tfrac{s}{4}|\psi|^2 + \tfrac{1}{4}|\psi|^4 = 0$.

theorem clifford_quadratic_from_curvature {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] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) : spinc.hermitianInnerPlus (spinc.γ_on_2forms sol.F_A_plus sol.ψ) sol.ψ = 1 / 2 * sol.supNormSq ^ 2

The Clifford pairing $\langle \gamma(F_A^+)\psi, \psi\rangle = \tfrac{1}{2}|\psi|^4$, derived from the curvature equation $\gamma(F_A^+) = (\psi^*\otimes\psi)_0$.

theorem SWSolution.clifford_quadratic_derived {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] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) : sol.cliffordInnerProd = 1 / 2 * sol.supNormSq ^ 2

The Clifford inner product of a Seiberg-Witten solution equals $\tfrac{1}{2}|\psi|^4$.

def SWSolution.isReducible {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] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) : Prop

A Seiberg-Witten solution is reducible if its spinor vanishes identically: $\psi \equiv 0$.

theorem SWSolution.isReducible_iff_supNormSq_zero {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] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) : sol.isReducible ↔ sol.supNormSq = 0

Reducibility is equivalent to vanishing of the supremum of $|\psi|^2$.

structure IsSWSolutionWith {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] {spinc : SpinCStructure M Ω1 Ω2} [Zero spinc.SectionsMinus] (sol : SWSolution spinc) (μ : Ω2) : Prop

The perturbed Seiberg-Witten equations $D_A \psi = 0$ and $\gamma(F_A^+) = (\psi^*\otimes\psi)_0 + \gamma(\mu)$ with perturbation $\mu \in \Omega^{2,+}$.

• dirac_eq : sol.dirac.D_plus sol.ψ = 0
• curvature_eq (φ : spinc.SectionsPlus) : spinc.γ_on_2forms sol.F_A_plus φ = spinc.tracelessQuadratic sol.ψ φ + spinc.γ_on_2forms μ φ

structure 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] {spinc : SpinCStructure M Ω1 Ω2} [Zero spinc.SectionsMinus] (sol : SWSolution spinc) : Prop

The unperturbed Seiberg-Witten equations $D_A \psi = 0$ and $\gamma(F_A^+) = (\psi^*\otimes\psi)_0$.

• dirac_eq : sol.dirac.D_plus sol.ψ = 0
• curvature_eq (φ : spinc.SectionsPlus) : spinc.γ_on_2forms sol.F_A_plus φ = spinc.tracelessQuadratic sol.ψ φ

theorem IsSWSolution.toPerturbed {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] {spinc : SpinCStructure M Ω1 Ω2} [Zero spinc.SectionsMinus] (sol : SWSolution spinc) (h : IsSWSolution sol) (hγ_zero : ∀ (φ : spinc.SectionsPlus), spinc.γ_on_2forms 0 φ = 0) : IsSWSolutionWith sol 0

Any unperturbed Seiberg-Witten solution is a perturbed one with perturbation $\mu = 0$.

theorem IsSWSolution.ofPerturbed {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] {spinc : SpinCStructure M Ω1 Ω2} [Zero spinc.SectionsMinus] (sol : SWSolution spinc) (h : IsSWSolutionWith sol 0) (hγ_zero : ∀ (φ : spinc.SectionsPlus), spinc.γ_on_2forms 0 φ = 0) : IsSWSolution sol

A perturbed Seiberg-Witten solution with perturbation $\mu = 0$ is an unperturbed solution.

theorem IsSWSolutionWith.dirac_vanishes {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] {spinc : SpinCStructure M Ω1 Ω2} [Zero spinc.SectionsMinus] (sol : SWSolution spinc) (μ : Ω2) (h : IsSWSolutionWith sol μ) : sol.dirac.D_plus sol.ψ = 0

For a perturbed Seiberg-Witten solution, the Dirac equation $D_A \psi = 0$ holds.

theorem IsSWSolutionWith.ofIsSWSolution {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] {spinc : SpinCStructure M Ω1 Ω2} [Zero spinc.SectionsMinus] (sol : SWSolution spinc) (μ : Ω2) (h_dirac : sol.dirac.D_plus sol.ψ = 0) (h_curv : ∀ (φ : spinc.SectionsPlus), spinc.γ_on_2forms sol.F_A_plus φ = spinc.tracelessQuadratic sol.ψ φ + spinc.γ_on_2forms μ φ) : IsSWSolutionWith sol μ

Constructor for a perturbed Seiberg-Witten solution from the Dirac equation and the perturbed curvature equation.

structure GaugeActionData {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] (spinc : SpinCStructure M Ω1 Ω2) : Type (max (max 1 u_2) u_3)

Abstract data of a gauge group $\mathcal{G}$ acting on Seiberg-Witten solutions $(A,\psi) \mapsto (A - 2df \cdot f^{-1}, f\psi)$: the group, its action on solutions and on $\psi, F_A^+$, compatibility with the group structure, preservation of $|\psi|^2$, and the condition that the action is free away from reducibles.

• GaugeGroup : Type
• gaugeGroupGroup : Group self.GaugeGroup
• gauge_action : self.GaugeGroup → SWSolution spinc → SWSolution spinc
• gauge_transform_spinor : self.GaugeGroup → spinc.SectionsPlus → spinc.SectionsPlus
• gauge_transform_curvature : self.GaugeGroup → Ω2 → Ω2
• spinor_formula (f : self.GaugeGroup) (sol : SWSolution spinc) : (self.gauge_action f sol).ψ = self.gauge_transform_spinor f sol.ψ
• curvature_formula (f : self.GaugeGroup) (sol : SWSolution spinc) : (self.gauge_action f sol).F_A_plus = self.gauge_transform_curvature f sol.F_A_plus
• gauge_action_one (sol : SWSolution spinc) : self.gauge_action 1 sol = sol
• gauge_action_mul (f g : self.GaugeGroup) (sol : SWSolution spinc) : self.gauge_action (f * g) sol = self.gauge_action f (self.gauge_action g sol)
• gauge_action_preserves_supNormSq (f : self.GaugeGroup) (sol : SWSolution spinc) : (self.gauge_action f sol).supNormSq = sol.supNormSq
• gauge_nontrivial : ∃ (f : self.GaugeGroup), f ≠ 1
• gauge_free_on_irreducible (sol : SWSolution spinc) : ¬sol.isReducible → ∀ (f : self.GaugeGroup), self.gauge_action f sol = sol → f = 1

@[reducible]

def GaugeActionData.toSMul {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] {spinc : SpinCStructure M Ω1 Ω2} (gd : GaugeActionData spinc) : SMul gd.GaugeGroup (SWSolution spinc)

Equip the solution space with the canonical $\mathcal{G}$-action via SMul.

theorem GaugeActionData.free_iff_irreducible {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] {spinc : SpinCStructure M Ω1 Ω2} (gauge : GaugeActionData spinc) (sol : SWSolution spinc) (hirr : ¬sol.isReducible) (f : gauge.GaugeGroup) (hfix : gauge.gauge_action f sol = sol) : f = 1

Gauge action is free on irreducible solutions: if $\psi \not\equiv 0$ and $f \cdot (A,\psi) = (A,\psi)$, then $f = 1$.

def SmoothGaugeGroup (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] : Type u_1

The smooth gauge group $\mathcal{G} = \mathrm{Map}(M, S^1)$ of continuous (here, smooth) circle-valued maps on $M$.

theorem SmoothGaugeGroup.ext {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {f g : SmoothGaugeGroup M} (h : ↑f = ↑g) : f = g

Extensionality for SmoothGaugeGroup: two gauge transformations are equal iff their underlying maps are equal.

theorem SmoothGaugeGroup.ext_iff {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {f g : SmoothGaugeGroup M} : f = g ↔ ↑f = ↑g

def SmoothGaugeGroup.eval {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] (f : SmoothGaugeGroup M) (x : M) : Circle

Evaluation of a smooth gauge transformation $f : M \to S^1$ at a point $x \in M$.

def GaugeActionData.gaugeEquivSetoid {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] {spinc : SpinCStructure M Ω1 Ω2} (gd : GaugeActionData spinc) : Setoid (SWSolution spinc)

The gauge-equivalence setoid on $\mathrm{SWSolution}$: two solutions are related iff one is the image of the other under some $g \in \mathcal{G}$.

def SWModuliQuotient {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] {spinc : SpinCStructure M Ω1 Ω2} (gd : GaugeActionData spinc) : Type (max u_2 u_3)

The Seiberg-Witten moduli quotient: the set-theoretic quotient $\mathcal{M} = \{(A,\psi)\} / \mathcal{G}$ of solutions modulo gauge equivalence.

def SWModuliQuotient.mk {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] {spinc : SpinCStructure M Ω1 Ω2} (gd : GaugeActionData spinc) (sol : SWSolution spinc) : SWModuliQuotient gd

The canonical projection $\mathrm{SWSolution} \to \mathrm{SWModuliQuotient}$ sending a solution to its gauge equivalence class.

theorem SWModuliQuotient.eq_iff {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] {spinc : SpinCStructure M Ω1 Ω2} (gd : GaugeActionData spinc) (sol₁ sol₂ : SWSolution spinc) : mk gd sol₁ = mk gd sol₂ ↔ ∃ (g : gd.GaugeGroup), gd.gauge_action g sol₁ = sol₂

Two elements of the moduli quotient are equal iff the underlying solutions are gauge-equivalent.

theorem GaugeActionData.gaugeEquivSetoid_iff_orbitRel {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] {spinc : SpinCStructure M Ω1 Ω2} (gd : GaugeActionData spinc) (sol₁ sol₂ : SWSolution spinc) : gd.gaugeEquivSetoid sol₁ sol₂ ↔ ∃ (g : gd.GaugeGroup), gd.gauge_action g sol₁ = sol₂

The setoid relation on solutions is exactly the gauge orbit relation: $\mathrm{sol}_1 \sim \mathrm{sol}_2$ iff $\exists g, g \cdot \mathrm{sol}_1 = \mathrm{sol}_2$.

def IsSelfDual {Ω2 : Type u_1} (hodge_star : Ω2 → Ω2) (ω : Ω2) : Prop

A 2-form $\omega$ is self-dual if $*\omega = \omega$.

def IsAntiSelfDual {Ω2 : Type u_1} [Neg Ω2] (hodge_star : Ω2 → Ω2) (ω : Ω2) : Prop

A 2-form $\omega$ is anti-self-dual if $*\omega = -\omega$.

structure CliffordIsomorphisms {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} {Ω0 : Type u_4} {Ω3 : Type u_5} {Ω4 : Type u_6} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] [AddCommGroup Ω0] [Module ℝ Ω0] [AddCommGroup Ω3] [Module ℝ Ω3] [AddCommGroup Ω4] [Module ℝ Ω4] (spinc : SpinCStructure M Ω1 Ω2) : Type (max (max (max (max (max 1 u_2) u_3) u_4) u_5) u_6)

The Clifford module isomorphisms relating differential forms and spinor endomorphisms on a Spin-c 4-manifold: the decomposition $\Omega^2 = \Omega^{2,+} \oplus \Omega^{2,-}$, the full Clifford equivalence $\Omega^0 \oplus \Omega^1 \oplus \Omega^2 \oplus \Omega^3 \oplus \Omega^4 \simeq \mathrm{End}(S^+ \oplus S^-)$, and its even/odd splittings, together with the $\mathrm{End}(S^\pm) \simeq \mathbb{C} \oplus \Omega^{2,\pm}$ decompositions.

• instModCPlus : Module ℂ spinc.SectionsPlus
• instModCMinus : Module ℂ spinc.SectionsMinus
• Ω2plus : Type
• Ω2minus : Type
• instΩ2plus_acg : AddCommGroup self.Ω2plus
• instΩ2plus_mod : Module ℝ self.Ω2plus
• instΩ2minus_acg : AddCommGroup self.Ω2minus
• instΩ2minus_mod : Module ℝ self.Ω2minus
• incl_plus : self.Ω2plus →ₗ[ℝ] Ω2
• incl_minus : self.Ω2minus →ₗ[ℝ] Ω2
• self_dual_condition (ω : self.Ω2plus) : IsSelfDual spinc.hodge_star (self.incl_plus ω)
• anti_self_dual_condition (ω : self.Ω2minus) : IsAntiSelfDual spinc.hodge_star (self.incl_minus ω)
• γ_full_equiv : (Ω0 × Ω1 × Ω2 × Ω3 × Ω4) ≃ₗ[ℝ] ((spinc.SectionsPlus →ₗ[ℝ] spinc.SectionsPlus) × (spinc.SectionsMinus →ₗ[ℝ] spinc.SectionsMinus)) × (spinc.SectionsPlus →ₗ[ℝ] spinc.SectionsMinus) × (spinc.SectionsMinus →ₗ[ℝ] spinc.SectionsPlus)
• even_clifford_equiv : (Ω0 × Ω2 × Ω4) ≃ₗ[ℝ] (spinc.SectionsPlus →ₗ[ℝ] spinc.SectionsPlus) × (spinc.SectionsMinus →ₗ[ℝ] spinc.SectionsMinus)
• odd_clifford_equiv : (Ω1 × Ω3) ≃ₗ[ℝ] (spinc.SectionsPlus →ₗ[ℝ] spinc.SectionsMinus) × (spinc.SectionsMinus →ₗ[ℝ] spinc.SectionsPlus)
• endSplus_decomp : (spinc.SectionsPlus →ₗ[ℝ] spinc.SectionsPlus) ≃ₗ[ℝ] ℂ × self.Ω2plus
• endSminus_decomp : (spinc.SectionsMinus →ₗ[ℝ] spinc.SectionsMinus) ≃ₗ[ℝ] ℂ × self.Ω2minus

noncomputable def clifford_isomorphisms_exist {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} {Ω0 : Type u_4} {Ω3 : Type u_5} {Ω4 : Type u_6} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] [AddCommGroup Ω0] [Module ℝ Ω0] [AddCommGroup Ω3] [Module ℝ Ω3] [AddCommGroup Ω4] [Module ℝ Ω4] (spinc : SpinCStructure M Ω1 Ω2) : CliffordIsomorphisms spinc

Existence of the Clifford module isomorphisms for any Spin-c structure on a 4-manifold.

def GaugeEquiv {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] {spinc : SpinCStructure M Ω1 Ω2} (gauge : GaugeActionData spinc) (sol₁ sol₂ : SWSolution spinc) : Prop

Gauge equivalence of two Seiberg-Witten solutions: $\mathrm{sol}_1 \sim \mathrm{sol}_2$ iff there exists $f \in \mathcal{G}$ with $f \cdot \mathrm{sol}_1 = \mathrm{sol}_2$.

theorem GaugeEquiv.refl {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] {spinc : SpinCStructure M Ω1 Ω2} (gauge : GaugeActionData spinc) (sol : SWSolution spinc) : GaugeEquiv gauge sol sol

Reflexivity of gauge equivalence: every solution is gauge-equivalent to itself via $1 \in \mathcal{G}$.

structure SWModuliSpace {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] (spinc : SpinCStructure M Ω1 Ω2) [htop : Has4ManifoldTopology M] [Zero spinc.SectionsMinus] : Type (max (max 1 u_2) u_3)

The Seiberg-Witten moduli space $\mathcal{M}(S, g, \mu) = \{(A,\psi)\}/\mathcal{G}$ together with its expected dimension $d(S)$, total point count, and a well-defined signed count for the zero-dimensional case (whose absolute value is bounded by the cardinality).

• gauge : GaugeActionData spinc
• quotientType : Type
• quotientProj : SWSolution spinc → self.quotientType
• sol_is_solution (sol : SWSolution spinc) : IsSWSolution sol
• proj_faithful (sol₁ sol₂ : SWSolution spinc) : self.quotientProj sol₁ = self.quotientProj sol₂ ↔ GaugeEquiv self.gauge sol₁ sol₂
• expectedDim : ℤ
• numPoints : ℕ
• signedCount : ℤ
• signedCount_bound : self.signedCount.natAbs ≤ self.numPoints

structure HasSWInvariant (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] [htop : Has4ManifoldTopology M] : Type (max (max 1 u_2) u_3)

Axiomatic data for the Seiberg-Witten invariant $\mathrm{SW} : \mathrm{Spin}^c(M) \to \mathbb{Z}$ on a compact 4-manifold $M$ with $b_2^+ \geq 1$: $\mathrm{SW}$ vanishes when the moduli space is empty, equals the signed count in the zero-dimensional case, has finite support, and depends only on $c_1(L)$.

• b₂_plus_pos : (Has4ManifoldTopology.Q M).b₂_plus ≥ 1
• SW : SpinCStructure M Ω1 Ω2 → ℤ
• SW_empty (spinc : SpinCStructure M Ω1 Ω2) [Zero spinc.SectionsMinus] : (∀ (sol : SWSolution spinc), ¬IsSWSolution sol) → self.SW spinc = 0
• SW_count_dim_zero (spinc : SpinCStructure M Ω1 Ω2) [Zero spinc.SectionsMinus] (Mod : SWModuliSpace spinc) : Mod.expectedDim = 0 → self.SW spinc = Mod.signedCount
• SW_finiteness : {spinc : SpinCStructure M Ω1 Ω2 | self.SW spinc ≠ 0}.Finite
• SW_of_c₁ : ℤ → ℤ
• SW_eq_SW_of_c₁ (spinc : SpinCStructure M Ω1 Ω2) : self.SW spinc = self.SW_of_c₁ spinc.c₁_L

class HasScalarCurvature (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] : Type

Typeclass recording a scalar curvature value $s$ for the Riemannian metric on $M$.

• scalarCurvature : ℝ

theorem no_reducibles_axiom {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [htop : Has4ManifoldTopology M] (hb₂_pos : (Has4ManifoldTopology.Q M).b₂_plus ≥ 1) {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) : ¬sol.isReducible

For $b_2^+(M) \geq 1$ and a generic perturbation, no Seiberg-Witten solution is reducible (stated here as an axiom).

theorem sc_compat_axiom {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [hsc : HasScalarCurvature M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) : sol.scalarCurvatureVal = HasScalarCurvature.scalarCurvature M

Compatibility axiom: the abstract scalar curvature value carried by a Seiberg-Witten solution agrees with the scalar curvature of $M$.

theorem weitzenboeck_maximum_principle {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [hsc : HasScalarCurvature M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) (hsc_eq : sol.scalarCurvatureVal = HasScalarCurvature.scalarCurvature M) : HasScalarCurvature.scalarCurvature M * sol.supNormSq + sol.supNormSq ^ 2 ≤ 0

Weitzenböck maximum principle: at a point of maximum of $|\psi|^2$ on a compact manifold, the Bochner identity yields $s \cdot |\psi|^2 + |\psi|^4 \leq 0$.

theorem sw_apriori_bound {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [hsc : HasScalarCurvature M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) (hsc_eq : sol.scalarCurvatureVal = HasScalarCurvature.scalarCurvature M) : sol.supNormSq ≤ max (-HasScalarCurvature.scalarCurvature M) 0

A priori bound on the spinor of a Seiberg-Witten solution: $\sup|\psi|^2 \leq \max(-s, 0)$.

theorem positive_scalar_curvature_vanishing {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [htop : Has4ManifoldTopology M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] (hSW : HasSWInvariant M Ω1 Ω2) [hsc : HasScalarCurvature M] (hs_pos : HasScalarCurvature.scalarCurvature M > 0) (spinc : SpinCStructure M Ω1 Ω2) [Zero spinc.SectionsMinus] : hSW.SW spinc = 0

Positive scalar curvature vanishing theorem: if $M$ admits a metric of positive scalar curvature ($s > 0$), then $\mathrm{SW}(\mathfrak{s}) = 0$ for every Spin-c structure $\mathfrak{s}$.

def s2_cross_s2_intersection_form : IntersectionForm

The intersection form of $S^2 \times S^2$: even hyperbolic form of rank 2, signature 0 with the off-diagonal pairing $\langle x, y\rangle = x_0 y_1 + x_1 y_0$.

def k3_intersection_form : IntersectionForm

The intersection form of the $K3$ surface: even of rank 22, with $b_2^+ = 3$, $b_2^- = 19$, and signature $-16$ (the form $2(-E_8) \oplus 3 H$).

def negOneCircle : Circle

The element $-1 \in S^1 \subset \mathbb{C}$ regarded as a member of the circle group.

theorem negOneCircle_sq : negOneCircle ^ 2 = 1

$(-1)^2 = 1$ in the circle group.

def SpinCGroupRel (Q : QuadraticForm ℝ (Fin 4 → ℝ)) : ↥(spinGroup Q) × Circle → ↥(spinGroup Q) × Circle → Prop

The equivalence relation defining $\mathrm{Spin}^c(4) = (\mathrm{Spin}(4) \times S^1)/\{\pm 1\}$ on pairs $(p, z) \in \mathrm{Spin}(Q) \times S^1$: $(p, z) \sim (-p, -z)$.

def SpinCGroup (Q : QuadraticForm ℝ (Fin 4 → ℝ)) : Type

The Spin-c group $\mathrm{Spin}^c(Q) = (\mathrm{Spin}(Q) \times S^1)/\{\pm 1\}$.

def SpinCGroup.mk (Q : QuadraticForm ℝ (Fin 4 → ℝ)) : ↥(spinGroup Q) × Circle → SpinCGroup Q

The canonical projection $\mathrm{Spin}(Q) \times S^1 \to \mathrm{Spin}^c(Q)$.

noncomputable def SpinCGroup.det (Q : QuadraticForm ℝ (Fin 4 → ℝ)) : SpinCGroup Q → Circle

The determinant homomorphism $\det : \mathrm{Spin}^c(Q) \to S^1$, $[p, z] \mapsto z^2$, well-defined modulo $\{\pm 1\}$.

theorem spinc_theorem3_complete {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [CompactSpace M] [htop : Has4ManifoldTopology M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] : ∃ (c₁_map : SpinCStructure M Ω1 Ω2 → Fin (Has4ManifoldTopology.Q M).b₂ → ℤ), Nonempty (SpinCStructure M Ω1 Ω2) ∧ (∀ (c : Fin (Has4ManifoldTopology.Q M).b₂ → ℤ), {s : SpinCStructure M Ω1 Ω2 | c₁_map s = c}.Finite ∧ ∃ (k : ℕ), Nat.card ↑{s : SpinCStructure M Ω1 Ω2 | c₁_map s = c} ≤ 2 ^ k) ∧ (∀ (s : SpinCStructure M Ω1 Ω2) (α : Fin (Has4ManifoldTopology.Q M).b₂ → ℤ), (Has4ManifoldTopology.Q M).bilinForm (c₁_map s) α % 2 = (Has4ManifoldTopology.Q M).bilinForm α α % 2) ∧ ∀ (s : SpinCStructure M Ω1 Ω2), (Has4ManifoldTopology.Q M).bilinForm (c₁_map s) (c₁_map s) = s.c₁_L

Classification of $\mathrm{Spin}^c$-structures: on a compact simply-connected 4-manifold, the set $\mathrm{Spin}^c(M)$ is nonempty, the first Chern class map $c_1 : \mathrm{Spin}^c(M) \to H^2(X;\mathbb{Z})$ has finite fibres of size at most $2^k$ (2-torsion ambiguity), its image consists of characteristic elements (i.e. $\langle c_1, \alpha\rangle \equiv Q(\alpha,\alpha) \pmod 2$), and $c_1(L) \cdot c_1(L) = c_1(L)^2$.