Closed points on the blow-up of the concrete surface

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.ExceptionalLayers7import SurfaceBlowup.Surfaces.ChartCompletions8 9/-!10# Closed points on the blow-up of the concrete surface11 12We classify the closed points of the exceptional divisor of the blow-up of the concrete surface13and identify the completed local rings there: at points of the `t`-chart they are concrete14surfaces (over `O` or an unramified extension), and at the point at infinity of the `x`-chart15the strict transform of a curve meets the exceptional divisor transversally.16 17## Main results18 19* `concrete_chart_point_span_form`: classification of closed points of the `t`-chart.20* `concrete_left_point_completion_is_surface`, `concrete_left_point_completion_instances`,21  `concrete_left_point_exceptional_regular`.22* `concrete_infinity_point_completion`, `concrete_infinity_strict_transform_transverse_finite`.23 24Provenance: `concrete_chart_point_span_form`, `concrete_left_point_completion_{is_surface,25instances}`, `concrete_left_point_exceptional_regular`, `concrete_infinity_point_completion`,26`concrete_infinity_strict_transform_transverse_finite`.27-/28 29 30namespace SurfaceBlowup31 32/-! ### Notation33 34Local notations for the charts of the blow-up of `R = ConcreteSurface O pi u a b` at its35closed point, taking the surface data as explicit arguments. -/36 37/-- The `t`-chart `R[x/t]` of the blow-up of the concrete surface `R` at `(t, x)`. -/38local notation:max "tChart" O:max pi:max u:max a:max b:max =>39  BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)40 41/-- The structure map `R → R[x/t]` of the `t`-chart. -/42local notation:max "tBase" O:max pi:max u:max a:max b:max =>43  chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)44 45/-- The slope `x/t` in the `t`-chart. -/46local notation:max "tSlope" O:max pi:max u:max a:max b:max =>47  chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)48 49/-- The `x`-chart `R[t/x]` of the blow-up of the concrete surface `R` at `(t, x)`. -/50local notation:max "xChart" O:max pi:max u:max a:max b:max =>51  BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)52 53/-- The structure map `R → R[t/x]` of the `x`-chart. -/54local notation:max "xBase" O:max pi:max u:max a:max b:max =>55  chartBase (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)56 57/-- The slope `t/x` in the `x`-chart. -/58local notation:max "xSlope" O:max pi:max u:max a:max b:max =>59  chartSlope (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)60 61/-- A closed point `P` of `R[x/t]` on the exceptional divisor, cut out on the exceptional line62by an irreducible `φ`, equals `(t, Φ₀(x/t))` for every lift `Φ₀` of `φ` along `O → R/(t, x)`. -/63private theorem chart_point_eq_span_of_lift (O : Type) [CommRing O] (R : Type) [CommRing R]64    [Algebra O R] (t x : R) [(Ideal.span ({t, x} : Set R)).IsMaximal]65    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial66      (R ⧸ Ideal.span ({t,x} : Set R)))67    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =68      Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r))69    (heZ : e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X)70    (P : Ideal (BlowupChart R t x)) [P.IsMaximal] (hP : chartBase R t x t ∈ P)71    (φ : Polynomial (R ⧸ Ideal.span ({t,x} : Set R))) (hirr : Irreducible φ)72    (hmap : (P.map (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {φ})73    (Φ₀ : Polynomial O)74    (hΦ₀ : Φ₀.map ((Ideal.Quotient.mk (Ideal.span ({t, x} : Set R))).comp (algebraMap O R)) = φ) :75    P = Ideal.span {chartBase R t x t,76      Polynomial.eval₂ ((chartBase R t x).comp (algebraMap O R)) (chartSlope R t x) Φ₀} := by77  set ρ : O →+* R ⧸ Ideal.span ({t, x} : Set R) :=78    (Ideal.Quotient.mk (Ideal.span ({t, x} : Set R))).comp (algebraMap O R) with hρdef79  set F := Polynomial.eval₂ ((chartBase R t x).comp (algebraMap O R)) (chartSlope R t x) Φ₀80  have hF : e (Ideal.Quotient.mk (chartExceptional R t x) F) = φ := by81    rw [← hΦ₀]82    have : ((e : _ →+* _).comp ((Ideal.Quotient.mk (chartExceptional R t x)).comp83        (Polynomial.eval₂RingHom ((chartBase R t x).comp (algebraMap O R)) (chartSlope R t x))))84        = Polynomial.mapRingHom ρ := by85      apply Polynomial.ringHom_ext86      · intro c; simp [he, ρ]87      · simp [heZ]88    exact congrArg (fun g => g Φ₀) this89  have hFP : F ∈ P := by90    have h1 : φ ∈ (P.map (Ideal.Quotient.mk (chartExceptional R t x))).map e := by91      rw [hmap]; exact Ideal.subset_span rfl92    rw [← hF] at h193    rw [Ideal.mem_map_of_equiv] at h194    obtain ⟨y, hy, hye⟩ := h195    rw [e.injective hye] at hy96    rwa [Ideal.mem_quotient_iff_mem] at hy97    rw [chartExceptional, Ideal.span_le]98    simpa using hP99  have hirr' : Irreducible ((Φ₀.map (algebraMap O R)).map100      (Ideal.Quotient.mk (Ideal.span ({t, x} : Set R)))) := by101    rw [Polynomial.map_map, ← hρdef, hΦ₀]; exact hirr102  let _ : Field (BlowupChart R t x ⧸ P) := Ideal.Quotient.field P103  obtain ⟨-, hspan⟩ := chart_nonrational_point_span_eq_comap R t x (Φ₀.map (algebraMap O R)) hirr'104    (BlowupChart R t x ⧸ P) (Ideal.Quotient.mk P)105    (by rw [IsLocalRing.maximalIdeal_eq_bot, Ideal.mem_bot, Ideal.Quotient.eq_zero_iff_mem]106        exact hP)107    (by108      rw [IsLocalRing.maximalIdeal_eq_bot, Ideal.mem_bot, Ideal.Quotient.eq_zero_iff_mem,109        Polynomial.eval₂_map]; exact hFP)110  rw [Polynomial.eval₂_map] at hspan111  rw [hspan, IsLocalRing.maximalIdeal_eq_bot, ← RingHom.ker_eq_comap_bot, Ideal.mk_ker]112 113/-- Classification of the closed points on the exceptional divisor of a chart `R[x/t]` with114residue field that of `O`: the origin, a rational point `x/t = α` with `α` a unit, or a115non-rational point cut out by an unramified lift `Φ` of degree at least `2`. -/116private theorem chart_point_trichotomy (O : Type) [CommRing O] [IsLocalRing O] (R : Type)117    [CommRing R] [Algebra O R] (t x : R) [(Ideal.span ({t, x} : Set R)).IsMaximal]118    (ψ : (R ⧸ Ideal.span ({t, x} : Set R)) ≃+* IsLocalRing.ResidueField O)119    (hψρ : ∀ c : O, ψ (Ideal.Quotient.mk _ (algebraMap O R c)) = IsLocalRing.residue O c)120    (P : Ideal (BlowupChart R t x)) [P.IsMaximal] (hP : chartBase R t x t ∈ P) :121    P = Ideal.span {chartBase R t x t, chartSlope R t x} ∨122    (∃ α : O, IsUnit α ∧ P = Ideal.span123        {chartBase R t x t, chartSlope R t x - chartBase R t x (algebraMap O R α)}) ∨124    (∃ Φ : Polynomial O, IsUnramifiedLift O Φ ∧ 2 ≤ Φ.natDegree ∧ P = Ideal.span {chartBase R t x t,125      Polynomial.eval₂ ((chartBase R t x).comp (algebraMap O R)) (chartSlope R t x) Φ}) := by126  obtain ⟨e, he, heZ⟩ := exceptional_line_equiv_chart_exceptional R t x127  obtain ⟨φ, hmon, hirr, hmap, -, -⟩ :=128    blowup_chart_exceptional_point_polynomial R t x e he heZ P hP129  set ρ : O →+* R ⧸ Ideal.span ({t, x} : Set R) :=130    (Ideal.Quotient.mk (Ideal.span ({t, x} : Set R))).comp (algebraMap O R) with hρdef131  have hρ : ∀ c : O, ρ c = ψ.symm (IsLocalRing.residue O c) := fun c => by132    rw [← hψρ, RingEquiv.symm_apply_apply]; rfl133  have hρsurj : Function.Surjective ρ := by134    intro y135    obtain ⟨c, hc⟩ := IsLocalRing.residue_surjective (ψ y)136    exact ⟨c, by rw [hρ, hc, RingEquiv.symm_apply_apply]⟩137  have key (Φ₀ : Polynomial O) (hΦ₀ : Φ₀.map ρ = φ) :=138    chart_point_eq_span_of_lift O R t x e he heZ P hP φ hirr hmap Φ₀ hΦ₀139  have hdeg : φ.natDegree ≠ 0 := by140    intro h141    rw [hmon.natDegree_eq_zero] at h142    exact hirr.not_isUnit (h ▸ isUnit_one)143  by_cases hX : φ = Polynomial.X144  · left145    simpa using key Polynomial.X (by simp [hX])146  by_cases h1 : φ.natDegree = 1147  · right; left148    have hφ := hmon.eq_X_add_C h1149    set c := φ.coeff 0150    have hc : c ≠ 0 := fun hc => hX (by rw [hφ, hc]; simp)151    obtain ⟨α, hα⟩ := hρsurj (-c)152    refine ⟨α, ?_, ?_⟩153    · by_contra hu154      have : IsLocalRing.residue O α = 0 := (IsLocalRing.residue_eq_zero_iff α).2155        ((IsLocalRing.mem_maximalIdeal α).2 hu)156      apply hc157      rw [← neg_eq_zero, ← hα, hρ, this, map_zero]158    · have := key (Polynomial.X - Polynomial.C α) (by rw [hφ]; simp [hα, sub_eq_add_neg])159      simpa using this160  · right; right161    obtain ⟨Φ₀, hmapΦ, hdegΦ, hmonΦ⟩ :=162      Polynomial.lifts_and_natDegree_eq_and_monic (Polynomial.mem_lifts_of_surjective hρsurj φ) hmon163    refine ⟨Φ₀, ⟨hmonΦ, ?_⟩, by omega, key Φ₀ hmapΦ⟩164    have hres : residuePoly O Φ₀ = (Polynomial.mapEquiv ψ) φ := by165      rw [← hmapΦ]166      simp only [residuePoly, Polynomial.mapEquiv_apply, Polynomial.map_map]167      congr 1168      ext c169      simp [hρ]170    rw [hres]171    exact (MulEquiv.irreducible_iff (Polynomial.mapEquiv ψ).toMulEquiv).2 hirr172 173/-- The closed points of the `t`-chart of the concrete surface lying over the closed point are the174origin, rational points `(t, x/t - α)` with `α` a unit, and non-rational points `(t, Φ(x/t))`. -/175theorem concrete_chart_point_span_form (O : Type) [CommRing O] [IsDomain O]176    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]177    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)178    (a b : ℕ) (ha : 0 < a) (P : Ideal (tChart O pi u a b)) [P.IsMaximal]179    (hP : tBase O pi u a b (surfaceT O pi u a b) ∈ P) :180    P = Ideal.span {tBase O pi u a b (surfaceT O pi u a b), tSlope O pi u a b} ∨181      (∃ α : O, IsUnit α ∧ P = Ideal.span {tBase O pi u a b (surfaceT O pi u a b),182        tSlope O pi u a b - tBase O pi u a b (algebraMap O (ConcreteSurface O pi u a b) α)}) ∨183      (∃ Φ : Polynomial O, IsUnramifiedLift O Φ ∧ 2 ≤ Φ.natDegree ∧184        P = Ideal.span {tBase O pi u a b (surfaceT O pi u a b),185          Polynomial.eval₂ ((tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b)))186            (tSlope O pi u a b) Φ}) := by187  obtain ⟨ψ, hψ⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha188  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} :189      Set (ConcreteSurface O pi u a b))).IsMaximal :=190    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha191  exact chart_point_trichotomy O (ConcreteSurface O pi u a b) _ _ ψ192    (fun c ↦ hψ (MvPowerSeries.C c)) P hP193 194/-- The completion of the `t`-chart at any closed point over the closed point of the concrete195surface is again a concrete surface over a complete discrete valuation ring, with `t ↦ t'`. -/196theorem concrete_left_point_completion_is_surface (O : Type) [CommRing O] [IsDomain O]197    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]198    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)199    (a b : ℕ) (ha : 0 < a) (P : Ideal (tChart O pi u a b)) [P.IsMaximal] [P.IsPrime]200    (hP : tBase O pi u a b (surfaceT O pi u a b) ∈ P) :201    ∃ (O' : Type) (_ : CommRing O') (_ : IsDomain O') (_ : IsDiscreteValuationRing O')202      (_ : IsAdicComplete (IsLocalRing.maximalIdeal O') O')203      (_ : Finite (IsLocalRing.ResidueField O')) (pi' : O') (u' : (TwoSeries O')ˣ) (a' b' : ℕ),204      Irreducible pi' ∧ 0 < a' ∧205      ∃ Eq : CompletedLocalAt (tChart O pi u a b) P ≃+* ConcreteSurface O' pi' u' a' b',206      Eq (completedPointMap (tChart O pi u a b) P (tBase O pi u a b (surfaceT O pi u a b))) =207          surfaceT O' pi' u' a' b' := by208  have hT : ∀ (R : Type) [CommRing R] (α : R), chartSubst R α (axisT R) = axisT R :=209    fun R _ α => (chartSubst_apply_generators R α).2.1210  rcases concrete_chart_point_span_form O pi hpi u a b ha P hP with h | ⟨α, hα, h⟩ | ⟨Φ, hΦ, h2, h⟩211  · obtain ⟨E, hE, -⟩ := t_chart_origin_completion_equiv O pi hpi u a b ha P h212    refine ⟨O, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance, pi,213          substUnit O 0 u, a + b, b, hpi, by omega, E, (hE _).trans (congrArg _ (hT O 0))⟩214  · obtain ⟨E, hE, -⟩ := t_chart_unit_point_completion_equiv O pi hpi u a b ha α hα P h215    refine ⟨O, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance, pi, _,216          a + b, 0, hpi, by omega, E, (hE _).trans (congrArg _ (hT O α))⟩217  · have hθ := unramified_root_isUnit_of_two_le_natDegree O Φ hΦ h2218    obtain ⟨E, hE, -⟩ := t_chart_nonrational_point_completion_equiv O pi hpi u a b ha Φ hΦ hθ P h219    obtain ⟨hd, hl, hdvr, -, hirr, hc, hf, -⟩ := unramified_is_dvr O Φ hΦ220    refine ⟨AdjoinRoot Φ, inferInstance, hd, hdvr, hc, hf, algebraMap O (AdjoinRoot Φ) pi, _, a + b,221          0, hirr pi hpi, by omega, E, ?_⟩222    have hm : MvPowerSeries.map (algebraMap O (AdjoinRoot Φ)) (axisT O) = axisT (AdjoinRoot Φ) := by223      simp [axisT, MvPowerSeries.map_X]224    exact (hE _).trans (congrArg _ (by rw [hm, hT]))225 226/-- The completion of the `t`-chart at a closed point over the closed point of the concrete227surface is a noetherian complete local domain. -/228theorem concrete_left_point_completion_instances (O : Type) [CommRing O] [IsDomain O]229    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]230    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)231    (a b : ℕ) (ha : 0 < a) (P : Ideal (tChart O pi u a b)) [P.IsMaximal] [P.IsPrime]232    (hP : tBase O pi u a b (surfaceT O pi u a b) ∈ P) :233    IsNoetherianRing (CompletedLocalAt (tChart O pi u a b) P) ∧234      IsDomain (CompletedLocalAt (tChart O pi u a b) P) ∧235      ∃ _ : IsLocalRing (CompletedLocalAt (tChart O pi u a b) P),236      IsAdicComplete (IsLocalRing.maximalIdeal (CompletedLocalAt (tChart O pi u a b) P))237      (CompletedLocalAt (tChart O pi u a b) P) := by238  obtain ⟨O', c1, c2, c3, c4, c5, pi', u', a', b', hpi', ha', Eq, -⟩ :=239    concrete_left_point_completion_is_surface O pi hpi u a b ha P hP240  exact concrete_surface_equiv_instances _ O' pi' hpi' u' a' b' ha' Eq241 242/-- The exceptional equation `t` is a non-zero-divisor in the completion of the `t`-chart at any243closed point over the closed point. -/244theorem concrete_left_point_exceptional_regular (O : Type) [CommRing O] [IsDomain O]245    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]246    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)247    (a b : ℕ) (ha : 0 < a) (P : Ideal (tChart O pi u a b)) [P.IsMaximal] [P.IsPrime]248    (hP : tBase O pi u a b (surfaceT O pi u a b) ∈ P) :249    Function.Injective250      (fun y : CompletedLocalAt (tChart O pi u a b) P => completedPointMap (tChart O pi u a b) P251        (tBase O pi u a b (surfaceT O pi u a b)) * y) := by252  obtain ⟨O', c1, c2, c3, c4, c5, pi', u', a', b', hpi', ha', Eq, hEq⟩ :=253    concrete_left_point_completion_is_surface O pi hpi u a b ha P hP254  have e : Eq.symm (surfaceT O' pi' u' a' b') = completedPointMap _ P255      (tBase O pi u a b (surfaceT O pi u a b)) := by256    rw [← hEq]; simp257  exact e ▸ (concrete_surface_equiv_regular_pair _ O' pi' hpi' u' a' b' ha' Eq).2.2258 259/-- The point at infinity `(x, t/x)` of the `x`-chart: its completion is a concrete surface, a260noetherian complete local ring in which `x` is a non-zero-divisor. -/261theorem concrete_infinity_point_completion (O : Type) [CommRing O] [IsDomain O]262    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]263    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)264    (a b : ℕ) (ha : 0 < a) (P : Ideal (xChart O pi u a b)) [P.IsMaximal] [P.IsPrime]265    (hx : xBase O pi u a b (surfaceX O pi u a b) ∈ P) (hW : xSlope O pi u a b ∈ P) :266    P = Ideal.span {xBase O pi u a b (surfaceX O pi u a b), xSlope O pi u a b} ∧267      (∃ Eq : CompletedLocalAt (xChart O pi u a b) P ≃+*268          ConcreteSurface O pi (xSubstUnit O u) (a + b) a,269        Eq (completedPointMap (xChart O pi u a b) P (xBase O pi u a b (surfaceX O pi u a b))) =270          surfaceT O pi (xSubstUnit O u) (a + b) a) ∧271      IsNoetherianRing (CompletedLocalAt (xChart O pi u a b) P) ∧272      (∃ _ : IsLocalRing (CompletedLocalAt (xChart O pi u a b) P),273        IsAdicComplete (IsLocalRing.maximalIdeal (CompletedLocalAt (xChart O pi u a b) P))274        (CompletedLocalAt (xChart O pi u a b) P)) ∧ Function.Injective275      (fun y : CompletedLocalAt (xChart O pi u a b) P => completedPointMap (xChart O pi u a b) P276        (xBase O pi u a b (surfaceX O pi u a b)) * y) := by277  obtain ⟨hd, hr, D, hpi', ht, hx', h5, h6, h7⟩ :=278      concrete_surface_data_exists_unconditional O pi hpi u a b ha279  have hmax := (infinity_point_maximal O (ConcreteSurface O pi u a b) D).1280  rw [ht, hx'] at hmax281  have hPeq : P = Ideal.span {xBase O pi u a b (surfaceX O pi u a b), xSlope O pi u a b} := by282    symm283    apply Ideal.IsMaximal.eq_of_le hmax (Ideal.IsPrime.ne_top inferInstance)284    unfold infinityPoint285    rw [Ideal.span_le]286    rintro z (rfl | rfl)287    exacts [hx, hW]288  obtain ⟨E, hE, hEs, hEc⟩ := x_chart_infinity_completion_equiv O pi hpi u a b ha P hPeq289  have hT : E (completedPointMap (xChart O pi u a b) P (xBase O pi u a b (surfaceX O pi u a b))) =290      surfaceT O pi (xSubstUnit O u) (a + b) a :=291    (hE _).trans (congrArg _ (chartSubst_apply_generators O 0).2.2.2.2.2.1)292  have hinst := concrete_surface_equiv_instances _ O pi hpi (xSubstUnit O u) (a+b) a (by omega) E293  refine ⟨hPeq, ⟨E, hT⟩, hinst.1, hinst.2.2, ?_⟩294  have hreg :=295      (concrete_surface_equiv_regular_pair _ O pi hpi (xSubstUnit O u) (a+b) a (by omega) E).2.2296  have : completedPointMap (xChart O pi u a b) P (xBase O pi u a b (surfaceX O pi u a b)) =297      E.symm (surfaceT O pi (xSubstUnit O u) (a + b) a) := by298    rw [← hT]; simp299  rw [this]; exact hreg300 301/-- `residueKillT` kills the `x`-chart substitution down to the residue of the constant term. -/302theorem residueKillT_xChartSubst (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]303    (pi : O) (hpi : Irreducible pi) (s : TwoSeries O) :304    residueKillT O (xChartSubst O s) = PowerSeries.C305      (IsLocalRing.residue O (MvPowerSeries.constantCoeff s)) := by306  obtain ⟨-, -, -, hC, hT, hX, -⟩ := chartSubst_apply_generators O 0307  obtain ⟨kC, kT, kX, -, -⟩ := residueKillT_apply_ker O pi hpi308  let L : TwoSeries O →+* PowerSeries (IsLocalRing.ResidueField O) :=309    (residueKillT O).comp (xChartSubst O : TwoSeries O →+* TwoSeries O)310  let R : TwoSeries O →+* PowerSeries (IsLocalRing.ResidueField O) :=311    (PowerSeries.C).comp ((IsLocalRing.residue O).comp MvPowerSeries.constantCoeff)312  have LT : L (axisT O) = 0 := by313    change residueKillT O (xChartSubst O (axisT O)) = 0314    rw [hT, map_mul, kT, zero_mul]315  have LX : L (axisX O) = 0 := by316    change residueKillT O (xChartSubst O (axisX O)) = 0317    rw [hX, kT]318  have RT : R (axisT O) = 0 := by simp [R, axisT]319  have RX : R (axisX O) = 0 := by simp [R, axisX]320  have h : L = R := by321    apply twoSeries_ringHom_ext_of_isNilpotent O _ L R322    · intro c323      change residueKillT O (xChartSubst O (MvPowerSeries.C c)) = _324      simp [R, hC, kC]325    · rw [LT, RT]326    · rw [LX, RX]327    · exact LT ▸ IsNilpotent.zero328    · exact LX ▸ IsNilpotent.zero329  exact congrArg (fun f => f s) h330 331/-- A power series `∑ rᵢ X^(d - i)` with some `rᵢ ≠ 0` is nonzero. -/332private theorem sum_C_mul_X_pow_ne_zero {K : Type} [Field K] (d : ℕ) (r : Fin (d + 1) → K)333    (hne : ∃ i, r i ≠ 0) :334    (∑ i : Fin (d+1), PowerSeries.C (r i) * PowerSeries.X ^ (d - i.val) : PowerSeries K) ≠ 0 := by335  obtain ⟨i, hi⟩ := hne336  intro h337  apply hi338  have := congrArg (PowerSeries.coeff (d - i.val)) h339  rw [map_zero, map_sum, Finset.sum_eq_single i] at this340  · rwa [PowerSeries.coeff_C_mul_X_pow, if_pos rfl] at this341  · intro j _ hj342    rw [PowerSeries.coeff_C_mul_X_pow, if_neg]343    intro h'; apply hj; ext; have := j.isLt; have := i.isLt; omega344  · simp345 346/-- At the point at infinity of the `x`-chart, the strict transform `∑ cᵢ (t/x)^(d-i)` of a curve347`f = ∑ cᵢ t^(d-i) x^i` (some `cᵢ` a unit) and the exceptional equation `x` form a transverse pair,348and they cut out a finite-length quotient. -/349theorem concrete_infinity_strict_transform_transverse_finite (O : Type) [CommRing O] [IsDomain O]350    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]351    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)352    (a b : ℕ) (ha : 0 < a) (d : ℕ)353    (c : Fin (d + 1) → ConcreteSurface O pi u a b)354    (hne : ∃ i : Fin (d + 1), c i ∉ Ideal.span {(surfaceT O pi u a b), (surfaceX O pi u a b)})355    (P : Ideal (xChart O pi u a b)) [P.IsMaximal] [P.IsPrime]356    (hx : xBase O pi u a b (surfaceX O pi u a b) ∈ P) (hW : xSlope O pi u a b ∈ P) :357    Function.Injective358      (fun w : CompletedLocalAt (xChart O pi u a b) P ⧸ Ideal.span359          {completedPointMap (xChart O pi u a b) P (∑ i : Fin (d+1),360            algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *361              xSlope O pi u a b ^ (d - i.val))} =>362        Ideal.Quotient.mk (Ideal.span {completedPointMap (xChart O pi u a b) P (∑ i : Fin (d+1),363            algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *364              xSlope O pi u a b ^ (d - i.val))})365          (completedPointMap (xChart O pi u a b) P (xBase O pi u a b (surfaceX O pi u a b))) * w) ∧366    Function.Injective367      (fun w : CompletedLocalAt (xChart O pi u a b) P ⧸ Ideal.span368          {completedPointMap (xChart O pi u a b) P (xBase O pi u a b (surfaceX O pi u a b))} =>369        Ideal.Quotient.mk (Ideal.span370            {completedPointMap (xChart O pi u a b) P (xBase O pi u a b (surfaceX O pi u a b))})371          (completedPointMap (xChart O pi u a b) P (∑ i : Fin (d+1),372            algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *373              xSlope O pi u a b ^ (d - i.val))) * w) ∧374    ∃ L : ℕ, ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map375        (localCompletionMap (Localization.AtPrime P)))^L ≤376      finiteLocalCurveIdeal (xChart O pi u a b) P (xBase O pi u a b (surfaceX O pi u a b))377        (completedPointMap (xChart O pi u a b) P (∑ i : Fin (d+1),378          algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *379            xSlope O pi u a b ^ (d - i.val))) 1 := by380  have : IsLocalRing (ConcreteSurface O pi u a b) :=381    concrete_surface_isLocalRing O pi u a b hpi.not_isUnit ha382  obtain ⟨hP, -, hN, ⟨hLoc, -⟩, hreg⟩ :=383      concrete_infinity_point_completion O pi hpi u a b ha P hx hW384  obtain ⟨Eq, hb, hs, -⟩ := x_chart_infinity_completion_equiv O pi hpi u a b ha P hP385  obtain ⟨q, hq⟩ := concrete_surface_quotient_T_equiv O pi hpi (xSubstUnit O u) (a + b) a (by omega)386  obtain ⟨e0, he0⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha387  have h461 := concrete_surface_maximalIdeal_eq O pi hpi u a b ha388  let κ : IsLocalRing.ResidueField (ConcreteSurface O pi u a b) ≃+* IsLocalRing.ResidueField O :=389    (Ideal.quotEquivOfEq h461).trans e0390  have hκ : ∀ s : TwoSeries O,391      κ (IsLocalRing.residue (ConcreteSurface O pi u a b) (surfaceMk O pi u a b s)) =392      IsLocalRing.residue O (MvPowerSeries.constantCoeff s) := fun s => by393    change e0 (Ideal.quotEquivOfEq h461 (Ideal.Quotient.mk _ (surfaceMk O pi u a b s))) = _394    rw [Ideal.quotEquivOfEq_mk]395    exact he0 s396  have hxT : Eq (completedPointMap _ P (xBase O pi u a b (surfaceX O pi u a b))) =397      surfaceT O pi (xSubstUnit O u) (a + b) a := by398    have h := hb (axisX O)399    rwa [(chartSubst_apply_generators O 0).2.2.2.2.2.1] at h400  let Ψ : xChart O pi u a b →+* PowerSeries (IsLocalRing.ResidueField O) :=401    q.toRingHom.comp ((Ideal.Quotient.mk _).comp (Eq.toRingHom.comp (completedPointMap _ P)))402  have hΨc : ∀ r, Ψ (algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) r) =403      PowerSeries.C (κ (IsLocalRing.residue _ r)) := fun r => by404    obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective r405    change q (Ideal.Quotient.mk _ (Eq (completedPointMap _ P (xBase O pi u a b406        (surfaceMk O pi u a b s))))) = _407    rw [hb, hq, residueKillT_xChartSubst O pi hpi]; exact congrArg _ (hκ s).symm408  have hΨW : Ψ (xSlope O pi u a b) = PowerSeries.X := by409    change q (Ideal.Quotient.mk _ (Eq (completedPointMap _ P _))) = _410    rw [hs, show surfaceX O pi (xSubstUnit O u) (a + b) a = surfaceMk _ _ _ _ _ (axisX O) from rfl,411      hq, (residueKillT_apply_ker O pi hpi).2.2.1]412  set S := CompletedLocalAt (xChart O pi u a b) P413  set e := completedPointMap (xChart O pi u a b) P (xBase O pi u a b (surfaceX O pi u a b))414  set g := completedPointMap (xChart O pi u a b) P415      (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *416          xSlope O pi u a b ^ (d - i.val))417  have hmap : Ideal.map Eq (Ideal.span {e}) = Ideal.span418      {surfaceT O pi (xSubstUnit O u) (a + b) a} := by419    rw [Ideal.map_span, Set.image_singleton, hxT]420  let e1 : (S ⧸ Ideal.span {e}) ≃+*421      (ConcreteSurface O pi (xSubstUnit O u) (a + b) a ⧸ Ideal.span422        {surfaceT O pi (xSubstUnit O u) (a + b) a}) :=423    Ideal.quotientEquiv (Ideal.span {e})424        (Ideal.span {surfaceT O pi (xSubstUnit O u) (a + b) a}) Eq hmap.symm425  obtain ⟨k1, k2, L, hL'⟩ := transverse_of_reduction_ne_zero S e g hreg426    (IsLocalRing.ResidueField O) (e1.trans q) (by427      change Ψ (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *428        xSlope O pi u a b ^ (d - i.val)) ≠ 0429      simp only [map_sum, map_mul, map_pow, hΨc, hΨW]430      obtain ⟨i, hi⟩ := hne431      refine sum_C_mul_X_pow_ne_zero d _ ⟨i, ?_⟩432      rwa [Ne, map_eq_zero_iff κ κ.injective, IsLocalRing.residue_eq_zero_iff, h461])433  refine ⟨k1, k2, L, ?_⟩434  unfold finiteLocalCurveIdeal435  rw [pow_one]436  convert hL' using 2437  all_goals exact (AdicCompletion.maximalIdeal_eq_map (R := Localization.AtPrime P)).symm438 439end SurfaceBlowup