GAGA (Theorem 13.10)
DisprovedCondC.gagaTheorem 13.10 of the paper: the fully faithful functor from the perfect complexes of an algebraic variety to the perfect complexes of its analytification is an equivalence of infinity-categories. The milestone splits the equivalence into its two visible halves over the coherent world interface: essential surjectivity - every coherent coefficient on the analytic side is the image of a coherent coefficient of the algebraic side - and the cohomology comparison - for every coherent coefficient, the cohomology groups of the algebraic and the analytic sides are isomorphic, compatibly with the bundled operations.
Formalization Note The analytification functor enters as an abstract action on coefficients respecting coherence; the derived equivalence of perfect complexes of the paper is the proposed work of the milestone.
import Mathlib import Definitions.Def_CondC_liq import Definitions.Def_CondC_geo
namespace CondC
/-! Milestone 7: GAGA (Theorem 13.10). An analytification functor between
the coherent worlds of an algebraic variety and its analytification is
essentially surjective on coherent coefficients, and for every coherent
coefficient the cohomology groups are isomorphic, compatibly with the
bundled operations. This is the equivalence of Theorem 13.10, split into
essential surjectivity and the cohomology comparison. -/
theorem gaga : ∀ (wX wAn : CompactCxWorld) (anF : Type → Type),
(∀ F : Type, wX.coherent F → wAn.coherent (anF F)) →
(∀ E : Type, wAn.coherent E → ∃ F : Type, wX.coherent F ∧ Nonempty (anF F ≃ E)) ∧
(∀ (F : Type) (_hF : wX.coherent F) (i : ℕ),
∃ e : wX.Coh F i ≃ wAn.Coh (anF F) i,
(∀ x y : wX.Coh F i, e (wX.add F i x y) = wAn.add (anF F) i (e x) (e y)) ∧
(∀ (k : ℂ) (x : wX.Coh F i), e (wX.smul F i k x) = wAn.smul (anF F) i k (e x)) ∧
e (wX.zero F i) = wAn.zero (anF F) i) := by sorry
end CondC
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for any two compact complex worlds and any coefficient functor between them that respects coherence wherever it is defined on the coherent coefficients of the source, the functor is essentially surjective: every coherent coefficient of the target is equivalent to the image of a coherent coefficient of the source; and the cohomology compares: for every coherent coefficient of the source and every degree, the cohomology group of the source identifies with the cohomology group of the image coefficient, compatibly with the bundled addition, zero, and scalar multiplication. No other hypotheses appear.