Regularity 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.Charts7import SurfaceBlowup.Surfaces.Completeness8import Mathlib.RingTheory.AdicCompletion.LocalRing9import Mathlib.RingTheory.KrullDimension.NonZeroDivisors10 11/-!12# Regularity of the concrete surface13 14The concrete surface `R = O[[T,X]] / (π - u T^a X^b)` is a two-dimensional regular local15domain, `(t, x)` and `(x, t)` are regular parameter pairs, and quotients `R/(f)` by suitable16non-units are free `O`-modules of rank `length R/(π, f)`. We also construct the maps from17completed local rings of blow-up charts to child surfaces.18 19## Main results20 21* `concrete_surface_isDomain`, `concrete_surface_isRegularLocalRing`,22  `concrete_surface_ringKrullDim_eq_two`, `concrete_surface_data_exists_unconditional`.23* `concrete_surface_regular_pair_tx`, `concrete_surface_equiv_regular_pair`.24* `concrete_surface_curve_free_of_length`.25* `chart_child_completion_map_exists`, `chart_child_completion_map_local`,26  `child_series_eval_comp_chart_subst`.27 28Provenance: `blowupChart_concrete_isNoetherianRing`, `nonrational_point_residue_surjective`,29`chart_child_completion_map_{exists,local}`, `concrete_surface_{regular_pair_tx, regular_pair_xt,30isDomain, equiv_instances, equiv_regular_pair, two_le_ringKrullDim, isRegularLocalRing,31ringKrullDim_eq_two, data_exists, data_exists_unconditional, pi_regular_mod_curve, curve_basis,32curve_free_finrank, curve_free_of_length}`, `regular_pair_first_regular_mod_second`,33`child_series_eval_comp_chart_subst`.34-/35 36namespace SurfaceBlowup37 38/-! ### Blow-up charts and their completions -/39 40/-- Every blow-up chart of the concrete surface is noetherian. -/41theorem blowupChart_concrete_isNoetherianRing (O : Type) [CommRing O] [IsNoetherianRing O] (pi : O)42    (u : (TwoSeries O)ˣ) (a b : ℕ) (e f : ConcreteSurface O pi u a b) :43    IsNoetherianRing (BlowupChart (ConcreteSurface O pi u a b) e f) := by44  have := concrete_surface_isNoetherianRing O pi u a b45  unfold BlowupChart46  infer_instance47 48/-- For the chart map `Λ` to the concrete surface over `O[θ] = O[X]/(Φ)` attached to a49non-rational point, every element of the target is congruent modulo the parameter ideal to an50element in the image of `Λ`. -/51theorem nonrational_point_residue_surjective (O : Type) [CommRing O] [IsDomain O]52    [IsDiscreteValuationRing O] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ)53    [IsAdicComplete (IsLocalRing.maximalIdeal O) O]54    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O)55    (hθ : IsUnit (AdjoinRoot.root Φ))56    (Λ : BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)57      (surfaceX O pi u a b) →+* ConcreteSurface (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)58      (substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)59      (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) * shiftUnit (AdjoinRoot Φ)60      (AdjoinRoot.root Φ) hθ ^ b) (a + b) 0)61    (hΛ : ∀ g : TwoSeries O,62      Λ (chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)63      (surfaceMk O pi u a b g)) = surfaceMk (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)64      (substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)65      (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) * shiftUnit (AdjoinRoot Φ)66      (AdjoinRoot.root Φ) hθ ^ b) (a + b) 067      (chartSubst (AdjoinRoot Φ) (AdjoinRoot.root Φ)68      (MvPowerSeries.map (algebraMap O (AdjoinRoot Φ)) g)))69    (hΛZ : Λ (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) =70      surfaceX (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)71      (substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)72      (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) * shiftUnit (AdjoinRoot Φ)73      (AdjoinRoot.root Φ) hθ ^ b) (a + b) 0 + algebraMap (AdjoinRoot Φ)74      (ConcreteSurface (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)75      (substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)76      (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) * shiftUnit (AdjoinRoot Φ)77      (AdjoinRoot.root Φ) hθ ^ b) (a + b) 0) (AdjoinRoot.root Φ)) :78    ∀ y : ConcreteSurface (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)79      (substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)80        (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) * shiftUnit (AdjoinRoot Φ)81        (AdjoinRoot.root Φ) hθ ^ b) (a + b) 0,82      ∃ x : BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b),83      Λ x - y ∈ surfaceParameterIdeal (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)84      (substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)85        (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) * shiftUnit (AdjoinRoot Φ)86        (AdjoinRoot.root Φ) hθ ^ b) (a + b) 0 := by87  intro y88  obtain ⟨s', rfl⟩ := Ideal.Quotient.mk_surjective y89  set B := chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)90  set I := surfaceParameterIdeal (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)91    (substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)92      (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) * shiftUnit (AdjoinRoot Φ)93      (AdjoinRoot.root Φ) hθ ^ b) (a + b) 094  have hXI : surfaceX _ _ _ _ _ ∈ I := Ideal.subset_span (Set.mem_insert_of_mem _ rfl)95  obtain ⟨p, hp⟩ : ∃ p, AdjoinRoot.mk Φ p = MvPowerSeries.constantCoeff s' :=96    Ideal.Quotient.mk_surjective _97  refine ⟨p.eval₂ (B.comp (algebraMap O _)) (chartSlope _ _ _), ?_⟩98  -- `Λ (p(θ)) ≡ p(θ) ≡ s'(0, 0) ≡ s'` modulo the parameter ideal99  have key : Λ (p.eval₂ (B.comp (algebraMap O _)) (chartSlope _ _ _)) -100      algebraMap (AdjoinRoot Φ) _ (MvPowerSeries.constantCoeff s') ∈ I := by101    rw [← Ideal.Quotient.eq, Polynomial.hom_eval₂, hΛZ, ← hp, ← AdjoinRoot.aeval_eq,102      Polynomial.aeval_def, Polynomial.hom_eval₂, Polynomial.hom_eval₂, map_add,103      Ideal.Quotient.eq_zero_iff_mem.mpr hXI, zero_add, Polynomial.hom_eval₂]104    congr 1105    refine RingHom.ext fun c₀ ↦ ?_106    change Ideal.Quotient.mk I (Λ (B (surfaceMk O pi u a b (MvPowerSeries.C c₀)))) = _107    rw [hΛ, MvPowerSeries.map_C,108      (chartSubst_apply_generators (AdjoinRoot Φ) (AdjoinRoot.root Φ)).1]109    rfl110  have := I.sub_mem key (concrete_surface_sub_constantCoeff_mem_parameterIdeal _ _ _ _ _ s')111  rwa [sub_sub_sub_cancel_right] at this112 113/-- A ring map `Λ : A → R'` to a concrete surface, under which `P` is the preimage of the114parameter ideal, extends to the completed local ring of `A` at `P`. -/115theorem chart_child_completion_map_exists (A : Type) [CommRing A] [IsNoetherianRing A] (O' : Type)116    [CommRing O'] [IsDomain O'] [IsDiscreteValuationRing O'] (pi' : O') (hpi' : Irreducible pi')117    (u' : (TwoSeries O')ˣ) (a' b' : ℕ) (ha' : 0 < a') (Λ : A →+* ConcreteSurface O' pi' u' a' b')118    (P : Ideal A) [P.IsPrime] (hP : ∀ x : A, x ∈ P ↔ Λ x ∈ surfaceParameterIdeal O' pi' u' a' b') :119    ∃ Λ' : CompletedLocalAt A P →+* ConcreteSurface O' pi' u' a' b', ∀ x : A,120      Λ' (completedPointMap A P x) = Λ x := by121  have hloc : IsLocalRing (ConcreteSurface O' pi' u' a' b') :=122    concrete_surface_isLocalRing O' pi' u' a' b' hpi'.not_isUnit ha'123  set R := ConcreteSurface O' pi' u' a' b'124  have hmax : IsLocalRing.maximalIdeal R = surfaceParameterIdeal O' pi' u' a' b' :=125    concrete_surface_maximalIdeal_eq O' pi' hpi' u' a' b' ha'126  have hcomp : IsAdicComplete (IsLocalRing.maximalIdeal R) R :=127    concrete_surface_isAdicComplete_maximalIdeal O' pi' hpi' u' a' b' ha'128  set m' := IsLocalRing.maximalIdeal R129  -- Step 1: localize130  have hunit (y : P.primeCompl) : IsUnit (Λ y) := by131    by_contra h132    exact y.2 ((hP y).2 (hmax ▸ (IsLocalRing.mem_maximalIdeal _).2 h))133  let ΛP : (Localization.AtPrime P) →+* R := IsLocalization.lift (M := P.primeCompl) hunit134  have hΛP : ∀ x : A,135      ΛP (algebraMap A (Localization.AtPrime P) x) = Λ x := fun x ↦ IsLocalization.lift_eq _ _136  -- Step 2137  have hle : (IsLocalRing.maximalIdeal (Localization.AtPrime P)).map ΛP ≤ m' := by138    rw [← IsLocalization.AtPrime.map_eq_maximalIdeal P (Localization.AtPrime P), Ideal.map_map,139          Ideal.map_le_iff_le_comap]140    intro x hx141    simp only [Ideal.mem_comap, RingHom.coe_comp, Function.comp_apply]142    rw [hΛP, hmax]; exact (hP x).1 hx143  have hlen (n : ℕ) :144      (IsLocalRing.maximalIdeal (Localization.AtPrime P)) ^ n ≤ (m' ^ n).comap ΛP := by145    rw [← Ideal.map_le_iff_le_comap, Ideal.map_pow]146    exact Ideal.pow_right_mono hle n147  -- Step 3148  let f : (n : ℕ) → CompletedLocalAt A P →+* R ⧸ m' ^ n := fun n ↦149    (Ideal.quotientMap (m' ^ n) ΛP (hlen n)).comp150        (AdicCompletion.evalₐ (IsLocalRing.maximalIdeal (Localization.AtPrime P)) n).toRingHom151  have hf : ∀ {m n : ℕ} (hmn : m ≤ n), (Ideal.Quotient.factorPow m' hmn).comp (f n) = f m := by152    intro m n hmn153    ext y154    induction y using AdicCompletion.induction_on with155    | h s =>156      simp only [f, RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe,157        RingHom.coe_coe, AdicCompletion.evalₐ_mk, Ideal.quotientMap_mk,158        Ideal.Quotient.factorPow, Ideal.Quotient.factor_mk]159      rw [Ideal.Quotient.eq, ← map_sub]160      apply Ideal.mem_comap.mp (hlen m _)161      have := (s.property hmn)162      rw [SModEq.comm, SModEq.sub_mem] at this163      simpa [smul_eq_mul, Ideal.mul_top] using this164  refine ⟨IsAdicComplete.liftRingHom m' f hf, fun x ↦ ?_⟩165  rw [← sub_eq_zero]166  apply IsHausdorff.haus hcomp.toIsHausdorff167  intro n168  rw [SModEq.sub_mem, sub_zero, smul_eq_mul, Ideal.mul_top, ← Ideal.Quotient.eq_zero_iff_mem,169    map_sub, IsAdicComplete.mk_liftRingHom, sub_eq_zero]170  simp only [f, completedPointMap, localCompletionMap, RingHom.coe_comp, Function.comp_apply,171    AlgHom.toRingHom_eq_coe, RingHom.coe_coe]172  rw [AdicCompletion.algebraMap_apply, AdicCompletion.evalₐ_of, Ideal.quotientMap_mk,173        Algebra.algebraMap_self, RingHom.id_apply, hΛP]174 175/-- The extension `Λ'` of `chart_child_completion_map_exists` is local: the maximal ideal of176the completion is exactly the preimage of the parameter ideal. -/177theorem chart_child_completion_map_local (A : Type) [CommRing A] [IsNoetherianRing A] (O' : Type)178    [CommRing O'] [IsDomain O'] [IsDiscreteValuationRing O'] (pi' : O') (hpi' : Irreducible pi')179    (u' : (TwoSeries O')ˣ) (a' b' : ℕ) (ha' : 0 < a') (Λ : A →+* ConcreteSurface O' pi' u' a' b')180    (P : Ideal A) [P.IsPrime] (hP : ∀ x : A, x ∈ P ↔ Λ x ∈ surfaceParameterIdeal O' pi' u' a' b')181    (Λ' : CompletedLocalAt A P →+* ConcreteSurface O' pi' u' a' b')182    (hΛ' : ∀ x : A, Λ' (completedPointMap A P x) = Λ x) :183    ∀ y : CompletedLocalAt A P,184      y ∈ (IsLocalRing.maximalIdeal (Localization.AtPrime P)).map185      (localCompletionMap (Localization.AtPrime P)) ↔186      Λ' y ∈ surfaceParameterIdeal O' pi' u' a' b' := by187  have : IsLocalRing (ConcreteSurface O' pi' u' a' b') :=188    concrete_surface_isLocalRing O' pi' u' a' b' hpi'.not_isUnit ha'189  have e2 : (IsLocalRing.maximalIdeal (Localization.AtPrime P)).map190      (localCompletionMap (Localization.AtPrime P)) = P.map (completedPointMap A P) :=191    (congrArg (Ideal.map (localCompletionMap (Localization.AtPrime P)))192      (IsLocalization.AtPrime.map_eq_maximalIdeal P (Localization.AtPrime P)).symm).trans193      (Ideal.map_map _ _)194  intro y195  rw [e2]196  constructor197  · refine fun hy ↦ (Ideal.map_le_iff_le_comap.2 fun x hx ↦ ?_ :198      P.map (completedPointMap A P) ≤ (surfaceParameterIdeal O' pi' u' a' b').comap Λ') hy199    change Λ' (completedPointMap A P x) ∈ surfaceParameterIdeal O' pi' u' a' b'200    rw [hΛ']201    exact (hP x).1 hx202  · refine fun hy ↦ by_contra fun hn ↦ ?_203    have : IsNoetherianRing (Localization.AtPrime P) :=204      IsLocalization.isNoetherianRing P.primeCompl _ inferInstance205    have hu : IsUnit y := by_contra fun hnu ↦ hn <|206      AdicCompletion.maximalIdeal_eq_map.trans e2 ▸ (IsLocalRing.mem_maximalIdeal _).2 hnu207    rw [← concrete_surface_maximalIdeal_eq O' pi' hpi' u' a' b' ha'] at hy208    exact (IsLocalRing.mem_maximalIdeal _).1 hy (hu.map Λ')209 210/-! ### Regularity and dimension -/211 212/-- `(t, x)` is a regular parameter pair of the concrete surface. -/213theorem concrete_surface_regular_pair_tx (O : Type) [CommRing O] [IsDomain O] (pi : O)214    (hpi : pi ≠ 0) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a) :215    RegularParameterPair (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b) :=216      by217  have hP : MvPowerSeries.constantCoeff (surfaceRelation O pi u a b) ≠ 0 := by218    rw [surfaceRelation_constantCoeff O pi u a b ha]; exact hpi219  exact ⟨mvPowerSeries_quotient_var_regular (Fin 2) O 0 _ hP,220    mvPowerSeries_fin_two_quotient_var_regular_mod_var O 0 1 (by decide) _ hP⟩221 222/-- The concrete surface over a discrete valuation ring is a domain. -/223theorem concrete_surface_isDomain (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]224    (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a) :225    IsDomain (ConcreteSurface O pi u a b) := by226  have : Nontrivial (ConcreteSurface O pi u a b) :=227    Ideal.Quotient.nontrivial_iff.mpr (surfaceIdeal_ne_top O pi u a b hpi.not_isUnit ha)228  have := concrete_surface_isNoetherianRing O pi u a b229  have := concrete_surface_isLocalRing O pi u a b hpi.not_isUnit ha230  have hp := concrete_surface_span_T_isPrime O pi hpi u a b ha231  exact isDomain_of_regular_prime_element _ (surfaceT O pi u a b)232    (concrete_surface_regular_pair_tx O pi hpi.ne_zero u a b ha).1 hp233    (Ideal.iInf_pow_eq_bot_of_isLocalRing _ hp.ne_top)234 235/-- A ring isomorphic to a concrete surface is a noetherian complete local domain. -/236theorem concrete_surface_equiv_instances (S : Type) [CommRing S] (O' : Type) [CommRing O']237    [IsDomain O'] [IsDiscreteValuationRing O'] (pi' : O') (hpi' : Irreducible pi')238    (u' : (TwoSeries O')ˣ) (a' b' : ℕ) (ha' : 0 < a') (Eq : S ≃+* ConcreteSurface O' pi' u' a' b') :239    IsNoetherianRing S ∧ IsDomain S ∧ ∃ _ : IsLocalRing S,240      IsAdicComplete (IsLocalRing.maximalIdeal S) S := by241  have := concrete_surface_isNoetherianRing O' pi' u' a' b'242  have := concrete_surface_isDomain O' pi' hpi' u' a' b' ha'243  have := concrete_surface_isLocalRing O' pi' u' a' b' hpi'.not_isUnit ha'244  have hC := concrete_surface_isAdicComplete_maximalIdeal O' pi' hpi' u' a' b' ha'245  refine ⟨isNoetherianRing_of_ringEquiv _ Eq.symm, Eq.toMulEquiv.isDomain, ?_⟩246  have : Nontrivial S := Eq.toEquiv.nontrivial247  have hLS : IsLocalRing S :=248    IsLocalRing.of_surjective' (Eq.symm : ConcreteSurface O' pi' u' a' b' →+* S) Eq.symm.surjective249  refine ⟨hLS, ?_⟩250  have : ((IsLocalRing.maximalIdeal (ConcreteSurface O' pi' u' a' b')).comap251      (Eq : S →+* _)).IsMaximal := Ideal.comap_isMaximal_of_surjective _ Eq.surjective252  have hm : (IsLocalRing.maximalIdeal (ConcreteSurface O' pi' u' a' b')).map Eq.symm =253      IsLocalRing.maximalIdeal S := by254    rw [← IsLocalRing.eq_maximalIdeal this]; exact Ideal.map_symm Eq255  rw [← hm]256  exact (IsAdicComplete.congr_ringEquiv257    (I := IsLocalRing.maximalIdeal (ConcreteSurface O' pi' u' a' b')) Eq.symm).mpr hC258 259/-- `(x, t)` is a regular parameter pair of the concrete surface. -/260theorem concrete_surface_regular_pair_xt (O : Type) [CommRing O] [IsDomain O] (pi : O)261    (hpi : pi ≠ 0) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a) :262    RegularParameterPair (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b) :=263      by264  have hP : MvPowerSeries.constantCoeff (surfaceRelation O pi u a b) ≠ 0 := by265    rw [surfaceRelation_constantCoeff O pi u a b ha]; exact hpi266  exact ⟨mvPowerSeries_quotient_var_regular (Fin 2) O 1 _ hP,267    mvPowerSeries_fin_two_quotient_var_regular_mod_var O 1 0 (by decide) _ hP⟩268 269/-- Regular parameter pairs transport along ring isomorphisms. -/270private theorem regularParameterPair_transport {S R : Type} [CommRing S] [CommRing R] (e : S ≃+* R)271    (t x : R)272    (h : RegularParameterPair R t x) :273    RegularParameterPair S (e.symm t) (e.symm x) := by274  obtain ⟨h1, h2⟩ := h275  refine ⟨fun a b hab ↦ ?_, ?_⟩276  · apply e.injective277    apply h1278    simpa using congrArg e hab279  · have hJ : Ideal.span {t} = (Ideal.span {e.symm t}).map e := by280      rw [Ideal.map_span]; simp281    let Q := Ideal.quotientEquiv (Ideal.span {e.symm t}) (Ideal.span {t}) e hJ282    intro a b hab283    apply Q.injective284    apply h2285    obtain ⟨a', rfl⟩ := Ideal.Quotient.mk_surjective a286    obtain ⟨b', rfl⟩ := Ideal.Quotient.mk_surjective b287    have hx : Q (Ideal.Quotient.mk (Ideal.span {e.symm t}) (e.symm x)) =288        Ideal.Quotient.mk (Ideal.span {t}) x := by289      change Ideal.Quotient.mk _ (e (e.symm x)) = _290      simp291    have hab' : Ideal.Quotient.mk (Ideal.span {e.symm t}) (e.symm x * a') =292        Ideal.Quotient.mk (Ideal.span {e.symm t}) (e.symm x * b') := by293      simpa only [map_mul] using hab294    change _ * Q _ = _ * Q _295    rw [← hx, ← map_mul, ← map_mul, hab']296    simp only [map_mul]297 298/-- In a ring isomorphic to a concrete surface, the images of `(t, x)` and `(x, t)` are regular299parameter pairs; in particular `t` is a non-zero-divisor. -/300theorem concrete_surface_equiv_regular_pair (S : Type) [CommRing S] (O' : Type) [CommRing O']301    [IsDomain O'] [IsDiscreteValuationRing O'] (pi' : O') (hpi' : Irreducible pi')302    (u' : (TwoSeries O')ˣ) (a' b' : ℕ) (ha' : 0 < a') (Eq : S ≃+* ConcreteSurface O' pi' u' a' b') :303    RegularParameterPair S (Eq.symm (surfaceT O' pi' u' a' b'))304      (Eq.symm (surfaceX O' pi' u' a' b')) ∧ RegularParameterPair S305      (Eq.symm (surfaceX O' pi' u' a' b')) (Eq.symm (surfaceT O' pi' u' a' b')) ∧ Function.Injective306      (fun y : S ↦ Eq.symm (surfaceT O' pi' u' a' b') * y) := by307  have h1 := regularParameterPair_transport Eq _ _308    (concrete_surface_regular_pair_tx O' pi' hpi'.ne_zero u' a' b' ha')309  exact ⟨h1, regularParameterPair_transport Eq _ _310    (concrete_surface_regular_pair_xt O' pi' hpi'.ne_zero u' a' b' ha'), h1.1⟩311 312/-- A regular sequence `t, x` with `R/(t, x)` nontrivial forces `2 ≤ dim R`. -/313private theorem two_le_ringKrullDim_of_regular_pair {R : Type} [CommRing R] (t x : R)314    (h1 : Function.Injective (fun a : R ↦ t*a))315    (h2 : Function.Injective316        (fun a : R ⧸ Ideal.span {t} ↦ Ideal.Quotient.mk (Ideal.span {t}) x * a))317    (hP : Nontrivial (R ⧸ Ideal.span {t, x})) :318    (2 : WithBot ℕ∞) ≤ ringKrullDim R := by319  have ht : t ∈ nonZeroDivisors R := mem_nonZeroDivisors_iff_right.2 fun z hz ↦320    h1 (by simp only [mul_zero]; rw [mul_comm]; exact hz)321  have hx : Ideal.Quotient.mk (Ideal.span {t}) x ∈ nonZeroDivisors (R ⧸ Ideal.span {t}) :=322    mem_nonZeroDivisors_iff_right.2 fun z hz ↦323      h2 (by simp only [mul_zero]; rw [mul_comm]; exact hz)324  let f1 : R ⧸ Ideal.span {t} →+* R ⧸ Ideal.span {t, x} :=325    Ideal.Quotient.factor (Ideal.span_mono (by simp))326  let f2 : (R ⧸ Ideal.span {t}) ⧸ Ideal.span {Ideal.Quotient.mk (Ideal.span {t}) x} →+*327      R ⧸ Ideal.span {t, x} :=328    Ideal.Quotient.lift _ f1 fun z hz ↦ by329      obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.mp hz330      rw [map_mul, show f1 (Ideal.Quotient.mk (Ideal.span {t}) x) = 0 from331        Ideal.Quotient.eq_zero_iff_mem.2 (Ideal.subset_span (by simp)), mul_zero]332  have := f2.domain_nontrivial333  have k1 := ringKrullDim_quotient_succ_le_of_nonZeroDivisor ht334  have k2 := ringKrullDim_quotient_succ_le_of_nonZeroDivisor hx335  have k0 := ringKrullDim_nonneg_of_nontrivial336    (R := (R ⧸ Ideal.span {t}) ⧸ Ideal.span {Ideal.Quotient.mk (Ideal.span {t}) x})337  calc (2 : WithBot ℕ∞) = 0 + 1 + 1 := by norm_num338    _ ≤ ringKrullDim ((R ⧸ Ideal.span {t}) ⧸ Ideal.span {Ideal.Quotient.mk (Ideal.span {t}) x})339        + 1 + 1 := by gcongr340    _ ≤ ringKrullDim (R ⧸ Ideal.span {t}) + 1 := by gcongr341    _ ≤ _ := k1342 343/-- The concrete surface has Krull dimension at least `2`. -/344private theorem concrete_surface_two_le_ringKrullDim (O : Type) [CommRing O] [IsDomain O]345    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)346    (ha : 0 < a) :347    (2 : WithBot ℕ∞) ≤ ringKrullDim (ConcreteSurface O pi u a b) := by348  obtain ⟨h1, h2⟩ := concrete_surface_regular_pair_tx O pi hpi.ne_zero u a b ha349  obtain ⟨e, -⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha350  exact two_le_ringKrullDim_of_regular_pair _ _ h1 h2 e.toRingHom.domain_nontrivial351 352/-- The concrete surface is a regular local ring. -/353theorem concrete_surface_isRegularLocalRing (O : Type) [CommRing O] [IsDomain O]354    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)355    (ha : 0 < a) :356    IsRegularLocalRing (ConcreteSurface O pi u a b) := by357  have : IsLocalRing (ConcreteSurface O pi u a b) :=358    concrete_surface_isLocalRing O pi u a b hpi.not_isUnit ha359  have := concrete_surface_isNoetherianRing O pi u a b360  apply IsRegularLocalRing.of_spanFinrank_maximalIdeal_le361  exact le_trans (by exact_mod_cast concrete_surface_spanFinrank_le_two O pi hpi u a b ha)362    (concrete_surface_two_le_ringKrullDim O pi hpi u a b ha)363 364/-- The concrete surface has Krull dimension `2`. -/365theorem concrete_surface_ringKrullDim_eq_two (O : Type) [CommRing O] [IsDomain O]366    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)367    (ha : 0 < a) :368    ringKrullDim (ConcreteSurface O pi u a b) = 2 := by369  have : IsLocalRing (ConcreteSurface O pi u a b) :=370    concrete_surface_isLocalRing O pi u a b hpi.not_isUnit ha371  refine le_antisymm ((ringKrullDim_le_spanFinrank_maximalIdeal _).trans ?_)372    (concrete_surface_two_le_ringKrullDim O pi hpi u a b ha)373  exact_mod_cast concrete_surface_spanFinrank_le_two O pi hpi u a b ha374 375/-- The concrete surface carries `SurfaceData` with uniformizer `π`, parameters `t, x`, unit376`u` and exponents `a, b`. -/377private theorem concrete_surface_data_exists (O : Type) [CommRing O] [IsDomain O]378    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (pi : O)379    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)380    [IsDomain (ConcreteSurface O pi u a b)] [IsRegularLocalRing (ConcreteSurface O pi u a b)] :381    ∃ S : SurfaceData O (ConcreteSurface O pi u a b),382      S.pi = pi ∧ S.t = surfaceT O pi u a b ∧ S.x = surfaceX O pi u a b ∧ S.unit =383      surfaceUnit O pi u a b ∧ S.a = a ∧ S.b = b := by384  obtain ⟨e, he⟩ := concrete_surface_residueField_equiv O pi hpi u a b ha385  exact ⟨{386    pi := pi387    pi_irreducible := hpi388    t := surfaceT O pi u a b389    x := surfaceX O pi u a b390    unit := surfaceUnit O pi u a b391    a := a392    b := b393    a_pos := ha394    parameters := (concrete_surface_maximalIdeal_eq O pi hpi u a b ha).symm395    dimension := concrete_surface_ringKrullDim_eq_two O pi hpi u a b ha396    complete := concrete_surface_isAdicComplete_maximalIdeal O pi hpi u a b ha397    base_injective := concrete_surface_base_injective O pi hpi u a b ha398    residueEquiv := e399    residue_compat := he400    vertical := concrete_surface_vertical O pi u a b }, rfl, rfl, rfl, rfl, rfl, rfl⟩401 402/-- The concrete surface is a regular local domain carrying `SurfaceData` with uniformizer `π`,403parameters `t, x`, unit `u` and exponents `a, b`. -/404theorem concrete_surface_data_exists_unconditional (O : Type) [CommRing O] [IsDomain O]405    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (pi : O)406    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a) :407    ∃ (_ : IsDomain (ConcreteSurface O pi u a b))408      (_ : IsRegularLocalRing (ConcreteSurface O pi u a b)),409      ∃ D : SurfaceData O (ConcreteSurface O pi u a b),410      D.pi = pi ∧ D.t = surfaceT O pi u a b ∧ D.x = surfaceX O pi u a b ∧ D.unit =411      surfaceUnit O pi u a b ∧ D.a = a ∧ D.b = b := by412  have := concrete_surface_isDomain O pi hpi u a b ha413  have := concrete_surface_isRegularLocalRing O pi hpi u a b ha414  exact ⟨‹_›, ‹_›, concrete_surface_data_exists O pi hpi u a b ha⟩415 416/-! ### Curves on the concrete surface -/417 418/-- If `(p, f)` is a regular parameter pair, then `p` is a non-zero-divisor modulo `f`. -/419private theorem regular_pair_first_regular_mod_second (A : Type) [CommRing A] (p f : A)420    (h : RegularParameterPair A p f) :421    Function.Injective (fun v : A ⧸ Ideal.span {f} ↦ Ideal.Quotient.mk (Ideal.span {f}) p * v) :=422      by423  obtain ⟨h1, h2⟩ := h424  intro a b hab425  obtain ⟨a', rfl⟩ := Ideal.Quotient.mk_surjective a426  obtain ⟨b', rfl⟩ := Ideal.Quotient.mk_surjective b427  simp only at hab428  rw [← map_mul, ← map_mul, Ideal.Quotient.eq, ← mul_sub, Ideal.mem_span_singleton] at hab429  obtain ⟨w, hw⟩ := hab430  have hw0 : Ideal.Quotient.mk (Ideal.span {p}) f * Ideal.Quotient.mk (Ideal.span {p}) w431      = Ideal.Quotient.mk (Ideal.span {p}) f * 0 := by432    rw [mul_zero, ← map_mul, ← hw, Ideal.Quotient.eq_zero_iff_mem]433    exact Ideal.mem_span_singleton.2 (dvd_mul_right _ _)434  have := h2 hw0435  rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton] at this436  obtain ⟨w1, rfl⟩ := this437  have : a' - b' = f * w1 := h1 (by simp only; rw [hw]; ring)438  rw [Ideal.Quotient.eq, this, Ideal.mem_span_singleton]439  exact dvd_mul_right _ _440 441/-- If `f` is a non-zero-divisor modulo `π` on the concrete surface, then `π` is a442non-zero-divisor modulo `f`. -/443private theorem concrete_surface_pi_regular_mod_curve (O : Type) [CommRing O] [IsDomain O]444    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)445    (f : ConcreteSurface O pi u a b)446    (hf : Function.Injective447      (fun w : ConcreteSurface O pi u a b ⧸ Ideal.span448      {algebraMap O (ConcreteSurface O pi u a b) pi} => Ideal.Quotient.mk449      (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi}) f * w)) :450    Function.Injective451      (fun v : ConcreteSurface O pi u a b ⧸ Ideal.span {f} ↦ Ideal.Quotient.mk (Ideal.span {f})452        (algebraMap O (ConcreteSurface O pi u a b) pi) * v) :=453  regular_pair_first_regular_mod_second _ _ _454    ⟨concrete_surface_pi_regular O pi hpi u a b, hf⟩455 456/-- For `f` regular modulo `π`, a family that is a basis modulo `π` lifts to an457`O`-basis of the curve ring `R/(f)`. -/458theorem concrete_surface_curve_basis (O : Type) [CommRing O] [IsDomain O]459    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (pi : O)460    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)461    (f : ConcreteSurface O pi u a b)462    (hf : Function.Injective463      (fun w : ConcreteSurface O pi u a b ⧸ Ideal.span464      {algebraMap O (ConcreteSurface O pi u a b) pi} => Ideal.Quotient.mk465      (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi}) f * w)) {N : ℕ}466    (β : Fin N → ConcreteSurface O pi u a b)467    (hβ : ResidueBasisFamily pi (fun i ↦ Ideal.Quotient.mk (Ideal.span {f}) (β i))) :468    ∃ B : Module.Basis (Fin N) O (ConcreteSurface O pi u a b ⧸ Ideal.span {f}), ∀ i,469      B i = Ideal.Quotient.mk (Ideal.span {f}) (β i) := by470  have := dvr_isAdicComplete_span_uniformizer O pi hpi471  have := concrete_surface_curve_isAdicComplete O pi hpi u a b ha f472  have hinj := concrete_surface_pi_regular_mod_curve O pi hpi u a b f hf473  refine residue_basis_family_basis O _ pi (fun m hm ↦ ?_) _ hβ474  have h2 : (Ideal.Quotient.mk (Ideal.span {f}))475      ((algebraMap O (ConcreteSurface O pi u a b)) pi) * m = 0 :=476    (Algebra.smul_def pi m).symm.trans hm477  exact hinj (h2.trans (mul_zero (M₀ := ConcreteSurface O pi u a b ⧸ Ideal.span {f}) _).symm)478 479/-- For `f` regular modulo `π`, a residue basis family of size `N` shows that480`R/(f)` is free of rank `N` over `O`. -/481private theorem concrete_surface_curve_free_finrank (O : Type) [CommRing O] [IsDomain O]482    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (pi : O)483    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)484    (f : ConcreteSurface O pi u a b)485    (hf : Function.Injective486      (fun w : ConcreteSurface O pi u a b ⧸ Ideal.span487      {algebraMap O (ConcreteSurface O pi u a b) pi} => Ideal.Quotient.mk488      (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi}) f * w)) {N : ℕ}489    (β : Fin N → ConcreteSurface O pi u a b)490    (hβ : ResidueBasisFamily pi (fun i ↦ Ideal.Quotient.mk (Ideal.span {f}) (β i))) :491    Module.Free O (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) ∧ Module.Finite O492      (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) ∧ Module.finrank O493      (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) = N := by494  obtain ⟨B, _⟩ := concrete_surface_curve_basis O pi hpi u a b ha f hf β hβ495  exact ⟨Module.Free.of_basis B, Module.Finite.of_basis B, by simp [Module.finrank_eq_card_basis B]⟩496 497/-- Over an `O`-algebra `R`, the kernel of the reduction `R/(f) → R/(π, f)` consists of the498multiples of `π`. -/499private theorem factor_span_pair_eq_zero_iff {O R : Type} [CommRing O] [CommRing R] [Algebra O R]500    (pi : O) (f : R) (hle : Ideal.span {f} ≤ Ideal.span {algebraMap O R pi, f})501    (m : R ⧸ Ideal.span {f}) :502    Ideal.Quotient.factorₐ O hle m = 0 ↔ ∃ w, m = pi • w := by503  have hsm (I : Ideal R) (r : R) : pi • Ideal.Quotient.mk I r =504      Ideal.Quotient.mk I (algebraMap O _ pi * r) :=505    congrArg (Ideal.Quotient.mk I) (Algebra.smul_def pi r)506  obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective m507  change Ideal.Quotient.mk _ r = 0 ↔ _508  rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_pair]509  constructor510  · rintro ⟨α, g, hr⟩511    refine ⟨Ideal.Quotient.mk _ α, ?_⟩512    rw [hsm, Ideal.Quotient.eq, ← hr]513    exact Ideal.mem_span_singleton.mpr ⟨g, by ring⟩514  · rintro ⟨w, hw⟩515    obtain ⟨α, rfl⟩ := Ideal.Quotient.mk_surjective w516    rw [hsm, Ideal.Quotient.eq, Ideal.mem_span_singleton'] at hw517    obtain ⟨g, hg⟩ := hw518    exact ⟨α, g, by rw [hg]; ring⟩519 520/-- For `f` regular modulo `π`, the curve ring `R/(f)` is free over `O` of rank521equal to the length of `R/(π, f)`. -/522theorem concrete_surface_curve_free_of_length (O : Type) [CommRing O] [IsDomain O]Lemma 2.1523    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (pi : O)524    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)525    (f : ConcreteSurface O pi u a b)526    (hf : Function.Injective527      (fun w : ConcreteSurface O pi u a b ⧸ Ideal.span528      {algebraMap O (ConcreteSurface O pi u a b) pi} => Ideal.Quotient.mk529      (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi}) f * w)) (N : ℕ)530    (hN : Module.length (ConcreteSurface O pi u a b)531      (ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi, f}) =532      N) :533    Module.Free O (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) ∧ Module.Finite O534      (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) ∧ Module.finrank O535      (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) = N := by536  have : IsLocalRing (ConcreteSurface O pi u a b) :=537      concrete_surface_isLocalRing O pi u a b hpi.not_isUnit ha538  obtain ⟨e, he⟩ := concrete_surface_residueField_equiv O pi hpi u a b ha539  have hsurj : ∀ r : (ConcreteSurface O pi u a b), ∃ c : O,540      r - algebraMap O (ConcreteSurface O pi u a b) c ∈ IsLocalRing.maximalIdeal541      (ConcreteSurface O pi u a b) := by542    intro r543    obtain ⟨k, hk⟩ := e.surjective (IsLocalRing.residue (ConcreteSurface O pi u a b) r)544    obtain ⟨c, rfl⟩ := IsLocalRing.residue_surjective k545    exact ⟨c, by rw [← IsLocalRing.residue_eq_zero_iff, map_sub, ← he, hk, sub_self]⟩546  have hker : ∀ c : O,547      algebraMap O (ConcreteSurface O pi u a b) c ∈ IsLocalRing.maximalIdeal548      (ConcreteSurface O pi u a b) → pi ∣ c := by549    intro c hc550    rwa [← IsLocalRing.residue_eq_zero_iff, ← he, map_eq_zero_iff e e.injective,551      IsLocalRing.residue_eq_zero_iff, hpi.maximalIdeal_eq, Ideal.mem_span_singleton] at hc552  have hsm : ∀ (I : Ideal (ConcreteSurface O pi u a b)) (r : ConcreteSurface O pi u a b),553      pi • Ideal.Quotient.mk I r = Ideal.Quotient.mk I (algebraMap O _ pi * r) :=554    fun I r ↦ congrArg (Ideal.Quotient.mk I) (Algebra.smul_def pi r)555  have hpiM : ∀ m :556      (ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi, f}),557      pi • m = 0 := by558    intro m559    obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective m560    rw [hsm, Ideal.Quotient.eq_zero_iff_mem]561    exact Ideal.mul_mem_right _ _ (Ideal.subset_span (Set.mem_insert _ _))562  obtain ⟨γ, hγ⟩ := residue_basis_family_of_length O (ConcreteSurface O pi u a b)563      ((ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi, f}))564      pi hsurj hker hpiM N hN565  have hle : Ideal.span {f} ≤ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi, f} :=566      Ideal.span_mono (by simp)567  let q : ((ConcreteSurface O pi u a b) ⧸ Ideal.span {f}) →ₗ[O]568      ((ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi, f}))569      := (Ideal.Quotient.factorₐ O hle).toLinearMap570  have hq : Function.Surjective q := Ideal.Quotient.factor_surjective hle571  obtain ⟨β₀, -, hβ₀⟩ :=572    residue_basis_family_lift_along_reduction O ((ConcreteSurface O pi u a b) ⧸ Ideal.span {f})573        ((ConcreteSurface O pi u a b ⧸ Ideal.span574          {algebraMap O (ConcreteSurface O pi u a b) pi, f})) pi q hq575          (factor_span_pair_eq_zero_iff pi f hle) γ hγ576  choose β hβ using fun i ↦ Ideal.Quotient.mk_surjective (β₀ i)577  have hfun : (fun i ↦ Ideal.Quotient.mk (Ideal.span {f}) (β i)) = β₀ := funext hβ578  exact concrete_surface_curve_free_finrank O pi hpi u a b ha f hf β (hfun ▸ hβ₀)579 580/-! ### Evaluation on completed charts -/581 582/-- Elements of `P` map into the maximal ideal of the completion at `P`. -/583private theorem completedPointMap_mem_maximalIdeal (A : Type) [CommRing A] [IsNoetherianRing A]584    (P : Ideal A) [P.IsPrime] (x : A) (hx : x ∈ P) :585    completedPointMap A P x ∈ IsLocalRing.maximalIdeal (CompletedLocalAt A P) := by586  have h1 : algebraMap A (Localization.AtPrime P) x ∈587      IsLocalRing.maximalIdeal (Localization.AtPrime P) := by588    rw [← IsLocalization.AtPrime.map_eq_maximalIdeal P (Localization.AtPrime P)]589    exact Ideal.mem_map_of_mem _ hx590  rw [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff] at h1 ⊢591  intro hu592  exact h1 ((isUnit_map_iff (algebraMap (Localization.AtPrime P)593    (AdicCompletion (IsLocalRing.maximalIdeal (Localization.AtPrime P))594      (Localization.AtPrime P))) _).mp hu)595 596/-- Elements of `I` are nilpotent modulo `I ^ n`. -/597private theorem isNilpotent_mk_pow_of_mem (S : Type) [CommRing S] (I : Ideal S) (n : ℕ) (y : S)598    (hy : y ∈ I) : IsNilpotent (Ideal.Quotient.mk (I ^ n) y) :=599  ⟨n, by rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]; exact Ideal.pow_mem_pow hy n⟩600 601/-- General form of `child_series_eval_comp_chart_subst` for an arbitrary quotient map602`sm : O[[T,X]] → R`. -/603private theorem eval_comp_chart_eq (O O' R : Type) [CommRing O] [CommRing O'] [CommRing R]604    (sm : TwoSeries O →+* R) (E F : TwoSeries O)605    (hEF : (E = axisT O ∧ F = axisX O) ∨ (E = axisX O ∧ F = axisT O))606    (P : Ideal (BlowupChart R (sm E) (sm F))) [P.IsPrime]607    [IsNoetherianRing (BlowupChart R (sm E) (sm F))]608    (hE : chartBase R (sm E) (sm F) (sm E) ∈ P) (hF : chartBase R (sm E) (sm F) (sm F) ∈ P)609    (ρ : O →+* O') (α : O') (s : TwoSeries O →+* TwoSeries O')610    (hsC : ∀ c : O, s (MvPowerSeries.C c) = MvPowerSeries.C (ρ c)) (hsE : s E = axisT O')611    (hsF : s F = axisT O' * (axisX O' + MvPowerSeries.C α))612    (κ : O' →+* CompletedLocalAt (BlowupChart R (sm E) (sm F)) P)613    (hκ : ∀ c : O, κ (ρ c) = completedPointMap (BlowupChart R (sm E) (sm F)) P614      (chartBase R (sm E) (sm F) (sm (MvPowerSeries.C c))))615    (Θ : TwoSeries O' →+* CompletedLocalAt (BlowupChart R (sm E) (sm F)) P)616    (hΘC : ∀ c : O', Θ (MvPowerSeries.C c) = κ c)617    (hΘT : Θ (axisT O') = completedPointMap (BlowupChart R (sm E) (sm F)) P618      (chartBase R (sm E) (sm F) (sm E)))619    (hΘX : Θ (axisX O') = completedPointMap (BlowupChart R (sm E) (sm F)) P620      (chartSlope R (sm E) (sm F)) - κ α) :621    Θ.comp s = (completedPointMap (BlowupChart R (sm E) (sm F)) P).comp622      ((chartBase R (sm E) (sm F)).comp sm) := by623  set A := BlowupChart R (sm E) (sm F)624  set cb := chartBase R (sm E) (sm F)625  set cp := completedPointMap A P626  set m := IsLocalRing.maximalIdeal (CompletedLocalAt A P)627  have gC (c : O) : Θ (s (.C c)) = cp (cb (sm (.C c))) := by rw [hsC, hΘC, hκ]628  have gE : Θ (s E) = cp (cb (sm E)) := by rw [hsE, hΘT]629  have gF : Θ (s F) = cp (cb (sm F)) := by630    rw [hsF, map_mul, map_add, hΘT, hΘX, hΘC, sub_add_cancel, ← map_mul, blowup_chart_relation]631  -- the variables `T, X` are `E, F` in some order632  have hG (G : TwoSeries O) (hG : G = E ∨ G = F) :633      Θ (s G) = cp (cb (sm G)) ∧ cp (cb (sm G)) ∈ m := by634    rcases hG with rfl | rfl635    exacts [⟨gE, completedPointMap_mem_maximalIdeal A P _ hE⟩,636      ⟨gF, completedPointMap_mem_maximalIdeal A P _ hF⟩]637  obtain ⟨gT, nT⟩ := hG (axisT O) (by rcases hEF with ⟨h1, h2⟩ | ⟨h1, h2⟩ <;> simp [h1, h2])638  obtain ⟨gX, nX⟩ := hG (axisX O) (by rcases hEF with ⟨h1, h2⟩ | ⟨h1, h2⟩ <;> simp [h1, h2])639  refine DFunLike.coe_injective (IsHausdorff.funext' m fun n r ↦ ?_)640  have key := twoSeries_ringHom_ext_of_isNilpotent O _641    ((Ideal.Quotient.mk (m ^ n)).comp (Θ.comp s))642    ((Ideal.Quotient.mk (m ^ n)).comp (cp.comp (cb.comp sm))) (fun c ↦ congrArg _ (gC c))643    (congrArg _ gT) (congrArg _ gX)644    (by simpa only [RingHom.comp_apply, gT] using isNilpotent_mk_pow_of_mem _ m n _ nT)645    (by simpa only [RingHom.comp_apply, gX] using isNilpotent_mk_pow_of_mem _ m n _ nX)646  exact congrArg (· r) key647 648/-- The evaluation `Θ` of the child power series, composed with the chart substitution `s`,649agrees with the canonical map from `O[[T,X]]` through the chart to its completion at `P`. -/650theorem child_series_eval_comp_chart_subst (O O' : Type) [CommRing O] [IsNoetherianRing O]651    [CommRing O'] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) (E F : TwoSeries O)652    (hEF : (E = axisT O ∧ F = axisX O) ∨ (E = axisX O ∧ F = axisT O))653    (P : Ideal654      (BlowupChart (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F)))655    [P.IsPrime]656    (hE : chartBase (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F)657      (surfaceMk O pi u a b E) ∈ P)658    (hF : chartBase (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F)659      (surfaceMk O pi u a b F) ∈ P) (ρ : O →+* O') (α : O') (s : TwoSeries O →+* TwoSeries O')660    (hsC : ∀ c : O, s (MvPowerSeries.C c) = MvPowerSeries.C (ρ c)) (hsE : s E = axisT O')661    (hsF : s F = axisT O' * (axisX O' + MvPowerSeries.C α))662    (κ : O' →+* CompletedLocalAt663      (BlowupChart (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F))664      P) (hκ : ∀ c : O,665      κ (ρ c) = completedPointMap666      (BlowupChart (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F)) P667      (chartBase (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F)668      (algebraMap O (ConcreteSurface O pi u a b) c)))669    (Θ : TwoSeries O' →+* CompletedLocalAt670      (BlowupChart (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F))671      P) (hΘC : ∀ c : O', Θ (MvPowerSeries.C c) = κ c)672    (hΘT : Θ (axisT O') = completedPointMap673      (BlowupChart (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F)) P674      (chartBase (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F)675      (surfaceMk O pi u a b E)))676    (hΘX : Θ (axisX O') = completedPointMap677      (BlowupChart (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F)) P678      (chartSlope (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F))679      - κ α) :680    Θ.comp s =681      (completedPointMap682        (BlowupChart (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E) (surfaceMk O pi u a b F))683        P).comp ((chartBase (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E)684        (surfaceMk O pi u a b F)).comp (surfaceMk O pi u a b)) := by685  have : IsNoetherianRing (BlowupChart (ConcreteSurface O pi u a b) (surfaceMk O pi u a b E)686      (surfaceMk O pi u a b F)) :=687    blowupChart_concrete_isNoetherianRing O pi u a b _ _688  exact eval_comp_chart_eq O O' _ (surfaceMk O pi u a b) E F hEF P hE hF ρ α s hsC hsE hsF κ689    (fun c ↦ (hκ c).trans rfl) Θ hΘC hΘT hΘX690 691end SurfaceBlowup