Stability of the finite Čech coefficients

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Blowup.TwoChartCurveData7 8/-!9# Stability of the finite Čech coefficients10 11For a regular parameter pair `(t, x)` of `R`, the finite Čech complexes of the two-chart cover12of the blow-up compute, level by level, the cokernel of the twisted Čech differential. This file13shows that the reduction maps between consecutive cokernels are bijective once the level exceeds14the twist `d`, computes the length of the level-`n` cokernel as `∑_{j < n} (d - j - 1)`, and hence15identifies it with `chooseTwo d` in the stable range. As an application, threads of the curve16order limit that are approximable at one stable level lie in the image of the surface.17 18## Main results19 20* `SurfaceBlowup.actual_twisted_coker_reduction_bijective`: for `d ≤ j + 1` the reduction map21  between the cokernels at levels `j + 1` and `j` is bijective.22* `SurfaceBlowup.actual_finite_cech_coefficient_length`: the length of the level-`n` cokernel.23* `SurfaceBlowup.actual_finite_cech_coefficient_triangular`: in the stable range `d - 1 ≤ n`24  this length is `chooseTwo d`.25* `SurfaceBlowup.curve_limit_range_of_stable_level`: a thread approximable by a surface function at26  a stable level is in the range of any section of the surface-to-curve map.27 28Provenance: `Thm_SurfaceBlowupV2_{actual_twisted_coker_reduction_bijective,29actual_finite_cech_coefficient_length, actual_finite_cech_coefficient_triangular,30curve_limit_range_of_stable_level}`.31-/32 33namespace SurfaceBlowup34 35/-! ### The cokernel tower -/36 37/-- In the stable range `d ≤ j + 1`, the map induced by reduction between the cokernels of the38twisted finite Čech differentials at levels `j + 1` and `j` is a bijection. -/39theorem actual_twisted_coker_reduction_bijective (R : Type) [CommRing R] (t x : R)Lemma 4.1Appendix A40    (hreg : RegularParameterPair R t x) (beta : BlowupRestriction R t x) (d j : ℕ) (hd : d ≤ j + 1)41    (hnext : cechInputLattice R t x (j + 1) ≤42      (cechOutputLattice R t x (j + 1)).comap (fullCechDifferential R t x beta d))43    (hnow : cechInputLattice R t x j ≤44      (cechOutputLattice R t x j).comap (fullCechDifferential R t x beta d))45    (hcomm : (cechOutputReduction R t x j).comp46        (finiteCechDifferential R t x beta d (j + 1) hnext) =47      (finiteCechDifferential R t x beta d j hnow).comp (cechInputReduction R t x j)) :48    Function.Bijective (twoTermCokerMap (finiteCechDifferential R t x beta d (j+1) hnext)49      (finiteCechDifferential R t x beta d j hnow) (cechInputReduction R t x j)50      (cechOutputReduction R t x j) hcomm) := by51  refine ⟨?_, two_term_coker_map_surjective R _ _ _ _ _ _ _ _ hcomm52    (actual_cech_reductions_surjective R t x j).2⟩53  rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff]54  intro q hq55  obtain ⟨wbar, rfl⟩ := Submodule.Quotient.mk_surjective _ q56  obtain ⟨w, rfl⟩ := Submodule.Quotient.mk_surjective _ wbar57  obtain ⟨abar, ha⟩ := (Submodule.Quotient.mk_eq_zero _).1 hq58  obtain ⟨a, rfl⟩ := Submodule.Quotient.mk_surjective _ abar59  replace ha := (Submodule.Quotient.eq _).1 ha60  have hbase : ∀ r : R, (beta.right : BlowupChart R x t →+* BlowupOverlap R t x) (chartBase R x t r)61      = (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x r) := fun r =>62    (beta.right.commutes r).trans (IsScalarTower.algebraMap_apply R _ _ r)63  obtain ⟨a', b', -, -, hc⟩ := two_chart_layer_correction R t x hreg64    (beta.right : BlowupChart R x t →+* BlowupOverlap R t x) hbase beta.slope j d hd65    (w - fullCechDifferential R t x beta d a) (by simpa [cechOutputLattice] using neg_mem ha)66  refine (Submodule.Quotient.mk_eq_zero _).267    ⟨Submodule.Quotient.mk (a + (a', b')), (Submodule.Quotient.eq _).2 ?_⟩68  have : fullCechDifferential R t x beta d (a + (a', b')) - w =69      -(w - fullCechDifferential R t x beta d a - ((algebraMap (BlowupChart R t x)70        (BlowupOverlap R t x)) a' - (IsLocalization.Away.invSelf (chartSlope R t x))^d *71          beta.right b')) := by72    rw [map_add]73    change _ + ((IsScalarTower.toAlgHom R (BlowupChart R t x) (BlowupOverlap R t x)) a' - _ *74      beta.right b') - w = _75    simp only [IsScalarTower.coe_toAlgHom']76    ring77  rw [this]78  exact neg_mem hc79 80/-- The length of the cokernel of the twisted finite Čech differential at level `n` is81`∑_{j < n} (d - j - 1)`. -/82theorem actual_finite_cech_coefficient_length (O R : Type) [CommRing O] [CommRing R] [Algebra O R]Lemma 4.283    (t x : R) (hreg : RegularParameterPair R t x) (beta : BlowupRestriction R t x)84    (hregSwap : RegularParameterPair R x t) [(Ideal.span ({t,x} : Set R)).IsMaximal]85    (hres : Function.Surjective (algebraMap O (R ⧸ Ideal.span {t,x}))) (d n : ℕ)86    (hpres : ∀ j : ℕ, cechInputLattice R t x j ≤87      (cechOutputLattice R t x j).comap (fullCechDifferential R t x beta d)) :88    Module.length O89      (CechLevelOutput R t x n ⧸ LinearMap.range (finiteCechDifferential R t x beta d n (hpres n)))90      = ((∑ j ∈ Finset.range n, (d-j-1) : ℕ) : ℕ∞) := by91  induction n with92  | zero =>93    simp only [Finset.range_zero, Finset.sum_empty, Nat.cast_zero]94    apply Module.length_eq_zero_iff.mpr95    have : Subsingleton (CechLevelOutput R t x 0) := by96      constructor97      intro a b98      induction a using Submodule.Quotient.induction_on99      induction b using Submodule.Quotient.induction_on100      rw [Submodule.Quotient.eq]101      simp [cechOutputLattice]102    infer_instance103  | succ j ih =>104    have hcomm := actual_cech_differentials_commute_with_reduction R t x beta d j (hpres (j+1))105      (hpres j)106    have hsurj := two_term_coker_map_surjective R _ _ _ _ _ _ _ _ hcomm107      (actual_cech_reductions_surjective R t x j).2108    rw [Finset.sum_range_succ, Nat.cast_add, ← ih]109    by_cases hj : j < d110    · obtain ⟨i, hi, hex⟩ := actual_negative_layer_coker_exact R t x hreg beta hregSwap d j hj111        (hpres (j+1)) (hpres j) hcomm112      rw [Module.length_eq_add_of_exact (i.restrictScalars O)113        ((twoTermCokerMap _ _ _ _ hcomm).restrictScalars O) hi hsurj hex, add_comm]114      congr 1115      rw [Module.length_eq_of_surjective hres]116      let _ := Ideal.Quotient.field (Ideal.span ({t,x} : Set R))117      exact (Module.length_eq_finrank _ _).trans (by simp)118    · have hbij := actual_twisted_coker_reduction_bijective R t x hreg beta d j (by omega)119        (hpres (j+1)) (hpres j) hcomm120      rw [(LinearEquiv.ofBijective ((twoTermCokerMap _ _ _ _ hcomm).restrictScalars O)121        hbij).length_eq]122      simp [show d - j - 1 = 0 by omega]123 124private theorem sum_range_sub_sub_one_eq_chooseTwo (d n : ℕ) (hn : d - 1 ≤ n) :125    (∑ j ∈ Finset.range n, (d-j-1) : ℕ) = chooseTwo d := by126  have h1 : ∀ m, (∑ j ∈ Finset.range (d-1+m), (d-j-1) : ℕ)127      = ∑ j ∈ Finset.range (d-1), (d-j-1) := by128    intro m129    induction m with130    | zero => rfl131    | succ m ih =>132      rw [← add_assoc, Finset.sum_range_succ, ih]133      omega134  obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le hn135  rw [h1]136  have h2 : (∑ j ∈ Finset.range (d-1), (d-j-1) : ℕ) = ∑ j ∈ Finset.range d, (d-1-j) := by137    rcases d with _ | d138    · rfl139    · rw [Finset.sum_range_succ]140      simp only [Nat.add_sub_cancel]141      rw [show d - d = 0 by omega, add_zero]142      exact Finset.sum_congr rfl fun j _ => by omega143  rw [h2, Finset.sum_range_reflect (fun j => j) d, Finset.sum_range_id]144  rfl145 146/-- In the stable range `d - 1 ≤ n`, the cokernel of the twisted finite Čech differential at147level `n` has length `chooseTwo d`. -/148theorem actual_finite_cech_coefficient_triangular (O R : Type) [CommRing O] [CommRing R]Lemma 4.2149    [Algebra O R] (t x : R) (hreg : RegularParameterPair R t x) (beta : BlowupRestriction R t x)150    (hregSwap : RegularParameterPair R x t) [(Ideal.span ({t,x} : Set R)).IsMaximal]151    (hres : Function.Surjective (algebraMap O (R ⧸ Ideal.span {t,x}))) (d n : ℕ) (hn : d - 1 ≤ n)152    (hpres : ∀ j : ℕ, cechInputLattice R t x j ≤153      (cechOutputLattice R t x j).comap (fullCechDifferential R t x beta d)) :154    Module.length O155      (CechLevelOutput R t x n ⧸ LinearMap.range (finiteCechDifferential R t x beta d n (hpres n)))156      = (chooseTwo d : ℕ∞) := by157  rw [actual_finite_cech_coefficient_length O R t x hreg beta hregSwap hres d n hpres,158    sum_range_sub_sub_one_eq_chooseTwo d n hn]159 160/-! ### Threads of the curve order limit -/161 162section Threads163 164variable {R : Type} [CommRing R] {t x : R} {beta : BlowupRestriction R t x} {d : ℕ}165  (G : GluedGenerators R t x beta d)166 167private theorem curveIdealLattice_le_of_le {j k : ℕ} (hjk : j ≤ k) :168    curveIdealLattice R t x beta G k ≤ curveIdealLattice R t x beta G j := by169  induction k, hjk using Nat.le_induction with170  | base => exact le_rfl171  | succ k _ ih => exact le_trans (curve_lattices_antitone R t x beta d G k).1 ih172 173private theorem thread_sub_succ_mem (p : curveThreads R t x beta G) (j : ℕ) :174    p.val j - p.val (j+1) ∈ curveIdealLattice R t x beta G j := by175  have h := (Submodule.mem_inf.mp p.2).2176  rw [Submodule.mem_comap, Submodule.mem_pi] at h177  exact h j (Set.mem_univ _)178 179private theorem thread_mem_curveSections (p : curveThreads R t x beta G) (j : ℕ) :180    p.val j ∈ curveSections R t x beta G j :=181  Submodule.mem_pi.mp (Submodule.mem_inf.mp p.2).1 j (Set.mem_univ _)182 183private theorem thread_sub_mem (p : curveThreads R t x beta G) {j k : ℕ} (hjk : j ≤ k) :184    p.val j - p.val k ∈ curveIdealLattice R t x beta G j := by185  induction k, hjk using Nat.le_induction with186  | base => simp187  | succ k hk ih =>188    simpa only [sub_add_sub_cancel] using189      add_mem ih (curveIdealLattice_le_of_le G hk (thread_sub_succ_mem G p k))190 191end Threads192 193/-- A curve thread that is approximable by surface functions modulo the curve lattice at one194stable level `J ≥ d - 1` is approximable at every level: going up uses the bijectivity of the195cokernel reduction maps, going down the antitonicity of the curve lattices. -/196private theorem exists_surface_approx_of_stable_level {R : Type} [CommRing R] {t x : R}197    {beta : BlowupRestriction R t x} {d : ℕ} (G : GluedGenerators R t x beta d)198    (hreg : RegularParameterPair R t x) (hregSwap : RegularParameterPair R x t)199    (hregF : ∀ j : ℕ, Function.Injective (fun c : BlowupOverlap R t x ⧸200      (Ideal.span {overlapException R t x})^j =>201      Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j)202      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j)) * c))203    {J : ℕ} (hJ : d - 1 ≤ J) (p : curveThreads R t x beta G)204    (hp : ∃ r : R, p.val J - surfaceToChartPair R t x r ∈ curveIdealLattice R t x beta G J)205    (j : ℕ) : ∃ r : R, p.val j - surfaceToChartPair R t x r ∈ curveIdealLattice R t x beta G j := by206  -- Step 1: `p` is approximable by surface functions at every level `≥ J`.207  have step1 : ∀ n : ℕ, ∃ r : R, p.val (J+n) - surfaceToChartPair R t x r ∈208      curveIdealLattice R t x beta G (J+n) := by209    intro n210    induction n with211    | zero => simpa using hp212    | succ n ih =>213      obtain ⟨r0, hr0⟩ := ih214      rw [← add_assoc]215      generalize hj : J + n = j at hr0 ⊢216      have hsec := thread_mem_curveSections G p (j+1)217      obtain ⟨_, hyy, zz, hzz, hyz⟩ := Submodule.mem_sup.mp hsec218      obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp hyy219      have hc : fullCechDifferential R t x beta 0 (p.val (j+1)) -220          (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left (j+1)) * a ∈221          (Ideal.span {overlapException R t x})^(j+1) := by222        rw [← hyz, mul_comm a, add_sub_cancel_left]; exact hzz223      have hnow := actual_cech_preserves_exceptional_lattices R t x beta d j224      have hnext := actual_cech_preserves_exceptional_lattices R t x beta d (j+1)225      have hbij := actual_twisted_coker_reduction_bijective R t x hreg beta d j (by omega) hnext226        hnow (actual_cech_differentials_commute_with_reduction R t x beta d j hnext hnow)227      refine (curve_section_connecting_class_zero_iff R t x beta d G hreg hregSwap (j+1) hnext228        (hregF (j+1)) (p.val (j+1)) hsec a hc).mp (hbij.1 ?_)229      rw [map_zero]230      have hcj : fullCechDifferential R t x beta 0 (p.val (j+1)) -231          (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j) * a ∈232          (Ideal.span {overlapException R t x})^j := by233        have hm := Ideal.mem_map_of_mem (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))234          (G.left_compat j)235        rw [chartExceptional, Ideal.map_pow, Ideal.map_span, Set.image_singleton] at hm236        convert add_mem (Ideal.pow_le_pow_right (Nat.le_succ j) hc) (Ideal.mul_mem_right a _ hm)237          using 1238        rw [map_sub]; ring239      refine (curve_section_connecting_class_zero_iff R t x beta d G hreg hregSwap j hnow240        (hregF j) (p.val (j+1)) ((curve_lattices_antitone R t x beta d G j).2 hsec) a hcj).mpr241        ⟨r0, ?_⟩242      convert sub_mem hr0 (thread_sub_succ_mem G p j) using 1; abel243  -- Step 2: hence at every level.244  obtain ⟨r, hr⟩ := step1 j245  refine ⟨r, ?_⟩246  simpa only [sub_add_sub_cancel] using add_mem (thread_sub_mem G p (k := J + j) (by omega))247    (curveIdealLattice_le_of_le G (j := j) (by omega) hr)248 249/-- Let `σ` be a section of the surface-to-curve-limit map that sends a surface function to its250constant thread. If a thread `p` of the curve order limit agrees with a surface function modulo the251curve lattice at a single stable level `J ≥ d - 1`, then its class lies in the range of `σ`. -/252theorem curve_limit_range_of_stable_level (R : Type) [CommRing R] (t x : R)253    (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d)254    (hreg : RegularParameterPair R t x) (hregSwap : RegularParameterPair R x t)255    (hregF : ∀ j : ℕ, Function.Injective (fun c : BlowupOverlap R t x ⧸256      (Ideal.span {overlapException R t x})^j =>257      Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j)258      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j)) * c))259    (f : R)260    (hf : ∀ j : ℕ, surfaceToCechInput R t x j f =261      (cechInputLattice R t x j).mkQ (gluedFunctionPair R t x G j))262    [IsAdicComplete (Ideal.span {t,x}) R] (J : ℕ) (hJ : d - 1 ≤ J)263    (σ : R →ₗ[R] CurveOrderLimit R t x beta G)264    (hσ : ∀ r : R, ∃ p : curveThreads R t x beta G, σ r = curveLimitMk R t x beta G p ∧ ∀ j : ℕ,265      p.val j = surfaceToChartPair R t x r)266    (p : curveThreads R t x beta G)267    (hp : ∃ r : R, p.val J - surfaceToChartPair R t x r ∈ curveIdealLattice R t x beta G J) :268    curveLimitMk R t x beta G p ∈ LinearMap.range σ := by269  -- Approximate `p` at every level, correct the approximants into an adically Cauchy sequence270  -- of surface functions, and take its limit.271  choose r hr using exists_surface_approx_of_stable_level G hreg hregSwap hregF hJ p hp272  have hker : ∀ (j : ℕ) (a : R), surfaceToChartPair R t x a ∈ curveIdealLattice R t x beta G j ↔273      a ∈ Ideal.span {f} ⊔ (Ideal.span {t,x})^j := fun j a ↦274    surface_to_curve_quotient_kernel R t x beta d G hreg hregSwap j (hregF j) f hf a275  have hdiff : ∀ j, r (j+1) - r j ∈ Ideal.span {f} ⊔ (Ideal.span {t,x})^j := fun j ↦ by276    rw [← hker]277    convert sub_mem (sub_mem (hr j) (thread_sub_succ_mem G p j))278      ((curve_lattices_antitone R t x beta d G j).1 (hr (j+1))) using 1279    rw [map_sub]; abel280  choose y hy z hz hyz using fun j ↦ Submodule.mem_sup.mp (hdiff j)281  set r' : ℕ → R := fun j ↦ r j - ∑ i ∈ Finset.range j, y i with hr'282  have hcauchy : ∀ m n, m ≤ n → r' m - r' n ∈ (Ideal.span {t,x})^m := by283    intro m n hmn284    induction n, hmn using Nat.le_induction with285    | base => simp286    | succ n hn ih =>287      have h2 : r' n - r' (n+1) = -z n := by288        simp only [hr', Finset.sum_range_succ]; linear_combination hyz n289      simpa only [← h2, sub_add_sub_cancel] using290        add_mem ih (neg_mem (Ideal.pow_le_pow_right hn (hz n)))291  obtain ⟨Lim, hLim⟩ := IsPrecomplete.prec (I := Ideal.span {t,x}) (M := R) inferInstance292    (f := r') fun {m n} hmn ↦ by293      rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top]294      exact hcauchy m n hmn295  have hLim' : ∀ j, p.val j - surfaceToChartPair R t x Lim ∈ curveIdealLattice R t x beta G j :=296    fun j ↦ by297      have h := hLim j298      rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top] at h299      have h1 := (hker j (Lim - r j)).2 <| by300        convert sub_mem301          (Ideal.mem_sup_left (neg_mem (sum_mem fun i (_ : i ∈ Finset.range j) ↦ hy i)))302          (Ideal.mem_sup_right h) using 1303        simp only [hr']; abel304      convert sub_mem (hr j) h1 using 1305      rw [map_sub]; abel306  obtain ⟨q, hq1, hq2⟩ := hσ Lim307  refine ⟨Lim, hq1.trans ((Submodule.Quotient.eq _).2 (Submodule.mem_pi.2 fun j _ ↦ ?_))⟩308  change q.val j - p.val j ∈ curveIdealLattice R t x beta G j309  rw [hq2 j, ← neg_sub]310  exact neg_mem (hLim' j)311 312end SurfaceBlowup