Lean sources / SurfaceBlowup / Blowup / H0Comparison.lean
Comparing surface functions with Čech data on the blow-up
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.NilpotentGluing7 8/-!9# Comparing surface functions with Čech data on the blow-up10 11For a regular parameter pair `(t, x)` of `R`, the blow-up is covered by the two charts12`R[x/t]` and `R[t/x]`; truncating modulo powers of the exceptional ideals gives a tower of13two-term Čech complexes with twisted differentials. This file shows that `R` computes the14degree-`0` cohomology of this tower: the surface-to-Čech map has kernel `(t, x) ^ j` and image15the closed classes at each level, and for `(t, x)`-adically complete `R` it is an isomorphism16onto compatible closed threads. Consequences: glued generators come from a unique surface17function of order `d`, closed twisted classes come from surface functions, and the connecting18class of a curve section is detected by the curve ideal lattice. The file also records basic19facts on surface states and tangent divisors, and partitions a fixed tangent cell inside a20coordinate chart into `pi`-adic cosets.21 22## Main results23 24* `surface_to_cech_kernel`, `surface_to_cech_range`, `surface_threads_injective`,25 `surface_threads_range`: the `H⁰` comparison.26* `glued_function_exists_unique`, `glued_function_initial_form`.27* `twisted_kernel_from_surface`, `curve_section_connecting_class_zero_iff`.28* `has_tangent_divisor_multiplicity`, `surface_state_vertical_perturbation`.29* `fixed_tangent_cell_chart_partition`, `fixed_tangent_cell_chart_measurable`.30 31Provenance: `Thm_SurfaceBlowupV2_*` nodes `surface_layer_kernel_lift`,32`surface_parameters_mem_maximal`, `has_tangent_divisor_multiplicity`,33`initial_form_lift_independent`, `surface_section_closed`, `surface_state_{ideal_proper,34generator_mem_maximal, vertical_perturbation}`, `surface_to_cech_{kernel, range}`,35`glued_function_{order, initial_form, exists_unique}`, `surface_threads_{injective, range}`,36`curve_section_connecting_class_zero_iff`, `surface_to_curve_limit_exists`,37`surface_vertical_parameter`, `surface_tangent_jet_small_perturbation`,38`fixed_tangent_cell_chart_{partition, measurable}`, `transition_unit_congruent_one`,39`twisted_kernel_from_surface`.40-/41 42open scoped BigOperators ENNReal43 44namespace SurfaceBlowup45 46/-! ### Lifting through the layers of the Čech complex -/47 48/-- In the chart `R[x/t]`, `x = t * (x/t)`. -/49theorem chartBase_x_eq (R : Type) [CommRing R] (t x : R) :50 chartBase R t x x = chartBase R t x t * chartSlope R t x := by51 simp only [chartBase, chartSlope, RingHom.comp_apply, ← map_mul]52 rw [eq_comm, Ideal.Quotient.eq]53 exact Ideal.subset_span rfl54 55/-- Overlap image of a right-chart monomial, twisted by `(x/t)⁻ᵈ`. -/56private theorem beta_right_monomial (R : Type) [CommRing R] (t x : R)57 (beta : BlowupRestriction R t x)58 (r : R) (i j d : ℕ) :59 beta.right (chartBase R x t r * chartSlope R x t ^ i * chartBase R x t x ^ j) *60 IsLocalization.Away.invSelf (chartSlope R t x) ^ d =61 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x r) *62 selfZPow (chartSlope R t x) (BlowupOverlap R t x) ((j:ℤ) - d + -(i:ℤ)) *63 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) ^ j := by64 have hβr := beta_right_chartBase beta65 have hz : (j:ℤ) - d + -(i:ℤ) = -(i:ℤ) + j + -(d:ℤ) := by ring66 rw [map_mul, map_mul, map_pow, map_pow, hβr, hβr, beta.slope, chartBase_x_eq, map_mul, hz,67 selfZPow_add, selfZPow_add, ← invSelf_pow_eq_selfZPow, ← invSelf_pow_eq_selfZPow,68 selfZPow_natCast, mul_pow]69 ring70 71 72/-- The left chart's layer coordinates are compatible with the overlap's Laurent coordinates. -/73private theorem cech_layer_coordinates_left (R : Type) [CommRing R] (t x : R) (j : ℕ)74 (LA : Polynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R]75 PrincipalLayer (BlowupChart R t x) (chartBase R t x t) j)76 (hLA : ∀ r : R, ∀ i : ℕ,77 (LA (Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) * Polynomial.X^i)).val =78 principalLayerMap (BlowupChart R t x) (chartBase R t x t) j79 (chartBase R t x r * (chartSlope R t x)^i))80 (LO : LaurentPolynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer (BlowupOverlap R t x)81 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)) j)82 (hLO : ∀ r : R, ∀ ell : ℤ, (LO (LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) *83 LaurentPolynomial.T ell)).val = principalLayerMap (BlowupOverlap R t x)84 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)) j85 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x r) *86 selfZPow (chartSlope R t x) (BlowupOverlap R t x) ell))87 (hψ : (Ideal.span {chartBase R t x t})^(j+1) ≤ ((Ideal.span88 {(algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)})^(j+1)).comap89 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)))90 (P : Polynomial (R ⧸ Ideal.span {t,x})) :91 Ideal.quotientMap _ (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) hψ (LA P).val =92 (LO P.toLaurent).val := by93 induction P using Polynomial.induction_on' with94 | add p q hp hq =>95 rw [map_add, Submodule.coe_add, map_add, hp, hq, map_add, map_add, Submodule.coe_add]96 | monomial i c =>97 obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective c98 rw [← Polynomial.C_mul_X_pow_eq_monomial, hLA, Polynomial.toLaurent_C_mul_X_pow, hLO,99 principalLayerMap_apply_eq_mk, principalLayerMap_apply_eq_mk, Ideal.quotientMap_mk,100 selfZPow_natCast]101 simp only [map_mul, map_pow]102 103/-- The right chart's layer coordinates, twisted by `(x/t)⁻ᵈ`, are compatible with the overlap's104Laurent coordinates. -/105private theorem cech_layer_coordinates_right (R : Type) [CommRing R] (t x : R)106 (beta : BlowupRestriction R t x) (d j : ℕ)107 (LB : Polynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R]108 PrincipalLayer (BlowupChart R x t) (chartBase R x t x) j)109 (hLB : ∀ r : R, ∀ i : ℕ,110 (LB (Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) * Polynomial.X^i)).val =111 principalLayerMap (BlowupChart R x t) (chartBase R x t x) j112 (chartBase R x t r * (chartSlope R x t)^i))113 (LO : LaurentPolynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer (BlowupOverlap R t x)114 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)) j)115 (hLO : ∀ r : R, ∀ ell : ℤ, (LO (LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) *116 LaurentPolynomial.T ell)).val = principalLayerMap (BlowupOverlap R t x)117 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)) j118 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x r) *119 selfZPow (chartSlope R t x) (BlowupOverlap R t x) ell))120 (hψ : (Ideal.span {chartBase R x t x})^(j+1) ≤ ((Ideal.span121 {(algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)})^(j+1)).comap122 beta.right.toRingHom)123 (Q : Polynomial (R ⧸ Ideal.span {t,x})) :124 Ideal.quotientMap _ beta.right.toRingHom hψ (LB Q).val *125 Ideal.Quotient.mk _ ((IsLocalization.Away.invSelf (chartSlope R t x))^d) =126 (LO (LaurentPolynomial.T ((j:ℤ) - d) * LaurentPolynomial.invert Q.toLaurent)).val := by127 induction Q using Polynomial.induction_on' with128 | add p q hp hq =>129 rw [map_add, Submodule.coe_add, map_add, add_mul, hp, hq]130 simp only [map_add, mul_add, Submodule.coe_add]131 | monomial i c =>132 obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective c133 have hT : LaurentPolynomial.T ((j:ℤ) - d) * LaurentPolynomial.invert134 (Polynomial.toLaurent (Polynomial.C (Ideal.Quotient.mk (Ideal.span {t, x}) r) *135 Polynomial.X ^ i)) = LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t, x}) r) *136 LaurentPolynomial.T ((j:ℤ) - d + -(i:ℤ)) := by137 rw [Polynomial.toLaurent_C_mul_X_pow]138 simp only [map_mul, LaurentPolynomial.invert_C, LaurentPolynomial.invert_T]139 rw [mul_left_comm, ← LaurentPolynomial.T_add]140 rw [← Polynomial.C_mul_X_pow_eq_monomial, hLB, hT, hLO, principalLayerMap_apply_eq_mk,141 principalLayerMap_apply_eq_mk, Ideal.quotientMap_mk, ← map_mul]142 exact congrArg _ (beta_right_monomial R t x beta r i j d)143 144/-- Polynomial coordinates on the `j`-th layers: a Čech input pair `(a, b)` of order `j` with145twist-`d` differential of order `j + 1` has coordinates `P, Q` with `P = Tʲ⁻ᵈ · Q(T⁻¹)`. -/146private theorem cech_layer_coordinates (R : Type) [CommRing R] (t x : R)147 (hreg : RegularParameterPair R t x)148 (beta : BlowupRestriction R t x) (hregSwap : RegularParameterPair R x t) (d j : ℕ)149 (a : BlowupChart R t x) (b : BlowupChart R x t)150 (ha : a ∈ (Ideal.span {chartBase R t x t}) ^ j) (hb : b ∈ (Ideal.span {chartBase R x t x}) ^ j)151 (hD : fullCechDifferential R t x beta d (a, b) ∈152 (Ideal.span {algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t)}) ^153 (j + 1))154 :155 ∃ LA : Polynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R]156 PrincipalLayer (BlowupChart R t x) (chartBase R t x t) j,157 ∃ LB : Polynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R]158 PrincipalLayer (BlowupChart R x t) (chartBase R x t x) j,159 (∀ r : R, ∀ i : ℕ,160 (LA (Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) * Polynomial.X^i)).val161 = principalLayerMap (BlowupChart R t x) (chartBase R t x t) j162 (chartBase R t x r * (chartSlope R t x)^i)) ∧163 (∀ r : R, ∀ i : ℕ,164 (LB (Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) * Polynomial.X^i)).val165 = principalLayerMap (BlowupChart R x t) (chartBase R x t x) j166 (chartBase R x t r * (chartSlope R x t)^i)) ∧167 ∃ P Q : Polynomial (R ⧸ Ideal.span {t,x}),168 (LA P).val = Ideal.Quotient.mk _ a ∧ (LB Q).val = Ideal.Quotient.mk _ b ∧169 P.toLaurent - LaurentPolynomial.T ((j:ℤ) - d) * LaurentPolynomial.invert Q.toLaurent = 0 := by170 set ι := algebraMap (BlowupChart R t x) (BlowupOverlap R t x)171 set eA := chartBase R t x t172 set eB := chartBase R x t x173 set eO := ι eA174 set W := chartSlope R t x175 have hιx : ι (chartBase R t x x) = eO * algebraMap (BlowupChart R t x) (BlowupOverlap R t x)176 W := by177 rw [chartBase_x_eq, map_mul]178 have hβr : ∀ r : R, beta.right (chartBase R x t r) = ι (chartBase R t x r) :=179 beta_right_chartBase beta180 have hβeB : beta.right eB = eO * algebraMap (BlowupChart R t x) (BlowupOverlap R t x) W := by181 rw [hβr, hιx]182 obtain ⟨LA, hLA⟩ := chart_layer_polynomial_coordinates R t x hreg j183 have hB := chart_layer_polynomial_coordinates R x t hregSwap j184 rw [Set.pair_comm x t] at hB185 obtain ⟨LB, hLB⟩ := hB186 obtain ⟨LO, hLO⟩ := overlap_layer_laurent_coordinates R t x hreg j187 -- the reduction maps188 have hψA : (Ideal.span {eA})^(j+1) ≤ ((Ideal.span {eO})^(j+1)).comap ι := by189 rw [← Ideal.map_le_iff_le_comap, Ideal.map_pow, Ideal.map_span, Set.image_singleton]190 have hψB : (Ideal.span {eB})^(j+1) ≤ ((Ideal.span {eO})^(j+1)).comap beta.right.toRingHom := by191 rw [← Ideal.map_le_iff_le_comap, Ideal.map_pow, Ideal.map_span, Set.image_singleton]192 apply Ideal.pow_right_mono193 rw [Ideal.span_le, Set.singleton_subset_iff]194 change beta.right eB ∈ _195 rw [hβeB]196 exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)197 let ψA := Ideal.quotientMap _ ι hψA198 let ψB := Ideal.quotientMap _ beta.right.toRingHom hψB199 let c : (BlowupOverlap R t x) ⧸ (Ideal.span {eO})^(j+1) :=200 Ideal.Quotient.mk _ ((IsLocalization.Away.invSelf W)^d)201 have hPA : ∀ P, ψA (LA P).val = (LO P.toLaurent).val :=202 cech_layer_coordinates_left R t x j LA hLA LO hLO hψA203 have hPB : ∀ Q, ψB (LB Q).val * c =204 (LO (LaurentPolynomial.T ((j:ℤ) - d) * LaurentPolynomial.invert Q.toLaurent)).val :=205 cech_layer_coordinates_right R t x beta d j LB hLB LO hLO hψB206 set P := LA.symm ⟨_, mk_mem_principalLayer _ j ha⟩ with hPdef207 set Q := LB.symm ⟨_, mk_mem_principalLayer _ j hb⟩ with hQdef208 have hP : (LA P).val = Ideal.Quotient.mk _ a := by rw [hPdef, LinearEquiv.apply_symm_apply]209 have hQ : (LB Q).val = Ideal.Quotient.mk _ b := by rw [hQdef, LinearEquiv.apply_symm_apply]210 have key : LO (P.toLaurent - LaurentPolynomial.T ((j:ℤ) - d) *211 LaurentPolynomial.invert Q.toLaurent) = 0 := by212 apply Subtype.ext213 rw [map_sub, Submodule.coe_sub, ← hPA, ← hPB, hP, hQ]214 simp only [ψA, ψB, c]215 rw [Ideal.quotientMap_mk, Ideal.quotientMap_mk, ← map_mul, ← map_sub, ZeroMemClass.coe_zero,216 Ideal.Quotient.eq_zero_iff_mem]217 convert hD using 1218 change _ = ι a - _ * _219 simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe]220 ring221 exact ⟨LA, LB, hLA, hLB, P, Q, hP, hQ, (LinearEquiv.map_eq_zero_iff LO).1 key⟩222 223 224/-- One lifting step: such a pair agrees to order `j + 1` with `(tᵈ r, xᵈ r)` for some225`r ∈ (t, x) ^ (j - d)`. -/226private theorem cech_layer_step (R : Type) [CommRing R] (t x : R)227 (hreg : RegularParameterPair R t x)228 (beta : BlowupRestriction R t x) (hregSwap : RegularParameterPair R x t) (d j : ℕ)229 (a : BlowupChart R t x) (b : BlowupChart R x t)230 (ha : a ∈ (Ideal.span {chartBase R t x t}) ^ j) (hb : b ∈ (Ideal.span {chartBase R x t x}) ^ j)231 (hD : fullCechDifferential R t x beta d (a, b) ∈232 (Ideal.span {algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t)}) ^233 (j + 1))234 :235 ∃ r ∈ (Ideal.span {t,x})^(j - d),236 a - (chartBase R t x t)^d * chartBase R t x r ∈ (Ideal.span {chartBase R t x t})^(j+1) ∧237 b - (chartBase R x t x)^d * chartBase R x t r ∈ (Ideal.span {chartBase R x t x})^(j+1) := by238 obtain ⟨LA, LB, hLA, hLB, P, Q, hP, hQ, hz⟩ :=239 cech_layer_coordinates R t x hreg beta hregSwap d j a b ha hb hD240 rcases lt_or_ge j d with hjd | hjd241 · obtain ⟨hP0, hQ0⟩ := negative_laurent_twist_has_no_kernel _ ((j:ℤ) - d) (by omega) P Q hz242 refine ⟨0, Ideal.zero_mem _, ?_, ?_⟩243 · rw [map_zero, mul_zero, sub_zero, ← Ideal.Quotient.eq_zero_iff_mem, ← hP, hP0, map_zero]; rfl244 · rw [map_zero, mul_zero, sub_zero, ← Ideal.Quotient.eq_zero_iff_mem, ← hQ, hQ0, map_zero]; rfl245 obtain ⟨m, rfl⟩ : ∃ m, j = d + m := ⟨j - d, by omega⟩246 have hz' : P.toLaurent = LaurentPolynomial.T (m : ℤ) * LaurentPolynomial.invert Q.toLaurent := by247 rw [sub_eq_zero] at hz248 rw [hz]249 congr 2250 push_cast251 ring252 obtain ⟨hdeg, hcoef⟩ := laurent_nonnegative_twist_kernel _ m P Q hz'253 choose c hc using fun i => Ideal.Quotient.mk_surjective (I := Ideal.span {t,x}) (P.coeff i)254 have hPsum : P = ∑ i ∈ Finset.range (m+1),255 Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) (c i)) * Polynomial.X^i := by256 ext n257 simp only [Polynomial.finsetSum_coeff, Polynomial.coeff_C_mul_X_pow, hc]258 rw [Finset.sum_ite_eq]259 split_ifs with hn260 · rfl261 · simp only [Finset.mem_range, not_lt] at hn262 exact Polynomial.coeff_eq_zero_of_natDegree_lt (by omega)263 have hQsum : Q = ∑ i ∈ Finset.range (m+1),264 Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) (c (m - i))) * Polynomial.X^i := by265 ext n266 simp only [Polynomial.finsetSum_coeff, Polynomial.coeff_C_mul_X_pow, hc]267 rw [Finset.sum_ite_eq, hcoef n]268 simp only [Finset.mem_range]269 split_ifs <;> first | rfl | omega270 refine ⟨∑ i ∈ Finset.range (m+1), c i * t^(m-i) * x^i, ?_, ?_, ?_⟩271 · rw [Nat.add_sub_cancel_left]272 refine Ideal.sum_mem _ fun i hi => ?_273 have hi' : i ≤ m := Nat.lt_succ_iff.1 (Finset.mem_range.1 hi)274 rw [mul_assoc]275 refine Ideal.mul_mem_left _ _ ?_276 have := Ideal.mul_mem_mul (Ideal.pow_mem_pow (Ideal.subset_span (Set.mem_insert t {x})) (m-i))277 (Ideal.pow_mem_pow (Ideal.subset_span (Set.mem_insert_of_mem t (Set.mem_singleton x))) i)278 rwa [← pow_add, Nat.sub_add_cancel hi'] at this279 · rw [← Ideal.Quotient.eq, ← hP, hPsum, map_sum, Submodule.coe_sum]280 simp_rw [hLA, principalLayerMap_apply_eq_mk]281 rw [← map_sum]282 congr 1283 rw [map_sum, Finset.mul_sum]284 refine Finset.sum_congr rfl fun i hi => ?_285 have hi' : i ≤ m := by simp at hi; omega286 simp only [map_mul, map_pow, chartBase_x_eq]287 rw [show d + m = d + (m - i) + i by omega, pow_add, pow_add, mul_pow]288 ring289 · rw [← Ideal.Quotient.eq, ← hQ, hQsum, map_sum, Submodule.coe_sum]290 simp_rw [hLB, principalLayerMap_apply_eq_mk]291 rw [← map_sum]292 congr 1293 rw [map_sum, Finset.mul_sum, ← Finset.sum_range_reflect]294 refine Finset.sum_congr rfl fun i hi => ?_295 have hi' : i ≤ m := by simp at hi; omega296 simp only [map_mul, map_pow, chartBase_x_eq R x t, Nat.add_sub_cancel]297 rw [show m - (m - i) = i by omega, show d + m = d + i + (m - i) by omega, pow_add, pow_add,298 mul_pow]299 ring300 301/-- A Čech input class of level `j + 1` that is closed (for twist `0`) and vanishes at level302`j` comes from a surface function `r ∈ (t, x) ^ j`. -/303private theorem surface_layer_kernel_lift (R : Type) [CommRing R] (t x : R)304 (hreg : RegularParameterPair R t x) (hregSwap : RegularParameterPair R x t)305 (beta : BlowupRestriction R t x) (j : ℕ)306 (hnext : cechInputLattice R t x (j + 1) ≤ (cechOutputLattice R t x (j + 1)).comap307 (fullCechDifferential R t x beta 0)) (w : CechLevelInput R t x (j + 1))308 (hw : finiteCechDifferential R t x beta 0 (j + 1) hnext w = 0)309 (hred : cechInputReduction R t x j w = 0) :310 ∃ r ∈ (Ideal.span {t,x})^j, surfaceToCechInput R t x (j+1) r = w := by311 induction w using Submodule.Quotient.induction_on with312 | H z =>313 obtain ⟨a, b⟩ := z314 rw [finiteCechDifferential, Submodule.mapQ_apply, Submodule.Quotient.mk_eq_zero] at hw315 change Submodule.Quotient.mk (a, b) = (0 : CechLevelInput R t x j) at hred316 rw [Submodule.Quotient.mk_eq_zero] at hred317 have hD : fullCechDifferential R t x beta 0 (a, b) ∈318 (Ideal.span {algebraMap (BlowupChart R t x) (BlowupOverlap R t x)319 (chartBase R t x t)})^(j+1) := hw320 have ha : a ∈ (Ideal.span {chartBase R t x t})^j := hred.1321 have hb : b ∈ (Ideal.span {chartBase R x t x})^j := hred.2322 obtain ⟨r, hr, hA, hB⟩ := cech_layer_step R t x hreg beta hregSwap 0 j a b ha hb hD323 rw [pow_zero, one_mul] at hA hB324 refine ⟨r, hr, ?_⟩325 rw [surfaceToCechInput, LinearMap.comp_apply, Submodule.mkQ_apply, Submodule.Quotient.eq]326 exact Submodule.mem_prod.2 ⟨sub_mem_comm_iff.mp hA, sub_mem_comm_iff.mp hB⟩327 328/-! ### Tangent divisors and surface states -/329 330/-- The surface parameters `t` and `x` lie in the maximal ideal. -/331private theorem surface_parameters_mem_maximal (O R : Type) [CommRing O] [IsDomain O]332 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]333 (S : SurfaceData O R) :334 S.t ∈ IsLocalRing.maximalIdeal R ∧ S.x ∈ IsLocalRing.maximalIdeal R := by335 rw [← S.parameters]336 exact ⟨Ideal.subset_span (by simp), Ideal.subset_span (by simp)⟩337 338/-- An ideal with a tangent divisor of degree `d` has multiplicity exactly `d`. -/339theorem has_tangent_divisor_multiplicity (O R : Type) [CommRing O] [IsDomain O]340 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]341 (S : SurfaceData O R) (hreg : RegularParameterPair R S.t S.x) (J : Ideal R) (d : ℕ)342 (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R)) (hJ : HasTangentDivisor O R S J d Dv) :343 HasMultiplicity R J d := by344 obtain ⟨f, H, rfl, ⟨hH, hdeg, -, -⟩, hf⟩ := hJ345 obtain ⟨ht, hx⟩ := surface_parameters_mem_maximal O R S346 set m := IsLocalRing.maximalIdeal R with hm347 have hspan : Ideal.span ({S.t, S.x} : Set R) = m := S.parameters348 have hlift : tangentLift O R S d H ∈ m ^ d := by349 unfold tangentLift350 refine Ideal.sum_mem _ fun i _ => ?_351 have h1 : S.t ^ (d - i.val) * S.x ^ i.val ∈ m ^ d := by352 have : m ^ (d - i.val) * m ^ i.val ≤ m ^ d := by353 rw [← pow_add]; apply Ideal.pow_le_pow_right; omega354 exact this (Ideal.mul_mem_mul (Ideal.pow_mem_pow ht _) (Ideal.pow_mem_pow hx _))355 rw [mul_assoc]356 exact Ideal.mul_mem_left _ _ h1357 have hpow : m ^ (d+1) ≤ m ^ d := Ideal.pow_le_pow_right (by omega)358 refine ⟨?_, ?_⟩359 · rw [Ideal.span_singleton_le_iff_mem]360 have h2 : f = (f - tangentLift O R S d H) + tangentLift O R S d H := by ring361 rw [h2]; exact Ideal.add_mem _ (hpow hf) hlift362 · intro hle363 have hfm : f ∈ m ^ (d+1) := hle (Ideal.mem_span_singleton_self f)364 have hlm : tangentLift O R S d H ∈ m ^ (d+1) := by365 have h2 : tangentLift O R S d H = f - (f - tangentLift O R S d H) := by ring366 rw [h2]; exact Ideal.sub_mem _ hfm hf367 obtain ⟨i₀, hi₀⟩ : ∃ i : ℕ, H.coeff i ≠ 0 :=368 ⟨H.natDegree, Polynomial.leadingCoeff_ne_zero.mpr hH⟩369 have hi₀d : i₀ ≤ d := le_trans (Polynomial.le_natDegree_of_ne_zero hi₀) hdeg370 have : (Ideal.span ({S.t, S.x} : Set R)).IsMaximal := by rw [hspan]; infer_instance371 have key := homogeneous_form_not_mem_pow_succ R S.t S.x hreg d372 (fun i => residueRepresentative R (H.coeff i.val)) ⟨i₀, by omega⟩ (by373 rw [hspan, hm, ← IsLocalRing.residue_eq_zero_iff]374 have : IsLocalRing.residue R (residueRepresentative R (H.coeff i₀)) = H.coeff i₀ :=375 Function.rightInverse_invFun (IsLocalRing.residue_surjective) _376 rw [this]; exact hi₀)377 apply key378 rw [hspan]379 exact hlm380 381/-- Two degree-`d` forms in `t, x` whose coefficients agree modulo the maximal ideal differ by382an element of `𝔪 ^ (d + 1)`. -/383theorem initial_form_lift_independent (O R : Type) [CommRing O] [IsDomain O]384 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]385 (S : SurfaceData O R) (d : ℕ) (b c : Fin (d + 1) → R)386 (hbc : ∀ i, b i - c i ∈ IsLocalRing.maximalIdeal R) :387 (∑ i : Fin (d+1), b i*S.t^(d-i.val)*S.x^i.val) - (∑ i : Fin (d+1), c i*S.t^(d-i.val)*S.x^i.val)388 ∈ (IsLocalRing.maximalIdeal R)^(d+1) := by389 obtain ⟨ht, hx⟩ := surface_parameters_mem_maximal O R S390 rw [← Finset.sum_sub_distrib]391 refine Ideal.sum_mem _ fun i _ => ?_392 have hi : i.val ≤ d := Nat.lt_succ_iff.mp i.isLt393 have key : (b i - c i) * (S.t ^ (d - i.val) * S.x ^ i.val) ∈ (IsLocalRing.maximalIdeal R) ^394 (d+1) := by395 rw [pow_succ']396 refine Ideal.mul_mem_mul (hbc i) ?_397 have h := Ideal.mul_mem_mul (Ideal.pow_mem_pow ht (d - i.val)) (Ideal.pow_mem_pow hx i.val)398 rwa [← pow_add, Nat.sub_add_cancel hi] at h399 have e : b i * S.t ^ (d - i.val) * S.x ^ i.val - c i * S.t ^ (d - i.val) * S.x ^ i.val400 = (b i - c i) * (S.t ^ (d - i.val) * S.x ^ i.val) := by ring401 rw [e]; exact key402 403/-- Surface functions give closed Čech inputs: the twist-`0` Čech differential kills the image404of `surfaceToCechInput`. -/405private theorem surface_section_closed (R : Type) [CommRing R] (t x : R)406 (beta : BlowupRestriction R t x)407 (j : ℕ) (h : cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap408 (fullCechDifferential R t x beta 0)) (r : R) :409 finiteCechDifferential R t x beta 0 j h (surfaceToCechInput R t x j r) = 0 := by410 simp only [finiteCechDifferential, surfaceToCechInput, LinearMap.comp_apply, Submodule.mkQ_apply,411 Submodule.mapQ_apply]412 rw [Submodule.Quotient.mk_eq_zero]413 convert (cechOutputLattice R t x j).zero_mem414 simp only [fullCechDifferential, ringCechDifferential, IsScalarTower.coe_toAlgHom', pow_zero,415 one_mul, surfaceToChartPair, LinearMap.prod_apply, Function.prod_apply,416 Algebra.linearMap_apply, LinearMap.coe_mk, AddHom.coe_mk, AlgHom.commutes]417 rw [← IsScalarTower.algebraMap_apply, sub_self]418 419/-- Every ideal in the surface state set of a state is proper. -/420theorem surface_state_ideal_proper (O R : Type) [CommRing O] [IsDomain O]421 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]422 (S : SurfaceData O R) (s : State) (J : Ideal R) (hJ : J ∈ surfaceStateSet O R S s) :423 J ≠ ⊤ := by424 intro hT425 have h0 : ∀ y : R, idealContact R J y = 0 := by426 intro y427 unfold idealContact428 rw [hT, top_sup_eq]429 have : Subsingleton (R ⧸ (⊤ : Ideal R)) := Ideal.Quotient.subsingleton_iff.mpr rfl430 exact Module.length_eq_zero431 obtain ⟨_, hv, hs⟩ := hJ432 cases s with433 | single a c =>434 obtain ⟨_, _, hc⟩ := hs435 rw [h0] at hc436 have : c = 0 := by exact_mod_cast hc.symm437 exact absurd hv.2 (by omega)438 | crossing a b c h =>439 obtain ⟨_, _, hc, _⟩ := hs440 rw [h0] at hc441 have : c = 0 := by exact_mod_cast hc.symm442 exact absurd hv.2.2.1 (by omega)443 444/-- A generator of an ideal in a surface state set lies in the maximal ideal. -/445theorem surface_state_generator_mem_maximal (O R : Type) [CommRing O] [IsDomain O]446 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]447 (S : SurfaceData O R) (s : State) (J : Ideal R) (hJ : J ∈ surfaceStateSet O R S s) (f : R)448 (hf : J = Ideal.span {f}) :449 f ∈ IsLocalRing.maximalIdeal R := by450 rw [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff]451 exact fun hu => surface_state_ideal_proper O R S s J hJ (hf ▸ Ideal.span_singleton_eq_top.mpr hu)452 453/-- `(f + p * h) + (y) = (f) + (y)` whenever `y ∣ p`. -/454private theorem span_add_mul_sup_span_of_dvd {R : Type} [CommRing R] (f p h y : R) (hy : y ∣ p) :455 Ideal.span {f + p * h} ⊔ Ideal.span {y} = Ideal.span {f} ⊔ Ideal.span {y} := by456 obtain ⟨c, rfl⟩ := hy457 have hyI : ∀ I : Ideal R, y ∈ I ⊔ Ideal.span {y} :=458 fun I => Ideal.mem_sup_right (Ideal.mem_span_singleton_self y)459 have hmul : ∀ I : Ideal R, y * c * h ∈ I ⊔ Ideal.span {y} := fun I => by460 rw [mul_assoc]; exact Ideal.mul_mem_right _ _ (hyI I)461 apply le_antisymm462 · refine sup_le ?_ le_sup_right463 rw [Ideal.span_singleton_le_iff_mem]464 exact Ideal.add_mem _ (Ideal.mem_sup_left (Ideal.mem_span_singleton_self f)) (hmul _)465 · refine sup_le ?_ le_sup_right466 rw [Ideal.span_singleton_le_iff_mem]467 simpa using Ideal.sub_mem _ (Ideal.mem_sup_left (Ideal.mem_span_singleton_self (f + y * c * h)))468 (hmul _)469 470/-- Surface state sets are stable under vertical perturbation: if `(f)` is in the state set,471so is `(f + pi * h)`. -/472theorem surface_state_vertical_perturbation (O R : Type) [CommRing O] [IsDomain O]473 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]474 (S : SurfaceData O R) (s : State) (f h : R) (hf : Ideal.span {f} ∈ surfaceStateSet O R S s) :475 Ideal.span {f + algebraMap O R S.pi * h} ∈ surfaceStateSet O R S s := by476 have ht : S.t ∣ algebraMap O R S.pi := by477 rw [S.vertical]478 obtain ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero S.a_pos.ne'479 rw [hk, pow_succ]480 exact ⟨S.unit * S.t ^ k * S.x ^ S.b, by ring⟩481 obtain ⟨-, hv, hm⟩ := hf482 refine ⟨⟨_, rfl⟩, hv, ?_⟩483 cases s with484 | single a c =>485 obtain ⟨h1, h2, h3⟩ := hm486 refine ⟨h1, h2, ?_⟩487 unfold idealContact at *488 rw [span_add_mul_sup_span_of_dvd _ _ _ _ ht]; exact h3489 | crossing a b c e =>490 obtain ⟨h1, h2, h3, h4⟩ := hm491 have hx : S.x ∣ algebraMap O R S.pi := by492 rw [S.vertical]493 have hb : 0 < S.b := h2 ▸ hv.2.1494 obtain ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero hb.ne'495 rw [hk, pow_succ]496 exact ⟨S.unit * S.t ^ S.a * S.x ^ k, by ring⟩497 refine ⟨h1, h2, ?_, ?_⟩498 · unfold idealContact at *499 rw [span_add_mul_sup_span_of_dvd _ _ _ _ ht]; exact h3500 · unfold idealContact at *501 rw [span_add_mul_sup_span_of_dvd _ _ _ _ hx]; exact h4502 503/-! ### The surface-to-Čech comparison -/504 505/-- Membership in the kernel of the surface-to-Čech map, chart by chart. -/506private theorem mem_ker_surfaceToCechInput_iff (R : Type) [CommRing R] (t x : R) (j : ℕ) (r : R) :507 r ∈ LinearMap.ker (surfaceToCechInput R t x j) ↔508 chartBase R t x r ∈ (chartExceptional R t x)^j ∧509 chartBase R x t r ∈ (chartExceptional R x t)^j := by510 rw [LinearMap.mem_ker]511 unfold surfaceToCechInput512 rw [LinearMap.comp_apply, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]513 rfl514 515/-- `(t, x)` maps into the exceptional ideal of the chart `R[x/t]`. -/516private theorem map_span_le_chartExceptional (R : Type) [CommRing R] (t x : R) :517 Ideal.map (chartBase R t x) (Ideal.span {t, x}) ≤ chartExceptional R t x := by518 rw [Ideal.map_span, Ideal.span_le]519 rintro _ ⟨y, hy, rfl⟩520 rcases hy with rfl | rfl521 · exact Ideal.subset_span rfl522 · rw [← blowup_chart_relation]523 exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)524 525/-- `(t, x) ^ j` maps into the `j`-th power of the exceptional ideal. -/526private theorem chartBase_mem_chartExceptional_pow (R : Type) [CommRing R] (t x : R) (j : ℕ) (r : R)527 (hr : r ∈ (Ideal.span {t, x}) ^ j) : chartBase R t x r ∈ (chartExceptional R t x)^j := by528 have h1 : chartBase R t x r ∈ Ideal.map (chartBase R t x) ((Ideal.span {t, x})^j) :=529 Ideal.mem_map_of_mem _ hr530 rw [Ideal.map_pow] at h1531 exact Ideal.pow_right_mono (map_span_le_chartExceptional R t x) j h1532 533/-- If `r ∈ (t, x) ^ j` and its image lies in the `(j + 1)`-st power of the exceptional ideal,534then `r ∈ (t, x) ^ (j + 1)`. -/535private theorem mem_span_pow_succ_of_chartBase_mem (R : Type) [CommRing R] (t x : R)536 (hreg : RegularParameterPair R t x) (j : ℕ)537 (r : R) (hr : r ∈ (Ideal.span {t, x}) ^ j)538 (hA : chartBase R t x r ∈ (chartExceptional R t x) ^ (j + 1)) :539 r ∈ (Ideal.span {t, x})^(j+1) := by540 obtain ⟨c, rfl⟩ := monomial_span_pow R t x j r hr541 set T := chartBase R t x t542 set Z := chartSlope R t x543 set P : BlowupChart R t x := ∑ i : Fin (j+1), chartBase R t x (c i) * Z ^ i.val with hP544 have hrel : T * Z = chartBase R t x x := blowup_chart_relation R t x545 have himg : chartBase R t x (∑ i : Fin (j+1), c i * t^(j - i.val) * x^i.val) = T^j * P := by546 rw [hP, map_sum, Finset.mul_sum]547 refine Finset.sum_congr rfl fun i _ => ?_548 have hi : j - i.val + i.val = j := Nat.sub_add_cancel (Nat.lt_succ_iff.mp i.isLt)549 rw [map_mul, map_mul, map_pow, map_pow, ← hrel, mul_pow]550 rw [← pow_sub_mul_pow T (Nat.lt_succ_iff.mp i.isLt)]551 ring552 rw [himg, chartExceptional, Ideal.span_singleton_pow, Ideal.mem_span_singleton'] at hA553 obtain ⟨q, hq⟩ := hA554 have hreg' : IsLeftRegular T := blowup_exceptional_parameter_regular R t x hreg555 have hPq : P = T * q := by556 apply hreg'.pow j557 simp only558 rw [← hq]; ring559 have hmk : Ideal.Quotient.mk (exceptionalLevelIdeal R t x 1) P = 0 := by560 rw [Ideal.Quotient.eq_zero_iff_mem, exceptionalLevelIdeal, pow_one, hPq]561 exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)562 obtain ⟨e, he1, he2⟩ := exceptional_chart_is_affine_line R t x563 have hmk' : Ideal.Quotient.mk (exceptionalLevelIdeal R t x 1) P =564 ∑ i : Fin (j+1), levelBase R t x 1 (c i) * levelSlope R t x 1 ^ i.val := by565 rw [hP, map_sum]566 rfl567 have hpoly : (∑ i : Fin (j+1), Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) (c i)) *568 Polynomial.X ^ i.val) = 0 := by569 rw [← map_zero e, ← hmk, hmk', map_sum]570 refine Finset.sum_congr rfl fun i _ => ?_571 rw [map_mul, map_pow, he1, he2]572 have hc : ∀ i : Fin (j+1), c i ∈ Ideal.span {t, x} := by573 intro i574 have := congrArg (fun p => Polynomial.coeff p i.val) hpoly575 simp only [Polynomial.finsetSum_coeff, Polynomial.coeff_C_mul_X_pow, Polynomial.coeff_zero]576 at this577 rw [Finset.sum_eq_single i] at this578 · simpa [Ideal.Quotient.eq_zero_iff_mem] using this579 · intro b _ hb580 rw [if_neg]581 intro h; exact hb (Fin.ext h.symm)582 · simp583 refine Ideal.sum_mem _ fun i _ => ?_584 have hi : j - i.val + i.val = j := Nat.sub_add_cancel (Nat.lt_succ_iff.mp i.isLt)585 have hmon : t^(j - i.val) * x^i.val ∈ (Ideal.span {t, x})^j := by586 have h := Ideal.mul_mem_mul587 (Ideal.pow_mem_pow (Ideal.subset_span (by simp) : t ∈ Ideal.span {t, x}) (j - i.val))588 (Ideal.pow_mem_pow (Ideal.subset_span (by simp) : x ∈ Ideal.span {t, x}) i.val)589 rwa [← pow_add, hi] at h590 rw [mul_assoc, pow_succ']591 exact Ideal.mul_mem_mul (hc i) hmon592 593/-- The kernel of the surface-to-Čech map at level `j` is `(t, x) ^ j`. -/594theorem surface_to_cech_kernel (R : Type) [CommRing R] (t x : R) (hreg : RegularParameterPair R t x)595 (j : ℕ) :596 LinearMap.ker (surfaceToCechInput R t x j) = (Ideal.span {t,x})^j := by597 ext r598 rw [mem_ker_surfaceToCechInput_iff]599 constructor600 · rintro ⟨hA, -⟩601 induction j generalizing r with602 | zero => simp603 | succ j ih =>604 exact mem_span_pow_succ_of_chartBase_mem R t x hreg j r605 (ih r (Ideal.pow_le_pow_right (Nat.le_succ j) hA)) hA606 · intro hr607 refine ⟨chartBase_mem_chartExceptional_pow R t x j r hr, ?_⟩608 rw [Set.pair_comm] at hr609 exact chartBase_mem_chartExceptional_pow R x t j r hr610 611/-- A surface function whose Čech images are the glued generator pairs lies in `(t, x) ^ d`. -/612theorem glued_function_order (R : Type) [CommRing R] (t x : R) (beta : BlowupRestriction R t x)613 (d : ℕ) (G : GluedGenerators R t x beta d) (hreg : RegularParameterPair R t x) (f : R)614 (hf : ∀ j : ℕ, surfaceToCechInput R t x j f = (cechInputLattice R t x j).mkQ615 (gluedFunctionPair R t x G j)) :616 f ∈ (Ideal.span {t,x})^d := by617 rw [← surface_to_cech_kernel R t x hreg d, LinearMap.mem_ker, hf d,618 Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]619 unfold cechInputLattice gluedFunctionPair620 rw [Submodule.mem_prod]621 exact ⟨Ideal.mul_mem_right _ _ (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self _) d),622 Ideal.mul_mem_right _ _ (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self _) d)⟩623 624/-- Telescoping lemma used to identify the initial form of a glued function. -/625private theorem sub_mem_span_of_pow_mul_sub_mem {A : Type} [CommRing A] (T : A)626 (hinj : Function.Injective (fun a : A => T * a))627 (L : ℕ → A) (hL : ∀ j : ℕ, L (j+1) - L j ∈ (Ideal.span {T})^j) (d : ℕ) (P : A)628 (h : T^d * P - T^d * L (d+1) ∈ (Ideal.span {T})^(d+1)) :629 L 1 - P ∈ Ideal.span {T} := by630 have hinjd : ∀ n : ℕ, IsLeftRegular (T ^ n) := fun n => IsLeftRegular.pow n hinj631 have htel : ∀ k : ℕ, L (k+1) - L 1 ∈ Ideal.span {T} := by632 intro k633 induction k with634 | zero => simp635 | succ k ih =>636 have := Ideal.pow_le_self (Nat.succ_ne_zero k) (hL (k+1))637 have e : L (k+1+1) - L 1 = (L (k+1+1) - L (k+1)) + (L (k+1) - L 1) := by ring638 rw [e]; exact Ideal.add_mem _ this ih639 rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton'] at h640 obtain ⟨y, hy⟩ := h641 have hPL : P - L (d+1) = T * y := by642 apply hinjd d643 simp only644 rw [mul_sub, ← hy]; ring645 have h1 : P - L (d+1) ∈ Ideal.span {T} := by646 rw [hPL]; exact Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self T)647 have e : L 1 - P = -((P - L (d+1)) + (L (d+1) - L 1)) := by ring648 rw [e]; exact (Ideal.neg_mem_iff _).mpr (Ideal.add_mem _ h1 (htel d))649 650/-- The glued function is a degree-`d` form `∑ cᵢ t^(d-i) xⁱ` whose dehomogenizations agree with651the first glued generators modulo the exceptional ideals of the two charts. -/652theorem glued_function_initial_form (R : Type) [CommRing R] (t x : R)653 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d)654 (hreg : RegularParameterPair R t x) (hregSwap : RegularParameterPair R x t) (f : R)655 (hf : ∀ j : ℕ, surfaceToCechInput R t x j f = (cechInputLattice R t x j).mkQ656 (gluedFunctionPair R t x G j)) :657 ∃ c : Fin (d+1) → R, f = ∑ i : Fin (d+1), c i * t^(d - i.val) * x^i.val ∧ G.left 1 - ∑ i : Fin658 (d+1), algebraMap R (BlowupChart R t x) (c i) * (chartSlope R t x)^i.val ∈ chartExceptional R659 t x ∧ G.right 1 - ∑ i : Fin (d+1), algebraMap R (BlowupChart R x t) (c i) *660 (chartSlope R x t)^(d - i.val) ∈ chartExceptional R x t := by661 obtain ⟨c, hc⟩ := monomial_span_pow R t x d f662 (glued_function_order R t x beta d G hreg f hf)663 refine ⟨c, hc, ?_, ?_⟩664 · have hA : ∀ r : R, algebraMap R (BlowupChart R t x) r = chartBase R t x r := fun _ => rfl665 have hrel := blowup_chart_relation R t x666 have hmap : algebraMap R (BlowupChart R t x) f = (chartBase R t x t)^d *667 ∑ i : Fin (d+1), algebraMap R (BlowupChart R t x) (c i) * (chartSlope R t x)^i.val := by668 rw [hc, map_sum, Finset.mul_sum]669 refine Finset.sum_congr rfl (fun i _ => ?_)670 have hi : i.val + (d - i.val) = d := by omega671 simp only [map_mul, map_pow, hA, ← hrel]672 rw [show (chartBase R t x t)^d = (chartBase R t x t)^i.val * (chartBase R t x t)^(d - i.val)673 from by rw [← pow_add, hi]]674 ring675 have h := glued_function_left_chart R t x beta d G f hf (d+1)676 rw [hmap] at h677 exact sub_mem_span_of_pow_mul_sub_mem _ (blowup_exceptional_parameter_regular R t x hreg)678 G.left G.left_compat d _ h679 · have hA : ∀ r : R, algebraMap R (BlowupChart R x t) r = chartBase R x t r := fun _ => rfl680 have hrel := blowup_chart_relation R x t681 have hmap : algebraMap R (BlowupChart R x t) f = (chartBase R x t x)^d *682 ∑ i : Fin (d+1), algebraMap R (BlowupChart R x t) (c i) *683 (chartSlope R x t)^(d - i.val) := by684 rw [hc, map_sum, Finset.mul_sum]685 refine Finset.sum_congr rfl (fun i _ => ?_)686 have hi : (d - i.val) + i.val = d := by omega687 simp only [map_mul, map_pow, hA, ← hrel]688 rw [show (chartBase R x t x)^d = (chartBase R x t x)^(d - i.val) * (chartBase R x t x)^i.val689 from by rw [← pow_add, hi]]690 ring691 have h := glued_function_right_chart R t x beta d G f hf (d+1)692 rw [hmap] at h693 exact sub_mem_span_of_pow_mul_sub_mem _ (blowup_exceptional_parameter_regular R x t hregSwap)694 G.right G.right_compat d _ h695 696/-- For `(t, x)`-adically complete `R`, the map from `R` to compatible Čech threads is injective. -/697theorem surface_threads_injective (R : Type) [CommRing R] (t x : R)Lemma 4.2698 [IsAdicComplete (Ideal.span {t,x}) R] (hreg : RegularParameterPair R t x) :699 Function.Injective (surfaceThreads R t x) := by700 rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff]701 intro r hr702 rw [LinearMap.mem_ker] at hr703 have hj : ∀ j : ℕ, r ∈ (Ideal.span {t,x})^j := by704 intro j705 rw [← surface_to_cech_kernel R t x hreg j, LinearMap.mem_ker]706 exact (congrArg (cechInputThreadLinear R t x j) hr).trans (map_zero _)707 have h := IsHausdorff.haus (IsAdicComplete.toIsHausdorff (I := Ideal.span {t,x}) (M := R)) r708 (fun n => by709 rw [SModEq.zero, smul_eq_mul, Ideal.mul_top]710 exact hj n)711 simpa using h712 713/-- Exactness at level `j`: the image of the surface-to-Čech map is the kernel of the twist-`0`714Čech differential. -/715theorem surface_to_cech_range (R : Type) [CommRing R] (t x : R) (hreg : RegularParameterPair R t x)716 (hregSwap : RegularParameterPair R x t) (beta : BlowupRestriction R t x) (j : ℕ)717 (h : cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap718 (fullCechDifferential R t x beta 0)) :719 LinearMap.range (surfaceToCechInput R t x j) = LinearMap.ker720 (finiteCechDifferential R t x beta 0 j h) := by721 have key : ∀ k (w : CechLevelInput R t x k),722 finiteCechDifferential R t x beta 0 k723 (actual_cech_preserves_exceptional_lattices R t x beta 0 k) w = 0 →724 w ∈ LinearMap.range (surfaceToCechInput R t x k) := by725 intro k726 induction k with727 | zero =>728 intro w _729 refine ⟨0, ?_⟩730 induction w using Submodule.Quotient.induction_on with731 | H z =>732 rw [map_zero, eq_comm, Submodule.Quotient.mk_eq_zero]733 simp only [cechInputLattice]734 refine ⟨?_, ?_⟩735 · change z.1 ∈ (1 : Ideal (BlowupChart R t x))736 exact (Ideal.one_eq_top (R := BlowupChart R _ _)) ▸ Submodule.mem_top737 · change z.2 ∈ (1 : Ideal (BlowupChart R x t))738 exact (Ideal.one_eq_top (R := BlowupChart R _ _)) ▸ Submodule.mem_top739 | succ k ih =>740 intro w hw741 have hcomm := actual_cech_differentials_commute_with_reduction R t x beta 0 k742 (actual_cech_preserves_exceptional_lattices R t x beta 0 (k+1))743 (actual_cech_preserves_exceptional_lattices R t x beta 0 k)744 have hw' : finiteCechDifferential R t x beta 0 k745 (actual_cech_preserves_exceptional_lattices R t x beta 0 k)746 (cechInputReduction R t x k w) = 0 := by747 have := congrArg (fun f => f w) hcomm748 simp only [LinearMap.comp_apply] at this749 rw [← this, hw, map_zero]750 obtain ⟨r, hr⟩ := ih _ hw'751 have hred : cechInputReduction R t x k (surfaceToCechInput R t x (k+1) r) =752 surfaceToCechInput R t x k r := rfl753 obtain ⟨r', -, hr'⟩ := surface_layer_kernel_lift R t x hreg hregSwap beta k754 (actual_cech_preserves_exceptional_lattices R t x beta 0 (k+1))755 (w - surfaceToCechInput R t x (k+1) r)756 (by rw [map_sub, hw, surface_section_closed, sub_zero])757 (by rw [map_sub, hred, hr, sub_self])758 exact ⟨r + r', by rw [map_add, hr', add_sub_cancel]⟩759 ext w760 exact ⟨by rintro ⟨r, rfl⟩; exact surface_section_closed R t x beta j h r, key j w⟩761 762private theorem sub_mem_span_sup_of_sub_mem {A : Type} [CommRing A] (g a p s : A) (K : Ideal A)763 (h : s - (p - g * a) ∈ K) : p - s ∈ Ideal.span {g} ⊔ K := by764 rw [show p - s = g * a + -(s - (p - g * a)) by ring]765 exact Submodule.add_mem_sup (Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self _))766 (neg_mem h)767 768/-- If the twist-`d` Čech differential preserves the level-`j` lattices, so does the twist-`0`769one: the twist `(x/t)⁻ᵈ` is a unit modulo the overlap exceptional ideal. -/770private theorem cechInputLattice_le_comap_twist_zero (R : Type) [CommRing R] (t x : R)771 (beta : BlowupRestriction R t x) (d j : ℕ)772 (h : cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap773 (fullCechDifferential R t x beta d)) :774 cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap775 (fullCechDifferential R t x beta 0) := by776 set u := IsLocalization.Away.invSelf (chartSlope R t x) (S := BlowupOverlap R t x)777 let π := Ideal.Quotient.mk ((Ideal.span {overlapException R t x}) ^ j)778 have hπ : ∀ w, w ∈ cechOutputLattice R t x j ↔ π w = 0 :=779 fun w => (Ideal.Quotient.eq_zero_iff_mem).symm780 have hfc : ∀ (d' : ℕ) (a : BlowupChart R t x) (b : BlowupChart R x t),781 fullCechDifferential R t x beta d' (a, b) =782 algebraMap _ (BlowupOverlap R t x) a - u ^ d' * beta.right b := fun _ _ _ => rfl783 have hpow : (π (overlapSlope R t x) * π u) ^ d = 1 := by784 rw [← map_mul, show overlapSlope R t x * u = 1 from IsLocalization.Away.mul_invSelf _, map_one,785 one_pow]786 rintro ⟨a, b⟩ ⟨ha, hb⟩787 have hA' := (hπ _).1 (h (show (a, 0) ∈ cechInputLattice R t x j from ⟨ha, zero_mem _⟩))788 have hB' := (hπ _).1 (h (show (0, b) ∈ cechInputLattice R t x j from ⟨zero_mem _, hb⟩))789 change _ ∈ cechOutputLattice R t x j790 rw [hπ, hfc]791 rw [hfc] at hA' hB'792 simp only [map_sub, map_mul, map_pow, map_zero, map_neg, mul_zero, sub_zero, zero_sub,793 pow_zero, one_mul] at hA' hB' ⊢794 linear_combination hA' + (π (overlapSlope R t x)) ^ d * hB' + π (beta.right b) * hpow795 796/-- The connecting class of a curve section vanishes iff the section differs from the image of797a surface function by an element of the curve ideal lattice. -/798theorem curve_section_connecting_class_zero_iff (R : Type) [CommRing R] (t x : R)799 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d)800 (hreg : RegularParameterPair R t x) (hregSwap : RegularParameterPair R x t) (j : ℕ)801 (h : cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap802 (fullCechDifferential R t x beta d))803 (hregF : Function.Injective804 (fun c : BlowupOverlap R t x ⧸ (Ideal.span {overlapException R t x})^j => Ideal.Quotient.mk805 ((Ideal.span {overlapException R t x})^j)806 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j)) * c))807 (p : BlowupChart R t x × BlowupChart R x t) (hp : p ∈ curveSections R t x beta G j)808 (c : BlowupOverlap R t x)809 (hc : fullCechDifferential R t x beta 0 p -810 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j) * c ∈811 (Ideal.span {overlapException R t x})^j) :812 (LinearMap.range (finiteCechDifferential R t x beta d j h)).mkQ813 ((cechOutputLattice R t x j).mkQ c) = 0 ↔ ∃ r : R, p - surfaceToChartPair R t x r ∈814 curveIdealLattice R t x beta G j := by815 set E := (Ideal.span {overlapException R t x})^j with hE816 set α := algebraMap (BlowupChart R t x) (BlowupOverlap R t x) with hα817 set u := IsLocalization.Away.invSelf (chartSlope R t x) (S := BlowupOverlap R t x) with hu818 have hmemE : ∀ w, w ∈ cechOutputLattice R t x j ↔ w ∈ E := fun _ => Iff.rfl819 have hfc : ∀ (d' : ℕ) (a : BlowupChart R t x) (b : BlowupChart R x t),820 fullCechDifferential R t x beta d' (a, b) = α a - u ^ d' * beta.right b := fun _ _ _ => rfl821 let π := Ideal.Quotient.mk E822 have hπ : ∀ w, w ∈ E ↔ π w = 0 := fun w => (Ideal.Quotient.eq_zero_iff_mem).symm823 have hpow : (π (overlapSlope R t x) * π u) ^ d = 1 := by824 rw [← map_mul, show overlapSlope R t x * u = 1 from IsLocalization.Away.mul_invSelf _, map_one,825 one_pow]826 -- u^d α F_A ≡ β F_B827 have hov : π (u ^ d * α (G.left j)) = π (beta.right (G.right j)) := by828 have h1 := (hπ _).1 (G.overlap j)829 simp only [map_sub, map_mul, map_pow] at h1 ⊢830 rw [← hα] at h1831 linear_combination (π u) ^ d * h1 + π (beta.right (G.right j)) * hpow832 have h0 := cechInputLattice_le_comap_twist_zero R t x beta d j h833 obtain ⟨p1, p2⟩ := p834 have hc' := (hπ _).1 hc835 rw [hfc] at hc'836 simp only [map_sub, map_mul, pow_zero, one_mul] at hc'837 have hαr : ∀ r : R, α (algebraMap R _ r) = algebraMap R (BlowupOverlap R t x) r := fun r =>838 (IsScalarTower.algebraMap_apply R (BlowupChart R t x) (BlowupOverlap R t x) r).symm839 have hβr : ∀ r : R, beta.right (algebraMap R _ r) = algebraMap R (BlowupOverlap R t x) r :=840 fun r => beta.right.commutes r841 simp only [map_mul, map_pow] at hov842 constructor843 · intro hz844 rw [Submodule.mkQ_apply, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at hz845 obtain ⟨q, hq⟩ := hz846 obtain ⟨⟨a', b'⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ q847 rw [finiteCechDifferential, Submodule.mapQ_apply, Submodule.Quotient.eq, hmemE, hπ, hfc] at hq848 simp only [map_sub, map_mul, map_pow] at hq849 have hker : (Submodule.Quotient.mk (p1 - G.left j * a', p2 - G.right j * b') :850 CechLevelInput R t x j) ∈ LinearMap.ker (finiteCechDifferential R t x beta 0 j h0) := by851 rw [LinearMap.mem_ker, finiteCechDifferential, Submodule.mapQ_apply,852 Submodule.Quotient.mk_eq_zero, hmemE, hπ, hfc]853 simp only [map_sub, map_mul, pow_zero, one_mul]854 linear_combination hc' - π (α (G.left j)) * hq - π (beta.right b') * hov855 rw [← surface_to_cech_range R t x hreg hregSwap beta j h0] at hker856 obtain ⟨r, hr⟩ := hker857 rw [surfaceToCechInput, LinearMap.comp_apply, Submodule.mkQ_apply, Submodule.Quotient.eq] at hr858 obtain ⟨hr1, hr2⟩ := hr859 exact ⟨r, sub_mem_span_sup_of_sub_mem _ _ _ _ _ hr1, sub_mem_span_sup_of_sub_mem _ _ _ _ _ hr2⟩860 · rintro ⟨r, h1, h2⟩861 change p1 - algebraMap R _ r ∈ leftCurveIdeal R t x beta G j at h1862 change p2 - algebraMap R _ r ∈ rightCurveIdeal R t x beta G j at h2863 obtain ⟨y, hy, z, hz, hyz⟩ := Submodule.mem_sup.1 h1864 obtain ⟨y', hy', z', hz', hyz'⟩ := Submodule.mem_sup.1 h2865 obtain ⟨a', rfl⟩ := Ideal.mem_span_singleton'.1 hy866 obtain ⟨b', rfl⟩ := Ideal.mem_span_singleton'.1 hy'867 have hzz := (hπ _).1 ((hmemE _).1 (h0 (show (z, z') ∈ cechInputLattice R t x j from ⟨hz, hz'⟩)))868 rw [hfc] at hzz869 simp only [map_sub, pow_zero, one_mul] at hzz870 have ep1 : p1 = a' * G.left j + z + algebraMap R _ r := by linear_combination -hyz871 have ep2 : p2 = b' * G.right j + z' + algebraMap R _ r := by linear_combination -hyz'872 rw [ep1, ep2] at hc'873 simp only [map_add, map_mul, hαr, hβr] at hc'874 rw [Submodule.mkQ_apply, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]875 refine ⟨Submodule.Quotient.mk (a', b'), ?_⟩876 rw [finiteCechDifferential, Submodule.mapQ_apply, Submodule.Quotient.eq, hmemE, hπ, hfc]877 have key : π c = π (α a' - u ^ d * beta.right b') := by878 apply hregF879 change π (α (G.left j)) * π c = π (α (G.left j)) * π (α a' - u ^ d * beta.right b')880 simp only [map_sub, map_mul, map_pow]881 linear_combination -hc' + hzz + π (beta.right b') * hov882 rw [map_sub, key, sub_self]883 884/-- For complete `R`, the image of `R` in Čech threads is the intersection of the kernels of the885levelwise twist-`0` Čech differentials. -/886theorem surface_threads_range (R : Type) [CommRing R] (t x : R)Lemma 4.1Lemma 4.2Appendix A887 [IsAdicComplete (Ideal.span {t,x}) R] (hreg : RegularParameterPair R t x)888 (hregSwap : RegularParameterPair R x t) (beta : BlowupRestriction R t x)889 (hpres : ∀ j : ℕ, cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap890 (fullCechDifferential R t x beta 0)) :891 LinearMap.range (surfaceThreads R t x) = ⨅ j : ℕ, LinearMap.ker892 ((finiteCechDifferential R t x beta 0 j (hpres j)).comp (cechInputThreadLinear R t x j)) := by893 set I : Ideal R := Ideal.span {t,x}894 -- key: equal images iff difference in I^j895 have hEq : ∀ (j : ℕ) (r s : R), surfaceToCechInput R t x j r = surfaceToCechInput R t x j s ↔896 r - s ∈ I ^ j := by897 intro j r s898 rw [← sub_eq_zero, ← map_sub, ← LinearMap.mem_ker, surface_to_cech_kernel R t x hreg j]899 have hcoord : ∀ (r : R) (j : ℕ), cechInputThreadLinear R t x j (surfaceThreads R t x r) =900 surfaceToCechInput R t x j r := fun _ _ => rfl901 apply le_antisymm902 · rintro _ ⟨r, rfl⟩903 rw [Submodule.mem_iInf]904 intro j905 rw [LinearMap.mem_ker, LinearMap.comp_apply, hcoord]906 exact surface_section_closed R t x beta j (hpres j) r907 · intro a ha908 rw [Submodule.mem_iInf] at ha909 have hr : ∀ j, ∃ r : R, surfaceToCechInput R t x j r = cechInputThreadLinear R t x j a := by910 intro j911 have := ha j912 rwa [LinearMap.mem_ker, LinearMap.comp_apply, ← LinearMap.mem_ker,913 ← surface_to_cech_range R t x hreg hregSwap beta j (hpres j)] at this914 choose f hf using hr915 have hcompat : ∀ j, cechInputReduction R t x j (cechInputThreadLinear R t x (j+1) a) =916 cechInputThreadLinear R t x j a :=917 fun j => (sub_eq_zero.mp (congrFun (LinearMap.mem_ker.mp a.2) j :)).symm918 have hstep : ∀ j, f (j+1) - f j ∈ I ^ j := by919 intro j920 rw [← hEq, hf j, ← hcompat j, ← hf (j+1)]921 rfl922 have hcauchy : ∀ m n, m ≤ n → f n - f m ∈ I ^ m := by923 intro m n hmn924 induction n, hmn using Nat.le_induction with925 | base => simp926 | succ n hmn ih => simpa using Submodule.add_mem _ (Ideal.pow_le_pow_right hmn (hstep n)) ih927 obtain ⟨L, hL⟩ := IsPrecomplete.prec (IsAdicComplete.toIsPrecomplete (I := I) (M := R))928 (f := f) (fun {m n} hmn => by929 rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top, ← neg_mem_iff, neg_sub]930 exact hcauchy m n hmn)931 refine ⟨L, ?_⟩932 apply Subtype.ext933 funext j934 change surfaceToCechInput R t x j L = cechInputThreadLinear R t x j a935 rw [← hf j, hEq]936 have := hL j937 rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top] at this938 rwa [← neg_mem_iff, neg_sub]939 940/-- For complete `R`, there is a unique surface function whose Čech images are the glued941generator pairs at every level. -/942theorem glued_function_exists_unique (R : Type) [CommRing R] (t x : R)Lemma 4.2943 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d)944 [IsAdicComplete (Ideal.span {t,x}) R] (hreg : RegularParameterPair R t x)945 (hregSwap : RegularParameterPair R x t) :946 ∃! f : R, ∀ j : ℕ, surfaceToCechInput R t x j f = (cechInputLattice R t x j).mkQ947 (gluedFunctionPair R t x G j) := by948 let v : ∀ j, CechLevelInput R t x j :=949 fun j => (cechInputLattice R t x j).mkQ (gluedFunctionPair R t x G j)950 have hv : v ∈ towerThreads R (fun j => CechLevelInput R t x j) (cechInputReduction R t x) := by951 rw [towerThreads, LinearMap.mem_ker]952 funext j953 change v j - cechInputReduction R t x j (v (j+1)) = 0954 rw [sub_eq_zero]955 exact (glued_function_pair_compatible R t x beta d G j).symm956 let a : CechInputThreads R t x := ⟨v, hv⟩957 have hpres := fun j => actual_cech_preserves_exceptional_lattices R t x beta 0 j958 have ha : a ∈ LinearMap.range (surfaceThreads R t x) := by959 rw [surface_threads_range R t x hreg hregSwap beta hpres, Submodule.mem_iInf]960 intro j961 rw [LinearMap.mem_ker, LinearMap.comp_apply]962 exact glued_function_pair_closed R t x beta d G j (hpres j)963 obtain ⟨f, hf⟩ := ha964 refine ⟨f, fun j => ?_, fun g hg => ?_⟩965 · exact congrArg (fun b => cechInputThreadLinear R t x j b) hf966 · apply surface_threads_injective R t x hreg967 rw [hf]968 apply Subtype.ext969 funext j970 exact hg j971 972/-- Surface functions map linearly to the curve order limit, through constant curve threads. -/973theorem surface_to_curve_limit_exists (R : Type) [CommRing R] (t x : R)974 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d) :975 ∃ σ : R →ₗ[R] CurveOrderLimit R t x beta G, ∀ r : R, ∃ p : curveThreads R t x beta G, σ r =976 curveLimitMk R t x beta G p ∧ ∀ j : ℕ, p.val j = surfaceToChartPair R t x r := by977 have hmem : ∀ r : R, (fun _ : ℕ => surfaceToChartPair R t x r) ∈ curveThreads R t x beta G := by978 intro r979 refine ⟨?_, ?_⟩980 · rw [SetLike.mem_coe, Submodule.mem_pi]981 intro j _982 rw [curveSections, Submodule.mem_comap]983 have : fullCechDifferential R t x beta 0 (surfaceToChartPair R t x r) = 0 := by984 simp [fullCechDifferential, surfaceToChartPair, ringCechDifferential, ←985 IsScalarTower.algebraMap_apply]986 rw [this]; exact Submodule.zero_mem _987 · rw [SetLike.mem_coe, Submodule.mem_comap]988 have : towerDelta R (fun _ => ChartPair R t x) (fun _ => LinearMap.id)989 (fun _ : ℕ => surfaceToChartPair R t x r) = 0 := by990 ext j <;> simp [towerDelta]991 rw [this]; exact Submodule.zero_mem _992 let f : R →ₗ[R] curveThreads R t x beta G :=993 LinearMap.codRestrict _ (LinearMap.pi fun _ : ℕ => surfaceToChartPair R t x) hmem994 refine ⟨(curveLimitMk R t x beta G).comp f, fun r => ⟨f r, rfl, fun j => rfl⟩⟩995 996/-! ### Fixed tangent cells in coordinate charts -/997 998/-- The image of the uniformizer `pi` in `R` is nonzero and lies in the maximal ideal. -/999theorem surface_vertical_parameter (O R : Type) [CommRing O] [IsDomain O]1000 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]1001 (S : SurfaceData O R) :1002 algebraMap O R S.pi ≠ 0 ∧ algebraMap O R S.pi ∈ IsLocalRing.maximalIdeal R := by1003 refine ⟨?_, ?_⟩1004 · intro h1005 apply S.pi_irreducible.ne_zero1006 apply S.base_injective1007 rw [h, map_zero]1008 · have ht : S.t ∈ IsLocalRing.maximalIdeal R := by1009 rw [← S.parameters]1010 exact Ideal.subset_span (by simp)1011 rw [S.vertical]1012 apply Ideal.mul_mem_right1013 apply Ideal.mul_mem_left1014 exact Ideal.pow_mem_of_mem _ ht _ S.a_pos1015 1016/-- Perturbing a generator by a multiple of `pi ^ M` with `M ≥ d + 1` does not change its tangent1017divisor of degree `d`. -/1018private theorem surface_tangent_jet_small_perturbation (O R : Type) [CommRing O] [IsDomain O]1019 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]1020 (S : SurfaceData O R) (d M : ℕ) (hM : d + 1 ≤ M) (f h : R)1021 (H : Polynomial (IsLocalRing.ResidueField R))1022 (D : ExceptionalDivisor (IsLocalRing.ResidueField R))1023 (hD : HasHomogeneousDivisor (IsLocalRing.ResidueField R) d H D)1024 (hjet : f - tangentLift O R S d H ∈ (IsLocalRing.maximalIdeal R) ^ (d + 1)) :1025 HasTangentDivisor O R S (Ideal.span {f + algebraMap O R S.pi^M * h}) d D := by1026 refine ⟨f + algebraMap O R S.pi^M * h, H, rfl, hD, ?_⟩1027 have hpi := (surface_vertical_parameter O R S).21028 have h1 : algebraMap O R S.pi ^ M * h ∈ (IsLocalRing.maximalIdeal R)^(d+1) := by1029 apply Ideal.mul_mem_right1030 exact Ideal.pow_le_pow_right hM (Ideal.pow_mem_pow hpi M)1031 have : f + algebraMap O R S.pi ^ M * h - tangentLift O R S d H1032 = (f - tangentLift O R S d H) + algebraMap O R S.pi ^ M * h := by ring1033 rw [this]1034 exact Ideal.add_mem _ hjet h11035 1036/-- `coordinateLift` is additive. -/1037private theorem coordinateLift_add {O R : Type} [CommRing O] [CommRing R] [Algebra O R] {n : ℕ}1038 (b : Fin n → R) (z w : Fin n → O) :1039 coordinateLift b (z + w) = coordinateLift b z + coordinateLift b w := by1040 unfold coordinateLift1041 rw [← Finset.sum_add_distrib]1042 refine Finset.sum_congr rfl fun i _ => ?_1043 rw [Pi.add_apply, add_smul]1044 1045/-- Having a given tangent divisor of degree `d ≤ M` is constant on `pi ^ M`-congruence classes1046of chart coordinates. -/1047private theorem hasTangentDivisor_of_adicCongr (O R : Type) [CommRing O] [IsDomain O]1048 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]1049 (S : SurfaceData O R) (n : ℕ) (b : Fin n → R) (f : R)1050 (d M : ℕ) (hM : d ≤ M) (D : ExceptionalDivisor (IsLocalRing.ResidueField R))1051 (z z' : Fin n → O) (hc : adicCongr (Ideal.span {S.pi}) M z z')1052 (ht : HasTangentDivisor O R S (coordinateIdeal S.pi f b z') d D) :1053 HasTangentDivisor O R S (coordinateIdeal S.pi f b z) d D := by1054 rw [finite_coordinate_adic_congruence] at hc1055 have hy : ∀ i, ∃ y : O, z i = z' i + S.pi ^ M * y := by1056 intro i1057 have := hc i1058 rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton] at this1059 obtain ⟨y, hy⟩ := this1060 exact ⟨y, by rw [← hy]; ring⟩1061 choose y hy using hy1062 have hz : z = z' + S.pi ^ M • y := by1063 funext i; simp [hy i]1064 obtain ⟨g, H, hJ, hD, hjet⟩ := ht1065 unfold coordinateIdeal normalizedIdeal normalizedGenerator at hJ ⊢1066 rw [Ideal.span_singleton_eq_span_singleton] at hJ1067 obtain ⟨u, hu⟩ := hJ1068 have hgen : f + coordinateLift b (S.pi • z) =1069 f + coordinateLift b (S.pi • z') + algebraMap O R S.pi ^ (M+1) * coordinateLift b y := by1070 rw [hz, smul_add, coordinateLift_add, smul_smul,1071 coordinateLift_smul_eq_mul b (S.pi * S.pi ^ M)]1072 simp only [map_mul, map_pow]1073 ring1074 have := surface_tangent_jet_small_perturbation O R S d (M+1) (by omega) g1075 (coordinateLift b y * (u : R)) H D hD hjet1076 rw [← hu] at this1077 rw [hgen, ← Ideal.span_singleton_mul_right_unit u.isUnit]1078 convert this using 31079 ring1080 1081open scoped Classical in1082/-- Inside a coordinate chart, the fixed tangent cell is the disjoint union of the chart images1083of the `pi ^ M`-cosets of those representatives that have the prescribed tangent divisor. -/1084theorem fixed_tangent_cell_chart_partition (O R : Type) [CommRing O] [IsDomain O]1085 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]1086 (S : SurfaceData O R) (st : State) (n : ℕ) (b : Fin n → R) (f : R)1087 (hf : Ideal.span {f} ∈ surfaceStateSet O R S st)1088 (hinj : Function.Injective (coordinateIdeal S.pi f b)) (d M : ℕ) (hM : d ≤ M)1089 (D : ExceptionalDivisor (IsLocalRing.ResidueField R)) (reps : Finset (Fin n → O))1090 (hreps : ∀ z : Fin n → O, ∃! z₀, z₀ ∈ reps ∧ adicCongr (Ideal.span {S.pi}) M z z₀) :1091 fixedTangentCell O R S st d D ∩ Set.range (coordinateIdeal S.pi f b) = ⋃ z₀ ∈ reps.filter1092 (fun z₀ => HasTangentDivisor O R S (coordinateIdeal S.pi f b z₀) d D), coordinateIdeal S.pi f1093 b '' coordinateCoset S.pi M z₀ ∧ (reps : Set (Fin n → O)).PairwiseDisjoint1094 (fun z₀ => coordinateIdeal S.pi f b '' coordinateCoset S.pi M z₀) := by1095 have hsymm : ∀ z z' : Fin n → O, adicCongr (Ideal.span {S.pi}) M z z' →1096 adicCongr (Ideal.span {S.pi}) M z' z := by1097 intro z z' h1098 unfold adicCongr at *1099 rw [← neg_sub]; exact Submodule.neg_mem _ h1100 have hstate : ∀ z, coordinateIdeal S.pi f b z ∈ surfaceStateSet O R S st := by1101 intro z1102 unfold coordinateIdeal normalizedIdeal normalizedGenerator1103 rw [coordinateLift_smul_eq_mul]1104 exact surface_state_vertical_perturbation O R S st f _ hf1105 refine ⟨?_, ?_⟩1106 · ext J1107 simp only [Set.mem_inter_iff, Set.mem_range, Set.mem_iUnion, Finset.mem_filter,1108 exists_prop, Set.mem_image]1109 constructor1110 · rintro ⟨⟨_, htd⟩, z, rfl⟩1111 obtain ⟨z₀, ⟨hz₀, hc⟩, _⟩ := hreps z1112 exact ⟨z₀, ⟨hz₀, hasTangentDivisor_of_adicCongr O R S n b f d M hM D z₀ z (hsymm _ _ hc) htd⟩,1113 z, hc, rfl⟩1114 · rintro ⟨z₀, ⟨_, htd⟩, z, hz, rfl⟩1115 exact ⟨⟨hstate z, hasTangentDivisor_of_adicCongr O R S n b f d M hM D z z₀ hz htd⟩, z, rfl⟩1116 · intro a ha a' ha' hne1117 simp only [Function.onFun]1118 rw [Set.disjoint_image_iff hinj]1119 refine Set.disjoint_left.mpr fun z hz hz' => hne ?_1120 obtain ⟨w, _, huniq⟩ := hreps z1121 rw [huniq a ⟨ha, hz⟩, huniq a' ⟨ha', hz'⟩]1122 1123/-- The part of a fixed tangent cell inside a coordinate chart is measurable for the chart1124σ-algebra. -/1125theorem fixed_tangent_cell_chart_measurable (O R : Type) [CommRing O] [IsDomain O]1126 [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]1127 [MeasurableSpace O] (S : SurfaceData O R) (st : State) (n : ℕ) (b : Fin n → R) (f : R)1128 (hf : Ideal.span {f} ∈ surfaceStateSet O R S st)1129 (hinj : Function.Injective (coordinateIdeal S.pi f b)) (hchart : IsDivisionChart O R S.pi f b)1130 (d M : ℕ) (hM : d ≤ M) (D : ExceptionalDivisor (IsLocalRing.ResidueField R))1131 (reps : Finset (Fin n → O))1132 (hreps : ∀ z : Fin n → O, ∃! z₀, z₀ ∈ reps ∧ adicCongr (Ideal.span {S.pi}) M z z₀)1133 (hcoset : ∀ z₀ : Fin n → O, MeasurableSet (coordinateCoset S.pi M z₀)) :1134 @MeasurableSet (Ideal R) (idealChartSigma O R S.pi)1135 (fixedTangentCell O R S st d D ∩ Set.range (coordinateIdeal S.pi f b)) := by1136 rw [(fixed_tangent_cell_chart_partition O R S st n b f hf hinj d M hM D reps hreps).1]1137 let := idealChartSigma O R S.pi1138 exact Finset.measurableSet_biUnion _ fun z₀ _ =>1139 chart_image_measurable_chart_sigma O R S.pi n f b hchart _ (hcoset z₀)1140 1141/-! ### Twisted kernels -/1142 1143/-- A transition unit relating two compatible chart representatives is congruent to `1` modulo1144the `j`-th power of the overlap exceptional ideal. -/1145theorem transition_unit_congruent_one (R : Type) [CommRing R] (t x : R)1146 (beta : BlowupRestriction R t x) (d j : ℕ) (a a2 : BlowupChart R t x) (b b2 : BlowupChart R x t)1147 (ha : a2 - a ∈ (chartExceptional R t x) ^ j) (hb : b2 - b ∈ (chartExceptional R x t) ^ j)1148 (hlevel : (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) a - (overlapSlope R t x) ^ d *1149 beta.right b ∈ (Ideal.span {overlapException R t x}) ^ j)1150 (hregB : Function.Injective1151 (fun c : BlowupOverlap R t x ⧸ (Ideal.span {overlapException R t x})^j => Ideal.Quotient.mk1152 ((Ideal.span {overlapException R t x})^j) ((overlapSlope R t x)^d * beta.right b) * c))1153 (v : BlowupOverlap R t x)1154 (hv : (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) a2 - v *1155 ((overlapSlope R t x)^d * beta.right b2) ∈ (Ideal.span {overlapException R t x})^j) :1156 v - 1 ∈ (Ideal.span {overlapException R t x})^j := by1157 set I := (Ideal.span {overlapException R t x})^j with hI1158 set α := algebraMap (BlowupChart R t x) (BlowupOverlap R t x)1159 have hA : α a2 - α a ∈ I := by1160 have h := Ideal.mem_map_of_mem α ha1161 rw [Ideal.map_pow, chartExceptional, Ideal.map_span, Set.image_singleton] at h1162 rw [← map_sub]; exact h1163 have hx : beta.right (chartBase R x t x) ∈ Ideal.span {overlapException R t x} := by1164 have h1 : beta.right (chartBase R x t x) = algebraMap R (BlowupOverlap R t x) x :=1165 beta.right.commutes x1166 have h2 : α (chartBase R t x x) = algebraMap R (BlowupOverlap R t x) x :=1167 (IsScalarTower.toAlgHom R (BlowupChart R t x) (BlowupOverlap R t x)).commutes x1168 rw [h1, ← h2, ← blowup_chart_relation, map_mul]1169 exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)1170 have hB : beta.right b2 - beta.right b ∈ I := by1171 have h := Ideal.mem_map_of_mem beta.right.toRingHom hb1172 rw [Ideal.map_pow, chartExceptional, Ideal.map_span, Set.image_singleton] at h1173 rw [← map_sub]1174 refine Ideal.pow_right_mono ?_ j h1175 rw [Ideal.span_le, Set.singleton_subset_iff]; exact hx1176 have key : (v - 1) * ((overlapSlope R t x)^d * beta.right b) ∈ I := by1177 have e : (v - 1) * ((overlapSlope R t x)^d * beta.right b) =1178 -(α a2 - v * ((overlapSlope R t x)^d * beta.right b2)) + (α a2 - α a)1179 + (α a - (overlapSlope R t x)^d * beta.right b)1180 - (v * (overlapSlope R t x)^d) * (beta.right b2 - beta.right b) := by ring1181 rw [e]1182 exact I.sub_mem (I.add_mem (I.add_mem (I.neg_mem hv) hA) hlevel) (I.mul_mem_left _ hB)1183 rw [← Ideal.Quotient.eq_zero_iff_mem]1184 apply hregB1185 simp only1186 rw [← map_mul, mul_comm, Ideal.Quotient.eq_zero_iff_mem.mpr key, mul_zero]1187 1188/-- Every closed Čech input class for twist `d` is the class of `(tᵈ r, xᵈ r)` for some surface1189function `r`. -/1190theorem twisted_kernel_from_surface (R : Type) [CommRing R] (t x : R)1191 (hreg : RegularParameterPair R t x) (hregSwap : RegularParameterPair R x t)1192 (beta : BlowupRestriction R t x) (d j : ℕ)1193 (h : cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap1194 (fullCechDifferential R t x beta d)) (w : CechLevelInput R t x j)1195 (hw : finiteCechDifferential R t x beta d j h w = 0) :1196 ∃ r : R, w = (cechInputLattice R t x j).mkQ1197 ((chartBase R t x t)^d * algebraMap R (BlowupChart R t x) r, (chartBase R x t x)^d *1198 algebraMap R (BlowupChart R x t) r) := by1199 have hβr := beta_right_chartBase beta1200 have hD0 : ∀ r : R, fullCechDifferential R t x beta d1201 ((chartBase R t x t)^d * chartBase R t x r, (chartBase R x t x)^d * chartBase R x t r) =1202 0 := by1203 intro r1204 change algebraMap (BlowupChart R t x) (BlowupOverlap R t x) _ -1205 (IsLocalization.Away.invSelf (chartSlope R t x))^d * beta.right _ = 01206 rw [map_mul, map_mul, map_pow, map_pow, hβr, hβr, chartBase_x_eq, map_mul]1207 have hu : (IsLocalization.Away.invSelf (chartSlope R t x) *1208 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartSlope R t x))^d = 1 := by1209 rw [mul_comm, IsLocalization.Away.mul_invSelf, one_pow]1210 linear_combination1211 (-(algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t)^d *1212 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x r))) * hu1213 have main : ∀ n : ℕ, ∀ (a : BlowupChart R t x) (b : BlowupChart R x t),1214 fullCechDifferential R t x beta d (a, b) ∈1215 (Ideal.span {algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t)})^n →1216 ∃ r : R, a - (chartBase R t x t)^d * chartBase R t x r ∈ (Ideal.span {chartBase R t x t})^n ∧1217 b - (chartBase R x t x)^d * chartBase R x t r ∈ (Ideal.span {chartBase R x t x})^n := by1218 intro n1219 induction n with1220 | zero => exact fun _ _ _ => ⟨0, by simp, by simp⟩1221 | succ n ih =>1222 intro a b hab1223 obtain ⟨r, har, hbr⟩ := ih a b (Ideal.pow_le_pow_right (Nat.le_succ n) hab)1224 have hD' : fullCechDifferential R t x beta d1225 (a - (chartBase R t x t)^d * chartBase R t x r, b - (chartBase R x t x)^d * chartBase R x1226 t r) ∈1227 (Ideal.span1228 {algebraMap (BlowupChart R t x) (BlowupOverlap R t x)1229 (chartBase R t x t)})^(n+1) := by1230 rw [← Prod.mk_sub_mk, map_sub, hD0, sub_zero]1231 exact hab1232 obtain ⟨r', -, ha', hb'⟩ := cech_layer_step R t x hreg beta hregSwap d n _ _ har hbr hD'1233 refine ⟨r + r', ?_, ?_⟩1234 · convert ha' using 1; rw [map_add]; ring1235 · convert hb' using 1; rw [map_add]; ring1236 induction w using Submodule.Quotient.induction_on with1237 | H z =>1238 obtain ⟨a, b⟩ := z1239 rw [finiteCechDifferential, Submodule.mapQ_apply, Submodule.Quotient.mk_eq_zero] at hw1240 obtain ⟨r, har, hbr⟩ := main j a b hw1241 refine ⟨r, ?_⟩1242 rw [Submodule.mkQ_apply, Submodule.Quotient.eq]1243 exact ⟨har, hbr⟩1244 1245end SurfaceBlowup