Completions of the blow-up charts 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.CurveOrders7import SurfaceBlowup.Surfaces.Regularity8 9/-!10# Completions of the blow-up charts of the concrete surface11 12Let `R = O[[T,X]]/(π - u T^a X^b)` be the concrete surface and `R[x/t]`, `R[t/x]` the two charts13of its blow-up at the closed point. We show that the completed local rings of these charts at14the closed points of the exceptional divisor are again concrete surfaces (over `O` at rational15points, over the unramified extension `O[θ]` at non-rational points).16 17## Main results18 19* `chart_child_completion_equiv`: the general completion isomorphism for a chart map.20* `t_chart_nonrational_point_completion_equiv`, `t_chart_origin_completion_equiv`,21  `t_chart_unit_point_completion_equiv`, `x_chart_infinity_completion_equiv`.22* `concrete_residue_ideal_chart_exists`: lifting curves of the special fiber.23 24Provenance: `chart_child_{completion_equiv, map_exists}`, `concrete_residue_ideal_chart_exists`,25`chart_point_quotient_adjoinRoot_equiv`, `chart_{nonrational,rational}_point_span_eq_comap`,26`nonrational_point_{derivative_isUnit_mod, hensel_root}`,27`t_chart_{nonrational_point, origin, unit_point}_completion_equiv`,28`x_chart_infinity_completion_equiv`.29-/30 31 32namespace SurfaceBlowup33 34/-! ### Notation35 36Local notations for the charts of the blow-up of `R = ConcreteSurface O pi u a b` at its37closed point, taking the surface data as explicit arguments. -/38 39/-- The `t`-chart `R[x/t]` of the blow-up of the concrete surface `R` at `(t, x)`. -/40local notation:max "tChart" O:max pi:max u:max a:max b:max =>41  BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)42 43/-- The structure map `R → R[x/t]` of the `t`-chart. -/44local notation:max "tBase" O:max pi:max u:max a:max b:max =>45  chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)46 47/-- The slope `x/t` in the `t`-chart. -/48local notation:max "tSlope" O:max pi:max u:max a:max b:max =>49  chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)50 51/-- The `x`-chart `R[t/x]` of the blow-up of the concrete surface `R` at `(t, x)`. -/52local notation:max "xChart" O:max pi:max u:max a:max b:max =>53  BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)54 55/-- The structure map `R → R[t/x]` of the `x`-chart. -/56local notation:max "xBase" O:max pi:max u:max a:max b:max =>57  chartBase (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)58 59/-- The slope `t/x` in the `x`-chart. -/60local notation:max "xSlope" O:max pi:max u:max a:max b:max =>61  chartSlope (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)62 63/-- The chart `R[f/e]` of the concrete surface `R`, where `e, f` are the images of `E, F`. -/64local notation:max "efChart" O:max pi:max u:max a:max b:max E:max F:max =>65  BlowupChart (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F)66 67/-- The structure map `R → R[f/e]`. -/68local notation:max "efBase" O:max pi:max u:max a:max b:max E:max F:max =>69  chartBase (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F)70 71/-- The slope `f/e` in the chart `R[f/e]`. -/72local notation:max "efSlope" O:max pi:max u:max a:max b:max E:max F:max =>73  chartSlope (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F)74 75/-- The child surface over `O[θ] = O[X]/(Φ)` at a non-rational point of the exceptional divisor. -/76local notation:max "childSurface" O:max pi:max u:max a:max b:max Φ:max hθ:max =>77  ConcreteSurface (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)78      (substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)79        (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) * shiftUnit (AdjoinRoot Φ)80        (AdjoinRoot.root Φ) hθ ^ b) (a + b) 081 82/-- The unit of the child surface over `O[θ] = O[X]/(Φ)` at a non-rational point. -/83local notation:max "childUnit" O:max u:max b:max Φ:max hθ:max =>84  substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)85      (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) * shiftUnit (AdjoinRoot Φ)86      (AdjoinRoot.root Φ) hθ ^ b87 88/-! ### Completions of charts at closed points -/89 90/-- An endomorphism of the completed local ring of a noetherian ring `A` at a maximal ideal `P`91that fixes the image of `A` and preserves the maximal ideal is the identity. -/92private theorem completedLocalAt_ringHom_eq_id (A : Type) [CommRing A] [IsNoetherianRing A]93    (P : Ideal A) [P.IsMaximal] (φ : CompletedLocalAt A P →+* CompletedLocalAt A P)94    (hφ : φ.comp (completedPointMap A P) = completedPointMap A P)95    (hle : IsLocalRing.maximalIdeal (CompletedLocalAt A P) ≤96      (IsLocalRing.maximalIdeal (CompletedLocalAt A P)).comap φ) :97    φ = RingHom.id _ := by98  have : IsNoetherianRing (Localization.AtPrime P) :=99    IsLocalization.isNoetherianRing P.primeCompl _ inferInstance100  set M := IsLocalRing.maximalIdeal (CompletedLocalAt A P)101  have hmhat : M = (IsLocalRing.maximalIdeal (Localization.AtPrime P)).map102      (localCompletionMap (Localization.AtPrime P)) := AdicCompletion.maximalIdeal_eq_map103  refine RingHom.ext <| congrFun <| IsHausdorff.funext' M (f := fun y => φ y)104    (g := fun y => y) fun n y => ?_105  obtain ⟨x, hx⟩ := finite_completed_point_quotient_surjective A P n (M ^ n) (by rw [hmhat])106    (Ideal.Quotient.mk _ y)107  rw [RingHom.comp_apply] at hx108  have h : φ (completedPointMap A P x - y) ∈ M ^ n :=109    (Ideal.pow_right_mono hle n).trans (Ideal.le_comap_pow φ n) (Ideal.Quotient.eq.mp hx)110  rw [map_sub, ← RingHom.comp_apply φ, hφ] at h111  exact (Ideal.Quotient.eq.mpr h).symm.trans hx112 113/-- Let `Λ : R[f/e] → R'` be a chart map to a concrete surface `R'` over `O'`, compatible with a114substitution `s : O[[T,X]] → O'[[T,X]]` (`E ↦ T`, `F ↦ T (X + α)`), and surjective modulo the115parameter ideal. Then the completion of `R[f/e]` at `P = Λ⁻¹(t', x')` is isomorphic to `R'`. -/116theorem chart_child_completion_equiv (O O' : Type) [CommRing O] [IsNoetherianRing O] [CommRing O']117    [IsDomain O'] [IsDiscreteValuationRing O'] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) (pi' : O')118    (hpi' : Irreducible pi') (u' : (TwoSeries O')ˣ) (a' b' : ℕ) (ha' : 0 < a') (E F : TwoSeries O)119    (hEF : (E = axisT O ∧ F = axisX O) ∨ (E = axisX O ∧ F = axisT O)) (ρ : O →+* O') (α : O')120    (s : TwoSeries O →+* TwoSeries O')121    (hsC : ∀ c : O, s (MvPowerSeries.C c) = MvPowerSeries.C (ρ c)) (hsE : s E = axisT O')122    (hsF : s F = axisT O' * (axisX O' + MvPowerSeries.C α))123    (hs : s (surfaceRelation O pi u a b) = surfaceRelation O' pi' u' a' b')124    (Λ : efChart O pi u a b E F →+* ConcreteSurface O' pi' u' a' b')125    (hΛ : ∀ g : TwoSeries O, Λ (efBase O pi u a b E F (surfaceMk O pi u a b g)) =126        surfaceMk O' pi' u' a' b' (s g))127    (hΛZ : Λ (efSlope O pi u a b E F) = surfaceX O' pi' u' a' b' + algebraMap O'128        (ConcreteSurface O' pi' u' a' b') α)129    (P : Ideal (efChart O pi u a b E F)) [P.IsPrime] (hP : ∀ x, x ∈ P ↔ Λ x ∈ surfaceParameterIdeal130        O' pi' u' a' b')131    (hsurj : ∀ y : ConcreteSurface O' pi' u' a' b', ∃ x : efChart O pi u a b E F,132      Λ x - y ∈ surfaceParameterIdeal O' pi' u' a' b')133    (Λ' : CompletedLocalAt (efChart O pi u a b E F) P →+* ConcreteSurface O' pi' u' a' b')134    (hΛ' : ∀ x, Λ' (completedPointMap (efChart O pi u a b E F) P x) = Λ x)135        (κ : O' →+* CompletedLocalAt (efChart O pi u a b E F) P)136    (hκ : ∀ c : O', Λ' (κ c) = algebraMap O' (ConcreteSurface O' pi' u' a' b') c)137    (hκρ : ∀ c : O,138      κ (ρ c) = completedPointMap (efChart O pi u a b E F) P139      (efBase O pi u a b E F (algebraMap O (ConcreteSurface O pi u a b) c))) :140    ∃ Eq : CompletedLocalAt (efChart O pi u a b E F) P ≃+* ConcreteSurface O' pi' u' a' b',141      (∀ y, Eq y = Λ' y) ∧ ∀ c : O',142      Eq.symm (algebraMap O' (ConcreteSurface O' pi' u' a' b') c) = κ c := by143  have : IsNoetherianRing (efChart O pi u a b E F) :=144    blowupChart_concrete_isNoetherianRing O pi u a b _ _145  have : IsNoetherianRing (Localization.AtPrime P) :=146    IsLocalization.isNoetherianRing P.primeCompl _ inferInstance147  have : IsLocalRing (ConcreteSurface O' pi' u' a' b') :=148    concrete_surface_isLocalRing O' pi' u' a' b' hpi'.not_isUnit ha'149  have hm := concrete_surface_maximalIdeal_eq O' pi' hpi' u' a' b' ha'150  have := concrete_surface_isAdicComplete_maximalIdeal O' pi' hpi' u' a' b' ha'151  set M := IsLocalRing.maximalIdeal (CompletedLocalAt (efChart O pi u a b E F) P) with hM152  have hmhat : M = (IsLocalRing.maximalIdeal (Localization.AtPrime P)).map153      (localCompletionMap (Localization.AtPrime P)) := AdicCompletion.maximalIdeal_eq_map154  have hmem : ∀ y, y ∈ M ↔ Λ' y ∈ surfaceParameterIdeal O' pi' u' a' b' := by155    rw [hmhat]; exact chart_child_completion_map_local _ O' pi' hpi' u' a' b' ha' Λ P hP Λ' hΛ'156  have hTmem : surfaceT O' pi' u' a' b' ∈ surfaceParameterIdeal O' pi' u' a' b' :=157    Ideal.subset_span (by simp)158  have hXmem : surfaceX O' pi' u' a' b' ∈ surfaceParameterIdeal O' pi' u' a' b' :=159    Ideal.subset_span (by simp)160  -- The images `e` of `E` and `z = f/e - α` in the completion lie in its maximal ideal `M`.161  set e := completedPointMap _ P (efBase O pi u a b E F (surfaceMk O pi u a b E)) with he_def162  set z := completedPointMap _ P (efSlope O pi u a b E F) - κ α with hz_def163  have hΛE : Λ (efBase O pi u a b E F (surfaceMk O pi u a b E)) = surfaceT O' pi' u' a' b' := by164    rw [hΛ, hsE]; rfl165  have hΛ'e : Λ' e = surfaceT O' pi' u' a' b' := by rw [hΛ', hΛE]166  have hΛ'z : Λ' z = surfaceX O' pi' u' a' b' := by rw [map_sub, hΛ', hΛZ, hκ]; ring167  have he : e ∈ M := by rw [hmem, hΛ'e]; exact hTmem168  have hz : z ∈ M := by rw [hmem, hΛ'z]; exact hXmem169  -- Evaluating `T ↦ e`, `X ↦ z` gives an inverse candidate `Θ : R' → completion`.170  obtain ⟨Θt, hΘC, hΘT, hΘX⟩ := twoSeries_eval_exists_of_isAdicComplete _ M O' κ _ _ he hz171  have hcomp : ∀ g,172      Θt (s g) = completedPointMap _ P (efBase O pi u a b E F (surfaceMk O pi u a b g)) :=173    congrFun <| congrArg DFunLike.coe <| child_series_eval_comp_chart_subst O O' pi u a b E F hEF174      P (by rw [hP, hΛE]; exact hTmem)175      (by rw [hP, hΛ, hsF, map_mul]; exact Ideal.mul_mem_right _ _ hTmem) ρ α s hsC hsE hsF κ hκρ176      Θt hΘC hΘT hΘX177  have hrel : Θt (surfaceRelation O' pi' u' a' b') = 0 := by178    have : surfaceMk O pi u a b (surfaceRelation O pi u a b) = 0 :=179      Ideal.Quotient.eq_zero_iff_mem.2 (Ideal.mem_span_singleton_self _)180    rw [← hs, hcomp, this, map_zero, map_zero]181  let Θ : ConcreteSurface O' pi' u' a' b' →+* CompletedLocalAt (efChart O pi u a b E F) P :=182    Ideal.Quotient.lift (surfaceIdeal O' pi' u' a' b') Θt fun r hr => by183      obtain ⟨q, rfl⟩ := Ideal.mem_span_singleton'.1 hr184      rw [map_mul, hrel, mul_zero]185  have hΘmk : ∀ g, Θ (surfaceMk O' pi' u' a' b' g) = Θt g := fun g => Ideal.Quotient.lift_mk _ _ _186  have hΘalg : ∀ c : O', Θ (algebraMap O' (ConcreteSurface O' pi' u' a' b') c) = κ c :=187    fun c => (hΘmk _).trans (hΘC c)188  have hΘT' : Θ (surfaceT O' pi' u' a' b') = e := (hΘmk _).trans hΘT189  have hΘX' : Θ (surfaceX O' pi' u' a' b') = z := (hΘmk _).trans hΘX190  -- `Λ' ∘ Θ = id`, checked modulo each power of the maximal ideal of `R'`.191  have h5 : Λ'.comp Θ = RingHom.id _ := by192    refine RingHom.ext <| congrFun <| IsHausdorff.funext' (IsLocalRing.maximalIdeal _)193      (f := fun r => Λ' (Θ r)) (g := fun r => r) fun n r => ?_194    let Q := IsLocalRing.maximalIdeal (ConcreteSurface O' pi' u' a' b') ^ n195    refine DFunLike.congr_fun (concrete_surface_ringHom_ext_of_isNilpotent O'196      (ConcreteSurface O' pi' u' a' b' ⧸ Q) pi' u' a' b' ((Ideal.Quotient.mk Q).comp (Λ'.comp Θ))197      (Ideal.Quotient.mk Q) ?_ ?_ ?_ ?_ ?_) r198    all_goals simp only [RingHom.comp_apply, hΘalg, hκ, hΘT', hΘX', hΛ'e, hΛ'z, implies_true]199    all_goals refine ⟨n, ?_⟩200    all_goals rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]201    exacts [Ideal.pow_mem_pow (hm ▸ hTmem) n, Ideal.pow_mem_pow (hm ▸ hXmem) n]202  -- `Θ ∘ Λ' = id`, checked modulo each power of `M`, using that `P` is maximal.203  have hPe : (IsLocalRing.maximalIdeal _).comap Λ = P := by ext x; rw [Ideal.mem_comap, hm, hP]204  have : P.IsMaximal := by205    rw [← hPe]; exact chart_point_isMaximal_of_residue_surjective _ _ Λ (hm ▸ hsurj)206  have hfix : Θ.comp Λ = completedPointMap _ P := by207    apply blowup_chart_ringHom_ext208    · intro r209      obtain ⟨g, rfl⟩ := Ideal.Quotient.mk_surjective r210      change Θ (Λ (chartBase _ _ _ (surfaceMk O pi u a b g))) = _211      rw [hΛ, hΘmk, hcomp]; rfl212    · change Θ (Λ _) = _213      rw [hΛZ, map_add, hΘalg, hΘX', hz_def]; ring214  have hle : M ≤ M.comap (Θ.comp Λ') := fun y hy => by215    refine (Ideal.span_le (I := M.comap Θ)).2 ?_ ((hmem y).1 hy)216    rintro w (rfl | rfl) <;> simp only [SetLike.mem_coe, Ideal.mem_comap, hΘT', hΘX', he, hz]217  have h6 : Θ.comp Λ' = RingHom.id _ :=218    completedLocalAt_ringHom_eq_id _ P _ (RingHom.ext fun x => by219      simp only [RingHom.comp_apply, hΛ' x]; exact DFunLike.congr_fun hfix x) hle220  exact ⟨RingEquiv.ofRingHom Λ' Θ h5 h6, fun y => rfl, hΘalg⟩221 222/-- A substitution `s : O[[T,X]] → O'[[T,X]]` with `E ↦ T`, `F ↦ T (X + α)` that maps the223relation of `R` into the relation ideal of `R'` induces a chart map `R[f/e] → R'` with224`f/e ↦ x' + α`. -/225private theorem chart_child_map_exists (O O' : Type) [CommRing O] [CommRing O'] (pi : O)226    (u : (TwoSeries O)ˣ) (a b : ℕ) (pi' : O') (u' : (TwoSeries O')ˣ) (a' b' : ℕ) (E F : TwoSeries O)227    (s : TwoSeries O →+* TwoSeries O')228    (hs : s (surfaceRelation O pi u a b) ∈ surfaceIdeal O' pi' u' a' b') (α : O')229    (hE : s E = axisT O') (hF : s F = axisT O' * (axisX O' + MvPowerSeries.C α)) :230    ∃ Λ : efChart O pi u a b E F →+* ConcreteSurface O' pi' u' a' b',231      (∀ g : TwoSeries O, Λ (efBase O pi u a b E F (surfaceMk O pi u a b g)) =232          surfaceMk O' pi' u' a' b' (s g)) ∧233      Λ (efSlope O pi u a b E F) = surfaceX O' pi' u' a' b' + algebraMap O'234          (ConcreteSurface O' pi' u' a' b') α := by235  have hk : ∀ x ∈ surfaceIdeal O pi u a b, (surfaceMk O' pi' u' a' b') (s x) = 0 := by236    intro x hx237    obtain ⟨h, rfl⟩ := Ideal.mem_span_singleton.mp hx238    rw [map_mul, map_mul]239    have : (surfaceMk O' pi' u' a' b') (s (surfaceRelation O pi u a b)) = 0 :=240      Ideal.Quotient.eq_zero_iff_mem.mpr hs241    rw [this, zero_mul]242  let σ : ConcreteSurface O pi u a b →+* ConcreteSurface O' pi' u' a' b' :=243    Ideal.Quotient.lift _ ((surfaceMk O' pi' u' a' b').comp s) hk244  have hσ : ∀ g, σ (surfaceMk O pi u a b g) = surfaceMk O' pi' u' a' b' (s g) := fun g =>245    Ideal.Quotient.lift_mk _ _ _246  have hC : surfaceMk O' pi' u' a' b' (MvPowerSeries.C α) = algebraMap O'247      (ConcreteSurface O' pi' u' a' b') α := rfl248  obtain ⟨psi, h1, h2⟩ := blowup_chart_universal (ConcreteSurface O pi u a b)249      (ConcreteSurface O' pi' u' a' b')250    (surfaceMk O pi u a b E) (surfaceMk O pi u a b F) σ251    (surfaceX O' pi' u' a' b' + algebraMap O' (ConcreteSurface O' pi' u' a' b') α) (by252      rw [hσ, hσ, hE, hF, map_mul, map_add, hC]; rfl)253  exact ⟨psi, fun g => by rw [h1, hσ], h2⟩254 255/-- Every non-unit, non-zero-divisor `f̄` of the special fiber lifts to an ideal chart of the256concrete surface whose reduction generates the same ideal as `f̄`. -/257theorem concrete_residue_ideal_chart_exists (O : Type) [CommRing O] [IsDomain O]258    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (pi : O)259    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)260    (e : (ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})261      ≃+* SpecialFiber (IsLocalRing.ResidueField O) a b)262    (fbar : SpecialFiber (IsLocalRing.ResidueField O) a b) (hunit : ¬ IsUnit fbar)263    (hreg : Function.Injective (fun w : SpecialFiber (IsLocalRing.ResidueField O) a b => fbar * w))264    (N : ℕ) (hN : Module.length (SpecialFiber (IsLocalRing.ResidueField O) a b)265      (SpecialFiber (IsLocalRing.ResidueField O) a b ⧸ Ideal.span {fbar}) = N) :266    ∃ ch : IdealChart O (ConcreteSurface O pi u a b) pi N,267      Ideal.span268      {e ((Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})) ch.f)} =269      Ideal.span {fbar} := by270  obtain ⟨q, hq⟩ := e.surjective fbar271  obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective q272  have hfu : ¬ IsUnit f := fun h => hunit273      (hq ▸ (h.map274        (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi}))).map e)275  have hreg' : Function.Injective (fun w : SpecialFiber (IsLocalRing.ResidueField O) a b =>276      e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi}) f) * w) := by277          rw [hq]; exact hreg278  have hregR := concrete_surface_residue_regular_of_special_fiber O pi u a b f e hreg'279  have hlen := concrete_surface_special_fiber_length_transport O pi u a b f e280  rw [hq, hN] at hlen281  obtain ⟨hfree, hfin, hrank⟩ :=282    concrete_surface_curve_free_of_length O pi hpi u a b ha f hregR N hlen283  have := concrete_surface_isDomain O pi hpi u a b ha284  have hf0 : f ≠ 0 := by285    rintro rfl286    have : Subsingleton (SpecialFiber (IsLocalRing.ResidueField O) a b) :=287      ⟨fun x y => hreg (by simp only [← hq, map_zero, zero_mul])⟩288    exact hunit (Subsingleton.elim 1 fbar ▸ isUnit_one)289  let B0 := Module.Free.chooseBasis O (ConcreteSurface O pi u a b ⧸ Ideal.span {f})290  have hcard : Fintype.card291      (Module.Free.ChooseBasisIndex O (ConcreteSurface O pi u a b ⧸ Ideal.span {f})) = N := by292    rw [← hrank, Module.finrank_eq_card_chooseBasisIndex]293  let B : Module.Basis (Fin N) O (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) :=294    B0.reindex ((Fintype.equivFin _).trans (finCongr hcard))295  choose bb hbb using fun i => Ideal.Quotient.mk_surjective (B i)296  obtain ⟨E, hE⟩ := division_linear_equivalence O (ConcreteSurface O pi u a b) N f B bb hbb hf0297  refine ⟨⟨f, bb, E, hE, ?_⟩, ?_⟩298  · intro x y hxy299    apply hregR300    simp only at hxy ⊢301    exact (mul_comm _ _).trans (hxy.trans (mul_comm _ _))302  · exact congrArg (fun z => Ideal.span {z}) hq303 304/-! ### Closed points of the exceptional divisor -/305 306/-- For a polynomial `Φ` over `R`, the quotient of the chart `R[f/e]` by `(e, Φ(f/e))` is307`(R/(e, f))[X]/(Φ̄)`. -/308private theorem chart_point_quotient_adjoinRoot_equiv (R : Type) [CommRing R] (e f : R)309    (Φ : Polynomial R) :310    ∃ q : (BlowupChart R e f ⧸ Ideal.span311        {chartBase R e f e, Polynomial.eval₂ (chartBase R e f) (chartSlope R e f) Φ}) ≃+* AdjoinRoot312      (Φ.map (Ideal.Quotient.mk (Ideal.span ({e, f} : Set R)))),313      (∀ r : R, q (Ideal.Quotient.mk _ (chartBase R e f r)) = AdjoinRoot.of _314        (Ideal.Quotient.mk (Ideal.span ({e, f} : Set R)) r)) ∧ q315      (Ideal.Quotient.mk _ (chartSlope R e f)) = AdjoinRoot.root _ := by316  obtain ⟨ε, hεb, hεs⟩ := exceptional_chart_is_affine_line R e f317  set P := Polynomial.eval₂ (chartBase R e f) (chartSlope R e f) Φ with hP318  set J := exceptionalLevelIdeal R e f 1 with hJ319  have hsup : Ideal.span {chartBase R e f e, P} = J ⊔ Ideal.span {P} := by320    rw [hJ, exceptionalLevelIdeal, pow_one, ← Ideal.span_insert]321  have hεP : ε (Ideal.Quotient.mk J P) =322      Φ.map (Ideal.Quotient.mk (Ideal.span ({e, f} : Set R))) := by323    rw [hP, Polynomial.hom_eval₂]324    change (ε.toRingHom) _ = _325    rw [Polynomial.hom_eval₂]326    have h1 : ε.toRingHom.comp ((Ideal.Quotient.mk J).comp (chartBase R e f)) =327        Polynomial.C.comp (Ideal.Quotient.mk (Ideal.span ({e, f} : Set R))) := by328      exact RingHom.ext hεb329    have h2 : ε.toRingHom (Ideal.Quotient.mk J (chartSlope R e f)) = Polynomial.X := hεs330    rw [h1, h2]331    rfl332  have hK : Ideal.span {Φ.map (Ideal.Quotient.mk (Ideal.span ({e, f} : Set R)))} =333      (Ideal.map (Ideal.Quotient.mk J) (Ideal.span {P})).map ε.toRingHom := by334    rw [Ideal.map_span, Ideal.map_span, Set.image_singleton, Set.image_singleton]335    simp [hεP]336  let E1 := Ideal.quotEquivOfEq hsup337  let E2 := (DoubleQuot.quotQuotEquivQuotSup J (Ideal.span {P})).symm338  let E3 : ((BlowupChart R e f ⧸ J) ⧸ (Ideal.map (Ideal.Quotient.mk J) (Ideal.span {P}))) ≃+*339      AdjoinRoot (Φ.map (Ideal.Quotient.mk (Ideal.span ({e, f} : Set R)))) :=340    Ideal.quotientEquiv _ _ ε hK341  refine ⟨(E1.trans E2).trans E3, ?_, ?_⟩342  · intro r343    change Ideal.Quotient.mk _ (ε (Ideal.Quotient.mk J (chartBase R e f r))) = _344    rw [show Ideal.Quotient.mk J (chartBase R e f r) = levelBase R e f 1 r from rfl, hεb]345    rfl346  · change Ideal.Quotient.mk _ (ε (Ideal.Quotient.mk J (chartSlope R e f))) = _347    rw [show Ideal.Quotient.mk J (chartSlope R e f) = levelSlope R e f 1 from rfl, hεs]348    rfl349 350/-- If `Φ̄` is irreducible over the field `R/(e, f)`, then `(e, Φ(f/e))` is a maximal ideal of the351chart, equal to the preimage of the maximal ideal under any local map `Λ` killing it. -/352theorem chart_nonrational_point_span_eq_comap (R : Type) [CommRing R] (e f : R)353    [(Ideal.span ({e, f} : Set R)).IsMaximal] (Φ : Polynomial R)354    (hΦ : Irreducible (Φ.map (Ideal.Quotient.mk (Ideal.span ({e, f} : Set R))))) (S : Type)355    [CommRing S] [IsLocalRing S] (Λ : BlowupChart R e f →+* S)356    (he : Λ (chartBase R e f e) ∈ IsLocalRing.maximalIdeal S)357    (hΦZ : Λ (Polynomial.eval₂ (chartBase R e f) (chartSlope R e f) Φ)358      ∈ IsLocalRing.maximalIdeal S) :359    (Ideal.span360        {chartBase R e f e, Polynomial.eval₂ (chartBase R e f) (chartSlope R e f) Φ}).IsMaximal ∧361      Ideal.span {chartBase R e f e, Polynomial.eval₂ (chartBase R e f) (chartSlope R e f) Φ} =362      (IsLocalRing.maximalIdeal S).comap Λ := by363  obtain ⟨q, -, -⟩ := chart_point_quotient_adjoinRoot_equiv R e f Φ364  let _ := Ideal.Quotient.field (Ideal.span ({e, f} : Set R))365  have : Fact (Irreducible (Φ.map (Ideal.Quotient.mk (Ideal.span ({e, f} : Set R))))) := ⟨hΦ⟩366  have hF : IsField (AdjoinRoot (Φ.map (Ideal.Quotient.mk (Ideal.span ({e, f} : Set R))))) :=367    Field.toIsField _368  have hmax :369      (Ideal.span370        {chartBase R e f e, Polynomial.eval₂ (chartBase R e f) (chartSlope R e f) Φ}).IsMaximal :=371    Ideal.Quotient.maximal_of_isField _ (MulEquiv.isField hF q.toMulEquiv)372  refine ⟨hmax,373        hmax.eq_of_le (Ideal.comap_ne_top _ (IsLocalRing.maximalIdeal.isMaximal S).ne_top) ?_⟩374  rw [Ideal.span_le]375  rintro x (rfl | rfl)376  exacts [he, hΦZ]377 378/-- `(e, f/e - r)` is a maximal ideal of the chart `R[f/e]`, equal to the preimage of the maximal379ideal under any local map `Λ` killing it. -/380private theorem chart_rational_point_span_eq_comap (R : Type) [CommRing R] (e f : R)381    [(Ideal.span ({e, f} : Set R)).IsMaximal] (S : Type) [CommRing S] [IsLocalRing S]382    (Λ : BlowupChart R e f →+* S) (r : R) (he : Λ (chartBase R e f e) ∈ IsLocalRing.maximalIdeal S)383    (hr : Λ (chartSlope R e f) - Λ (chartBase R e f r) ∈ IsLocalRing.maximalIdeal S) :384    (Ideal.span {chartBase R e f e, chartSlope R e f - chartBase R e f r}).IsMaximal ∧ Ideal.span385      {chartBase R e f e, chartSlope R e f - chartBase R e f r} =386      (IsLocalRing.maximalIdeal S).comap Λ := by387  have hmax : (Ideal.span {chartBase R e f e, chartSlope R e f - chartBase R e f r}).IsMaximal := by388    obtain ⟨q, -, -⟩ := chart_point_quotient_adjoinRoot_equiv R e f389      (Polynomial.X - Polynomial.C r)390    have hev : Polynomial.eval₂ (chartBase R e f) (chartSlope R e f) (Polynomial.X - Polynomial.C r)391        = chartSlope R e f - chartBase R e f r := by392      simp [Polynomial.eval₂_sub]393    rw [hev] at q394    have hmap : (Polynomial.X - Polynomial.C r).map395        (Ideal.Quotient.mk (Ideal.span ({e, f} : Set R)))396        = Polynomial.X - Polynomial.C (Ideal.Quotient.mk (Ideal.span ({e, f} : Set R)) r) := by397      simp398    rw [hmap] at q399    let : Field (R ⧸ Ideal.span ({e, f} : Set R)) := Ideal.Quotient.field _400    let q2 := (Polynomial.quotientSpanXSubCAlgEquiv401      (Ideal.Quotient.mk (Ideal.span ({e, f} : Set R)) r)).toRingEquiv402    apply Ideal.Quotient.maximal_of_isField403    exact MulEquiv.isField (Field.toIsField (R ⧸ Ideal.span ({e, f} : Set R)))404      (q.trans q2).toMulEquiv405  refine ⟨hmax,406        hmax.eq_of_le (Ideal.comap_ne_top _ (IsLocalRing.maximalIdeal.isMaximal S).ne_top) ?_⟩407  rw [Ideal.span_le]408  rintro x (rfl | rfl)409  exacts [he, by simpa [map_sub] using hr]410 411/-- For an unramified lift `Φ`, the derivative `Φ'(x/t)` is invertible modulo the non-rational412point `(t, Φ(x/t))` of the `t`-chart. -/413private theorem nonrational_point_derivative_isUnit_mod (O : Type) [CommRing O] [IsDomain O]414    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)415    (ha : 0 < a) [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O)416    (hΦ : IsUnramifiedLift O Φ) :417    ∃ w : tChart O pi u a b,418      Polynomial.eval₂ ((tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b)))419          (tSlope O pi u a b)420      (Polynomial.derivative Φ) * w - 1 ∈ Ideal.span421      {tBase O pi u a b (surfaceT O pi u a b),422        Polynomial.eval₂ ((tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b)))423            (tSlope O pi u a b) Φ} := by424  set R := ConcreteSurface O pi u a b425  set t := surfaceT O pi u a b426  set x := surfaceX O pi u a b427  set I : Ideal R := Ideal.span ({t, x} : Set R) with hI428  have hmax : I.IsMaximal := concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha429  let _ : Field (R ⧸ I) := Ideal.Quotient.field I430  obtain ⟨e, -⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha431  have : Finite (R ⧸ I) := Finite.of_equiv _ e.toEquiv.symm432  set ψ : Polynomial (R ⧸ I) := (Φ.map (algebraMap O R)).map (Ideal.Quotient.mk I) with hψ433  have hirr : Irreducible ψ := by434    rw [hψ, Polynomial.map_map]435    exact unramified_lift_map_parameter_quotient_irreducible O pi hpi u a b ha Φ hΦ436  have : Fact (Irreducible ψ) := ⟨hirr⟩437  have hder : Polynomial.derivative ψ ≠ 0 :=438    (Polynomial.separable_iff_derivative_ne_zero hirr).1439        (PerfectField.separable_of_irreducible hirr)440  rw [← Polynomial.eval₂_map, ← Polynomial.eval₂_map, ← Polynomial.derivative_map]441  set J := Ideal.span442      {chartBase R t x t,443        Polynomial.eval₂ (chartBase R t x) (chartSlope R t x) (Φ.map (algebraMap O R))} with hJ444  obtain ⟨q, hqb, hqs⟩ := chart_point_quotient_adjoinRoot_equiv R t x (Φ.map (algebraMap O R))445  have hcomp : ((q : _ →+* AdjoinRoot ψ).comp (Ideal.Quotient.mk J)).comp (chartBase R t x)446      = (AdjoinRoot.of ψ).comp (Ideal.Quotient.mk I) := RingHom.ext hqb447  have heval : ∀ P : Polynomial R,448      q (Ideal.Quotient.mk J (Polynomial.eval₂ (chartBase R t x) (chartSlope R t x) P))449      = AdjoinRoot.mk ψ (P.map (Ideal.Quotient.mk I)) := by450    intro P451    change ((q : _ →+* AdjoinRoot ψ).comp (Ideal.Quotient.mk J))452        (Polynomial.eval₂ (chartBase R t x) (chartSlope R t x) P) = _453    rw [Polynomial.hom_eval₂, hcomp, RingHom.comp_apply]454    erw [hqs]455    rw [← Polynomial.eval₂_map, ← AdjoinRoot.aeval_eq, Polynomial.aeval_def]456    rfl457  set D := Polynomial.eval₂ (chartBase R t x) (chartSlope R t x)458      (Polynomial.derivative (Φ.map (algebraMap O R)))459  have hD : q (Ideal.Quotient.mk J D) = AdjoinRoot.mk ψ (Polynomial.derivative ψ) := by460    rw [heval]461    simp only [hψ, Polynomial.derivative_map]462  have hne : AdjoinRoot.mk ψ (Polynomial.derivative ψ) ≠ 0 := by463    rw [Ne, AdjoinRoot.mk_eq_zero]464    exact fun hdvd => hder465      (Polynomial.eq_zero_of_dvd_of_degree_lt hdvd (Polynomial.degree_derivative_lt hirr.ne_zero))466  obtain ⟨w, hw⟩ := Ideal.Quotient.mk_surjective467      (q.symm (AdjoinRoot.mk ψ (Polynomial.derivative ψ))⁻¹)468  refine ⟨w, ?_⟩469  rw [← Ideal.Quotient.eq_zero_iff_mem]470  have hsplit : Ideal.Quotient.mk J (D * w - 1) =471      Ideal.Quotient.mk J D * Ideal.Quotient.mk J w - 1 := rfl472  apply q.injective473  rw [hsplit, RingEquiv.map_zero]474  erw [map_sub q, map_mul q, map_one q, hD, hw, RingEquiv.apply_symm_apply, mul_inv_cancel₀ hne,475        sub_self]476 477/-- Hensel's lemma at a non-rational point `P = (t, Φ(x/t))` of the `t`-chart: `Φ` has a root in478the completion at `P` congruent to `x/t` modulo the maximal ideal. -/479private theorem nonrational_point_hensel_root (O : Type) [CommRing O] [IsDomain O]480    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)481    (ha : 0 < a) [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O)482    (hΦ : IsUnramifiedLift O Φ) (P : Ideal (tChart O pi u a b)) [P.IsPrime]483    (hP : P = Ideal.span484      {tBase O pi u a b (surfaceT O pi u a b),485      Polynomial.eval₂ ((tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b)))486          (tSlope O pi u a b) Φ}) :487    ∃ θ' : CompletedLocalAt (tChart O pi u a b) P,488      Polynomial.eval₂489      ((completedPointMap (tChart O pi u a b) P).comp ((tBase O pi u a b).comp490          (algebraMap O (ConcreteSurface O pi u a b))))491      θ' Φ = 0 ∧ θ' - completedPointMap (tChart O pi u a b) P (tSlope O pi u a b) ∈492      (IsLocalRing.maximalIdeal (Localization.AtPrime P)).map493      (localCompletionMap (Localization.AtPrime P)) := by494  set A := tChart O pi u a b495  set φ := (tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b)) with hφ496  set Z := tSlope O pi u a b497  obtain ⟨w, hw⟩ := nonrational_point_derivative_isUnit_mod O pi hpi u a b ha Φ hΦ498  rw [← hP] at hw499  have : IsNoetherianRing A := blowupChart_concrete_isNoetherianRing O pi u a b _ _500  have : IsNoetherianRing (Localization.AtPrime P) :=501    IsLocalization.isNoetherianRing P.primeCompl _ inferInstance502  set L := Localization.AtPrime P503  set c := completedPointMap A P504  have hmap : (IsLocalRing.maximalIdeal L).map (localCompletionMap L)505      = IsLocalRing.maximalIdeal (CompletedLocalAt A P) :=506    (AdicCompletion.maximalIdeal_eq_map (R := L)).symm507  have hPm : ∀ x ∈ P, c x ∈ IsLocalRing.maximalIdeal (CompletedLocalAt A P) := by508    intro x hx509    rw [← hmap]510    apply Ideal.mem_map_of_mem511    rw [← IsLocalization.AtPrime.map_eq_maximalIdeal P L]512    exact Ideal.mem_map_of_mem _ hx513  have hmem : Polynomial.eval₂ φ Z Φ ∈ P := by514    rw [hP]; exact Ideal.subset_span (by simp)515  have key : ∀ q : Polynomial O, (q.map (c.comp φ)).eval (c Z) = c (q.eval₂ φ Z) := fun q => by516    rw [Polynomial.eval_map, Polynomial.hom_eval₂]517  obtain ⟨θ, hθ, hθZ⟩ := HenselianRing.is_henselian518      (I := IsLocalRing.maximalIdeal (CompletedLocalAt A P))519    (Φ.map (c.comp φ)) (hΦ.1.map _) (c Z) (by rw [key]; exact hPm _ hmem) (by520      rw [Polynomial.derivative_map, key]521      refine IsUnit.of_mul_eq_one (Ideal.Quotient.mk _ (c w)) ?_522      rw [← map_mul, ← map_mul, ← map_one (Ideal.Quotient.mk _), Ideal.Quotient.eq, ← map_one c,523        ← map_sub]524      exact hPm _ hw)525  refine ⟨θ, by rwa [Polynomial.IsRoot, Polynomial.eval_map] at hθ, ?_⟩526  rw [hmap]; exact hθZ527 528/-- Let `Λ' : Â_P → R'` map the completion at a non-rational point `P` to the child surface529over `O[θ]`, compatibly with `O`, with `Λ'(x/t) = x' + θ`. Then `Λ'` sends a Hensel root `θ'` of530`Φ` near `x/t` to `θ`, so the lift `κ : O[θ] → Â_P`, `θ ↦ θ'`, is a section of `Λ'` on `O[θ]`. -/531private theorem nonrational_point_root_lift (O : Type) [CommRing O] [IsDomain O]532    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)533    (ha : 0 < a) [IsAdicComplete (IsLocalRing.maximalIdeal O) O]534    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O)535    (hΦ : IsUnramifiedLift O Φ) (hθ : IsUnit (AdjoinRoot.root Φ))536    (P : Ideal (tChart O pi u a b)) [P.IsPrime]537    (Λ' : CompletedLocalAt (tChart O pi u a b) P →+* childSurface O pi u a b Φ hθ)538    (hΛ'O : Λ'.comp ((completedPointMap (tChart O pi u a b) P).comp539        ((tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b)))) =540      (algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ)).comp541        (algebraMap O (AdjoinRoot Φ)))542    (hΛ'Z : Λ' (completedPointMap (tChart O pi u a b) P (tSlope O pi u a b)) =543      surfaceX (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi) (childUnit O u b Φ hθ) (a + b) 0 +544        algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ) (AdjoinRoot.root Φ))545    (θ' : CompletedLocalAt (tChart O pi u a b) P)546    (hroot : Polynomial.eval₂ ((completedPointMap (tChart O pi u a b) P).comp547      ((tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b)))) θ' Φ = 0)548    (hcong : Λ' (θ' - completedPointMap (tChart O pi u a b) P (tSlope O pi u a b)) ∈549      surfaceParameterIdeal (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)550        (childUnit O u b Φ hθ) (a + b) 0) (c : AdjoinRoot Φ) :551    Λ' (AdjoinRoot.lift ((completedPointMap (tChart O pi u a b) P).comp552      ((tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b)))) θ' hroot c) =553      algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ) c := by554  obtain ⟨_, _, hdvr, -, hirr, -, -, -⟩ := unramified_is_dvr O Φ hΦ555  have := hdvr556  have hpiδ : Irreducible (algebraMap O (AdjoinRoot Φ) pi) := hirr pi hpi557  have hab : 0 < a + b := by omega558  have : IsLocalRing (childSurface O pi u a b Φ hθ) :=559    concrete_surface_isLocalRing _ _ _ _ _ hpiδ.not_isUnit hab560  have hmax := concrete_surface_maximalIdeal_eq _ _ hpiδ (childUnit O u b Φ hθ) (a + b) 0 hab561  have hρθ : Φ.eval₂ (algebraMap O (AdjoinRoot Φ)) (AdjoinRoot.root Φ) = 0 :=562    AdjoinRoot.eval₂_root Φ563  -- `Λ' θ'` and `θ` are roots of `Φ` congruent modulo the maximal ideal, and `θ` is simple.564  have hθ' : Λ' θ' = algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ)565      (AdjoinRoot.root Φ) := by566    refine polynomial_root_unique_of_derivative_isUnit _ (Φ.map ((algebraMap (AdjoinRoot Φ)567      (childSurface O pi u a b Φ hθ)).comp (algebraMap O (AdjoinRoot Φ)))) _ (Λ' θ') ?_ ?_ ?_ ?_568    · rw [Polynomial.eval_map, ← Polynomial.hom_eval₂, hρθ, map_zero]569    · rw [Polynomial.eval_map, ← hΛ'O, ← Polynomial.hom_eval₂, hroot, map_zero]570    · rw [hmax, ← sub_add_cancel (Λ' θ') (Λ' (completedPointMap _ P (tSlope O pi u a b))),571        ← map_sub, hΛ'Z, add_sub_assoc, add_sub_cancel_right]572      exact Ideal.add_mem _ hcong (Ideal.subset_span (Set.mem_insert_of_mem _ rfl))573    · have hu := (simple_root_derivative_unit O Φ hΦ (AdjoinRoot.root Φ) (by574        rw [Polynomial.eval_map]; exact (congrArg _ hρθ).trans (map_zero _))).2575      have h2 : Polynomial.eval (algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ)576          (AdjoinRoot.root Φ)) (Polynomial.derivative (Φ.map ((algebraMap (AdjoinRoot Φ)577            (childSurface O pi u a b Φ hθ)).comp (algebraMap O (AdjoinRoot Φ))))) =578          algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ)579            ((Φ.map (AdjoinRoot.of Φ)).derivative.eval (AdjoinRoot.root Φ)) := by580        rw [Polynomial.derivative_map, Polynomial.derivative_map, Polynomial.eval_map,581          Polynomial.eval_map, Polynomial.hom_eval₂]582        rfl583      rw [h2]; exact hu.map _584  induction c using AdjoinRoot.induction_on with585  | ih p =>586    rw [AdjoinRoot.lift_mk, Polynomial.hom_eval₂, hΛ'O, hθ', ← Polynomial.hom_eval₂,587      ← AdjoinRoot.aeval_eq, Polynomial.aeval_def]588 589/-- A chart map `Λ : R[x/t] → R'` to the child surface over `O[θ]`, compatible with `O`, with590`Λ(t) = t'` and `Λ(x/t) = x' + θ`, contracts the maximal ideal of `R'` to the non-rational point591`P = (t, Φ(x/t))`. -/592private theorem nonrational_point_mem_iff (O : Type) [CommRing O] [IsDomain O]593    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)594    (ha : 0 < a) [IsAdicComplete (IsLocalRing.maximalIdeal O) O]595    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)596    (hθ : IsUnit (AdjoinRoot.root Φ)) (P : Ideal (tChart O pi u a b))597    (hP : P = Ideal.span598      {tBase O pi u a b (surfaceT O pi u a b),599      Polynomial.eval₂ ((tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b)))600          (tSlope O pi u a b) Φ})601    (Λ : tChart O pi u a b →+* childSurface O pi u a b Φ hθ)602    (hΛT : Λ (tBase O pi u a b (surfaceT O pi u a b)) =603      surfaceT (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi) (childUnit O u b Φ hθ) (a + b) 0)604    (hΛO : Λ.comp ((tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b))) =605      (algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ)).comp606        (algebraMap O (AdjoinRoot Φ)))607    (hΛZ : Λ (tSlope O pi u a b) =608      surfaceX (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi) (childUnit O u b Φ hθ) (a + b) 0 +609        algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ) (AdjoinRoot.root Φ))610    (x : tChart O pi u a b) :611    x ∈ P ↔ Λ x ∈ surfaceParameterIdeal (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)612      (childUnit O u b Φ hθ) (a + b) 0 := by613  obtain ⟨_, _, hdvr, -, hirr, -, -, -⟩ := unramified_is_dvr O Φ hΦ614  have := hdvr615  have hpiδ : Irreducible (algebraMap O (AdjoinRoot Φ) pi) := hirr pi hpi616  have hab : 0 < a + b := by omega617  have : IsLocalRing (childSurface O pi u a b Φ hθ) :=618    concrete_surface_isLocalRing _ _ _ _ _ hpiδ.not_isUnit hab619  have hmax := concrete_surface_maximalIdeal_eq _ _ hpiδ (childUnit O u b Φ hθ) (a + b) 0 hab620  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} :621      Set (ConcreteSurface O pi u a b))).IsMaximal :=622    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha623  have hirrR := unramified_lift_map_parameter_quotient_irreducible O pi hpi u a b ha Φ hΦ624  rw [← Polynomial.map_map] at hirrR625  obtain ⟨-, hspan⟩ := chart_nonrational_point_span_eq_comap _ _ _626    (Φ.map (algebraMap O (ConcreteSurface O pi u a b))) hirrR _ Λ627    (by rw [hΛT, hmax]; exact Ideal.subset_span (Set.mem_insert _ _)) (by628      -- `Φ(x' + θ) ≡ Φ(θ) = 0` modulo `x'`629      rw [Polynomial.eval₂_map, Polynomial.hom_eval₂, hΛO, hΛZ, hmax]630      obtain ⟨k, hk⟩ := Polynomial.sub_dvd_eval_sub (surfaceX (AdjoinRoot Φ)631        (algebraMap O (AdjoinRoot Φ) pi) (childUnit O u b Φ hθ) (a + b) 0 + algebraMap632          (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ) (AdjoinRoot.root Φ))633        (algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ) (AdjoinRoot.root Φ))634        (Φ.map ((algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ)).comp635          (algebraMap O (AdjoinRoot Φ))))636      have hF0 : Φ.eval₂ ((algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ)).comp637          (algebraMap O (AdjoinRoot Φ))) (algebraMap (AdjoinRoot Φ)638            (childSurface O pi u a b Φ hθ) (AdjoinRoot.root Φ)) = 0 := by639        rw [← Polynomial.hom_eval₂, show Φ.eval₂ (algebraMap O (AdjoinRoot Φ))640          (AdjoinRoot.root Φ) = 0 from AdjoinRoot.eval₂_root Φ, map_zero]641      rw [Polynomial.eval_map, Polynomial.eval_map, hF0, sub_zero, add_sub_cancel_right] at hk642      rw [hk]; exact Ideal.mul_mem_right _ _ (Ideal.subset_span (Set.mem_insert_of_mem _ rfl)))643  rw [← hmax, ← Ideal.mem_comap, ← hspan, hP, Polynomial.eval₂_map]644 645/-! ### The completion isomorphisms -/646 647/-- The completion of the `t`-chart at a non-rational point `(t, Φ(x/t))` is isomorphic to the648child surface over `O[θ] = O[X]/(Φ)`, compatibly with the chart substitution, and the image of649`θ` is the Hensel root of `Φ`. -/650theorem t_chart_nonrational_point_completion_equiv (O : Type) [CommRing O] [IsDomain O]651    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)652    (ha : 0 < a) [IsAdicComplete (IsLocalRing.maximalIdeal O) O]653    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)654    (hθ : IsUnit (AdjoinRoot.root Φ)) (P : Ideal (tChart O pi u a b)) [P.IsPrime]655    (hP : P = Ideal.span656      {tBase O pi u a b (surfaceT O pi u a b),657      Polynomial.eval₂ ((tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b)))658          (tSlope O pi u a b) Φ}) :659    ∃ Eq : CompletedLocalAt (tChart O pi u a b) P ≃+* childSurface O pi u a b Φ hθ,660      (∀ s : TwoSeries O,661        Eq (completedPointMap (tChart O pi u a b) P (tBase O pi u a b (surfaceMk O pi u a b s))) =662          surfaceMk (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi) (childUnit O u b Φ hθ) (a + b) 0663            (chartSubst (AdjoinRoot Φ) (AdjoinRoot.root Φ)664              (MvPowerSeries.map (algebraMap O (AdjoinRoot Φ)) s))) ∧665      Eq (completedPointMap (tChart O pi u a b) P (tSlope O pi u a b)) =666        surfaceX (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi) (childUnit O u b Φ hθ) (a + b) 0 +667          algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ) (AdjoinRoot.root Φ) ∧668      (∀ c : O,669        Eq (completedPointMap (tChart O pi u a b) P670            (tBase O pi u a b (algebraMap O (ConcreteSurface O pi u a b) c))) =671          algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ)672            (algebraMap O (AdjoinRoot Φ) c)) ∧673      Polynomial.eval₂ ((completedPointMap (tChart O pi u a b) P).comp674          ((tBase O pi u a b).comp (algebraMap O (ConcreteSurface O pi u a b))))675        (Eq.symm (algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ) (AdjoinRoot.root Φ)))676        Φ = 0 ∧677      Eq.symm (algebraMap (AdjoinRoot Φ) (childSurface O pi u a b Φ hθ) (AdjoinRoot.root Φ)) -678          completedPointMap (tChart O pi u a b) P (tSlope O pi u a b) ∈679        (IsLocalRing.maximalIdeal (Localization.AtPrime P)).map680          (localCompletionMap (Localization.AtPrime P)) := by681  obtain ⟨_, _, hdvr, -, hirr, -, -, -⟩ := unramified_is_dvr O Φ hΦ682  have := hdvr683  set θ := AdjoinRoot.root Φ684  set ρ := algebraMap O (AdjoinRoot Φ)685  set uδ := substUnit (AdjoinRoot Φ) θ (baseChangeUnit O ρ u) * shiftUnit (AdjoinRoot Φ) θ hθ ^ b686  set R := ConcreteSurface O pi u a b687  set Rδ := ConcreteSurface (AdjoinRoot Φ) (ρ pi) uδ (a + b) 0688  set A := BlowupChart R (surfaceT O pi u a b) (surfaceX O pi u a b)689  set cb := chartBase R (surfaceT O pi u a b) (surfaceX O pi u a b)690  set Z := chartSlope R (surfaceT O pi u a b) (surfaceX O pi u a b)691  set cpm := completedPointMap A P692  set aδ := algebraMap (AdjoinRoot Φ) Rδ693  set Xδ := surfaceX (AdjoinRoot Φ) (ρ pi) uδ (a + b) 0694  have hpiδ : Irreducible (ρ pi) := hirr pi hpi695  have hab : 0 < a + b := by omega696  have : IsLocalRing Rδ := concrete_surface_isLocalRing _ _ _ _ _ hpiδ.not_isUnit hab697  have : IsNoetherianRing A := blowupChart_concrete_isNoetherianRing O pi u a b _ _698  -- The chart substitution `s = chartSubst θ ∘ map ρ` and the chart map `Λ : A → Rδ` it induces.699  obtain ⟨hsC0, hsT0, hsX0, -⟩ := chartSubst_apply_generators (AdjoinRoot Φ) θ700  set s := (chartSubst (AdjoinRoot Φ) θ).toRingHom.comp (MvPowerSeries.map ρ)701  have hsC : ∀ c : O, s (MvPowerSeries.C c) = MvPowerSeries.C (ρ c) := fun c =>702    (congrArg (chartSubst (AdjoinRoot Φ) θ) (MvPowerSeries.map_C _ _)).trans (hsC0 _)703  have hsE : s (axisT O) = axisT (AdjoinRoot Φ) :=704    (congrArg (chartSubst (AdjoinRoot Φ) θ) (MvPowerSeries.map_X _ _)).trans hsT0705  have hsF : s (axisX O) = axisT (AdjoinRoot Φ) * (axisX (AdjoinRoot Φ) + MvPowerSeries.C θ) :=706    (congrArg (chartSubst (AdjoinRoot Φ) θ) (MvPowerSeries.map_X _ _)).trans hsX0707  have hs : s (surfaceRelation O pi u a b) = surfaceRelation (AdjoinRoot Φ) (ρ pi) uδ (a + b) 0 :=708    (chartSubst_surfaceRelation_base_change_and_x_chart O (AdjoinRoot Φ) ρ pi u a b).1 θ hθ709  obtain ⟨Λ, hΛ, hΛZ⟩ : ∃ Λ : A →+* Rδ, (∀ g : TwoSeries O,710      Λ (cb (surfaceMk O pi u a b g)) = surfaceMk (AdjoinRoot Φ) (ρ pi) uδ (a + b) 0 (s g)) ∧711      Λ Z = Xδ + aδ θ := chart_child_map_exists O (AdjoinRoot Φ) pi u a b (ρ pi) uδ (a + b) 0712    (axisT O) (axisX O) s (hs ▸ Ideal.mem_span_singleton_self _) θ hsE hsF713  have hΛC : ∀ c : O, Λ (cb (algebraMap O R c)) = aδ (ρ c) :=714    fun c ↦ (hΛ (MvPowerSeries.C c)).trans (congrArg _ (hsC c))715  have hΛCc : Λ.comp (cb.comp (algebraMap O R)) = aδ.comp ρ := RingHom.ext hΛC716  -- `P` is the preimage of the maximal ideal of `Rδ`; pass to the completion.717  have hP' := nonrational_point_mem_iff O pi hpi u a b ha Φ hΦ hθ P hP Λ718    (by have := hΛ (axisT O); rw [hsE] at this; exact this) hΛCc hΛZ719  obtain ⟨Λ', hΛ'⟩ := chart_child_completion_map_exists A (AdjoinRoot Φ) (ρ pi) hpiδ uδ720    (a + b) 0 hab Λ P hP'721  have hloc' := chart_child_completion_map_local A (AdjoinRoot Φ) (ρ pi) hpiδ uδ722    (a + b) 0 hab Λ P hP' Λ' hΛ'723  -- The Hensel root `θ'` of `Φ` maps to `θ`, so `θ ↦ θ'` extends `O → completion` to `κ`.724  obtain ⟨θ', hroot, hcong⟩ := nonrational_point_hensel_root O pi hpi u a b ha Φ hΦ P hP725  set κO := cpm.comp (cb.comp (algebraMap O R))726  have hΛ'κO : Λ'.comp κO = aδ.comp ρ := by rw [← hΛCc]; ext c; exact hΛ' _727  set κ := AdjoinRoot.lift κO θ' hroot with hκdef728  have hκ := nonrational_point_root_lift O pi hpi u a b ha Φ hΦ hθ P Λ' hΛ'κO729    ((hΛ' _).trans hΛZ) θ' hroot ((hloc' _).1 hcong)730  obtain ⟨E, hE, hEs⟩ : ∃ E : CompletedLocalAt A P ≃+* Rδ,731      (∀ y, E y = Λ' y) ∧ ∀ c, E.symm (aδ c) = κ c :=732    @chart_child_completion_equiv O (AdjoinRoot Φ) _ _ _ _ _ pi u a b (ρ pi)733    hpiδ uδ (a + b) 0 hab (axisT O) (axisX O) (Or.inl ⟨rfl, rfl⟩) ρ θ s hsC hsE hsF hs Λ hΛ hΛZ P734    ‹_› hP'735    (nonrational_point_residue_surjective O pi u a b Φ hθ Λ hΛ hΛZ) Λ' hΛ' κ hκ736    fun c => AdjoinRoot.lift_of (h := hroot)737  have hEθ : E.symm (aδ (AdjoinRoot.root Φ)) = θ' := by738    rw [hEs]; exact AdjoinRoot.lift_root (h := hroot)739  refine ⟨E, fun g => ((hE _).trans (hΛ' _)).trans (hΛ g), ((hE _).trans (hΛ' _)).trans hΛZ,740    fun c => ((hE _).trans (hΛ' _)).trans (hΛC c), ?_, ?_⟩741  · rw [hEθ]; exact hroot742  · rw [hEθ]; exact hcong743 744/-- Common form of the completion isomorphisms at the rational points of the exceptional745divisor: if `s : O[[T,X]] → O[[T,X]]` fixes constants, sends `E ↦ T`, `F ↦ T (X + α)` and the746relation to a child relation, then the completed local ring of `R[f/e]` at747`P = (e, f/e - α)` is isomorphic to the child surface, compatibly with `s`. -/748private theorem rational_point_completion_equiv (O : Type) [CommRing O] [IsDomain O]749    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)750    (u' : (TwoSeries O)ˣ) (a' b' : ℕ) (ha' : 0 < a') (E F : TwoSeries O)751    (hEF : (E = axisT O ∧ F = axisX O) ∨ (E = axisX O ∧ F = axisT O))752    (hEFmax : (Ideal.span ({surfaceMk O pi u a b E, surfaceMk O pi u a b F} :753      Set (ConcreteSurface O pi u a b))).IsMaximal)754    (α : O) (s : TwoSeries O →+* TwoSeries O)755    (hsC : ∀ c : O, s (MvPowerSeries.C c) = MvPowerSeries.C c) (hsE : s E = axisT O)756    (hsF : s F = axisT O * (axisX O + MvPowerSeries.C α))757    (hrel : s (surfaceRelation O pi u a b) = surfaceRelation O pi u' a' b')758    (P : Ideal (efChart O pi u a b E F)) (hPp : P.IsPrime)759    (hP : P = Ideal.span {efBase O pi u a b E F (surfaceMk O pi u a b E),760      efSlope O pi u a b E F - efBase O pi u a b E F (algebraMap O (ConcreteSurface O pi u a b)761          α)}) :762    ∃ Eq : CompletedLocalAt (efChart O pi u a b E F) P ≃+* ConcreteSurface O pi u' a' b',763      (∀ g : TwoSeries O, Eq (completedPointMap (efChart O pi u a b E F) P764          (efBase O pi u a b E F (surfaceMk O pi u a b g))) =765        surfaceMk O pi u' a' b' (s g)) ∧766      Eq (completedPointMap (efChart O pi u a b E F) P (efSlope O pi u a b E F)) =767        surfaceX O pi u' a' b' + algebraMap O (ConcreteSurface O pi u' a' b') α ∧768      ∀ c : O, Eq769        (completedPointMap (efChart O pi u a b E F) P (efBase O pi u a b E F770            (algebraMap O (ConcreteSurface O pi u a b) c))) =771        algebraMap O (ConcreteSurface O pi u' a' b') c := by772  have : IsLocalRing (ConcreteSurface O pi u' a' b') :=773    concrete_surface_isLocalRing O pi _ _ _ hpi.not_isUnit ha'774  have : IsNoetherianRing (efChart O pi u a b E F) := blowupChart_concrete_isNoetherianRing O pi u a775      b _ _776  have hmax := concrete_surface_maximalIdeal_eq O pi hpi u' a' b' ha'777  obtain ⟨Λ, hΛ, hΛZ⟩ := chart_child_map_exists O O pi u a b pi u' a' b' E F s778    (hrel ▸ Ideal.mem_span_singleton_self _) α hsE hsF779  set R0 := ConcreteSurface O pi u' a' b'780  have hT : surfaceMk O pi u' a' b' (axisT O) ∈ IsLocalRing.maximalIdeal R0 := by781    rw [hmax]; exact Ideal.subset_span (Set.mem_insert _ _)782  have hXm : surfaceX O pi u' a' b' ∈ IsLocalRing.maximalIdeal R0 := by783    rw [hmax]; exact Ideal.subset_span (Set.mem_insert_of_mem _ rfl)784  have hΛC : ∀ c : O,785      Λ (efBase O pi u a b E F (algebraMap O (ConcreteSurface O pi u a b) c)) = algebraMap O R0 c :=786    fun c ↦ (hΛ (MvPowerSeries.C c)).trans (congrArg _ (hsC c))787  have := hEFmax788  have := hPp789  obtain ⟨-, hspan⟩ := chart_rational_point_span_eq_comap (ConcreteSurface O pi u a b)790    (surfaceMk O pi u a b E) (surfaceMk O pi u a b F) R0 Λ (algebraMap O _ α)791    (by rw [hΛ, hsE]; exact hT) (by rw [hΛZ, hΛC, add_sub_cancel_right]; exact hXm)792  have hP' : ∀ x, x ∈ P ↔ Λ x ∈ surfaceParameterIdeal O pi u' a' b' := fun x ↦ by793    rw [← hmax, ← Ideal.mem_comap, ← hspan, hP]794  have hsurj : ∀ y : R0, ∃ x, Λ x - y ∈ surfaceParameterIdeal O pi u' a' b' := by795    intro y796    obtain ⟨s', rfl⟩ := Ideal.Quotient.mk_surjective y797    refine ⟨efBase O pi u a b E F (algebraMap O (ConcreteSurface O pi u a b)798        (MvPowerSeries.constantCoeff s')), ?_⟩799    rw [hΛC, ← neg_sub]800    exact (Ideal.neg_mem_iff _).mpr801      (concrete_surface_sub_constantCoeff_mem_parameterIdeal O pi u' a' b' s')802  obtain ⟨Λ', hΛ'⟩ := chart_child_completion_map_exists _ O pi hpi u' a' b' ha' Λ P hP'803  obtain ⟨e, he, -⟩ := chart_child_completion_equiv O O pi u a b pi hpi u' a' b' ha' E F hEF804    (RingHom.id O) α s hsC hsE hsF hrel Λ hΛ hΛZ P hP' hsurj Λ' hΛ'805    ((completedPointMap (efChart O pi u a b E F) P).comp ((efBase O pi u a b E F).comp806        (algebraMap O _)))807    (fun c ↦ by808      change Λ' (completedPointMap _ P (efBase O pi u a b E F (algebraMap O _ c))) = _809      rw [hΛ', hΛC]) fun c ↦ rfl810  exact ⟨e, fun g ↦ ((he _).trans (hΛ' _)).trans (hΛ g), ((he _).trans (hΛ' _)).trans hΛZ,811    fun c ↦ ((he _).trans (hΛ' _)).trans (hΛC c)⟩812 813/-- The completion of the `t`-chart at its origin `(t, x/t)` is the concrete surface814with unit `substUnit O 0 u` and exponents `(a + b, b)`, compatibly with the chart substitution. -/815theorem t_chart_origin_completion_equiv (O : Type) [CommRing O] [IsDomain O]816    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)817    (ha : 0 < a) (P : Ideal (tChart O pi u a b)) [P.IsPrime]818    (hP : P = Ideal.span {tBase O pi u a b (surfaceT O pi u a b), tSlope O pi u a b}) :819    ∃ Eq : CompletedLocalAt (tChart O pi u a b) P ≃+* ConcreteSurface O pi (substUnit O 0 u) (a + b)820        b,821      (∀ s : TwoSeries O,822        Eq (completedPointMap (tChart O pi u a b) P (tBase O pi u a b (surfaceMk O pi u a b s))) =823            surfaceMk O pi824        (substUnit O 0 u) (a + b) b (chartSubst O 0 s)) ∧ Eq (completedPointMap (tChart O pi u a b)825            P (tSlope O pi u a b)) =826      surfaceX O pi (substUnit O 0 u) (a + b) b ∧ ∀ c : O,827      Eq (completedPointMap (tChart O pi u a b) P (tBase O pi u a b828          (algebraMap O (ConcreteSurface O pi u a b) c))) =829      algebraMap O (ConcreteSurface O pi (substUnit O 0 u) (a + b) b) c := by830  obtain ⟨hsC, hsT, hsX, -⟩ := chartSubst_apply_generators O 0831  obtain ⟨e, h1, h2, h3⟩ := rational_point_completion_equiv O pi hpi u a b (substUnit O 0 u)832    (a + b) b (by omega) (axisT O) (axisX O) (Or.inl ⟨rfl, rfl⟩)833    (concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha) 0 (chartSubst O 0).toRingHom834    hsC hsT hsX (chartSubst_surfaceRelation_origin_and_unit_point O pi u a b).1 P ‹_›835    (by rw [hP]; simp only [map_zero, sub_zero]; rfl)836  rw [map_zero, add_zero] at h2837  exact ⟨e, h1, h2, h3⟩838 839/-- The completion of the `t`-chart at a rational point `(t, x/t - α)` with `α` a unit is the840child concrete surface with exponents `(a + b, 0)`, compatibly with the chart substitution. -/841theorem t_chart_unit_point_completion_equiv (O : Type) [CommRing O] [IsDomain O]842    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)843    (ha : 0 < a) (α : O) (hα : IsUnit α) (P : Ideal (tChart O pi u a b)) [P.IsPrime]844    (hP : P = Ideal.span845      {tBase O pi u a b (surfaceT O pi u a b), tSlope O pi u a b - tBase O pi u a b846          (algebraMap O (ConcreteSurface O pi u a b) α)}) :847    ∃ Eq : CompletedLocalAt (tChart O pi u a b) P ≃+* ConcreteSurface O pi848      (substUnit O α u * shiftUnit O α hα ^ b) (a + b) 0,849      (∀ s : TwoSeries O,850        Eq (completedPointMap (tChart O pi u a b) P (tBase O pi u a b (surfaceMk O pi u a b s))) =851            surfaceMk O pi852        (substUnit O α u * shiftUnit O α hα ^ b) (a + b) 0 (chartSubst O α s)) ∧ Eq853      (completedPointMap (tChart O pi u a b) P (tSlope O pi u a b)) =854          surfaceX O pi (substUnit O α u * shiftUnit O α hα ^ b)855      (a + b) 0 + algebraMap O856      (ConcreteSurface O pi (substUnit O α u * shiftUnit O α hα ^ b) (a + b) 0) α ∧ ∀ c : O,857      Eq (completedPointMap (tChart O pi u a b) P (tBase O pi u a b858          (algebraMap O (ConcreteSurface O pi u a b) c))) =859      algebraMap O (ConcreteSurface O pi (substUnit O α u * shiftUnit O α hα ^ b) (a + b) 0) c := by860  obtain ⟨hsC, hsT, hsX, -⟩ := chartSubst_apply_generators O α861  exact rational_point_completion_equiv O pi hpi u a b _ (a + b) 0 (by omega) (axisT O) (axisX O)862    (Or.inl ⟨rfl, rfl⟩) (concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha) α863    (chartSubst O α).toRingHom hsC hsT hsX864    ((chartSubst_surfaceRelation_origin_and_unit_point O pi u a b).2 α hα) P ‹_› hP865 866/-- The completion of the `x`-chart at its origin `(x, t/x)` is the child concrete surface with867exponents `(a + b, a)`, compatibly with the `x`-chart substitution. -/868theorem x_chart_infinity_completion_equiv (O : Type) [CommRing O] [IsDomain O]869    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)870    (ha : 0 < a) (P : Ideal (xChart O pi u a b)) [P.IsPrime]871    (hP : P = Ideal.span {xBase O pi u a b (surfaceX O pi u a b), xSlope O pi u a b}) :872    ∃ Eq : CompletedLocalAt (xChart O pi u a b) P ≃+* ConcreteSurface O pi (xSubstUnit O u) (a + b)873        a,874      (∀ s : TwoSeries O,875        Eq (completedPointMap (xChart O pi u a b) P (xBase O pi u a b (surfaceMk O pi u a b s))) =876            surfaceMk O pi877        (xSubstUnit O u) (a + b) a (xChartSubst O s)) ∧ Eq (completedPointMap (xChart O pi u a b) P878            (xSlope O pi u a b)) =879      surfaceX O pi (xSubstUnit O u) (a + b) a ∧ ∀ c : O,880      Eq (completedPointMap (xChart O pi u a b) P (xBase O pi u a b881          (algebraMap O (ConcreteSurface O pi u a b) c))) =882      algebraMap O (ConcreteSurface O pi (xSubstUnit O u) (a + b) a) c := by883  obtain ⟨-, -, -, hsC, hsT, hsX, -⟩ := chartSubst_apply_generators O 0884  obtain ⟨e, h1, h2, h3⟩ := rational_point_completion_equiv O pi hpi u a b (xSubstUnit O u)885    (a + b) a (by omega) (axisX O) (axisT O) (Or.inr ⟨rfl, rfl⟩)886    (by rw [Ideal.span_pair_comm]; exact concrete_surface_parameterIdeal_isMaximal O pi hpi u a b887          ha)888    0 (xChartSubst O).toRingHom hsC hsX (by rw [map_zero, add_zero]; exact hsT)889    (chartSubst_surfaceRelation_base_change_and_x_chart O O (RingHom.id O) pi u a b).2 P ‹_›890    (by rw [hP]; simp only [map_zero, sub_zero]; rfl)891  rw [map_zero, add_zero] at h2892  exact ⟨e, h1, h2, h3⟩893 894end SurfaceBlowup