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

A blow-up of a smooth $4$-manifold $M$ at finitely many points, producing a new manifold $\hat M$ together with a smooth blow-down map $\pi : \hat M \to M$. The structure records the points blown up and the existence of local complex blow-up models around each exceptional set, where the blow-down fails to be a submersion.

• blowdown : Mhat → M
• blowdown_smooth : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ self.blowdown
• numBlowups : ℕ
• numBlowups_pos : 0 < self.numBlowups
• blownUpPoints : Fin self.numBlowups → M
• hasLocalBlowupModel (j : Fin self.numBlowups) : ∃ (U : Set M) (_ : IsOpen U) (_ : self.blownUpPoints j ∈ U) (Uhat : Set Mhat) (_ : IsOpen Uhat) (φ : M → ℂ × ℂ) (_φhat : Mhat → ℂ × ℂ), (∀ x ∈ Uhat, φ (self.blowdown x) = (0, 0) → ¬Function.Surjective ⇑(mfderiv% self.blowdown x)) ∧ φ (self.blownUpPoints j) = (0, 0)

structure AdmitsLefschetzFibrationToS2 (Mhat : Type u_1) [TopologicalSpace Mhat] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) Mhat] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ Mhat] : Type (max u_1 (u_2 + 1))

The data witnessing that a $4$-manifold $\hat M$ admits a Lefschetz fibration to a compact $2$-manifold $B$ (the base, which is $S^2$ for Donaldson's theorem), together with a closed nondegenerate area form on the base.

• B : Type u_2
• topoB : TopologicalSpace self.B
• chartedB : ChartedSpace (EuclideanSpace ℝ (Fin 2)) self.B
• manifoldB : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 2))) ⊤ self.B
• compactB : CompactSpace self.B
• lf : LefschetzFibrationMathlib Mhat self.B
• baseAreaForm : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) [⋀^Fin 2]→L[ℝ] ℝ
• baseForm_closed (x : EuclideanSpace ℝ (Fin 2)) : extDeriv self.baseAreaForm x = 0
• baseForm_nondegenerate (x : EuclideanSpace ℝ (Fin 2)) : self.baseAreaForm x ≠ 0

theorem donaldson_theorem3_axiom (M : Type u_1) [NormedAddCommGroup M] [NormedSpace ℝ M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ M] [CompactSpace M] (sympl : SymplecticGeometry.SymplecticManifold 2 M) : ∃ (Mhat : Type u_2) (x : TopologicalSpace Mhat) (x_1 : ChartedSpace (EuclideanSpace ℝ (Fin 4)) Mhat) (x_2 : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ Mhat) (_ : CompactSpace Mhat), Nonempty (BlowupMathlib M Mhat) ∧ Nonempty (AdmitsLefschetzFibrationToS2 Mhat)

Donaldson's Theorem 3 (axiomatic form). Every compact symplectic $4$-manifold $(M, \omega)$ admits a blow-up $\hat M$ at finitely many points such that $\hat M$ carries a Lefschetz fibration over $S^2$.

theorem donaldson_theorem3_lefschetz_fibration (M : Type u_1) [NormedAddCommGroup M] [NormedSpace ℝ M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ M] [CompactSpace M] (sympl : SymplecticGeometry.SymplecticManifold 2 M) : ∃ (Mhat : Type u_2) (x : TopologicalSpace Mhat) (x_1 : ChartedSpace (EuclideanSpace ℝ (Fin 4)) Mhat) (x_2 : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) ⊤ Mhat) (_ : CompactSpace Mhat), Nonempty (BlowupMathlib M Mhat) ∧ Nonempty (AdmitsLefschetzFibrationToS2 Mhat)

Donaldson's Theorem 3. A compact symplectic $4$-manifold $(M, \omega)$ becomes, after blowing up finitely many points, the total space of a Lefschetz fibration over $S^2$.