def IsSymplecticFibration {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_B : ℕ → Type u_3} {VF_B : Type u_4} {Ω_F : ℕ → Type u_5} {VF_F : Type u_6} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_B : DifferentialFormSpace Ω_B VF_B] [inst_F : DifferentialFormSpace Ω_F VF_F] (f : DFSMorphism Ω_M VF_M Ω_B VF_B) (fiberInclusion : DFSMorphism Ω_F VF_F Ω_M VF_M) (fiberSymplectic : SymplecticManifold Ω_F VF_F) : Prop

Definition 1: a map $f : M \to B$ is a symplectic fibration with fiber $(F, \omega_F)$ if there exists a SymplecticFibration structure realizing $f$, the fiber inclusion, and the fiber symplectic form (so the structure group reduces to $\mathrm{Symp}(F, \omega_F)$).

def IsLefschetzFibration {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_B2 : ℕ → Type u_3} {VF_B2 : Type u_4} {Ω_F : ℕ → Type u_5} {VF_F : Type u_6} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_B2 : DifferentialFormSpace Ω_B2 VF_B2] [inst_F : DifferentialFormSpace Ω_F VF_F] [IsOriented Ω_M VF_M] [IsOriented Ω_B2 VF_B2] (f : DFSMorphism Ω_M VF_M Ω_B2 VF_B2) (genericFiberInclusion : DFSMorphism Ω_F VF_F Ω_M VF_M) : Prop

A map $f : M \to B^2$ is a Lefschetz fibration (with generic fiber inclusion) if it is realized by some LefschetzFibration structure.

theorem gompf_lefschetz_symplectic {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_B2 : ℕ → Type u_3} {VF_B2 : Type u_4} {Ω_F : ℕ → Type u_5} {VF_F : Type u_6} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_B2 : DifferentialFormSpace Ω_B2 VF_B2] [inst_F : DifferentialFormSpace Ω_F VF_F] [IsOriented Ω_M VF_M] [IsOriented Ω_B2 VF_B2] (lf : LefschetzFibration) (hF : FiberClassNonzero lf) : ∃ (S_M : SymplecticManifold Ω_M VF_M) (S_F : SymplecticManifold Ω_F VF_F), S_F.ω = lf.genericFiberInclusion.pullback S_M.ω ∧ IsSymplecticSubmanifold S_M lf.genericFiberInclusion

Gompf's construction: if the generic fiber class is nonzero, a Lefschetz fibration carries a symplectic structure on the total space whose restriction to the fiber agrees with $\omega_F$, making the fiber a symplectic submanifold.

theorem IsLefschetzFibration.toLefschetzFibration {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_B2 : ℕ → Type u_3} {VF_B2 : Type u_4} {Ω_F : ℕ → Type u_5} {VF_F : Type u_6} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_B2 : DifferentialFormSpace Ω_B2 VF_B2] [inst_F : DifferentialFormSpace Ω_F VF_F] [IsOriented Ω_M VF_M] [IsOriented Ω_B2 VF_B2] {f : DFSMorphism Ω_M VF_M Ω_B2 VF_B2} {fiberIncl : DFSMorphism Ω_F VF_F Ω_M VF_M} (hfib : IsLefschetzFibration f fiberIncl) : ∃ (lf : LefschetzFibration), lf.f = f ∧ lf.genericFiberInclusion = fiberIncl

Extract the underlying LefschetzFibration structure from IsLefschetzFibration data.

theorem IsSymplecticFibration.toSymplecticFibration {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_B : ℕ → Type u_3} {VF_B : Type u_4} {Ω_F : ℕ → Type u_5} {VF_F : Type u_6} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_B : DifferentialFormSpace Ω_B VF_B] [inst_F : DifferentialFormSpace Ω_F VF_F] {f : DFSMorphism Ω_M VF_M Ω_B VF_B} {fiberIncl : DFSMorphism Ω_F VF_F Ω_M VF_M} {fiberSymp : SymplecticManifold Ω_F VF_F} (hfib : IsSymplecticFibration f fiberIncl fiberSymp) : ∃ (fib : SymplecticFibration), fib.f = f ∧ fib.fiberInclusion = fiberIncl ∧ fib.fiberSymplectic = fiberSymp

Extract the underlying SymplecticFibration structure from IsSymplecticFibration data.

theorem SymplecticFibration.transition_self_eq {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_B : ℕ → Type u_3} {VF_B : Type u_4} {Ω_F : ℕ → Type u_5} {VF_F : Type u_6} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_B : DifferentialFormSpace Ω_B VF_B] [inst_F : DifferentialFormSpace Ω_F VF_F] (fib : SymplecticFibration) (i : fib.CoverIdx) {p : ℕ} (α : Ω_F p) : (fib.transitionMap i i).pullback α = α

A self-transition $g_{ii}$ acts as the identity on forms: $(g_{ii})^* \alpha = \alpha$, deduced from the cocycle and inverse axioms.

structure SymplecticFibration.LocalTrivializationData {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_B : ℕ → Type u_3} {VF_B : Type u_4} {Ω_F : ℕ → Type u_5} {VF_F : Type u_6} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_B : DifferentialFormSpace Ω_B VF_B] [inst_F : DifferentialFormSpace Ω_F VF_F] (fib : SymplecticFibration) : Type (max u_1 u_5)

Data for local trivializations of a symplectic fibration: local fiber projections $p_i : M \supset U_i \to F$ that are compatible with transition functions, plus primitives $\beta_i$ realizing $p_i^*\omega_F - \eta = d\beta_i$ for a global $2$-form $\eta$ (used in Thurston's construction).

• localProj : fib.CoverIdx → DFSMorphism Ω_M VF_M Ω_F VF_F
• proj_transition_compat (i j : fib.CoverIdx) {p : ℕ} (α : Ω_F p) : (self.localProj i).pullback ((fib.transitionMap i j).pullback α) = (self.localProj j).pullback α
• localPrimitive : fib.CoverIdx → Ω_M 1
• proj_pullback_eq (i : fib.CoverIdx) (η : Ω_M 2) : (self.localProj i).pullback fib.fiberSymplectic.ω = η + DifferentialFormSpace.d VF_M (self.localPrimitive i)

theorem SymplecticFibration.LocalTrivializationData.patching_restricts_to_fiber {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_B : ℕ → Type u_3} {VF_B : Type u_4} {Ω_F : ℕ → Type u_5} {VF_F : Type u_6} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_B : DifferentialFormSpace Ω_B VF_B] [inst_F : DifferentialFormSpace Ω_F VF_F] {fib : SymplecticFibration} (triv : fib.LocalTrivializationData) (i j : fib.CoverIdx) (r₁ r₂ : ℝ) (hsum : r₁ + r₂ = 1) (h_η_restricts_via_i : fib.fiberInclusion.pullback ((triv.localProj i).pullback fib.fiberSymplectic.ω) = fib.fiberSymplectic.ω) (h_η_restricts_via_j : fib.fiberInclusion.pullback ((triv.localProj j).pullback fib.fiberSymplectic.ω) = fib.fiberSymplectic.ω) : fib.fiberInclusion.pullback (r₁ • (triv.localProj i).pullback fib.fiberSymplectic.ω + r₂ • (triv.localProj j).pullback fib.fiberSymplectic.ω) = fib.fiberSymplectic.ω

A convex combination $r_1 p_i^*\omega_F + r_2 p_j^*\omega_F$ (with $r_1 + r_2 = 1$) restricts to $\omega_F$ on the fiber, provided each summand does — a key step in Thurston's patching argument.