def Gompf.lefschetzLocalModel : ℂ × ℂ → ℂ

Local model for a Lefschetz singularity: the holomorphic map $(z_1, z_2) \mapsto z_1^2 + z_2^2$.

structure Gompf.LefschetzFibration {E_M : Type u_1} [NormedAddCommGroup E_M] [NormedSpace ℝ E_M] [Module.Oriented ℝ E_M (Fin 4)] {H_M : Type u_2} [TopologicalSpace H_M] (I_M : ModelWithCorners ℝ E_M H_M) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H_M M] {E_B : Type u_4} [NormedAddCommGroup E_B] [NormedSpace ℝ E_B] [Module.Oriented ℝ E_B (Fin 2)] {H_B : Type u_5} [TopologicalSpace H_B] (I_B : ModelWithCorners ℝ E_B H_B) (B : Type u_6) [TopologicalSpace B] [ChartedSpace H_B B] {E_F : Type u_7} [NormedAddCommGroup E_F] [NormedSpace ℝ E_F] {H_F : Type u_8} [TopologicalSpace H_F] (I_F : ModelWithCorners ℝ E_F H_F) (F : Type u_9) [TopologicalSpace F] [ChartedSpace H_F F] : Type (max (max u_3 u_6) u_9)

A Lefschetz fibration $f: M^4 \to \Sigma^2$: a smooth map between an oriented 4-manifold and an oriented surface, a submersion away from finitely many isolated critical points, each of which has a local quadratic model $z_1^2 + z_2^2$.

• f : M → B
• f_smooth : ContMDiff I_M I_B ⊤ self.f
• fiberInclusion : F → M
• fiberInclusion_smooth : ContMDiff I_F I_M ⊤ self.fiberInclusion
• fiberInclusion_injective : Function.Injective self.fiberInclusion
• dim_total : Module.finrank ℝ E_M = 4
• dim_base : Module.finrank ℝ E_B = 2
• numCriticalPoints : ℕ
• criticalPoints : Fin self.numCriticalPoints → M
• isCritical (i : Fin self.numCriticalPoints) : ¬Function.Surjective ⇑(mfderiv I_M I_B self.f (self.criticalPoints i))
• isSubmersionAway (x : M) : (∀ (i : Fin self.numCriticalPoints), x ≠ self.criticalPoints i) → Function.Surjective ⇑(mfderiv I_M I_B self.f x)
• criticalPoints_isolated (i : Fin self.numCriticalPoints) : ∃ (U : Set M), self.criticalPoints i ∈ U ∧ IsOpen U ∧ ∀ (j : Fin self.numCriticalPoints), self.criticalPoints j ∈ U → j = i
• hasLocalQuadraticModel (i : Fin self.numCriticalPoints) : ∃ (U : Set M) (_ : IsOpen U) (_ : self.criticalPoints i ∈ U) (φ : M → ℂ × ℂ) (ψ : B → ℂ), (∀ x ∈ U, ψ (self.f x) = lefschetzLocalModel (φ x)) ∧ φ (self.criticalPoints i) = (0, 0) ∧ ψ (self.f (self.criticalPoints i)) = 0

structure Gompf.FiberClassNonzero {E_M : Type u_1} [NormedAddCommGroup E_M] [NormedSpace ℝ E_M] [Module.Oriented ℝ E_M (Fin 4)] {H_M : Type u_2} [TopologicalSpace H_M] {I_M : ModelWithCorners ℝ E_M H_M} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H_M M] {E_B : Type u_4} [NormedAddCommGroup E_B] [NormedSpace ℝ E_B] [Module.Oriented ℝ E_B (Fin 2)] {H_B : Type u_5} [TopologicalSpace H_B] {I_B : ModelWithCorners ℝ E_B H_B} {B : Type u_6} [TopologicalSpace B] [ChartedSpace H_B B] {E_F : Type u_7} [NormedAddCommGroup E_F] [NormedSpace ℝ E_F] {H_F : Type u_8} [TopologicalSpace H_F] {I_F : ModelWithCorners ℝ E_F H_F} {F : Type u_9} [TopologicalSpace F] [ChartedSpace H_F F] (lf : LefschetzFibration I_M M I_B B I_F F) : Type u_1

