Taubes–Gromov theory
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
TheoremThe good-curve component inequality#
If e = ∑ m i • C i is a combination with natural
coefficients of classes which meet pairwise nonnegatively, and e is at least -1 on every
class C i of negative square (as for a good class and exceptional spheres), then the virtual
dimensions d(x) = x · x - κ · x satisfy ∑ m i d(C i) ≤ d(e).
TauCeti.sum_mul_apply_self_sub_apply_canonical_le.{u_1, u_2} {H : Type u_1} {ι : Type u_2}
[AddCommGroup H] [Fintype ι] {B : LinearMap.BilinForm ℤ H} {κ e : H} {C : ι → H} {m : ι → ℕ}
(he : ∑ i, m i • C i = e) (hpos : ∀ {i j : ι}, i ≠ j → 0 ≤ (B (C i)) (C j))
(hgood : ∀ (i : ι), (B (C i)) (C i) < 0 → -1 ≤ (B e) (C i)) :
∑ i, ↑(m i) * ((B (C i)) (C i) - (B κ) (C i)) ≤ (B e) e - (B κ) e
Lean
Formalized in Tau Ceti as TauCeti.sum_mul_apply_self_sub_apply_canonical_le.
Sources
TheoremTauCeti.IsGoodCycle.apply_self_eq_zero_of_one_lt_mult#
An image occurring with multiplicity at least two has square zero.
TauCeti.IsGoodCycle.apply_self_eq_zero_of_one_lt_mult.{u_1, u_2, u_3} {H : Type u_1} {ι : Type u_2}
{P : Type u_3} [AddCommGroup H] [Fintype ι] {B : LinearMap.BilinForm ℤ H} {κ e : H} {C : ι → H}
{m : ι → ℕ} [Fintype P] {δ : ι → ℕ} {pts : ι → Finset P} (hB : B.IsSymm)
(h : TauCeti.IsGoodCycle B κ e C m δ pts) {i : ι} (hi : 1 < m i) : (B (C i)) (C i) = 0
Lean
Formalized in Tau Ceti as TauCeti.IsGoodCycle.apply_self_eq_zero_of_one_lt_mult.
Sources
Uses 1
TheoremIndependent-component expansion of the ray series#
its n-th coefficient is the sum,
over all configurations l of total class n • A₀ (the elements of
s.weightedFinsuppAntidiag m n), of the products of the local weights
w_(σ c, i c)(l c).
TauCeti.coeff_rayTorusWeightSeries.{u_1} {ι : Type u_1} (s : Finset ι) (m : ι → ℕ+) (σ : ι → Bool)
(i : ι → Fin 4) (n : ℕ) :
(PowerSeries.coeff n) (TauCeti.rayTorusWeightSeries s m σ i) =
∑ l ∈ s.weightedFinsuppAntidiag m n, ∏ c ∈ s, TauCeti.torusWeight (σ c) (i c) (l c)
Uses 1
TheoremThe Weitzenböck identity at the vacuum on tempered fields#
L₀* L₀ = -Δ + 1 / 4.
TauCeti.Vortex.temperedVacuumAdjoint_temperedVacuumOperator (x : Fin 4 → TemperedDistribution ℂ ℂ) :
TauCeti.Vortex.temperedVacuumAdjoint (TauCeti.Vortex.temperedVacuumOperator x) = fun i =>
-Laplacian.laplacian (x i) + (1 / 4) • x i
Lean
Formalized in Tau Ceti as TauCeti.Vortex.temperedVacuumAdjoint_temperedVacuumOperator.
Other forms
The Weitzenböck identity at the vacuum. Formalized in Tau Ceti as TauCeti.Vortex.vacuumAdjoint_vacuumOperator.
TauCeti.Vortex.vacuumAdjoint_vacuumOperator (x : SchwartzMap ℂ (EuclideanSpace ℝ (Fin 4))) :
TauCeti.Vortex.vacuumAdjoint (TauCeti.Vortex.vacuumOperator x) =
-Laplacian.laplacian x + (1 / 4) • x
Sources
Used by 1
DefinitionThe vacuum operator is invertible on tempered fields#
L₀ as a continuous linear
automorphism of the fields of tempered distributions. Its inverse is L₀⁻¹ = L₀* (-Δ + 1 / 4)⁻¹
(temperedVacuumOperatorEquiv_symm_apply).
TauCeti.Vortex.temperedVacuumOperatorEquiv :
(Fin 4 → TemperedDistribution ℂ ℂ) ≃L[ℂ] Fin 4 → TemperedDistribution ℂ ℂ
Uses 2 · Used by 1
TheoremThe vacuum operator restricts to a bijection H^s → H^{s-1}#
a tempered field x lies in
H^s if and only if L₀ x lies in H^{s-1}. Since L₀ is bijective on tempered fields
(temperedVacuumOperatorEquiv), it restricts to a bijection from H^s onto H^{s-1}, for every
real s.
TauCeti.Vortex.memSobolev_temperedVacuumOperator_iff {x : Fin 4 → TemperedDistribution ℂ ℂ}
{s : ℝ} :
(∀ (i : Fin 4),
TemperedDistribution.MemSobolev (s - 1) 2 (TauCeti.Vortex.temperedVacuumOperator x i)) ↔
∀ (i : Fin 4), TemperedDistribution.MemSobolev s 2 (x i)
Lean
Formalized in Tau Ceti as TauCeti.Vortex.memSobolev_temperedVacuumOperator_iff.
Sources
TheoremThe integral Wang torsion order#
If H₁(F; ℤ) is free of finite rank and
det (1 - φ_*) ≠ 0 on it, the torsion subgroup of H₁(T_φ; ℤ) has order |det (1 - φ_*)|.
TauCeti.MappingTorus.card_torsion_homology_one_eq_natAbs_det {F : Type} [TopologicalSpace F]
(φ : F ≃ₜ F)
[Module.Free ℤ
↑(HomologicalComplex.homology
(((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj ↧ℤ).obj ↧F) 1)]
[Module.Finite ℤ
↑(HomologicalComplex.homology
(((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj ↧ℤ).obj ↧F) 1)]
(hdet :
LinearMap.det
(LinearMap.id -
ModuleCat.Hom.hom
(HomologicalComplex.homologyMap (TauCeti.MappingTorus.monodromyChainMap φ ↧ℤ) 1)) ≠
0) :
Nat.card
↥(Submodule.torsion ℤ
↑(HomologicalComplex.homology
(((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj ↧ℤ).obj
↧(TauCeti.MappingTorus φ))
1)) =
(LinearMap.det
(LinearMap.id -
ModuleCat.Hom.hom
(HomologicalComplex.homologyMap (TauCeti.MappingTorus.monodromyChainMap φ ↧ℤ)
1))).natAbs
Lean
Formalized in Tau Ceti as TauCeti.MappingTorus.card_torsion_homology_one_eq_natAbs_det.
Sources
TheoremOrbit-torus weights are local zeta factors#
Let P be a 2 × 2 matrix of determinant
one all of whose iterates are nondegenerate, det (1 - P ^ k) ≠ 0 for k ≥ 1. Read off the label
σ = (0 < det (1 - P)) and i = 1 if det (1 + P) < 0, i = 0 otherwise. Then the local series
f = f_(σ, i) satisfies t f' = f ∑_{k ≥ 1} sgn det (1 - P ^ k) t ^ k; over ℚ this says
log f = ∑_{k ≥ 1} sgn det (1 - P ^ k) t ^ k / k.
TauCeti.X_mul_derivative_torusWeightSeries_of_det_eq_one.{u_1} {R : Type u_1} [CommRing R]
[LinearOrder R] [IsStrictOrderedRing R] {P : Matrix (Fin 2) (Fin 2) R} (hdet : P.det = 1)
(hP : ∀ (k : ℕ), k ≠ 0 → (1 - P ^ k).det ≠ 0) :
PowerSeries.X *
PowerSeries.derivative
(TauCeti.torusWeightSeries (decide (0 < (1 - P).det)) (if (1 + P).det < 0 then 1 else 0)) =
TauCeti.torusWeightSeries (decide (0 < (1 - P).det)) (if (1 + P).det < 0 then 1 else 0) *
PowerSeries.mk fun k => if k = 0 then 0 else ↑(SignType.sign (1 - P ^ k).det)
Lean
Formalized in Tau Ceti as TauCeti.X_mul_derivative_torusWeightSeries_of_det_eq_one.
Sources
Uses 2
DefinitionTauCeti.torusWeightSeries#
The local multiplicity series f_(σ, i) ∈ ℤ⟦X⟧ attached to an embedded square-zero
pseudoholomorphic torus with determinant sign σ (true for +, false for -) and with
i negative signs among its three nontrivially twisted normal operators. The positive series
are 1 / (1 - X), 1 + X, (1 + X) / (1 + X ^ 2) and (1 + X) (1 - X ^ 2) / (1 + X ^ 2),
and each negative series is the inverse of the positive series with the same index. The weight
of the torus with multiplicity m is the coefficient coeff m (torusWeightSeries σ i).
TauCeti.torusWeightSeries (σ : Bool) (i : Fin 4) : PowerSeries ℤ
DefinitionTemperedDistribution.laplacianResolvent#
The resolvent of the Laplacian (c - Δ)⁻¹ on tempered distributions: the Fourier
multiplier with symbol ((2π)² ‖ξ‖² + c)⁻¹. For c > 0 it is the two-sided inverse of -Δ + c
(laplacianResolvent_neg_laplacian_add_smul and neg_laplacian_laplacianResolvent_add_smul);
for c ≤ 0 the value is not meaningful.
TemperedDistribution.laplacianResolvent.{u_1, u_2} {E : Type u_1} (F : Type u_2)
[NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
[BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (c : ℝ) :
TemperedDistribution E F →L[ℂ] TemperedDistribution E F
TheoremElliptic regularity for the shifted Laplacian#
for c > 0, a tempered distribution f
lies in the Sobolev space H^{s+2} if and only if -Δ f + c f lies in H^s.
TemperedDistribution.memSobolev_add_two_iff_neg_laplacian_add_smul.{u_1, u_2} {E : Type u_1}
{F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
[MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F]
[CompleteSpace F] {c s : ℝ} (hc : 0 < c) {f : TemperedDistribution E F} :
TemperedDistribution.MemSobolev (s + 2) 2 f ↔
TemperedDistribution.MemSobolev s 2 (-Laplacian.laplacian f + c • f)
Lean
Formalized in Tau Ceti as TemperedDistribution.memSobolev_add_two_iff_neg_laplacian_add_smul.
Sources
Uses 1
StructureTauCeti.IsGoodCycle#
The numerical properties of a positive cycle ∑ m i • C i of distinct simple
pseudoholomorphic images in a good class e of a symplectic four-manifold with canonical class
κ, passing through generic points indexed by P, read in the intersection form B on
integral homology. The image C i has singularity number δ i and contains the points pts i.
The fields say: the multiplicities are positive; distinct images meet nonnegatively; the number
of points on an image is at most half the index d(C i) - 2 δ i of simple curves in its class,
where d(x) = x · x - κ · x; the good class e is at least -1 on every image of negative
square; the cycle represents e; every point lies on some image; and the number of points is
half the virtual dimension of e. The square -1 of an image of negative square, which
adjunction forces for an exceptional sphere, then follows (IsGoodCycle.apply_self_eq_neg_one).
TauCeti.IsGoodCycle.{u_1, u_2, u_3} {H : Type u_1} {ι : Type u_2} {P : Type u_3} [AddCommGroup H]
[Fintype ι] [Fintype P] (B : LinearMap.BilinForm ℤ H) (κ e : H) (C : ι → H) (m δ : ι → ℕ)
(pts : ι → Finset P) : Prop
Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.