Nilpotent gluing of exceptional levels

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.PointTransport7import Mathlib.Algebra.Group.NatPowAssoc8 9/-!10# Nilpotent gluing of exceptional levels11 12Gluing of the two chart descriptions of the exceptional levels of a point blow-up. The overlap13layers are Laurent polynomial modules, which makes the truncated Čech differential injective in14negative twist; the level kernels of finitely many transverse curve germs are principal, with15generators that are nonzerodivisors on all exceptional levels; and on the concrete surface we16compute residue series of strict transforms and boundary contact numbers.17 18## Main results19 20* `SurfaceBlowup.overlap_layer_laurent_coordinates`: the overlap layers are Laurent polynomial21  modules over `R ⧸ (t, x)`.22* `SurfaceBlowup.actual_negative_twist_kernel_zero`: the truncated Čech differential is injective23  in negative twist.24* `SurfaceBlowup.finite_support_level_kernels_principal`: level kernels of finitely many transverse25  curve germs are principal; `SurfaceBlowup.finite_support_level_generator_regular` and26  `SurfaceBlowup.overlap_level_generator_regular`: their generators are nonzerodivisors on all27  exceptional levels.28* `SurfaceBlowup.concrete_strict_transform_residue_series`: residue series of strict transforms at29  exceptional points of the concrete surface.30* `SurfaceBlowup.concrete_infinity_boundary_contact`,31  `SurfaceBlowup.concrete_zero_boundary_contact`: boundary contact numbers of a degree-`d` form32  with `T = 0` and `X = 0`.33 34Provenance: `Thm_SurfaceBlowupV2_` nodes `overlap_layer_laurent_coordinates`,35`actual_negative_twist_kernel_zero`, `principal_lift_from_nilpotent_saturation`,36`finite_curve_support_{principal_lift,generator_exists}`, `finite_support_level_kernels_principal`,37`principal_power_unit_lift`, `reduced_form_eq_of_residue_coeff`,38`curve_datum_surj_and_inf_clauses`, `regular_element_on_all_principal_power_quotients`,39`finite_support_level_generator_regular`, `overlap_level_generator_regular`,40`residueKillT_chartSubst`, `chart_point_residue_series_formula`,41`concrete_strict_transform_residue_series`, `residueKillX_apply_ker`,42`concrete_surface_quotient_X_equiv`, `concrete_{infinity,zero}_boundary_contact`.43-/44 45open scoped BigOperators ENNReal46 47namespace SurfaceBlowup48 49/-! ### Laurent coordinates on the overlap layers -/50 51/-- Each exceptional layer of the overlap is `R`-linearly isomorphic to the Laurent polynomial ring52`(R/(t,x))[Z, Z⁻¹]`, the monomial `r Z^ℓ` corresponding to the layer class of `r · z^ℓ`. -/53theorem overlap_layer_laurent_coordinates (R : Type) [CommRing R] (t x : R)(4.1)54    (hreg : RegularParameterPair R t x) (j : ℕ) :55    ∃ L : LaurentPolynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer (BlowupOverlap R t x)56    ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)) j, ∀ r : R,57    ∀ ell : ℤ, (L (LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) *58      LaurentPolynomial.T ell)).val = principalLayerMap (BlowupOverlap R t x)59    ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)) j60    ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x r) * selfZPow61      (chartSlope R t x) (BlowupOverlap R t x) ell) := by62  set A := BlowupChart R t x63  set C := BlowupOverlap R t x64  set z : A := chartSlope R t x65  set a : A := chartBase R t x t66  set e : C := algebraMap A C a with he_def67  have hA : Function.Injective (fun b : A ↦ a * b) :=68    blowup_exceptional_parameter_regular R t x hreg69  have hC : Function.Injective (fun b : C ↦ e * b) :=70    nonzerodivisor_survives_localization A a z hA71  obtain ⟨L1, hL1⟩ := principal_layer_quotient_equiv C e j hC72  obtain ⟨L2, hL2⟩ := localization_principal_quotient_commute A a z 173  obtain ⟨L4, hL4b, hL4s⟩ := exceptional_overlap_is_laurent_line R t x74  -- step a75  let Φa : (C ⧸ Ideal.span {e}) ≃+* PrincipalPowerQuotient C e 1 :=76    Ideal.quotEquivOfEq (by rw [pow_one])77  -- step c78  have hI : (Ideal.span {a}) ^ 1 = exceptionalLevelIdeal R t x 1 := by79    simp only [exceptionalLevelIdeal, pow_one]; rfl80  let φ : PrincipalPowerQuotient A a 1 ≃+* ExceptionalChartLevel R t x 1 :=81    Ideal.quotEquivOfEq hI82  have hφ : ∀ b : A, φ (Ideal.Quotient.mk _ b) = Ideal.Quotient.mk _ b := fun b ↦ rfl83  let Φc : Localization.Away (Ideal.Quotient.mk ((Ideal.span {a})^1) z) ≃+*84      ExceptionalOverlapLevel R t x 1 :=85    IsLocalization.ringEquivOfRingEquiv (M := Submonoid.powers86        (Ideal.Quotient.mk ((Ideal.span {a})^1) z))87      (T := Submonoid.powers (levelSlope R t x 1)) _ _ φ (by88        rw [Submonoid.map_powers]; rfl)89  let Ψ : (C ⧸ Ideal.span {e}) ≃+* LaurentPolynomial (R ⧸ Ideal.span {t,x}) :=90    ((Φa.trans L2).trans Φc).trans L491  have hΨ (b : A) : Ψ (Ideal.Quotient.mk _ (algebraMap A C b)) =92      L4 (levelOverlapMap R t x 1 (Ideal.Quotient.mk _ b)) := by93    simp only [Ψ, RingEquiv.trans_apply]94    congr 195    have h1 : Φa (Ideal.Quotient.mk _ (algebraMap A C b)) =96        Ideal.Quotient.mk ((Ideal.span {e})^1) (algebraMap A C b) := rfl97    rw [h1, hL2]98    simp only [Φc]99    rw [IsLocalization.ringEquivOfRingEquiv_eq]100    rfl101  have hbase : ∀ r : R, Ψ (Ideal.Quotient.mk _ (algebraMap A C (chartBase R t x r))) =102      LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) :=103    fun r ↦ by rw [hΨ, ← hL4b]; rfl104  have hslope : Ψ (Ideal.Quotient.mk _ (algebraMap A C z)) = LaurentPolynomial.T 1 := by105    rw [hΨ, ← hL4s]; rfl106  have hz1 : selfZPow z C 1 = algebraMap A C z := by107    simpa using selfZPow_natCast z C 1108  have hT (ell : ℤ) : Ψ (Ideal.Quotient.mk _ (selfZPow z C ell)) = LaurentPolynomial.T ell := by109    induction ell using Int.induction_on with110    | zero => simp [LaurentPolynomial.T_zero]111    | succ i ih =>112      rw [selfZPow_add, map_mul, map_mul, ih, hz1, hslope, ← LaurentPolynomial.T_add]113    | pred i ih =>114      have h : selfZPow z C (-(i:ℤ)) = selfZPow z C (-(i:ℤ) - 1) * selfZPow z C 1 := by115        rw [← selfZPow_add]; congr 1; ring116      rw [h, map_mul, map_mul, hz1, hslope] at ih117      calc Ψ (Ideal.Quotient.mk _ (selfZPow z C (-(i:ℤ) - 1)))118          = Ψ (Ideal.Quotient.mk _ (selfZPow z C (-(i:ℤ) - 1))) * LaurentPolynomial.T 1 *119              LaurentPolynomial.T (-1) := by120            rw [LaurentPolynomial.mul_T_assoc]; simp [LaurentPolynomial.T_zero]121        _ = LaurentPolynomial.T (-(i:ℤ) - 1) := by122            rw [ih, ← LaurentPolynomial.T_add]; congr 1123  let Ψa : (C ⧸ Ideal.span {e}) ≃ₐ[R] LaurentPolynomial (R ⧸ Ideal.span {t,x}) :=124    AlgEquiv.ofRingEquiv (f := Ψ) fun r ↦ by rw [LaurentPolynomial.algebraMap_apply]; exact hbase r125  refine ⟨Ψa.symm.toLinearEquiv.trans (L1.restrictScalars R), fun r ell ↦ ?_⟩126  have hpre : Ψa.symm (LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) *127      LaurentPolynomial.T ell) = Ideal.Quotient.mk _128        (algebraMap A C (chartBase R t x r) * selfZPow z C ell) := by129    rw [AlgEquiv.symm_apply_eq]130    change _ = Ψ _131    rw [map_mul, map_mul, hbase, hT]132  simp only [LinearEquiv.trans_apply, AlgEquiv.toLinearEquiv_apply,133      LinearEquiv.restrictScalars_apply]134  rw [hpre, hL1]135 136/-- `principalLayerMap` sends `a` to the class of `a eʲ`. -/137theorem principalLayerMap_apply_eq_mk (A : Type) [CommRing A] (e : A) (j : ℕ) (a : A) :138    principalLayerMap A e j a = Ideal.Quotient.mk ((Ideal.span {e})^(j+1)) (a * e^j) := by139  simp [principalLayerMap, LinearMap.toSpanSingleton_apply, Algebra.smul_def]140 141/-- `(1/w)^i = w^(-i)` in a localization away from `w`. -/142theorem invSelf_pow_eq_selfZPow (A B : Type) [CommRing A] [CommRing B] [Algebra A B] (w : A)143    [IsLocalization.Away w B] (i : ℕ) :144    (IsLocalization.Away.invSelf (S := B) w)^i = selfZPow w B (-(i:ℤ)) := by145  rw [selfZPow_neg_natCast, IsLocalization.Away.invSelf, ← IsLocalization.mk'_pow, one_pow]146  congr 1147 148/-- The algebra map to a blow-up chart is `chartBase`. -/149theorem algebraMap_chart_eq_chartBase (R : Type) [CommRing R] (t x r : R) :150    algebraMap R (BlowupChart R t x) r = chartBase R t x r := rfl151 152/-! ### Injectivity of the truncated Čech differential in negative twist -/153 154/-- The restriction `beta.right` is compatible with the structure maps from `R`. -/155theorem beta_right_chartBase {R : Type} [CommRing R] {t x : R}156    (beta : BlowupRestriction R t x) (r : R) : beta.right (chartBase R x t r) =157      algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x r) :=158  (beta.right.commutes r).trans (IsScalarTower.algebraMap_apply R _ _ r)159 160private lemma beta_monomial_mul_invSelf_pow (R : Type) [CommRing R] (t x : R)161    (beta : BlowupRestriction R t x) (r : R) (i j d : ℕ) :162    beta.right (chartBase R x t r * chartSlope R x t ^ i * chartBase R x t x ^ j) *163      IsLocalization.Away.invSelf (chartSlope R t x) ^ d =164    algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x r) *165      selfZPow (chartSlope R t x) (BlowupOverlap R t x) ((j:ℤ) - d + -(i:ℤ)) *166      algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) ^ j := by167  have hβr := beta_right_chartBase beta168  have hz : (j:ℤ) - d + -(i:ℤ) = -(i:ℤ) + j + -(d:ℤ) := by ring169  rw [map_mul, map_mul, map_pow, map_pow, hβr, hβr, beta.slope, ← blowup_chart_relation, map_mul,170    hz, selfZPow_add, selfZPow_add, ← invSelf_pow_eq_selfZPow, ← invSelf_pow_eq_selfZPow,171    selfZPow_natCast, mul_pow]172  ring173 174private lemma left_layer_coordinates_reduce (R : Type) [CommRing R] (t x : R) (j : ℕ)175    (LA : Polynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer (BlowupChart R t x)176      (chartBase R t x t) j)177    (hLA : ∀ r : R, ∀ i : ℕ,178      (LA (Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) * Polynomial.X^i)).val =179      principalLayerMap (BlowupChart R t x) (chartBase R t x t) j180        (chartBase R t x r * (chartSlope R t x)^i))181    (LO : LaurentPolynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer (BlowupOverlap R t x)182      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)) j)183    (hLO : ∀ r : R, ∀ ell : ℤ, (LO (LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) *184      LaurentPolynomial.T ell)).val = principalLayerMap (BlowupOverlap R t x)185      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)) j186      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x r) * selfZPow187        (chartSlope R t x) (BlowupOverlap R t x) ell))188    (hψA : (Ideal.span {chartBase R t x t})^(j+1) ≤ ((Ideal.span189      {algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t)})^(j+1)).comap190      (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)))191    (P : Polynomial (R ⧸ Ideal.span {t,x})) :192    Ideal.quotientMap _ (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) hψA (LA P).val =193      (LO P.toLaurent).val := by194  induction P using Polynomial.induction_on' with195  | add p q hp hq => rw [map_add, Submodule.coe_add, map_add, hp, hq, map_add, map_add,196      Submodule.coe_add]197  | monomial i c =>198    obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective c199    rw [← Polynomial.C_mul_X_pow_eq_monomial, hLA, Polynomial.toLaurent_C_mul_X_pow, hLO,200      principalLayerMap_apply_eq_mk, principalLayerMap_apply_eq_mk, Ideal.quotientMap_mk,201      selfZPow_natCast]202    simp only [map_mul, map_pow]203 204private lemma right_layer_coordinates_reduce_twist (R : Type) [CommRing R] (t x : R)205    (beta : BlowupRestriction R t x) (d j : ℕ)206    (LB : Polynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer (BlowupChart R x t)207      (chartBase R x t x) j)208    (hLB : ∀ r : R, ∀ i : ℕ,209      (LB (Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) * Polynomial.X^i)).val =210      principalLayerMap (BlowupChart R x t) (chartBase R x t x) j211        (chartBase R x t r * (chartSlope R x t)^i))212    (LO : LaurentPolynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer (BlowupOverlap R t x)213      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)) j)214    (hLO : ∀ r : R, ∀ ell : ℤ, (LO (LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) *215      LaurentPolynomial.T ell)).val = principalLayerMap (BlowupOverlap R t x)216      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t)) j217      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x r) * selfZPow218        (chartSlope R t x) (BlowupOverlap R t x) ell))219    (hψB : (Ideal.span {chartBase R x t x})^(j+1) ≤ ((Ideal.span220      {algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t)})^(j+1)).comap221      beta.right.toRingHom)222    (Q : Polynomial (R ⧸ Ideal.span {t,x})) :223    Ideal.quotientMap _ beta.right.toRingHom hψB (LB Q).val *224      Ideal.Quotient.mk _ ((IsLocalization.Away.invSelf (chartSlope R t x))^d) =225      (LO (LaurentPolynomial.T ((j:ℤ) - d) * LaurentPolynomial.invert Q.toLaurent)).val := by226  induction Q using Polynomial.induction_on' with227  | add p q hp hq =>228    rw [map_add, Submodule.coe_add, map_add, add_mul, hp, hq]229    simp only [map_add, mul_add, Submodule.coe_add]230  | monomial i c =>231    obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective c232    have hT : LaurentPolynomial.T ((j:ℤ) - d) * LaurentPolynomial.invert233        (Polynomial.toLaurent (Polynomial.C (Ideal.Quotient.mk (Ideal.span {t, x}) r) *234          Polynomial.X ^ i)) = LaurentPolynomial.C (Ideal.Quotient.mk (Ideal.span {t, x}) r) *235          LaurentPolynomial.T ((j:ℤ) - d + -(i:ℤ)) := by236      rw [Polynomial.toLaurent_C_mul_X_pow]237      simp only [map_mul, LaurentPolynomial.invert_C, LaurentPolynomial.invert_T]238      rw [mul_left_comm, ← LaurentPolynomial.T_add]239    rw [← Polynomial.C_mul_X_pow_eq_monomial, hLB, hT, hLO, principalLayerMap_apply_eq_mk,240        principalLayerMap_apply_eq_mk, Ideal.quotientMap_mk, ← map_mul]241    congr 1242    exact beta_monomial_mul_invSelf_pow R t x beta r i j d243 244/-- An element of `(e) ^ j` defines an element of the `j`-th principal layer `(e)^j / (e)^(j+1)`. -/245theorem mk_mem_principalLayer {A : Type} [CommRing A] (e : A) (j : ℕ) {a : A}246    (ha : a ∈ (Ideal.span {e}) ^ j) :247    Ideal.Quotient.mk ((Ideal.span {e})^(j+1)) a ∈ PrincipalLayer A e j := by248  rw [LinearMap.mem_ker]249  simpa only [principalPowerReduction, AlgHom.toLinearMap_apply, Ideal.Quotient.factorₐ_apply,250    Ideal.Quotient.factor_mk, Ideal.Quotient.eq_zero_iff_mem] using ha251 252private lemma cech_kernel_step (R : Type) [CommRing R] (t x : R) (hreg : RegularParameterPair R t x)253    (beta : BlowupRestriction R t x) (hregSwap : RegularParameterPair R x t) (d j : ℕ) (hj : j < d)254    (a : BlowupChart R t x) (b : BlowupChart R x t) (ha : a ∈ (Ideal.span {chartBase R t x t}) ^ j)255    (hb : b ∈ (Ideal.span {chartBase R x t x}) ^ j)256    (hD : fullCechDifferential R t x beta d (a, b) ∈257      (Ideal.span {algebraMap (BlowupChart R t x) (BlowupOverlap R t x)258          (chartBase R t x t)}) ^ (j + 1)) :259    a ∈ (Ideal.span {chartBase R t x t})^(j+1) ∧ b ∈ (Ideal.span {chartBase R x t x})^(j+1) := by260  set ι := algebraMap (BlowupChart R t x) (BlowupOverlap R t x)261  set eA := chartBase R t x t262  set eB := chartBase R x t x263  set eO := ι eA264  set W := chartSlope R t x265  have hβeB : beta.right eB = eO * ι W := by266    rw [beta_right_chartBase, ← blowup_chart_relation, map_mul]267  obtain ⟨LA, hLA⟩ := chart_layer_polynomial_coordinates R t x hreg j268  have hB := chart_layer_polynomial_coordinates R x t hregSwap j269  rw [Set.pair_comm x t] at hB270  obtain ⟨LB, hLB⟩ := hB271  obtain ⟨LO, hLO⟩ := overlap_layer_laurent_coordinates R t x hreg j272  -- the reduction maps273  have hψA : (Ideal.span {eA})^(j+1) ≤ ((Ideal.span {eO})^(j+1)).comap ι := by274    rw [← Ideal.map_le_iff_le_comap, Ideal.map_pow, Ideal.map_span, Set.image_singleton]275  have hψB : (Ideal.span {eB})^(j+1) ≤ ((Ideal.span {eO})^(j+1)).comap beta.right.toRingHom := by276    rw [← Ideal.map_le_iff_le_comap, Ideal.map_pow, Ideal.map_span, Set.image_singleton]277    apply Ideal.pow_right_mono278    rw [Ideal.span_le, Set.singleton_subset_iff]279    change beta.right eB ∈ _280    rw [hβeB]281    exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)282  have hPA := left_layer_coordinates_reduce R t x j LA hLA LO hLO hψA283  have hPB := right_layer_coordinates_reduce_twist R t x beta d j LB hLB LO hLO hψB284  set P := LA.symm ⟨_, mk_mem_principalLayer eA j ha⟩ with hPdef285  set Q := LB.symm ⟨_, mk_mem_principalLayer eB j hb⟩ with hQdef286  have hP : (LA P).val = Ideal.Quotient.mk _ a := by rw [hPdef, LinearEquiv.apply_symm_apply]287  have hQ : (LB Q).val = Ideal.Quotient.mk _ b := by rw [hQdef, LinearEquiv.apply_symm_apply]288  have key : LO (P.toLaurent - LaurentPolynomial.T ((j:ℤ) - d) *289      LaurentPolynomial.invert Q.toLaurent) = 0 := by290    apply Subtype.ext291    rw [map_sub, Submodule.coe_sub, ← hPA, ← hPB, hP, hQ, Ideal.quotientMap_mk,292      Ideal.quotientMap_mk, ← map_mul, ← map_sub, ZeroMemClass.coe_zero,293      Ideal.Quotient.eq_zero_iff_mem]294    convert hD using 1295    change _ = ι a - _ * _296    simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe]297    ring298  have hz := (LinearEquiv.map_eq_zero_iff LO).1 key299  obtain ⟨hP0, hQ0⟩ := negative_laurent_twist_has_no_kernel _ ((j:ℤ) - d) (by omega) P Q hz300  constructor301  · rw [← Ideal.Quotient.eq_zero_iff_mem, ← hP, hP0, map_zero]; rfl302  · rw [← Ideal.Quotient.eq_zero_iff_mem, ← hQ, hQ0, map_zero]; rfl303 304/-- In negative twist (`n ≤ d`), the finite Čech differential of the two-chart cover, truncated at305level `n`, is injective. -/306theorem actual_negative_twist_kernel_zero (R : Type) [CommRing R] (t x : R)307    (hreg : RegularParameterPair R t x) (beta : BlowupRestriction R t x)308    (hregSwap : RegularParameterPair R x t) (d n : ℕ) (hn : n ≤ d)309    (h : cechInputLattice R t x n ≤ (cechOutputLattice R t x n).comap310      (fullCechDifferential R t x beta d)) :311    Function.Injective (finiteCechDifferential R t x beta d n h) := by312  rw [injective_iff_map_eq_zero]313  intro z hz314  induction z using Submodule.Quotient.induction_on with315  | H z =>316    obtain ⟨a, b⟩ := z317    rw [finiteCechDifferential, Submodule.mapQ_apply, Submodule.Quotient.mk_eq_zero] at hz318    rw [Submodule.Quotient.mk_eq_zero]319    have hz' : fullCechDifferential R t x beta d (a, b) ∈320        (Ideal.span {algebraMap (BlowupChart R t x) (BlowupOverlap R t x)321          (chartBase R t x t)})^n := hz322    have main (j : ℕ) (hj : j ≤ n) : a ∈ (Ideal.span {chartBase R t x t})^j ∧323        b ∈ (Ideal.span {chartBase R x t x})^j := by324      induction j with325      | zero => simp326      | succ j ih =>327        obtain ⟨ha, hb⟩ := ih (by omega)328        exact cech_kernel_step R t x hreg beta hregSwap d j (by omega) a b ha hb329          (Ideal.pow_le_pow_right (by omega) hz')330    exact main n le_rfl331 332/-! ### Principal level kernels -/333 334/-- If `e` is nilpotent and the ideal `J ∋ f` satisfies `J ≤ (f) + (e)` and `J ∩ (e) ≤ e J`, then335`J = (f)`. -/336private theorem principal_lift_from_nilpotent_saturation (A : Type) [CommRing A] (e f : A) (j : ℕ)337    (he : e ^ j = 0) (J : Ideal A) (hf : f ∈ J) (hred : J ≤ Ideal.span {f} ⊔ Ideal.span {e})338    (hsat : J ⊓ Ideal.span {e} ≤ Ideal.span {e} * J) : J = Ideal.span {f} := by339  have hfJ : Ideal.span {f} ≤ J := (Ideal.span_singleton_le_iff_mem J).mpr hf340  have step (x : A) (hx : x ∈ J) : ∃ a : A, ∃ y ∈ J, x = f * a + e * y := by341    obtain ⟨u, hu, v, hv, huv⟩ := Submodule.mem_sup.mp (hred hx)342    obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp hu343    have hvJ : v ∈ J := by344      rw [show v = x - a * f by rw [← huv]; ring]; exact J.sub_mem hx (hfJ hu)345    obtain ⟨w, hw, hew⟩ := (Ideal.mem_span_singleton_mul).mp (hsat ⟨hvJ, hv⟩)346    exact ⟨a, w, hw, by rw [← huv, ← hew]; ring⟩347  refine le_antisymm (fun x hx ↦ ?_) hfJ348  have key (k : ℕ) : ∃ a : A, ∃ y ∈ J, x = f * a + e ^ k * y := by349    induction k with350    | zero => exact ⟨0, x, hx, by ring⟩351    | succ k ih =>352      obtain ⟨a, y, hy, rfl⟩ := ih353      obtain ⟨b, z, hz, rfl⟩ := step y hy354      exact ⟨a + e ^ k * b, z, hz, by ring⟩355  obtain ⟨a, y, _, rfl⟩ := key j356  rw [he, zero_mul, add_zero]357  exact Ideal.mem_span_singleton'.mpr ⟨a, mul_comm a f⟩358 359/-- A level kernel of finitely many transverse curve germs is principal, generated by any of its360elements generating it modulo `e`. -/361private theorem finite_curve_support_principal_lift (A : Type) [CommRing A] [IsNoetherianRing A]362    (ι : Type) [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsMaximal] (hP : Function.Injective P)363    (e : A) (j : ℕ) (hj : 0 < j) (g : ∀ i, CompletedLocalAt A (P i)) (L : ι → ℕ)364    (hfinite : ∀ i, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map365      (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤ finiteLocalCurveIdeal A (P i) e366      (g i) j) (htransverse : ∀ i, Function.Injective367      (fun a : CompletedLocalAt A (P i) ⧸ Ideal.span {g i} ↦ Ideal.Quotient.mk (Ideal.span {g i})368      (completedPointMap A (P i) e) * a)) (f : (A ⧸ (Ideal.span {e})^j))369    (hf : f ∈ finiteSupportLevelKernel A ι P (fun i ↦ finiteLocalCurveIdeal A (P i) e (g i) j) e j)370    (hred : finiteSupportLevelKernel A ι P (fun i ↦ finiteLocalCurveIdeal A (P i) e (g i) j) e j ≤371      Ideal.span {f} ⊔ Ideal.span {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)}) :372    finiteSupportLevelKernel A ι P (fun i ↦ finiteLocalCurveIdeal A (P i) e (g i) j) e j =373    Ideal.span {f} := by374  refine principal_lift_from_nilpotent_saturation _ _ f j ?_ _ hf hred375    (finite_curve_support_kernel_saturated A ι P hP e j hj g L hfinite htransverse)376  rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem, Ideal.span_singleton_pow]377  exact Ideal.subset_span rfl378 379/-- If the reduction modulo `e` of a level kernel of finitely many transverse curve germs is380generated by `h`, the kernel is generated by a lift of `h`. -/381private theorem finite_curve_support_generator_exists (A : Type) [CommRing A] [IsNoetherianRing A]382    (ι : Type) [Finite ι] (P : ι → Ideal A) [∀ i, (P i).IsMaximal] (hP : Function.Injective P)383    (e : A) (j : ℕ) (hj : 0 < j) (g : ∀ i, CompletedLocalAt A (P i)) (L : ι → ℕ)384    (hfinite : ∀ i, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map385      (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤ finiteLocalCurveIdeal A (P i) e386      (g i) j) (htransverse : ∀ i, Function.Injective387      (fun a : CompletedLocalAt A (P i) ⧸ Ideal.span {g i} ↦ Ideal.Quotient.mk (Ideal.span {g i})388      (completedPointMap A (P i) e) * a)) (h : (A ⧸ (Ideal.span {e})^j) ⧸ Ideal.span389      {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)})390    (hred : (finiteSupportLevelKernel A ι P (fun i ↦ finiteLocalCurveIdeal A (P i) e (g i) j) e391      j).map (Ideal.Quotient.mk (Ideal.span {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)})) =392      Ideal.span {h}) :393    ∃ f : (A ⧸ (Ideal.span {e})^j), finiteSupportLevelKernel A ι P394    (fun i ↦ finiteLocalCurveIdeal A (P i) e (g i) j) e j = Ideal.span {f} ∧ Ideal.Quotient.mk395    (Ideal.span {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)}) f = h := by396  set I := finiteSupportLevelKernel A ι P (fun i ↦ finiteLocalCurveIdeal A (P i) e397      (g i) j) e j with hI398  set ρ := Ideal.Quotient.mk (Ideal.span {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)}) with hρ399  have hh : h ∈ I.map ρ := by rw [hred]; exact Ideal.mem_span_singleton_self h400  obtain ⟨f, hfI, hfh⟩ := (Ideal.mem_map_iff_of_surjective ρ Ideal.Quotient.mk_surjective).1 hh401  refine ⟨f, ?_, hfh⟩402  apply finite_curve_support_principal_lift A ι P hP e j hj g L hfinite htransverse f hfI403  intro x hx404  have hxm : ρ x ∈ Ideal.span {h} := by rw [← hred]; exact Ideal.mem_map_of_mem ρ hx405  obtain ⟨b, hb⟩ := Ideal.mem_span_singleton'.1 hxm406  obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective b407  have hdiff : x - a * f ∈ Ideal.span {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)} := by408    rw [← Ideal.Quotient.eq_zero_iff_mem]409    change ρ (x - a * f) = 0410    rw [map_sub, map_mul, hfh, ← hb, sub_self]411  have : x = a * f + (x - a * f) := by ring412  rw [this]413  exact Submodule.add_mem_sup (Ideal.mul_mem_left _ _ (Ideal.mem_span_singleton_self f)) hdiff414 415private theorem isPrincipal_quotient_quotient (A : Type) [CommRing A] (e : A) (j : ℕ)416    (hPIR : IsPrincipalIdealRing (A ⧸ Ideal.span {e}))417    (I : Ideal ((A ⧸ (Ideal.span {e}) ^ j) ⧸ Ideal.span418        {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)})) :419    ∃ h, I = Ideal.span {h} := by420  let π : A →+* ((A ⧸ (Ideal.span {e})^j) ⧸ Ideal.span421      {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)}) :=422    (Ideal.Quotient.mk _).comp (Ideal.Quotient.mk _)423  have hπ : Function.Surjective π :=424    (Ideal.Quotient.mk_surjective).comp Ideal.Quotient.mk_surjective425  let ψ : A ⧸ Ideal.span {e} →+* ((A ⧸ (Ideal.span {e})^j) ⧸ Ideal.span426      {(Ideal.Quotient.mk ((Ideal.span {e})^j) e)}) :=427    Ideal.Quotient.lift (Ideal.span {e}) π (by428      intro a ha429      obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.mp ha430      simp only [map_mul, π, RingHom.comp_apply]431      rw [Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_span_singleton_self _), mul_zero])432  have hψ : Function.Surjective ψ := fun q ↦433    let ⟨a, ha⟩ := hπ q; ⟨Ideal.Quotient.mk _ a, ha⟩434  exact (@IsPrincipalIdealRing.principal _ _ (.of_surjective ψ hψ) I).principal435 436/-- On the chart, the level kernels of finitely many transverse curve germs at exceptional points437are principal at every level, generated by the images of chart elements `F j`. -/438theorem finite_support_level_kernels_principal (R : Type) [CommRing R] (t x : R)439    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)] (ι : Type)440    [Finite ι] (P : ι → Ideal (BlowupChart R t x)) [∀ i, (P i).IsMaximal]441    (hP : Function.Injective P) (_hPe : ∀ i, chartBase R t x t ∈ P i)442    (g : ∀ i, CompletedLocalAt (BlowupChart R t x) (P i))443    (htransverse : ∀ i, Function.Injective (fun a : CompletedLocalAt (BlowupChart R t x) (P i) ⧸444      Ideal.span {g i} => Ideal.Quotient.mk (Ideal.span {g i})445      (completedPointMap (BlowupChart R t x) (P i) (chartBase R t x t)) * a))446    (hfinite : ∀ j : ℕ, ∀ i, ∃ L : ℕ, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map447      (localCompletionMap (Localization.AtPrime (P i))))^L ≤ finiteLocalCurveIdeal448      (BlowupChart R t x) (P i) (chartBase R t x t) (g i) j) :449    ∃ F : ℕ → BlowupChart R t x, ∀ j : ℕ, finiteSupportLevelKernel (BlowupChart R t x) ι P450    (fun i ↦ finiteLocalCurveIdeal (BlowupChart R t x) (P i) (chartBase R t x t) (g i) j)451    (chartBase R t x t) j = Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R t x t})^j)452      (F j)} := by453  obtain ⟨φ, -, -⟩ := exceptional_chart_is_affine_line R t x454  let _ : Field (R ⧸ Ideal.span ({t,x} : Set R)) := Ideal.Quotient.field _455  have hPIR1 : IsPrincipalIdealRing (ExceptionalChartLevel R t x 1) :=456    IsPrincipalIdealRing.of_surjective φ.symm.toRingHom φ.symm.surjective457  have hEq : exceptionalLevelIdeal R t x 1 = Ideal.span {chartBase R t x t} := by458    simp [exceptionalLevelIdeal]459  have hPIR : IsPrincipalIdealRing (BlowupChart R t x ⧸ Ideal.span {chartBase R t x t}) :=460    IsPrincipalIdealRing.of_surjective (Ideal.quotEquivOfEq hEq).toRingHom461        (Ideal.quotEquivOfEq hEq).surjective462  have key (j : ℕ) : ∃ f : BlowupChart R t x, finiteSupportLevelKernel (BlowupChart R t x) ι P463      (fun i ↦ finiteLocalCurveIdeal (BlowupChart R t x) (P i) (chartBase R t x t) (g i) j)464      (chartBase R t x t) j = Ideal.span {Ideal.Quotient.mk465      ((Ideal.span {chartBase R t x t})^j) f} := by466    rcases Nat.eq_zero_or_pos j with rfl | hj467    · refine ⟨0, ?_⟩468      have : Subsingleton (BlowupChart R t x ⧸ (Ideal.span {chartBase R t x t})^0) := by469        rw [pow_zero, Ideal.one_eq_top]; infer_instance470      exact Subsingleton.elim _ _471    · choose L hL using hfinite j472      obtain ⟨h, hh⟩ := isPrincipal_quotient_quotient (BlowupChart R t x) (chartBase R t x t) j hPIR473        ((finiteSupportLevelKernel (BlowupChart R t x) ι P474            (fun i ↦ finiteLocalCurveIdeal (BlowupChart R t x) (P i) (chartBase R t x t) (g i) j)475            (chartBase R t x t) j).map (Ideal.Quotient.mk _))476      obtain ⟨f, hf, -⟩ := finite_curve_support_generator_exists477          (BlowupChart R t x) ι P hP (chartBase R t x t) j hj g L hL htransverse h hh478      obtain ⟨f', rfl⟩ := Ideal.Quotient.mk_surjective f479      exact ⟨f', hf⟩480  exact ⟨_, fun j ↦ (key j).choose_spec⟩481 482/-- A unit of `A ⧸ (e)^j` (with `j ≥ 1`) lifts to an element of `A` whose image in `A ⧸ (e)^(j+1)`483is a unit. -/484theorem principal_power_unit_lift (A : Type) [CommRing A] (e : A) (j : ℕ) (hj : 1 ≤ j)485    (u : A ⧸ (Ideal.span {e}) ^ j) (hu : IsUnit u) :486    ∃ v : A, IsUnit (Ideal.Quotient.mk ((Ideal.span {e})^(j+1)) v) ∧ Ideal.Quotient.mk487    ((Ideal.span {e})^j) v = u := by488  obtain ⟨v, hv⟩ := Ideal.Quotient.mk_surjective u489  obtain ⟨w, hw⟩ := Ideal.Quotient.mk_surjective (↑hu.unit⁻¹ : A ⧸ (Ideal.span {e})^j)490  refine ⟨v, ?_, hv⟩491  set I := Ideal.span {e}492  have hmem : v * w - 1 ∈ I ^ j := by493    rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_mul, map_one, hv, hw]494    simp495  have hnil : IsNilpotent (Ideal.Quotient.mk (I ^ (j+1)) (v * w - 1)) := by496    refine ⟨2, ?_⟩497    rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]498    have h2 : (v * w - 1) ^ 2 ∈ I ^ (j + j) := by499      rw [pow_two, pow_add]; exact Ideal.mul_mem_mul hmem hmem500    exact Ideal.pow_le_pow_right (by omega) h2501  have hunit := hnil.isUnit_one_add502  rw [← map_one (Ideal.Quotient.mk (I ^ (j+1))), ← map_add, add_sub_cancel, map_mul] at hunit503  exact isUnit_of_mul_isUnit_left hunit504 505/-- If the residues of `c₀, …, c_d` are the coefficients of `H` with `deg H ≤ d`, then `∑ c̄ᵢ Xⁱ =506H`. -/507theorem reduced_form_eq_of_residue_coeff (R : Type) [CommRing R] [IsLocalRing R] (d : ℕ)508    (c : Fin (d + 1) → R) (H : Polynomial (IsLocalRing.ResidueField R)) (hH : H.natDegree ≤ d)509    (hcH : ∀ i : Fin (d+1), IsLocalRing.residue R (c i) = H.coeff i.val) :510    (∑ i : Fin (d+1), Polynomial.C (IsLocalRing.residue R (c i)) * Polynomial.X^i.val : Polynomial511      (IsLocalRing.ResidueField R)) = H := by512  conv_rhs => rw [Polynomial.as_sum_range' H (d+1) (Nat.lt_succ_of_le hH)]513  rw [← Fin.sum_univ_eq_sum_range (fun i ↦ Polynomial.monomial i (H.coeff i)) (d+1)]514  refine Finset.sum_congr rfl fun i _ ↦ ?_515  rw [hcH, Polynomial.C_mul_X_pow_eq_monomial]516 517/-! ### Curve data on the concrete surface518 519From here on we use local notations for the residue field and the two charts of the blow-up of520`R = ConcreteSurface O pi u a b` at `(t, x)`, taking the surface data as explicit arguments. -/521 522/-- The residue field of the concrete surface. -/523local notation:max "kRes" O:max pi:max u:max a:max b:max =>524  IsLocalRing.ResidueField (ConcreteSurface O pi u a b)525 526/-- The `t`-chart `R[x/t]` of the blow-up of the concrete surface `R` at `(t, x)`. -/527local notation:max "tChart" O:max pi:max u:max a:max b:max =>528  BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)529 530/-- The structure map `R → R[x/t]` of the `t`-chart. -/531local notation:max "tBase" O:max pi:max u:max a:max b:max =>532  chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)533 534/-- The slope `x/t` in the `t`-chart. -/535local notation:max "tSlope" O:max pi:max u:max a:max b:max =>536  chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)537 538/-- The exceptional ideal `(t)` of the `t`-chart. -/539local notation:max "tExc" O:max pi:max u:max a:max b:max =>540  chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)541 542/-- The `x`-chart `R[t/x]` of the blow-up of the concrete surface `R` at `(t, x)`. -/543local notation:max "xChart" O:max pi:max u:max a:max b:max =>544  BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)545 546/-- The structure map `R → R[t/x]` of the `x`-chart. -/547local notation:max "xBase" O:max pi:max u:max a:max b:max =>548  chartBase (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)549 550/-- The slope `t/x` in the `x`-chart. -/551local notation:max "xSlope" O:max pi:max u:max a:max b:max =>552  chartSlope (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)553 554/-- If the last coefficient `c_d` lies in `(t, x)`, the strict transform `∑ cᵢ (t/x)^(d-i)` in the555`x`-chart passes through the point at infinity, so the curve datum has a point at infinity. -/556private theorem curve_datum_nonempty_inf (O : Type) [CommRing O] [IsDomain O]557    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]558    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)559    (a b : ℕ) (ha : 0 < a) (d : ℕ) (c : Fin (d + 1) → (ConcreteSurface O pi u a b))560    (hcd : c (Fin.last d) ∈ Ideal.span {surfaceT O pi u a b, surfaceX O pi u a b})561    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)562      (surfaceX O pi u a b))563    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)564      beta)565    (hrightsurj : ∀ P : Ideal (xChart O pi u a b), P.IsMaximal →566      (xBase O pi u a b) (surfaceX O pi u a b) ∈ P → (∑ i : Fin (d+1), algebraMap567        (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) * (xSlope O pi u a b)^(d - i.val)) ∈568          P → ∃ s : D.ι ⊕ D.ιinf, rightPoint D s = P) :569    Nonempty D.ιinf := by570  have : (Ideal.span {surfaceT O pi u a b, surfaceX O pi u a b}).IsMaximal :=571    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha572  obtain ⟨_, _, S, -, hSt, hSx, -⟩ := concrete_surface_data_exists_unconditional O pi hpi u a b ha573  obtain ⟨hIM, hIx, hIW, -⟩ := infinity_point_maximal O (ConcreteSurface O pi u a b) S574  rw [hSt, hSx] at hIM hIx hIW575  have hbase : Ideal.span {surfaceT O pi u a b, surfaceX O pi u a b} ≤576      (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)577        (surfaceX O pi u a b)).comap (xBase O pi u a b) := by578    rw [Ideal.span_le]579    rintro _ (rfl | rfl)580    · change _ ∈ infinityPoint _ _ _581      rw [← blowup_chart_relation]582      exact Ideal.mul_mem_right _ _ hIx583    · exact hIx584  obtain ⟨i | l, hs⟩ := hrightsurj _ hIM hIx (Ideal.sum_mem _ fun i _ ↦ by585    by_cases hi : i.val = d586    · obtain rfl : i = Fin.last d := Fin.ext hi587      simp only [Fin.val_last, Nat.sub_self, pow_zero, mul_one]588      exact hbase hcd589    · exact Ideal.mul_mem_left _ _ (Ideal.pow_mem_of_mem _ hIW _ (by omega)))590  · exact ((overlap_exceptional_point_comap_maximal_right _ _ _ beta (D.Q i) (D.onE i)).2.1591      (show _ ∈ rightPoint D (Sum.inl i) by rw [hs]; exact hIW)).elim592  · exact ⟨l⟩593 594/-- For the strict transform of a degree-`d` form with residue polynomial `H` and homogeneous595divisor `Dv` on the concrete surface, the curve datum has a point over every direction in the596support of `Dv`, a point at the origin and at infinity when `Dv` charges them, and the597multiplicity at infinity is `Dv none`. -/598theorem curve_datum_surj_and_inf_clauses (O : Type) [CommRing O] [IsDomain O]599    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]600    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)601    (a b : ℕ) (ha : 0 < a) (d : ℕ) (f : (ConcreteSurface O pi u a b))602    (c : Fin (d + 1) → (ConcreteSurface O pi u a b))603    (_hc : f = ∑ i : Fin (d + 1), c i * (surfaceT O pi u a b) ^ (d - i.val) *604      (surfaceX O pi u a b) ^ i.val)605    [IsLocalRing (ConcreteSurface O pi u a b)] (H : Polynomial (kRes O pi u a b))606    (Dv : ExceptionalDivisor (kRes O pi u a b))607    (hH : HasHomogeneousDivisor (kRes O pi u a b) d H Dv)608    (hcH : ∀ i : Fin (d+1), IsLocalRing.residue (ConcreteSurface O pi u a b) (c i) = H.coeff i.val)609    (e : ((tChart O pi u a b) ⧸ tExc O pi u a b) ≃+* Polynomial (kRes O pi u a b))610    (he : ∀ r : ConcreteSurface O pi u a b,611      e (Ideal.Quotient.mk (tExc O pi u a b) (tBase O pi u a b r)) =612        Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))613    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)614    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)615      (surfaceX O pi u a b))616    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)617      beta)618    (_hleft : ∀ s : D.ι ⊕ D.ι0, leftData D s = completedPointMap (tChart O pi u a b) (leftPoint D s)619      (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *620        (tSlope O pi u a b)^i.val) ∧ (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)621          (tChart O pi u a b) (c i) * (tSlope O pi u a b)^i.val) ∈ leftPoint D s)622    (hleftsurj : ∀ P : Ideal (tChart O pi u a b), P.IsMaximal →623      (tBase O pi u a b) (surfaceT O pi u a b) ∈ P → (∑ i : Fin (d+1), algebraMap624        (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) * (tSlope O pi u a b)^i.val) ∈ P →625      ∃ s : D.ι ⊕ D.ι0, leftPoint D s = P)626    (hright : ∀ s : D.ι ⊕ D.ιinf, Ideal.span {rightData D s} = Ideal.span {completedPointMap627      (xChart O pi u a b) (rightPoint D s) (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)628        (xChart O pi u a b) (c i) * (xSlope O pi u a b)^(d - i.val))} ∧629      (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *630        (xSlope O pi u a b)^(d - i.val)) ∈ rightPoint D s)631    (hrightsurj : ∀ P : Ideal (xChart O pi u a b), P.IsMaximal →632      (xBase O pi u a b) (surfaceX O pi u a b) ∈ P → (∑ i : Fin (d+1), algebraMap633        (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) * (xSlope O pi u a b)^(d - i.val)) ∈634          P → ∃ s : D.ι ⊕ D.ιinf, rightPoint D s = P) :635    (∀ φ : AffineDirection (kRes O pi u a b), φ ≠ zeroAffine (kRes O pi u a b) → 0 < Dv (some φ) →636      ∃ i : D.ι, D.Q i = (directionPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)637        (surfaceX O pi u a b) e φ).map (algebraMap (tChart O pi u a b) (BlowupOverlap638          (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)))) ∧639    (0 < Dv (zeroDirection (kRes O pi u a b)) → Nonempty D.ι0) ∧640    (∀ l : D.ιinf, D.Pinf l = infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)641      (surfaceX O pi u a b) ∧ Dv none = rightMultiplicity D (Sum.inr l)) ∧642    (0 < Dv none → Nonempty D.ιinf) := by643  have hmax : (Ideal.span {surfaceT O pi u a b, surfaceX O pi u a b}).IsMaximal :=644    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha645  have hne : ∃ i : Fin (d+1), c i ∉ Ideal.span {surfaceT O pi u a b, surfaceX O pi u a b} := by646    obtain ⟨j, hj⟩ : ∃ j, H.coeff j ≠ 0 := by647      by_contra h; push Not at h; exact hH.1 (Polynomial.ext h)648    have hjd := Nat.lt_succ_of_le ((Polynomial.le_natDegree_of_ne_zero hj).trans hH.2.1)649    refine ⟨⟨j, hjd⟩, fun hmem ↦ hj ?_⟩650    rw [← hcH ⟨j, hjd⟩]651    exact (IsLocalRing.residue_eq_zero_iff _).2 (IsLocalRing.le_maximalIdeal hmax.ne_top hmem)652  have hHBAR := reduced_form_eq_of_residue_coeff (ConcreteSurface O pi u a b) d c H hH.2.1 hcH653  obtain ⟨hdp, -, -⟩ := directionPoint_properties (ConcreteSurface O pi u a b)654      (surfaceT O pi u a b) (surfaceX O pi u a b) e he heZ655  have heF : e (Ideal.Quotient.mk (tExc O pi u a b) (∑ i : Fin (d+1),656      algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *657        (tSlope O pi u a b)^i.val)) = H := by658    rw [← hHBAR, map_sum, map_sum]659    refine Finset.sum_congr rfl fun i _ ↦ ?_660    rw [map_mul, map_mul, map_pow, map_pow, heZ, ← he]661    rfl662  have hFmem (φ) (hφ : 0 < Dv (some φ)) : (∑ i : Fin (d+1), algebraMap663      (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) * (tSlope O pi u a b)^i.val) ∈664      directionPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b) e665        φ := by666    change _ ∈ Ideal.comap _ _667    rw [Ideal.mem_comap, RingHom.comp_apply]668    change e _ ∈ _669    rw [heF, Ideal.mem_span_singleton, hH.2.2.2]670    exact dvd_mul_of_dvd_right ((count_normalizedFactors_divisorAffinePolynomial _ Dv _671      (Polynomial.leadingCoeff_ne_zero.2 hH.1) φ).2.2 hφ) _672  refine ⟨fun φ hφ0 hφ ↦ ?_, fun hφ ↦ ?_, fun l ↦ ?_, fun hpos ↦ ?_⟩673  · obtain ⟨hM, hT, hZ, -⟩ := hdp φ674    obtain ⟨i | k, hs⟩ := hleftsurj _ hM hT (hFmem φ hφ)675    · exact ⟨i, hs ▸ (IsLocalization.map_under (Submonoid.powers (tSlope O pi u a b)) _676        (D.Q i)).symm⟩677    · exact absurd (hZ.1 (hs ▸ D.slope0 k)) hφ0678  · obtain ⟨hM, hT, hZ, -⟩ := hdp (zeroAffine _)679    obtain ⟨i | k, hs⟩ := hleftsurj _ hM hT (hFmem _ hφ)680    · exact ((overlap_exceptional_point_comap_maximal _ _ _ (D.Q i) (D.onE i)).2.1681        (show _ ∈ leftPoint D (Sum.inl i) by rw [hs]; exact hZ.2 rfl)).elim682    · exact ⟨k⟩683  · refine ⟨(concrete_infinity_point_completion O pi hpi u a b ha (D.Pinf l) (D.onEinf l)684      (D.slopeinf l)).1, ?_⟩685    have : (rightPoint D (Sum.inr l)).IsMaximal := D.maximalinf l686    unfold rightMultiplicity rightLevelIdeal finiteLocalCurveIdeal687    rw [pow_one, Ideal.span_insert, (hright (Sum.inr l)).1, ← Ideal.span_insert,688      concrete_infinity_strict_transform_multiplicity O pi hpi u a b ha d c hne689        (rightPoint D (Sum.inr l)) (D.onEinf l) (D.slopeinf l), hHBAR, ENat.toNat_natCast, hH.2.2.1]690  · rw [hH.2.2.1] at hpos691    have hlt : H.natDegree < d := by omega692    have hcd : c (Fin.last d) ∈ Ideal.span {surfaceT O pi u a b, surfaceX O pi u a b} := by693      have hm := concrete_surface_maximalIdeal_eq O pi hpi u a b ha694      unfold surfaceParameterIdeal at hm695      rw [← hm, ← IsLocalRing.residue_eq_zero_iff, hcH]696      exact Polynomial.coeff_eq_zero_of_natDegree_lt hlt697    exact curve_datum_nonempty_inf O pi hpi u a b ha d c hcd beta D hrightsurj698 699/-! ### Regularity of the level generators -/700 701/-- If `e` is a nonzerodivisor and `f` is a nonzerodivisor modulo `e`, then `f` is a nonzerodivisor702modulo every power `(e)^j`. -/703private theorem regular_element_on_all_principal_power_quotients (A : Type) [CommRing A] (e f : A)704    (he : Function.Injective (fun a : A ↦ e*a))705    (hf : Function.Injective706      (fun a : A ⧸ Ideal.span {e} ↦ Ideal.Quotient.mk (Ideal.span {e}) f * a)) (j : ℕ) :707    Function.Injective708      (fun a : A ⧸ (Ideal.span {e})^j ↦ Ideal.Quotient.mk ((Ideal.span {e})^j) f * a) := by709  have key (n : ℕ) : ∀ a : A, e ^ n ∣ f * a → e ^ n ∣ a := by710    induction n with711    | zero => intro a _; simp712    | succ n ih =>713      rintro a ⟨c, hc⟩714      have h1 : Ideal.Quotient.mk (Ideal.span {e}) f * Ideal.Quotient.mk (Ideal.span {e}) a715          = Ideal.Quotient.mk (Ideal.span {e}) f * 0 := by716        rw [mul_zero, ← map_mul, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton, hc]717        exact ⟨e ^ n * c, by ring⟩718      have h2 := hf h1719      rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton] at h2720      obtain ⟨b, rfl⟩ := h2721      have h3 : f * b = e ^ n * c :=722        he (show e * (f * b) = e * (e ^ n * c) by linear_combination hc)723      obtain ⟨d, hd⟩ := ih b ⟨c, h3⟩724      exact ⟨d, by rw [hd]; ring⟩725  intro x y hxy726  obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective x727  obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective y728  have hxy' : Ideal.Quotient.mk ((Ideal.span {e})^j) (f * a)729      = Ideal.Quotient.mk ((Ideal.span {e})^j) (f * b) := by730    simpa only [map_mul] using hxy731  rw [Ideal.Quotient.eq, Ideal.span_singleton_pow, Ideal.mem_span_singleton, ← mul_sub] at hxy'732  rw [Ideal.Quotient.eq, Ideal.span_singleton_pow, Ideal.mem_span_singleton]733  exact key j _ hxy'734 735private theorem sup_pow_le_sup_pow {B : Type} [CommRing B] (I J : Ideal B) (n : ℕ) :736    (I ⊔ J) ^ n ≤ I ⊔ J ^ n := by737  induction n with738  | zero => simp739  | succ n ih =>740    rw [pow_succ, pow_succ]741    refine (Ideal.mul_mono_left ih).trans ?_742    rw [Ideal.sup_mul, Ideal.mul_sup, Ideal.mul_sup]743    exact sup_le (sup_le (Ideal.mul_le_left.trans le_sup_left)744      (Ideal.mul_le_left.trans le_sup_left)) (sup_le (Ideal.mul_le_right.trans le_sup_left)745        le_sup_right)746 747private theorem map_ne_bot_of_prod_pow_le {A Q k : Type} [CommRing A] [CommRing Q] [CommRing k]748    [IsDomain k] (f : Q ≃+* Polynomial k) (π : A →+* Q) (hπ : Function.Surjective π) {ι : Type}749    [Fintype ι] (P : ι → Ideal A) [∀ i, (P i).IsMaximal] (hk : ∀ i, RingHom.ker π ≤ P i) (L : ι → ℕ)750    (K : Ideal A) (hle : ∏ i, P i ^ L i ≤ K) : K.map π ≠ ⊥ := by751  have : IsDomain Q := f.toMulEquiv.isDomain752  have hnf : ¬ IsField Q := fun h ↦ Polynomial.not_isField _ (f.symm.toMulEquiv.isField h)753  have hne : ∀ i, (P i).map π ≠ ⊥ := fun i ↦754    Ring.ne_bot_of_isMaximal_of_not_isField (Ideal.IsMaximal.map_of_surjective_of_ker_le hπ755        (hk i)) hnf756  intro hbot757  have h2 := Ideal.map_mono (f := π) hle758  have hmp := map_prod (Ideal.mapHom π) (fun i ↦ P i ^ L i) Finset.univ759  simp only [Ideal.mapHom_apply] at hmp760  rw [hbot, le_bot_iff, hmp] at h2761  simp only [Ideal.map_pow] at h2762  rw [Ideal.zero_eq_bot.symm, Finset.prod_eq_zero_iff] at h2763  obtain ⟨i, -, hi⟩ := h2764  exact hne i (pow_eq_zero_iff'.mp hi).1765 766private theorem map_mk_ne_bot_of_prod_pow_le {A k : Type} [CommRing A] [CommRing k] [IsDomain k]767    (I : Ideal A) (f : A ⧸ I ≃+* Polynomial k) {ι : Type} [Fintype ι] (P : ι → Ideal A)768    [∀ i, (P i).IsMaximal] (hk : ∀ i, I ≤ P i) (L : ι → ℕ) (K : Ideal A) (hle : ∏ i,769        P i ^ L i ≤ K) :770    K.map (Ideal.Quotient.mk I) ≠ ⊥ :=771  map_ne_bot_of_prod_pow_le f (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective P772    (fun i ↦ by rw [Ideal.mk_ker]; exact hk i) L K hle773 774/-- If the level kernels of finitely many exceptional points of the chart are generated by the775elements `F j`, then each `F j` with `j > 0` does not vanish on the exceptional divisor. -/776private theorem level_generator_ne_zero (R : Type) [CommRing R] (t x : R)777    [(Ideal.span ({t,x} : Set R)).IsMaximal] (ι : Type) [Finite ι]778    (P : ι → Ideal (BlowupChart R t x)) [∀ i, (P i).IsMaximal] (hPe : ∀ i, chartBase R t x t ∈ P i)779    (g : ∀ i, CompletedLocalAt (BlowupChart R t x) (P i)) (L : ι → ℕ)780    (hfin : ∀ i, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map781      (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤ finiteLocalCurveIdeal782      (BlowupChart R t x) (P i) (chartBase R t x t) (g i) 1) (F : ℕ → BlowupChart R t x)783    (hF : ∀ j : ℕ, finiteSupportLevelKernel (BlowupChart R t x) ι P784      (fun i ↦ finiteLocalCurveIdeal (BlowupChart R t x) (P i) (chartBase R t x t) (g i) j)785      (chartBase R t x t) j = Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R t x t})^j)786      (F j)}) (j : ℕ) (hj : 0 < j) : Ideal.Quotient.mk (chartExceptional R t x) (F j) ≠ 0 := by787  have := Fintype.ofFinite ι788  set K := finiteSupportKernel (BlowupChart R t x) ι P789      (fun i ↦ finiteLocalCurveIdeal (BlowupChart R t x) (P i) (chartBase R t x t) (g i) j)790  have hle : ∏ i, P i ^ (L i * j) ≤ K := by791    refine Ideal.prod_le_inf.trans ?_792    rw [Finset.inf_univ_eq_iInf]793    refine iInf_mono fun i ↦ completed_point_power_contraction _ (P i) (L i * j) _ ?_794    rw [pow_mul]795    refine (Ideal.pow_right_mono (hfin i) j).trans ?_796    dsimp only797    unfold finiteLocalCurveIdeal798    rw [Ideal.span_insert, Ideal.span_insert]799    refine (sup_pow_le_sup_pow _ _ j).trans ?_800    rw [Ideal.span_singleton_pow, pow_one]801  obtain ⟨e, -, -⟩ := exceptional_chart_is_affine_line R t x802  have e0 : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* ExceptionalChartLevel R t x 1 :=803    Ideal.quotEquivOfEq (by rw [exceptionalLevelIdeal, pow_one]; rfl)804  let f := e0.trans e805  have hKne : K.map (Ideal.Quotient.mk (chartExceptional R t x)) ≠ ⊥ := by806    refine map_mk_ne_bot_of_prod_pow_le (chartExceptional R t x) f P ?_ (fun i ↦ L i * j) K hle807    intro i; rw [chartExceptional, Ideal.span_le]; simpa using hPe i808  have hIj : chartExceptional R t x ^ j ≤ chartExceptional R t x := Ideal.pow_le_self hj.ne'809  intro h0810  apply hKne811  have hfac : Ideal.Quotient.mk (chartExceptional R t x) =812      (Ideal.Quotient.factor hIj).comp (Ideal.Quotient.mk (chartExceptional R t x ^ j)) :=813    (Ideal.Quotient.factor_comp_mk hIj).symm814  have : Ideal.map (Ideal.Quotient.mk (chartExceptional R t x ^ j)) K =815      Ideal.span {Ideal.Quotient.mk (chartExceptional R t x ^ j) (F j)} := hF j816  rw [hfac, ← Ideal.map_map, this, Ideal.map_span, Set.image_singleton]817  simpa using h0818 819/-- The generators `F j` of the level kernels of finitely many exceptional points of the chart are820nonzerodivisors modulo the powers of the exceptional divisor. -/821theorem finite_support_level_generator_regular (R : Type) [CommRing R] (t x : R)822    [(Ideal.span ({t,x} : Set R)).IsMaximal] (ι : Type) [Finite ι]823    (P : ι → Ideal (BlowupChart R t x)) [∀ i, (P i).IsMaximal] (hPe : ∀ i, chartBase R t x t ∈ P i)824    (g : ∀ i, CompletedLocalAt (BlowupChart R t x) (P i)) (L : ι → ℕ)825    (hfin : ∀ i, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map826      (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤ finiteLocalCurveIdeal827      (BlowupChart R t x) (P i) (chartBase R t x t) (g i) 1) (hreg : RegularParameterPair R t x)828    (F : ℕ → BlowupChart R t x) (hF : ∀ j : ℕ,829      finiteSupportLevelKernel (BlowupChart R t x) ι P830      (fun i ↦ finiteLocalCurveIdeal (BlowupChart R t x) (P i) (chartBase R t x t) (g i) j)831      (chartBase R t x t) j = Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R t x t})^j)832      (F j)}) (j : ℕ) :833    Function.Injective (fun c : BlowupChart R t x ⧸ (chartExceptional R t x)^j ↦ Ideal.Quotient.mk834      ((chartExceptional R t x)^j) (F j) * c) := by835  have := Fintype.ofFinite ι836  rcases Nat.eq_zero_or_pos j with rfl | hj837  · exact fun a b _ ↦ Subsingleton.elim (h := Ideal.Quotient.subsingleton_iff.mpr (by simp)) a b838  have hFne := level_generator_ne_zero R t x ι P hPe g L hfin F hF j hj839  obtain ⟨e, -, -⟩ := exceptional_chart_is_affine_line R t x840  have e0 : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* ExceptionalChartLevel R t x 1 :=841    Ideal.quotEquivOfEq (by rw [exceptionalLevelIdeal, pow_one]; rfl)842  have : IsDomain (BlowupChart R t x ⧸ chartExceptional R t x) := (e0.trans e).toMulEquiv.isDomain843  have hinj1 : Function.Injective (fun a : BlowupChart R t x ⧸ chartExceptional R t x ↦844      Ideal.Quotient.mk (chartExceptional R t x) (F j) * a) := fun _ _ ↦ mul_left_cancel₀ hFne845  exact regular_element_on_all_principal_power_quotients (BlowupChart R t x) (chartBase R t x t)846    (F j) (blowup_exceptional_parameter_regular R t x hreg) hinj1 j847 848/-- The images in the overlap of the generators `F j` of the level kernels of the opposite chart are849nonzerodivisors modulo the powers of the exceptional divisor. -/850theorem overlap_level_generator_regular (R : Type) [CommRing R] (t x : R)851    [(Ideal.span ({t,x} : Set R)).IsMaximal] (hreg : RegularParameterPair R t x)852    (_hregSwap : RegularParameterPair R x t) (beta : BlowupRestriction R t x) (ι : Type) [Finite ι]853    (P : ι → Ideal (BlowupChart R x t)) [∀ i, (P i).IsMaximal] (hPe : ∀ i, chartBase R x t x ∈ P i)854    (g : ∀ i, CompletedLocalAt (BlowupChart R x t) (P i)) (L : ι → ℕ)855    (hfin : ∀ i, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P i))).map856      (localCompletionMap (Localization.AtPrime (P i)))) ^ (L i) ≤ finiteLocalCurveIdeal857      (BlowupChart R x t) (P i) (chartBase R x t x) (g i) 1) (F : ℕ → BlowupChart R x t)858    (hF : ∀ j : ℕ, finiteSupportLevelKernel (BlowupChart R x t) ι P859      (fun i ↦ finiteLocalCurveIdeal (BlowupChart R x t) (P i) (chartBase R x t x) (g i) j)860      (chartBase R x t x) j = Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R x t x})^j)861      (F j)}) (j : ℕ) :862    Function.Injective (fun c : BlowupOverlap R t x ⧸ (Ideal.span {overlapException R t x})^j ↦863      Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^j) (beta.right (F j)) * c) := by864  have := Fintype.ofFinite ι865  rcases Nat.eq_zero_or_pos j with rfl | hj866  · exact fun a b _ ↦ Subsingleton.elim (h := Ideal.Quotient.subsingleton_iff.mpr (by simp)) a b867  have : (Ideal.span ({x,t} : Set R)).IsMaximal := by rw [Set.pair_comm]; infer_instance868  have hFne := level_generator_ne_zero R x t ι P hPe g L hfin F hF j hj869  obtain ⟨hdom, hker⟩ := overlap_exceptional_quotient_domain R t x hreg beta870  have hFne' : Ideal.Quotient.mk (Ideal.span {overlapException R t x}) (beta.right (F j)) ≠ 0 :=871    fun h0 ↦ hFne (Ideal.Quotient.eq_zero_iff_mem.mpr (hker _ h0))872  exact regular_element_on_all_principal_power_quotients (BlowupOverlap R t x)873    (overlapException R t x) (beta.right (F j))874    (nonzerodivisor_survives_localization _ _ _ (blowup_exceptional_parameter_regular R t x hreg))875    (fun a b hab ↦ mul_left_cancel₀ hFne' hab) j876 877/-! ### Residue series of strict transforms -/878 879/-- Killing `T` and reducing after a chart substitution of a series with coefficients mapped along880`ρ` leaves the residue of its (mapped) constant term. -/881private theorem residueKillT_chartSubst (O O' : Type) [CommRing O] [CommRing O'] [IsDomain O']882    [IsDiscreteValuationRing O'] (pi' : O') (hpi' : Irreducible pi') (ρ : O →+* O') (alpha : O')883    (s : TwoSeries O) :884    residueKillT O' (chartSubst O' alpha (MvPowerSeries.map ρ s)) = PowerSeries.C885    (IsLocalRing.residue O' (ρ (MvPowerSeries.constantCoeff s))) := by886  obtain ⟨hC, hT, hX, -⟩ := chartSubst_apply_generators O' alpha887  obtain ⟨kC, kT, kX, -, -⟩ := residueKillT_apply_ker O' pi' hpi'888  let L : TwoSeries O →+* PowerSeries (IsLocalRing.ResidueField O') :=889    (residueKillT O').comp ((chartSubst O' alpha : TwoSeries O' →+* TwoSeries O').comp890        (MvPowerSeries.map ρ))891  let R : TwoSeries O →+* PowerSeries (IsLocalRing.ResidueField O') :=892    (PowerSeries.C).comp ((IsLocalRing.residue O').comp (ρ.comp MvPowerSeries.constantCoeff))893  have hmT : MvPowerSeries.map ρ (axisT O) = axisT O' := by simp [axisT, MvPowerSeries.map_X]894  have hmX : MvPowerSeries.map ρ (axisX O) = axisX O' := by simp [axisX, MvPowerSeries.map_X]895  have LT : L (axisT O) = 0 := by896    simp only [L, RingHom.comp_apply]897    change residueKillT O' (chartSubst O' alpha (MvPowerSeries.map ρ (axisT O))) = 0898    rw [hmT, hT, kT]899  have LX : L (axisX O) = 0 := by900    change residueKillT O' (chartSubst O' alpha (MvPowerSeries.map ρ (axisX O))) = 0901    rw [hmX, hX, map_mul, kT, zero_mul]902  have RT : R (axisT O) = 0 := by simp [R, axisT]903  have RX : R (axisX O) = 0 := by simp [R, axisX]904  have h : L = R := by905    apply twoSeries_ringHom_ext_of_isNilpotent O _ L R906    · intro c907      change residueKillT O' (chartSubst O' alpha (MvPowerSeries.map ρ (MvPowerSeries.C c))) = _908      simp [R, MvPowerSeries.map_C, hC, kC]909    · rw [LT, RT]910    · rw [LX, RX]911    · rw [LT]; exact IsNilpotent.zero912    · rw [LX]; exact IsNilpotent.zero913  exact congrArg (fun f ↦ f s) h914 915/-- If a map from the chart into a concrete surface sends the base and slope to chart substitutions,916then the reduction modulo `T` of the image of any chart element is the residue polynomial of917that element, shifted by the residue of `alphaTilde`. -/918private theorem chart_point_residue_series_formula (O O' : Type) [CommRing O] [IsDomain O]919    [IsDiscreteValuationRing O] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ)920    [IsLocalRing (ConcreteSurface O pi u a b)] [CommRing O'] [IsDomain O']921    [IsDiscreteValuationRing O'] (pi' : O') (hpi' : Irreducible pi') (u' : (TwoSeries O')ˣ)922    (a' b' : ℕ) (ρ : O →+* O') (alphaTilde : O') (S : Type) [CommRing S]923    (Eq : S ≃+* ConcreteSurface O' pi' u' a' b') (ψ : (tChart O pi u a b) →+* S)924    (hbase : ∀ s : TwoSeries O, Eq (ψ (tBase O pi u a b (surfaceMk O pi u a b s))) =925      surfaceMk O' pi' u' a' b' (chartSubst O' alphaTilde (MvPowerSeries.map ρ s)))926    (hslope : Eq (ψ (tSlope O pi u a b)) =927      surfaceX O' pi' u' a' b' + algebraMap O' (ConcreteSurface O' pi' u' a' b') alphaTilde)928    (q : (ConcreteSurface O' pi' u' a' b' ⧸ Ideal.span {surfaceT O' pi' u' a' b'}) ≃+*929      PowerSeries (IsLocalRing.ResidueField O'))930    (hq : ∀ s' : TwoSeries O',931      q (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'}) (surfaceMk O' pi' u' a' b' s')) =932        residueKillT O' s')933    (e : ((tChart O pi u a b) ⧸ tExc O pi u a b) ≃+* Polynomial (kRes O pi u a b))934    (he : ∀ r : ConcreteSurface O pi u a b,935      e (Ideal.Quotient.mk (tExc O pi u a b) (tBase O pi u a b r)) =936        Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))937    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)938    (ι : kRes O pi u a b →+* (IsLocalRing.ResidueField O'))939    (hι : ∀ s : TwoSeries O,940      ι (IsLocalRing.residue (ConcreteSurface O pi u a b) (surfaceMk O pi u a b s)) =941        IsLocalRing.residue O' (ρ (MvPowerSeries.constantCoeff s))) :942    ∀ FA : tChart O pi u a b,943      q (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'}) (Eq (ψ FA))) =944        ((((e (Ideal.Quotient.mk (tExc O pi u a b) FA)).map ι).comp945          (Polynomial.X + Polynomial.C (IsLocalRing.residue O' alphaTilde)) :946          Polynomial (IsLocalRing.ResidueField O')) :947          PowerSeries (IsLocalRing.ResidueField O')) := by948  have hker := residueKillT_apply_ker O' pi' hpi'949  intro FA950  let Θ : tChart O pi u a b →+* PowerSeries (IsLocalRing.ResidueField O') :=951    ((q.toRingHom.comp (Ideal.Quotient.mk _)).comp Eq.toRingHom).comp ψ952  let Λ : tChart O pi u a b →+* PowerSeries (IsLocalRing.ResidueField O') :=953    ((((Polynomial.coeToPowerSeries.ringHom).comp954      (Polynomial.compRingHom (Polynomial.X + Polynomial.C955          (IsLocalRing.residue O' alphaTilde)))).comp956      (Polynomial.mapRingHom ι)).comp e.toRingHom).comp (Ideal.Quotient.mk _)957  have key : Θ = Λ := by958    apply Ideal.Quotient.ringHom_ext959    apply Polynomial.ringHom_ext960    · intro r961      obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective r962      have h1 := hbase s963      have h2 := he (surfaceMk O pi u a b s)964      have h3 := hι s965      simp only [chartBase, surfaceMk, RingHom.comp_apply] at h1 h2 h3966      simp only [Θ, Λ, RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom,967        h1, h2]968      rw [show Ideal.Quotient.mk _ (chartSubst O' alphaTilde (MvPowerSeries.map ρ s)) =969        surfaceMk O' pi' u' a' b' (chartSubst O' alphaTilde (MvPowerSeries.map ρ s)) from rfl, hq,970        residueKillT_chartSubst O O' pi' hpi' ρ alphaTilde s]971      simp [Polynomial.compRingHom, h3]972    · have h1 := hslope973      have h2 := heZ974      simp only [chartSlope] at h1 h2975      simp only [Θ, Λ, RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom,976        h1, h2]977      rw [show surfaceX O' pi' u' a' b' + algebraMap O'978          (ConcreteSurface O' pi' u' a' b') alphaTilde =979        surfaceMk O' pi' u' a' b' (axisX O' + MvPowerSeries.C alphaTilde) from rfl, hq, map_add,980        hker.2.2.1, hker.1]981      simp [Polynomial.compRingHom]982  exact congrArg (fun f ↦ f FA) key983 984private theorem residue_series_of_completion_equiv (O : Type) [CommRing O] [IsDomain O]985    [IsDiscreteValuationRing O] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ)986    [IsLocalRing (ConcreteSurface O pi u a b)] (P : Ideal (tChart O pi u a b)) [P.IsMaximal]987    [P.IsPrime] (e : ((tChart O pi u a b) ⧸ tExc O pi u a b) ≃+* Polynomial (kRes O pi u a b))988    (he : ∀ r : ConcreteSurface O pi u a b,989      e (Ideal.Quotient.mk (tExc O pi u a b) (tBase O pi u a b r)) =990        Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))991    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)992    (φ : Polynomial (kRes O pi u a b))993    (hPφ : (P.map (Ideal.Quotient.mk (tExc O pi u a b))).map e = Ideal.span {φ}) (O' : Type)994    [CommRing O'] [IsDomain O'] [IsDiscreteValuationRing O'] (pi' : O') (hpi' : Irreducible pi')995    (u' : (TwoSeries O')ˣ) (a' b' : ℕ) (ha' : 0 < a') (ρ : O →+* O') (alphaTilde : O')996    (Eq : CompletedLocalAt (tChart O pi u a b) P ≃+* ConcreteSurface O' pi' u' a' b')997    (hbase : ∀ s : TwoSeries O, Eq998      (completedPointMap (tChart O pi u a b) P (tBase O pi u a b (surfaceMk O pi u a b s))) =999      surfaceMk O' pi' u' a' b' (chartSubst O' alphaTilde (MvPowerSeries.map ρ s)))1000    (hslope : Eq (completedPointMap (tChart O pi u a b) P (tSlope O pi u a b)) = surfaceX O' pi' u'1001      a' b' + algebraMap O' (ConcreteSurface O' pi' u' a' b') alphaTilde)1002    (ι : kRes O pi u a b →+* (IsLocalRing.ResidueField O'))1003    (hι : ∀ s : TwoSeries O,1004      ι (IsLocalRing.residue (ConcreteSurface O pi u a b) (surfaceMk O pi u a b s)) =1005        IsLocalRing.residue O' (ρ (MvPowerSeries.constantCoeff s)))1006    (g2 : tChart O pi u a b) (hPg : P = Ideal.span {tBase O pi u a b (surfaceT O pi u a b), g2})1007    (hg2 : ∀ q : (ConcreteSurface O' pi' u' a' b' ⧸ Ideal.span {surfaceT O' pi' u' a' b'}) ≃+*1008      PowerSeries (IsLocalRing.ResidueField O'),1009      (∀ s' : TwoSeries O', q1010        (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'}) (surfaceMk O' pi' u' a' b' s')) =1011        residueKillT O' s') →1012      PowerSeries.constantCoeff (q (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'})1013        (Eq (completedPointMap (tChart O pi u a b) P g2)))) = 0) :1014    ∃ (q : (ConcreteSurface O' pi' u' a' b' ⧸ Ideal.span {surfaceT O' pi' u' a' b'}) ≃+*1015        PowerSeries (IsLocalRing.ResidueField O'))1016      (ι : kRes O pi u a b →+* IsLocalRing.ResidueField O')1017      (alphaBar : IsLocalRing.ResidueField O'),1018      Eq (completedPointMap (tChart O pi u a b) P (tBase O pi u a b (surfaceT O pi u a b))) =1019        surfaceT O' pi' u' a' b' ∧ (φ.map ι).eval alphaBar = 0 ∧1020      ∀ FA : tChart O pi u a b, q (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'})1021        (Eq (completedPointMap (tChart O pi u a b) P FA))) =1022        ((((e (Ideal.Quotient.mk (tExc O pi u a b) FA)).map ι).comp1023          (Polynomial.X + Polynomial.C alphaBar) : Polynomial (IsLocalRing.ResidueField O')) :1024          PowerSeries (IsLocalRing.ResidueField O')) := by1025  obtain ⟨q, hq⟩ := concrete_surface_quotient_T_equiv O' pi' hpi' u' a' b' ha'1026  have hform := chart_point_residue_series_formula O O' pi u a b pi' hpi' u' a' b' ρ alphaTilde1027    _ Eq (completedPointMap _ P) hbase hslope q hq e he heZ ι hι1028  have hT : Eq (completedPointMap (tChart O pi u a b) P (tBase O pi u a b (surfaceT O pi u a b))) =1029      surfaceT O' pi' u' a' b' := by1030    have h := hbase (axisT O)1031    rwa [show axisT O = MvPowerSeries.X 0 from rfl, MvPowerSeries.map_X,1032      show (MvPowerSeries.X 0 : TwoSeries O') = axisT O' from rfl,1033      (chartSubst_apply_generators O' alphaTilde).2.1] at h1034  refine ⟨q, ι, IsLocalRing.residue O' alphaTilde, hT, ?_, hform⟩1035  let Ψ : tChart O pi u a b →+* IsLocalRing.ResidueField O' :=1036    PowerSeries.constantCoeff.comp (q.toRingHom.comp ((Ideal.Quotient.mk _).comp1037      (Eq.toRingHom.comp (completedPointMap _ P))))1038  have hle : P ≤ RingHom.ker Ψ := by1039    rw [hPg, Ideal.span_le]1040    rintro z (rfl | rfl)1041    · simp only [SetLike.mem_coe, RingHom.mem_ker, Ψ, RingHom.comp_apply,1042        RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom, hT]1043      rw [(Ideal.Quotient.eq_zero_iff_mem).2 (Ideal.mem_span_singleton_self _), map_zero, map_zero]1044    · exact hg2 q hq1045  have hφmem : φ ∈ (P.map (Ideal.Quotient.mk (tExc O pi u a b))).map e := by1046    rw [hPφ]; exact Ideal.mem_span_singleton_self _1047  obtain ⟨y, hy, rfl⟩ := (Ideal.mem_map_iff_of_surjective _ e.surjective).1 hφmem1048  obtain ⟨FA, hFA, rfl⟩ := (Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective).1 hy1049  have h0 : Ψ FA = 0 := hle hFA1050  have h1 := congrArg PowerSeries.constantCoeff (hform FA)1051  simp only [Ψ, RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom] at h01052  rw [h0, ← PowerSeries.coeff_zero_eq_constantCoeff_apply, Polynomial.coeff_coe,1053    Polynomial.coeff_zero_eq_eval_zero, Polynomial.eval_comp] at h11054  simpa using h1.symm1055 1056/-- Under an identification `q` of `S ⧸ (T)` with `k⟦X⟧` through `residueKillT`, the class of `X`1057has zero constant term. -/1058private theorem constantCoeff_quotient_surfaceX (O' : Type) [CommRing O'] [IsDomain O']1059    [IsDiscreteValuationRing O'] (pi' : O') (hpi' : Irreducible pi') (u' : (TwoSeries O')ˣ)1060    (a' b' : ℕ) (q : (ConcreteSurface O' pi' u' a' b' ⧸ Ideal.span {surfaceT O' pi' u' a' b'}) ≃+*1061      PowerSeries (IsLocalRing.ResidueField O'))1062    (hq : ∀ s', q (Ideal.Quotient.mk _ (surfaceMk O' pi' u' a' b' s')) = residueKillT O' s') :1063    PowerSeries.constantCoeff (q (Ideal.Quotient.mk _ (surfaceX O' pi' u' a' b'))) = 0 := by1064  rw [show surfaceX O' pi' u' a' b' = surfaceMk O' pi' u' a' b' (axisX O') from rfl, hq,1065    (residueKillT_apply_ker O' pi' hpi').2.2.1]1066  simp1067 1068/-- Under an identification `q` of `S ⧸ (T)` with `k⟦X⟧` through `residueKillT`, the class of a1069constant `c` has constant term the residue of `c`. -/1070private theorem constantCoeff_quotient_algebraMap (O' : Type) [CommRing O'] [IsDomain O']1071    [IsDiscreteValuationRing O'] (pi' : O') (hpi' : Irreducible pi') (u' : (TwoSeries O')ˣ)1072    (a' b' : ℕ) (q : (ConcreteSurface O' pi' u' a' b' ⧸ Ideal.span {surfaceT O' pi' u' a' b'}) ≃+*1073      PowerSeries (IsLocalRing.ResidueField O'))1074    (hq : ∀ s', q (Ideal.Quotient.mk _ (surfaceMk O' pi' u' a' b' s')) = residueKillT O' s')1075    (c : O') : PowerSeries.constantCoeff (q (Ideal.Quotient.mk _1076      (algebraMap O' (ConcreteSurface O' pi' u' a' b') c))) = IsLocalRing.residue O' c := by1077  rw [show algebraMap O' (ConcreteSurface O' pi' u' a' b') c =1078    surfaceMk O' pi' u' a' b' (MvPowerSeries.C c) from rfl, hq,1079    (residueKillT_apply_ker O' pi' hpi').1]1080  simp1081 1082/-- At an exceptional point of the left chart of the concrete surface, the completed local ring is1083again a concrete surface, and the reduction modulo `T` of a chart element is its residue1084polynomial shifted by a root `ᾱ` of the direction polynomial `φ`. -/1085theorem concrete_strict_transform_residue_series (O : Type) [CommRing O] [IsDomain O]1086    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1087    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)1088    (a b : ℕ) (ha : 0 < a) [IsLocalRing (ConcreteSurface O pi u a b)]1089    (P : Ideal (tChart O pi u a b)) [P.IsMaximal] [P.IsPrime]1090    (hP : tBase O pi u a b (surfaceT O pi u a b) ∈ P)1091    (e : ((tChart O pi u a b) ⧸ tExc O pi u a b) ≃+* Polynomial (kRes O pi u a b))1092    (he : ∀ r : ConcreteSurface O pi u a b,1093      e (Ideal.Quotient.mk (tExc O pi u a b) (tBase O pi u a b r)) =1094        Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))1095    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)1096    (φ : Polynomial (kRes O pi u a b)) (_hφ : φ.Monic ∧ Irreducible φ)1097    (hPφ : (P.map (Ideal.Quotient.mk (tExc O pi u a b))).map e = Ideal.span {φ}) :1098    ∃ (O' : Type) (_ : CommRing O') (_ : IsDomain O') (_ : IsDiscreteValuationRing O')1099      (_ : IsAdicComplete (IsLocalRing.maximalIdeal O') O')1100      (_ : Finite (IsLocalRing.ResidueField O'))1101      (pi' : O') (u' : (TwoSeries O')ˣ) (a' b' : ℕ), Irreducible pi' ∧ 0 < a' ∧1102    ∃ (Eq : CompletedLocalAt (tChart O pi u a b) P ≃+* ConcreteSurface O' pi' u' a' b')1103      (q : (ConcreteSurface O' pi' u' a' b' ⧸ Ideal.span {surfaceT O' pi' u' a' b'}) ≃+*1104        PowerSeries (IsLocalRing.ResidueField O'))1105      (ι : kRes O pi u a b →+* IsLocalRing.ResidueField O')1106      (alphaBar : IsLocalRing.ResidueField O'),1107      Eq (completedPointMap (tChart O pi u a b) P (tBase O pi u a b (surfaceT O pi u a b))) =1108        surfaceT O' pi' u' a' b' ∧ (φ.map ι).eval alphaBar = 0 ∧1109      ∀ FA : tChart O pi u a b, q (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'})1110        (Eq (completedPointMap (tChart O pi u a b) P FA))) =1111        ((((e (Ideal.Quotient.mk (tExc O pi u a b) FA)).map ι).comp1112          (Polynomial.X + Polynomial.C alphaBar) : Polynomial (IsLocalRing.ResidueField O')) :1113          PowerSeries (IsLocalRing.ResidueField O')) := by1114  obtain ⟨e0, he0⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha1115  have h461 := concrete_surface_maximalIdeal_eq O pi hpi u a b ha1116  let κ : kRes O pi u a b ≃+* IsLocalRing.ResidueField O :=1117    (Ideal.quotEquivOfEq h461).trans e01118  have hκ (s : TwoSeries O) : κ (IsLocalRing.residue (ConcreteSurface O pi u a b)1119      (surfaceMk O pi u a b s)) = IsLocalRing.residue O (MvPowerSeries.constantCoeff s) := by1120    change e0 (Ideal.quotEquivOfEq h461 (Ideal.Quotient.mk _ (surfaceMk O pi u a b s))) = _1121    rw [Ideal.quotEquivOfEq_mk]1122    exact he0 s1123  rcases concrete_chart_point_span_form O pi hpi u a b ha P hP with1124    hP1 | ⟨α, hα, hP2⟩ | ⟨Φ, hΦ, h2, hP3⟩1125  · obtain ⟨Eq, hb, hs, -⟩ := t_chart_origin_completion_equiv O pi hpi u a b ha P hP11126    refine ⟨O, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance, pi,1127      substUnit O 0 u, a + b, b, hpi, by omega, Eq, ?_⟩1128    refine residue_series_of_completion_equiv O pi u a b P e he heZ φ hPφ O pi hpi1129      (substUnit O 0 u) (a + b) b (by omega) (RingHom.id O) 0 Eq1130      (fun s ↦ by rw [MvPowerSeries.map_id]; exact hb s) (by rw [hs, map_zero, add_zero])1131      κ.toRingHom hκ _ hP1 fun q hq ↦ ?_1132    rw [hs]; exact constantCoeff_quotient_surfaceX O pi hpi _ _ _ q hq1133  · obtain ⟨Eq, hb, hs, hc⟩ := t_chart_unit_point_completion_equiv O pi hpi u a b ha α hα P hP21134    refine ⟨O, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance, pi,1135      substUnit O α u * shiftUnit O α hα ^ b, a + b, 0, hpi, by omega, Eq, ?_⟩1136    refine residue_series_of_completion_equiv O pi u a b P e he heZ φ hPφ O pi hpi _ (a + b) 01137      (by omega) (RingHom.id O) α Eq (fun s ↦ by rw [MvPowerSeries.map_id]; exact hb s) hs1138      κ.toRingHom hκ _ hP2 fun q hq ↦ ?_1139    rw [map_sub, map_sub, hs, hc, add_sub_cancel_right]1140    exact constantCoeff_quotient_surfaceX O pi hpi _ _ _ q hq1141  · have hθ := unramified_root_isUnit_of_two_le_natDegree O Φ hΦ h21142    obtain ⟨Eq, hb, hs, hc, -, -⟩ :=1143      t_chart_nonrational_point_completion_equiv O pi hpi u a b ha Φ hΦ hθ P hP31144    obtain ⟨hdom, hloc, hdvr, -, hirr, hcomp, hfin, -⟩ := unramified_is_dvr O Φ hΦ1145    let ρ : O →+* AdjoinRoot Φ := algebraMap O (AdjoinRoot Φ)1146    have : IsLocalHom ρ := by1147      refine ⟨fun x hx ↦ by_contra fun hnu ↦ ?_⟩1148      have hxm : x ∈ IsLocalRing.maximalIdeal O := hnu1149      rw [(IsDiscreteValuationRing.irreducible_iff_uniformizer pi).1 hpi,1150        Ideal.mem_span_singleton] at hxm1151      exact (hirr pi hpi).not_isUnit (isUnit_of_dvd_unit (map_dvd ρ hxm) hx)1152    refine ⟨AdjoinRoot Φ, inferInstance, hdom, hdvr, hcomp, hfin, ρ pi, _, a + b, 0, hirr pi hpi,1153      by omega, Eq, ?_⟩1154    refine residue_series_of_completion_equiv O pi u a b P e he heZ φ hPφ (AdjoinRoot Φ) (ρ pi)1155      (hirr pi hpi) _ (a + b) 0 (by omega) ρ (AdjoinRoot.root Φ) Eq hb hs1156      ((IsLocalRing.ResidueField.map ρ).comp κ.toRingHom) ?_ _ hP3 ?_1157    · exact fun s ↦ by simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe,1158        RingEquiv.coe_toRingHom, hκ, IsLocalRing.ResidueField.map_residue]1159    · intro q hq1160      let Ψ : tChart O pi u a b →+* IsLocalRing.ResidueField (AdjoinRoot Φ) :=1161        PowerSeries.constantCoeff.comp (q.toRingHom.comp ((Ideal.Quotient.mk _).comp1162          (Eq.toRingHom.comp (completedPointMap _ P))))1163      change Ψ _ = 01164      rw [Polynomial.hom_eval₂]1165      have h1 : Ψ.comp ((tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b))) =1166          (IsLocalRing.residue (AdjoinRoot Φ)).comp ρ := by1167        ext c1168        simp only [Ψ, RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom, hc]1169        exact constantCoeff_quotient_algebraMap (AdjoinRoot Φ) (ρ pi) (hirr pi hpi) _ _ _ q hq (ρ c)1170      have h2 : Ψ (tSlope O pi u a b) = IsLocalRing.residue (AdjoinRoot Φ) (AdjoinRoot.root Φ) := by1171        simp only [Ψ, RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom, hs,1172          map_add]1173        rw [constantCoeff_quotient_surfaceX (AdjoinRoot Φ) (ρ pi) (hirr pi hpi) _ _ _ q hq,1174          constantCoeff_quotient_algebraMap (AdjoinRoot Φ) (ρ pi) (hirr pi hpi) _ _ _ q hq,1175          zero_add]1176      rw [h1, h2, ← Polynomial.hom_eval₂, show ρ = AdjoinRoot.of Φ from rfl, AdjoinRoot.eval₂_root,1177        map_zero]1178 1179private theorem coeff_killX (O : Type) [CommRing O] (g : TwoSeries O) (n : ℕ) :1180    PowerSeries.coeff n (killX O g) = MvPowerSeries.coeff (Finsupp.single 0 n) g :=1181  coeff_substAlgHom_kill O _ (killXFamily_hasSubst O) 1 0 (by decide) rfl rfl g n1182 1183private theorem coeff_residueKillX (O : Type) [CommRing O] [IsLocalRing O] (g : TwoSeries O)1184    (n : ℕ) : PowerSeries.coeff n (residueKillX O g) =1185      IsLocalRing.residue O (MvPowerSeries.coeff (Finsupp.single 0 n) g) := by1186  rw [← coeff_killX]1187  rfl1188 1189/-- `residueKillX` sends constants to their residues, `T ↦ X` and `X ↦ 0`; it is surjective with1190kernel `(π, X)`, and it is compatible with the chart substitutions. -/1191private theorem residueKillX_apply_ker (O : Type) [CommRing O] [IsDomain O]1192    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) :1193    (∀ c : O, residueKillX O (MvPowerSeries.C c) = PowerSeries.C (IsLocalRing.residue O c)) ∧1194    residueKillX O (axisT O) = PowerSeries.X ∧ residueKillX O (axisX O) = 0 ∧ Function.Surjective1195    (residueKillX O) ∧ RingHom.ker (residueKillX O) = Ideal.span1196    {(MvPowerSeries.C pi : TwoSeries O), axisX O} ∧1197    (∀ s : TwoSeries O, killX O (xChartSubst O s) = killT O s) ∧ ∀ s : TwoSeries O, killX O1198    (chartSubst O 0 s) = killX O s := by1199  have hX : ∀ i, MvPowerSeries.subst (killXFamily O) (MvPowerSeries.X i : TwoSeries O) =1200      killXFamily O i := fun i ↦ MvPowerSeries.subst_X (killXFamily_hasSubst O) i1201  have hM := fun a b : TwoSeries O ↦ MvPowerSeries.subst_mul (killXFamily_hasSubst O) a b1202  refine ⟨fun c ↦ ?_, ?_, ?_, ?_, ?_, fun s ↦ ?_, fun s ↦ ?_⟩1203  · ext n1204    rw [coeff_residueKillX]1205    by_cases hn : n = 01206    · subst hn; simp [MvPowerSeries.coeff_C]1207    · simp [MvPowerSeries.coeff_C, PowerSeries.coeff_C, hn]1208  · ext n1209    rw [coeff_residueKillX]1210    by_cases hn : n = 11211    · subst hn; simp [axisT, MvPowerSeries.coeff_X]1212    · simp only [Fin.isValue, axisT, MvPowerSeries.coeff_X, MonoidWithZeroHom.map_ite_one_zero,1213        PowerSeries.coeff_X, hn, ↓reduceIte, ite_eq_right_iff, one_ne_zero, imp_false]1214      intro h; have := congrArg (fun f ↦ f 0) h1215      simp only [Fin.isValue, Finsupp.single_eq_same] at this; exact hn this1216  · ext n1217    rw [coeff_residueKillX]1218    simp only [Fin.isValue, axisX, MvPowerSeries.coeff_X, MonoidWithZeroHom.map_ite_one_zero,1219      map_zero, ite_eq_right_iff, one_ne_zero, imp_false]1220    intro h; have := congrArg (fun f ↦ f 1) h; simp at this1221  · intro h1222    let g : TwoSeries O := fun m ↦1223      if m 1 = 0 then (IsLocalRing.residue_surjective (PowerSeries.coeff (m 0) h)).choose else 01224    refine ⟨g, ?_⟩1225    ext n1226    rw [coeff_residueKillX]1227    change IsLocalRing.residue O (if _ then _ else _) = _1228    simp only [Fin.isValue, ne_eq, one_ne_zero, not_false_eq_true, Finsupp.single_eq_of_ne,1229      ↓reduceIte, Finsupp.single_eq_same]1230    exact (IsLocalRing.residue_surjective (PowerSeries.coeff n h)).choose_spec1231  · ext g1232    rw [RingHom.mem_ker, axisX, mvPowerSeries_mem_span_C_var_iff]1233    have hm (x : O) : IsLocalRing.residue O x = 0 ↔ pi ∣ x := by1234      rw [IsLocalRing.residue_eq_zero_iff, hpi.maximalIdeal_eq, Ideal.mem_span_singleton]1235    constructor1236    · intro hg m hm01237      have := congrArg (PowerSeries.coeff (m (0 : Fin 2))) hg1238      rw [coeff_residueKillX, map_zero (PowerSeries.coeff _), hm] at this1239      have hmeq : Finsupp.single (0 : Fin 2) (m (0 : Fin 2)) = m := by1240        ext i; fin_cases i <;> simp [hm0]1241      rwa [hmeq] at this1242    · refine fun hg ↦ PowerSeries.ext fun n ↦ ?_1243      rw [coeff_residueKillX, map_zero, hm]1244      exact hg _ (by simp)1245  · simp only [killX, xChartSubst, killT, MvPowerSeries.coe_substAlgHom]1246    rw [MvPowerSeries.subst_comp_subst_apply (xChartFamily_hasSubst O) (killXFamily_hasSubst O)]1247    congr 11248    funext i1249    fin_cases i1250    · simp only [xChartFamily, axisT, axisX, Fin.zero_eta, Matrix.cons_val_zero]1251      rw [hM, hX, hX]; simp [killXFamily, killTFamily]1252    · simp only [xChartFamily, axisT, axisX, Fin.mk_one, Matrix.cons_val_one,1253        Matrix.cons_val_fin_one]1254      rw [hX]; simp [killXFamily, killTFamily]1255  · simp only [killX, chartSubst, MvPowerSeries.coe_substAlgHom]1256    rw [MvPowerSeries.subst_comp_subst_apply (tChartFamily_hasSubst O 0) (killXFamily_hasSubst O)]1257    congr 11258    funext i1259    fin_cases i1260    · simp only [tChartFamily, axisT, axisX, Fin.zero_eta, Matrix.cons_val_zero]1261      rw [hX]1262    · simp only [tChartFamily, axisT, axisX, map_zero, add_zero, Fin.mk_one, Matrix.cons_val_one,1263        Matrix.cons_val_fin_one]1264      rw [hM, hX, hX]; simp [killXFamily]1265 1266/-- For `b > 0`, the quotient of the concrete surface by `X` is the power series ring over the1267residue field, via `residueKillX`. -/1268private theorem concrete_surface_quotient_X_equiv (O : Type) [CommRing O] [IsDomain O]1269    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)1270    (hb : 0 < b) :1271    ∃ q : (ConcreteSurface O pi u a b ⧸ Ideal.span {surfaceX O pi u a b}) ≃+* PowerSeries1272    (IsLocalRing.ResidueField O), ∀ s : TwoSeries O, q1273    (Ideal.Quotient.mk (Ideal.span {surfaceX O pi u a b}) (surfaceMk O pi u a b s)) =1274    residueKillX O s := by1275  obtain ⟨-, -, -, hsurj, hker, -⟩ := residueKillX_apply_ker O pi hpi1276  set I := surfaceIdeal O pi u a b1277  set J : Ideal (TwoSeries O) := Ideal.span {axisX O}1278  have h1 : Ideal.span {surfaceX O pi u a b} = J.map (Ideal.Quotient.mk I) := by1279    rw [Ideal.map_span, Set.image_singleton]; rfl1280  have hdiff : surfaceRelation O pi u a b - MvPowerSeries.C pi ∈ J := by1281    obtain ⟨b', rfl⟩ : ∃ b', b = b' + 1 := ⟨b - 1, by omega⟩1282    have : surfaceRelation O pi u a (b'+1) - MvPowerSeries.C pi1283        = axisX O * (-(u : TwoSeries O) * axisT O ^ a * axisX O ^ b') := by1284      unfold surfaceRelation; ring1285    rw [this]; exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)1286  have hX : axisX O ∈ J := Ideal.subset_span rfl1287  have h2 : I ⊔ J = RingHom.ker (residueKillX O) := by1288    rw [hker]1289    apply le_antisymm1290    · refine sup_le ?_ ?_1291      · refine Ideal.span_le.2 ?_1292        rintro _ rfl1293        have : surfaceRelation O pi u a b =1294            (surfaceRelation O pi u a b - MvPowerSeries.C pi) + MvPowerSeries.C pi := by ring1295        change _ ∈ _1296        rw [this]1297        refine Ideal.add_mem _ ?_ (Ideal.subset_span (by simp))1298        exact (Ideal.span_mono (by simp) : J ≤ _) hdiff1299      · exact Ideal.span_mono (by simp)1300    · refine Ideal.span_le.2 ?_1301      rintro _ (rfl | rfl)1302      · have : (MvPowerSeries.C pi : TwoSeries O) = surfaceRelation O pi u a b -1303          (surfaceRelation O pi u a b - MvPowerSeries.C pi) := by ring1304        rw [SetLike.mem_coe, this]1305        exact Ideal.sub_mem _ (Ideal.mem_sup_left (Ideal.subset_span rfl))1306            (Ideal.mem_sup_right hdiff)1307      · exact Ideal.mem_sup_right hX1308  refine ⟨((Ideal.quotEquivOfEq h1).trans (DoubleQuot.quotQuotEquivQuotSup I J)).trans1309    ((Ideal.quotEquivOfEq h2).trans (RingHom.quotientKerEquivOfSurjective hsurj)), fun _ ↦ rfl⟩1310 1311/-! ### Boundary contact numbers -/1312 1313private theorem length_quotient_comap_of_surjective {S T : Type} [CommRing S] [CommRing T]1314    (φ : S →+* T) (hφ : Function.Surjective φ) (J : Ideal T) :1315    Module.length S (S ⧸ J.comap φ) = Module.length T (T ⧸ J) := by1316  have : RingHomSurjective φ := ⟨hφ⟩1317  let g := Ideal.quotientMap J φ le_rfl1318  let f : (S ⧸ J.comap φ) →ₛₗ[φ] (T ⧸ J) :=1319    { toFun := g1320      map_add' := map_add g1321      map_smul' := by1322        intro s x1323        induction x using Quotient.inductionOn' with1324        | h x =>1325          change g (Ideal.Quotient.mk _ (s * x)) = _1326          simp only [g, Ideal.quotientMap_mk, map_mul]1327          rfl }1328  have hb : Function.Bijective f := ⟨Ideal.quotientMap_injective,1329      Ideal.quotientMap_surjective (H := le_rfl) hφ⟩1330  apply WithBot.coe_injective1331  rw [Module.coe_length, Module.coe_length,1332    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComapOfBijective f hb)]1333 1334private theorem length_quotient_sup_eq_order {S k : Type} [CommRing S] [Field k]1335    (φ : S →+* PowerSeries k) (hφ : Function.Surjective φ) (w g : S)1336    (hker : RingHom.ker φ = Ideal.span {w}) :1337    Module.length S (S ⧸ (Ideal.span {g} ⊔ Ideal.span {w})) = (φ g).order := by1338  have h1 : Ideal.span {g} ⊔ Ideal.span {w} = (Ideal.span {φ g}).comap φ := by1339    rw [← Set.image_singleton, ← Ideal.map_span, Ideal.comap_map_of_surjective _ hφ,1340      ← RingHom.ker_eq_comap_bot, hker]1341  rw [h1, length_quotient_comap_of_surjective φ hφ,1342      (powerSeries_quotient_length_eq_order k _).1]1343 1344/-- Composing a ring isomorphism `E : S ≃+* T` with the projection onto `T ⧸ (y)` and an1345isomorphism `q` of that quotient with `k⟦X⟧` gives a surjection with kernel `(w)`, where1346`E w = y`. -/1347private theorem surjective_ker_comp_quotient_equiv {S T k : Type} [CommRing S] [CommRing T]1348    [Field k] (E : S ≃+* T) (y : T) (q : (T ⧸ Ideal.span {y}) ≃+* PowerSeries k) (w : S)1349    (hw : E w = y) :1350    Function.Surjective (q.toRingHom.comp ((Ideal.Quotient.mk (Ideal.span {y})).comp E.toRingHom)) ∧1351    RingHom.ker (q.toRingHom.comp ((Ideal.Quotient.mk (Ideal.span {y})).comp E.toRingHom)) =1352      Ideal.span {w} := by1353  refine ⟨q.surjective.comp (Ideal.Quotient.mk_surjective.comp E.surjective), ?_⟩1354  have hspan : Ideal.span {y} = (Ideal.span {w}).map E.toRingHom := by1355    rw [Ideal.map_span, Set.image_singleton]; exact congrArg _ (congrArg _ hw.symm)1356  rw [RingHom.ker_comp_of_injective _ q.injective, ← RingHom.comap_ker, Ideal.mk_ker, hspan]1357  exact Ideal.comap_map_of_bijective E.toRingHom E.bijective1358 1359/-- The intersection length of a degree-`d` form with `(T)` on the concrete surface is `d` plus the1360intersection length of its strict transform with the exceptional divisor at the point at1361infinity. -/1362theorem concrete_infinity_boundary_contact (O : Type) [CommRing O] [IsDomain O](4.6)1363    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1364    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)1365    (a b : ℕ) (ha : 0 < a) (d : ℕ) (f : (ConcreteSurface O pi u a b))1366    (c : Fin (d + 1) → (ConcreteSurface O pi u a b))1367    (hc : f = ∑ i : Fin (d + 1), c i * (surfaceT O pi u a b) ^ (d - i.val) *1368      (surfaceX O pi u a b) ^ i.val)1369    (Pinf : Ideal (xChart O pi u a b)) [Pinf.IsMaximal] [Pinf.IsPrime]1370    (hx : xBase O pi u a b (surfaceX O pi u a b) ∈ Pinf) (hW : xSlope O pi u a b ∈ Pinf) :1371    Module.length (ConcreteSurface O pi u a b)1372    ((ConcreteSurface O pi u a b) ⧸ (Ideal.span {f} ⊔ Ideal.span {(surfaceT O pi u a b)})) =1373    (d : ℕ∞) + Module.length (CompletedLocalAt (xChart O pi u a b) Pinf)1374    (CompletedLocalAt (xChart O pi u a b) Pinf ⧸1375      (Ideal.span {completedPointMap (xChart O pi u a b) Pinf1376          (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *1377            (xSlope O pi u a b)^(d - i.val))} ⊔1378        Ideal.span {completedPointMap (xChart O pi u a b) Pinf (xSlope O pi u a b)})) := by1379  obtain ⟨s, hs⟩ := Ideal.Quotient.mk_surjective (c (Fin.last d))1380  change surfaceMk O pi u a b s = _ at hs1381  have hvan : ∀ {M : Type} [CommMonoidWithZero M] (i : Fin d), (0 : M) ^1382      (d - (Fin.castSucc i).val) = 0 :=1383    fun i ↦ zero_pow (by simp; omega)1384  -- parent side1385  obtain ⟨q, hq⟩ := concrete_surface_quotient_T_equiv O pi hpi u a b ha1386  let φ := q.toRingHom.comp (Ideal.Quotient.mk (Ideal.span {surfaceT O pi u a b}))1387  have hφs : Function.Surjective φ := q.surjective.comp Ideal.Quotient.mk_surjective1388  have hφk : RingHom.ker φ = Ideal.span {surfaceT O pi u a b} := by1389    rw [RingHom.ker_comp_of_injective _ q.injective, Ideal.mk_ker]1390  have hφ : ∀ t, φ (surfaceMk O pi u a b t) = residueKillT O t := fun t ↦ hq t1391  obtain ⟨hC, hT, hX, -⟩ := residueKillT_apply_ker O pi hpi1392  rw [length_quotient_sup_eq_order φ hφs _ f hφk]1393  have hf : φ f = residueKillT O s * PowerSeries.X ^ d := by1394    rw [hc, map_sum, Fin.sum_univ_castSucc]1395    simp only [map_mul, map_pow, surfaceT, surfaceX, hφ, hT, hX]1396    rw [Finset.sum_eq_zero (fun i _ ↦ by rw [hvan i, mul_zero, zero_mul])]1397    simp [← hs, hφ]1398  -- child side1399  obtain ⟨hP, -⟩ := concrete_infinity_point_completion O pi hpi u a b ha Pinf hx hW1400  obtain ⟨E, hE1, hE2, -⟩ := x_chart_infinity_completion_equiv O pi hpi u a b ha Pinf hP1401  obtain ⟨q', hq'⟩ := concrete_surface_quotient_X_equiv O pi hpi (xSubstUnit O u) (a + b) a ha1402  obtain ⟨-, -, hX', -, -, hKX, -⟩ := residueKillX_apply_ker O pi hpi1403  let ψ := q'.toRingHom.comp1404    ((Ideal.Quotient.mk (Ideal.span {surfaceX O pi (xSubstUnit O u) (a + b) a})).comp E.toRingHom)1405  obtain ⟨hψs, hψk⟩ := surjective_ker_comp_quotient_equiv E _ q' _ hE21406  rw [length_quotient_sup_eq_order ψ hψs _ _ hψk]1407  have hψW : ψ (completedPointMap _ Pinf (xSlope O pi u a b)) = 0 := by1408    change q' (Ideal.Quotient.mk _ (E _)) = 01409    rw [hE2, Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_span_singleton_self _), map_zero]1410  have hψB (t) : ψ (completedPointMap _ Pinf (xBase O pi u a b (surfaceMk O pi u a b t))) =1411      residueKillT O t := by1412    change q' (Ideal.Quotient.mk _ (E _)) = _1413    rw [hE1, hq']1414    simp only [residueKillX, residueKillT, RingHom.comp_apply]1415    exact congrArg _ (hKX t)1416  have hg : ψ (completedPointMap _ Pinf (∑ i : Fin (d+1),1417      algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *1418      (xSlope O pi u a b)^(d - i.val))) = residueKillT O s := by1419    rw [map_sum, map_sum, Fin.sum_univ_castSucc]1420    simp only [map_mul, map_pow, hψW]1421    rw [Finset.sum_eq_zero (fun i _ ↦ by rw [hvan i, mul_zero])]1422    simp only [Fin.val_last, Nat.sub_self, pow_zero, mul_one, zero_add, ← hs]1423    exact hψB s1424  rw [hf, hg, PowerSeries.order_mul, PowerSeries.order_X_pow, add_comm]1425 1426/-- The intersection length of a degree-`d` form with `(X)` on the concrete surface is `d` plus the1427intersection length of its strict transform with the exceptional divisor at the origin of the1428left chart. -/1429theorem concrete_zero_boundary_contact (O : Type) [CommRing O] [IsDomain O](4.6)1430    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1431    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)1432    (a b : ℕ) (ha : 0 < a) (hb : 0 < b) (d : ℕ) (f : (ConcreteSurface O pi u a b))1433    (c : Fin (d + 1) → (ConcreteSurface O pi u a b))1434    (hc : f = ∑ i : Fin (d + 1), c i * (surfaceT O pi u a b) ^ (d - i.val) *1435      (surfaceX O pi u a b) ^ i.val)1436    (P : Ideal (tChart O pi u a b)) [P.IsPrime]1437    (hP : P = Ideal.span {tBase O pi u a b (surfaceT O pi u a b), (tSlope O pi u a b)}) :1438    Module.length (ConcreteSurface O pi u a b)1439    ((ConcreteSurface O pi u a b) ⧸ (Ideal.span {f} ⊔ Ideal.span {(surfaceX O pi u a b)})) =1440    (d : ℕ∞) + Module.length (CompletedLocalAt (tChart O pi u a b) P)1441    (CompletedLocalAt (tChart O pi u a b) P ⧸1442      (Ideal.span {completedPointMap (tChart O pi u a b) P1443          (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *1444            (tSlope O pi u a b)^i.val)} ⊔1445        Ideal.span {completedPointMap (tChart O pi u a b) P (tSlope O pi u a b)})) := by1446  obtain ⟨s, hs⟩ := Ideal.Quotient.mk_surjective (c 0)1447  change surfaceMk O pi u a b s = _ at hs1448  have hvan : ∀ {M : Type} [CommMonoidWithZero M] (i : Fin d), (0 : M) ^ (Fin.succ i).val = 0 :=1449    fun i ↦ zero_pow (by simp)1450  -- parent side1451  obtain ⟨q, hq⟩ := concrete_surface_quotient_X_equiv O pi hpi u a b hb1452  let φ := q.toRingHom.comp (Ideal.Quotient.mk (Ideal.span {surfaceX O pi u a b}))1453  have hφs : Function.Surjective φ := q.surjective.comp Ideal.Quotient.mk_surjective1454  have hφk : RingHom.ker φ = Ideal.span {surfaceX O pi u a b} := by1455    rw [RingHom.ker_comp_of_injective _ q.injective, Ideal.mk_ker]1456  have hφ : ∀ t, φ (surfaceMk O pi u a b t) = residueKillX O t := fun t ↦ hq t1457  obtain ⟨hC, hT, hX, -, -, -, hKX⟩ := residueKillX_apply_ker O pi hpi1458  rw [length_quotient_sup_eq_order φ hφs _ f hφk]1459  have hf : φ f = residueKillX O s * PowerSeries.X ^ d := by1460    rw [hc, map_sum, Fin.sum_univ_succ]1461    simp only [map_mul, map_pow, surfaceT, surfaceX, hφ, hT, hX]1462    rw [Finset.sum_eq_zero (fun i _ ↦ by rw [hvan i, mul_zero])]1463    simp [← hs, hφ]1464  -- child side1465  obtain ⟨E, hE1, hE2, -⟩ := t_chart_origin_completion_equiv O pi hpi u a b ha P hP1466  obtain ⟨q', hq'⟩ := concrete_surface_quotient_X_equiv O pi hpi (substUnit O 0 u) (a + b) b hb1467  let ψ := q'.toRingHom.comp1468    ((Ideal.Quotient.mk (Ideal.span {surfaceX O pi (substUnit O 0 u) (a + b) b})).comp E.toRingHom)1469  obtain ⟨hψs, hψk⟩ := surjective_ker_comp_quotient_equiv E _ q' _ hE21470  rw [length_quotient_sup_eq_order ψ hψs _ _ hψk]1471  have hψW : ψ (completedPointMap _ P (tSlope O pi u a b)) = 0 := by1472    change q' (Ideal.Quotient.mk _ (E _)) = 01473    rw [hE2, Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_span_singleton_self _), map_zero]1474  have hψB (t) : ψ (completedPointMap _ P (tBase O pi u a b (surfaceMk O pi u a b t))) =1475      residueKillX O t := by1476    change q' (Ideal.Quotient.mk _ (E _)) = _1477    rw [hE1, hq']1478    simp only [residueKillX, RingHom.comp_apply]1479    exact congrArg _ (hKX t)1480  have hg : ψ (completedPointMap _ P (∑ i : Fin (d+1),1481      algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *1482      (tSlope O pi u a b)^i.val)) = residueKillX O s := by1483    rw [map_sum, map_sum, Fin.sum_univ_succ]1484    simp only [map_mul, map_pow, hψW]1485    rw [Finset.sum_eq_zero (fun i _ ↦ by rw [hvan i, mul_zero])]1486    simp only [Fin.val_zero, pow_zero, mul_one, add_zero, ← hs]1487    exact hψB s1488  rw [hf, hg, PowerSeries.order_mul, PowerSeries.order_X_pow, add_comm]1489 1490end SurfaceBlowup