Lean sources / SurfaceBlowup / Blowup / CurveSections.lean
Curve sections on the two-chart 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.H0Comparison7import SurfaceBlowup.Blowup.StrictNormalizer8 9/-!10# Curve sections on the two-chart blow-up11 12Let `(t, x)` be a regular parameter pair of `R` and consider the two affine charts of the blow-up13of `(t, x)` together with their overlap. This file studies the lattices of curve sections cut out14by a compatible system of glued generators: it identifies their pullbacks to the surface, proves15that the layer-by-layer reduction maps are surjective (via a Laurent-polynomial description of the16exceptional layers of the overlap), constructs glued generators from compatible chart generators,17and establishes the basic transversality and finiteness properties of two-chart curve data.18 19## Main results20 21* `SurfaceBlowup.surface_to_curve_quotient_kernel`: a surface function lies in the level-`j` curve22 lattice iff it lies in `(f) + (t, x)^j`.23* `SurfaceBlowup.two_chart_layer_correction`: every element of the `j`-th exceptional layer of the24 overlap is a twisted Čech coboundary modulo the next layer.25* `SurfaceBlowup.curve_limit_level_map_surjective`: the projection from the curve order limit to26 each level is surjective.27* `SurfaceBlowup.glued_generators_exist`: compatible chart generators glue to glued generators.28* `SurfaceBlowup.mul_injective_quotient_transport`,29 `SurfaceBlowup.exists_pow_le_span_pair_transport`: transversality and finite contact transport30 along a ring isomorphism sending the exceptional parameter to a unit multiple of another.31* `SurfaceBlowup.strict_transform_equation_of_kernels`: the chart-independent strict-transform32 equation `f = eᵈ · g · unit` at a point of finite support.33* `SurfaceBlowup.two_chart_left_data_transverse_finite`,34 `SurfaceBlowup.two_chart_right_data_transverse_finite`: transversality and finiteness of the local35 data of two-chart curve data at the points of the two charts.36 37Provenance: `Thm_SurfaceBlowupV2_{surface_to_curve_quotient_kernel,38parent_ideal_unique_of_level_lattice, surface_to_curve_limit_kernel, two_chart_layer_correction,39curve_sections_reduction_surjective, curve_limit_level_map_surjective,40two_chart_additive_approximation, curve_sections_cover_overlap, two_chart_layer_correction_positive,41glued_generators_step, glued_generators_exist, two_chart_left_data_transverse_finite,42two_chart_left_points_maximal, strict_transform_left_point_equation,43two_chart_right_data_transverse_finite}` (the node `glued_generators_step` is the private44`glued_generators_succ` here).45-/46 47namespace SurfaceBlowup48 49/-! ### Transport between the charts and the overlap -/50 51section Transport52 53variable {R : Type} [CommRing R] {t x : R}54 55/-- The right chart map sends `x` to `e · z` on the overlap. -/56theorem beta_right_chartBase_self (beta : BlowupRestriction R t x) :57 beta.right (chartBase R x t x) = overlapException R t x * overlapSlope R t x := by58 rw [beta_right_chartBase, ← blowup_chart_relation, map_mul]59 rfl60 61private theorem algebraMap_mem_overlap_pow (j : ℕ) (a : BlowupChart R t x)62 (ha : a ∈ (chartExceptional R t x) ^ j) :63 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) a ∈64 (Ideal.span {overlapException R t x})^j := by65 have := Ideal.mem_map_of_mem (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) ha66 rwa [Ideal.map_pow, chartExceptional, Ideal.map_span, Set.image_singleton] at this67 68private theorem beta_right_mem_overlap_pow (beta : BlowupRestriction R t x) (j : ℕ)69 (b : BlowupChart R x t) (hb : b ∈ (chartExceptional R x t) ^ j) :70 beta.right b ∈ (Ideal.span {overlapException R t x})^j := by71 have := Ideal.mem_map_of_mem (beta.right : BlowupChart R x t →+* BlowupOverlap R t x) hb72 rw [Ideal.map_pow, chartExceptional, Ideal.map_span, Set.image_singleton] at this73 refine Ideal.pow_right_mono ?_ j this74 rw [Ideal.span_singleton_le_span_singleton]75 change _ ∣ beta.right (chartBase R x t x)76 rw [beta_right_chartBase_self]77 exact dvd_mul_right _ _78 79end Transport80 81/-! ### Curve lattices and the surface -/82 83private theorem algebraMap_sub_mul_mem {R A : Type} [CommRing R] [CommRing A] [Algebra R A]84 (I : Ideal A) (T g a c : A) (d : ℕ) {r f s : R}85 (hyc : a * g + c = algebraMap R A r) (hs : a - T ^ d * algebraMap R A s ∈ I) (hc : c ∈ I)86 (hf : algebraMap R A f - T ^ d * g ∈ I) : algebraMap R A (r - f * s) ∈ I := by87 have : algebraMap R A (r - f * s) =88 g * (a - T ^ d * algebraMap R A s) + c -89 (algebraMap R A f - T ^ d * g) * algebraMap R A s := by90 rw [map_sub, map_mul, ← hyc]; ring91 rw [this]92 exact sub_mem (add_mem (Ideal.mul_mem_left _ _ hs) hc) (Ideal.mul_mem_right _ _ hf)93 94private theorem algebraMap_mem_span_sup {R A : Type} [CommRing R] [CommRing A] [Algebra R A]95 (I : Ideal A) (T g : A) (d : ℕ) {f : R} (hf : algebraMap R A f - T ^ d * g ∈ I) :96 algebraMap R A f ∈ Ideal.span {g} ⊔ I := by97 rw [← sub_add_cancel (algebraMap R A f) (T ^ d * g)]98 exact add_mem (Ideal.mem_sup_right hf)99 (Ideal.mem_sup_left (Ideal.mem_span_singleton.mpr (dvd_mul_left _ _)))100 101/-- A surface function `r` lies in the level-`j` curve lattice of the glued generators `G` iff102`r ∈ (f) + (t, x)^j`, where `f` is a surface function inducing `G` at every level. -/103theorem surface_to_curve_quotient_kernel (R : Type) [CommRing R] (t x : R)104 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d)105 (hreg : RegularParameterPair R t x) (hregSwap : RegularParameterPair R x t) (j : ℕ)106 (hregF : Function.Injective (fun c : BlowupOverlap R t x ⧸107 (Ideal.span {overlapException R t x})^j =>108 Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j)109 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j)) * c))110 (f : R)111 (hf : ∀ j : ℕ, surfaceToCechInput R t x j f =112 (cechInputLattice R t x j).mkQ (gluedFunctionPair R t x G j))113 (r : R) :114 surfaceToChartPair R t x r ∈ curveIdealLattice R t x beta G j ↔ r ∈ Ideal.span {f} ⊔115 (Ideal.span {t,x})^j := by116 have hker := surface_to_cech_kernel R t x hreg j117 have hfA := glued_function_left_chart R t x beta d G f hf j118 have hfB := glued_function_right_chart R t x beta d G f hf j119 -- kernel elements map into the input lattice120 have hlat : ∀ u : R, u ∈ (Ideal.span {t,x})^j ↔121 surfaceToChartPair R t x u ∈ cechInputLattice R t x j := by122 intro u123 rw [← hker, LinearMap.mem_ker]124 change (cechInputLattice R t x j).mkQ _ = 0 ↔ _125 rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]126 have hin : cechInputLattice R t x j ≤ curveIdealLattice R t x beta G j := by127 rintro ⟨a, b⟩ ⟨ha, hb⟩128 exact ⟨Ideal.mem_sup_right ha, Ideal.mem_sup_right hb⟩129 constructor130 · intro h131 obtain ⟨hA, hB⟩ := h132 change algebraMap R (BlowupChart R t x) r ∈ Ideal.span {G.left j} ⊔ _ at hA133 change algebraMap R (BlowupChart R x t) r ∈ Ideal.span {G.right j} ⊔ _ at hB134 obtain ⟨y, hy, c, hc, hyc⟩ := Submodule.mem_sup.mp hA135 obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp hy136 obtain ⟨y', hy', c', hc', hyc'⟩ := Submodule.mem_sup.mp hB137 obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.mp hy'138 set alpha := algebraMap (BlowupChart R t x) (BlowupOverlap R t x) with halpha139 set Zi := IsLocalization.Away.invSelf (chartSlope R t x) (S := BlowupOverlap R t x) with hZi140 set I := (Ideal.span {overlapException R t x})^j with hI141 have hZ : overlapSlope R t x * Zi = 1 := IsLocalization.Away.mul_invSelf _142 have hZd : overlapSlope R t x ^ d * Zi ^ d = 1 := by rw [← mul_pow, hZ, one_pow]143 have h1 : alpha (a * G.left j + c) = beta.right (b * G.right j + c') := by144 rw [hyc, hyc', AlgHom.commutes, halpha, ← IsScalarTower.algebraMap_apply]145 rw [map_add, map_add, map_mul, map_mul] at h1146 have hov := G.overlap j147 have hmem : alpha (G.left j) * (alpha a - Zi ^ d * beta.right b) ∈ I := by148 have heq : alpha (G.left j) * (alpha a - Zi ^ d * beta.right b) =149 beta.right c' - alpha c - Zi ^ d * beta.right b *150 (alpha (G.left j) - overlapSlope R t x ^ d * beta.right (G.right j)) := by151 linear_combination h1 - (beta.right b * beta.right (G.right j)) * hZd152 rw [heq]153 exact sub_mem (sub_mem (beta_right_mem_overlap_pow beta j c' hc')154 (algebraMap_mem_overlap_pow j c hc)) (Ideal.mul_mem_left _ _ hov)155 have hcl : alpha a - Zi ^ d * beta.right b ∈ I := by156 rw [← Ideal.Quotient.eq_zero_iff_mem]157 apply hregF158 simp only [mul_zero]159 rw [← map_mul, Ideal.Quotient.eq_zero_iff_mem]160 exact hmem161 have hle : cechInputLattice R t x j ≤162 (cechOutputLattice R t x j).comap (fullCechDifferential R t x beta d) := by163 rintro ⟨a₁, b₁⟩ ⟨ha₁, hb₁⟩164 change alpha a₁ - Zi ^ d * beta.right b₁ ∈ I165 exact sub_mem (algebraMap_mem_overlap_pow j a₁ ha₁)166 (Ideal.mul_mem_left _ _ (beta_right_mem_overlap_pow beta j b₁ hb₁))167 obtain ⟨s, hs⟩ := twisted_kernel_from_surface R t x hreg hregSwap beta d j hle168 ((cechInputLattice R t x j).mkQ (a, b)) (by169 rw [finiteCechDifferential, Submodule.mkQ_apply, Submodule.mapQ_apply,170 Submodule.Quotient.mk_eq_zero]171 exact hcl)172 rw [Submodule.mkQ_apply, Submodule.mkQ_apply, Submodule.Quotient.eq] at hs173 obtain ⟨hsA, hsB⟩ := hs174 refine Submodule.mem_sup.mpr ⟨f * s, Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self f),175 r - f * s, ?_, by ring⟩176 rw [hlat]177 exact ⟨algebraMap_sub_mul_mem _ _ _ a c d hyc hsA hc hfA,178 algebraMap_sub_mul_mem _ _ _ b c' d hyc' hsB hc' hfB⟩179 · intro h180 obtain ⟨y, hy, u, hu, rfl⟩ := Submodule.mem_sup.mp h181 obtain ⟨s, rfl⟩ := Ideal.mem_span_singleton'.mp hy182 rw [map_add]183 refine add_mem ?_ (hin ((hlat u).mp hu))184 rw [show s * f = s • f from rfl, map_smul]185 exact Submodule.smul_mem _ _186 ⟨algebraMap_mem_span_sup _ _ _ d hfA, algebraMap_mem_span_sup _ _ _ d hfB⟩187 188/-- In a regular local ring, a surface function `f'` lying in every curve lattice of `G` and of189multiplicity at most `d` generates the same principal ideal as the function `f` inducing `G`. -/190theorem parent_ideal_unique_of_level_lattice (R : Type) [CommRing R] (t x : R)191 [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsLocalRing R] [IsNoetherianRing R]192 (hreg : RegularParameterPair R t x) (hregSwap : RegularParameterPair R x t)193 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d)194 (hregF : ∀ j : ℕ, Function.Injective (fun c : BlowupOverlap R t x ⧸195 (Ideal.span {overlapException R t x})^j =>196 Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j)197 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j)) * c))198 (f : R)199 (hf : ∀ j : ℕ, surfaceToCechInput R t x j f =200 (cechInputLattice R t x j).mkQ (gluedFunctionPair R t x G j))201 (f' : R) (hf' : ∀ j : ℕ, surfaceToChartPair R t x f' ∈ curveIdealLattice R t x beta G j)202 (hmult : f' ∉ (Ideal.span {t,x})^(d+1)) :203 Ideal.span {f'} = Ideal.span {f} := by204 have hm : Ideal.span ({t,x} : Set R) = IsLocalRing.maximalIdeal R :=205 IsLocalRing.eq_maximalIdeal inferInstance206 have h1 : f' ∈ Ideal.span {f} := by207 have := ideal_closed_noetherian_local R (Ideal.span {f})208 rw [← this, Ideal.mem_iInf]209 intro j210 rw [← hm]211 exact (surface_to_curve_quotient_kernel R t x beta d G hreg hregSwap j (hregF j) f hf f').mp212 (hf' j)213 obtain ⟨r, hr⟩ := Ideal.mem_span_singleton'.mp h1214 have hfd := glued_function_order R t x beta d G hreg f hf215 have hru : IsUnit r := by216 by_contra hn217 apply hmult218 rw [hm] at hfd ⊢219 have : r ∈ IsLocalRing.maximalIdeal R := by220 simpa [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff] using hn221 rw [← hr, pow_succ, mul_comm]222 exact Ideal.mul_mem_mul this hfd223 obtain ⟨u, rfl⟩ := hru224 rw [← hr]225 exact principal_ideal_unit_invariance R f u226 227/-- If `(f)` is closed in the `(t, x)`-adic topology, the kernel of a section `σ` of the map from228the surface to the curve order limit is the principal ideal `(f)`. -/229theorem surface_to_curve_limit_kernel (R : Type) [CommRing R] (t x : R)230 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d)231 (hreg : RegularParameterPair R t x) (hregSwap : RegularParameterPair R x t)232 (hregF : ∀ j : ℕ, Function.Injective (fun c : BlowupOverlap R t x ⧸233 (Ideal.span {overlapException R t x})^j =>234 Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j)235 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j)) * c))236 (f : R)237 (hf : ∀ j : ℕ, surfaceToCechInput R t x j f =238 (cechInputLattice R t x j).mkQ (gluedFunctionPair R t x G j))239 (hclosed : (⨅ j : ℕ, (Ideal.span {f} ⊔ (Ideal.span {t,x})^j)) = Ideal.span {f})240 (σ : R →ₗ[R] CurveOrderLimit R t x beta G)241 (hσ : ∀ r : R, ∃ p : curveThreads R t x beta G, σ r = curveLimitMk R t x beta G p ∧ ∀ j : ℕ,242 p.val j = surfaceToChartPair R t x r) :243 LinearMap.ker σ = (Ideal.span {f} : Submodule R R) := by244 ext r245 obtain ⟨p, hp, hpj⟩ := hσ r246 have key : σ r = 0 ↔ ∀ j, r ∈ Ideal.span {f} ⊔ (Ideal.span {t,x})^j := by247 rw [hp]248 change Submodule.Quotient.mk p = 0 ↔ _249 rw [Submodule.Quotient.mk_eq_zero]250 change (∀ j ∈ (Set.univ : Set ℕ), p.val j ∈ curveIdealLattice R t x beta G j) ↔ _251 simp only [Set.mem_univ, forall_true_left]252 refine forall_congr' fun j => ?_253 rw [hpj j]254 exact surface_to_curve_quotient_kernel R t x beta d G hreg hregSwap j (hregF j) f hf r255 rw [LinearMap.mem_ker, key]256 rw [← Submodule.mem_iInf, hclosed]257 258/-! ### Exceptional layers of the overlap -/259 260private theorem principalLayerMap_apply' {A : Type} [CommRing A] (e : A) (j : ℕ) (a : A) :261 principalLayerMap A e j a = Ideal.Quotient.mk ((Ideal.span {e})^(j+1)) (a * e^j) := by262 simp [principalLayerMap, LinearMap.toSpanSingleton_apply, Algebra.smul_def]263 264/-- Twisted layer correction with an arbitrary integral twist `k ≥ -1 - j`: an element of the265`j`-th power of the exceptional ideal of the overlap is, modulo the `(j + 1)`-st power,266of the form `a - z^k β(b)` with `a`, `b` in the `j`-th powers of the exceptional ideals of the267charts (`z` the slope). -/268private theorem two_chart_layer_correction_zpow (R : Type) [CommRing R] (t x : R)269 (hreg : RegularParameterPair R t x) (beta : BlowupChart R x t →+* BlowupOverlap R t x)270 (hbase : ∀ r : R, beta (chartBase R x t r) =271 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x r))272 (hslope : beta (chartSlope R x t) = IsLocalization.Away.invSelf (chartSlope R t x))273 (j : ℕ) (k : ℤ) (hk : -1 ≤ (j : ℤ) + k) (w : BlowupOverlap R t x)274 (hw : w ∈ (Ideal.span {algebraMap (BlowupChart R t x) (BlowupOverlap R t x)275 (chartBase R t x t)})^j) :276 ∃ a ∈ (chartExceptional R t x)^j, ∃ b ∈ (chartExceptional R x t)^j,277 w - (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) a -278 selfZPow (chartSlope R t x) (BlowupOverlap R t x) k * beta b) ∈279 (Ideal.span {algebraMap (BlowupChart R t x) (BlowupOverlap R t x)280 (chartBase R t x t)})^(j+1) := by281 obtain ⟨L, hL⟩ := overlap_layer_laurent_coordinates R t x hreg j282 have hP : ∀ P : Polynomial (R ⧸ Ideal.span {t, x}), ∃ a ∈ (chartExceptional R t x)^j,283 (L P.toLaurent).val = Ideal.Quotient.mk ((Ideal.span {algebraMap (BlowupChart R t x)284 (BlowupOverlap R t x) (chartBase R t x t)})^(j+1))285 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) a) := by286 intro P287 induction P using Polynomial.induction_on' with288 | add p q hp hq =>289 obtain ⟨a1, ha1, h1⟩ := hp290 obtain ⟨a2, ha2, h2⟩ := hq291 refine ⟨a1 + a2, add_mem ha1 ha2, ?_⟩292 rw [map_add, map_add, Submodule.coe_add, h1, h2, map_add, map_add]293 | monomial n c =>294 obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective c295 refine ⟨chartBase R t x r * chartSlope R t x ^ n * chartBase R t x t ^ j,296 Ideal.mul_mem_left _ _ (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self _) j), ?_⟩297 rw [Polynomial.toLaurent_C_mul_T, hL, principalLayerMap_apply']298 simp only [map_mul, map_pow, selfZPow_natCast]299 have hQ : ∀ Q : Polynomial (R ⧸ Ideal.span {t, x}), ∃ b ∈ (chartExceptional R x t)^j,300 (L (LaurentPolynomial.T ((j : ℤ) + k) * LaurentPolynomial.invert Q.toLaurent)).val301 = Ideal.Quotient.mk ((Ideal.span {algebraMap (BlowupChart R t x)302 (BlowupOverlap R t x) (chartBase R t x t)})^(j+1))303 (selfZPow (chartSlope R t x) (BlowupOverlap R t x) k * beta b) := by304 intro Q305 induction Q using Polynomial.induction_on' with306 | add p q hp hq =>307 obtain ⟨a1, ha1, h1⟩ := hp308 obtain ⟨a2, ha2, h2⟩ := hq309 refine ⟨a1 + a2, add_mem ha1 ha2, ?_⟩310 rw [map_add, map_add, mul_add, map_add, Submodule.coe_add, h1, h2, map_add, mul_add, map_add]311 | monomial n c =>312 obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective c313 refine ⟨chartBase R x t r * chartBase R x t x ^ j * chartSlope R x t ^ n,314 Ideal.mul_mem_right _ _315 (Ideal.mul_mem_left _ _ (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self _) j)), ?_⟩316 have hT : LaurentPolynomial.T ((j : ℤ) + k) * LaurentPolynomial.invert317 (Polynomial.toLaurent (Polynomial.monomial n (Ideal.Quotient.mk (Ideal.span {t, x}) r)))318 = LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t, x}) r)319 * LaurentPolynomial.T ((j : ℤ) + k + -(n : ℤ)) := by320 rw [Polynomial.toLaurent_C_mul_T, map_mul, LaurentPolynomial.invert_C,321 LaurentPolynomial.invert_T, mul_left_comm, ← LaurentPolynomial.T_add]322 rw [hT, hL, principalLayerMap_apply']323 congr 1324 rw [map_mul, map_mul, map_pow, map_pow, hbase, hbase, hslope,325 ← blowup_chart_relation R t x, map_mul, selfZPow_add, selfZPow_add, selfZPow_natCast,326 invSelf_pow_eq_selfZPow]327 ring328 obtain ⟨P, Q, hF⟩ := laurent_split_nonnegative_twist (R ⧸ Ideal.span {t, x}) ((j : ℤ) + k) hk329 (L.symm ⟨Ideal.Quotient.mk ((Ideal.span {algebraMap (BlowupChart R t x)330 (BlowupOverlap R t x) (chartBase R t x t)})^(j+1)) w, by331 rw [LinearMap.mem_ker]332 unfold principalPowerReduction333 rw [AlgHom.toLinearMap_apply, Ideal.Quotient.factorₐ_apply, Ideal.Quotient.factor_mk]334 exact Ideal.Quotient.eq_zero_iff_mem.mpr hw⟩)335 obtain ⟨a, ha, hPa⟩ := hP P336 obtain ⟨b, hb, hQb⟩ := hQ Q337 refine ⟨a, ha, b, hb, ?_⟩338 rw [← Ideal.Quotient.eq_zero_iff_mem]339 have := congrArg (fun F => (L F).val) hF340 simp only [LinearEquiv.apply_symm_apply, map_sub, Submodule.coe_sub] at this341 rw [hPa, hQb] at this342 rw [map_sub, this, map_sub, sub_self]343 344/-- Layer correction with negative twist: for `d ≤ j + 1`, every `w` in the `j`-th power of the345exceptional ideal of the overlap agrees modulo the `(j + 1)`-st power with `a - z⁻ᵈ β(b)`, where346`a`, `b` lie in the `j`-th powers of the exceptional ideals of the two charts. -/347theorem two_chart_layer_correction (R : Type) [CommRing R] (t x : R)348 (hreg : RegularParameterPair R t x) (beta : (BlowupChart R x t) →+* (BlowupOverlap R t x))349 (hbase : ∀ r : R, beta (chartBase R x t r) =350 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x r))351 (hslope : beta (chartSlope R x t) = IsLocalization.Away.invSelf (chartSlope R t x)) (j d : ℕ)352 (hd : d ≤ j+1) (w : (BlowupOverlap R t x))353 (hw : w ∈354 (Ideal.span {(algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)})^j) :355 ∃ a : (BlowupChart R t x), ∃ b : (BlowupChart R x t), a ∈ (chartExceptional R t x)^j ∧ b ∈356 (chartExceptional R x t)^j ∧ w - ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) a -357 (IsLocalization.Away.invSelf (chartSlope R t x))^d * beta b) ∈ (Ideal.span358 {(algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)})^(j+1) := by359 obtain ⟨a, ha, b, hb, h⟩ :=360 two_chart_layer_correction_zpow R t x hreg beta hbase hslope j (-d) (by omega) w hw361 exact ⟨a, b, ha, hb, by rwa [← invSelf_pow_eq_selfZPow] at h⟩362 363/-- The reduction map from the level-`(j + 1)` to the level-`j` quotient of curve sections is364surjective. -/365private theorem curve_sections_reduction_surjective (R : Type) [CommRing R] (t x : R)366 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d)367 (hreg : RegularParameterPair R t x) (j : ℕ)368 (ρ : curveSectionsQuot R t x beta G (j + 1) →ₗ[R] curveSectionsQuot R t x beta G j)369 (hρ : ∀ q : curveSectionsQuot R t x beta G (j+1), ∀ p : BlowupChart R t x × BlowupChart R x t,370 (q : (BlowupChart R t x × BlowupChart R x t) ⧸ curveIdealLattice R t x beta G (j+1)) =371 (curveIdealLattice R t x beta G (j+1)).mkQ p → ((ρ q : curveSectionsQuot R t x beta G j) :372 (BlowupChart R t x × BlowupChart R x t) ⧸ curveIdealLattice R t x beta G j) =373 (curveIdealLattice R t x beta G j).mkQ p) :374 Function.Surjective ρ := by375 set α := algebraMap (BlowupChart R t x) (BlowupOverlap R t x) with hα376 set E : Ideal (BlowupOverlap R t x) := Ideal.span {α (chartBase R t x t)} with hE377 have hbase : ∀ r : R, beta.right.toRingHom (chartBase R x t r) = α (chartBase R t x r) :=378 beta_right_chartBase beta379 have hdiff : ∀ p : BlowupChart R t x × BlowupChart R x t,380 fullCechDifferential R t x beta 0 p = α p.1 - beta.right p.2 := by381 intro p382 change α p.1 - (IsLocalization.Away.invSelf (chartSlope R t x))^0 * beta.right p.2 = _383 simp384 rintro ⟨y, hy⟩385 obtain ⟨p, hp, rfl⟩ := Submodule.mem_map.mp hy386 have hp' : α p.1 - beta.right p.2 ∈ overlapCurveIdeal R t x beta G j := by387 rw [← hdiff]; exact hp388 obtain ⟨u, hu, v, hv, huv⟩ := Submodule.mem_sup.mp hp'389 obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.mp hu390 have hEeq : Ideal.span {overlapException R t x} = E := rfl391 rw [hEeq] at hv392 have hcompat : α (G.left j) - α (G.left (j+1)) ∈ E ^ j := by393 have := Ideal.mem_map_of_mem α (G.left_compat j)394 rw [chartExceptional, Ideal.map_pow, Ideal.map_span, Set.image_singleton] at this395 rw [← neg_sub, ← map_sub]396 exact neg_mem this397 set w := α p.1 - beta.right p.2 - c * α (G.left (j+1)) with hw398 have hwmem : w ∈ E ^ j := by399 have : w = c * (α (G.left j) - α (G.left (j+1))) + v := by400 rw [hw, ← huv]; ring401 rw [this]402 exact add_mem (Ideal.mul_mem_left _ _ hcompat) hv403 obtain ⟨a₁, b₁, ha₁, hb₁, hres⟩ := two_chart_layer_correction R t x hreg beta.right.toRingHom404 hbase beta.slope j 0 (by omega) w hwmem405 simp only [pow_zero, one_mul] at hres406 set p' : BlowupChart R t x × BlowupChart R x t := (p.1 - a₁, p.2 - b₁) with hp'def407 have hp'mem : p' ∈ curveSections R t x beta G (j+1) := by408 change fullCechDifferential R t x beta 0 p' ∈ overlapCurveIdeal R t x beta G (j+1)409 rw [hdiff]410 have : α p'.1 - beta.right p'.2 = c * α (G.left (j+1)) +411 (w - (α a₁ - beta.right.toRingHom b₁)) := by412 simp only [hp'def, hw, map_sub]; change _ = _ + (_ - (_ - beta.right b₁))413 ring414 rw [this]415 exact add_mem (Submodule.mem_sup_left (Ideal.mul_mem_left _ _ (Ideal.subset_span rfl)))416 (Submodule.mem_sup_right hres)417 refine ⟨⟨(curveIdealLattice R t x beta G (j+1)).mkQ p', Submodule.mem_map_of_mem hp'mem⟩, ?_⟩418 apply Subtype.ext419 rw [hρ _ p' rfl]420 simp only [Submodule.mkQ_apply]421 rw [Submodule.Quotient.eq]422 refine ⟨?_, ?_⟩423 · change p.1 - a₁ - p.1 ∈ leftCurveIdeal R t x beta G j424 rw [sub_sub_cancel_left]425 exact Submodule.mem_sup_right (neg_mem ha₁)426 · change p.2 - b₁ - p.2 ∈ rightCurveIdeal R t x beta G j427 rw [sub_sub_cancel_left]428 exact Submodule.mem_sup_right (neg_mem hb₁)429 430/-- The projection from the curve order limit to the level-`J` quotient of curve sections is431surjective. -/432theorem curve_limit_level_map_surjective (R : Type) [CommRing R] (t x : R)Lemma 4.1433 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d)434 (hreg : RegularParameterPair R t x) (J : ℕ)435 (π : CurveOrderLimit R t x beta G →ₗ[R] curveSectionsQuot R t x beta G J)436 (hπ : ∀ p : curveThreads R t x beta G,437 ((π (curveLimitMk R t x beta G p) : curveSectionsQuot R t x beta G J) :438 (BlowupChart R t x × BlowupChart R x t) ⧸ curveIdealLattice R t x beta G J) =439 (curveIdealLattice R t x beta G J).mkQ (p.val J)) :440 Function.Surjective π := by441 classical442 -- key lifting step443 have key : ∀ j : ℕ, ∀ a, a ∈ curveSections R t x beta G j →444 ∃ b, b ∈ curveSections R t x beta G (j+1) ∧ a - b ∈ curveIdealLattice R t x beta G j := by445 intro j a ha446 obtain ⟨ρ, hρ⟩ := curve_sections_quot_reduction_exists R t x beta d G j447 have hs := curve_sections_reduction_surjective R t x beta d G hreg j ρ hρ448 obtain ⟨q', hq'⟩ := hs ⟨(curveIdealLattice R t x beta G j).mkQ a, Submodule.mem_map_of_mem ha⟩449 obtain ⟨b, hb, hbq⟩ := Submodule.mem_map.mp q'.2450 refine ⟨b, hb, ?_⟩451 have h1 := hρ q' b hbq.symm452 rw [hq'] at h1453 have h2 : (curveIdealLattice R t x beta G j).mkQ (a - b) = 0 := by454 rw [map_sub]; exact sub_eq_zero.mpr h1455 exact (Submodule.Quotient.mk_eq_zero _).mp h2456 have anti : Antitone (fun j => curveSections R t x beta G j) :=457 antitone_nat_of_succ_le (fun j => (curve_lattices_antitone R t x beta d G j).2)458 intro q459 obtain ⟨a, ha, haq⟩ := Submodule.mem_map.mp q.2460 let f : ℕ → ChartPair R t x := fun n => Nat.rec a (fun n fn =>461 if h : fn ∈ curveSections R t x beta G (J+n) then Classical.choose (key (J+n) fn h) else 0) n462 have f0 : f 0 = a := rfl463 have fmem : ∀ n, f n ∈ curveSections R t x beta G (J+n) ∧464 f n - f (n+1) ∈ curveIdealLattice R t x beta G (J+n) := by465 have hs : ∀ n (h : f n ∈ curveSections R t x beta G (J+n)),466 f (n+1) = Classical.choose (key (J+n) (f n) h) := fun n h => dif_pos h467 intro n468 induction n with469 | zero => exact ⟨ha, by rw [hs 0 ha]; exact (Classical.choose_spec (key _ _ ha)).2⟩470 | succ n ih =>471 have h : f (n+1) ∈ curveSections R t x beta G (J+(n+1)) := by472 rw [hs n ih.1]; exact (Classical.choose_spec (key _ _ ih.1)).1473 exact ⟨h, by rw [hs (n+1) h]; exact (Classical.choose_spec (key _ _ h)).2⟩474 let p : ℕ → ChartPair R t x := fun j => f (j - J)475 have hp : p ∈ curveThreads R t x beta G := by476 refine ⟨?_, ?_⟩477 · intro j _478 exact anti (show j ≤ J + (j - J) by omega) (fmem (j - J)).1479 · intro j _480 change p j - LinearMap.id (p (j+1)) ∈ curveIdealLattice R t x beta G j481 simp only [LinearMap.id_apply, p]482 by_cases hj : j < J483 · rw [show j - J = 0 by omega, show j + 1 - J = 0 by omega, sub_self]484 exact Submodule.zero_mem _485 · rw [show j + 1 - J = (j - J) + 1 by omega]486 have := (fmem (j - J)).2487 rwa [show J + (j - J) = j by omega] at this488 refine ⟨curveLimitMk R t x beta G ⟨p, hp⟩, ?_⟩489 apply Subtype.ext490 rw [hπ]491 change (curveIdealLattice R t x beta G J).mkQ (f (J - J)) = _492 rw [Nat.sub_self, f0, haq]493 494/-- Every element of the overlap is, modulo the `n`-th power of the exceptional ideal, a495difference `a - β(b)` of functions on the two charts. -/496private theorem two_chart_additive_approximation (R : Type) [CommRing R] (t x : R)497 (hreg : RegularParameterPair R t x) (beta : (BlowupChart R x t) →+* (BlowupOverlap R t x))498 (hbase : ∀ r : R, beta (chartBase R x t r) =499 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x r))500 (hslope : beta (chartSlope R x t) = IsLocalization.Away.invSelf (chartSlope R t x)) (n : ℕ)501 (w : (BlowupOverlap R t x)) :502 ∃ a : (BlowupChart R t x), ∃ b : (BlowupChart R x t),503 w - ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) a - beta b) ∈504 (Ideal.span {(algebraMap (BlowupChart R t x) (BlowupOverlap R t x))505 (chartBase R t x t)})^n := by506 induction n with507 | zero => exact ⟨0, 0, by simp⟩508 | succ n ih =>509 obtain ⟨a, b, hab⟩ := ih510 obtain ⟨c, d, -, -, hcd⟩ := two_chart_layer_correction R t x hreg beta hbase511 hslope n 0 (Nat.zero_le _) _ hab512 refine ⟨a + c, b + d, ?_⟩513 simp only [pow_zero, one_mul] at hcd514 convert hcd using 1515 rw [map_add, map_add]; ring516 517/-- Every multiple `G.left j * c` on the overlap is the untwisted Čech differential of a level-`j`518curve section, modulo the `j`-th power of the exceptional ideal. -/519theorem curve_sections_cover_overlap (R : Type) [CommRing R] (t x : R)520 (beta : BlowupRestriction R t x) (d : ℕ) (G : GluedGenerators R t x beta d)521 (hreg : RegularParameterPair R t x) (j : ℕ) (c : BlowupOverlap R t x) :522 ∃ p ∈ curveSections R t x beta G j, fullCechDifferential R t x beta 0 p -523 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j) * c ∈524 (Ideal.span {overlapException R t x})^j := by525 obtain ⟨a, b, hab⟩ := two_chart_additive_approximation R t x hreg526 (beta.right : BlowupChart R x t →+* BlowupOverlap R t x) (beta_right_chartBase beta)527 beta.slope j528 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j) * c)529 have hdiff : fullCechDifferential R t x beta 0 (a, b)530 = (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) a - beta.right b := by531 simp [fullCechDifferential, ringCechDifferential]532 have key : fullCechDifferential R t x beta 0 (a, b)533 - (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j) * c534 ∈ (Ideal.span {overlapException R t x})^j := by535 rw [hdiff]536 have := (Ideal.neg_mem_iff _).2 hab537 convert this using 1538 · rfl539 · change _ - beta.right b - _ = -(_ - (_ - beta.right b)); ring540 refine ⟨(a, b), ?_, key⟩541 change fullCechDifferential R t x beta 0 (a, b) ∈ overlapCurveIdeal R t x beta G j542 have : fullCechDifferential R t x beta 0 (a, b)543 = (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j) * c544 + (fullCechDifferential R t x beta 0 (a, b)545 - (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (G.left j) * c) := by ring546 rw [this]547 exact Ideal.add_mem _548 (Ideal.mem_sup_left (Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)))549 (Ideal.mem_sup_right key)550 551/-- Layer correction with nonnegative twist: every `w` in the `j`-th power of the exceptional ideal552of the overlap agrees modulo the `(j + 1)`-st power with `a - zᵈ β(b)`, where `a`, `b` lie in the553`j`-th powers of the exceptional ideals of the two charts. -/554private theorem two_chart_layer_correction_positive (R : Type) [CommRing R] (t x : R)555 (beta : BlowupRestriction R t x) (hreg : RegularParameterPair R t x) (j d : ℕ)556 (w : BlowupOverlap R t x) (hw : w ∈ (Ideal.span {overlapException R t x}) ^ j) :557 ∃ a ∈ (chartExceptional R t x)^j, ∃ b ∈ (chartExceptional R x t)^j, w -558 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) a - (overlapSlope R t x)^d *559 beta.right b) ∈ (Ideal.span {overlapException R t x})^(j+1) := by560 obtain ⟨a, ha, b, hb, h⟩ := two_chart_layer_correction_zpow R t x hreg beta.right561 (beta_right_chartBase beta) beta.slope j d (by omega) w hw562 exact ⟨a, ha, b, hb, by rwa [selfZPow_natCast] at h⟩563 564/-! ### Gluing generators level by level -/565 566private theorem isUnit_mk_map {A C : Type} [CommRing A] [CommRing C] (f : A →+* C) (I : Ideal A)567 (J : Ideal C) (h : ∀ a ∈ I, f a ∈ J) (a : A) (ha : IsUnit (Ideal.Quotient.mk I a)) :568 IsUnit (Ideal.Quotient.mk J (f a)) :=569 ha.map (Ideal.quotientMap J f h)570 571private theorem injective_unit_mul_mul {Q : Type} [CommRing Q] (U g : Q) (hU : IsUnit U)572 (hg : Function.Injective (fun c : Q => g * c)) :573 Function.Injective (fun c : Q => (U * g) * c) := by574 obtain ⟨u, rfl⟩ := hU575 intro a b hab576 apply hg577 simpa [mul_assoc] using congrArg (fun y => (↑u⁻¹ : Q) * y) hab578 579private theorem exists_unit_eq_mul_of_span_eq {Q : Type} [CommRing Q] (g F : Q)580 (hg : Function.Injective (fun c : Q => g * c)) (h : Ideal.span {F} = Ideal.span {g}) :581 ∃ u : Qˣ, F = (u : Q) * g := by582 apply regular_principal_generators_associated Q g F583 · intro a b hab; apply hg; simpa [mul_comm] using hab584 · exact h.symm585 586private theorem chart_generator_step {A : Type} [CommRing A] (T : A) (j : ℕ) (hj : 1 ≤ j)587 (g g' F : A)588 (hg' : Ideal.span {Ideal.Quotient.mk ((Ideal.span {T})^j) g'} =589 Ideal.span {Ideal.Quotient.mk ((Ideal.span {T})^j) g})590 (hreg : Function.Injective (fun c : A ⧸ (Ideal.span {T})^j =>591 Ideal.Quotient.mk ((Ideal.span {T})^j) g * c))592 (hF : Ideal.span {Ideal.Quotient.mk ((Ideal.span {T})^j) F} =593 Ideal.span {Ideal.Quotient.mk ((Ideal.span {T})^j) g}) :594 ∃ w : A, IsUnit (Ideal.Quotient.mk ((Ideal.span {T})^(j+1)) w) ∧595 w * g' - F ∈ (Ideal.span {T})^j ∧596 Ideal.span {Ideal.Quotient.mk ((Ideal.span {T})^(j+1)) (w * g')} =597 Ideal.span {Ideal.Quotient.mk ((Ideal.span {T})^(j+1)) g'} := by598 obtain ⟨u1, hu1⟩ := exists_unit_eq_mul_of_span_eq _ _ hreg hg'599 obtain ⟨u, hu⟩ := exists_unit_eq_mul_of_span_eq _ _ hreg hF600 obtain ⟨w, hwu, hw⟩ := principal_power_unit_lift A T j hj601 ((u * u1⁻¹ : _ˣ) : A ⧸ (Ideal.span {T})^j) (Units.isUnit _)602 refine ⟨w, hwu, ?_, ?_⟩603 · rw [← Ideal.Quotient.eq, map_mul, hw, hu1, hu]604 simp only [Units.val_mul]605 rw [mul_assoc, Units.inv_mul_cancel_left]606 · obtain ⟨v, hv⟩ := hwu607 rw [map_mul, ← hv]608 exact Ideal.span_singleton_mul_left_unit v.isUnit _609 610private theorem span_mk_mul_eq_of_mul_one_add {S : Type} [CommRing S] (I : Ideal S)611 (a' a F g : S) (h : a' * (1 + a) - 1 ∈ I)612 (hF : Ideal.span {Ideal.Quotient.mk I F} = Ideal.span {Ideal.Quotient.mk I g}) :613 Ideal.span {Ideal.Quotient.mk I (a' * F)} = Ideal.span {Ideal.Quotient.mk I g} := by614 have h1 : Ideal.Quotient.mk I a' * Ideal.Quotient.mk I (1 + a) = 1 := by615 rw [← map_mul, ← sub_eq_zero, ← map_one (Ideal.Quotient.mk I), ← map_sub,616 Ideal.Quotient.eq_zero_iff_mem]617 exact h618 rw [map_mul]619 exact (Ideal.span_singleton_mul_left_unit ⟨⟨_, _, h1, by rw [mul_comm, h1]⟩, rfl⟩ _).trans hF620 621private theorem glued_step_combination {S : Type} [CommRing S] (J : Ideal S) (X aF Y P v γ β : S)622 (hv : aF - v * P ∈ J) (hcd : v - 1 - (γ - β) ∈ J) (h3 : X * (1 + γ) - 1 ∈ J)623 (h4 : Y * (1 + β) - 1 ∈ J) (h5 : (v - 1) * β ∈ J) : X * aF - Y * P ∈ J := by624 have : X * aF - Y * P = X * (aF - v * P) + P * (-(X * v) * (Y * (1 + β) - 1) +625 Y * (X * (1 + γ) - 1) + X * Y * ((v - 1 - (γ - β)) + (v - 1) * β)) := by ring626 rw [this]627 refine J.add_mem (J.mul_mem_left _ hv) (J.mul_mem_left _ ?_)628 exact J.add_mem (J.add_mem (J.mul_mem_left _ h4) (J.mul_mem_left _ h3))629 (J.mul_mem_left _ (J.add_mem hcd h5))630 631private theorem mul_mem_pow_succ {S : Type} [CommRing S] (I : Ideal S) {j : ℕ} (hj : 1 ≤ j)632 {a b : S} (ha : a ∈ I ^ j) (hb : b ∈ I ^ j) : a * b ∈ I ^ (j + 1) := by633 have := Ideal.mul_mem_mul ha hb634 rw [← pow_add] at this635 exact Ideal.pow_le_pow_right (by omega) this636 637/-- For `a ∈ I^j` (`j ≥ 1`), `1 + a` is invertible modulo `I^(j+1)` with inverse `≡ 1 mod I^j`. -/638private theorem exists_inv_one_add {S : Type} [CommRing S] (I : Ideal S) {j : ℕ} (hj : 1 ≤ j)639 {a : S} (ha : a ∈ I ^ j) : ∃ a' : S, a' * (1 + a) - 1 ∈ I ^ (j + 1) ∧ a' - 1 ∈ I ^ j := by640 have hn : IsNilpotent (Ideal.Quotient.mk (I ^ (j + 1)) a) :=641 ⟨2, by642 rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem, pow_two]; exact mul_mem_pow_succ I hj ha ha⟩643 have hu := hn.isUnit_one_add644 obtain ⟨a', ha'⟩ :=645 Ideal.Quotient.mk_surjective ((hu.unit⁻¹ : (S ⧸ I ^ (j + 1))ˣ) : S ⧸ I ^ (j + 1))646 have h1 : a' * (1 + a) - 1 ∈ I ^ (j + 1) := by647 rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_mul, ha', map_add, map_one,648 hu.val_inv_mul, sub_self]649 refine ⟨a', h1, ?_⟩650 rw [show a' - 1 = (a' * (1 + a) - 1) - a' * a by ring]651 exact Ideal.sub_mem _ (Ideal.pow_le_pow_right (Nat.le_succ j) h1) (Ideal.mul_mem_left _ _ ha)652 653/-- If `g` is regular modulo `I` and `F` generates the same ideal as `g` there, then a unit654multiple of `f F` is regular modulo `J` whenever `f g` is. -/655private theorem injective_mk_mul_of_span_eq {A C : Type} [CommRing A] [CommRing C] (f : A →+* C)656 (I : Ideal A) (J : Ideal C) (hIJ : ∀ a ∈ I, f a ∈ J) (g F : A) (z : C)657 (hz : IsUnit (Ideal.Quotient.mk J z))658 (hreg : Function.Injective (fun c : A ⧸ I => Ideal.Quotient.mk I g * c))659 (hF : Ideal.span {Ideal.Quotient.mk I F} = Ideal.span {Ideal.Quotient.mk I g})660 (hregJ : Function.Injective (fun c : C ⧸ J => Ideal.Quotient.mk J (f g) * c)) :661 Function.Injective (fun c : C ⧸ J => Ideal.Quotient.mk J (z * f F) * c) := by662 obtain ⟨u, hu⟩ := exists_unit_eq_mul_of_span_eq _ _ hreg hF663 obtain ⟨b, hb⟩ := Ideal.Quotient.mk_surjective (u : A ⧸ I)664 have hbu : IsUnit (Ideal.Quotient.mk J (f b)) :=665 isUnit_mk_map f I J hIJ b (by rw [hb]; exact u.isUnit)666 have hdiff : F - b * g ∈ I := by rw [← Ideal.Quotient.eq, map_mul, hb, hu]667 have hdiff' := hIJ _ hdiff668 rw [map_sub, ← Ideal.Quotient.eq, map_mul] at hdiff'669 have : Ideal.Quotient.mk J (z * f F) =670 (Ideal.Quotient.mk J z * Ideal.Quotient.mk J (f b)) * Ideal.Quotient.mk J (f g) := by671 rw [map_mul, hdiff', map_mul, mul_assoc]672 rw [this]673 exact injective_unit_mul_mul _ _ (hz.mul hbu) hregJ674 675/-- If `p ≡ u q` modulo `J` for a unit `u` and `b`, `z` are units modulo `J`, then `a p` is676congruent modulo `J` to some multiple of `z (b q)`. -/677private theorem exists_mul_sub_mul_mem {C : Type} [CommRing C] (J : Ideal C) (a b p q z : C)678 (hb : IsUnit (Ideal.Quotient.mk J b)) (hz : IsUnit (Ideal.Quotient.mk J z))679 (u : (C ⧸ J)ˣ) (hu : Ideal.Quotient.mk J p = u * Ideal.Quotient.mk J q) :680 ∃ v : C, a * p - v * (z * (b * q)) ∈ J := by681 obtain ⟨v, hv⟩ := Ideal.Quotient.mk_surjective682 (Ideal.Quotient.mk J a * (u : C ⧸ J) * ((hb.unit⁻¹ : (C ⧸ J)ˣ) : C ⧸ J) *683 ((hz.unit⁻¹ : (C ⧸ J)ˣ) : C ⧸ J))684 refine ⟨v, ?_⟩685 rw [← Ideal.Quotient.eq, map_mul, map_mul, map_mul, map_mul, hu, hv]686 have e1 := hb.mul_val_inv687 have e2 := hz.mul_val_inv688 linear_combination (Ideal.Quotient.mk J a * (u : C ⧸ J) * Ideal.Quotient.mk J q) *689 (-(Ideal.Quotient.mk J z * ((hz.unit⁻¹ : (C ⧸ J)ˣ) : C ⧸ J)) * e1 - e2)690 691/-- One step of the gluing: chart representatives `FA`, `FB` of the level-`j` generators that agree692on the overlap modulo the `j`-th exceptional power can be corrected, modulo the `j`-th powers, to693representatives of the level-`(j + 1)` generators agreeing modulo the `(j + 1)`-st power. -/694private theorem glued_generators_succ (R : Type) [CommRing R] (t x : R)695 (beta : BlowupRestriction R t x) (hreg : RegularParameterPair R t x) (d : ℕ)696 (gA : ℕ → BlowupChart R t x) (gB : ℕ → BlowupChart R x t)697 (hA : ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (gA (j+1))} =698 Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (gA j)})699 (hB : ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (gB (j+1))} =700 Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (gB j)})701 (hregA : ∀ j : ℕ, Function.Injective (fun c : BlowupChart R t x ⧸ (chartExceptional R t x)^j =>702 Ideal.Quotient.mk ((chartExceptional R t x)^j) (gA j) * c))703 (hregBc : ∀ j : ℕ, Function.Injective (fun c : BlowupChart R x t ⧸ (chartExceptional R x t)^j =>704 Ideal.Quotient.mk ((chartExceptional R x t)^j) (gB j) * c))705 (hoverlap : ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j)706 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (gA j))} =707 Ideal.span {Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j) (beta.right (gB j))})708 (hregC : ∀ j : ℕ, Function.Injective (fun c : BlowupOverlap R t x ⧸709 (Ideal.span {overlapException R t x})^j =>710 Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j) (beta.right (gB j)) * c))711 (j : ℕ) (hj : 1 ≤ j) (FA : BlowupChart R t x) (FB : BlowupChart R x t)712 (hIA : Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) FA} =713 Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (gA j)})714 (hIB : Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) FB} =715 Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (gB j)})716 (hIC : (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) FA - (overlapSlope R t x)^d *717 beta.right FB ∈ (Ideal.span {overlapException R t x})^j) :718 ∃ (FA' : BlowupChart R t x) (FB' : BlowupChart R x t), FA' - FA ∈ (chartExceptional R t x)^j ∧719 FB' - FB ∈ (chartExceptional R x t)^j ∧720 Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^(j+1)) FA'} =721 Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^(j+1)) (gA (j+1))} ∧722 Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^(j+1)) FB'} =723 Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^(j+1)) (gB (j+1))} ∧724 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) FA' - (overlapSlope R t x)^d *725 beta.right FB' ∈ (Ideal.span {overlapException R t x})^(j+1) := by726 set α := algebraMap (BlowupChart R t x) (BlowupOverlap R t x) with hα727 set E := Ideal.span {overlapException R t x} with hE728 set Z := overlapSlope R t x with hZ729 have TA : ∀ m (a : BlowupChart R t x), a ∈ (chartExceptional R t x)^m → α a ∈ E^m :=730 algebraMap_mem_overlap_pow731 have TB : ∀ m (b : BlowupChart R x t), b ∈ (chartExceptional R x t)^m → beta.right b ∈ E^m :=732 beta_right_mem_overlap_pow beta733 have hZu : ∀ m, IsUnit (Ideal.Quotient.mk (E^m) (Z^d)) :=734 fun _ => ((IsLocalization.Away.algebraMap_isUnit _).pow d).map _735 -- normalize the level-`(j + 1)` generators on each chart736 obtain ⟨wA, hwAu, hwA, hwAI⟩ := chart_generator_step (chartBase R t x t) j hj (gA j)737 (gA (j+1)) FA (hA j) (hregA j) hIA738 obtain ⟨wB, hwBu, hwB, hwBI⟩ := chart_generator_step (chartBase R x t x) j hj (gB j)739 (gB (j+1)) FB (hB j) (hregBc j) hIB740 -- the transition unit `v` between the normalized representatives on the overlap741 obtain ⟨u2, hu2⟩ := exists_unit_eq_mul_of_span_eq _ _ (hregC (j+1)) (hoverlap (j+1))742 obtain ⟨v, hv⟩ := exists_mul_sub_mul_mem (E^(j+1)) (α wA) (beta.right wB) (α (gA (j+1)))743 (beta.right (gB (j+1))) (Z^d)744 (isUnit_mk_map beta.right.toRingHom _ _ (fun y hy => TB (j+1) y hy) wB hwBu) (hZu _) u2 hu2745 rw [← map_mul, ← map_mul] at hv746 have hv1 : v - 1 ∈ E^j := transition_unit_congruent_one R t x beta d j FA _ FB _ hwA hwB hIC747 (injective_mk_mul_of_span_eq beta.right.toRingHom _ _ (fun y hy => TB j y hy) _ FB _748 (hZu j) (hregBc j) hIB (hregC j))749 v (Ideal.pow_le_pow_right (Nat.le_succ j) hv)750 -- correct `v` by a Čech coboundary `c - d1`751 obtain ⟨c, hc, d1, hd1, hcd⟩ :=752 two_chart_layer_correction_positive R t x beta hreg j 0 (v - 1) hv1753 rw [pow_zero, one_mul] at hcd754 obtain ⟨c', hc'1, hc'2⟩ := exists_inv_one_add _ hj hc755 obtain ⟨d', hd'1, hd'2⟩ := exists_inv_one_add _ hj hd1756 refine ⟨c' * (wA * gA (j+1)), d' * (wB * gB (j+1)), ?_, ?_, ?_, ?_, ?_⟩757 · rw [show c' * (wA * gA (j+1)) - FA = (c' - 1) * (wA * gA (j+1)) + (wA * gA (j+1) - FA) by758 ring]759 exact Ideal.add_mem _ (Ideal.mul_mem_right _ _ hc'2) hwA760 · rw [show d' * (wB * gB (j+1)) - FB = (d' - 1) * (wB * gB (j+1)) + (wB * gB (j+1) - FB) by761 ring]762 exact Ideal.add_mem _ (Ideal.mul_mem_right _ _ hd'2) hwB763 · exact span_mk_mul_eq_of_mul_one_add _ c' c _ (gA (j+1)) hc'1 hwAI764 · exact span_mk_mul_eq_of_mul_one_add _ d' d1 _ (gB (j+1)) hd'1 hwBI765 · have h3 := TA (j+1) _ hc'1766 have h4 := TB (j+1) _ hd'1767 rw [map_sub, map_mul, map_add, map_one] at h3 h4768 rw [map_mul α c', map_mul beta.right d', mul_left_comm (Z^d)]769 exact glued_step_combination _ (α c') _ (beta.right d') _ v (α c) (beta.right d1) hv hcd h3 h4770 (mul_mem_pow_succ E hj hv1 (TB j d1 hd1))771 772/-- Compatible systems of chart generators `gA`, `gB` that are regular, agree on the overlap and are773normalized at level one can be replaced by glued generators generating the same ideals at every774level. -/775theorem glued_generators_exist (R : Type) [CommRing R] (t x : R) (beta : BlowupRestriction R t x)Lemma 4.3776 (hreg : RegularParameterPair R t x) (d : ℕ)777 (gA : ℕ → BlowupChart R t x) (gB : ℕ → BlowupChart R x t)778 (hA : ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (gA (j+1))} =779 Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (gA j)})780 (hB : ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (gB (j+1))} =781 Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (gB j)})782 (hregA : ∀ j : ℕ, Function.Injective (fun c : BlowupChart R t x ⧸ (chartExceptional R t x)^j =>783 Ideal.Quotient.mk ((chartExceptional R t x)^j) (gA j) * c))784 (hregBc : ∀ j : ℕ, Function.Injective (fun c : BlowupChart R x t ⧸ (chartExceptional R x t)^j =>785 Ideal.Quotient.mk ((chartExceptional R x t)^j) (gB j) * c))786 (hoverlap : ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j)787 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (gA j))} =788 Ideal.span {Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j) (beta.right (gB j))})789 (hregC : ∀ j : ℕ, Function.Injective (fun c : BlowupOverlap R t x ⧸790 (Ideal.span {overlapException R t x})^j =>791 Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j) (beta.right (gB j)) * c))792 (hnorm : ∃ u : Rˣ, (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (gA 1) - algebraMap793 R (BlowupOverlap R t x) (u : R) * ((overlapSlope R t x)^d * beta.right (gB 1)) ∈794 (Ideal.span {overlapException R t x})) :795 ∃ G : GluedGenerators R t x beta d, ∀ j : ℕ,796 Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)} =797 Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (gA j)} ∧798 Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)} =799 Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (gB j)} := by800 let A := BlowupChart R t x801 let B := BlowupChart R x t802 let Inv : ℕ → A × B → Prop := fun j p =>803 Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) p.1} =804 Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (gA j)} ∧805 Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) p.2} =806 Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (gB j)} ∧807 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) p.1 - (overlapSlope R t x)^d *808 beta.right p.2 ∈ (Ideal.span {overlapException R t x})^j809 have hstep : ∀ n : ℕ, ∀ p : {p : A × B // Inv (n+1) p}, ∃ q : A × B,810 (q.1 - p.1.1 ∈ (chartExceptional R t x)^(n+1) ∧811 q.2 - p.1.2 ∈ (chartExceptional R x t)^(n+1)) ∧ Inv (n+2) q := by812 intro n p813 obtain ⟨FA', FB', h1, h2, h3⟩ := glued_generators_succ R t x beta hreg d gA gB hA hB hregA814 hregBc hoverlap hregC (n+1) (by omega) p.1.1 p.1.2 p.2.1 p.2.2.1 p.2.2.2815 exact ⟨(FA', FB'), ⟨h1, h2⟩, h3⟩816 obtain ⟨FA1, FB1, h1⟩ := glued_generators_level_one R t x beta d (gA 1) (gB 1) hnorm817 choose next hnext using hstep818 let seq : ∀ n : ℕ, {p : A × B // Inv (n+1) p} := fun n =>819 Nat.rec ⟨(FA1, FB1), h1⟩ (fun n p => ⟨next n p, (hnext n p).2⟩) n820 let left : ℕ → A := fun j => match j with | 0 => gA 0 | n+1 => (seq n).1.1821 let right : ℕ → B := fun j => match j with | 0 => gB 0 | n+1 => (seq n).1.2822 refine ⟨⟨left, right, ?_, ?_, ?_⟩, ?_⟩ <;> rintro (_ | n)823 · simp824 · exact (hnext n (seq n)).1.1825 · simp826 · exact (hnext n (seq n)).1.2827 · simp828 · exact (seq n).2.2.2829 · exact ⟨rfl, rfl⟩830 · exact ⟨(seq n).2.1, (seq n).2.2.1⟩831 832/-! ### Transport of transversality and finite contact along completion isomorphisms -/833 834section TransportCompletion835 836variable {S T : Type} [CommRing S] [CommRing T]837 838private theorem injective_mk_mul_iff (g e : S) :839 Function.Injective (fun a : S ⧸ Ideal.span {g} => Ideal.Quotient.mk (Ideal.span {g}) e * a) ↔840 ∀ a, e * a ∈ Ideal.span {g} → a ∈ Ideal.span {g} := by841 constructor842 · intro h a ha843 rw [← Ideal.Quotient.eq_zero_iff_mem]844 apply h845 simp only [mul_zero]846 rw [← map_mul, Ideal.Quotient.eq_zero_iff_mem]847 exact ha848 · intro h a b hab849 induction a using Quotient.inductionOn' with | h a => ?_850 induction b using Quotient.inductionOn' with | h b => ?_851 change Ideal.Quotient.mk _ a = Ideal.Quotient.mk _ b852 change Ideal.Quotient.mk _ e * Ideal.Quotient.mk _ a =853 Ideal.Quotient.mk _ e * Ideal.Quotient.mk _ b at hab854 rw [← map_mul, ← map_mul, Ideal.Quotient.eq] at hab855 rw [Ideal.Quotient.eq]856 apply h857 rw [mul_sub]; exact hab858 859/-- Transversality transports along a ring isomorphism `Θ` sending the parameter `e` to a unit860multiple of `eT`: if multiplication by `e` is injective modulo `g`, then multiplication by `eT` is861injective modulo `Θ g`. -/862theorem mul_injective_quotient_transport (Θ : S ≃+* T) {g e : S} {eT u : T} (hu : IsUnit u)863 (he : Θ e * u = eT)864 (h : Function.Injective865 (fun a : S ⧸ Ideal.span {g} => Ideal.Quotient.mk (Ideal.span {g}) e * a)) :866 Function.Injective867 (fun a : T ⧸ Ideal.span {Θ g} => Ideal.Quotient.mk (Ideal.span {Θ g}) eT * a) := by868 rw [injective_mk_mul_iff] at h ⊢869 intro b hb870 rw [← he, mul_assoc, Ideal.mem_span_singleton] at hb871 have h1 := h (Θ.symm (u * b)) (Ideal.mem_span_singleton.mpr (by simpa using map_dvd Θ.symm hb))872 rw [Ideal.mem_span_singleton, ← hu.dvd_mul_left]873 simpa using map_dvd Θ (Ideal.mem_span_singleton.mp h1)874 875private theorem sup_pow_le (I J : Ideal S) (j : ℕ) : (I ⊔ J) ^ j ≤ I ⊔ J ^ j := by876 induction j with877 | zero => simp878 | succ n ih =>879 calc (I ⊔ J) ^ (n+1) = (I ⊔ J) * (I ⊔ J) ^ n := pow_succ' _ _880 _ ≤ (I ⊔ J) * (I ⊔ J ^ n) := Ideal.mul_mono_right ih881 _ ≤ I ⊔ J ^ (n+1) := by882 rw [Ideal.sup_mul, Ideal.mul_sup, Ideal.mul_sup, pow_succ']883 exact sup_le (sup_le (le_sup_of_le_left Ideal.mul_le_right)884 (le_sup_of_le_left Ideal.mul_le_left))885 (sup_le (le_sup_of_le_left Ideal.mul_le_right) le_sup_right)886 887private theorem exists_pow_le_span_pair {M : Ideal S} {g e : S}888 (h : ∃ L, M ^ L ≤ Ideal.span {g, e ^ 1}) (j : ℕ) : ∃ L, M ^ L ≤ Ideal.span {g, e ^ j} := by889 obtain ⟨L, hL⟩ := h890 refine ⟨L * j, ?_⟩891 rw [pow_mul]892 refine (Ideal.pow_right_mono hL j).trans ?_893 rw [Ideal.span_insert, Ideal.span_insert, pow_one, ← Ideal.span_singleton_pow]894 exact sup_pow_le _ _ j895 896/-- Finite contact transports along a ring isomorphism `Θ` sending the parameter `e` to a unit897multiple of `eT`: if a power of `MS` lies in `(g, e)` and `MT ⊆ Θ(MS)`, then for every `j` a power898of `MT` lies in `(Θ g, eT^j)`. -/899theorem exists_pow_le_span_pair_transport (Θ : S ≃+* T) {g e : S} {eT u : T} (hu : IsUnit u)900 (he : Θ e * u = eT) {MS : Ideal S} {MT : Ideal T} (hM : MT ≤ MS.map Θ)901 (h : ∃ L, MS ^ L ≤ Ideal.span {g, e ^ 1}) (j : ℕ) :902 ∃ L, MT ^ L ≤ Ideal.span {Θ g, eT ^ j} := by903 refine exists_pow_le_span_pair ?_ j904 obtain ⟨L, hL⟩ := h905 refine ⟨L, (Ideal.pow_right_mono hM L).trans ?_⟩906 rw [← Ideal.map_pow]907 refine (Ideal.map_mono hL).trans ?_908 rw [Ideal.map_span, Set.image_pair, Ideal.span_le]909 rintro _ (rfl | rfl)910 · exact Ideal.subset_span (Set.mem_insert _ _)911 · obtain ⟨v, rfl⟩ := hu912 have : Θ e = eT * ↑v⁻¹ := by rw [← he, mul_assoc, Units.mul_inv, mul_one]913 simp only [this, pow_one]914 exact Ideal.mul_mem_right _ _ (Ideal.subset_span (Set.mem_insert_of_mem _ rfl))915 916end TransportCompletion917 918/-- The maximal ideal of `A_P` generates in the completion `(A_P)^` the extension of `P`. -/919theorem map_maximalIdeal_localCompletion {A : Type} [CommRing A] (P : Ideal A) [P.IsPrime] :920 (IsLocalRing.maximalIdeal (Localization.AtPrime P)).map921 (localCompletionMap (Localization.AtPrime P)) =922 P.map (completedPointMap A P) := by923 calc _ = (P.map (algebraMap A (Localization.AtPrime P))).map924 (localCompletionMap (Localization.AtPrime P)) := by925 rw [Localization.AtPrime.map_eq_maximalIdeal]926 _ = _ := by rw [Ideal.map_map]; rfl927 928/-- A ring isomorphism `Θ : (B_Q)^ ≃ (A_P)^` compatible with `f : A → B` carries the extension of929`f(P)` to the maximal ideal of `(A_P)^`. -/930theorem map_maximalIdeal_localCompletion_transport {A B : Type} [CommRing A] [CommRing B]931 (f : A →+* B) (P : Ideal A) (Q : Ideal B) [P.IsPrime] [Q.IsPrime]932 (Θ : CompletedLocalAt B Q ≃+* CompletedLocalAt A P)933 (hΘ : ∀ a, Θ (completedPointMap B Q (f a)) = completedPointMap A P a) :934 ((P.map f).map (completedPointMap B Q)).map (Θ : _ →+* _) =935 (IsLocalRing.maximalIdeal (Localization.AtPrime P)).map (localCompletionMap _) := by936 rw [map_maximalIdeal_localCompletion, Ideal.map_map, Ideal.map_map]937 exact congrArg (Ideal.map · P) (RingHom.ext hΘ)938 939/-- For a ring isomorphism `Θ : (B_Q)^ ≃ (A_{f⁻¹Q})^` compatible with `f : A → B`, the maximal ideal940of `(A_{f⁻¹Q})^` is contained in the image under `Θ` of the maximal ideal of `(B_Q)^`. -/941theorem map_maximalIdeal_localCompletion_comap_le {A B : Type} [CommRing A] [CommRing B]942 (f : A →+* B) (Q : Ideal B) [Q.IsPrime]943 (Θ : CompletedLocalAt B Q ≃+* CompletedLocalAt A (Q.comap f))944 (hΘ : ∀ a, Θ (completedPointMap B Q (f a)) = completedPointMap A (Q.comap f) a) :945 (IsLocalRing.maximalIdeal (Localization.AtPrime (Q.comap f))).map (localCompletionMap _) ≤946 ((IsLocalRing.maximalIdeal (Localization.AtPrime Q)).map (localCompletionMap _)).map947 (Θ : _ →+* _) := by948 rw [← map_maximalIdeal_localCompletion_transport f _ Q Θ hΘ, map_maximalIdeal_localCompletion Q]949 exact Ideal.map_mono (Ideal.map_mono Ideal.map_comap_le)950 951/-- Chart-independent form of the strict-transform equation: let `P` be finitely many distinct952maximal ideals of a noetherian ring `A` containing `z`, with local equations `g` of finite contact953with `z`, and let `F` be generators of the level kernels, `(F j) + (z)^j = ⋂ (g, z^j)`. If954`y ≡ z^d F j mod z^j` for every `j` and `z`, `g` form a regular sequence in `(A_P)^`, then955`y = z^d · g · unit` in `(A_P)^`. -/956theorem strict_transform_equation_of_kernels {A ι : Type} [CommRing A] [IsNoetherianRing A]957 [Finite ι] (P : ι → Ideal A) [∀ s, (P s).IsMaximal] (hP : Function.Injective P) (z : A)958 (hz : ∀ s, z ∈ P s) (g : ∀ s, CompletedLocalAt A (P s))959 (hfin : ∀ j s, ∃ L, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P s))).map960 (localCompletionMap _)) ^ L ≤ finiteLocalCurveIdeal A (P s) z (g s) j)961 (F : ℕ → A) (hF : ∀ j, Ideal.span {F j} ⊔ Ideal.span {z} ^ j =962 finiteSupportKernel A ι P (fun s => finiteLocalCurveIdeal A (P s) z (g s) j))963 (d : ℕ) (y : A) (hy : ∀ j, y - z ^ d * F j ∈ Ideal.span {z} ^ j) (s : ι)964 [IsNoetherianRing (CompletedLocalAt A (P s))]965 (hereg : Function.Injective966 (fun a : CompletedLocalAt A (P s) => completedPointMap A (P s) z * a))967 (hgreg : Function.Injective (fun a : CompletedLocalAt A (P s) ⧸968 Ideal.span {completedPointMap A (P s) z} =>969 Ideal.Quotient.mk (Ideal.span {completedPointMap A (P s) z}) (g s) * a)) :970 ∃ v : (CompletedLocalAt A (P s))ˣ, completedPointMap A (P s) y =971 completedPointMap A (P s) z ^ d * g s * (v : CompletedLocalAt A (P s)) := by972 set φ := completedPointMap A (P s)973 have he : φ z ∈ IsLocalRing.maximalIdeal (CompletedLocalAt A (P s)) := by974 have h1 : algebraMap A (Localization.AtPrime (P s)) z ∈975 IsLocalRing.maximalIdeal (Localization.AtPrime (P s)) := by976 rw [Localization.AtPrime.map_eq_maximalIdeal.symm]977 exact Ideal.mem_map_of_mem _ (hz s)978 have := AdicCompletion.algebraMap_isLocalHom_of_fg (R := Localization.AtPrime (P s))979 (IsNoetherian.noetherian _)980 have : IsLocalHom (localCompletionMap (Localization.AtPrime (P s))) := this981 exact map_nonunit (localCompletionMap (Localization.AtPrime (P s))) _ h1982 refine strict_transform_equation_from_levels _ (φ z) (g s) he hereg hgreg d (fun j => φ (F j))983 (fun j => ?_) _ (fun j => ?_)984 · have hrec := finite_support_completion_recovers A ι P hP (fun s => (hfin j s).choose) _985 (fun s => (hfin j s).choose_spec) s986 rw [← hF, Ideal.map_sup, Ideal.map_span, Ideal.map_pow, Ideal.map_span, Set.image_singleton,987 Set.image_singleton, Ideal.span_singleton_pow, finiteLocalCurveIdeal] at hrec988 rw [← hrec, Ideal.span_insert]989 · have := Ideal.mem_map_of_mem φ (hy j)990 rw [Ideal.map_pow, Ideal.map_span, Set.image_singleton, Ideal.span_singleton_pow] at this991 simpa [map_sub, map_mul, map_pow] using this992 993/-! ### Two-chart curve data -/994 995/-- At every point of the first chart in two-chart curve data, the exceptional parameter is a996nonzerodivisor modulo the local equation, and some power of the maximal ideal of the completion lies997in the level-`j` local curve ideal. -/998theorem two_chart_left_data_transverse_finite (R : Type) [CommRing R] (t x : R)999 (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta) (j : ℕ) :1000 (∀ s, Function.Injective (fun a : CompletedLocalAt (BlowupChart R t x) (leftPoint D s) ⧸1001 Ideal.span {leftData D s} => Ideal.Quotient.mk (Ideal.span {leftData D s})1002 (completedPointMap (BlowupChart R t x) (leftPoint D s) (chartBase R t x t)) * a)) ∧ ∀ s, ∃ L :1003 ℕ, ((IsLocalRing.maximalIdeal (Localization.AtPrime (leftPoint D s))).map (localCompletionMap1004 (Localization.AtPrime (leftPoint D s))))^L ≤ leftLevelIdeal D j s := by1005 have he (i : D.ι) : D.leftIso i (completedPointMap _ (D.Q i) (overlapException R t x)) * 1 =1006 completedPointMap _ (leftPoint D (.inl i)) (chartBase R t x t) :=1007 (mul_one _).trans (D.leftIso_compat i _)1008 constructor1009 · rintro (i | k)1010 · exact mul_injective_quotient_transport (D.leftIso i) isUnit_one (he i) (D.transverse i)1011 · exact D.transverse0 k1012 · rintro (i | k)1013 · exact exists_pow_le_span_pair_transport (D.leftIso i) isUnit_one (he i)1014 (map_maximalIdeal_localCompletion_comap_le _ _ _ (D.leftIso_compat i)) (D.finite i) j1015 · exact exists_pow_le_span_pair (D.finite0 k) j1016 1017/-- The points of the first chart in two-chart curve data are distinct maximal ideals lying on the1018exceptional divisor. -/1019theorem two_chart_left_points_maximal (R : Type) [CommRing R] (t x : R)1020 (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)1021 [(Ideal.span ({t,x} : Set R)).IsMaximal] :1022 (∀ s, (leftPoint D s).IsMaximal) ∧ Function.Injective (leftPoint D) ∧ ∀ s, chartBase R t x t ∈1023 leftPoint D s := by1024 have key : ∀ i, ((D.Q i).comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).IsMaximal ∧1025 chartSlope R t x ∉ (D.Q i).comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) ∧1026 chartBase R t x t ∈ (D.Q i).comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) :=1027 fun i => overlap_exceptional_point_comap_maximal R t x (D.Q i) (D.onE i)1028 refine ⟨?_, ?_, ?_⟩1029 · rintro (i | k)1030 · exact (key i).11031 · exact D.maximal0 k1032 · rintro (i | i) (j | j) h1033 · congr 11034 apply D.inj1035 have h' : (D.Q i).comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) =1036 (D.Q j).comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) := h1037 have := congrArg (Ideal.map (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))) h'1038 rwa [IsLocalization.map_under (Submonoid.powers (chartSlope R t x)),1039 IsLocalization.map_under (Submonoid.powers (chartSlope R t x))] at this1040 · exfalso1041 have h' : (D.Q i).comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) = D.P0 j := h1042 exact (key i).2.1 (h' ▸ D.slope0 j)1043 · exfalso1044 have h' : D.P0 i = (D.Q j).comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) := h1045 exact (key j).2.1 (h' ▸ D.slope0 i)1046 · congr 11047 exact D.inj0 h1048 · rintro (i | k)1049 · exact (key i).2.21050 · exact D.onE0 k1051 1052/-- At a point of the first chart, the pullback of the surface function `f` factors in the completed1053local ring as `tᵈ · (local equation) · unit`. -/1054theorem strict_transform_left_point_equation (R : Type) [CommRing R] (t x : R)1055 [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]1056 [IsNoetherianRing (BlowupChart R x t)] (beta : BlowupRestriction R t x)1057 (D : TwoChartCurveData R t x beta) (d : ℕ) (G : GluedGenerators R t x beta d)1058 (hG : ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)} =1059 leftLevelKernel D j ∧ Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)}1060 = rightLevelKernel D j)1061 (f : R)1062 (hf : ∀ j : ℕ, surfaceToCechInput R t x j f =1063 (cechInputLattice R t x j).mkQ (gluedFunctionPair R t x G j))1064 (s : D.ι ⊕ D.ι0) [IsNoetherianRing (CompletedLocalAt (BlowupChart R t x) (leftPoint D s))]1065 (hereg : Function.Injective (fun a : CompletedLocalAt (BlowupChart R t x) (leftPoint D s) =>1066 completedPointMap (BlowupChart R t x) (leftPoint D s) (chartBase R t x t) * a))1067 (hgreg : Function.Injective (fun a : CompletedLocalAt (BlowupChart R t x) (leftPoint D s) ⧸1068 Ideal.span {completedPointMap (BlowupChart R t x) (leftPoint D s) (chartBase R t x t)} =>1069 Ideal.Quotient.mk1070 (Ideal.span {completedPointMap (BlowupChart R t x) (leftPoint D s) (chartBase R t x t)})1071 (leftData D s) * a)) :1072 ∃ v : (CompletedLocalAt (BlowupChart R t x) (leftPoint D s))ˣ, completedPointMap1073 (BlowupChart R t x) (leftPoint D s) (algebraMap R (BlowupChart R t x) f) =1074 (completedPointMap (BlowupChart R t x) (leftPoint D s) (chartBase R t x t))^d * leftData D s *1075 (v : CompletedLocalAt (BlowupChart R t x) (leftPoint D s)) := by1076 obtain ⟨hmax, hinj, hmem⟩ := two_chart_left_points_maximal R t x beta D1077 have : ∀ s, (leftPoint D s).IsMaximal := hmax1078 exact strict_transform_equation_of_kernels (leftPoint D) hinj _ hmem (leftData D)1079 (fun j => (two_chart_left_data_transverse_finite R t x beta D j).2) G.left1080 (fun j => (curve_ideal_lattice_eq_kernels R t x beta D d G hG j).1) d _1081 (glued_function_left_chart R t x beta d G f hf) s hereg hgreg1082 1083/-- At every point of the second chart in two-chart curve data, the exceptional parameter is a1084nonzerodivisor modulo the local equation, and some power of the maximal ideal of the completion lies1085in the level-`j` local curve ideal. -/1086theorem two_chart_right_data_transverse_finite (R : Type) [CommRing R] (t x : R)1087 (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta) (j : ℕ) :1088 (∀ s, Function.Injective (fun a : CompletedLocalAt (BlowupChart R x t) (rightPoint D s) ⧸1089 Ideal.span {rightData D s} => Ideal.Quotient.mk (Ideal.span {rightData D s})1090 (completedPointMap (BlowupChart R x t) (rightPoint D s) (chartBase R x t x)) * a)) ∧ ∀ s, ∃ L1091 : ℕ, ((IsLocalRing.maximalIdeal (Localization.AtPrime (rightPoint D s))).map1092 (localCompletionMap (Localization.AtPrime (rightPoint D s))))^L ≤ rightLevelIdeal D j s := by1093 -- `x = t · (x/t)` on the overlap, and the slope `x/t` is a unit there1094 have hu (i : D.ι) : IsUnit (D.rightIso i (completedPointMap _ (D.Q i) (overlapSlope R t x))) :=1095 ((IsLocalization.Away.algebraMap_isUnit _).map _).map _1096 have he (i : D.ι) : D.rightIso i (completedPointMap _ (D.Q i) (overlapException R t x)) *1097 D.rightIso i (completedPointMap _ (D.Q i) (overlapSlope R t x)) =1098 completedPointMap _ (rightPoint D (.inl i)) (chartBase R x t x) := by1099 rw [← map_mul, ← map_mul, ← beta_right_chartBase_self]1100 exact D.rightIso_compat i _1101 constructor1102 · rintro (i | l)1103 · exact mul_injective_quotient_transport (D.rightIso i) (hu i) (he i) (D.transverse i)1104 · exact D.transverseinf l1105 · rintro (i | l)1106 · exact exists_pow_le_span_pair_transport (D.rightIso i) (hu i) (he i)1107 (map_maximalIdeal_localCompletion_comap_le _ _ _ (D.rightIso_compat i)) (D.finite i) j1108 · exact exists_pow_le_span_pair (D.finiteinf l) j1109 1110end SurfaceBlowup