Two-chart curve data

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.CurveSections7 8/-!9# Two-chart curve data10 11Two-chart curve data records a curve on the blow-up of a regular parameter pair `(t, x)` through12finitely many points of the two charts and of their overlap, with local equations and completed13local isomorphisms. This file compares the level kernels of the two charts on the overlap, builds14glued generators from such data, identifies the quotients of curve sections and the curve order15limit with products of local level quotients (hence with the child order), and computes the16cokernel of the twisted Čech differential in the negative range.17 18## Main results19 20* `SurfaceBlowup.two_chart_kernels_agree_on_overlap`: both chart kernels extend to the common21  kernel.22* `SurfaceBlowup.curve_sections_quot_equiv_product`,23  `SurfaceBlowup.curve_limit_equiv_product_threads`: local descriptions of curve sections and of the24  curve order limit.25* `SurfaceBlowup.child_order_equiv_linear`: the curve order limit is linearly isomorphic to the26  child order.27* `SurfaceBlowup.glued_generators_of_two_chart_curve_data`: glued generators from two-chart data.28* `SurfaceBlowup.actual_negative_layer_coker_exact`: the cokernel tower in the negative range.29 30Provenance: `Thm_SurfaceBlowupV2_{two_chart_kernels_agree_on_overlap,31two_chart_level_generators_agree_on_overlap, two_chart_right_points_maximal,32curve_sections_quot_equiv_product, curve_limit_equiv_product_threads, child_order_equiv_linear,33glued_generators_of_two_chart_curve_data, strict_transform_right_point_equation,34global_function_strict_transform_at_right_point, two_chart_left_generators_regular_on_overlap,35two_chart_level_generators_exist, two_term_coker_map_representative,36actual_negative_layer_coker_exact, two_term_coker_map_surjective}`.37-/38 39namespace SurfaceBlowup40 41/-! ### Comparing the charts on the overlap -/42 43private theorem map_inf_eq_of_isUnit_pow_mem {A S : Type} [CommRing A] [CommRing S] (f : A →+* S)44    (I K : Ideal A) (m : A) (N : ℕ) (hm : IsUnit (f m)) (hK : m ^ N ∈ K) :45    (I ⊓ K).map f = I.map f := by46  refine le_antisymm (Ideal.map_mono inf_le_left) ?_47  rw [Ideal.map_le_iff_le_comap]48  intro a ha49  rw [Ideal.mem_comap]50  have h1 : m ^ N * a ∈ I ⊓ K := ⟨I.mul_mem_left _ ha, K.mul_mem_right _ hK⟩51  have h2 := Ideal.mem_map_of_mem f h152  obtain ⟨u, hu⟩ := hm.pow N53  have : f a = ↑u⁻¹ * f (m ^ N * a) := by54    rw [map_mul, map_pow, ← hu, ← mul_assoc, Units.inv_mul, one_mul]55  rw [this]56  exact Ideal.mul_mem_left _ _ h257 58private theorem exists_pow_mem_iInf {A : Type} [CommRing A] {κ : Type} [Finite κ]59    (J : κ → Ideal A) (m : A) (L : κ → ℕ) (hL : ∀ k, m ^ L k ∈ J k) :60    ∃ N, m ^ N ∈ ⨅ k, J k := by61  have := Fintype.ofFinite κ62  refine ⟨∑ k, L k, ?_⟩63  rw [Ideal.mem_iInf]64  intro k65  exact (J k).pow_mem_of_pow_mem (hL k)66    (Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ k))67 68private theorem leftLevelIdeal_map_leftIso_symm {R : Type} [CommRing R] {t x : R}69    {beta : BlowupRestriction R t x} (D : TwoChartCurveData R t x beta) (j : ℕ) (i : D.ι) :70    (finiteLocalCurveIdeal (BlowupChart R t x)71      ((D.Q i).comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)))72      (chartBase R t x t) (D.leftIso i (D.g i)) j).map (D.leftIso i).symm =73      commonLevelIdeal D j i := by74  unfold commonLevelIdeal finiteLocalCurveIdeal75  rw [Ideal.map_span, Set.image_pair, RingEquiv.symm_apply_apply, map_pow,76    (RingEquiv.symm_apply_eq _).2 (D.leftIso_compat i (chartBase R t x t)).symm]77  rfl78 79private theorem rightLevelIdeal_map_rightIso_symm {R : Type} [CommRing R] {t x : R}80    {beta : BlowupRestriction R t x} (D : TwoChartCurveData R t x beta) (j : ℕ) (i : D.ι) :81    (finiteLocalCurveIdeal (BlowupChart R x t) ((D.Q i).comap beta.right.toRingHom)82      (chartBase R x t x) (D.rightIso i (D.g i)) j).map (D.rightIso i).symm =83      commonLevelIdeal D j i := by84  have hZ : IsUnit (overlapSlope R t x) := IsLocalization.Away.algebraMap_isUnit _85  unfold commonLevelIdeal finiteLocalCurveIdeal86  rw [Ideal.map_span, Set.image_pair, RingEquiv.symm_apply_apply, map_pow,87    (RingEquiv.symm_apply_eq _).2 (D.rightIso_compat i (chartBase R x t x)).symm,88    beta_right_chartBase_self, map_mul, mul_pow, Ideal.span_insert, Ideal.span_insert,89    Ideal.span_singleton_mul_right_unit ((hZ.map _).pow _)]90 91/-- Localizing away from `m` sends the kernel of finitely many local level ideals onto the kernel92of the transported ideals at the surviving points, provided `m` lies in every collapsing point. -/93private theorem finiteSupportKernel_map_away {A S : Type} [CommRing A] [CommRing S] [Algebra A S]94    (m : A) [IsLocalization.Away m S] {ι κ : Type} [Finite ι] [Finite κ] (P : ι ⊕ κ → Ideal A)95    [∀ s, (P s).IsPrime] (J : ∀ s, Ideal (CompletedLocalAt A (P s))) (Q : ι → Ideal S)96    [∀ i, (Q i).IsPrime] (J' : ∀ i, Ideal (CompletedLocalAt S (Q i)))97    (Φ : ∀ i, CompletedLocalAt A (P (Sum.inl i)) ≃+* CompletedLocalAt S (Q i))98    (hΦ : ∀ i a, Φ i (completedPointMap A (P (Sum.inl i)) a) =99      completedPointMap S (Q i) (algebraMap A S a))100    (hJ : ∀ i, (J (Sum.inl i)).map (Φ i) = J' i) (hm : ∀ k, m ∈ P (Sum.inr k))101    (hmax : ∀ s, (P s).IsMaximal) (hJL : ∀ s, ∃ L : ℕ,102      ((IsLocalRing.maximalIdeal (Localization.AtPrime (P s))).map103        (localCompletionMap (Localization.AtPrime (P s)))) ^ L ≤ J s) :104    (finiteSupportKernel A (ι ⊕ κ) P J).map (algebraMap A S) = finiteSupportKernel S ι Q J' := by105  choose L hL' using hJL106  have hL : ∀ s, P s ^ L s ≤ (J s).comap (completedPointMap A (P s)) := fun s =>107    have := hmax s108    completed_point_power_contraction _ _ _ _ (hL' s)109  obtain ⟨N, hN⟩ := exists_pow_mem_iInf110    (fun k => (J (Sum.inr k)).comap (completedPointMap A (P (Sum.inr k)))) m111    (fun k => L (Sum.inr k)) (fun k => hL (Sum.inr k) (Ideal.pow_mem_pow (hm k) _))112  unfold finiteSupportKernel113  rw [iInf_sum, map_inf_eq_of_isUnit_pow_mem _ _ _ m N114    (IsLocalization.Away.algebraMap_isUnit _) hN]115  have key := finite_support_kernel_localize A S (Submonoid.powers m) ι (fun i => P (Sum.inl i))116    (fun i => J (Sum.inl i)) (fun _ => True) (fun i => CompletedLocalAt S (Q i))117    (fun i => completedPointMap S (Q i)) Φ (fun i _ a => hΦ i a) (fun i h => absurd trivial h)118    (fun i => L (Sum.inl i)) (fun i => hL (Sum.inl i))119  unfold finiteSupportKernel at key120  rw [key]121  refine le_antisymm (le_iInf fun i => ?_) (le_iInf fun i => ?_)122  · exact (iInf_le _ ⟨i, trivial⟩).trans (by rw [hJ])123  · exact (iInf_le _ i.val).trans (by rw [hJ])124 125/-- The level-`j` kernels of the two charts both extend to the common level-`j` kernel on the126overlap. -/127theorem two_chart_kernels_agree_on_overlap (R : Type) [CommRing R] (t x : R)128    (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)129    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]130    [IsNoetherianRing (BlowupChart R x t)] (j : ℕ) :131    (leftKernel D j).map (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) = commonKernel D j ∧132      (rightKernel D j).map beta.right.toRingHom = commonKernel D j := by133  constructor134  · exact finiteSupportKernel_map_away (chartSlope R t x) (leftPoint D) (leftLevelIdeal D j) D.Q135      (commonLevelIdeal D j) (fun i => (D.leftIso i).symm)136      (fun i a => (RingEquiv.symm_apply_eq _).2 (D.leftIso_compat i a).symm)137      (leftLevelIdeal_map_leftIso_symm D j) D.slope0 (two_chart_left_points_maximal R t x beta D).1138      (two_chart_left_data_transverse_finite R t x beta D j).2139  · let _ : Algebra (BlowupChart R x t) (BlowupOverlap R t x) := beta.right.toRingHom.toAlgebra140    have := blowup_overlap_isLocalization_right R t x beta141    exact finiteSupportKernel_map_away (chartSlope R x t) (rightPoint D) (rightLevelIdeal D j) D.Q142      (commonLevelIdeal D j) (fun i => (D.rightIso i).symm)143      (fun i a => (RingEquiv.symm_apply_eq _).2 (D.rightIso_compat i a).symm)144      (rightLevelIdeal_map_rightIso_symm D j) D.slopeinf145      (fun s => match s with146        | Sum.inl i =>147          (overlap_exceptional_point_comap_maximal_right R t x beta (D.Q i) (D.onE i)).1148        | Sum.inr l => D.maximalinf l)149      (two_chart_right_data_transverse_finite R t x beta D j).2150 151private theorem span_mk_map_eq_map_map {A C : Type} [CommRing A] [CommRing C] (f : A →+* C) (a : A)152    (c : C)153    (h : f a ∈ Ideal.span {c}) (j : ℕ) (K : Ideal A) (F : A)154    (hF : K.map (Ideal.Quotient.mk ((Ideal.span {a}) ^ j)) =155      Ideal.span {Ideal.Quotient.mk ((Ideal.span {a})^j) F}) :156    Ideal.span {Ideal.Quotient.mk ((Ideal.span {c})^j) (f F)}157      = (K.map f).map (Ideal.Quotient.mk ((Ideal.span {c})^j)) := by158  have cond : ∀ z ∈ (Ideal.span {a})^j,159      ((Ideal.Quotient.mk ((Ideal.span {c})^j)).comp f) z = 0 := by160    intro z hz161    simp only [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem]162    have h1 : f z ∈ ((Ideal.span {a})^j).map f := Ideal.mem_map_of_mem f hz163    rw [Ideal.map_pow, Ideal.map_span, Set.image_singleton] at h1164    exact Ideal.pow_right_mono ((Ideal.span_singleton_le_iff_mem _).2 h) j h1165  let φ := Ideal.Quotient.lift ((Ideal.span {a})^j)166    ((Ideal.Quotient.mk ((Ideal.span {c})^j)).comp f) cond167  have hφ : ∀ z, φ (Ideal.Quotient.mk ((Ideal.span {a})^j) z) =168      Ideal.Quotient.mk ((Ideal.span {c})^j) (f z) := fun z => rfl169  have := congrArg (Ideal.map φ) hF170  rw [Ideal.map_map, Ideal.map_span, Set.image_singleton, hφ] at this171  rw [← this, Ideal.map_map]172  rfl173 174/-- Generators of the level-`j` kernels of the two charts generate the same ideal on the overlap175modulo the `j`-th power of the exceptional ideal. -/176theorem two_chart_level_generators_agree_on_overlap (R : Type) [CommRing R] (t x : R) (beta :177    BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)178    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]179    [IsNoetherianRing (BlowupChart R x t)] (FA : ℕ → BlowupChart R t x) (hFA : ∀ j : ℕ,180    leftLevelKernel D j =181    Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R t x t})^j) (FA j)}) (FB : ℕ →182    BlowupChart R x t) (hFB : ∀ j : ℕ, rightLevelKernel D j =183    Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R x t x})^j) (FB j)}) (j : ℕ) :184    Ideal.span {Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j)185      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (FA j))} =186      Ideal.span {Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j)187        (beta.right (FB j))} := by188  obtain ⟨h1, h2⟩ := two_chart_kernels_agree_on_overlap R t x beta D j189  have e1 := span_mk_map_eq_map_map (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))190    (chartBase R t x t) (overlapException R t x) (by simp [overlapException]) j (leftKernel D j)191    (FA j)192    (by rw [← hFA j]; rfl)193  have hx : beta.right.toRingHom (chartBase R x t x) ∈ Ideal.span {overlapException R t x} := by194    change beta.right _ ∈ _195    rw [beta_right_chartBase_self]196    exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)197  have e2 := span_mk_map_eq_map_map beta.right.toRingHom (chartBase R x t x)198    (overlapException R t x) hx j (rightKernel D j) (FB j)199    (by rw [← hFB j]; rfl)200  rw [e1, h1]201  rw [h2] at e2202  exact e2.symm203 204/-- The points of the second chart in two-chart curve data are distinct maximal ideals lying on the205exceptional divisor. -/206theorem two_chart_right_points_maximal (R : Type) [CommRing R] (t x : R)207    (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)208    [(Ideal.span ({t,x} : Set R)).IsMaximal] :209    (∀ s, (rightPoint D s).IsMaximal) ∧ Function.Injective (rightPoint D) ∧ ∀ s, chartBase R x t x ∈210      rightPoint D s := by211  have key : ∀ i, ((D.Q i).comap beta.right.toRingHom).IsMaximal ∧212      chartSlope R x t ∉ (D.Q i).comap beta.right.toRingHom ∧213      chartBase R x t x ∈ (D.Q i).comap beta.right.toRingHom :=214    fun i => overlap_exceptional_point_comap_maximal_right R t x beta (D.Q i) (D.onE i)215  let _ : Algebra (BlowupChart R x t) (BlowupOverlap R t x) := beta.right.toRingHom.toAlgebra216  have := blowup_overlap_isLocalization_right R t x beta217  refine ⟨?_, ?_, ?_⟩218  · rintro (i | k)219    · exact (key i).1220    · exact D.maximalinf k221  · rintro (i | i) (j | j) h222    · congr 1223      apply D.inj224      have h' : (D.Q i).comap (algebraMap (BlowupChart R x t) (BlowupOverlap R t x)) =225          (D.Q j).comap (algebraMap (BlowupChart R x t) (BlowupOverlap R t x)) := h226      have := congrArg (Ideal.map (algebraMap (BlowupChart R x t) (BlowupOverlap R t x))) h'227      rwa [IsLocalization.map_under (Submonoid.powers (chartSlope R x t)),228        IsLocalization.map_under (Submonoid.powers (chartSlope R x t))] at this229    · exfalso230      have h' : (D.Q i).comap beta.right.toRingHom = D.Pinf j := h231      exact (key i).2.1 (h' ▸ D.slopeinf j)232    · exfalso233      have h' : D.Pinf i = (D.Q j).comap beta.right.toRingHom := h234      exact (key j).2.1 (h' ▸ D.slopeinf i)235    · congr 1236      exact D.injinf h237  · rintro (i | k)238    · exact (key i).2.2239    · exact D.onEinf k240 241section CurveProduct242variable {R : Type} [CommRing R] {t x : R} {beta : BlowupRestriction R t x}243  (D : TwoChartCurveData R t x beta) (j : ℕ)244 245private theorem mem_commonLevelIdeal_iff_left (i : D.ι)246    (y : CompletedLocalAt (BlowupOverlap R t x) (D.Q i)) :247    y ∈ commonLevelIdeal D j i ↔ D.leftIso i y ∈ leftLevelIdeal D j (Sum.inl i) := by248  rw [← leftLevelIdeal_map_leftIso_symm D j i, Ideal.map_symm]249  rfl250 251private theorem mem_commonLevelIdeal_iff_right (i : D.ι)252    (y : CompletedLocalAt (BlowupOverlap R t x) (D.Q i)) :253    y ∈ commonLevelIdeal D j i ↔ D.rightIso i y ∈ rightLevelIdeal D j (Sum.inl i) := by254  rw [← rightLevelIdeal_map_rightIso_symm D j i, Ideal.map_symm]255  rfl256 257/-- Finitely many local functions at distinct maximal ideals are simultaneously approximated by a258global function, modulo ideals containing a power of the maximal ideal. -/259private theorem exists_sub_mem_of_finite_support {A : Type} [CommRing A] [IsNoetherianRing A]260    {ι : Type} [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsPrime] (hmax : ∀ i, (P i).IsMaximal)261    (hP : Function.Injective P) (L : ι → ℕ) (J : ∀ i, Ideal (CompletedLocalAt A (P i)))262    (hJ : ∀ i, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map263      (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤ J i)264    (w : ∀ i, CompletedLocalAt A (P i)) :265    ∃ a : A, ∀ i, completedPointMap A (P i) a - w i ∈ J i := by266  obtain ⟨a, ha⟩ := finite_support_quotient_surjective_of_isPrime A ι P hmax hP L J hJ267    fun i => Ideal.Quotient.mk _ (w i)268  exact ⟨a, fun i => Ideal.Quotient.eq.1 (congrFun ha i)⟩269 270/-- A pair of chart functions maps to zero in the local product iff all its local components lie271in the local level ideals. -/272private theorem sectionsToProduct_eq_zero_iff (p : ChartPair R t x) :273    sectionsToProduct D j p = 0 ↔274      (∀ i, completedPointMap _ (D.Q i) (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)275        p.1) ∈ commonLevelIdeal D j i) ∧276      (∀ k, completedPointMap _ (leftPoint D (Sum.inr k)) p.1 ∈ leftLevelIdeal D j (Sum.inr k)) ∧277      ∀ l, completedPointMap _ (rightPoint D (Sum.inr l)) p.2 ∈278        rightLevelIdeal D j (Sum.inr l) := by279  simp only [funext_iff, Sum.forall, Pi.zero_apply, sectionsToProduct, RingHom.pi_apply,280    RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem]281  rfl282 283variable [(Ideal.span ({t,x} : Set R)).IsMaximal]284 285/-- Local functions at the points of the `t`-chart are approximated by a single chart function. -/286private theorem exists_left_chart_lift [IsNoetherianRing (BlowupChart R t x)]287    (y : ∀ i, CompletedLocalAt (BlowupOverlap R t x) (D.Q i))288    (y0 : ∀ k, CompletedLocalAt (BlowupChart R t x) (leftPoint D (Sum.inr k))) :289    ∃ a : BlowupChart R t x,290      (∀ i, completedPointMap _ (D.Q i) (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) a) -291        y i ∈ commonLevelIdeal D j i) ∧292      ∀ k, completedPointMap _ (leftPoint D (Sum.inr k)) a - y0 k ∈293        leftLevelIdeal D j (Sum.inr k) := by294  choose L hL using (two_chart_left_data_transverse_finite R t x beta D j).2295  obtain ⟨a, ha⟩ := exists_sub_mem_of_finite_support (leftPoint D)296    (two_chart_left_points_maximal R t x beta D).1297    (two_chart_left_points_maximal R t x beta D).2.1 L (leftLevelIdeal D j) hL fun s =>298      match s with299      | Sum.inl i => D.leftIso i (y i)300      | Sum.inr k => y0 k301  refine ⟨a, fun i => ?_, fun k => ha (Sum.inr k)⟩302  rw [mem_commonLevelIdeal_iff_left, map_sub, D.leftIso_compat]303  exact ha (Sum.inl i)304 305/-- Local functions at the points of the `x`-chart are approximated by a single chart function. -/306private theorem exists_right_chart_lift [IsNoetherianRing (BlowupChart R x t)]307    (y : ∀ i, CompletedLocalAt (BlowupOverlap R t x) (D.Q i))308    (y1 : ∀ l, CompletedLocalAt (BlowupChart R x t) (rightPoint D (Sum.inr l))) :309    ∃ b : BlowupChart R x t,310      (∀ i, completedPointMap _ (D.Q i) (beta.right b) - y i ∈ commonLevelIdeal D j i) ∧311      ∀ l, completedPointMap _ (rightPoint D (Sum.inr l)) b - y1 l ∈312        rightLevelIdeal D j (Sum.inr l) := by313  choose L hL using (two_chart_right_data_transverse_finite R t x beta D j).2314  obtain ⟨b, hb⟩ := exists_sub_mem_of_finite_support (rightPoint D)315    (two_chart_right_points_maximal R t x beta D).1316    (two_chart_right_points_maximal R t x beta D).2.1 L (rightLevelIdeal D j) hL fun s =>317      match s with318      | Sum.inl i => D.rightIso i (y i)319      | Sum.inr l => y1 l320  refine ⟨b, fun i => ?_, fun l => hb (Sum.inr l)⟩321  rw [mem_commonLevelIdeal_iff_right, map_sub, D.rightIso_compat]322  exact hb (Sum.inl i)323 324/-- Every element of the local product is the image of a pair of chart functions whose local325components agree on the overlap modulo the common level ideals. -/326private theorem exists_sectionsToProduct_eq [IsNoetherianRing (BlowupChart R t x)]327    [IsNoetherianRing (BlowupChart R x t)] (u : curveProduct D j) :328    ∃ p : ChartPair R t x, (∀ i, completedPointMap _ (D.Q i)329        (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) p.1 - beta.right p.2) ∈330        commonLevelIdeal D j i) ∧ sectionsToProduct D j p = u := by331  choose w hw using fun q => Ideal.Quotient.mk_surjective (u q)332  obtain ⟨a, hLi, hA⟩ := exists_left_chart_lift D j (fun i => w (Sum.inl i))333    (fun k => w (Sum.inr (Sum.inl k)))334  obtain ⟨b, hRi, hB⟩ := exists_right_chart_lift D j (fun i => w (Sum.inl i))335    (fun l => w (Sum.inr (Sum.inr l)))336  refine ⟨(a, b), fun i => ?_, funext fun s => ?_⟩337  · rw [map_sub, ← Ideal.Quotient.eq]338    exact (Ideal.Quotient.eq.2 (hLi i)).trans (Ideal.Quotient.eq.2 (hRi i)).symm339  rw [← hw s]340  refine Ideal.Quotient.eq.2 ?_341  rcases s with i | k | l342  exacts [hLi i, hA k, hB l]343 344end CurveProduct345 346/-- The level-`j` quotient of curve sections is additively isomorphic to the product of the local347level quotients at all points, compatibly with `sectionsToProduct`. -/348theorem curve_sections_quot_equiv_product (R : Type) [CommRing R] (t x : R)349    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]350    [IsNoetherianRing (BlowupChart R x t)] (beta : BlowupRestriction R t x) (D : TwoChartCurveData R351    t x beta) (d : ℕ) (G : GluedGenerators R t x beta d) (hG : ∀ j : ℕ,352    Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)} = leftLevelKernel D j ∧353    Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)} = rightLevelKernel D j)354    (j : ℕ) :355    ∃ E : curveSectionsQuot R t x beta G j ≃+ curveProduct D j, ∀ q : curveSectionsQuot R t x beta G356      j, ∀ p : BlowupChart R t x × BlowupChart R x t,357      (q : (BlowupChart R t x × BlowupChart R x t) ⧸ curveIdealLattice R t x beta G j) =358      (curveIdealLattice R t x beta G j).mkQ p → E q = sectionsToProduct D j p := by359  -- Strategy: identify the curve lattices with the local kernels, descend `sectionsToProduct` to360  -- the quotient, and check injectivity locally and surjectivity by chart-wise approximation.361  set α := algebraMap (BlowupChart R t x) (BlowupOverlap R t x) with hα362  have hmemL := mem_commonLevelIdeal_iff_left D j363  have hmemR := mem_commonLevelIdeal_iff_right D j364  -- the overlap curve ideal is the common kernel365  have hover : overlapCurveIdeal R t x beta G j = commonKernel D j := by366    rw [← (two_chart_kernels_agree_on_overlap R t x beta D j).1,367      ← (curve_ideal_lattice_eq_kernels R t x beta D d G hG j).1]368    rw [leftCurveIdeal, Ideal.map_sup, Ideal.map_span, Set.image_singleton, chartExceptional,369      Ideal.map_pow, Ideal.map_span, Set.image_singleton]370    rfl371  have hlat : ∀ p : BlowupChart R t x × BlowupChart R x t, p ∈ curveIdealLattice R t x beta G j ↔372      p.1 ∈ leftKernel D j ∧ p.2 ∈ rightKernel D j := by373    intro p374    rw [← (curve_ideal_lattice_eq_kernels R t x beta D d G hG j).1,375      ← (curve_ideal_lattice_eq_kernels R t x beta D d G hG j).2]376    rfl377  have hsec : ∀ p : BlowupChart R t x × BlowupChart R x t, p ∈ curveSections R t x beta G j ↔378      α p.1 - beta.right p.2 ∈ commonKernel D j := by379    intro p380    rw [← hover]381    change α p.1 - (IsLocalization.Away.invSelf (chartSlope R t x))^0 * beta.right p.2 ∈382      overlapCurveIdeal R t x beta G j ↔ _383    rw [pow_zero, one_mul]384  have hkerL : ∀ a, a ∈ leftKernel D j ↔385      ∀ s, completedPointMap _ (leftPoint D s) a ∈ leftLevelIdeal D j s := fun a => by386    simp only [leftKernel, finiteSupportKernel, Ideal.mem_iInf, Ideal.mem_comap]387  have hkerR : ∀ b, b ∈ rightKernel D j ↔388      ∀ s, completedPointMap _ (rightPoint D s) b ∈ rightLevelIdeal D j s := fun b => by389    simp only [rightKernel, finiteSupportKernel, Ideal.mem_iInf, Ideal.mem_comap]390  have hkerC : ∀ c, c ∈ commonKernel D j ↔391      ∀ i, completedPointMap _ (D.Q i) c ∈ commonLevelIdeal D j i := fun c => by392    simp only [commonKernel, finiteSupportKernel, Ideal.mem_iInf, Ideal.mem_comap]393  -- `sectionsToProduct` descends to the quotient by the curve ideal lattice394  let φ : (BlowupChart R t x × BlowupChart R x t) →+ curveProduct D j :=395    (sectionsToProduct D j).toAddMonoidHom396  have hN : (curveIdealLattice R t x beta G j).toAddSubgroup ≤ φ.ker := by397    intro p hp398    rw [AddMonoidHom.mem_ker]399    obtain ⟨h1, h2⟩ := (hlat p).1 hp400    rw [hkerL] at h1401    rw [hkerR] at h2402    refine (sectionsToProduct_eq_zero_iff D j p).2403      ⟨fun i => ?_, fun k => h1 (Sum.inr k), fun l => h2 (Sum.inr l)⟩404    rw [hmemL, D.leftIso_compat]405    exact h1 (Sum.inl i)406  let Ψ : ((BlowupChart R t x × BlowupChart R x t) ⧸ curveIdealLattice R t x beta G j) →+407      curveProduct D j := QuotientAddGroup.lift _ φ hN408  have hΨ : ∀ p, Ψ ((curveIdealLattice R t x beta G j).mkQ p) = sectionsToProduct D j p :=409    fun p => rfl410  let E₀ : curveSectionsQuot R t x beta G j →+ curveProduct D j :=411    Ψ.comp (curveSectionsQuot R t x beta G j).subtype.toAddMonoidHom412  have hinj : Function.Injective E₀ := by413    rw [injective_iff_map_eq_zero]414    rintro ⟨q, hq⟩ h0415    obtain ⟨p, hp, rfl⟩ := Submodule.mem_map.1 hq416    obtain ⟨hc1, hc2, hc3⟩ := (sectionsToProduct_eq_zero_iff D j p).1 h0417    apply Subtype.ext418    change (curveIdealLattice R t x beta G j).mkQ p = 0419    rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, hlat]420    have hA : p.1 ∈ leftKernel D j := by421      rw [hkerL]422      rintro (i | k)423      · have h := hc1 i424        rwa [hmemL, D.leftIso_compat] at h425      · exact hc2 k426    refine ⟨hA, ?_⟩427    rw [hkerR]428    rintro (i | l)429    · have hs := (hkerC _).1 ((hsec p).1 hp) i430      have hb : completedPointMap _ (D.Q i) (beta.right p.2) ∈ commonLevelIdeal D j i := by431        have := Ideal.sub_mem _ (hc1 i) hs432        rwa [map_sub, sub_sub_cancel] at this433      rw [hmemR, D.rightIso_compat] at hb434      exact hb435    · exact hc3 l436  have hsurj : Function.Surjective E₀ := by437    intro u438    obtain ⟨p, hp, rfl⟩ := exists_sectionsToProduct_eq D j u439    have hs : p ∈ curveSections R t x beta G j := by440      rw [hsec, hkerC]441      exact hp442    exact ⟨⟨(curveIdealLattice R t x beta G j).mkQ p, Submodule.mem_map_of_mem hs⟩, rfl⟩443  refine ⟨AddEquiv.ofBijective E₀ ⟨hinj, hsurj⟩, ?_⟩444  intro q p hqp445  change Ψ q = _446  rw [hqp]447  exact hΨ p448 449section Limit450 451variable {R : Type} [CommRing R] {t x : R} {beta : BlowupRestriction R t x} {d : ℕ}452  {G : GluedGenerators R t x beta d}453 454/-- Consecutive terms of a curve thread have the same class modulo the curve ideal lattice. -/455private theorem curveThreads_mkQ_succ (p : curveThreads R t x beta G) (j : ℕ) :456    (curveIdealLattice R t x beta G j).mkQ (p.val j) =457      (curveIdealLattice R t x beta G j).mkQ (p.val (j+1)) := by458  have h := p.2.2 j (Set.mem_univ _)459  rw [Submodule.mkQ_apply, Submodule.mkQ_apply, Submodule.Quotient.eq]460  simpa [towerDelta] using h461 462/-- Two curve threads have the same class in the curve order limit iff they agree levelwise463modulo the curve ideal lattices. -/464private theorem curveLimitMk_eq_iff (p p' : curveThreads R t x beta G) :465    curveLimitMk R t x beta G p = curveLimitMk R t x beta G p' ↔466      ∀ j, (curveIdealLattice R t x beta G j).mkQ (p.val j) =467        (curveIdealLattice R t x beta G j).mkQ (p'.val j) := by468  change (Submodule.Quotient.mk p : curveThreads R t x beta G ⧸ curveNullThreads R t x beta G)469    = Submodule.Quotient.mk p' ↔ _470  rw [Submodule.Quotient.eq]471  simp only [curveNullThreads, Submodule.mem_comap, curveNull, Submodule.mem_pi, Set.mem_univ,472    true_implies, Submodule.coe_subtype]473  refine forall_congr' fun j => ?_474  rw [Submodule.mkQ_apply, Submodule.mkQ_apply, Submodule.Quotient.eq]475  rfl476 477end Limit478 479/-- The curve order limit is in bijection with compatible threads in the product of the local level480quotients, compatibly with the maps from curve threads. -/481theorem curve_limit_equiv_product_threads (R : Type) [CommRing R] (t x : R)482    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]483    [IsNoetherianRing (BlowupChart R x t)] (beta : BlowupRestriction R t x) (D : TwoChartCurveData R484    t x beta) (d : ℕ) (G : GluedGenerators R t x beta d) (hG : ∀ j : ℕ,485    Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)} = leftLevelKernel D j ∧486    Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)} = rightLevelKernel D j)487    :488    ∃ E : CurveOrderLimit R t x beta G ≃ curveProductThreads D, ∀ p : curveThreads R t x beta G, ∀ j489      : ℕ, (E (curveLimitMk R t x beta G p)).val j = sectionsToProduct D j (p.val j) := by490  choose Ej hEj using fun j => curve_sections_quot_equiv_product R t x beta D d G hG j491  choose ρ hρ using fun j => curve_sections_quot_reduction_exists R t x beta d G j492  -- key: equal classes, one in curveSections, give equal images493  have key : ∀ j (a b : ChartPair R t x), a ∈ curveSections R t x beta G j →494      (curveIdealLattice R t x beta G j).mkQ a = (curveIdealLattice R t x beta G j).mkQ b →495        sectionsToProduct D j a = sectionsToProduct D j b := by496    intro j a b ha hab497    have hm : (curveIdealLattice R t x beta G j).mkQ a ∈ curveSectionsQuot R t x beta G j :=498      ⟨a, ha, rfl⟩499    rw [← hEj j ⟨_, hm⟩ a rfl, ← hEj j ⟨_, hm⟩ b hab]500  have red : ∀ j (q : ChartPair R t x),501      curveProductReduction D j (sectionsToProduct D (j+1) q) = sectionsToProduct D j q := by502    intro j q; rfl503  have secs : ∀ (p : curveThreads R t x beta G) j, p.val j ∈ curveSections R t x beta G j :=504    fun p j => p.2.1 j (Set.mem_univ _)505  let F : curveThreads R t x beta G → curveProductThreads D := fun p =>506    ⟨fun j => sectionsToProduct D j (p.val j), fun j => by507      rw [red]; exact (key j _ _ (secs p j) (curveThreads_mkQ_succ p j)).symm⟩508  let Φ : CurveOrderLimit R t x beta G → curveProductThreads D :=509    Quotient.lift F (by510      intro p p' h511      have h' : curveLimitMk R t x beta G p = curveLimitMk R t x beta G p' := Quotient.sound h512      rw [curveLimitMk_eq_iff] at h'513      apply Subtype.ext; funext j514      exact key j _ _ (secs p j) (h' j))515  have hΦ : ∀ p, Φ (curveLimitMk R t x beta G p) = F p := fun p => rfl516  have inj : Function.Injective Φ := by517    intro a b hab518    induction a using Quotient.inductionOn with | _ p => ?_519    induction b using Quotient.inductionOn with | _ p' => ?_520    change Φ (curveLimitMk R t x beta G p) = Φ (curveLimitMk R t x beta G p') at hab521    change curveLimitMk R t x beta G p = curveLimitMk R t x beta G p'522    rw [hΦ, hΦ] at hab523    rw [curveLimitMk_eq_iff]; intro j524    have hj := congrArg (fun u : curveProductThreads D => u.val j) hab525    simp only [F] at hj526    have e1 := hEj j ⟨_, ⟨p.val j, secs p j, rfl⟩⟩ (p.val j) rfl527    have e2 := hEj j ⟨_, ⟨p'.val j, secs p' j, rfl⟩⟩ (p'.val j) rfl528    have := (Ej j).injective (e1.trans (hj.trans e2.symm))529    exact congrArg Subtype.val this530  have surj : Function.Surjective Φ := by531    intro u532    -- representatives533    have hrep : ∀ j, ∃ r ∈ curveSections R t x beta G j,534        (curveIdealLattice R t x beta G j).mkQ r =535          (((Ej j).symm (u.val j) : curveSectionsQuot R t x beta G j) : _) :=536      fun j => ((Ej j).symm (u.val j)).2537    choose r hr hre using hrep538    have hs : ∀ j, sectionsToProduct D j (r j) = u.val j := by539      intro j540      rw [← hEj j ((Ej j).symm (u.val j)) (r j) (hre j).symm, AddEquiv.apply_symm_apply]541    have mem : r ∈ curveThreads R t x beta G := by542      refine ⟨fun j _ => hr j, ?_⟩543      intro j _544      have e := hρ j ((Ej (j+1)).symm (u.val (j+1))) (r (j+1)) (hre (j+1)).symm545      have e2 := hEj j _ (r (j+1)) e546      rw [← red j (r (j+1)), hs (j+1), u.2 j, ← hs j] at e2547      have e3 := hEj j ((Ej j).symm (u.val j)) (r j) (hre j).symm548      have e4 : ρ j ((Ej (j+1)).symm (u.val (j+1))) = (Ej j).symm (u.val j) :=549        (Ej j).injective (by rw [e2, e3])550      have e5 : (curveIdealLattice R t x beta G j).mkQ (r (j+1)) =551          (curveIdealLattice R t x beta G j).mkQ (r j) := by552        rw [← e, e4, hre]553      rw [Submodule.mkQ_apply, Submodule.mkQ_apply, Submodule.Quotient.eq] at e5554      have e6 := (curveIdealLattice R t x beta G j).neg_mem e5555      rw [neg_sub] at e6556      change r j - r (j+1) ∈ _557      exact e6558    refine ⟨curveLimitMk R t x beta G ⟨r, mem⟩, ?_⟩559    rw [hΦ]; apply Subtype.ext; funext j; exact hs j560  refine ⟨Equiv.ofBijective Φ ⟨inj, surj⟩, fun p j => rfl⟩561 562/-! ### The child order as a linear equivalence -/563 564section ChildOrder565 566variable {R : Type} [CommRing R] {t x : R} {beta : BlowupRestriction R t x}567  (D : TwoChartCurveData R t x beta)568 569private theorem sectionsToProduct_surface_eq (j : ℕ) (r : R) (p : AllPoints D) :570    sectionsToProduct D j (surfaceToChartPair R t x r) p =571      Ideal.Quotient.mk _ (localFromSurface D p r) := by572  rcases p with i | k | l <;> rfl573 574private def childThreadsEquiv : curveProductThreads D ≃ ∀ p, {u : ∀ j, localQuotient D j p //575    ∀ j, levelReduction (localException D p) (localCurve D p) j (u (j+1)) = u j} where576  toFun u p := ⟨fun j => u.1 j p, fun j => congrFun (u.2 j) p⟩577  invFun v := ⟨fun j p => (v p).1 j, fun j => funext fun p => (v p).2 j⟩578  left_inv _ := rfl579  right_inv _ := rfl580 581private theorem localSection_smul (q : AllPoints D) (r : R) (c : ChartPair R t x) :582    localSection D q (r • c) = localFromSurface D q r * localSection D q c := by583  rw [show r • c = algebraMap R _ r * c from Algebra.smul_def r c, map_mul]584  congr 1585  rcases q with i | k | l <;> rfl586 587end ChildOrder588 589/-- The curve order limit is `O`-linearly isomorphic to the child order, compatibly with the maps590from surface functions. -/591theorem child_order_equiv_linear (R : Type) [CommRing R] (t x : R)592    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]593    [IsNoetherianRing (BlowupChart R x t)] (beta : BlowupRestriction R t x) (D : TwoChartCurveData R594    t x beta) (d : ℕ) (G : GluedGenerators R t x beta d) (hG : ∀ j : ℕ,595    Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)} = leftLevelKernel D j ∧596    Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)} = rightLevelKernel D j)597    [∀ p : AllPoints D, IsLocalRing (localRing D p)] [∀ p : AllPoints D,598    IsNoetherianRing (localRing D p)] [∀ p : AllPoints D,599    IsAdicComplete (IsLocalRing.maximalIdeal (localRing D p)) (localRing D p)] (he : ∀ p : AllPoints600    D, localException D p ∈ IsLocalRing.maximalIdeal (localRing D p)) (O : Type) [CommRing O]601    [Algebra O R] [∀ p : AllPoints D, Algebra O (localRing D p)] (hO : ∀ (p : AllPoints D) (o : O),602    localFromSurface D p (algebraMap O R o) = algebraMap O (localRing D p) o) :603    ∃ E : CurveOrderLimit R t x beta G ≃ₗ[O] childOrder D, ∀ (p : curveThreads R t x beta G)604      (r : R), (∀ j : ℕ, p.val j = surfaceToChartPair R t x r) → E (curveLimitMk R t x beta G p) =605      childOrderMap D r := by606  obtain ⟨E₁, hE₁⟩ := curve_limit_equiv_product_threads R t x beta D d G hG607  choose Φ hΦ using fun p => curve_quotient_complete_equiv_threads _ _ (localCurve D p) (he p)608  let E : CurveOrderLimit R t x beta G ≃ childOrder D :=609    E₁.trans ((childThreadsEquiv D).trans (Equiv.piCongrRight fun p => (Φ p).symm))610  have key : ∀ u q j, ((Φ q) (E u q)).val j = (E₁ u).val j q := by611    intro u q j612    change ((Φ q) ((Φ q).symm _)).val j = _613    rw [Equiv.apply_symm_apply]614    rfl615  have hmk : ∀ (p : curveThreads R t x beta G) q j,616      ((Φ q) (E (curveLimitMk R t x beta G p) q)).val j =617        Ideal.Quotient.mk _ (localSection D q (p.val j)) := by618    intro p q j619    rw [key, hE₁]620    rfl621  have hsurj : ∀ u : CurveOrderLimit R t x beta G, ∃ p, curveLimitMk R t x beta G p = u :=622    Submodule.mkQ_surjective _623  have fadd : ∀ q j (y z : localRing D q ⧸ Ideal.span {localCurve D q}),624      ((Φ q) (y + z)).val j = ((Φ q) y).val j + ((Φ q) z).val j := by625    intro q j y z626    obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y627    obtain ⟨s', rfl⟩ := Ideal.Quotient.mk_surjective z628    rw [← map_add, hΦ, hΦ, hΦ, map_add]629  have fsmul : ∀ q j (a : localRing D q) (y : localRing D q ⧸ Ideal.span {localCurve D q})630      (s' : localRing D q),631      ((Φ q) y).val j = Ideal.Quotient.mk _ s' →632      ((Φ q) (Ideal.Quotient.mk _ a * y)).val j = Ideal.Quotient.mk _ (a * s') := by633    intro q j a y s' h634    obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y635    rw [← map_mul, hΦ, map_mul, map_mul, ← h, hΦ]636  have hadd : ∀ u v, E (u + v) = E u + E v := by637    intro u v638    obtain ⟨p, rfl⟩ := hsurj u639    obtain ⟨p', rfl⟩ := hsurj v640    funext q641    apply (Φ q).injective642    apply Subtype.ext643    funext j644    change ((Φ q) (E (curveLimitMk R t x beta G p + curveLimitMk R t x beta G p') q)).val j =645      ((Φ q) (E (curveLimitMk R t x beta G p) q + E (curveLimitMk R t x beta G p') q)).val j646    rw [fadd, ← map_add, hmk, hmk, hmk, Submodule.coe_add, Pi.add_apply, map_add, map_add]647  have hsmulR : ∀ (r : R) u q,648      E (r • u) q = Ideal.Quotient.mk _ (localFromSurface D q r) * E u q := by649    intro r u q650    obtain ⟨p, rfl⟩ := hsurj u651    apply (Φ q).injective652    apply Subtype.ext653    funext j654    rw [fsmul _ _ _ _ _ (hmk p q j), ← map_smul, hmk, Submodule.coe_smul, Pi.smul_apply,655      localSection_smul]656  refine ⟨{ E with map_add' := hadd, map_smul' := ?_ }, ?_⟩657  · intro o u658    change E (o • u) = o • E u659    rw [← algebraMap_smul R o u]660    funext q661    rw [hsmulR, hO]662    exact (Algebra.smul_def o (E u q)).symm663  · intro p r hp664    funext q665    change (Φ q).symm ((childThreadsEquiv D) (E₁ (curveLimitMk R t x beta G p)) q) = _666    rw [Equiv.symm_apply_eq]667    apply Subtype.ext668    funext j669    change (E₁ (curveLimitMk R t x beta G p)).val j q = _670    rw [hE₁, hp, sectionsToProduct_surface_eq]671    change _ = ((Φ q) (Ideal.Quotient.mk _ (localFromSurface D q r))).val j672    rw [hΦ]673 674/-- Two-chart curve data with normalized level generators yield glued generators whose level ideals675are the level kernels of the two charts. -/676theorem glued_generators_of_two_chart_curve_data (R : Type) [CommRing R] (t x : R) (beta :677    BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)678    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsLocalRing R] [IsNoetherianRing (BlowupChart R t x)]679    [IsNoetherianRing (BlowupChart R x t)] (hreg : RegularParameterPair R t x) (hregSwap :680    RegularParameterPair R x t) (d : ℕ) (FA : ℕ → BlowupChart R t x) (hFA : ∀ j : ℕ, leftLevelKernel681    D j = Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R t x t})^j) (FA j)}) (FB : ℕ →682    BlowupChart R x t) (hFB : ∀ j : ℕ, rightLevelKernel D j =683    Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R x t x})^j) (FB j)}) (hnorm : ∃ u : Rˣ,684    (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (FA 1) - algebraMap685    R (BlowupOverlap R t x) (u : R) * ((overlapSlope R t x)^d * beta.right (FB 1)) ∈686    (Ideal.span {overlapException R t x})) :687    ∃ G : GluedGenerators R t x beta d, ∀ j : ℕ,688      Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)} = leftLevelKernel D j ∧689      Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)} =690        rightLevelKernel D j := by691  obtain ⟨hLmax, hLinj, hLe⟩ := two_chart_left_points_maximal R t x beta D692  obtain ⟨hRmax, hRinj, hRe⟩ := two_chart_right_points_maximal R t x beta D693  have _ : ∀ s, (leftPoint D s).IsMaximal := hLmax694  have _ : ∀ s, (rightPoint D s).IsMaximal := hRmax695  have _ : (Ideal.span ({x,t} : Set R)).IsMaximal := by696    rw [Set.pair_comm]; infer_instance697  choose LA hLA using (two_chart_left_data_transverse_finite R t x beta D 1).2698  choose LB hLB using (two_chart_right_data_transverse_finite R t x beta D 1).2699  obtain ⟨G, hG⟩ := glued_generators_exist R t x beta hreg d FA FB700    (fun j => finite_support_generators_compatible (BlowupChart R t x) _ (leftPoint D) hLinj701      (chartBase R t x t) (leftData D) LA hLA FA hFA j)702    (fun j => finite_support_generators_compatible (BlowupChart R x t) _ (rightPoint D) hRinj703      (chartBase R x t x) (rightData D) LB hLB FB hFB j)704    (fun j => finite_support_level_generator_regular R t x _ (leftPoint D) hLe (leftData D) LA hLA705      hreg FA hFA j)706    (fun j => finite_support_level_generator_regular R x t _ (rightPoint D) hRe (rightData D) LB hLB707      hregSwap FB hFB j)708    (fun j => two_chart_level_generators_agree_on_overlap R t x beta D FA hFA FB hFB j)709    (fun j => overlap_level_generator_regular R t x hreg hregSwap beta _ (rightPoint D) hRe710      (rightData D) LB hLB FB hFB j)711    hnorm712  exact ⟨G, fun j => ⟨(hG j).1.trans (hFA j).symm, (hG j).2.trans (hFB j).symm⟩⟩713 714/-- At a point of the second chart, the pullback of the surface function `f` factors in the715completed local ring as `xᵈ · (local equation) · unit`. -/716private theorem strict_transform_right_point_equation (R : Type) [CommRing R] (t x : R) [(Ideal.span717    ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)] [IsNoetherianRing718    (BlowupChart R x t)] (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta) (d : ℕ)719    (G : GluedGenerators R t x beta d) (hG : ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk720    ((chartExceptional R t x)^j) (G.left j)} = leftLevelKernel D j ∧ Ideal.span {Ideal.Quotient.mk721    ((chartExceptional R x t)^j) (G.right j)} = rightLevelKernel D j) (f : R) (hf : ∀ j : ℕ,722    surfaceToCechInput R t x j f = (cechInputLattice R t x j).mkQ (gluedFunctionPair R t x G j)) (s723    : D.ι ⊕ D.ιinf) [IsNoetherianRing (CompletedLocalAt (BlowupChart R x t) (rightPoint D s))]724    (hereg : Function.Injective (fun a : (CompletedLocalAt (BlowupChart R x t) (rightPoint D s)) =>725    (completedPointMap (BlowupChart R x t) (rightPoint D s)) (chartBase R x t x) * a)) (hgreg :726    Function.Injective (fun a : (CompletedLocalAt (BlowupChart R x t) (rightPoint D s)) ⧸ Ideal.span727    {(completedPointMap (BlowupChart R x t) (rightPoint D s)) (chartBase R x t x)} =>728    Ideal.Quotient.mk729    (Ideal.span {(completedPointMap (BlowupChart R x t) (rightPoint D s)) (chartBase R x t x)})730    (rightData D s) * a)) :731    ∃ v : (CompletedLocalAt (BlowupChart R x t) (rightPoint D s))ˣ,732      (completedPointMap (BlowupChart R x t) (rightPoint D s)) (algebraMap R (BlowupChart R x t) f)733      = ((completedPointMap (BlowupChart R x t) (rightPoint D s)) (chartBase R x t x))^d * rightData734      D s * (v : (CompletedLocalAt (BlowupChart R x t) (rightPoint D s))) := by735  obtain ⟨hmax, hinj, hmem⟩ := two_chart_right_points_maximal R t x beta D736  have : ∀ s, (rightPoint D s).IsMaximal := hmax737  exact strict_transform_equation_of_kernels (rightPoint D) hinj _ hmem (rightData D)738    (fun j => (two_chart_right_data_transverse_finite R t x beta D j).2) G.right739    (fun j => (curve_ideal_lattice_eq_kernels R t x beta D d G hG j).2) d _740    (glued_function_right_chart R t x beta d G f hf) s hereg hgreg741 742/-- At a point of the second chart, the strict transform of `(f)` is generated by the local equation743of the two-chart curve data. -/744theorem global_function_strict_transform_at_right_point (R : Type) [CommRing R] (t x : R)745    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]746    [IsNoetherianRing (BlowupChart R x t)] (beta : BlowupRestriction R t x) (D : TwoChartCurveData R747    t x beta) (d : ℕ) (G : GluedGenerators R t x beta d) (hG : ∀ j : ℕ, Ideal.span748    {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)} = leftLevelKernel D j ∧ Ideal.span749    {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)} = rightLevelKernel D j) (f : R) (hf750    : ∀ j : ℕ, surfaceToCechInput R t x j f = (cechInputLattice R t x j).mkQ (gluedFunctionPair R t751    x G j)) (s : D.ι ⊕ D.ιinf) [IsNoetherianRing (CompletedLocalAt (BlowupChart R x t)752    (rightPoint D s))] (hereg : Function.Injective (fun a :753    (CompletedLocalAt (BlowupChart R x t) (rightPoint D s)) =>754    (completedPointMap (BlowupChart R x t) (rightPoint D s)) (chartBase R x t x) * a)) (hgreg :755    Function.Injective (fun a : (CompletedLocalAt (BlowupChart R x t) (rightPoint D s)) ⧸ Ideal.span756    {(completedPointMap (BlowupChart R x t) (rightPoint D s)) (chartBase R x t x)} =>757    Ideal.Quotient.mk758    (Ideal.span {(completedPointMap (BlowupChart R x t) (rightPoint D s)) (chartBase R x t x)})759    (rightData D s) * a)) :760    strictTransformAt R x t (rightPoint D s) d (Ideal.span {f}) = Ideal.span {rightData D s} := by761  obtain ⟨v, hv⟩ := strict_transform_right_point_equation R t x beta D d G hG f hf s hereg hgreg762  unfold strictTransformAt763  rw [principal_ideal_image]764  simp only [RingHom.comp_apply]765  have hv' : completedPointMap (BlowupChart R x t) (rightPoint D s) (chartBase R x t f) =766      (completedPointMap (BlowupChart R x t) (rightPoint D s) (chartBase R x t x)) ^ d *767        rightData D s * (v : CompletedLocalAt (BlowupChart R x t) (rightPoint D s)) := hv768  clear hv769  generalize completedPointMap (BlowupChart R x t) (rightPoint D s) (chartBase R x t x) = c at *770  generalize rightData D s = g at *771  generalize completedPointMap (BlowupChart R x t) (rightPoint D s) (chartBase R x t f) = y at *772  have hcd : Function.Injective (fun a => c ^ d * a) := IsLeftRegular.pow d hereg773  subst hv'774  have hu := v.mul_inv775  generalize (v⁻¹ : (CompletedLocalAt (BlowupChart R x t) (rightPoint D s))ˣ).val = vi at hu776  generalize v.val = vv at hu ⊢777  ext u778  rw [Submodule.mem_colon_singleton, Ideal.mem_span_singleton', Ideal.mem_span_singleton']779  simp only [smul_eq_mul]780  constructor781  · rintro ⟨w, hw⟩782    have h1 : c ^ d * u = c ^ d * (w * vv * g) := by783      have : u * c ^ d = w * (c ^ d * g * vv) := hw.symm784      linear_combination this785    exact ⟨w * vv, (hcd h1).symm⟩786  · rintro ⟨w, rfl⟩787    exact ⟨w * vi, by788      calc _ = (w * g * c ^ d) * (vv * vi) := by ring789        _ = _ := by rw [hu]; ring⟩790 791private theorem injective_mul_of_span_eq (A : Type) [CommRing A] (f g : A)792    (hf : Function.Injective (fun c : A => f * c))793    (h : Ideal.span {f} = Ideal.span {g}) : Function.Injective (fun c : A => g * c) := by794  obtain ⟨u, hu⟩ := regular_principal_generators_associated A f g795    (fun a b hab => hf (by simpa only [mul_comm] using hab)) h796  intro a b hab797  apply hf798  have : (u : A) * (f * a) = (u : A) * (f * b) := by799    simp only [← mul_assoc, ← hu]; exact hab800  exact u.isUnit.mul_right_injective this801 802/-- The first-chart glued generators are nonzerodivisors on the overlap modulo every power of the803exceptional ideal. -/804theorem two_chart_left_generators_regular_on_overlap (R : Type) [CommRing R] (t x : R)805    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]806    [IsNoetherianRing (BlowupChart R x t)] (beta : BlowupRestriction R t x) (D : TwoChartCurveData R807    t x beta) (d : ℕ) (G : GluedGenerators R t x beta d) (hG : ∀ j : ℕ,808    Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)} = leftLevelKernel D j ∧809    Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)} = rightLevelKernel D j)810    (hreg : RegularParameterPair R t x) (hregSwap : RegularParameterPair R x t) (j : ℕ) :811    Function.Injective (fun c : BlowupOverlap R t x ⧸ (Ideal.span {overlapException R t x})^j =>812      Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j)813      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j)) * c) := by814  have h788 := two_chart_level_generators_agree_on_overlap R t x beta D G.left815    (fun j => (hG j).1.symm) G.right (fun j => (hG j).2.symm) j816  obtain ⟨hmax, -, hbase⟩ := two_chart_right_points_maximal R t x beta D817  have _ : ∀ s, (rightPoint D s).IsMaximal := hmax818  obtain ⟨htr, hfin⟩ := two_chart_right_data_transverse_finite R t x beta D 1819  have hreg2 := overlap_level_generator_regular R t x hreg hregSwap beta (D.ι ⊕ D.ιinf)820    (rightPoint D) hbase (rightData D) (fun s => (hfin s).choose) (fun s => (hfin s).choose_spec)821    G.right822    (fun j => (hG j).2.symm) j823  exact injective_mul_of_span_eq _ _ _ hreg2 h788.symm824 825/-- The level kernels of both charts are principal modulo the powers of the exceptional ideals. -/826theorem two_chart_level_generators_exist (R : Type) [CommRing R] (t x : R)827    (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)828    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]829    [IsNoetherianRing (BlowupChart R x t)] :830    (∃ FA : ℕ → BlowupChart R t x, ∀ j : ℕ, leftLevelKernel D j =831      Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R t x t})^j) (FA j)}) ∧ (∃ FB : ℕ →832      BlowupChart R x t, ∀ j : ℕ, rightLevelKernel D j =833      Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R x t x})^j) (FB j)}) := by834  constructor835  · obtain ⟨hm, hinj, hte⟩ := two_chart_left_points_maximal R t x beta D836    have _ : ∀ s, (leftPoint D s).IsMaximal := hm837    exact finite_support_level_kernels_principal R t x (D.ι ⊕ D.ι0) (leftPoint D) hinj hte838      (leftData D)839      (fun s => (two_chart_left_data_transverse_finite R t x beta D 0).1 s)840      (fun j s => (two_chart_left_data_transverse_finite R t x beta D j).2 s)841  · have _ : (Ideal.span ({x,t} : Set R)).IsMaximal := by842      rw [Set.pair_comm]; infer_instance843    obtain ⟨hm, hinj, hte⟩ := two_chart_right_points_maximal R t x beta D844    have _ : ∀ s, (rightPoint D s).IsMaximal := hm845    exact finite_support_level_kernels_principal R x t (D.ι ⊕ D.ιinf) (rightPoint D) hinj hte846      (rightData D)847      (fun s => (two_chart_right_data_transverse_finite R t x beta D 0).1 s)848      (fun j s => (two_chart_right_data_transverse_finite R t x beta D j).2 s)849 850/-- The map induced on cokernels sends the class of `a` to the class of `u1 a`. -/851private theorem two_term_coker_map_representative (O : Type) [CommRing O] (A0 A1 B0 B1 : Type)852    [AddCommGroup A0] [Module O A0] [AddCommGroup A1] [Module O A1] [AddCommGroup B0] [Module O B0]853    [AddCommGroup B1] [Module O B1] (dA : A0 →ₗ[O] A1) (dB : B0 →ₗ[O] B1) (u0 : A0 →ₗ[O] B0)854    (u1 : A1 →ₗ[O] B1) (h : u1.comp dA = dB.comp u0) (a : A1) :855    twoTermCokerMap dA dB u0 u1 h ((LinearMap.range dA).mkQ a) = (LinearMap.range dB).mkQ (u1 a) :=856  rfl857 858/-! ### The negative-twist cokernel -/859 860section LayerCoordinates861 862variable (R : Type) [CommRing R] (t x : R)863 864local notation "A" => BlowupChart R t x865local notation "O" => BlowupOverlap R t x866local notation "tO" => algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t)867local notation "z" => selfZPow (chartSlope R t x) (BlowupOverlap R t x)868 869private theorem layer_xO_eq : algebraMap A O (chartBase R t x x) = tO * z 1 := by870  rw [← blowup_chart_relation, map_mul]871  have := selfZPow_natCast (chartSlope R t x) (BlowupOverlap R t x) 1872  simp only [Nat.cast_one, pow_one] at this873  rw [this]874 875private theorem layer_invSelf_pow (n : ℕ) :876    (IsLocalization.Away.invSelf (chartSlope R t x) : O) ^ n = z (-n) := by877  rw [selfZPow_neg_natCast, IsLocalization.Away.invSelf, ← IsLocalization.mk'_pow, one_pow]878  congr 1879 880private theorem layer_slope_pow (n : ℕ) : (algebraMap A O (chartSlope R t x)) ^ n = z n :=881  (selfZPow_natCast _ _ n).symm882 883private theorem layer_z_nat (n : ℕ) : z (n:ℤ) = (z 1) ^ n := by884  rw [selfZPow_natCast]; have := selfZPow_natCast (chartSlope R t x) (BlowupOverlap R t x) 1885  simp only [Nat.cast_one, pow_one] at this; rw [this]886 887private theorem layer_tO_pow_mem (j : ℕ) (o : O) : tO ^ j * o ∈ (Ideal.span {tO}) ^ j :=888  Ideal.mul_mem_right _ _ (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self _) j)889 890private theorem layer_beta_right (beta : BlowupRestriction R t x) (c : R) (n : ℕ) :891    beta.right (chartBase R x t c * chartSlope R x t ^ n) =892      algebraMap A O (chartBase R t x c) * z (-(n:ℤ)) := by893  rw [map_mul, map_pow, beta.slope, layer_invSelf_pow]894  congr 1895  exact beta.right.commutes c896 897end LayerCoordinates898 899section LayerLifts900 901variable {R : Type} [CommRing R] {t x : R}902 903local notation "A" => BlowupChart R t x904local notation "O" => BlowupOverlap R t x905local notation "tO" => algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t)906 907/-- A linear map on the overlap whose values at all integral powers `z ℓ` of the slope lie in a908submodule takes all its values in that submodule. -/909private theorem layer_map_mem_of_slope_pows {Q : Type} [AddCommGroup Q] [Module R Q]910    (Φ : O →ₗ[R] Q) (N : Submodule R Q) (z : ℤ → O)911    (hznat : ∀ n : ℕ, (algebraMap A O (chartSlope R t x)) ^ n = z n)912    (hzadd : ∀ a b : ℤ, z (a + b) = z a * z b) (hz0 : z 0 = 1) (hmono : ∀ ℓ : ℤ, Φ (z ℓ) ∈ N)913    (o : O) : Φ o ∈ N := by914  obtain ⟨n, a, ha⟩ := IsLocalization.Away.surj (chartSlope R t x) o915  have ho : o = algebraMap A O a * z (-(n:ℤ)) := by916    rw [← ha, hznat, mul_assoc, ← hzadd]; simp [hz0]917  obtain ⟨p, rfl⟩ := Ideal.Quotient.mk_surjective a918  rw [ho]919  clear ha ho920  induction p using Polynomial.induction_on' with921  | add p q hp hq => rw [map_add, map_add, add_mul, map_add]; exact add_mem hp hq922  | monomial m c =>923    have : algebraMap A O (Ideal.Quotient.mk _ (Polynomial.monomial m c)) * z (-(n:ℤ)) =924        c • z (m + -(n:ℤ)) := by925      rw [← Polynomial.C_mul_X_pow_eq_monomial, map_mul (Ideal.Quotient.mk _),926        map_pow (Ideal.Quotient.mk _), hzadd, ← hznat, Algebra.smul_def]927      change algebraMap A O (chartBase R t x c * chartSlope R t x ^ m) * _ =928        algebraMap A O (chartBase R t x c) * _929      rw [map_mul, map_pow]; ring930    rw [this, map_smul]; exact Submodule.smul_mem _ _ (hmono _)931 932/-- A linear map on the overlap killing all multiples of `t` is `(t, x)`-torsion valued. -/933private theorem layer_span_le_ker {Q : Type} [AddCommGroup Q] [Module R Q] (Φ : O →ₗ[R] Q)934    (hΦt : ∀ o, Φ (tO * o) = 0) (e : O) :935    Ideal.span {t,x} ≤ LinearMap.ker (LinearMap.toSpanSingleton R Q (Φ e)) := by936  rw [Ideal.span_le]937  rintro c hc938  simp only [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.toSpanSingleton_apply]939  rw [← map_smul, Algebra.smul_def]940  rcases hc with h | h <;> (try rw [Set.mem_singleton_iff] at h) <;> rw [h]941  · exact hΦt e942  · change Φ (algebraMap A O (chartBase R t x x) * e) = 0943    rw [layer_xO_eq, mul_assoc]; exact hΦt _944 945private theorem principalLayerMap_tO_apply (j : ℕ) (a : O) :946    principalLayerMap O tO j a = Ideal.Quotient.mk _ (tO ^ j * a) := by947  rw [mul_comm]; rfl948 949/-- Laurent coordinates of the `j`-th layer classes of functions on the `t`-chart: they have no950negative coefficients. -/951private theorem layer_left_laurent_lift (j : ℕ) (z : ℤ → O)952    (hznat : ∀ n : ℕ, (algebraMap A O (chartSlope R t x)) ^ n = z n)953    (L : LaurentPolynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer O tO j)954    (hL : ∀ r : R, ∀ ell : ℤ, (L (LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) *955      LaurentPolynomial.T ell)).val = principalLayerMap O tO j (algebraMap A O (chartBase R t x r) *956        z ell))957    (p : Polynomial R) :958    ∃ F : LaurentPolynomial (R ⧸ Ideal.span {t,x}), (∀ ℓ : ℤ, ℓ < 0 → F.coeff ℓ = 0) ∧959      (L F).val = Ideal.Quotient.mk _ (tO ^ j * algebraMap A O (Ideal.Quotient.mk _ p)) := by960  induction p using Polynomial.induction_on' with961  | add p q hp hq =>962    obtain ⟨F1, h1, e1⟩ := hp963    obtain ⟨F2, h2, e2⟩ := hq964    refine ⟨F1 + F2, fun ℓ hℓ => ?_, ?_⟩965    · rw [AddMonoidAlgebra.coeff_add, Finsupp.add_apply, h1 ℓ hℓ, h2 ℓ hℓ, add_zero]966    · rw [map_add, Submodule.coe_add, e1, e2, map_add, map_add, mul_add, map_add]967  | monomial m c =>968    refine ⟨LaurentPolynomial.C (Ideal.Quotient.mk _ c) * LaurentPolynomial.T m, fun ℓ hℓ => ?_,969      ?_⟩970    · rw [← LaurentPolynomial.single_eq_C_mul_T, AddMonoidAlgebra.coeff_single,971        Finsupp.single_apply, if_neg (by omega)]972    · have hmonoA : Ideal.Quotient.mk (Ideal.span {blowupRelation R t x}) (Polynomial.monomial m c)973          = chartBase R t x c * chartSlope R t x ^ m := by974        rw [← Polynomial.C_mul_X_pow_eq_monomial, map_mul, map_pow]; rfl975      rw [hL, principalLayerMap_tO_apply, hmonoA, map_mul (algebraMap _ _),976        map_pow (algebraMap _ _), hznat]977 978/-- Laurent coordinates of the `j`-th layer classes of twisted functions on the `x`-chart: they979vanish above degree `j - d`. -/980private theorem layer_right_laurent_lift (beta : BlowupRestriction R t x) (d j : ℕ) (z : ℤ → O)981    (hzadd : ∀ a b : ℤ, z (a + b) = z a * z b)982    (hbeta : ∀ (c : R) (n : ℕ), beta.right (chartBase R x t c * chartSlope R x t ^ n) =983      algebraMap A O (chartBase R t x c) * z (-(n:ℤ)))984    (L : LaurentPolynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer O tO j)985    (hL : ∀ r : R, ∀ ell : ℤ, (L (LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) *986      LaurentPolynomial.T ell)).val = principalLayerMap O tO j (algebraMap A O (chartBase R t x r) *987        z ell))988    (q : Polynomial R) :989    ∃ F : LaurentPolynomial (R ⧸ Ideal.span {t,x}), (∀ ℓ : ℤ, (j:ℤ) - d < ℓ → F.coeff ℓ = 0) ∧990      (L F).val = Ideal.Quotient.mk _ (tO ^ j * (z ((j:ℤ) - d) *991        beta.right (Ideal.Quotient.mk _ q))) := by992  induction q using Polynomial.induction_on' with993  | add p q hp hq =>994    obtain ⟨F1, h1, e1⟩ := hp995    obtain ⟨F2, h2, e2⟩ := hq996    refine ⟨F1 + F2, fun ℓ hℓ => ?_, ?_⟩997    · rw [AddMonoidAlgebra.coeff_add, Finsupp.add_apply, h1 ℓ hℓ, h2 ℓ hℓ, add_zero]998    · rw [map_add, Submodule.coe_add, e1, e2, map_add, map_add, mul_add, mul_add, map_add]999  | monomial m c =>1000    refine ⟨LaurentPolynomial.C (Ideal.Quotient.mk _ c) * LaurentPolynomial.T ((j:ℤ) - d - m),1001      fun ℓ hℓ => ?_, ?_⟩1002    · rw [← LaurentPolynomial.single_eq_C_mul_T, AddMonoidAlgebra.coeff_single,1003        Finsupp.single_apply, if_neg (by omega)]1004    · have hmonoB : Ideal.Quotient.mk (Ideal.span {blowupRelation R x t}) (Polynomial.monomial m c)1005          = chartBase R x t c * chartSlope R x t ^ m := by1006        rw [← Polynomial.C_mul_X_pow_eq_monomial, map_mul, map_pow]; rfl1007      rw [hL, principalLayerMap_tO_apply, hmonoB, hbeta,1008        show (j:ℤ) - d - m = ((j:ℤ) - d) + -(m:ℤ) by ring, hzadd]1009      congr 1; ring1010 1011/-- A linear map on the overlap which kills `t^j`-multiples of Čech differentials maps every1012integral power `z ℓ` of the slope into a submodule containing the images of the window powers1013`z (-a-1)`, `a < d - j - 1`. -/1014private theorem layer_slope_pow_mem (beta : BlowupRestriction R t x) (d j : ℕ) {Q : Type}1015    [AddCommGroup Q] [Module R Q] (Φ : O →ₗ[R] Q) (N : Submodule R Q) (z : ℤ → O)1016    (hznat : ∀ n : ℕ, (algebraMap A O (chartSlope R t x)) ^ n = z n)1017    (hzadd : ∀ a b : ℤ, z (a + b) = z a * z b) (hz1 : ∀ n : ℕ, z n = z 1 ^ n)1018    (hinv : ∀ n : ℕ, (IsLocalization.Away.invSelf (chartSlope R t x) : O) ^ n = z (-n))1019    (hxO : algebraMap A O (chartBase R t x x) = tO * z 1)1020    (hbeta : ∀ (c : R) (n : ℕ), beta.right (chartBase R x t c * chartSlope R x t ^ n) =1021      algebraMap A O (chartBase R t x c) * z (-(n:ℤ)))1022    (hΦD : ∀ (o : O) (w : A × BlowupChart R x t), tO ^ j * o = fullCechDifferential R t x beta d w →1023      Φ o = 0)1024    (hwin : ∀ a : ℕ, a < d - j - 1 → Φ (z (-(a:ℤ) - 1)) ∈ N) (ℓ : ℤ) : Φ (z ℓ) ∈ N := by1025  have hDab : ∀ a b, fullCechDifferential R t x beta d (a, b) = algebraMap A O a -1026      (IsLocalization.Away.invSelf (chartSlope R t x))^d * beta.right b := fun _ _ => rfl1027  by_cases h0 : 0 ≤ ℓ1028  · obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le h01029    have : tO ^ j * z n = fullCechDifferential R t x beta d1030        ((chartBase R t x t)^j * chartSlope R t x ^ n, 0) := by1031      rw [hDab, map_zero, mul_zero, sub_zero, map_mul, map_pow, map_pow, hznat]1032    rw [hΦD _ _ this]; exact Submodule.zero_mem _1033  by_cases h1 : ℓ ≤ (j:ℤ) - d1034  · obtain ⟨s, hs⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ (j:ℤ) - d - ℓ by omega)1035    have : tO ^ j * z ℓ = fullCechDifferential R t x beta d1036        (0, -(chartBase R x t x ^ j * chartSlope R x t ^ s)) := by1037      rw [hDab, map_zero, zero_sub, map_neg, mul_neg, neg_neg, ← map_pow (chartBase R x t) x j,1038        hbeta, hinv, map_pow, map_pow, hxO]1039      rw [show ℓ = -(d:ℤ) + j + -(s:ℤ) by omega, hzadd, hzadd, hz1]1040      ring1041    rw [hΦD _ _ this]; exact Submodule.zero_mem _1042  · push Not at h0 h11043    obtain ⟨a, ha⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ -ℓ - 1 by omega)1044    rw [show ℓ = -(a:ℤ) - 1 by omega]1045    exact hwin a (by omega)1046 1047/-- In a Laurent polynomial identity `F_A = F_B + ∑ₐ vₐ T^(-a-1)` (`a < d - j - 1`) where `F_A` has1048no negative coefficients and `F_B` none above degree `j - d`, all `vₐ` vanish. -/1049private theorem laurent_window_coeffs_eq_zero {K : Type} [CommRing K] (d j : ℕ)1050    (FA FB : LaurentPolynomial K) (hFA0 : ∀ ℓ : ℤ, ℓ < 0 → FA.coeff ℓ = 0)1051    (hFB0 : ∀ ℓ : ℤ, (j:ℤ) - d < ℓ → FB.coeff ℓ = 0) (v : Fin (d-j-1) → K)1052    (hF : FA = FB + ∑ a : Fin (d-j-1), LaurentPolynomial.C (v a) *1053      LaurentPolynomial.T (-((a:ℕ):ℤ) - 1)) (a : Fin (d-j-1)) : v a = 0 := by1054  have hlt := a.isLt1055  have := congrArg (fun F : LaurentPolynomial K => F.coeff (-((a:ℕ):ℤ) - 1)) hF1056  rw [AddMonoidAlgebra.coeff_add, Finsupp.add_apply, hFA0 _ (by omega), hFB0 _ (by omega),1057    zero_add, AddMonoidAlgebra.coeff_sum, Finsupp.finsetSum_apply, Finset.sum_eq_single a] at this1058  · rw [← LaurentPolynomial.single_eq_C_mul_T, AddMonoidAlgebra.coeff_single,1059      Finsupp.single_eq_same] at this1060    exact this.symm1061  · intro b _ hb1062    rw [← LaurentPolynomial.single_eq_C_mul_T, AddMonoidAlgebra.coeff_single, Finsupp.single_apply,1063      if_neg]1064    intro h; apply hb; ext; omega1065  · simp1066 1067/-- Laurent coordinates of the window sums `t^j ∑ₐ vₐ z^(-a-1)`. -/1068private theorem layer_window_sum_eq {j : ℕ} (d : ℕ) (z : ℤ → O)1069    (L : LaurentPolynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer O tO j)1070    (hL : ∀ r : R, ∀ ell : ℤ, (L (LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) *1071      LaurentPolynomial.T ell)).val = principalLayerMap O tO j (algebraMap A O (chartBase R t x r) *1072        z ell))1073    (v' : Fin (d-j-1) → R) :1074    (L (∑ a : Fin (d-j-1), LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) (v' a)) *1075      LaurentPolynomial.T (-((a:ℕ):ℤ) - 1))).val =1076      Ideal.Quotient.mk _ (tO ^ j * ∑ a : Fin (d-j-1), v' a • z (-((a:ℕ):ℤ) - 1)) := by1077  rw [map_sum, Submodule.coe_sum, Finset.mul_sum, map_sum]1078  refine Finset.sum_congr rfl fun a _ => ?_1079  rw [hL, principalLayerMap_tO_apply, Algebra.smul_def]; rfl1080 1081/-- Laurent-coordinate core of `layer_window_coeffs_eq_zero_of_mem`: if1082`t^j (p - z^(j-d) q) ≡ t^j ∑ₐ vₐ z^(-a-1)` modulo `(t)^(j+1)`, then all `vₐ` vanish modulo1083`(t, x)`. -/1084private theorem layer_window_coeffs_eq_zero_of_layer_eq (beta : BlowupRestriction R t x) (d j : ℕ)1085    (z : ℤ → O) (hznat : ∀ n : ℕ, (algebraMap A O (chartSlope R t x)) ^ n = z n)1086    (hzadd : ∀ a b : ℤ, z (a + b) = z a * z b)1087    (hbeta : ∀ (c : R) (n : ℕ), beta.right (chartBase R x t c * chartSlope R x t ^ n) =1088      algebraMap A O (chartBase R t x c) * z (-(n:ℤ)))1089    (L : LaurentPolynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer O tO j)1090    (hL : ∀ r : R, ∀ ell : ℤ, (L (LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) *1091      LaurentPolynomial.T ell)).val = principalLayerMap O tO j (algebraMap A O (chartBase R t x r) *1092        z ell))1093    (v' : Fin (d-j-1) → R) (p q : Polynomial R)1094    (hq : tO ^ j * (algebraMap A O (Ideal.Quotient.mk _ p) -1095        z ((j:ℤ) - d) * beta.right (Ideal.Quotient.mk _ q)) -1096      tO ^ j * ∑ a : Fin (d-j-1), v' a • z (-((a:ℕ):ℤ) - 1) ∈ (Ideal.span {tO}) ^ (j+1))1097    (a : Fin (d-j-1)) : Ideal.Quotient.mk (Ideal.span {t,x}) (v' a) = 0 := by1098  obtain ⟨FA, hFA0, hFA⟩ := layer_left_laurent_lift j z hznat L hL p1099  obtain ⟨FB, hFB0, hFB⟩ := layer_right_laurent_lift beta d j z hzadd hbeta L hL q1100  have hFG := layer_window_sum_eq d z L hL v'1101  set FG := ∑ a : Fin (d-j-1), LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) (v' a)) *1102    LaurentPolynomial.T (-((a:ℕ):ℤ) - 1)1103  have heq : L FA = L (FB + FG) := by1104    apply Subtype.ext1105    rw [map_add, Submodule.coe_add, hFA, hFB, hFG, ← map_add, Ideal.Quotient.eq]1106    convert hq using 1; ring1107  exact laurent_window_coeffs_eq_zero d j FA FB hFA0 hFB0 _ (L.injective heq) a1108 1109/-- If a Čech input pair has differential congruent to `t^j ∑ₐ vₐ z^(-a-1)` modulo `(t)^(j+1)`1110(`a < d - j - 1`), then all `vₐ` vanish modulo `(t, x)`. -/1111private theorem layer_window_coeffs_eq_zero_of_mem (hreg : RegularParameterPair R t x)1112    (beta : BlowupRestriction R t x) (hregSwap : RegularParameterPair R x t) (d j : ℕ) (hj : j < d)1113    (hnow : cechInputLattice R t x j ≤1114      (cechOutputLattice R t x j).comap (fullCechDifferential R t x beta d))1115    (z : ℤ → O) (hznat : ∀ n : ℕ, (algebraMap A O (chartSlope R t x)) ^ n = z n)1116    (hzadd : ∀ a b : ℤ, z (a + b) = z a * z b) (hz1 : ∀ n : ℕ, z n = z 1 ^ n)1117    (hinv : ∀ n : ℕ, (IsLocalization.Away.invSelf (chartSlope R t x) : O) ^ n = z (-n))1118    (hxO : algebraMap A O (chartBase R t x x) = tO * z 1)1119    (hbeta : ∀ (c : R) (n : ℕ), beta.right (chartBase R x t c * chartSlope R x t ^ n) =1120      algebraMap A O (chartBase R t x c) * z (-(n:ℤ)))1121    (L : LaurentPolynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer O tO j)1122    (hL : ∀ r : R, ∀ ell : ℤ, (L (LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) *1123      LaurentPolynomial.T ell)).val = principalLayerMap O tO j (algebraMap A O (chartBase R t x r) *1124        z ell))1125    (v' : Fin (d-j-1) → R) (w : A × BlowupChart R x t)1126    (hq : fullCechDifferential R t x beta d w -1127      tO ^ j * ∑ a : Fin (d-j-1), v' a • z (-((a:ℕ):ℤ) - 1) ∈ (Ideal.span {tO}) ^ (j+1))1128    (a : Fin (d-j-1)) : Ideal.Quotient.mk (Ideal.span {t,x}) (v' a) = 0 := by1129  set G := ∑ a : Fin (d-j-1), v' a • z (-((a:ℕ):ℤ) - 1)1130  have hw0 : finiteCechDifferential R t x beta d j hnow (Submodule.Quotient.mk w) = 0 := by1131    change Submodule.Quotient.mk (p := cechOutputLattice R t x j)1132      (fullCechDifferential R t x beta d w) = 01133    rw [Submodule.Quotient.mk_eq_zero]1134    change _ ∈ (Ideal.span {tO}) ^ j1135    rw [← sub_add_cancel (fullCechDifferential R t x beta d w) (tO ^ j * G)]1136    exact Ideal.add_mem _ (Ideal.pow_le_pow_right (Nat.le_succ j) hq) (layer_tO_pow_mem R t x j G)1137  have hw : Submodule.Quotient.mk (p := cechInputLattice R t x j) w = 0 :=1138    actual_negative_twist_kernel_zero R t x hreg beta hregSwap d j hj.le hnow1139      (hw0.trans (map_zero _).symm)1140  rw [Submodule.Quotient.mk_eq_zero] at hw1141  obtain ⟨w1, w2⟩ := w1142  obtain ⟨h1, h2⟩ := hw1143  change w1 ∈ (Ideal.span {chartBase R t x t}) ^ j at h11144  change w2 ∈ (Ideal.span {chartBase R x t x}) ^ j at h21145  rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton'] at h1 h21146  obtain ⟨a', rfl⟩ := h11147  obtain ⟨b', rfl⟩ := h21148  have hDab : ∀ a b, fullCechDifferential R t x beta d (a, b) = algebraMap A O a -1149      (IsLocalization.Away.invSelf (chartSlope R t x))^d * beta.right b := fun _ _ => rfl1150  obtain ⟨p, rfl⟩ := Ideal.Quotient.mk_surjective a'1151  obtain ⟨q, rfl⟩ := Ideal.Quotient.mk_surjective b'1152  have hbx : beta.right (chartBase R x t x) = tO * z 1 := (beta.right.commutes x).trans hxO1153  have hDw : fullCechDifferential R t x beta d1154      (Ideal.Quotient.mk _ p * chartBase R t x t ^ j,1155        Ideal.Quotient.mk _ q * chartBase R x t x ^ j) =1156      tO ^ j * (algebraMap A O (Ideal.Quotient.mk _ p) -1157        z ((j:ℤ) - d) * beta.right (Ideal.Quotient.mk _ q)) := by1158    rw [hDab, map_mul, map_mul beta.right, map_pow beta.right, hbx, hinv, map_pow,1159      show (j:ℤ) - d = -(d:ℤ) + j by ring, hzadd, hz1]1160    ring1161  rw [hDw] at hq1162  exact layer_window_coeffs_eq_zero_of_layer_eq beta d j z hznat hzadd hbeta L hL v' p q hq a1163 1164end LayerLifts1165 1166/-- If `i (v mod I) = Φ (∑ₐ vₐ • wₐ)` for all `v`, then every `Φ wₐ` lies in the range of `i`. -/1167private theorem window_mem_range {R M Q : Type} [CommRing R] [AddCommGroup M] [Module R M]1168    [AddCommGroup Q] [Module R Q] {I : Ideal R} {n : ℕ} (i : (Fin n → R ⧸ I) →ₗ[R] Q)1169    (Φ : M →ₗ[R] Q) (w : Fin n → M)1170    (hi : ∀ v : Fin n → R, i (fun a => Ideal.Quotient.mk I (v a)) = Φ (∑ a, v a • w a))1171    (a : Fin n) : Φ (w a) ∈ LinearMap.range i := by1172  refine ⟨fun b => Ideal.Quotient.mk I ((Pi.single a (1:R) : Fin n → R) b), ?_⟩1173  rw [hi, Finset.sum_eq_single a]1174  · rw [Pi.single_eq_same, one_smul]1175  · intro b _ hb; rw [Pi.single_eq_of_ne hb, zero_smul]1176  · exact fun h => absurd (Finset.mem_univ _) h1177 1178/-- The projection of the overlap onto the level-`(j + 1)` Čech cokernel. -/1179private noncomputable def layerCokerProj (R : Type) [CommRing R] (t x : R)1180    (beta : BlowupRestriction R t x) (d j : ℕ) (hnext : cechInputLattice R t x (j + 1) ≤1181      (cechOutputLattice R t x (j + 1)).comap (fullCechDifferential R t x beta d)) :1182    BlowupOverlap R t x →ₗ[R] (CechLevelOutput R t x (j+1) ⧸1183      LinearMap.range (finiteCechDifferential R t x beta d (j+1) hnext)) :=1184  (LinearMap.range _).mkQ ∘ₗ (cechOutputLattice R t x (j+1)).mkQ1185 1186/-- The window map from `(R ⧸ (t, x))^(d - j - 1)` to the level-`(j + 1)` Čech cokernel, sending the1187`a`-th basis vector to the class of `t^j z^(-a-1)`; its image contains every class of `t^j o`. -/1188private theorem exists_layer_window_map (R : Type) [CommRing R] (t x : R)1189    (beta : BlowupRestriction R t x) (d j : ℕ) (hnext : cechInputLattice R t x (j + 1) ≤1190      (cechOutputLattice R t x (j + 1)).comap (fullCechDifferential R t x beta d)) :1191    ∃ i : (Fin (d-j-1) → (R ⧸ Ideal.span {t,x})) →ₗ[R] (CechLevelOutput R t x (j+1) ⧸1192      LinearMap.range (finiteCechDifferential R t x beta d (j+1) hnext)),1193      (∀ v : Fin (d-j-1) → R, i (fun a => Ideal.Quotient.mk _ (v a)) =1194        (LinearMap.range (finiteCechDifferential R t x beta d (j+1) hnext)).mkQ1195          ((cechOutputLattice R t x (j+1)).mkQ1196            (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) ^ j *1197              ∑ a, v a • selfZPow (chartSlope R t x) (BlowupOverlap R t x) (-((a:ℕ):ℤ)-1)))) ∧1198      ∀ o : BlowupOverlap R t x,1199        (LinearMap.range (finiteCechDifferential R t x beta d (j+1) hnext)).mkQ1200          ((cechOutputLattice R t x (j+1)).mkQ1201            (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) ^ j * o)) ∈1202          LinearMap.range i := by1203  set D := fullCechDifferential R t x beta d with hD1204  set D1 := finiteCechDifferential R t x beta d (j+1) hnext with hD11205  set tO := algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) with htO1206  have hxO := layer_xO_eq R t x1207  have hinv := layer_invSelf_pow R t x1208  have hznat : ∀ n : ℕ,1209      (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartSlope R t x)) ^ n =1210      selfZPow (chartSlope R t x) (BlowupOverlap R t x) n := layer_slope_pow R t x1211  have hz1 := layer_z_nat R t x1212  have hzadd : ∀ a b : ℤ, selfZPow (chartSlope R t x) (BlowupOverlap R t x) (a + b) =1213      selfZPow (chartSlope R t x) (BlowupOverlap R t x) a *1214        selfZPow (chartSlope R t x) (BlowupOverlap R t x) b :=1215    fun a b => selfZPow_add _ _1216  have hz0 := selfZPow_zero (chartSlope R t x) (BlowupOverlap R t x)1217  have hbeta := layer_beta_right R t x beta1218  set z := selfZPow (chartSlope R t x) (BlowupOverlap R t x)1219  clear_value z1220  set Q := CechLevelOutput R t x (j+1) ⧸ LinearMap.range D11221  let ψ := layerCokerProj R t x beta d j hnext1222  let Φ := ψ ∘ₗ LinearMap.mulLeft R (tO ^ j)1223  have hΦ : ∀ o, Φ o = ψ (tO ^ j * o) := fun o => rfl1224  have hψD : ∀ w, ψ (D w) = 0 := by1225    intro w1226    change (LinearMap.range D1).mkQ (D1 (Submodule.Quotient.mk w)) = 01227    exact (Submodule.Quotient.mk_eq_zero _).2 ⟨_, rfl⟩1228  have hΦt : ∀ o, Φ (tO * o) = 0 := by1229    intro o1230    rw [hΦ]1231    change (LinearMap.range D1).mkQ (Submodule.Quotient.mk _) = 01232    rw [(Submodule.Quotient.mk_eq_zero _).2, map_zero]1233    change _ ∈ (Ideal.span {tO}) ^ (j+1)1234    rw [← mul_assoc, ← pow_succ]1235    exact layer_tO_pow_mem R t x (j+1) o1236  have hI := layer_span_le_ker Φ hΦt1237  let i : (Fin (d-j-1) → (R ⧸ Ideal.span {t,x})) →ₗ[R] Q :=1238    ∑ a : Fin (d-j-1), (Submodule.liftQ (Ideal.span {t,x})1239      (LinearMap.toSpanSingleton R Q (Φ (z (-((a:ℕ):ℤ)-1)))) (hI _)) ∘ₗ LinearMap.proj a1240  have hi : ∀ v : Fin (d-j-1) → R, i (fun a => Ideal.Quotient.mk _ (v a)) =1241      Φ (∑ a, v a • z (-((a:ℕ):ℤ)-1)) := by1242    intro v1243    simp only [i, LinearMap.sum_apply, LinearMap.comp_apply, LinearMap.proj_apply, map_sum,1244      map_smul]1245    rfl1246  have hmono : ∀ ℓ : ℤ, Φ (z ℓ) ∈ LinearMap.range i := by1247    refine layer_slope_pow_mem beta d j Φ _ z hznat hzadd hz1 hinv hxO hbeta1248      (fun o w h => by rw [hΦ, h, hψD]) fun a har =>1249        window_mem_range i Φ (fun b : Fin (d-j-1) => z (-((b:ℕ):ℤ)-1)) hi ⟨a, har⟩1250  exact ⟨i, hi, layer_map_mem_of_slope_pows Φ _ z hznat hzadd hz0 hmono⟩1251 1252/-- Exactness half of `actual_negative_layer_coker_exact`: a map whose range consists of exactly1253the classes of `t^j o` is exact at the level-`(j + 1)` cokernel. -/1254private theorem layer_coker_exact_of_range (R : Type) [CommRing R] (t x : R)1255    (beta : BlowupRestriction R t x) (d j : ℕ) (hnext : cechInputLattice R t x (j + 1) ≤1256      (cechOutputLattice R t x (j + 1)).comap (fullCechDifferential R t x beta d))1257    (hnow : cechInputLattice R t x j ≤1258      (cechOutputLattice R t x j).comap (fullCechDifferential R t x beta d))1259    (hcomm : (cechOutputReduction R t x j).comp1260      (finiteCechDifferential R t x beta d (j + 1) hnext) =1261      (finiteCechDifferential R t x beta d j hnow).comp (cechInputReduction R t x j))1262    {M : Type} [AddCommGroup M] [Module R M] (i : M →ₗ[R] (CechLevelOutput R t x (j + 1) ⧸1263      LinearMap.range (finiteCechDifferential R t x beta d (j + 1) hnext)))1264    (hall : ∀ o : BlowupOverlap R t x,1265      (LinearMap.range (finiteCechDifferential R t x beta d (j + 1) hnext)).mkQ1266        ((cechOutputLattice R t x (j + 1)).mkQ1267          (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) ^ j * o)) ∈1268        LinearMap.range i)1269    (hi0 : ∀ v, ∃ o : BlowupOverlap R t x,1270      i v = (LinearMap.range (finiteCechDifferential R t x beta d (j + 1) hnext)).mkQ1271        ((cechOutputLattice R t x (j + 1)).mkQ1272          (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) ^ j * o))) :1273    Function.Exact i (twoTermCokerMap (finiteCechDifferential R t x beta d (j + 1) hnext)1274      (finiteCechDifferential R t x beta d j hnow) (cechInputReduction R t x j)1275      (cechOutputReduction R t x j) hcomm) := by1276  intro y1277  refine ⟨fun hy => ?_, ?_⟩1278  swap1279  · rintro ⟨v, rfl⟩1280    obtain ⟨o, ho⟩ := hi0 v1281    rw [ho]1282    refine (two_term_coker_map_representative R _ _ _ _ _ _ _ _ hcomm _).trans ?_1283    change (LinearMap.range _).mkQ (Submodule.Quotient.mk (p := cechOutputLattice R t x j)1284      (_ ^ j * o)) = 01285    rw [(Submodule.Quotient.mk_eq_zero _).2, map_zero]1286    exact layer_tO_pow_mem R t x j o1287  let ψ := layerCokerProj R t x beta d j hnext1288  have hψD : ∀ w, ψ (fullCechDifferential R t x beta d w) = 0 := fun w =>1289    (Submodule.Quotient.mk_eq_zero _).2 ⟨Submodule.Quotient.mk w, rfl⟩1290  obtain ⟨y1, rfl⟩ := Submodule.Quotient.mk_surjective _ y1291  obtain ⟨y0, rfl⟩ := Submodule.Quotient.mk_surjective _ y11292  have hred : twoTermCokerMap (finiteCechDifferential R t x beta d (j + 1) hnext)1293      (finiteCechDifferential R t x beta d j hnow) (cechInputReduction R t x j)1294      (cechOutputReduction R t x j) hcomm (ψ y0) =1295      (LinearMap.range (finiteCechDifferential R t x beta d j hnow)).mkQ1296        (Submodule.Quotient.mk y0) :=1297    two_term_coker_map_representative R _ _ _ _ _ _ _ _ hcomm _1298  change twoTermCokerMap _ _ _ _ hcomm (ψ y0) = 0 at hy1299  rw [hred, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at hy1300  obtain ⟨q, hq⟩ := hy1301  obtain ⟨w, rfl⟩ := Submodule.Quotient.mk_surjective _ q1302  change Submodule.Quotient.mk (fullCechDifferential R t x beta d w) =1303    Submodule.Quotient.mk y0 at hq1304  rw [Submodule.Quotient.eq] at hq1305  change _ ∈ (Ideal.span {algebraMap (BlowupChart R t x) (BlowupOverlap R t x)1306    (chartBase R t x t)}) ^ j at hq1307  rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton'] at hq1308  obtain ⟨o, ho⟩ := hq1309  obtain ⟨v, hv⟩ := hall (-o)1310  refine ⟨v, ?_⟩1311  rw [hv]1312  change ψ (_ ^ j * -o) = ψ y01313  rw [show y0 = fullCechDifferential R t x beta d w +1314    (-o) * algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) ^ j by1315      linear_combination ho, map_add, hψD, zero_add, mul_comm]1316 1317/-- In the negative range `j < d`, the reduction map between the cokernels at levels `j + 1` and `j`1318has kernel the image of an injection from `(R ⧸ (t, x))^(d - j - 1)`. -/1319theorem actual_negative_layer_coker_exact (R : Type) [CommRing R] (t x : R) (hreg :1320    RegularParameterPair R t x) (beta : BlowupRestriction R t x) (hregSwap : RegularParameterPair R1321    x t) (d j : ℕ) (hj : j < d) (hnext : cechInputLattice R t x (j + 1) ≤1322    (cechOutputLattice R t x (j + 1)).comap (fullCechDifferential R t x beta d)) (hnow :1323    cechInputLattice R t x j ≤1324    (cechOutputLattice R t x j).comap (fullCechDifferential R t x beta d)) (hcomm :1325    (cechOutputReduction R t x j).comp (finiteCechDifferential R t x beta d (j + 1) hnext) =1326    (finiteCechDifferential R t x beta d j hnow).comp (cechInputReduction R t x j)) :1327    ∃ i : (Fin (d-j-1) → (R ⧸ Ideal.span {t,x})) →ₗ[R] (CechLevelOutput R t x (j+1) ⧸1328      LinearMap.range (finiteCechDifferential R t x beta d (j+1) hnext)), Function.Injective i ∧1329      Function.Exact i (twoTermCokerMap (finiteCechDifferential R t x beta d (j+1) hnext)1330      (finiteCechDifferential R t x beta d j hnow) (cechInputReduction R t x j)1331      (cechOutputReduction R t x j) hcomm) := by1332  -- Strategy: `i` sends `v` to the class of `tO ^ j * Σ v a • z (-a - 1)`; injectivity is the1333  -- vanishing of Laurent window coefficients, exactness the description of the layer by windows.1334  set D := fullCechDifferential R t x beta d with hD1335  set D1 := finiteCechDifferential R t x beta d (j+1) hnext with hD11336  set D0 := finiteCechDifferential R t x beta d j hnow with hD01337  obtain ⟨i, hi, hall⟩ := exists_layer_window_map R t x beta d j hnext1338  set tO := algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) with htO1339  have hxO := layer_xO_eq R t x1340  have hinv := layer_invSelf_pow R t x1341  have hznat : ∀ n : ℕ,1342      (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartSlope R t x)) ^ n =1343      selfZPow (chartSlope R t x) (BlowupOverlap R t x) n := layer_slope_pow R t x1344  have hz1 := layer_z_nat R t x1345  have hzadd : ∀ a b : ℤ, selfZPow (chartSlope R t x) (BlowupOverlap R t x) (a + b) =1346      selfZPow (chartSlope R t x) (BlowupOverlap R t x) a *1347        selfZPow (chartSlope R t x) (BlowupOverlap R t x) b :=1348    fun a b => selfZPow_add _ _1349  obtain ⟨L, hL⟩ := overlap_layer_laurent_coordinates R t x hreg j1350  have hbeta := layer_beta_right R t x beta1351  set z := selfZPow (chartSlope R t x) (BlowupOverlap R t x)1352  clear_value z1353  have hmemO : ∀ (n : ℕ) (o : BlowupOverlap R t x),1354      o ∈ cechOutputLattice R t x n ↔ o ∈ (Ideal.span {tO}) ^ n :=1355    fun _ _ => Iff.rfl1356  have hlift : ∀ v : Fin (d-j-1) → (R ⧸ Ideal.span {t,x}), ∃ v' : Fin (d-j-1) → R,1357      (fun a => Ideal.Quotient.mk _ (v' a)) = v :=1358    fun v => ⟨fun a => (Ideal.Quotient.mk_surjective (v a)).choose,1359      funext fun a => (Ideal.Quotient.mk_surjective (v a)).choose_spec⟩1360  refine ⟨i, ?_, layer_coker_exact_of_range R t x beta d j hnext hnow hcomm i hall fun v => ?_⟩1361  · rw [injective_iff_map_eq_zero]1362    intro v hv1363    obtain ⟨v', rfl⟩ := hlift v1364    rw [hi] at hv1365    set G := ∑ a : Fin (d-j-1), v' a • z (-((a:ℕ):ℤ) - 1) with hG1366    change (LinearMap.range D1).mkQ (Submodule.Quotient.mk (tO ^ j * G)) = 0 at hv1367    rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at hv1368    obtain ⟨q, hq⟩ := hv1369    obtain ⟨w, rfl⟩ := Submodule.Quotient.mk_surjective _ q1370    change Submodule.Quotient.mk (D w) = Submodule.Quotient.mk (tO ^ j * G) at hq1371    rw [Submodule.Quotient.eq, hmemO] at hq1372    funext a1373    exact layer_window_coeffs_eq_zero_of_mem hreg beta hregSwap d j hj hnow z hznat hzadd hz1 hinv1374      hxO hbeta L hL v' w hq a1375  · obtain ⟨v', rfl⟩ := hlift v1376    exact ⟨_, hi v'⟩1377 1378/-- The map induced on cokernels is surjective when `u1` is surjective. -/1379theorem two_term_coker_map_surjective (O : Type) [CommRing O] (A0 A1 B0 B1 : Type) [AddCommGroup A0]1380    [Module O A0] [AddCommGroup A1] [Module O A1] [AddCommGroup B0] [Module O B0] [AddCommGroup B1]1381    [Module O B1] (dA : A0 →ₗ[O] A1) (dB : B0 →ₗ[O] B1) (u0 : A0 →ₗ[O] B0) (u1 : A1 →ₗ[O] B1)1382    (h : u1.comp dA = dB.comp u0) (hu1 : Function.Surjective u1) :1383    Function.Surjective (twoTermCokerMap dA dB u0 u1 h) := by1384  intro y1385  obtain ⟨b, rfl⟩ := Submodule.mkQ_surjective (LinearMap.range dB) y1386  obtain ⟨a, rfl⟩ := hu1 b1387  exact ⟨(LinearMap.range dA).mkQ a, rfl⟩1388 1389end SurfaceBlowup