Exceptional layers of the point blow-up

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Blowup.CurveOrders7 8/-!9# Exceptional layers of the point blow-up10 11Points and layers of the exceptional divisor of the blow-up of a two-dimensional local ring at12`(t, x)`. We identify the closed points of the exceptional fibre of the chart with monic13irreducible polynomials (affine directions) together with the point at infinity of the opposite14chart, compute their residue lengths, describe the principal layers `(e)^j ⧸ (e)^(j+1)` as15polynomial modules, and normalize glued generators at exceptional level one via Laurent16polynomial arithmetic.17 18## Main results19 20* `SurfaceBlowup.direction_point_maximal`, `SurfaceBlowup.infinity_point_maximal`: the closed21  points of the exceptional divisor and their lengths.22* `SurfaceBlowup.chart_point_eq_directionPoint`: every exceptional chart point is a direction23  point.24* `SurfaceBlowup.chart_layer_polynomial_coordinates`: layers are polynomial modules.25* `SurfaceBlowup.glued_level_one_normalization`: normalization of glued generators.26 27Provenance: `Thm_SurfaceBlowupV2_` nodes `laurent_monomial_shift_trailing_degree`,28`glued_level_one_normalization`, `laurent_nonnegative_twist_kernel`,29`laurent_split_nonnegative_twist`, `length_eq_of_surjective_onto_field`,30`blowup_chart_exceptional_point_polynomial`, `chart_point_eq_directionPoint`,31`direction_point_maximal`, `direction_point_overlap_maximal`, `infinity_point_maximal`,32`principal_layer_map_{kernel,range}`, `principal_layer_quotient_equiv`,33`chart_layer_polynomial_coordinates`, `rootMultiplicity_map_eq_count_normalizedFactors`.34-/35 36open scoped BigOperators ENNReal37 38namespace SurfaceBlowup39 40/-- If `PA = c T^m · T^d · PB(T⁻¹)` in `k[T, T⁻¹]` with `PA, PB ≠ 0`, then the trailing degree of41`PA` is `m + d - deg PB`. -/42private theorem laurent_monomial_shift_trailing_degree (k : Type) [Field k] (PA PB : Polynomial k)43    (hA : PA ≠ 0) (hB : PB ≠ 0) (c : k) (m : ℤ) (d : ℕ)44    (h : PA.toLaurent = LaurentPolynomial.C c * LaurentPolynomial.T m *45      (LaurentPolynomial.T (d : ℤ) * LaurentPolynomial.invert (R := k) PB.toLaurent)) :46    (PA.natTrailingDegree : ℤ) = m + (d : ℤ) - (PB.natDegree : ℤ) := by47  set e : ℤ := m + d - PB.natDegree with he48  set a : ℕ := e.toNat49  set b : ℕ := (-e).toNat50  have hab : (a : ℤ) - b = e := by omega51  have hinv : LaurentPolynomial.invert (R := k) PB.toLaurent52      = PB.reverse.toLaurent * LaurentPolynomial.T (-(PB.natDegree : ℤ)) := by53    rw [LaurentPolynomial.toLaurent_reverse, mul_assoc, ← LaurentPolynomial.T_add]54    simp55  have key : PA * Polynomial.X ^ b = Polynomial.C c * Polynomial.X ^ a * PB.reverse := by56    apply Polynomial.toLaurent_injective57    simp only [map_mul, Polynomial.toLaurent_X_pow, Polynomial.toLaurent_C, h, hinv]58    have : LaurentPolynomial.T (R := k) m * (LaurentPolynomial.T (d : ℤ) *59        LaurentPolynomial.T (-(PB.natDegree : ℤ))) * LaurentPolynomial.T (b : ℤ)60        = LaurentPolynomial.T (a : ℤ) := by61      simp only [← LaurentPolynomial.T_add]; congr 1; omega62    rw [← this]63    ring64  have hc : c ≠ 0 := by65    rintro rfl66    exact hA (by simpa using key)67  have hR : PB.reverse.natTrailingDegree = 0 := Polynomial.natTrailingDegree_reverse _68  have := congrArg Polynomial.natTrailingDegree key69  rw [Polynomial.natTrailingDegree_mul hA (pow_ne_zero _ Polynomial.X_ne_zero),70    Polynomial.natTrailingDegree_mul (mul_ne_zero (Polynomial.C_ne_zero.2 hc)71      (pow_ne_zero _ Polynomial.X_ne_zero)) (by simpa using hB),72    Polynomial.natTrailingDegree_mul (Polynomial.C_ne_zero.2 hc)73      (pow_ne_zero _ Polynomial.X_ne_zero), hR] at this74  simp at this75  omega76 77/-- The coefficients of `∑_{i ≤ N} f i X^i`. -/78private theorem coeff_sum_fin_C_mul_X_pow {S : Type} [Semiring S] (N : ℕ)79    (f : Fin (N + 1) → S) (j : ℕ) :80    (∑ i : Fin (N + 1), Polynomial.C (f i) * Polynomial.X ^ i.val).coeff j =81      if h : j < N + 1 then f ⟨j, h⟩ else 0 := by82  simp only [Polynomial.finsetSum_coeff, Polynomial.coeff_C_mul_X_pow]83  split_ifs with h84  · rw [Finset.sum_eq_single ⟨j, h⟩ (fun i _ hi ↦ if_neg fun hj ↦ hi (Fin.ext hj.symm))85      (by simp)]86    simp87  · exact Finset.sum_eq_zero fun i _ ↦ if_neg (by omega)88 89open LaurentPolynomial in90/-- The exceptional fibre of the overlap chart of the blow-up at `(t, x)` embeds into the Laurent91polynomial ring `(R ⧸ (t, x))[z, z⁻¹]`, sending constants to constants and the slope to `z`; the92embedding has a ring-hom left inverse. -/93private theorem exists_overlap_exceptional_laurent (R : Type) [CommRing R] (t x : R) :94    ∃ (φ : (BlowupOverlap R t x ⧸ Ideal.span {overlapException R t x}) →+*95        LaurentPolynomial (R ⧸ Ideal.span ({t,x} : Set R)))96      (ψ : LaurentPolynomial (R ⧸ Ideal.span ({t,x} : Set R)) →+*97        (BlowupOverlap R t x ⧸ Ideal.span {overlapException R t x})),98      ψ.comp φ = RingHom.id _ ∧99      (∀ r : R, φ (Ideal.Quotient.mk _ (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)100        (chartBase R t x r))) = C (Ideal.Quotient.mk _ r)) ∧101      φ (Ideal.Quotient.mk _ (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)102        (chartSlope R t x))) = T 1 := by103  set I : Ideal R := Ideal.span ({t,x} : Set R)104  set E : Ideal (BlowupOverlap R t x) := Ideal.span {overlapException R t x}105  have htI : t ∈ I := Ideal.subset_span (by simp)106  have hxI : x ∈ I := Ideal.subset_span (by simp)107  let zQ : (BlowupOverlap R t x ⧸ E)ˣ :=108    ((IsLocalization.Away.algebraMap_isUnit (chartSlope R t x)).map (Ideal.Quotient.mk E)).unit109  let fK : (R ⧸ I) →+* (BlowupOverlap R t x ⧸ E) :=110    Ideal.Quotient.lift I ((Ideal.Quotient.mk E).comp (algebraMap R (BlowupOverlap R t x)))111      fun a ha ↦ by112        refine (Ideal.span_le.2 (Set.pair_subset ?_ ?_) : I ≤ RingHom.ker _) ha <;>113          simp only [SetLike.mem_coe, RingHom.mem_ker, RingHom.comp_apply,114            Ideal.Quotient.eq_zero_iff_mem] <;>115          rw [IsScalarTower.algebraMap_apply R (BlowupChart R t x)]116        · exact Ideal.subset_span rfl117        · change algebraMap _ _ (chartBase R t x x) ∈ _118          rw [← blowup_chart_relation, map_mul]119          exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)120  let ψ := eval₂ fK zQ121  let φ₀ : BlowupChart R t x →+* LaurentPolynomial (R ⧸ I) :=122    Ideal.Quotient.lift _ (Polynomial.eval₂RingHom (C.comp (Ideal.Quotient.mk I)) (T 1))123      fun a ha ↦ by124        obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.mp ha125        simp [blowupRelation, Ideal.Quotient.eq_zero_iff_mem.mpr htI,126          Ideal.Quotient.eq_zero_iff_mem.mpr hxI]127  have hφ₀ : IsUnit (φ₀ (chartSlope R t x)) := by128    simpa [φ₀, chartSlope] using isUnit_T (R := R ⧸ I) 1129  let φ₁ : BlowupOverlap R t x →+* LaurentPolynomial (R ⧸ I) :=130    IsLocalization.Away.lift (chartSlope R t x) hφ₀131  let φ : (BlowupOverlap R t x ⧸ E) →+* LaurentPolynomial (R ⧸ I) :=132    Ideal.Quotient.lift E φ₁ fun a ha ↦ by133      obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.mp ha134      simp [φ₁, overlapException, φ₀, chartBase, Ideal.Quotient.eq_zero_iff_mem.mpr htI]135  have hφA : ∀ a : BlowupChart R t x,136      φ (Ideal.Quotient.mk E (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) a)) = φ₀ a :=137    fun a ↦ by simp only [φ, φ₁, Ideal.Quotient.lift_mk, IsLocalization.Away.lift_eq]138  have hφ₀C : ∀ r : R, φ₀ (chartBase R t x r) = C (Ideal.Quotient.mk I r) :=139    fun r ↦ by simp [φ₀, chartBase]140  have hφ₀Z : φ₀ (chartSlope R t x) = T 1 := by simp [φ₀, chartSlope]141  have hψC : ∀ r : R, ψ (C (Ideal.Quotient.mk I r)) = Ideal.Quotient.mk E142      (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x r)) := fun r ↦ by143    simp only [ψ, eval₂_C, fK]144    rfl145  have hψφ : ψ.comp φ = RingHom.id _ := by146    refine Ideal.Quotient.ringHom_ext <|147      IsLocalization.ringHom_ext (Submonoid.powers (chartSlope R t x)) <|148      Ideal.Quotient.ringHom_ext <| Polynomial.ringHom_ext (fun a ↦ ?_) ?_ <;>149      simp only [RingHom.comp_apply, RingHom.id_apply] <;> rw [hφA]150    · have := hφ₀C a151      simp only [chartBase, RingHom.comp_apply] at this hψC152      rw [this]; exact hψC a153    · change ψ (φ₀ (chartSlope R t x)) = _154      rw [hφ₀Z]; simp [ψ, zQ, chartSlope]155  exact ⟨φ, ψ, hψφ, fun r ↦ (hφA _).trans (hφ₀C r), (hφA _).trans hφ₀Z⟩156 157open LaurentPolynomial in158/-- Normalization of glued generators at exceptional level one: if the images of the chart elements159`gA` and `gB` generate the same principal ideal of the exceptional divisor of the overlap, `gA`160reduces to a polynomial of trailing degree `r` and `gB` to one of degree `n` with `r + n = d`,161then `gA ≡ u · z^d · gB` modulo the exceptional divisor for some unit `u` of `R`. -/162theorem glued_level_one_normalization (R : Type) [CommRing R] (t x : R)163    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsLocalRing R] (_hreg : RegularParameterPair R t x)164    (beta : BlowupRestriction R t x) (d : ℕ) (gA : BlowupChart R t x) (gB : BlowupChart R x t)165    (hoverlap : Ideal.span {Ideal.Quotient.mk (Ideal.span {overlapException R t x})166      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) gA)} =167      Ideal.span {Ideal.Quotient.mk (Ideal.span {overlapException R t x}) (beta.right gB)})168    (hregB : Function.Injective (fun c : BlowupOverlap R t x ⧸169      (Ideal.span {overlapException R t x}) => Ideal.Quotient.mk170      (Ideal.span {overlapException R t x}) (beta.right gB) * c)) (m n : ℕ) (cA : Fin (m+1) → R)171    (cB : Fin (n+1) → R) (hgA : gA - ∑ i : Fin (m+1),172      algebraMap R (BlowupChart R t x) (cA i) * (chartSlope R t x)^i.val ∈ chartExceptional R t x)173    (hgB : gB - ∑ i : Fin (n+1), algebraMap R (BlowupChart R x t) (cB i) * (chartSlope R x t)^i.val174      ∈ chartExceptional R x t) (r : ℕ) (hlow : ∀ i : Fin (m+1), i.val < r →175      cA i ∈ Ideal.span {t,x}) (hr : ∀ i : Fin (m+1), i.val = r → cA i ∉ Ideal.span {t,x})176    (hrm : r ≤ m) (htop : cB (Fin.last n) ∉ Ideal.span {t,x}) (hdeg : r + n = d) :177    ∃ u : Rˣ, (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) gA - algebraMap R178    (BlowupOverlap R t x) (u : R) * ((overlapSlope R t x)^d * beta.right gB) ∈179    (Ideal.span {overlapException R t x}) := by180  -- Reduce both generators to Laurent polynomials over `R ⧸ (t, x)` on the exceptional fibre181  -- of the overlap; they differ by a unit `c z^m'` there, and comparing degrees gives `m' = d`.182  set I : Ideal R := Ideal.span ({t,x} : Set R)183  set E : Ideal (BlowupOverlap R t x) := Ideal.span {overlapException R t x}184  have htI : t ∈ I := Ideal.subset_span (by simp)185  have hxI : x ∈ I := Ideal.subset_span (by simp)186  obtain ⟨φ, ψ, hψφ, hφC, hφZ⟩ := exists_overlap_exceptional_laurent R t x187  have hψ : ∀ y, ψ (φ y) = y := RingHom.congr_fun hψφ188  set PA : Polynomial (R ⧸ I) :=189    ∑ i : Fin (m+1), Polynomial.C (Ideal.Quotient.mk I (cA i)) * Polynomial.X ^ i.val with hPA190  set PB : Polynomial (R ⧸ I) :=191    ∑ i : Fin (n+1), Polynomial.C (Ideal.Quotient.mk I (cB i)) * Polynomial.X ^ i.val with hPB192  have hPAr : PA.coeff r ≠ 0 := by193    rw [hPA, coeff_sum_fin_C_mul_X_pow, dif_pos (by omega), Ne, Ideal.Quotient.eq_zero_iff_mem]194    exact hr ⟨r, by omega⟩ rfl195  have hPA0 : PA ≠ 0 := fun h ↦ hPAr (by simp [h])196  have hPAtr : PA.natTrailingDegree = r :=197    le_antisymm (Polynomial.natTrailingDegree_le_of_ne_zero hPAr) <|198      Polynomial.le_natTrailingDegree hPA0 fun j hj ↦ by199        rw [hPA, coeff_sum_fin_C_mul_X_pow, dif_pos (by omega)]200        exact Ideal.Quotient.eq_zero_iff_mem.mpr (hlow ⟨j, by omega⟩ hj)201  have hPBn : PB.coeff n ≠ 0 := by202    rw [hPB, coeff_sum_fin_C_mul_X_pow, dif_pos (by omega), Ne, Ideal.Quotient.eq_zero_iff_mem]203    exact htop204  have hPB0 : PB ≠ 0 := fun h ↦ hPBn (by simp [h])205  have hPBdeg : PB.natDegree = n :=206    Polynomial.natDegree_eq_of_le_of_coeff_ne_zero (Polynomial.natDegree_le_iff_coeff_eq_zero.2207      fun j hj ↦ by rw [hPB, coeff_sum_fin_C_mul_X_pow, dif_neg (by omega)]) hPBn208  -- images209  let ΦA : BlowupChart R t x →+* LaurentPolynomial (R ⧸ I) :=210    φ.comp ((Ideal.Quotient.mk E).comp (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)))211  have hΦAexc : ∀ y ∈ chartExceptional R t x, ΦA y = 0 := fun y hy ↦ by212    obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.mp hy213    rw [map_mul, show ΦA (chartBase R t x t) = _ from hφC t,214      Ideal.Quotient.eq_zero_iff_mem.mpr htI, map_zero, mul_zero]215  have hφa : φ (Ideal.Quotient.mk E (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) gA)) =216      PA.toLaurent := by217    change ΦA gA = _218    rw [sub_eq_zero.1 ((map_sub ΦA _ _).symm.trans (hΦAexc _ hgA)), hPA, map_sum, map_sum]219    refine Finset.sum_congr rfl fun i _ ↦ ?_220    rw [map_mul, map_pow, Polynomial.toLaurent_C_mul_X_pow, show ΦA (chartSlope R t x) = _ from hφZ,221      T_pow, mul_one]222    exact congrArg (· * _) (hφC _)223  let ΦB : BlowupChart R x t →+* LaurentPolynomial (R ⧸ I) :=224    φ.comp ((Ideal.Quotient.mk E).comp beta.right.toRingHom)225  have hΦBC : ∀ c : R,226      ΦB (algebraMap R (BlowupChart R x t) c) = C (Ideal.Quotient.mk I c) := by227    intro c228    simp only [ΦB, RingHom.comp_apply, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgHom.commutes]229    rw [IsScalarTower.algebraMap_apply R (BlowupChart R t x) (BlowupOverlap R t x)]230    exact hφC c231  have hΦBW : ΦB (chartSlope R x t) = T (-1) := by232    simp only [ΦB, RingHom.comp_apply, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, beta.slope]233    have h1 : φ (Ideal.Quotient.mk E (IsLocalization.Away.invSelf (chartSlope R t x))) *234        T 1 = 1 := by235      rw [← hφZ, ← map_mul, ← map_mul, mul_comm, IsLocalization.Away.mul_invSelf, map_one,236        map_one]237    have h2 : T (-1) * T (R := R ⧸ I) 1 = 1 := by rw [← T_add]; simp238    exact (isUnit_T (R := R ⧸ I) 1).mul_left_injective (h1.trans h2.symm)239  have hΦBexc : ∀ y ∈ chartExceptional R x t, ΦB y = 0 := fun y hy ↦ by240    obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.mp hy241    rw [map_mul, show chartBase R x t x = algebraMap R _ x from rfl, hΦBC,242      Ideal.Quotient.eq_zero_iff_mem.mpr hxI, map_zero, mul_zero]243  have hφb : φ (Ideal.Quotient.mk E (beta.right gB)) = invert PB.toLaurent := by244    change ΦB gB = _245    rw [sub_eq_zero.1 ((map_sub ΦB _ _).symm.trans (hΦBexc _ hgB)), hPB, map_sum, map_sum, map_sum]246    refine Finset.sum_congr rfl fun i _ ↦ ?_247    rw [map_mul, map_pow, Polynomial.toLaurent_C_mul_X_pow, hΦBW, T_pow, hΦBC,248      map_mul, invert_C, invert_T]249    congr 2250    ring251  -- unit comparison252  obtain ⟨v, hv⟩ := regular_principal_generators_associated (BlowupOverlap R t x ⧸ E)253    (Ideal.Quotient.mk E (beta.right gB))254    (Ideal.Quotient.mk E (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) gA))255    (fun y₁ y₂ h ↦ hregB (by simpa [mul_comm] using h)) hoverlap.symm256  obtain ⟨c, hc, m', hm'⟩ :=257    (letI := Ideal.Quotient.field I; laurent_isUnit_iff_monomial (R ⧸ I) (φ v)).mp (v.isUnit.map φ)258  have hmain : PA.toLaurent = C c * T m' *259      (T ((0:ℕ):ℤ) * invert (R := R ⧸ I) PB.toLaurent) := by260    rw [← hφa, hv, map_mul, hm', hφb]; simp261  have hdeg' := letI := Ideal.Quotient.field I262    laurent_monomial_shift_trailing_degree (R ⧸ I) PA PB hPA0 hPB0 c m' 0 hmain263  rw [hPAtr, hPBdeg] at hdeg'264  have hm'd : m' = (d : ℤ) := by push_cast at hdeg'; omega265  obtain ⟨u, hu⟩ := units_lift_from_local_quotient R I266    (IsLocalRing.le_maximalIdeal (Ideal.IsMaximal.ne_top inferInstance))267    (letI := Ideal.Quotient.field I; isUnit_iff_ne_zero.mpr hc).unit268  simp only [IsUnit.unit_spec] at hu269  refine ⟨u, ?_⟩270  rw [← Ideal.Quotient.eq, hv, ← hψ v, hm', hm'd, ← hu, show T (d : ℤ) = T 1 ^ d by271    rw [T_pow, mul_one], ← hφC, ← hφZ, ← map_pow, ← map_mul, hψ]272  rw [show algebraMap R (BlowupOverlap R t x) u =273    algebraMap (BlowupChart R t x) _ (chartBase R t x u) from rfl]274  simp only [map_mul, map_pow, overlapSlope]275  ring276 277private theorem laurent_twist_kernel_coeff_toLaurent {k : Type} [CommRing k] (f : Polynomial k)278    (z : ℤ) : f.toLaurent.coeff z = if 0 ≤ z then f.coeff z.toNat else 0 := by279  split_ifs with hz280  · obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le hz281    rw [LaurentPolynomial.coeff_toLaurent]282    have := Finsupp.mapDomain_apply (Nat.castEmbedding (R := ℤ)).injective f.toFinsupp.coeff n283    simp only [Nat.castEmbedding_apply] at this284    simp only [Int.toNat_natCast]; exact this.trans rfl285  · rw [LaurentPolynomial.coeff_toLaurent]286    apply Finsupp.mapDomain_of_notMem_range287    rintro ⟨n, hn⟩288    simp at hn289    omega290 291private theorem toLaurent_coeff_of_eq_T_mul_invert {k : Type} [CommRing k] (m : ℕ)292    (P Q : Polynomial k)293    (h : P.toLaurent = LaurentPolynomial.T (m : ℤ) * LaurentPolynomial.invert (R := k) Q.toLaurent)294    (n : ℤ) : P.toLaurent.coeff n = Q.toLaurent.coeff (m - n) := by295  rw [h, LaurentPolynomial.T, AddMonoidAlgebra.coeff_single_mul_apply,296    LaurentPolynomial.invert_apply, one_mul]297  congr 1; ring298 299/-- If `P(T) = T^m · Q(T⁻¹)` in `k[T, T⁻¹]` with `m ≥ 0`, then `deg P ≤ m` and `Q` is the reversal300of `P` at level `m`. -/301theorem laurent_nonnegative_twist_kernel (k : Type) [CommRing k] (m : ℕ) (P Q : Polynomial k)302    (h : P.toLaurent =303      LaurentPolynomial.T (m : ℤ) * LaurentPolynomial.invert (R := k) Q.toLaurent) :304    P.natDegree ≤ m ∧ ∀ i : ℕ, Q.coeff i = if i ≤ m then P.coeff (m - i) else 0 := by305  have key := toLaurent_coeff_of_eq_T_mul_invert m P Q h306  simp only [laurent_twist_kernel_coeff_toLaurent] at key307  refine ⟨?_, fun i ↦ ?_⟩308  · rw [Polynomial.natDegree_le_iff_coeff_eq_zero]309    intro n hn310    have := key n311    simp only [Nat.cast_nonneg, if_true, Int.toNat_natCast] at this312    rw [this, if_neg]313    have : (m : ℕ) < n := by exact_mod_cast hn314    omega315  · split_ifs with hi316    · have := key ((m - i : ℕ) : ℤ)317      simp only [Nat.cast_nonneg, if_true, Int.toNat_natCast] at this318      rw [this, if_pos (by omega)]319      congr 1; omega320    · have := key ((m : ℤ) - i)321      rw [if_neg (by omega), if_pos (by omega)] at this322      rw [show ((m : ℤ) - ((m : ℤ) - i)).toNat = i by omega] at this323      exact this.symm324 325/-- For `m ≥ -1`, every Laurent polynomial can be written as `P(T) - T^m · Q(T⁻¹)` with `P, Q`326polynomials. -/327theorem laurent_split_nonnegative_twist (k : Type) [CommRing k] (m : ℤ) (hm : -1 ≤ m)328    (F : LaurentPolynomial k) :329    ∃ P Q : Polynomial k, F = P.toLaurent - LaurentPolynomial.T m *330    (LaurentPolynomial.invert (R := k) Q.toLaurent) := by331  induction F using LaurentPolynomial.induction_on' with332  | add p q hp hq =>333    obtain ⟨P1, Q1, h1⟩ := hp334    obtain ⟨P2, Q2, h2⟩ := hq335    refine ⟨P1 + P2, Q1 + Q2, ?_⟩336    rw [h1, h2]337    simp only [map_add]338    ring339  | C_mul_T n a =>340    rcases le_or_gt 0 n with hn | hn341    · refine ⟨Polynomial.C a * Polynomial.X ^ n.toNat, 0, ?_⟩342      simp only [map_zero, mul_zero, sub_zero, map_mul, Polynomial.toLaurent_C,343        Polynomial.toLaurent_X_pow]344      rw [Int.toNat_of_nonneg hn]345    · refine ⟨0, -(Polynomial.C a * Polynomial.X ^ (m - n).toNat), ?_⟩346      simp only [map_zero, map_neg, map_mul, Polynomial.toLaurent_C,347        Polynomial.toLaurent_X_pow, LaurentPolynomial.invert_C, LaurentPolynomial.invert_T,348        zero_sub, mul_neg, neg_neg]349      rw [Int.toNat_of_nonneg (by omega), mul_left_comm, ← LaurentPolynomial.T_add]350      congr 2351      ring352 353/-- If `R` acts on a finite-dimensional `k`-vector space `M` through a surjection `f : R → k`, then354the `R`-length of `M` equals its `k`-dimension. -/355private theorem length_eq_of_surjective_onto_field (R k M : Type) [CommRing R] [Field k]356    [AddCommGroup M]357    [Module R M] [Module k M] (f : R →+* k) (hf : Function.Surjective f)358    (hcompat : ∀ (r : R) (m : M), r • m = f r • m) [Module.Finite k M] :359    Module.length R M = (Module.finrank k M : ℕ∞) := by360  have : RingHomSurjective f := ⟨hf⟩361  let g : M →ₛₗ[f] M := ⟨AddHom.id M, fun r m ↦ hcompat r m⟩362  rw [← Module.length_eq_finrank k M]363  rw [Module.length, Module.length, WithBot.unbot_inj,364    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComapOfBijective g Function.bijective_id)]365 366/-- Given an identification `e` of the exceptional fibre of the chart with `(R/(t,x))[Z]`, a maximal367ideal `P` containing `t` corresponds to a monic irreducible `φ`: `P` maps onto `(φ)`, contains368the slope iff `φ = Z`, and has `R`-length `deg φ`. -/369theorem blowup_chart_exceptional_point_polynomial (R : Type) [CommRing R] (t x : R)370    [(Ideal.span ({t,x} : Set R)).IsMaximal]371    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial372      (R ⧸ Ideal.span ({t,x} : Set R))) (he : ∀ r : R,373      e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =374      Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r))375    (heZ : e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X)376    (P : Ideal (BlowupChart R t x)) [P.IsMaximal] (hP : chartBase R t x t ∈ P) :377    ∃ φ : Polynomial (R ⧸ Ideal.span ({t,x} : Set R)), φ.Monic ∧ Irreducible φ ∧378    (P.map (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {φ} ∧379    (chartSlope R t x ∈ P ↔ φ = Polynomial.X) ∧ Module.length R (BlowupChart R t x ⧸ P) =380    (φ.natDegree : ℕ∞) := by381  let : Field (R ⧸ Ideal.span ({t,x} : Set R)) := Ideal.Quotient.field _382  have hIP : chartExceptional R t x ≤ P := by383    rw [show chartExceptional R t x = Ideal.span {chartBase R t x t} from rfl, Ideal.span_le]384    simpa using hP385  set Pb := P.map (Ideal.Quotient.mk (chartExceptional R t x)) with hPb386  have hmk : Function.Surjective (Ideal.Quotient.mk (chartExceptional R t x)) :=387    Ideal.Quotient.mk_surjective388  have hcomap : Pb.comap (Ideal.Quotient.mk (chartExceptional R t x)) = P := by389    rw [hPb, Ideal.comap_map_of_surjective _ hmk]390    exact le_antisymm391      (sup_le le_rfl fun a ha ↦ hIP (by simpa [Ideal.Quotient.eq_zero_iff_mem] using ha))392      le_sup_left393  have hPbmax : Pb.IsMaximal :=394    (Ideal.map_eq_top_or_isMaximal_of_surjective _ hmk ‹P.IsMaximal›).resolve_left fun h ↦395      Ideal.IsMaximal.ne_top ‹_› (by rw [← hcomap, hPb, h, Ideal.comap_top])396  set Q := Pb.map e with hQ397  have hQmax : Q.IsMaximal := (Ideal.isMaximal_map_iff_of_bijective _ e.bijective).2 hPbmax398  obtain ⟨ψ, hψ'⟩ := IsPrincipalIdealRing.principal Q399  rw [Ideal.submodule_span_eq] at hψ'400  have hψ0 : ψ ≠ 0 := by401    rintro rfl402    rw [hψ', Ideal.span_singleton_eq_bot.2 rfl] at hQmax403    exact Polynomial.not_isField _ (Ring.isField_iff_maximal_bot.2 hQmax)404  have hψprime : Prime ψ := (Ideal.span_singleton_prime hψ0).1 (hψ' ▸ hQmax.isPrime)405  have hu : IsUnit (Polynomial.C ψ.leadingCoeff⁻¹) :=406    Polynomial.isUnit_C.2 (inv_ne_zero (Polynomial.leadingCoeff_ne_zero.2 hψ0)).isUnit407  set φ := ψ * Polynomial.C ψ.leadingCoeff⁻¹ with hφ408  have hmon : φ.Monic := Polynomial.monic_mul_leadingCoeff_inv hψ0409  have hirr : Irreducible φ := (associated_mul_unit_right ψ _ hu).irreducible hψprime.irreducible410  have hQφ : Ideal.span {φ} = Q := by rw [hφ, Ideal.span_singleton_mul_right_unit hu, ← hψ']411  refine ⟨φ, hmon, hirr, hQφ.symm, ?_, ?_⟩412  · rw [← hcomap, Ideal.mem_comap, ← Ideal.apply_mem_of_equiv_iff (f := e), heZ, ← hQ, ← hQφ,413      Ideal.mem_span_singleton]414    exact ⟨fun h ↦ Polynomial.eq_of_monic_of_associated hmon Polynomial.monic_X415      (associated_of_dvd_dvd h (hirr.dvd_symm Polynomial.irreducible_X h)), fun h ↦ h ▸ dvd_rfl⟩416  · let Ψ : (BlowupChart R t x ⧸ P) ≃+*417        (Polynomial (R ⧸ Ideal.span ({t,x} : Set R)) ⧸ Ideal.span {φ}) :=418      (DoubleQuot.quotQuotEquivQuotOfLE hIP).symm.trans (Ideal.quotientEquiv _ _ e hQφ)419    have hΨ : ∀ r : R, Ψ (Ideal.Quotient.mk P (chartBase R t x r)) =420        Ideal.Quotient.mk (Ideal.span {φ})421          (Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r)) := by422      intro r423      simp only [Ψ, RingEquiv.trans_apply, DoubleQuot.quotQuotEquivQuotOfLE_symm_mk]424      exact congrArg _ (he r)425    let L := (AlgEquiv.ofRingEquiv (R := R) (f := Ψ) (fun r ↦ hΨ r)).toLinearEquiv426    rw [L.length_eq]427    have : Module.Finite (R ⧸ Ideal.span ({t,x} : Set R))428        (Polynomial (R ⧸ Ideal.span ({t,x} : Set R)) ⧸ Ideal.span {φ}) :=429      Module.finite_of_finrank_pos430        (by rw [finrank_quotient_span_eq_natDegree]; exact hirr.natDegree_pos)431    rw [length_eq_of_surjective_onto_field R (R ⧸ Ideal.span ({t,x} : Set R)) _432      (Ideal.Quotient.mk _) Ideal.Quotient.mk_surjective ?_, finrank_quotient_span_eq_natDegree]433    intro r m434    exact (algebraMap_smul (R ⧸ Ideal.span ({t,x} : Set R)) r m).symm435 436/-- Every maximal ideal of the chart containing `t` is the direction point of an affine direction437`φ` over the residue field; it maps onto `(φ)` in the exceptional fibre and contains the slope438iff `φ` is the zero direction. -/439theorem chart_point_eq_directionPoint (R : Type) [CommRing R] [IsLocalRing R] (t x : R)440    [(Ideal.span ({t,x} : Set R)).IsMaximal]441    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (IsLocalRing.ResidueField R))442    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =443      Polynomial.C (IsLocalRing.residue R r))444    (heZ : e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X)445    (P : Ideal (BlowupChart R t x)) [P.IsMaximal] (hP : chartBase R t x t ∈ P) :446    ∃ φ : AffineDirection (IsLocalRing.ResidueField R), P = directionPoint R t x e φ ∧447    (P.map (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {φ.val} ∧448    (chartSlope R t x ∈ P ↔ φ = zeroAffine (IsLocalRing.ResidueField R)) := by449  have hm : Ideal.span ({t,x} : Set R) = IsLocalRing.maximalIdeal R :=450    IsLocalRing.eq_maximalIdeal ‹_›451  let κ : (R ⧸ Ideal.span ({t,x} : Set R)) ≃+* IsLocalRing.ResidueField R :=452    Ideal.quotEquivOfEq hm453  have hκ : ∀ r : R, κ (Ideal.Quotient.mk _ r) = IsLocalRing.residue R r := fun r ↦ rfl454  let M := Polynomial.mapEquiv κ455  let e₀ := e.trans M.symm456  have he₀ : ∀ r : R, e₀ (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =457      Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r) := by458    intro r459    apply M.injective460    simp only [e₀, RingEquiv.trans_apply, RingEquiv.apply_symm_apply, he]461    simp [M, Polynomial.mapEquiv_apply, hκ]462  have heZ₀ :463      e₀ (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X := by464    apply M.injective465    simp only [e₀, RingEquiv.trans_apply, RingEquiv.apply_symm_apply, heZ]466    simp [M, Polynomial.mapEquiv_apply]467  obtain ⟨φ₀, hmon, hirr, himg, hZ, -⟩ :=468    blowup_chart_exceptional_point_polynomial R t x e₀ he₀ heZ₀ P hP469  have hirr' : Irreducible (Polynomial.map κ.toRingHom φ₀) :=470    (MulEquiv.irreducible_iff M.toMulEquiv).2 hirr471  let φ : AffineDirection (IsLocalRing.ResidueField R) :=472    ⟨Polynomial.map κ.toRingHom φ₀, hmon.map _, hirr'⟩473  have himg' : (P.map (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {φ.val} := by474    have he : e.toRingHom = M.toRingHom.comp e₀.toRingHom := by475      exact RingHom.ext fun a ↦ by simp [e₀]476    change Ideal.map e.toRingHom _ = _477    rw [he, ← Ideal.map_map]478    change Ideal.map M (Ideal.map e₀ _) = _479    rw [himg, Ideal.map_span, Set.image_singleton]480    rfl481  refine ⟨φ, ?_, himg', ?_⟩482  · let ψ := e.toRingHom.comp (Ideal.Quotient.mk (chartExceptional R t x))483    have hψ : Function.Surjective ψ :=484      e.surjective.comp Ideal.Quotient.mk_surjective485    have hmap : P.map ψ = Ideal.span {φ.val} := by486      rw [← himg']487      change _ = Ideal.map e.toRingHom _488      rw [Ideal.map_map]489    change P = (Ideal.span {φ.val}).comap ψ490    rw [← hmap, Ideal.comap_map_of_surjective _ hψ]491    have hker : Ideal.comap ψ ⊥ = chartExceptional R t x := by492      rw [← RingHom.ker_eq_comap_bot]493      ext a494      simp [ψ, RingHom.mem_ker, Ideal.Quotient.eq_zero_iff_mem]495    rw [hker, eq_comm, sup_eq_left]496    exact (Ideal.span_singleton_le_iff_mem _).2 hP497  · rw [hZ]498    refine ⟨by rintro rfl; apply Subtype.ext; simp [φ, zeroAffine], fun h ↦ M.injective ?_⟩499    have := congrArg Subtype.val h500    simp only [φ, zeroAffine] at this501    simpa [M] using this502 503/-- The direction point of an affine direction `φ` is a maximal ideal containing `t`; it contains504the slope iff `φ` is the zero direction, maps onto `(φ)` in the exceptional fibre, has505`R`-length `deg φ`, and depends injectively on `φ`. -/506theorem direction_point_maximal (O R : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]507    [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R] (S : SurfaceData O R)508    (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+* Polynomial509      (IsLocalRing.ResidueField R)) (he : ∀ r : R,510      e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =511      Polynomial.C (IsLocalRing.residue R r))512    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)513    (φ : AffineDirection (IsLocalRing.ResidueField R)) :514    (directionPoint R S.t S.x e φ).IsMaximal ∧515    chartBase R S.t S.x S.t ∈ directionPoint R S.t S.x e φ ∧516    (chartSlope R S.t S.x ∈ directionPoint R S.t S.x e φ ↔ φ =517      zeroAffine (IsLocalRing.ResidueField R)) ∧518    ((directionPoint R S.t S.x e φ).map (Ideal.Quotient.mk (chartExceptional R S.t S.x))).map e =519    Ideal.span {φ.val} ∧ Module.length R (BlowupChart R S.t S.x ⧸ directionPoint R S.t S.x e φ) =520    (φ.val.natDegree : ℕ∞) ∧ Function.Injective (directionPoint R S.t S.x e) := by521  set k := IsLocalRing.ResidueField R522  set A := BlowupChart R S.t S.x523  set ψ : A →+* Polynomial k :=524    e.toRingHom.comp (Ideal.Quotient.mk (chartExceptional R S.t S.x))525  have hψ : Function.Surjective ψ :=526    e.surjective.comp Ideal.Quotient.mk_surjective527  have hP : ∀ φ' : AffineDirection k,528      directionPoint R S.t S.x e φ' = (Ideal.span {φ'.val}).comap ψ := fun _ ↦ rfl529  have hmap : ∀ φ' : AffineDirection k,530      ((directionPoint R S.t S.x e φ').map (Ideal.Quotient.mk (chartExceptional R S.t S.x))).map e531        = Ideal.span {φ'.val} := by532    intro φ'533    change Ideal.map e.toRingHom (Ideal.map (Ideal.Quotient.mk _) _) = _534    rw [Ideal.map_map, hP]535    exact Ideal.map_comap_of_surjective ψ hψ _536  have hmon : ∀ φ₁ φ₂ : AffineDirection k, Ideal.span {φ₁.val} = Ideal.span {φ₂.val} → φ₁ = φ₂ := by537    intro φ₁ φ₂ h538    rw [Ideal.span_singleton_eq_span_singleton] at h539    exact Subtype.ext (Polynomial.eq_of_monic_of_associated φ₁.2.1 φ₂.2.1 h)540  have hbase : ∀ r : R, ψ (chartBase R S.t S.x r) = Polynomial.C (IsLocalRing.residue R r) := he541  refine ⟨?_, ?_, ?_, hmap φ, ?_, ?_⟩542  · rw [hP]543    have := PrincipalIdealRing.isMaximal_of_irreducible φ.2.2544    exact Ideal.comap_isMaximal_of_surjective ψ hψ545  · rw [hP, Ideal.mem_comap, hbase]546    have ht : S.t ∈ IsLocalRing.maximalIdeal R := by547      rw [← S.parameters]; exact Ideal.subset_span (by simp)548    rw [(IsLocalRing.residue_eq_zero_iff _).2 ht, map_zero]549    exact zero_mem _550  · rw [hP, Ideal.mem_comap]551    change e (Ideal.Quotient.mk _ (chartSlope R S.t S.x)) ∈ _ ↔ _552    rw [heZ, Ideal.mem_span_singleton]553    constructor554    · intro h555      exact Subtype.ext (Polynomial.eq_of_monic_of_associated φ.2.1 Polynomial.monic_X556        (φ.2.2.associated_of_dvd Polynomial.irreducible_X h))557    · rintro rfl; exact dvd_refl _558  · let E : (A ⧸ directionPoint R S.t S.x e φ) ≃+* Polynomial k ⧸ Ideal.span {φ.val} :=559      (Ideal.quotEquivOfEq (by rw [← RingHom.comap_ker, Ideal.mk_ker, hP])).trans560        (RingHom.quotientKerEquivOfSurjective (f := (Ideal.Quotient.mk (Ideal.span {φ.val})).comp ψ)561          (Ideal.Quotient.mk_surjective.comp hψ))562    let L := (AlgEquiv.ofRingEquiv (R := R) (f := E)563      fun r ↦ congrArg (Ideal.Quotient.mk _) (hbase r)).toLinearEquiv564    rw [L.length_eq]565    have : Module.Finite k (Polynomial k ⧸ Ideal.span {φ.val}) := Module.finite_of_finrank_pos566      (by rw [finrank_quotient_span_eq_natDegree]; exact φ.2.2.natDegree_pos)567    rw [length_eq_of_surjective_onto_field R k _ (IsLocalRing.residue R)568      IsLocalRing.residue_surjective ?_, finrank_quotient_span_eq_natDegree]569    intro r m570    exact (algebraMap_smul k r m).symm571  · intro φ₁ φ₂ h572    apply hmon573    rw [← hmap φ₁, ← hmap φ₂, h]574 575/-- For a nonzero affine direction, the direction point generates a maximal ideal of the overlap576chart that contains `t` and contracts back to the direction point. -/577theorem direction_point_overlap_maximal (O R : Type) [CommRing O] [IsDomain O]578    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]579    (S : SurfaceData O R) (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+* Polynomial580      (IsLocalRing.ResidueField R)) (he : ∀ r : R,581      e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =582      Polynomial.C (IsLocalRing.residue R r))583    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)584    (φ : AffineDirection (IsLocalRing.ResidueField R))585    (hφ : φ ≠ zeroAffine (IsLocalRing.ResidueField R)) :586    ((directionPoint R S.t S.x e φ).map (algebraMap (BlowupChart R S.t S.x)587      (BlowupOverlap R S.t S.x))).IsMaximal ∧588    (algebraMap (BlowupChart R S.t S.x) (BlowupOverlap R S.t S.x)) (chartBase R S.t S.x S.t) ∈589    (directionPoint R S.t S.x e φ).map (algebraMap (BlowupChart R S.t S.x)590      (BlowupOverlap R S.t S.x)) ∧ ((directionPoint R S.t S.x e φ).map591      (algebraMap (BlowupChart R S.t S.x) (BlowupOverlap R S.t S.x))).comap592    (algebraMap (BlowupChart R S.t S.x) (BlowupOverlap R S.t S.x)) =593      directionPoint R S.t S.x e φ := by594  obtain ⟨hmax, ht, hZ, -⟩ := direction_point_maximal O R S e he heZ φ595  set P := directionPoint R S.t S.x e φ596  have hZP : chartSlope R S.t S.x ∉ P := fun h ↦ hφ (hZ.mp h)597  have hd : Disjoint ((Submonoid.powers (chartSlope R S.t S.x) : Submonoid _) :598      Set (BlowupChart R S.t S.x)) (P : Set _) := by599    rw [Set.disjoint_left]600    rintro _ ⟨n, rfl⟩ hn601    exact hZP (hmax.isPrime.mem_of_pow_mem n hn)602  have hcomap : (P.map (algebraMap (BlowupChart R S.t S.x) (BlowupOverlap R S.t S.x))).comap603      (algebraMap (BlowupChart R S.t S.x) (BlowupOverlap R S.t S.x)) = P :=604    IsLocalization.under_map_of_isPrime_disjoint (Submonoid.powers (chartSlope R S.t S.x)) _605      hmax.isPrime hd606  have hprime :=607    IsLocalization.isPrime_of_isPrime_disjoint (Submonoid.powers (chartSlope R S.t S.x))608    (BlowupOverlap R S.t S.x) P hmax.isPrime hd609  refine ⟨?_, Ideal.mem_map_of_mem _ ht, hcomap⟩610  obtain ⟨M, hM, hle⟩ := Ideal.exists_le_maximal _ hprime.ne_top611  have hcM : M.comap (algebraMap (BlowupChart R S.t S.x) (BlowupOverlap R S.t S.x)) = P := by612    refine (hmax.eq_of_le (Ideal.comap_ne_top _ hM.ne_top) ?_).symm613    rw [← hcomap]; exact Ideal.comap_mono hle614  have : M = P.map (algebraMap (BlowupChart R S.t S.x) (BlowupOverlap R S.t S.x)) := by615    rw [← hcM]; exact (IsLocalization.map_under (Submonoid.powers (chartSlope R S.t S.x)) _ M).symm616  rw [← this]; exact hM617 618/-- The point at infinity of the opposite chart is a maximal ideal containing `x` and the slope,619with `R`-length one. -/620theorem infinity_point_maximal (O R : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]621    [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R] (S : SurfaceData O R) :622    (infinityPoint R S.t S.x).IsMaximal ∧ chartBase R S.x S.t S.x ∈ infinityPoint R S.t S.x ∧623    chartSlope R S.x S.t ∈ infinityPoint R S.t S.x ∧ Module.length R624    (BlowupChart R S.x S.t ⧸ infinityPoint R S.t S.x) = 1 := by625  have hker : ∃ φ : BlowupChart R S.x S.t →+* IsLocalRing.ResidueField R,626      (∀ r, φ (chartBase R S.x S.t r) = IsLocalRing.residue R r) ∧627      φ (chartSlope R S.x S.t) = 0 ∧ RingHom.ker φ = infinityPoint R S.t S.x := by628    have hx : IsLocalRing.residue R S.x = 0 := by629      rw [IsLocalRing.residue_eq_zero_iff, ← S.parameters]630      exact Ideal.subset_span (by simp)631    have ht : IsLocalRing.residue R S.t = 0 := by632      rw [IsLocalRing.residue_eq_zero_iff, ← S.parameters]633      exact Ideal.subset_span (by simp)634    let ψ : Polynomial R →+* IsLocalRing.ResidueField R :=635      Polynomial.eval₂RingHom (IsLocalRing.residue R) 0636    have hψ : Ideal.span {blowupRelation R S.x S.t} ≤ RingHom.ker ψ := by637      rw [Ideal.span_le, Set.singleton_subset_iff]638      simp [ψ, blowupRelation, ht]639    refine ⟨Ideal.Quotient.lift _ ψ fun a ha ↦ hψ ha, fun r ↦ ?_, ?_, ?_⟩640    · change ψ (Polynomial.C r) = _641      simp [ψ]642    · change ψ Polynomial.X = _643      simp [ψ]644    · ext b645      obtain ⟨p, rfl⟩ := Ideal.Quotient.mk_surjective b646      have hrel := blowup_chart_relation R S.x S.t647      have hI_x : chartBase R S.x S.t S.x ∈ infinityPoint R S.t S.x := Ideal.subset_span (by simp)648      have hI_W : chartSlope R S.x S.t ∈ infinityPoint R S.t S.x := Ideal.subset_span (by simp)649      have hI_t : chartBase R S.x S.t S.t ∈ infinityPoint R S.t S.x := by650        rw [← hrel]; exact Ideal.mul_mem_right _ _ hI_x651      have hp := Polynomial.divX_mul_X_add p652      have hmk : Ideal.Quotient.mk (Ideal.span {blowupRelation R S.x S.t}) p =653          Ideal.Quotient.mk (Ideal.span {blowupRelation R S.x S.t}) (p.divX) * chartSlope R S.x S.t654          + chartBase R S.x S.t (p.coeff 0) := by655        conv_lhs => rw [← hp]656        simp [chartSlope, chartBase]657      have hψp : ψ p = IsLocalRing.residue R (p.coeff 0) := by658        simp [ψ, Polynomial.eval₂_at_zero]659      simp only [RingHom.mem_ker]660      change ψ p = 0 ↔ _661      refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩662      · rw [hψp, IsLocalRing.residue_eq_zero_iff, ← S.parameters] at h663        rw [hmk]664        refine Ideal.add_mem _ (Ideal.mul_mem_left _ _ hI_W) ?_665        have : Ideal.map (chartBase R S.x S.t) (Ideal.span {S.t, S.x}) ≤666            infinityPoint R S.t S.x := by667          rw [Ideal.map_span, Ideal.span_le]668          rintro _ ⟨y, hy, rfl⟩669          rcases hy with rfl | rfl670          · exact hI_t671          · exact hI_x672        exact this (Ideal.mem_map_of_mem _ h)673      · have hle : infinityPoint R S.t S.x ≤674            RingHom.ker (Ideal.Quotient.lift _ ψ fun a ha ↦ hψ ha) := by675          rw [infinityPoint, Ideal.span_le]676          rintro _ (rfl | rfl)677          · change ψ (Polynomial.C S.x) = 0678            simpa [ψ] using hx679          · change ψ Polynomial.X = 0680            simp [ψ]681        exact hle h682  obtain ⟨φ, hφ1, hφ2, hφk⟩ := hker683  have hsurj : Function.Surjective φ := by684    intro y685    obtain ⟨r, rfl⟩ := IsLocalRing.residue_surjective y686    exact ⟨chartBase R S.x S.t r, hφ1 r⟩687  have hmax : (infinityPoint R S.t S.x).IsMaximal := by688    rw [← hφk]; exact RingHom.ker_isMaximal_of_surjective φ hsurj689  refine ⟨hmax, Ideal.subset_span (by simp), Ideal.subset_span (by simp), ?_⟩690  let e0 : (BlowupChart R S.x S.t ⧸ infinityPoint R S.t S.x) ≃+* IsLocalRing.ResidueField R :=691    (Ideal.quotEquivOfEq hφk.symm).trans (RingHom.quotientKerEquivOfSurjective hsurj)692  rw [(AlgEquiv.ofRingEquiv (R := R) (f := e0) fun r ↦ hφ1 r).toLinearEquiv.length_eq,693    length_eq_of_surjective_onto_field R _ _ (IsLocalRing.residue R)694      IsLocalRing.residue_surjective fun r m ↦ rfl]695  simp696 697/-- If `e` is a nonzerodivisor, the kernel of the layer map `a ↦ e^j a` into `A ⧸ (e)^(j+1)` is698`(e)`. -/699private theorem principal_layer_map_kernel (A : Type) [CommRing A] (e : A) (j : ℕ)700    (he : Function.Injective (fun a : A ↦ e*a)) :701    LinearMap.ker (principalLayerMap A e j) = Ideal.span {e} := by702  have hinj : IsLeftRegular (e ^ j) := IsLeftRegular.pow j he703  ext a704  simp only [LinearMap.mem_ker, principalLayerMap, LinearMap.toSpanSingleton_apply,705    Algebra.smul_def, Ideal.Quotient.algebraMap_eq]706  rw [← map_mul, Ideal.Quotient.eq_zero_iff_mem, Ideal.span_singleton_pow,707    Ideal.mem_span_singleton, Ideal.mem_span_singleton]708  constructor709  · rintro ⟨b, hb⟩710    exact ⟨b, hinj (show e ^ j * a = e ^ j * (e * b) by linear_combination hb)⟩711  · rintro ⟨b, rfl⟩712    exact ⟨b, by ring⟩713 714/-- The range of the layer map `a ↦ e^j a` into `A ⧸ (e)^(j+1)` is the kernel of the reduction to `A715⧸ (e)^j`. -/716private theorem principal_layer_map_range (A : Type) [CommRing A] (e : A) (j : ℕ) :717    LinearMap.range (principalLayerMap A e j) = LinearMap.ker718    (principalPowerReduction A e j).toLinearMap := by719  ext x720  constructor721  · rintro ⟨a, rfl⟩722    rw [LinearMap.mem_ker]723    simp only [principalLayerMap, LinearMap.toSpanSingleton_apply, principalPowerReduction,724      AlgHom.toLinearMap_apply, map_smul, Ideal.Quotient.factorₐ_apply, Ideal.Quotient.factor_mk]725    rw [(Ideal.Quotient.eq_zero_iff_mem).2 (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self e) j),726      smul_zero]727  · intro hx728    obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective x729    rw [LinearMap.mem_ker] at hx730    simp only [principalPowerReduction, AlgHom.toLinearMap_apply, Ideal.Quotient.factorₐ_apply,731      Ideal.Quotient.factor_mk] at hx732    rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.span_singleton_pow,733      Ideal.mem_span_singleton'] at hx734    obtain ⟨a, rfl⟩ := hx735    refine ⟨a, ?_⟩736    simp only [principalLayerMap, LinearMap.toSpanSingleton_apply]737    rw [Algebra.smul_def, Ideal.Quotient.algebraMap_eq, ← map_mul]738 739/-- If `e` is a nonzerodivisor, the layer map induces an `A`-linear isomorphism from `A ⧸ (e)` onto740the principal layer `(e)^j ⧸ (e)^(j+1)`. -/741theorem principal_layer_quotient_equiv (A : Type) [CommRing A] (e : A) (j : ℕ)742    (he : Function.Injective (fun a : A ↦ e*a)) :743    ∃ L : (A ⧸ Ideal.span {e}) ≃ₗ[A] PrincipalLayer A e j, ∀ a : A,744    (L (Ideal.Quotient.mk (Ideal.span {e}) a)).val = principalLayerMap A e j a := by745  have hk := principal_layer_map_kernel A e j he746  have hr := principal_layer_map_range A e j747  refine ⟨((Submodule.quotEquivOfEq _ _ hk.symm).trans748    (LinearMap.quotKerEquivRange (principalLayerMap A e j))).trans (LinearEquiv.ofEq _ _ hr), ?_⟩749  intro a750  rfl751 752/-- Each exceptional layer of the chart is `R`-linearly isomorphic to `(R/(t,x))[Z]`, the monomial753`r Z^i` corresponding to the layer class of `r · z^i`. -/754theorem chart_layer_polynomial_coordinates (R : Type) [CommRing R] (t x : R)(4.1)755    (hreg : RegularParameterPair R t x) (j : ℕ) :756    ∃ L : Polynomial (R ⧸ Ideal.span {t,x}) ≃ₗ[R] PrincipalLayer (BlowupChart R t x)757    (chartBase R t x t) j, ∀ r : R, ∀ i : ℕ,758    (L (Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) * Polynomial.X^i)).val =759    principalLayerMap (BlowupChart R t x) (chartBase R t x t) j760    (chartBase R t x r * (chartSlope R t x)^i) := by761  have he := blowup_exceptional_parameter_regular R t x hreg762  obtain ⟨L1, hL1⟩ := principal_layer_quotient_equiv (BlowupChart R t x)763    (chartBase R t x t) j he764  obtain ⟨e1, he1b, he1s⟩ := exceptional_chart_is_affine_line R t x765  have hI : exceptionalLevelIdeal R t x 1 = Ideal.span {chartBase R t x t} := by766    simp [exceptionalLevelIdeal]767  let φ : (BlowupChart R t x ⧸ Ideal.span {chartBase R t x t}) ≃+*768      Polynomial (R ⧸ Ideal.span {t,x}) :=769    (Ideal.quotEquivOfEq hI.symm).trans e1770  have hφ : ∀ a : BlowupChart R t x,771      φ (Ideal.Quotient.mk _ a) = e1 (Ideal.Quotient.mk (exceptionalLevelIdeal R t x 1) a) := by772    intro a; rfl773  have hφb : ∀ r : R, φ (Ideal.Quotient.mk _ (chartBase R t x r)) =774      Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) := by775    intro r; rw [hφ]; exact he1b r776  have hφs : φ (Ideal.Quotient.mk _ (chartSlope R t x)) = Polynomial.X := by777    rw [hφ]; exact he1s778  let φl := (AlgEquiv.ofRingEquiv (R := R) (f := φ) fun r ↦ hφb r).toLinearEquiv779  refine ⟨φl.symm.trans (L1.restrictScalars R), ?_⟩780  intro r i781  have key : φl.symm (Polynomial.C (Ideal.Quotient.mk (Ideal.span {t,x}) r) * Polynomial.X^i)782      = Ideal.Quotient.mk _ (chartBase R t x r * (chartSlope R t x)^i) := by783    rw [LinearEquiv.symm_apply_eq]784    change _ = φ _785    rw [map_mul, map_pow, map_mul, map_pow, hφb, hφs]786  simp only [LinearEquiv.trans_apply, key, LinearEquiv.restrictScalars_apply]787  exact hL1 _788 789open scoped Classical in790open Polynomial UniqueFactorizationMonoid in791/-- Over a finite field `k`, if `ᾱ` is a root of the monic irreducible `φ` in an extension `k'`,792then the multiplicity of `ᾱ` as a root of `G` equals the multiplicity of `φ` among the793normalized factors of `G`. -/794theorem rootMultiplicity_map_eq_count_normalizedFactors (k k' : Type) [Field k] [Finite k]795    [Field k'] (ι : k →+* k') (G : Polynomial k) (hG : G ≠ 0) (φ : Polynomial k)796    (hφ : φ.Monic ∧ Irreducible φ) (alphaBar : k') (hroot : (φ.map ι).eval alphaBar = 0) :797    Polynomial.rootMultiplicity alphaBar (G.map ι) = Multiset.count φ798    (UniqueFactorizationMonoid.normalizedFactors G) := by799  have key : ∀ ψ : k[X], ψ.Monic → Irreducible ψ →800      rootMultiplicity alphaBar (ψ.map ι) = Multiset.count φ {ψ} := by801    intro ψ hm hi802    rw [Multiset.count_singleton]803    split_ifs with h804    · subst h805      have := PerfectField.ofFinite (K := k)806      have hsep : (φ.map ι).Separable := (PerfectField.separable_of_irreducible hi).map807      have hne : φ.map ι ≠ 0 := Polynomial.map_ne_zero hi.ne_zero808      have h1 := rootMultiplicity_le_one_of_separable hsep alphaBar809      have h2 : 0 < rootMultiplicity alphaBar (φ.map ι) :=810        (rootMultiplicity_pos hne).2 hroot811      omega812    · rw [rootMultiplicity_eq_zero_iff]813      intro hr814      exfalso815      obtain ⟨a, b, hab⟩ := (EuclideanDomain.dvd_or_coprime φ ψ hφ.2).resolve_left (by816        intro hd817        exact h (eq_of_monic_of_associated hφ.1 hm (hφ.2.associated_of_dvd hi hd)))818        |>.map (mapRingHom ι)819      have := congrArg (eval alphaBar) hab820      simp only [coe_mapRingHom, eval_add, eval_mul, hroot, hr.eq_zero, mul_zero, add_zero,821        eval_one] at this822      exact zero_ne_one this823  induction G using UniqueFactorizationMonoid.induction_on_prime with824  | h₁ => exact absurd rfl hG825  | h₂ x hx =>826    obtain ⟨c, hc, rfl⟩ := Polynomial.isUnit_iff.1 hx827    rw [normalizedFactors_of_isUnit hx, Polynomial.map_C, rootMultiplicity_C]828    rfl829  | h₃ a p ha hp ih =>830    have ha0 : a ≠ 0 := right_ne_zero_of_mul hG831    have hp0 : p ≠ 0 := hp.ne_zero832    rw [normalizedFactors_mul hp0 ha0, Multiset.count_add, Polynomial.map_mul,833      rootMultiplicity_mul (by simpa using hG), ih ha0,834      normalizedFactors_irreducible hp.irreducible]835    congr 1836    rw [← key _ (Polynomial.monic_normalize hp0)837      ((normalize_associated p).symm.irreducible hp.irreducible), normalize_apply,838      Polynomial.map_mul,839      rootMultiplicity_mul (by simpa [Polynomial.map_ne_zero_iff ι.injective] using hp0),840      coe_normUnit, Polynomial.map_C, rootMultiplicity_C, add_zero]841 842end SurfaceBlowup