noncomputable def lefschetzLocalModel : ℂ × ℂ → ℂ

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

structure LefschetzFibrationMathlib (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ M] (B : Type u_2) [TopologicalSpace B] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) B] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 2))) ⊤ B] : Type (max u_1 u_2)

A Lefschetz fibration $f : M^4 \to B^2$: a smooth map with finitely many critical points, each modeled holomorphically by $(z_1, z_2) \mapsto z_1^2 + z_2^2$.

• f : M → B
• smooth_f : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 2))) ⊤ self.f
• criticalPoints : Finset M
• isCritical (x : M) : x ∈ self.criticalPoints ↔ ¬Function.Surjective ⇑(mfderiv% self.f x)
• hasLocalQuadraticModel (p : M) : p ∈ self.criticalPoints → ∃ (U : Set M) (_ : IsOpen U) (_ : p ∈ U) (φ : M → ℂ × ℂ) (ψ : B → ℂ), (∀ x ∈ U, ψ (self.f x) = lefschetzLocalModel (φ x)) ∧ φ p = (0, 0) ∧ ψ (self.f p) = 0

structure FiberClassNonzeroMathlib {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ M] {B : Type u_2} [TopologicalSpace B] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) B] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 2))) ⊤ B] (lf : LefschetzFibrationMathlib M B) : Type (max u_1 (u_3 + 1))

Witness data showing that the regular fiber $F \hookrightarrow M$ of a Lefschetz fibration represents a nonzero class in $H^2(M;\mathbb{R})$, via a closed witness $2$-form.

• F : Type u_3
• topoF : TopologicalSpace self.F
• chartedF : ChartedSpace (EuclideanSpace ℝ (Fin 2)) self.F
• manifoldF : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 2))) ⊤ self.F
• fiberInclusion : self.F → M
• smooth_inclusion : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 2))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ self.fiberInclusion
• witnessForm : EuclideanSpace ℝ (Fin 4) → EuclideanSpace ℝ (Fin 4) [⋀^Fin 2]→L[ℝ] ℝ
• witness_closed (x : EuclideanSpace ℝ (Fin 4)) : extDeriv self.witnessForm x = 0
• fiber_class_nonzero : ∃ (y : self.F), self.witnessForm (↑(chartAt (EuclideanSpace ℝ (Fin 4)) (self.fiberInclusion y)) (self.fiberInclusion y)) ≠ 0