Acyclicity on discs: the vanishing of the first cohomology (Theorem 1.1)
DisprovedCondC.sheaf_acyclicThe acyclicity half of Theorem 1.1: for any disc D, the sheaf cohomology groups H^i(D, O) vanish for i > 0. The paper proves this by induction over covers by two discs, using the sheaf condition established on the way. The milestone states the two-disc-cover form of the vanishing: a disc presheaf carrying the power-series identification and satisfying the two-disc sheaf condition has vanishing first cohomology on every two-disc cover - a pair of sections whose difference vanishes on every disc contained in the overlap of the cover is the pair of restrictions of a global section.
Formalization Note Only the first cohomology degree and only two-disc covers are formalized, in the form in which the paper's induction uses them; the propagation to all positive degrees and general covers is carried in prose as proposed work.
import Mathlib import Definitions.Def_CondC_liq import Definitions.Def_CondC_geo
namespace CondC
/-! Milestone 4: the acyclicity of the structure sheaf on discs. A disc
presheaf carrying the power-series identification and satisfying the
two-disc sheaf condition has vanishing first cohomology in the two-cover
form. This is the acyclicity half of Theorem 1.1 - H^i(D, O) = 0 for i > 0 -
in the two-disc cover form in which the paper proves it. -/
theorem sheaf_acyclic : ∀ (P : DiscModulePresheaf) (_ : OIdentification P),
SheafGlue2 P → H1Vanishes P := by sorry
end CondC
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: every disc presheaf carrying the power-series identification and satisfying the two-disc sheaf condition has vanishing first cohomology in the two-cover sense: any pair of sections on the two elements of a two-disc cover whose restrictions have vanishing difference on every disc contained in both cover elements is the pair of restrictions of a single global section. No other hypotheses appear.