Hypothesis that the fiber class is nonzero in cohomology: there exists a closed 2-form on $M$ (a witness for $[F]$) that evaluates non-trivially on the fiber.

• witnessForm : E_M → E_M [⋀^Fin 2]→L[ℝ] ℝ
• witness_closed (x : E_M) : extDeriv self.witnessForm x = 0
• fiber_class_nonzero : ∃ (y : F), self.witnessForm (↑I_M (↑(chartAt H_M (lf.fiberInclusion y)) (lf.fiberInclusion y))) ≠ 0

structure Gompf.SymplecticStructure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] : Type (max u_1 u_3)

A symplectic structure on a manifold $M$: a smooth, skew-symmetric, non-degenerate 2-form $\omega$ which is also closed ($d\omega = 0$).

• omega : M → E →L[ℝ] E →L[ℝ] ℝ
• skew (x : M) (v w : E) : ((self.omega x) v) w = -((self.omega x) w) v
• nondegenerate (x : M) (v : E) : (∀ (w : E), ((self.omega x) v) w = 0) → v = 0
• smooth : ContMDiff I (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ)) ⊤ self.omega
• omega_form : E → E [⋀^Fin 2]→L[ℝ] ℝ
• is_closed (x : E) : extDeriv self.omega_form x = 0

structure Gompf.FibersAreSymplectic {E_M : Type u_1} [NormedAddCommGroup E_M] [NormedSpace ℝ E_M] {H_M : Type u_2} [TopologicalSpace H_M] {I_M : ModelWithCorners ℝ E_M H_M} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H_M M] {E_F : Type u_4} [NormedAddCommGroup E_F] [NormedSpace ℝ E_F] {H_F : Type u_5} [TopologicalSpace H_F] {I_F : ModelWithCorners ℝ E_F H_F} {F : Type u_6} [TopologicalSpace F] [ChartedSpace H_F F] (omega_M : SymplecticStructure I_M M) (omega_F : SymplecticStructure I_F F) (fiberInclusion : F → M) : Prop

Compatibility condition stating that the fibers of the inclusion $F \hookrightarrow M$ are symplectic submanifolds: $\omega_F = (\iota)^* \omega_M$.

• is_pullback (p : F) (v w : E_F) : ((omega_F.omega p) v) w = ((omega_M.omega (fiberInclusion p)) ((mfderiv I_F I_M fiberInclusion p) v)) ((mfderiv I_F I_M fiberInclusion p) w)

theorem Gompf.gompf_construction {E_M : Type u_1} [NormedAddCommGroup E_M] [NormedSpace ℝ E_M] [Module.Oriented ℝ E_M (Fin 4)] {H_M : Type u_2} [TopologicalSpace H_M] {I_M : ModelWithCorners ℝ E_M H_M} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H_M M] {E_B : Type u_4} [NormedAddCommGroup E_B] [NormedSpace ℝ E_B] [Module.Oriented ℝ E_B (Fin 2)] {H_B : Type u_5} [TopologicalSpace H_B] {I_B : ModelWithCorners ℝ E_B H_B} {B : Type u_6} [TopologicalSpace B] [ChartedSpace H_B B] {E_F : Type u_7} [NormedAddCommGroup E_F] [NormedSpace ℝ E_F] {H_F : Type u_8} [TopologicalSpace H_F] {I_F : ModelWithCorners ℝ E_F H_F} {F : Type u_9} [TopologicalSpace F] [ChartedSpace H_F F] (lf : LefschetzFibration I_M M I_B B I_F F) (hF : FiberClassNonzero lf) : ∃ (S_M : SymplecticStructure I_M M) (S_F : SymplecticStructure I_F F), FibersAreSymplectic S_M S_F lf.fiberInclusion

Gompf's construction: if $f: M^4 \to \Sigma^2$ is a Lefschetz fibration with fiber class $[F] \neq 0$, then $M$ admits a symplectic structure for which the fibers are symplectic.