theorem
SWModuliQuotient.mk_surjective
{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)
:
Function.Surjective (mk gd)
The canonical quotient map from Seiberg–Witten solutions to the moduli space $\mathcal{M} = \{\text{SW solutions}\}/\mathcal{G}$ is surjective.
def
SWModuliQuotient.supNormSq
{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)
(q : SWModuliQuotient gd)
:
Gauge-invariant sup-norm-squared $\|\Phi\|_\infty^2$ descends to the moduli quotient.
Instances For
theorem
SWModuliQuotient.supNormSq_nonneg
{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)
(q : SWModuliQuotient gd)
:
The sup-norm-squared on the moduli quotient is nonnegative.
def
SWModuliQuotient.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}
(gd : GaugeActionData spinc)
(q : SWModuliQuotient gd)
:
A moduli class is reducible iff its sup-norm-squared vanishes, i.e. the spinor field $\Phi$ is identically zero.
Instances For
theorem
SWModuliQuotient.no_reducibles_generic
{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}
(gd : GaugeActionData spinc)
[hgeneric : IsGenericPair spinc]
(hb₂_pos : (Has4ManifoldTopology.Q M).b₂_plus ≥ 1)
(sol : SWSolution spinc)
:
¬IsReducible gd (mk gd sol)
When $b_2^+ \geq 1$ and the metric/perturbation pair is generic, no SW solution descends to a reducible class in the moduli space.
theorem
SWModuliQuotient.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}
(gd : GaugeActionData spinc)
[hgeneric : IsGenericPair spinc]
:
Dimension formula for the SW moduli space: $4d = c_1(L)^2 - (2\chi(M) + 3\sigma(M))$ for some integer $d \in \mathbb{Z}$.