def chartTransition {d : ℕ} {N : Type u_1} [TopologicalSpace N] [ChartedSpace (EuclideanSpace ℝ (Fin d)) N] (e e' : ↑(atlas (EuclideanSpace ℝ (Fin d)) N)) : OpenPartialHomeomorph (EuclideanSpace ℝ (Fin d)) (EuclideanSpace ℝ (Fin d))

The transition map between two charts $e, e'$ of a charted space, given by $e^{-1}$ followed by $e'$.

def chartTransitionPreservesOrientation {d : ℕ} {N : Type u_1} [TopologicalSpace N] [ChartedSpace (EuclideanSpace ℝ (Fin d)) N] (e e' : ↑(atlas (EuclideanSpace ℝ (Fin d)) N)) : Prop

A chart transition preserves orientation iff its Jacobian determinant is positive everywhere on its source.

def IsOrientableManifold (d : ℕ) (N : Type u_1) [TopologicalSpace N] [ChartedSpace (EuclideanSpace ℝ (Fin d)) N] : Prop

A $d$-dimensional charted space is orientable when every pair of chart transitions has positive Jacobian determinant.

class IsGenericPair {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ M] [CompactSpace M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] [htop : Has4ManifoldTopology M] (spinc : SpinCStructure M Ω1 Ω2) : Type (max u_2 u_3)

A generic pair $(g, \mu)$ ensures that the Seiberg–Witten linearization is surjective at irreducible solutions, the cokernel dimension is zero, and the Fredholm index equals $\tfrac{1}{4}(c_1(L)^2 \cdot [X] - (2\chi + 3\sigma))$.

• cokerDim : SWSolution spinc → ℕ
• fredholmIndex : SWSolution spinc → ℤ
• fredholmIndex_eq (sol : SWSolution spinc) : fredholmIndex sol * 4 = spinc.c₁_L - (2 * Has4ManifoldTopology.euler M + 3 * (Has4ManifoldTopology.Q M).signature)
• linearised_surjective (sol : SWSolution spinc) : ¬sol.isReducible → cokerDim sol = 0
• no_reducible_solutions : (Has4ManifoldTopology.Q M).b₂_plus ≥ 1 → ∀ (sol : SWSolution spinc), ¬sol.isReducible

def SWGaugeEquivalent {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

Two SW solutions are gauge-equivalent if some element $f \in \mathcal{G}$ of the gauge group maps one to the other.

theorem SWGaugeEquivalent.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) : SWGaugeEquivalent gauge sol sol

Gauge equivalence is reflexive: every SW solution is gauge-equivalent to itself via the identity gauge transformation.

structure SWModuliSmoothManifold {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ M] [CompactSpace 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] [IsGenericPair spinc] : Type (max (max 1 u_2) u_3)

Definition 2: a smooth-manifold structure on the SW moduli space $\mathcal{M}(S, g, \mu) = \{\text{SW solutions}\}/\mathcal{G}$, with the quotient projection identifying gauge orbits with points.

• dimension : ℕ
• carrier : Type
• topologicalSpace : TopologicalSpace self.carrier
• chartedSpace : ChartedSpace (EuclideanSpace ℝ (Fin self.dimension)) self.carrier
• isManifold : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin self.dimension))) ⊤ self.carrier
• orientable : IsOrientableManifold self.dimension self.carrier
• gauge : GaugeActionData spinc
• quotientProj : SWSolution spinc → self.carrier
• proj_identifies_orbits (sol₁ sol₂ : SWSolution spinc) : SWGaugeEquivalent self.gauge sol₁ sol₂ → self.quotientProj sol₁ = self.quotientProj sol₂
• proj_injective (sol₁ sol₂ : SWSolution spinc) : self.quotientProj sol₁ = self.quotientProj sol₂ → SWGaugeEquivalent self.gauge sol₁ sol₂

structure SWModuliManifold {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ M] [CompactSpace 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] [IsGenericPair spinc] : Type (max (max 1 u_2) u_3)

The SW moduli space packaged as a compact smooth manifold (smooth manifold structure plus compactness).

• smooth : SWModuliSmoothManifold spinc
• compactSpace : CompactSpace self.smooth.carrier

theorem sw_moduli_smooth_structure_axiom {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ M] [CompactSpace M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] [htop : Has4ManifoldTopology M] (spinc : SpinCStructure M Ω1 Ω2) [hgeneric : IsGenericPair spinc] : ∃ (sm : SWModuliSmoothManifold spinc), (∀ (sol : SWSolution spinc), ↑sm.dimension = IsGenericPair.fredholmIndex sol) ∧ (Nonempty sm.carrier → Nonempty (SWSolution spinc))

Axiomatic input: for a generic pair, the SW moduli space carries a smooth manifold structure whose dimension equals the Fredholm index.

theorem sw_moduli_compactness_axiom {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ M] [CompactSpace M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] [htop : Has4ManifoldTopology M] (spinc : SpinCStructure M Ω1 Ω2) [hgeneric : IsGenericPair spinc] (sm : SWModuliSmoothManifold spinc) : CompactSpace sm.carrier

Axiomatic input: the SW moduli space is compact (Uhlenbeck-type a priori estimates).

theorem sw_moduli_dimension_formula {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ M] [CompactSpace M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] [htop : Has4ManifoldTopology M] (spinc : SpinCStructure M Ω1 Ω2) [hgeneric : IsGenericPair spinc] (sm : SWModuliSmoothManifold spinc) (hdim_eq_index : ∀ (sol : SWSolution spinc), ↑sm.dimension = IsGenericPair.fredholmIndex sol) (sol : SWSolution spinc) : ↑sm.dimension * 4 = spinc.c₁_L - (2 * Has4ManifoldTopology.euler M + 3 * (Has4ManifoldTopology.Q M).signature)

Dimension formula: $4 \cdot \dim \mathcal{M} = c_1(L)^2 \cdot [X] - (2\chi + 3\sigma)$, obtained by combining the Fredholm index identity with $\dim \mathcal{M} = \mathrm{ind}$.

theorem sw_moduli_space_theorem1 {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ M] [CompactSpace M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] [htop : Has4ManifoldTopology M] (spinc : SpinCStructure M Ω1 Ω2) [hgeneric : IsGenericPair spinc] : ∃ (Mod : SWModuliManifold spinc), Nonempty Mod.smooth.carrier → IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin Mod.smooth.dimension))) ⊤ Mod.smooth.carrier ∧ CompactSpace Mod.smooth.carrier ∧ IsOrientableManifold Mod.smooth.dimension Mod.smooth.carrier ∧ ↑Mod.smooth.dimension * 4 = spinc.c₁_L - (2 * Has4ManifoldTopology.euler M + 3 * (Has4ManifoldTopology.Q M).signature)

Theorem 1: for generic $(g, \mu)$, the SW moduli space $\mathcal{M}$ is a smooth, compact, orientable manifold of dimension $d(S) = \tfrac{1}{4}(c_1(L)^2 \cdot [X] - (2\chi + 3\sigma))$.