A tangent-bundle splitting compatible with a 2-form $\eta$.
Encodes a decomposition $TM = V \oplus H$ into vertical and horizontal subbundles via
projections projV and projH. Contraction with $\eta$ (and with any $(p+1)$-form)
distributes over the splitting, the projections are idempotent and mutually
annihilating, and the splitting is "orthogonal" with respect to $\eta$ in the sense
that $\iota_{V Y} \iota_{H X} \eta = 0$.
- projV : VF → VF
- projH : VF → VF
- decompose (X : VF) {p : ℕ} (α : Ω (p + 1)) : DifferentialFormSpace.ι X α = DifferentialFormSpace.ι (projV η X) α + DifferentialFormSpace.ι (projH η X) α
- orthogonal (X Y : VF) : DifferentialFormSpace.ι (projV η Y) (DifferentialFormSpace.ι (projH η X) η) = 0
Instances
A symplectic fibration $f: M \to B$ with generic fiber $(F, \omega_F)$ symplectic.
Bundles together the projection f, the fiber inclusion, the symplectic form on the
fiber, and an open cover with local trivializations whose transition maps preserve
$\omega_F$. The cocycle and inverse axioms ensure the data really comes from a
fiber-bundle structure with structure group $\mathrm{Symp}(F,\omega_F)$.
- f : DFSMorphism Ω_M VF_M Ω_B VF_B
- fiberInclusion : DFSMorphism Ω_F VF_F Ω_M VF_M
- fiberSymplectic : SymplecticManifold Ω_F VF_F
- CoverIdx : Type
- localTriv : self.CoverIdx → DFSMorphism Ω_F VF_F Ω_M VF_M
- localTriv_symplectic (i : self.CoverIdx) (η : Ω_M 2) : self.fiberInclusion.pullback η = self.fiberSymplectic.ω → (self.localTriv i).pullback η = self.fiberSymplectic.ω
- transitionMap : self.CoverIdx → self.CoverIdx → DFSMorphism Ω_F VF_F Ω_F VF_F
- transition_preserves_symplectic (i j : self.CoverIdx) : (self.transitionMap i j).pullback self.fiberSymplectic.ω = self.fiberSymplectic.ω
- transition_inverse (i j : self.CoverIdx) {p : ℕ} (α : Ω_F p) : (self.transitionMap i j).pullback ((self.transitionMap j i).pullback α) = α
- transition_cocycle (i j k : self.CoverIdx) {p : ℕ} (α : Ω_F p) : (self.transitionMap j k).pullback ((self.transitionMap i j).pullback α) = (self.transitionMap i k).pullback α
- transition_diagonal (i : self.CoverIdx) {p : ℕ} (α : Ω_F p) : (self.transitionMap i i).pullback α = α
Instances For
Tangent-bundle data for a symplectic fibration adapted to a closed 2-form $\tilde\eta$ that restricts to the fiber symplectic form $\omega_F$.
Packages a TangentSplitting for $\tilde\eta$ together with a vertical restriction
map $VF_M \to VF_F$, with axioms saying the vertical part kills base-pulled forms,
restriction is compatible with contraction by $\tilde\eta$, the restriction is
injective on verticals, and a non-degeneracy criterion in the horizontal direction
detected by the base symplectic form.
- splitting : TangentSplitting η_tilde
- restrictV : VF_M → VF_F
- vertical_kills_base (X : VF_M) {p : ℕ} (β : Ω_B (p + 1)) : DifferentialFormSpace.ι (TangentSplitting.projV η_tilde X) (fib.f.pullback β) = 0
- restrictV_compat (X : VF_M) : fib.fiberInclusion.pullback (DifferentialFormSpace.ι (TangentSplitting.projV η_tilde X) η_tilde) = DifferentialFormSpace.ι (self.restrictV (TangentSplitting.projV η_tilde X)) (fib.fiberInclusion.pullback η_tilde)
- restrictV_inj (X Y : VF_M) : self.restrictV (TangentSplitting.projV η_tilde X) = self.restrictV (TangentSplitting.projV η_tilde Y) → TangentSplitting.projV η_tilde X = TangentSplitting.projV η_tilde Y
- horizontal_nondegen (baseSymplectic : SymplecticManifold Ω_B VF_B) (X Y : VF_M) : TangentSplitting.projV η_tilde X = TangentSplitting.projV η_tilde Y → DifferentialFormSpace.ι X (fib.f.pullback baseSymplectic.ω) = DifferentialFormSpace.ι Y (fib.f.pullback baseSymplectic.ω) → X = Y
Instances For
Existence of a tangent-bundle splitting on the total space of a symplectic fibration adapted to a closed 2-form $\tilde\eta$ that restricts to $\omega_F$ on fibers.
Instances For
Vertical-data packaging for a fibration tangent splitting: produces the vertical restriction map $VF_M \to VF_F$ together with the three key axioms (vertical kills base-pulled forms, restriction compatibility with $\tilde\eta$, and injectivity of restriction on vertical vectors).
Instances For
Vertical vectors annihilate base-pulled-back forms: $\iota_{\mathrm{projV}\,X}\,f^*\beta = 0$ for any $\beta \in \Omega_B^{p+1}$.
Restriction map $VF_M \to VF_F$ on the vertical part of the splitting, together with its compatibility with contraction by $\tilde\eta$ and its injectivity on verticals.
Instances For
Horizontal non-degeneracy: if $X, Y$ have the same vertical part and agree on contraction with $f^*\omega_B$, then $X = Y$. This expresses non-degeneracy of the base symplectic form in the horizontal direction.
The complete tangent-bundle data on the total space of a symplectic fibration
used in the proof of Thurston's theorem: assembles the splitting, vertical
restriction, kills-base, restriction compatibility, restriction injectivity, and
horizontal non-degeneracy into a single FibrationTangentBundle.
Instances For
Non-degeneracy is an open condition under small perturbations.
If a "vertical" injectivity criterion holds for the form $\omega_0$, then for all sufficiently large $k$ it also holds for the perturbed form $\omega_0 + k^{-1}\eta$. This underlies the rescaling step in Thurston's construction.
Extracts the underlying TangentSplitting from the Thurston fibration tangent bundle.
Instances For
Applied to the Thurston splitting: vertical vectors annihilate pullbacks of base forms.
The vertical restriction map $VF_M \to VF_F$ used in the Thurston construction.
Instances For
Compatibility of the vertical restriction map with contraction by $\tilde\eta$: $i_F^*(\iota_{\mathrm{projV}\,X}\tilde\eta) = \iota_{\mathrm{restrictV}(\mathrm{projV}\,X)}(i_F^*\tilde\eta)$.
Injectivity of the vertical restriction map: agreement of $\mathrm{restrictV}$ on vertical vectors implies equality of the verticals themselves.
Horizontal non-degeneracy for the Thurston splitting: equality of $X, Y$ follows from equality of their vertical parts and of their contractions with $f^*\omega_B$.
Perturbation stability for the Thurston splitting: if a 2-form $\omega_0$ satisfies
the vertical injectivity criterion, so does $\omega_0 + k^{-1}\tilde\eta$ for all
sufficiently large $k$. Specialization of nondegeneracy_open_condition.
Pulling back the base symplectic form to $M$ and then restricting to a fiber gives zero: $i_F^* f^* \omega_B = 0$, since $f$ is constant on each fiber.
The fiber-inclusion pullback is surjective: every form $\beta$ on the fiber arises as $i_F^* \gamma$ for some form $\gamma$ on $M$. Follows from the existence of a local trivialization whose pullback agrees with $i_F^*$.
Global correction step in Thurston's theorem.
Given a closed 2-form $\eta$ on $M$ whose restriction to the fiber is cohomologous to
$\omega_F$ (i.e. $i_F^*\eta = \omega_F + d\beta$), one can find a 1-form
correction on $M$ such that $\eta + d(\text{correction})$ restricts exactly to
$\omega_F$ on each fiber.
Auxiliary class bundling the data needed for Thurston's construction: a tangent splitting compatible with $\eta$, vanishing of the base pullback on vertical vectors, vertical non-degeneracy of $\eta$, and (for sufficiently large $k$) non-degeneracy of $\eta + k\, f^*\omega_B$.
- projV : VF → VF
- projH : VF → VF
- decompose (X : VF) {p : ℕ} (α : Ω (p + 1)) : DifferentialFormSpace.ι X α = DifferentialFormSpace.ι (projV η X) α + DifferentialFormSpace.ι (projH η X) α
- complement_VH (X : VF) {p : ℕ} (α : Ω (p + 1)) : DifferentialFormSpace.ι (projV η (projH η X)) α = 0
- complement_HV (X : VF) {p : ℕ} (α : Ω (p + 1)) : DifferentialFormSpace.ι (projH η (projV η X)) α = 0
- orthogonal (X Y : VF) : DifferentialFormSpace.ι (projV η Y) (DifferentialFormSpace.ι (projH η X) η) = 0
- pullback_vanishes (X : VF) : DifferentialFormSpace.ι (TangentSplitting.projV η X) (fib.f.pullback baseSymplectic.ω) = 0
- eta_nondegen_vertical (X Y : VF) : DifferentialFormSpace.ι (TangentSplitting.projV η X) η = DifferentialFormSpace.ι (TangentSplitting.projV η Y) η → TangentSplitting.projV η X = TangentSplitting.projV η Y
- horiz_nondegen : ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (X Y : VF), TangentSplitting.projV η X = TangentSplitting.projV η Y → DifferentialFormSpace.ι X (η + ↑k • fib.f.pullback baseSymplectic.ω) = DifferentialFormSpace.ι Y (η + ↑k • fib.f.pullback baseSymplectic.ω) → X = Y
Instances
Vertical vectors annihilate $f^*\omega_B$, given the general kernel property of the splitting. Simple specialization to the base symplectic form.
$\eta$ is non-degenerate on vertical vectors. If $\iota_{\mathrm{projV}\,X}\eta = \iota_{\mathrm{projV}\,Y}\eta$, then $\mathrm{projV}\,X = \mathrm{projV}\,Y$.
The argument transfers the equation to the fiber via the pullback, uses the non-degeneracy of $\omega_F$, and injectivity of the vertical restriction map.
For all sufficiently large $k$, the perturbed form $\eta + k\, f^*\omega_B$ is non-degenerate on the horizontal directions of the splitting.
Recasts the rescaling identity $\eta + k\,f^*\omega_B = k(f^*\omega_B + k^{-1}\eta)$ and applies the open-condition stability hypothesis.
Re-export of the vertical non-degeneracy axiom of ThurstonSplittingData.
Two 1-forms are equal if they have the same contraction with every vector field. This is the non-degeneracy of the contraction pairing on 1-forms.
If $\iota_{X_V}\beta = 0$, then $\iota_{X_V}(\eta + k\beta) = \iota_{X_V}\eta$: contraction by a vector annihilating $\beta$ ignores the $\beta$ term.
Extraction step in Thurston's argument: if $\iota_X(\eta + k\beta) = \iota_Y(\eta + k\beta)$ and $\beta$ is killed by all vertical vectors, then the vertical parts of $X$ and $Y$ already agree when contracted against $\eta$: $\iota_{\mathrm{projV}\,X}\eta = \iota_{\mathrm{projV}\,Y}\eta$.
Pullback of the zero form is zero: $\varphi^*(0) = 0$.
Pullback of a closed form is closed: $d\alpha = 0 \implies d(\varphi^*\alpha) = 0$, since $\varphi^*$ commutes with $d$.
Thurston's theorem (full statement).
Let $f: M \to B$ be a compact symplectic fibration with fiber symplectic form
$\omega_F$ and base symplectic form $\omega_B$. Given a closed 2-form $\eta$ on $M$
whose restriction to each fiber is cohomologous to $\omega_F$ (i.e. $i_F^*\eta = \omega_F + d\beta$), there exists a 1-form correction correction and an integer
$k_0$ such that for all $k \geq k_0$, the form
$$\omega_k = (\eta + d(\text{correction})) + k\, f^*\omega_B$$
is a closed, non-degenerate symplectic form on $M$ that restricts to $\omega_F$ on
every fiber, and represents the cohomology class $[\eta] + k\,f^*[\omega_B]$.
Thurston's theorem (Definition / clean statement).
Compact locally trivial symplectic fibration with symplectic fiber and base: if there
exists $c \in H^2(M,\mathbb{R})$ restricting to $[\omega_F]$, then for $k \gg 0$
there is a symplectic form on $M$ in class $c + k\, f^*[\omega_B]$ whose fibers are
symplectic. Convenience re-export of thurston_symplectic_fibration_with_axioms.
Convex-combination step: if two 2-forms $\alpha_1, \alpha_2$ both restrict to $\omega_F$ on the fiber, then so does any affine combination $r_1\alpha_1 + r_2\alpha_2$ with $r_1 + r_2 = 1$.
Local complex coordinates $(z_1, z_2)$ on a 2-complex-dimensional patch: two 0-forms $z_1, z_2$ with their differentials $dz_1, dz_2$, where $dz_1 \neq 0$ and $dz_2$ is not a real multiple of $dz_1$ (so $\{dz_1, dz_2\}$ are linearly independent). Used to express the Lefschetz local model $(z_1, z_2) \mapsto z_1^2 + z_2^2$.
- z₁ : Ω 0
- z₂ : Ω 0
- dz₁ : Ω 1
- dz₂ : Ω 1
Instances For
A single local complex coordinate $w$ with non-zero differential $dw$, used as the target coordinate for the standard Lefschetz model $w = z_1^2 + z_2^2$.
- w : Ω 0
- dw : Ω 1
Instances For
The local model map $q: \mathbb{C}^2 \to \mathbb{C}$ at a Lefschetz critical point, characterized in coordinates by the formula $q^*(w) = z_1^2 + z_2^2$.
- q_formula : q.pullback coord_tgt.w = DifferentialFormSpace.fMul VF_src coords_src.z₁ coords_src.z₁ + DifferentialFormSpace.fMul VF_src coords_src.z₂ coords_src.z₂
Instances For
A map $f: M^4 \to B^2$ has the standard Lefschetz local quadratic model at a critical point: there exist local source and target charts and a model map $q$ such that $f$ pulls back to $q$ on the charted domain, $q$ has a critical point (degenerate contraction with some non-zero 1-form), a non-degenerate symplectic 2-form pulls back to a non-degenerate form upstairs, and the pair is the standard quadratic map $(z_1, z_2) \mapsto z_1^2 + z_2^2$ in suitable complex coordinates.
Instances For
An orientation on a differential-form space: a fixed top-degree dimension, a nowhere-vanishing closed volume form.
Instances
A Lefschetz fibration $f: M^4 \to \Sigma^2$ between oriented manifolds with a finite set of isolated critical points, each locally modeled in oriented complex coordinates as $\mathbb{C}^2 \to \mathbb{C}$, $(z_1, z_2) \mapsto z_1^2 + z_2^2$.
Carries:
- the map $f$,
- inclusion of a generic fiber,
- a finite list of critical points, and
- at each critical point, an instance of
HasLocalQuadraticModel.
- f : DFSMorphism Ω_M VF_M Ω_B2 VF_B2
- genericFiberInclusion : DFSMorphism Ω_F VF_F Ω_M VF_M
- numCriticalPoints : ℕ
- hasLocalModel : ∀ (x : Fin self.numCriticalPoints), HasLocalQuadraticModel self.f
Instances For
A vanishing cycle of a Lefschetz fibration: a (codimension-one) cycle in a generic fiber that collapses to a point at a designated critical point, encoded as a morphism from a "cycle" form space into the fiber form space along with the critical-point index.
- cycle : DFSMorphism Ω_S VF_S Ω_F VF_F
- criticalPointIndex : ℕ
Instances For
The monodromy representation of a Lefschetz fibration: for each singular fiber, a Dehn twist of the generic fiber, together with its inverse, satisfying the two-sided inverse axioms.
- numSingularFibers : ℕ
- dehnTwist : Fin self.numSingularFibers → DFSMorphism Ω_F VF_F Ω_F VF_F
- dehnTwistInv : Fin self.numSingularFibers → DFSMorphism Ω_F VF_F Ω_F VF_F
- left_inv (j : Fin self.numSingularFibers) {p : ℕ} (α : Ω_F p) : (self.dehnTwistInv j).pullback ((self.dehnTwist j).pullback α) = α
- right_inv (j : Fin self.numSingularFibers) {p : ℕ} (α : Ω_F p) : (self.dehnTwist j).pullback ((self.dehnTwistInv j).pullback α) = α
Instances For
The hypothesis "$[F] \neq 0 \in H_2(M, \mathbb{R})$" of Gompf's theorem, expressed dually: there exists a closed 2-form $\eta$ on $M$ whose restriction to the generic fiber is non-zero (so $[F]$ pairs non-trivially with the cohomology class $[\eta]$).
- exists_pairing_witness : ∃ (η : Ω_M 2), DifferentialFormSpace.d VF_M η = 0 ∧ lf.genericFiberInclusion.pullback η ≠ 0
Instances For
Gompf's theorem (1998).
If $f: M^4 \to \Sigma^2$ is a Lefschetz fibration with $[F] \neq 0 \in H_2(M,\mathbb{R})$, then $M$ carries a symplectic form $\omega_M$ whose restriction to each generic fiber is symplectic, exhibiting the fiber as a symplectic submanifold.
The symplectic manifold $S$ admits a blowup $\hat M$, i.e. there is a blowdown morphism $\hat M \to M$ with finitely many exceptional divisors $E_j$, each closed non-exact (so genuinely contributes to cohomology), and the blowdown is locally modeled by the standard quadratic blowup $\hat{\mathbb{C}^2} = \{(x, \ell) \in \mathbb{C}^2 \times \mathbb{CP}^1 : x \in \ell\}$.
- exists_blowdown : ∃ (blowdown : DFSMorphism Ω_Mhat VF_Mhat Ω_M VF_M) (numBlowups : ℕ) (_ : 0 < numBlowups) (exceptionalClass : Fin numBlowups → Ω_Mhat 2), (∀ (j : Fin numBlowups), DifferentialFormSpace.d VF_Mhat (exceptionalClass j) = 0) ∧ (∀ (j : Fin numBlowups), ¬∃ (β : Ω_Mhat 1), DifferentialFormSpace.d VF_Mhat β = exceptionalClass j) ∧ ∀ (_j : Fin numBlowups), HasLocalQuadraticModel blowdown
Instances
The differential-form space admits a Lefschetz fibration to $S^2$: there exist
form spaces for a 2-dimensional base $B$ and a fiber $F$, orientations on both
total space and base, a LefschetzFibration between them, and a symplectic 2-form
on $B$ which is closed, non-degenerate, and non-exact (modeling the $S^2$ symplectic
form).
- exists_fibration : ∃ (Ω_B : ℕ → Type u_3) (VF_B : Type u_4) (inst_B : DifferentialFormSpace Ω_B VF_B) (Ω_F : ℕ → Type u_5) (VF_F : Type u_6) (inst_F : DifferentialFormSpace Ω_F VF_F) (_orientM : IsOriented Ω VF) (_orientB : IsOriented Ω_B VF_B) (_lf : LefschetzFibration) (ωB : Ω_B 2), DifferentialFormSpace.d VF_B ωB = 0 ∧ (Function.Injective fun (X : VF_B) => DifferentialFormSpace.ι X ωB) ∧ ¬∃ (β : Ω_B 1), DifferentialFormSpace.d VF_B β = ωB
Instances
Donaldson's theorem on Lefschetz pencils.
For any compact symplectic 4-manifold $(M^4, \omega)$, after blowing up finitely many points the resulting manifold $\hat M$ admits a Lefschetz fibration to $S^2$.
Data for forming the symplectic sum (a.k.a. fiber sum) of two compact symplectic manifolds $M_1, M_2$ along a common codimension-2 symplectic submanifold $Q$: inclusions $\iota_j : Q \hookrightarrow M_j$ pulling $\omega_{M_j}$ back to $\omega_Q$, with the codimension and a triviality witness for the normal bundle (a closed 2-form on each $M_j$ restricting to zero on $Q$ and itself non-zero).
- M₁ : SymplecticManifold Ω₁ VF₁
- M₂ : SymplecticManifold Ω₂ VF₂
- Q : SymplecticManifold Ω_Q VF_Q
- ι₁ : DFSMorphism Ω_Q VF_Q Ω₁ VF₁
- ι₂ : DFSMorphism Ω_Q VF_Q Ω₂ VF₂
Instances For
Symplectic sum (existence).
Given two symplectic manifolds $(M_1, \omega_1)$, $(M_2, \omega_2)$ and a common codimension-2 symplectic submanifold $Q$ with inclusions pulling back the ambient symplectic forms to $\omega_Q$, there exists a new symplectic manifold $R$ with embeddings $j_k : M_k \hookrightarrow R$ such that $j_k^*\omega_R = \omega_k$. Moreover $R$ admits a closed 2-form $\eta$ that is exact on each $M_k$ but not on $R$, witnessing a new cohomology class created by the sum.
A group $G$ is finitely presented: there exist $n, m \in \mathbb{N}$, a surjection $f: F_n \twoheadrightarrow G$ from the free group on $n$ generators, and $m$ relator words generating $\ker f$ as a normal subgroup.
Instances
The group $G$ is the fundamental group $\pi_1$ of the compact symplectic 4-manifold $S$: $S$ is finitely presented, admits a compatible almost complex structure, and there is a group isomorphism $\pi_1(S) \cong G$.
- fp : IsFinitelyPresented G
- has_acs : ∃ (J : AlmostComplexStr), IsCompatibleACS S J
- π₁ : Type u_4
Instances
Gompf's realization theorem for fundamental groups.
Every finitely presented group $G$ arises as the fundamental group $\pi_1(S)$ of some compact symplectic 4-manifold $S$.
A schematic handlebody decomposition of a closed 4-manifold: existence of $n_k$ $k$-handles for $k = 0, \dots, 4$ with the standard normalization (a single 0-handle and a single 4-handle, plus at least one 2-handle).
Instances For
Carrier for an Euler characteristic value $\chi \in \mathbb{Z}$.
- euler : ℤ
Instances For
A pullback morphism $\varphi$ is $\omega$-tame if the pulled-back form $\varphi^*\omega$ is non-degenerate on contraction.
- taming_nondeg : Function.Injective fun (v : VF) => DifferentialFormSpace.ι v (φ.pullback S.ω)
Instances
A symplectic branched covering: a symplectic target $(Y, \omega_Y)$, a covering map $f: X \to Y$, and an integer degree $\geq 1$.
- target : SymplecticManifold Ω_Y VF_Y
- f : DFSMorphism Ω_X VF_X Ω_Y VF_Y
- degree : ℕ
Instances For
A linear combination $\eta + \varepsilon\alpha$ of two closed 2-forms is closed: $d(\eta + \varepsilon\alpha) = d\eta + \varepsilon\, d\alpha = 0$.
Data for the perturbation step in symplectifying a branched cover: a closed auxiliary 2-form $\alpha$ and parameter $\varepsilon \neq 0$ together with a tangent splitting whose vertical kernel is annihilated by $\eta$ (the pullback of the base symplectic form), $\alpha$ is non-degenerate on the kernel, and $\eta + \varepsilon\alpha$ is non-degenerate on horizontal vectors.
- projV : VF → VF
- projH : VF → VF
- decompose (X : VF) {p : ℕ} (α : Ω (p + 1)) : DifferentialFormSpace.ι X α = DifferentialFormSpace.ι (projV α X) α + DifferentialFormSpace.ι (projH α X) α
- complement_VH (X : VF) {p : ℕ} (α : Ω (p + 1)) : DifferentialFormSpace.ι (projV α (projH α X)) α = 0
- complement_HV (X : VF) {p : ℕ} (α : Ω (p + 1)) : DifferentialFormSpace.ι (projH α (projV α X)) α = 0
- orthogonal (X Y : VF) : DifferentialFormSpace.ι (projV α Y) (DifferentialFormSpace.ι (projH α X) α) = 0
- alpha_nondeg_on_K (X Y : VF) : DifferentialFormSpace.ι (TangentSplitting.projV α X) α = DifferentialFormSpace.ι (TangentSplitting.projV α Y) α → TangentSplitting.projV α X = TangentSplitting.projV α Y
- complement_nondeg (X Y : VF) : TangentSplitting.projV α X = TangentSplitting.projV α Y → DifferentialFormSpace.ι X (η + ε • α) = DifferentialFormSpace.ι Y (η + ε • α) → X = Y
Instances
Rescaling identity for the contraction pairing: if $\iota_X(\eta + \varepsilon\alpha) = \iota_Y(\eta + \varepsilon\alpha)$, then $\iota_X(\alpha + \varepsilon^{-1}\eta) = \iota_Y(\alpha + \varepsilon^{-1}\eta)$, using $\eta + \varepsilon\alpha = \varepsilon(\alpha + \varepsilon^{-1}\eta)$ and the $\mathbb R$-linearity of $\iota$.
Given a perturbation data instance, there exist a closed $\alpha'$ and parameter $\varepsilon'$ such that $f^*\omega_Y + \varepsilon'\alpha'$ is non-degenerate upstairs. This is the symplectic non-degeneracy step in the branched-cover construction.
A symplectic branched covering equipped with valid perturbation data carries a symplectic form $\omega_X$ on the source: it is closed and non-degenerate.
Data for the adjunction formula for a symplectic surface inside a 4-manifold: the genus $g$, self-intersection $[\Sigma]\cdot[\Sigma]$, the value $\langle c_1, [\Sigma]\rangle$, the first Chern numbers of the tangent and normal bundles, and the relations
- $c_1(T\Sigma) = 2 - 2g$ (Gauss-Bonnet),
- $c_1(N\Sigma) = [\Sigma]\cdot[\Sigma]$ (normal-bundle degree),
- $\langle c_1, [\Sigma]\rangle = c_1(T\Sigma) + c_1(N\Sigma)$ (splitting of $c_1(TM)|_\Sigma$).
Instances For
Adjunction genus bound (axiomatic). For a symplectic surface with adjunction data, either $2g - 2 + [\Sigma]\cdot[\Sigma] \geq 0$, or the surface is a $(-1)$-sphere ($g = 0$, $[\Sigma]\cdot[\Sigma] = -1$).
Gauss-Bonnet: $c_1(T\Sigma) = 2 - 2g$.
Normal-bundle degree: $c_1(N\Sigma) = [\Sigma]\cdot[\Sigma]$.
Chern-class splitting: $\langle c_1, [\Sigma]\rangle = c_1(T\Sigma) + c_1(N\Sigma)$.
The genus formula deduced from the data: $\langle c_1, [\Sigma]\rangle = 2 - 2g + [\Sigma]\cdot[\Sigma]$.
Adjunction formula. For a symplectic surface $\Sigma \subset M$ with adjunction data, $\langle c_1, [\Sigma]\rangle = 2 - 2g + [\Sigma]\cdot[\Sigma]$.
Genus lower bound for a square-zero symplectic surface.
If $[\Sigma]\cdot[\Sigma] = 0$ and the adjunction inequality $2g - 2 \geq [\Sigma]\cdot[\Sigma]$ holds when $[\Sigma]\cdot[\Sigma] \geq 0$, then $g \geq 1$.
Data for the ramification locus $R \subset X$ of a symplectic branched cover $f: X \to Y$ and its image $D \subset Y$ (the branch divisor): inclusions $R \hookrightarrow X$ and $D \hookrightarrow Y$, the restricted map $f|_R: R \to D$, the property that $f^*\omega_Y$ degenerates along $R$, and the factorization $f \circ \mathrm{incl}_R = \mathrm{incl}_D \circ (f|_R)$.
- VF_R : Type u_6
- inst_R : DifferentialFormSpace self.Ω_R self.VF_R
- VF_D : Type u_8
- inst_D : DifferentialFormSpace self.Ω_D self.VF_D
- inclR : DFSMorphism self.Ω_R self.VF_R Ω_X VF_X
- inclD : DFSMorphism self.Ω_D self.VF_D Ω_Y VF_Y
- fRestrict : DFSMorphism self.Ω_R self.VF_R self.Ω_D self.VF_D
- pullback_degenerate_on_R : ¬Function.Injective fun (v : self.VF_R) => DifferentialFormSpace.ι v (self.inclR.pullback (bc.f.pullback bc.target.ω))
Instances For
A symplectic form on a manifold $M$ in the manifold-with-corners formalism: half the dimension, a skew-symmetric non-degenerate bilinear form on the model space $E$.
- halfDim : ℕ
- nondegenerate : Function.Injective ⇑self.form
Instances For
Symplectic fiber-sum data in the manifold-with-corners formalism: two symplectic manifolds $M_1, M_2$ with a common codimension-2 submanifold $Q$, smooth injective embeddings $\iota_j: Q \hookrightarrow M_j$, matching dimensions, and chosen trivializations of the normal $\mathbb R^2$-bundles of $Q$ in $M_1$ and $M_2$ along the zero section.
- ι₁ : Q → M₁
- ι₂ : Q → M₂
- ι₁_injective : Function.Injective self.ι₁
- ι₂_injective : Function.Injective self.ι₂
- ι₁_smooth : MDiff self.ι₁
- ι₂_smooth : MDiff self.ι₂
- symp₁ : ManifoldSymplecticForm I M₁
- symp₂ : ManifoldSymplecticForm I M₂
- sympQ : ManifoldSymplecticForm I Q
Instances For
Symplectic sum existence (manifold formulation).
Given symplectic fiber-sum data $(M_1, M_2, Q)$ in the manifold-with-corners formalism, there exists a smooth manifold $R$ carrying a symplectic form whose half-dimension matches that of $M_1$.
Lefschetz pencil data in the manifold-with-corners formalism: a smooth map $f: M^4 \to B^2$ between manifolds, finitely many isolated critical points where the derivative vanishes, and surjective derivative (i.e. submersion) at non-critical points; together with the existence of a generic regular value $b$ such that $f^{-1}(b)$ is non-empty and avoids the critical set.
- f : M → B₂
- numCriticalPoints : ℕ
- criticalPoints : Fin self.numCriticalPoints → M
- smooth_away (x : M) : (∀ (i : Fin self.numCriticalPoints), x ≠ self.criticalPoints i) → MDiffAt self.f x
- hessian_nondegenerate (x : M) : (∀ (i : Fin self.numCriticalPoints), x ≠ self.criticalPoints i) → Function.Surjective ⇑(mfderiv% self.f x)