The sheaf of holomorphic functions (Theorems 1.1 and 5.1)
DisprovedCondC.sheaf_existsTheorem 1.1 of the introduction, proved as Theorem 5.1: there is a necessarily unique sheaf O on the complex plane such that on each open disc D(x, r) the sections identify with the power series in (T - x) whose coefficients satisfy the decay condition, with transition maps compatible with evaluation at points; and the higher sheaf cohomology of each disc vanishes. The milestone states existence and uniqueness: there is a disc presheaf carrying the power-series identification and satisfying the two-disc sheaf condition; and any two such are uniquely isomorphic, by an isomorphism compatible with the restriction maps and with the power-series identifications.
Formalization Note The sheaf condition is stated in the two-disc form that the paper's proof uses: sections agreeing on every disc contained in the overlap of a two-disc cover glue uniquely. The uniqueness of the sheaf is stated up to restriction-compatible, identification-compatible isomorphism. The acyclicity half is the next milestone.
import Mathlib import Definitions.Def_CondC_liq import Definitions.Def_CondC_geo
namespace CondC
/-! Milestone 3: the sheaf of holomorphic functions. There is a disc
presheaf carrying the power-series identification of Theorem 5.1 and
satisfying the two-disc sheaf condition; and any two such are uniquely
isomorphic, by an isomorphism compatible with restriction and with the
power-series identifications. This is the existence and uniqueness of the
structure sheaf O (Theorems 1.1 and 5.1). -/
theorem sheaf_exists : ∃ (P : DiscModulePresheaf) (O : OIdentification P),
SheafGlue2 P ∧
∀ (Q : DiscModulePresheaf) (O' : OIdentification Q), SheafGlue2 Q →
∃! e : (d : Disc) → P.F d ≃ Q.F d,
(∀ (d d' : Disc) (h : SubDisc d d') (s : P.F d'),
Q.res d d' h (e d' s) = e d (P.res d d' h s)) ∧
(∀ (d : Disc) (s : P.F d), O.coeffs d s = O'.coeffs d (e d s)) := by sorry
end CondC
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: there is a disc presheaf and a power-series identification of it satisfying the decay condition of the structure sheaf theorem, such that the presheaf satisfies the two-disc sheaf condition; and for any second disc presheaf with such an identification also satisfying the sheaf condition, there is a unique family of bijections between the fibres over all discs that commutes with the restriction maps of both presheaves and carries power-series expansions to power-series expansions. No hypotheses appear.