Power series, residue bases and the local structure of concrete surfaces

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.Formula.LawAlgebra7import SurfaceBlowup.Surfaces.Lengths8 9/-!10# Power series, residue bases and the local structure of concrete surfaces11 12Commutative algebra of the power series rings `A[[T,X]]` and `k[[X]]` used to analyse the13concrete surfaces `O[[T,X]]/(π - u T^a X^b)` over a discrete valuation ring `O` with residue14field `k`: the ideal `(T, X)` and regular elements of `A[[T,X]]`, kernels of the reduction maps,15lengths of quotients of `k[[X]]`, residue basis families (bases modulo `π` lifting to bases), and16the local structure of the concrete surface (maximal ideal `(t, x)`, residue field, special fiber).17 18## Main results19 20* `mvPowerSeries_fin_two_mem_variableIdeal_iff`,21  `mvPowerSeries_fin_two_quotient_var_regular_mod_var`: the ideal `(T, X)` and regular sequences22  in `A[[T,X]]`.23* `powerSeries_quotient_length_eq_order`: `ℓ(k[[X]]/(g)) = ord g`.24* `residue_basis_family_of_length`, `residue_basis_family_basis`: residue basis families.25* `concrete_surface_special_fiber_equiv`, `concrete_surface_maximalIdeal_eq`,26  `concrete_surface_isLocalRing`, `concrete_surface_base_injective`: structure of the concrete27  surface.28 29Provenance: the `Thm_SurfaceBlowupV2_*` nodes named after the theorems of this file.30-/31 32noncomputable section33 34namespace SurfaceBlowup35 36/-! ### Power series in two variables -/37 38private theorem mvPowerSeries_X_ne_zero {σ A : Type} [CommRing A] [Nontrivial A] (s : σ) :39    (MvPowerSeries.X s : MvPowerSeries σ A) ≠ 0 := fun h ↦ by40  simpa [h] using MvPowerSeries.coeff_index_single_self_X (R := A) s41 42/-- A series lies in `(T^a X^b)` iff its coefficients vanish outside the quadrant43`a ≤ m 0, b ≤ m 1`. -/44theorem monomialIdeal_mem_iff (k : Type) [CommRing k] (a b : ℕ) (φ : TwoSeries k) :45    φ ∈ monomialIdeal k a b ↔ ∀ m : Fin 2 →₀ ℕ, ¬(a ≤ m 0 ∧ b ≤ m 1) →46    MvPowerSeries.coeff m φ = 0 := by47  set n₀ : Fin 2 →₀ ℕ := Finsupp.single 0 a + Finsupp.single 1 b with hn₀48  have hgen : axisT k ^ a * axisX k ^ b = MvPowerSeries.monomial n₀ (1 : k) := by49    simp only [axisT, axisX, MvPowerSeries.X_pow_eq, MvPowerSeries.monomial_mul_monomial, one_mul,50      hn₀]51  have hle : ∀ m : Fin 2 →₀ ℕ, n₀ ≤ m ↔ (a ≤ m 0 ∧ b ≤ m 1) := by52    intro m53    rw [Finsupp.le_def, Fin.forall_fin_two]54    simp [hn₀]55  unfold monomialIdeal56  rw [hgen, Ideal.mem_span_singleton]57  constructor58  · rintro ⟨ψ, rfl⟩ m hm59    rw [MvPowerSeries.coeff_monomial_mul, if_neg (by rwa [hle])]60  · intro h61    obtain ⟨ψ, hψ⟩ : ∃ ψ : MvPowerSeries (Fin 2) k,62        ∀ m, MvPowerSeries.coeff m ψ = MvPowerSeries.coeff (m + n₀) φ :=63      ⟨fun m ↦ MvPowerSeries.coeff (m + n₀) φ, fun m ↦ rfl⟩64    refine ⟨ψ, ?_⟩65    ext m66    rw [MvPowerSeries.coeff_monomial_mul, one_mul]67    split_ifs with hm68    · rw [hψ, tsub_add_cancel_of_le hm]69    · exact h m (by rwa [hle] at hm)70 71/-- A two-variable series lies in `(X 0, X 1)` iff its constant coefficient vanishes. -/72theorem mvPowerSeries_fin_two_mem_variableIdeal_iff (A : Type) [CommRing A]73    (g : MvPowerSeries (Fin 2) A) :74    g ∈ Ideal.span {(MvPowerSeries.X 0 : MvPowerSeries (Fin 2) A), MvPowerSeries.X 1} ↔75    MvPowerSeries.constantCoeff g = 0 := by76  refine (pow_one (Ideal.span {axisT A, axisX A}) ▸ axis_ideal_pow_mem_iff A 1 g).trans77    ⟨fun h ↦ h 0 (by simp), fun h m hm ↦ ?_⟩78  obtain rfl : m = 0 := by ext i; fin_cases i <;> simp <;> omega79  exact h80 81/-- A two-variable series with zero constant coefficient splits as `X t * h₁ + X s * q`. -/82private theorem mvPowerSeries_fin_two_split_of_constantCoeff_zero (A : Type) [CommRing A]83    (s t : Fin 2)84    (hst : s ≠ t) (h : MvPowerSeries (Fin 2) A) (h0 : MvPowerSeries.constantCoeff h = 0) :85    ∃ h₁ q : MvPowerSeries (Fin 2) A, h = MvPowerSeries.X t * h₁ + MvPowerSeries.X s * q := by86  obtain ⟨a, b, rfl⟩ :=87    Ideal.mem_span_pair.mp ((mvPowerSeries_fin_two_mem_variableIdeal_iff A h).2 h0)88  obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ : s = 0 ∧ t = 1 ∨ s = 1 ∧ t = 0 := by omega89  exacts [⟨b, a, by ring⟩, ⟨a, b, by ring⟩]90 91/-- The kernel of `O[[T,X]] → O → k` (constant coefficient, then residue) is `(π, T, X)`. -/92private theorem constantCoeff_residue_ker (O : Type) [CommRing O] [IsDomain O]93    [IsDiscreteValuationRing O]94    (pi : O) (hpi : Irreducible pi) :95    RingHom.ker ((IsLocalRing.residue O).comp (MvPowerSeries.constantCoeff : TwoSeries O →+* O)) =96    Ideal.span {(MvPowerSeries.C pi : TwoSeries O), axisT O, axisX O} := by97  have key : ∀ g : TwoSeries O,98      g ∈ RingHom.ker99          ((IsLocalRing.residue O).comp (MvPowerSeries.constantCoeff : TwoSeries O →+* O)) ↔100        pi ∣ MvPowerSeries.constantCoeff g := by101    intro g102    rw [RingHom.mem_ker, RingHom.comp_apply, IsLocalRing.residue_eq_zero_iff, hpi.maximalIdeal_eq,103      Ideal.mem_span_singleton]104  ext g105  rw [key]106  constructor107  · rintro ⟨c, hc⟩108    have h2 : g - MvPowerSeries.C (pi * c) ∈109        Ideal.span {(MvPowerSeries.X 0 : MvPowerSeries (Fin 2) O), MvPowerSeries.X 1} := by110      rw [mvPowerSeries_fin_two_mem_variableIdeal_iff]111      simp [hc]112    have h3 : g = MvPowerSeries.C pi * MvPowerSeries.C c + (g - MvPowerSeries.C (pi * c)) := by113      rw [map_mul]; ring114    rw [h3]115    refine Ideal.add_mem _ (Ideal.mul_mem_right _ _ (Ideal.subset_span (by simp))) ?_116    refine Ideal.span_mono (fun y hy ↦ ?_) h2117    rcases hy with rfl | rfl <;> simp [axisT, axisX]118  · intro h119    have : Ideal.span {(MvPowerSeries.C pi : TwoSeries O), axisT O, axisX O} ≤120        RingHom.ker ((IsLocalRing.residue O).comp121          (MvPowerSeries.constantCoeff : TwoSeries O →+* O)) := by122      rw [Ideal.span_le]123      intro y hy124      simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hy125      rw [SetLike.mem_coe, key]126      rcases hy with rfl | rfl | rfl <;> simp [axisT, axisX]127    exact (key g).1 (this h)128 129/-- If the constant coefficient of `P` is a nonzerodivisor and `X s ∣ P * h`, then `X s ∣ h`. -/130private theorem mvPowerSeries_var_dvd_of_var_dvd_mul (σ A : Type) [CommRing A] (s : σ)131    (P h : MvPowerSeries σ A) (hP : MvPowerSeries.constantCoeff P ∈ nonZeroDivisors A)132    (hdvd : (MvPowerSeries.X s : MvPowerSeries σ A) ∣ P * h) :133    (MvPowerSeries.X s : MvPowerSeries σ A) ∣ h := by134  classical135  rw [MvPowerSeries.X_dvd_iff] at hdvd ⊢136  intro m137  induction m using WellFoundedLT.induction with138  | _ e he =>139  intro hes140  have key := hdvd e hes141  rw [MvPowerSeries.coeff_mul, Finset.sum_eq_single (0, e),142    MvPowerSeries.coeff_zero_eq_constantCoeff] at key143  · exact (mem_nonZeroDivisors_iff_left.mp hP) _ key144  · rintro ⟨u, v⟩ huv hne145    have hsum : u + v = e := Finset.HasAntidiagonal.mem_antidiagonal.mp huv146    have hu : u ≠ 0 := by147      rintro rfl148      simp_all149    have hlt : v < e := lt_of_le_of_ne (hsum ▸ le_add_self) fun hve ↦150      hu (add_eq_right.mp (hsum.trans hve.symm))151    have hvs : v s = 0 := by152      have := DFunLike.congr_fun hsum s153      simp only [Finsupp.add_apply] at this154      omega155    simp [he v hlt hvs]156  · simp157 158/-- If `P` has nonzero constant coefficient over a domain, then `X s` is a nonzerodivisor159modulo `P`. -/160theorem mvPowerSeries_quotient_var_regular (σ A : Type) [CommRing A] [IsDomain A] (s : σ)161    (P : MvPowerSeries σ A) (hP : MvPowerSeries.constantCoeff P ≠ 0) :162    Function.Injective163    (fun g : MvPowerSeries σ A ⧸ Ideal.span {P} ↦ Ideal.Quotient.mk (Ideal.span {P})164      (MvPowerSeries.X s) * g) := by165  intro a b hab166  obtain ⟨g, rfl⟩ := Ideal.Quotient.mk_surjective a167  obtain ⟨g', rfl⟩ := Ideal.Quotient.mk_surjective b168  simp only [← map_mul] at hab169  rw [Ideal.Quotient.eq, Ideal.mem_span_singleton, ← mul_sub] at hab170  rw [Ideal.Quotient.eq, Ideal.mem_span_singleton]171  obtain ⟨h, hh⟩ := hab172  have hX : (MvPowerSeries.X s : MvPowerSeries σ A) ∣ P * h := ⟨g - g', hh.symm⟩173  obtain ⟨h1, rfl⟩ := mvPowerSeries_var_dvd_of_var_dvd_mul σ A s P h174    (mem_nonZeroDivisors_of_ne_zero hP) hX175  exact ⟨h1, mul_left_cancel₀ (mvPowerSeries_X_ne_zero s) (by rw [hh]; ring)⟩176 177/-- For distinct variables, `X t ∣ X s * w` implies `X t ∣ w`. -/178private theorem mvPowerSeries_var_dvd_of_var_dvd_other_var_mul (σ A : Type) [CommRing A] (s t : σ)179    (hst : s ≠ t) (w : MvPowerSeries σ A)180    (hdvd : (MvPowerSeries.X t : MvPowerSeries σ A) ∣ MvPowerSeries.X s * w) :181    (MvPowerSeries.X t : MvPowerSeries σ A) ∣ w := by182  rw [MvPowerSeries.X_dvd_iff] at hdvd ⊢183  intro m hm184  have h := hdvd (m + Finsupp.single s 1) (by simp [hm, Finsupp.single_eq_of_ne hst.symm])185  rw [MvPowerSeries.X, MvPowerSeries.coeff_monomial_mul] at h186  simpa using h187 188/-- If `P` has nonzero constant coefficient over a domain, then `X t` is a nonzerodivisor189modulo `(P, X s)` for `s ≠ t`. -/190theorem mvPowerSeries_fin_two_quotient_var_regular_mod_var (A : Type) [CommRing A] [IsDomain A]191    (s t : Fin 2) (hst : s ≠ t) (P : MvPowerSeries (Fin 2) A)192    (hP : MvPowerSeries.constantCoeff P ≠ 0) :193    Function.Injective194    (fun g : (MvPowerSeries (Fin 2) A ⧸ Ideal.span {P}) ⧸ Ideal.span195      {Ideal.Quotient.mk (Ideal.span {P}) (MvPowerSeries.X s)} => Ideal.Quotient.mk196      (Ideal.span {Ideal.Quotient.mk (Ideal.span {P}) (MvPowerSeries.X s)})197      (Ideal.Quotient.mk (Ideal.span {P}) (MvPowerSeries.X t)) * g) := by198  set I := Ideal.span {P}199  set J := Ideal.span {Ideal.Quotient.mk I (MvPowerSeries.X s)}200  -- key: kernel is zero201  have key : ∀ g : MvPowerSeries (Fin 2) A,202      Ideal.Quotient.mk J (Ideal.Quotient.mk I (MvPowerSeries.X t * g)) = 0 →203      Ideal.Quotient.mk J (Ideal.Quotient.mk I g) = 0 := by204    intro g hg205    rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton'] at hg206    obtain ⟨r', hr'⟩ := hg207    obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r'208    rw [← map_mul, Ideal.Quotient.eq, Ideal.mem_span_singleton'] at hr'209    obtain ⟨h, hh⟩ := hr'210    -- h * P = r * X s - X t * g211    have h0 : MvPowerSeries.constantCoeff h = 0 := by212      simpa [MvPowerSeries.constantCoeff_X, hP] using congrArg MvPowerSeries.constantCoeff hh213    obtain ⟨h₁, q, rfl⟩ :=214      mvPowerSeries_fin_two_split_of_constantCoeff_zero A s t hst h h0215    have hdvd : (MvPowerSeries.X t : MvPowerSeries (Fin 2) A) ∣216        MvPowerSeries.X s * (P * q - r) :=217      ⟨-(g + P * h₁), by linear_combination hh⟩218    obtain ⟨w, hw⟩ :=219      mvPowerSeries_var_dvd_of_var_dvd_other_var_mul (Fin 2) A s t hst _ hdvd220    have hg : g = P * (-h₁) + MvPowerSeries.X s * (-w) := by221      apply mul_left_cancel₀ (mvPowerSeries_X_ne_zero t)222      linear_combination hh - MvPowerSeries.X s * hw223    rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton']224    refine ⟨Ideal.Quotient.mk I (-w), ?_⟩225    rw [← map_mul, Ideal.Quotient.eq, Ideal.mem_span_singleton']226    exact ⟨h₁, by rw [hg]; ring⟩227  intro a b hab228  obtain ⟨a', rfl⟩ := Ideal.Quotient.mk_surjective a229  obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective a'230  obtain ⟨b', rfl⟩ := Ideal.Quotient.mk_surjective b231  obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective b'232  simp only at hab233  rw [← sub_eq_zero] at hab ⊢234  rw [← map_sub, ← map_sub]235  apply key236  rw [map_mul, map_mul, map_sub, map_sub]237  linear_combination hab238 239/-- Values of `nilpotentEval` on constants and on the two variables. -/240theorem nilpotentEval_apply_generators (O S : Type) [CommRing O] [CommRing S] (φ : O →+* S)241    (e z : S) (he : IsNilpotent e) (hz : IsNilpotent z) :242    (∀ c : O, nilpotentEval φ e z he hz (MvPowerSeries.C c) = φ c) ∧243    nilpotentEval φ e z he hz (axisT O) = e ∧ nilpotentEval φ e z he hz (axisX O) = z := by244  refine ⟨fun c ↦ ?_, ?_, ?_⟩245  · simp [nilpotentEval, MvPowerSeries.map_C]246  · simp only [nilpotentEval, AlgHom.toRingHom_eq_coe, axisT, RingHom.coe_comp, RingHom.coe_coe,247      MvPowerSeries.coe_substAlgHom, Function.comp_apply, MvPowerSeries.map_X]248    rw [MvPowerSeries.subst_X (nilpotentFamily_hasSubst e z he hz)]249    simp [nilpotentFamily]250  · simp only [nilpotentEval, AlgHom.toRingHom_eq_coe, axisX, RingHom.coe_comp, RingHom.coe_coe,251      MvPowerSeries.coe_substAlgHom, Function.comp_apply, MvPowerSeries.map_X]252    rw [MvPowerSeries.subst_X (nilpotentFamily_hasSubst e z he hz)]253    simp [nilpotentFamily]254 255/-- The kernel of coefficient reduction `O[[T,X]] → k[[T,X]]` is `(π)`. -/256private theorem residueSeries_ker (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]257    (pi : O)258    (hpi : Irreducible pi) :259    RingHom.ker (residueSeries O) = Ideal.span {(MvPowerSeries.C pi : TwoSeries O)} := by260  have key : ∀ g : TwoSeries O, residueSeries O g = 0 ↔ ∀ m, pi ∣ MvPowerSeries.coeff m g := by261    intro g262    unfold residueSeries263    rw [MvPowerSeries.ext_iff]264    refine forall_congr' fun m ↦ ?_265    rw [MvPowerSeries.coeff_map, map_zero, IsLocalRing.residue_eq_zero_iff,266      hpi.maximalIdeal_eq, Ideal.mem_span_singleton]267  ext g268  rw [RingHom.mem_ker, key, Ideal.mem_span_singleton]269  constructor270  · intro h271    choose q hq using h272    let Q : TwoSeries O := q273    refine ⟨Q, ?_⟩274    ext m275    rw [MvPowerSeries.coeff_C_mul, hq m]276    rfl277  · rintro ⟨q, rfl⟩ m278    rw [MvPowerSeries.coeff_C_mul]279    exact dvd_mul_right _ _280 281/-- Coefficient reduction `O[[T,X]] → k[[T,X]]` is surjective. -/282private theorem residueSeries_surjective (O : Type) [CommRing O] [IsLocalRing O] :283    Function.Surjective (residueSeries O) := by284  intro ψ285  refine ⟨fun m ↦286    Classical.choose (IsLocalRing.residue_surjective (R := O) (MvPowerSeries.coeff m ψ)), ?_⟩287  ext m288  have := Classical.choose_spec (IsLocalRing.residue_surjective (R := O) (MvPowerSeries.coeff m ψ))289  exact (MvPowerSeries.coeff_map (IsLocalRing.residue O) m _).trans this290 291/-- The kernel of `O[[T,X]] → k[[T,X]]/(T^a X^b)` is `(π, T^a X^b)`. -/292private theorem residueSeries_comp_monomial_ker (O : Type) [CommRing O] [IsDomain O]293    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (a b : ℕ) :294    RingHom.ker295    ((Ideal.Quotient.mk (monomialIdeal (IsLocalRing.ResidueField O) a b)).comp (residueSeries O)) =296    Ideal.span {(MvPowerSeries.C pi : TwoSeries O), axisT O ^ a * axisX O ^ b} := by297  have hker := residueSeries_ker O pi hpi298  have hmono : residueSeries O (axisT O ^ a * axisX O ^ b) =299      axisT (IsLocalRing.ResidueField O) ^ a * axisX (IsLocalRing.ResidueField O) ^ b := by300    simp [residueSeries, axisT, axisX, MvPowerSeries.map_X]301  ext g302  rw [RingHom.mem_ker, RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem, monomialIdeal,303    Ideal.mem_span_singleton', Ideal.mem_span_pair]304  constructor305  · rintro ⟨ψ, hψ⟩306    obtain ⟨q, hq⟩ := residueSeries_surjective O ψ307    have h0 : g - q * (axisT O ^ a * axisX O ^ b) ∈ RingHom.ker (residueSeries O) := by308      rw [RingHom.mem_ker, map_sub, map_mul, hq, hmono, ← hψ, mul_comm, sub_self]309    rw [hker, Ideal.mem_span_singleton'] at h0310    obtain ⟨c, hc⟩ := h0311    exact ⟨c, q, by rw [hc]; ring⟩312  · rintro ⟨c, q, hcq⟩313    refine ⟨residueSeries O q, ?_⟩314    have h1 : residueSeries O (MvPowerSeries.C pi) = 0 := by315      rw [← RingHom.mem_ker, hker]; exact Ideal.subset_span rfl316    rw [← hcq, map_add, map_mul, map_mul, h1, hmono]; ring317 318private theorem coeff_killT (O : Type) [CommRing O] (g : TwoSeries O) (n : ℕ) :319    PowerSeries.coeff n (killT O g) = MvPowerSeries.coeff (Finsupp.single 1 n) g :=320  coeff_substAlgHom_kill O _ (killTFamily_hasSubst O) 0 1 (by decide) rfl rfl g n321 322private theorem coeff_residueKillT (O : Type) [CommRing O] [IsLocalRing O] (g : TwoSeries O)323    (n : ℕ) :324    PowerSeries.coeff n (residueKillT O g) =325      IsLocalRing.residue O (MvPowerSeries.coeff (Finsupp.single 1 n) g) := by326  rw [← coeff_killT]327  rfl328 329/-- Values of `residueKillT` on generators; it is surjective with kernel `(π, T)`. -/330theorem residueKillT_apply_ker (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]331    (pi : O) (hpi : Irreducible pi) :332    (∀ c : O, residueKillT O (MvPowerSeries.C c) = PowerSeries.C (IsLocalRing.residue O c)) ∧333    residueKillT O (axisT O) = 0 ∧ residueKillT O (axisX O) = PowerSeries.X ∧334    Function.Surjective (residueKillT O) ∧335    RingHom.ker (residueKillT O) = Ideal.span {MvPowerSeries.C pi, axisT O} := by336  refine ⟨fun c ↦ ?_, ?_, ?_, ?_, ?_⟩337  · ext n338    rw [coeff_residueKillT]339    by_cases hn : n = 0340    · subst hn; simp [MvPowerSeries.coeff_C]341    · simp [MvPowerSeries.coeff_C, PowerSeries.coeff_C, hn]342  · ext n343    rw [coeff_residueKillT]344    simp [axisT, MvPowerSeries.coeff_X, Finsupp.single_eq_single_iff]345  · ext n346    rw [coeff_residueKillT]347    by_cases hn : n = 1348    · subst hn; simp [axisX, MvPowerSeries.coeff_X]349    · simp [axisX, MvPowerSeries.coeff_X, PowerSeries.coeff_X, hn, Finsupp.single_eq_single_iff]350  · intro h351    let g : TwoSeries O := fun m ↦352      if m 0 = 0 then (IsLocalRing.residue_surjective (PowerSeries.coeff (m 1) h)).choose else 0353    refine ⟨g, ?_⟩354    ext n355    rw [coeff_residueKillT]356    change IsLocalRing.residue O (if _ then _ else _) = _357    simp only [Finsupp.single_apply, one_ne_zero, ↓reduceIte]358    exact (IsLocalRing.residue_surjective (PowerSeries.coeff n h)).choose_spec359  · ext g360    rw [RingHom.mem_ker, axisT, mvPowerSeries_mem_span_C_var_iff]361    have hm : ∀ x : O, IsLocalRing.residue O x = 0 ↔ pi ∣ x := by362      intro x363      rw [IsLocalRing.residue_eq_zero_iff, hpi.maximalIdeal_eq, Ideal.mem_span_singleton]364    constructor365    · intro hg m hm0366      have := congrArg (PowerSeries.coeff (m 1)) hg367      rw [coeff_residueKillT, map_zero, hm] at this368      have hmeq : Finsupp.single 1 (m 1) = m := by369        ext i; fin_cases i <;> simp [hm0]370      rwa [hmeq] at this371    · intro hg372      ext n373      rw [coeff_residueKillT, map_zero, hm]374      exact hg _ (by simp)375 376/-! ### One-variable power series and polynomials -/377 378/-- The point-count expression evaluates to `(1/δ) ∑_{j ∣ δ} μ(j) q^(δ/j)`. -/379theorem pointCount_eval (δ : ℕ) (q : ℚ) :380    (pointCount δ).eval q = (1/(δ:ℚ)) * ∑ j ∈ δ.divisors, ((ArithmeticFunction.moebius j : ℤ) : ℚ) *381    q ^ (δ / j) := by382  unfold pointCount383  rw [Expr.eval, Expr.eval, expression_sum_eval, List.map_map]384  congr 1385  rw [← Finset.sum_map_toList]386  congr 1387  apply List.map_congr_left388  intro j _389  simp [Expr.eval, expression_pow_eval]390 391/-- Hensel uniqueness: two roots of `f` congruent modulo the maximal ideal coincide when392`f'(x)` is a unit. -/393theorem polynomial_root_unique_of_derivative_isUnit (S : Type) [CommRing S] [IsLocalRing S]394    (f : Polynomial S) (x y : S) (hx : Polynomial.eval x f = 0) (hy : Polynomial.eval y f = 0)395    (hxy : y - x ∈ IsLocalRing.maximalIdeal S)396    (hd : IsUnit (Polynomial.eval x (Polynomial.derivative f))) :397    y = x := by398  obtain ⟨k, hk⟩ := Polynomial.binomExpansion f x (y - x)399  have hy' : x + (y - x) = y := by ring400  rw [hy', hy, hx] at hk401  have h0 : (y - x) * (Polynomial.eval x (Polynomial.derivative f) + k * (y - x)) = 0 := by402    linear_combination -hk403  have hw : IsUnit (Polynomial.eval x (Polynomial.derivative f) + k * (y - x)) := by404    by_contra hn405    have h := (IsLocalRing.maximalIdeal S).sub_mem ((IsLocalRing.mem_maximalIdeal _).2 hn)406      (Ideal.mul_mem_left _ k hxy)407    exact (IsLocalRing.mem_maximalIdeal _).mp (by rwa [add_sub_cancel_right] at h) hd408  exact sub_eq_zero.mp (hw.mul_left_eq_zero.mp h0)409 410/-- `k[[X]]/(X^r)` has length `r`. -/411private theorem powerSeries_quotient_X_pow_length (k : Type) [Field k] (r : ℕ) :412    Module.length (PowerSeries k) (PowerSeries k ⧸ Ideal.span {(PowerSeries.X : PowerSeries k) ^ r})413    = r := by414  rw [← Ideal.span_singleton_pow, ← PowerSeries.maximalIdeal_eq_span_X]415  exact IsDiscreteValuationRing.length_quotient_pow_maximalIdeal _ r416 417/-- `k[[X]]/(g)` has length equal to the order of `g`, and multiplication by `g` is injective418iff `g ≠ 0`. -/419theorem powerSeries_quotient_length_eq_order (k : Type) [Field k] (g : PowerSeries k) :420    Module.length (PowerSeries k) (PowerSeries k ⧸ Ideal.span {g}) = g.order ∧421    (Function.Injective (fun w : PowerSeries k ↦ g * w) ↔ g ≠ 0) := by422  refine ⟨?_, ?_⟩423  · by_cases hg : g = 0424    · subst hg425      rw [PowerSeries.order_zero]426      refine ENat.eq_top_iff_forall_ge.mpr (fun r ↦ ?_)427      have hle : Ideal.span {(0 : PowerSeries k)} ≤428          Ideal.span {(PowerSeries.X : PowerSeries k) ^ r} := by429        rw [Ideal.span_singleton_le_span_singleton]; exact dvd_zero _430      rw [← powerSeries_quotient_X_pow_length k r]431      exact Module.length_le_of_surjective (Submodule.factor hle) (Submodule.factor_surjective hle)432    · have hu : IsUnit (PowerSeries.divXPowOrder g) := by433        rw [PowerSeries.isUnit_iff_constantCoeff, isUnit_iff_ne_zero]434        exact PowerSeries.constantCoeff_divXPowOrder_eq_zero_iff.not.mpr hg435      have hspan : Ideal.span {g} =436          Ideal.span {(PowerSeries.X : PowerSeries k) ^ g.order.toNat} := by437        conv_lhs => rw [← PowerSeries.X_pow_order_mul_divXPowOrder (f := g)]438        exact Ideal.span_singleton_mul_right_unit hu _439      rw [hspan, powerSeries_quotient_X_pow_length k,440        ENat.natCast_toNat (PowerSeries.order_eq_top.not.mpr hg)]441  · refine ⟨fun h hg ↦ ?_, mul_right_injective₀⟩442    subst hg443    exact one_ne_zero (h (show (0 : PowerSeries k) * 1 = 0 * 0 by simp))444 445/-! ### Residue basis families -/446 447/-- A residue basis family of a quotient `Q` of `M` (with kernel `π M`) lifts to `M`. -/448theorem residue_basis_family_lift_along_reduction (O M Q : Type) [CommRing O] [AddCommGroup M]449    [Module O M] [AddCommGroup Q] [Module O Q] (pi : O) (q : M →ₗ[O] Q) (hq : Function.Surjective q)450    (hkq : ∀ m : M, q m = 0 ↔ ∃ w : M, m = pi • w) {N : ℕ} (γ : Fin N → Q)451    (hγ : ResidueBasisFamily pi γ) :452    ∃ β : Fin N → M, (∀ i, q (β i) = γ i) ∧ ResidueBasisFamily pi β := by453  choose β hβ using fun i ↦ hq (γ i)454  refine ⟨β, hβ, ?_, ?_⟩455  · intro m456    obtain ⟨z, m', h⟩ := hγ.1 (q m)457    obtain ⟨m₀, hm₀⟩ := hq m'458    have h0 : q (m - ((∑ i, z i • β i) + pi • m₀)) = 0 := by459      simp [map_sum, hβ, hm₀, ← h]460    obtain ⟨w, hw⟩ := (hkq _).1 h0461    refine ⟨z, m₀ + w, ?_⟩462    rw [smul_add, ← add_assoc, ← hw]463    abel464  · intro z ⟨w, hw⟩465    apply hγ.2 z466    refine ⟨q w, ?_⟩467    have := congrArg q hw468    simpa [map_sum, hβ] using this469 470/-- Over a `π`-adically separated ring, a residue basis family of a `π`-torsion-free module471is linearly independent. -/472private theorem residue_basis_family_linearIndependent (O M : Type) [CommRing O] [AddCommGroup M]473    [Module O M] (pi : O) [IsHausdorff (Ideal.span {pi}) O] (hreg : ∀ m : M, pi • m = 0 → m = 0)474    {N : ℕ} (β : Fin N → M) (hβ : ResidueBasisFamily pi β) :475    LinearIndependent O β := by476  rw [Fintype.linearIndependent_iff]477  intro g hg478  have hregk : ∀ k : ℕ, ∀ m : M, pi ^ k • m = 0 → m = 0 := by479    intro k480    induction k with481    | zero => intro m h; simpa using h482    | succ k ih =>483      intro m h484      rw [pow_succ, mul_smul] at h485      exact hreg m (ih _ h)486  have key : ∀ k : ℕ, ∀ i, pi ^ k ∣ g i := by487    intro k488    induction k with489    | zero => intro i; simp490    | succ k ih =>491      choose y hy using ih492      have hsum : ∑ i, y i • β i = 0 := by493        apply hregk k494        rw [Finset.smul_sum]495        simp_rw [smul_smul, ← hy]496        exact hg497      have hdiv := hβ.2 y ⟨0, by rw [hsum, smul_zero]⟩498      intro i499      obtain ⟨c, hc⟩ := hdiv i500      exact ⟨c, by rw [hy i, hc, pow_succ, mul_assoc]⟩501  intro i502  apply IsHausdorff.haus (I := Ideal.span {pi}) (M := O) inferInstance503  intro n504  rw [SModEq.zero, smul_eq_mul, Ideal.mul_top, Ideal.span_singleton_pow,505    Ideal.mem_span_singleton]506  exact key n i507 508/-- A residue basis family of `M₁` extends by one vector to `M` when `M/M₁` is simple. -/509private theorem residue_basis_family_of_simple_quotient (O B M : Type) [CommRing O] [CommRing B]510    [IsLocalRing B] [Algebra O B] [AddCommGroup M] [Module B M] [Module O M] [IsScalarTower O B M]511    (pi : O) (hsurj : ∀ b : B, ∃ c : O, b - algebraMap O B c ∈ IsLocalRing.maximalIdeal B)512    (hker : ∀ c : O, algebraMap O B c ∈ IsLocalRing.maximalIdeal B → pi ∣ c)513    (hpiM : ∀ m : M, pi • m = 0) (M₁ : Submodule B M) [IsSimpleModule B (M ⧸ M₁)] {N : ℕ}514    (β : Fin N → M) (hβM₁ : ∀ i, β i ∈ M₁)515    (hβ : ResidueBasisFamily pi (fun i ↦ (⟨β i, hβM₁ i⟩ : M₁))) :516    ∃ γ : Fin (N+1) → M, ResidueBasisFamily pi γ := by517  have : Nontrivial (M ⧸ M₁) := IsSimpleModule.nontrivial B _518  obtain ⟨x, hx⟩ := exists_ne (0 : M ⧸ M₁)519  obtain ⟨v, rfl⟩ := Submodule.Quotient.mk_surjective M₁ x520  have hspan := IsSimpleModule.toSpanSingleton_surjective B hx521  -- the annihilator of `v̄ ∈ M/M₁` is the maximal ideal of `B`522  have hann (b : B) :523      b • (Submodule.Quotient.mk v : M ⧸ M₁) = 0 ↔ b ∈ IsLocalRing.maximalIdeal B := by524    rw [← IsLocalRing.eq_maximalIdeal (IsSimpleModule.ker_toSpanSingleton_isMaximal B hx),525      LinearMap.mem_ker, LinearMap.toSpanSingleton_apply]526  have hOsmul (c : O) (m : M) : c • m = algebraMap O B c • m := (algebraMap_smul B c m).symm527  refine ⟨Fin.snoc β v, ?_, ?_⟩528  · intro m529    obtain ⟨b, hb⟩ := hspan (Submodule.Quotient.mk m)530    rw [LinearMap.toSpanSingleton_apply] at hb531    obtain ⟨c, hc⟩ := hsurj b532    have hmem : m - c • v ∈ M₁ := by533      rw [← Submodule.Quotient.eq, ← hb, hOsmul, Submodule.Quotient.mk_smul, ← sub_eq_zero,534        ← sub_smul]535      exact (hann _).2 hc536    obtain ⟨z, m', hz⟩ := hβ.1 ⟨m - c • v, hmem⟩537    refine ⟨Fin.snoc z c, 0, ?_⟩538    have hz' := congrArg Subtype.val hz539    simp only [Submodule.coe_add, Submodule.coe_sum, Submodule.coe_smul_of_tower] at hz'540    rw [hpiM, add_zero] at hz'541    rw [Fin.sum_univ_castSucc]542    simp [Fin.snoc_castSucc, Fin.snoc_last, hpiM, ← hz']543  · intro z ⟨m', hm'⟩544    rw [Fin.sum_univ_castSucc, hpiM] at hm'545    simp only [Fin.snoc_castSucc, Fin.snoc_last] at hm'546    have hSmem : (∑ i : Fin N, z (Fin.castSucc i) • β i) ∈ M₁ :=547      Submodule.sum_mem _ (fun i _ ↦ Submodule.smul_of_tower_mem _ _ (hβM₁ i))548    have hlast : pi ∣ z (Fin.last N) := by549      refine hker _ ((hann _).1 ?_)550      have h := congrArg (Submodule.Quotient.mk (p := M₁)) hm'551      rw [Submodule.Quotient.mk_add, (Submodule.Quotient.mk_eq_zero M₁).mpr hSmem, zero_add,552        hOsmul, Submodule.Quotient.mk_smul] at h553      simpa using h554    obtain ⟨y, hy⟩ := hlast555    have hv0 : z (Fin.last N) • v = 0 := by556      rw [hy, mul_comm, mul_smul, hpiM, smul_zero]557    rw [hv0, add_zero] at hm'558    have hcast := hβ.2 (fun i ↦ z (Fin.castSucc i)) ⟨0, by559      apply Subtype.ext560      simp only [Submodule.coe_sum, Submodule.coe_smul_of_tower, smul_zero,561        Submodule.coe_zero]562      exact hm'⟩563    exact fun i ↦ Fin.lastCases ⟨y, hy⟩ hcast i564 565/-- A module of length `N` killed by `π` has a residue basis family of size `N`. -/566theorem residue_basis_family_of_length (O B M : Type) [CommRing O] [CommRing B] [IsLocalRing B]567    [Algebra O B] [AddCommGroup M] [Module B M] [Module O M] [IsScalarTower O B M] (pi : O)568    (hsurj : ∀ b : B, ∃ c : O, b - algebraMap O B c ∈ IsLocalRing.maximalIdeal B)569    (hker : ∀ c : O, algebraMap O B c ∈ IsLocalRing.maximalIdeal B → pi ∣ c)570    (hpiM : ∀ m : M, pi • m = 0) (N : ℕ) (hN : Module.length B M = N) :571    ∃ β : Fin N → M, ResidueBasisFamily pi β := by572  induction N generalizing M with573  | zero =>574    have hs : Subsingleton M := Module.length_eq_zero_iff.mp (by simpa using hN)575    refine ⟨Fin.elim0, fun m ↦ ⟨Fin.elim0, 0, Subsingleton.elim _ _⟩, fun z _ i ↦ i.elim0⟩576  | succ n ih =>577    have hfin : IsFiniteLength B M :=578      Module.length_ne_top_iff.mp (by rw [hN]; exact ENat.natCast_ne_top _)579    have hNoeth : IsNoetherian B M := (isFiniteLength_iff_isNoetherian_isArtinian.mp hfin).1580    have hnt : Nontrivial M := Module.length_pos_iff.mp (by rw [hN]; exact_mod_cast Nat.succ_pos n)581    obtain ⟨M₁, hco, -⟩ := (eq_top_or_exists_le_coatom (⊥ : Submodule B M)).resolve_left bot_ne_top582    have : IsSimpleModule B (M ⧸ M₁) := (isSimpleModule_iff_isCoatom).mpr hco583    have hadd := Module.length_eq_add_of_exact M₁.subtype M₁.mkQ M₁.injective_subtype584      M₁.mkQ_surjective (LinearMap.exact_subtype_mkQ M₁)585    rw [Module.length_eq_one B (M ⧸ M₁), hN] at hadd586    have hM₁ : Module.length B M₁ = n := by587      have : Module.length B M₁ ≠ ⊤ := by588        intro h; rw [h] at hadd; simp at hadd589      lift Module.length B M₁ to ℕ using this with k hk590      norm_cast at hadd ⊢591      omega592    obtain ⟨β, hβ⟩ := ih M₁ (fun m ↦ Subtype.ext (by simpa using hpiM m)) hM₁593    exact residue_basis_family_of_simple_quotient O B M pi hsurj hker hpiM M₁594      (fun i ↦ (β i : M)) (fun i ↦ (β i).2) (by simpa using hβ)595 596/-- Over a `π`-adically complete ring, a residue basis family of a separated module spans it. -/597private theorem residue_basis_family_spans (O M : Type) [CommRing O] [AddCommGroup M] [Module O M]598    (pi : O)599    [IsAdicComplete (Ideal.span {pi}) O] [IsHausdorff (Ideal.span {pi}) M] {N : ℕ} (β : Fin N → M)600    (hβ : ResidueBasisFamily pi β) :601    Submodule.span O (Set.range β) = ⊤ := by602  set I : Ideal O := Ideal.span {pi} with hI603  have hpow : ∀ n : ℕ, pi ^ n ∈ I ^ n := fun n ↦604    Ideal.pow_mem_pow (Ideal.mem_span_singleton_self pi) n605  have memO : ∀ (n : ℕ) (y : O), pi ^ n * y ∈ (I ^ n • ⊤ : Submodule O O) := fun n y ↦606    Submodule.smul_mem_smul (hpow n) Submodule.mem_top607  choose zf mf hf using hβ.1608  refine eq_top_iff.mpr fun m _ ↦ ?_609  let seq : ℕ → M := fun n ↦ Nat.rec m (fun _ x ↦ mf x) n610  have seq_succ : ∀ n, seq (n + 1) = mf (seq n) := fun n ↦ rfl611  let z : ℕ → Fin N → O := fun n ↦ zf (seq n)612  let c : ℕ → Fin N → O := fun n i ↦ ∑ j ∈ Finset.range n, pi ^ j * z j i613  have inv : ∀ n, m = (∑ i, c n i • β i) + pi ^ n • seq n := by614    intro n615    induction n with616    | zero => simp [c, seq]617    | succ n ih =>618      rw [ih, hf (seq n), seq_succ]619      simp only [c, Finset.sum_range_succ, add_smul, Finset.sum_add_distrib, smul_add,620        Finset.smul_sum, smul_smul, pow_succ, add_assoc]621      rfl622  have cauchy : ∀ i, ∃ L : O, ∀ n, c n i ≡ L [SMOD (I ^ n • ⊤ : Submodule O O)] := by623    intro i624    refine IsPrecomplete.prec inferInstance ?_625    intro a b hab626    rw [SModEq.sub_mem, ← neg_mem_iff, neg_sub]627    change ∑ j ∈ Finset.range b, pi ^ j * z j i - ∑ j ∈ Finset.range a, pi ^ j * z j i ∈ _628    rw [← Finset.sum_Ico_eq_sub _ hab]629    refine Submodule.sum_mem _ fun j hj ↦ ?_630    obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Finset.mem_Ico.mp hj).1631    rw [pow_add, mul_assoc]632    exact memO a _633  choose L hL using cauchy634  have key : m = ∑ i, L i • β i := by635    rw [← sub_eq_zero]636    refine IsHausdorff.haus (I := I) inferInstance _ fun n ↦ ?_637    rw [SModEq.zero]638    have : m - ∑ i, L i • β i = (∑ i, (c n i - L i) • β i) + pi ^ n • seq n := by639      conv_lhs => rw [inv n]640      simp only [sub_smul, Finset.sum_sub_distrib]641      abel642    rw [this]643    refine Submodule.add_mem _ (Submodule.sum_mem _ fun i _ ↦ ?_)644      (Submodule.smul_mem_smul (hpow n) Submodule.mem_top)645    have h1 := SModEq.sub_mem.mp (hL i n)646    rw [smul_eq_mul, Ideal.mul_top] at h1647    exact Submodule.smul_mem_smul h1 Submodule.mem_top648  rw [key]649  exact Submodule.sum_mem _ fun i _ ↦ Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)650 651/-- A residue basis family of a separated torsion-free module over a complete ring is a basis. -/652theorem residue_basis_family_basis (O M : Type) [CommRing O] [AddCommGroup M] [Module O M] (pi : O)653    [IsAdicComplete (Ideal.span {pi}) O] [IsHausdorff (Ideal.span {pi}) M]654    (hreg : ∀ m : M, pi • m = 0 → m = 0) {N : ℕ} (β : Fin N → M) (hβ : ResidueBasisFamily pi β) :655    ∃ B : Module.Basis (Fin N) O M, ∀ i, B i = β i := by656  have hs := residue_basis_family_spans O M pi β hβ657  exact ⟨.mk (residue_basis_family_linearIndependent O M pi hreg β hβ) (by rw [hs]), by simp⟩658 659/-! ### Concrete surfaces -/660 661/-- In the concrete surface, the image of `s` minus its constant coefficient lies in the662parameter ideal `(t, x)`. -/663theorem concrete_surface_sub_constantCoeff_mem_parameterIdeal (O : Type) [CommRing O] (pi : O)664    (u : (TwoSeries O)ˣ) (a b : ℕ) (s : TwoSeries O) :665    surfaceMk O pi u a b s -666    algebraMap O (ConcreteSurface O pi u a b) (MvPowerSeries.constantCoeff s) ∈667    surfaceParameterIdeal O pi u a b := by668  have h : s - MvPowerSeries.C (MvPowerSeries.constantCoeff s) ∈669      Ideal.span {(MvPowerSeries.X 0 : MvPowerSeries (Fin 2) O), MvPowerSeries.X 1} := by670    rw [mvPowerSeries_fin_two_mem_variableIdeal_iff]671    simp672  have h2 : surfaceMk O pi u a b (s - MvPowerSeries.C (MvPowerSeries.constantCoeff s)) ∈673      surfaceParameterIdeal O pi u a b := by674    have : Ideal.map (surfaceMk O pi u a b)675        (Ideal.span {(MvPowerSeries.X 0 : MvPowerSeries (Fin 2) O), MvPowerSeries.X 1}) ≤676        surfaceParameterIdeal O pi u a b := by677      rw [Ideal.map_span, Ideal.span_le]678      rintro _ ⟨y, hy, rfl⟩679      rcases hy with rfl | rfl680      · exact Ideal.subset_span (by simp [surfaceT, axisT])681      · exact Ideal.subset_span (by simp [surfaceX, axisX])682    exact this (Ideal.mem_map_of_mem _ h)683  convert h2 using 1684  rw [map_sub]685  congr 1686 687/-- The reduction of the surface relation is `-(ū T^a X^b)`. -/688private theorem residueSeries_surfaceRelation (O : Type) [CommRing O] [IsLocalRing O] (pi : O)689    (hpi : pi ∈ IsLocalRing.maximalIdeal O) (u : (TwoSeries O)ˣ) (a b : ℕ) :690    residueSeries O (surfaceRelation O pi u a b) =691    -(residueSeries O (u : TwoSeries O) * axisT (IsLocalRing.ResidueField O) ^ a *692      axisX (IsLocalRing.ResidueField O) ^ b) := by693  have h0 : IsLocalRing.residue O pi = 0 := (IsLocalRing.residue_eq_zero_iff pi).2 hpi694  have hT : residueSeries O (axisT O) = axisT (IsLocalRing.ResidueField O) := by695    simp [residueSeries, axisT, MvPowerSeries.map_X]696  have hX : residueSeries O (axisX O) = axisX (IsLocalRing.ResidueField O) := by697    simp [residueSeries, axisX, MvPowerSeries.map_X]698  have hC : residueSeries O (MvPowerSeries.C pi) = 0 := by699    simp [residueSeries, MvPowerSeries.map_C, h0]700  unfold surfaceRelation701  rw [map_sub, map_mul, map_mul, map_pow, map_pow, hT, hX, hC, zero_sub]702 703/-- The constant coefficient of the surface relation is `π` (when `a > 0`). -/704theorem surfaceRelation_constantCoeff (O : Type) [CommRing O] (pi : O) (u : (TwoSeries O)ˣ)705    (a b : ℕ) (ha : 0 < a) :706    MvPowerSeries.constantCoeff (surfaceRelation O pi u a b) = pi := by707  have hT : MvPowerSeries.constantCoeff (axisT O) = 0 := by708    simp [axisT, MvPowerSeries.constantCoeff_X]709  simp [surfaceRelation, hT, ha.ne']710 711/-- `π` is a nonzerodivisor in the concrete surface. -/712theorem concrete_surface_pi_regular (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]713    (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) :714    Function.Injective715    (fun r : ConcreteSurface O pi u a b ↦ algebraMap O (ConcreteSurface O pi u a b) pi * r) := by716  set P := surfaceRelation O pi u a b717  have hmem : pi ∈ IsLocalRing.maximalIdeal O := (IsLocalRing.mem_maximalIdeal _).2 hpi.not_isUnit718  have hker := residueSeries_ker O pi hpi719  have hrel := residueSeries_surfaceRelation O pi hmem u a b720  have key : ∀ d : TwoSeries O, MvPowerSeries.C pi * d ∈ surfaceIdeal O pi u a b →721      d ∈ surfaceIdeal O pi u a b := by722    intro d hd723    obtain ⟨h, hh⟩ := Ideal.mem_span_singleton'.1 hd724    have h1 : residueSeries O (MvPowerSeries.C pi) = 0 := by725      rw [← RingHom.mem_ker, hker]; exact Ideal.subset_span rfl726    have h2 : residueSeries O h * residueSeries O P = 0 := by727      rw [← map_mul, hh, map_mul, h1, zero_mul]728    have hX (i : Fin 2) : (MvPowerSeries.X i : TwoSeries (IsLocalRing.ResidueField O)) ≠ 0 :=729      mvPowerSeries_X_ne_zero i730    have hne : residueSeries O P ≠ 0 := by731      rw [hrel, neg_ne_zero]732      exact mul_ne_zero (mul_ne_zero (u.isUnit.map _).ne_zero (pow_ne_zero _ (hX 0)))733        (pow_ne_zero _ (hX 1))734    have h3 : residueSeries O h = 0 := (mul_eq_zero.1 h2).resolve_right hne735    rw [← RingHom.mem_ker, hker] at h3736    obtain ⟨h₁, rfl⟩ := Ideal.mem_span_singleton'.1 h3737    have hC : (MvPowerSeries.C pi : TwoSeries O) ≠ 0 := by738      intro h0739      exact hpi.ne_zero (MvPowerSeries.C_injective (by simpa using h0))740    have : d = h₁ * P := by741      apply mul_left_cancel₀ hC742      rw [← hh]; ring743    rw [this]744    exact Ideal.mul_mem_left _ _ (Ideal.subset_span rfl)745  intro r s hrs746  obtain ⟨g, rfl⟩ := Ideal.Quotient.mk_surjective r747  obtain ⟨g', rfl⟩ := Ideal.Quotient.mk_surjective s748  simp only at hrs749  rw [Ideal.Quotient.eq]750  apply key751  rw [← Ideal.Quotient.eq_zero_iff_mem, map_mul, map_sub, mul_sub, sub_eq_zero]752  exact hrs753 754/-- The structure map `O → O[[T,X]]/(π - u T^a X^b)` is injective. -/755theorem concrete_surface_base_injective (O : Type) [CommRing O] [IsDomain O]756    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)757    (ha : 0 < a) :758    Function.Injective (algebraMap O (ConcreteSurface O pi u a b)) := by759  have step1 : ∀ c : O, algebraMap O (ConcreteSurface O pi u a b) c = 0 → pi ∣ c := by760    intro c hc761    change Ideal.Quotient.mk _ (MvPowerSeries.C c) = 0 at hc762    rw [Ideal.Quotient.eq_zero_iff_mem, surfaceIdeal, Ideal.mem_span_singleton'] at hc763    obtain ⟨h, hh⟩ := hc764    have := congrArg (MvPowerSeries.constantCoeff) hh765    simp only [surfaceRelation, axisT, axisX, map_mul, map_sub, MvPowerSeries.constantCoeff_C,766      map_pow, MvPowerSeries.constantCoeff_X, zero_pow ha.ne', mul_zero, zero_mul, sub_zero] at this767    exact ⟨_, by rw [← this]; ring⟩768  have step2 : ∀ k : ℕ, ∀ c : O, algebraMap O (ConcreteSurface O pi u a b) c = 0 → pi ^ k ∣ c := by769    intro k770    induction k with771    | zero => simp772    | succ k ih =>773      intro c hc774      obtain ⟨c', rfl⟩ := step1 c hc775      have h0 : algebraMap O (ConcreteSurface O pi u a b) c' = 0 := by776        apply concrete_surface_pi_regular O pi hpi u a b777        simp only778        rw [← map_mul, hc, mul_zero]779      obtain ⟨d, rfl⟩ := ih c' h0780      exact ⟨d, by ring⟩781  rw [injective_iff_map_eq_zero]782  intro c hc783  have hI : Ideal.span {pi} ≠ ⊤ := by784    rw [Ne, Ideal.span_singleton_eq_top]; exact hpi.not_isUnit785  have hbot := Ideal.iInf_pow_eq_bot_of_isLocalRing (Ideal.span {pi}) hI786  have : c ∈ ⨅ k : ℕ, Ideal.span {pi} ^ k := by787    rw [Ideal.mem_iInf]788    intro k789    rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton]790    exact step2 k c hc791  rw [hbot] at this792  exact (Ideal.mem_bot).1 this793 794/-- The special fiber of the concrete surface is `k[[T,X]]/(T^a X^b)`, compatibly with795reduction of coefficients. -/796theorem concrete_surface_special_fiber_equiv (O : Type) [CommRing O] [IsDomain O]Lemma 2.1797    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) :798    ∃ e : (ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})799    ≃+* SpecialFiber (IsLocalRing.ResidueField O) a b, ∀ s :800    TwoSeries O, e801    (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})802      (surfaceMk O pi u a b s)) =803    Ideal.Quotient.mk (monomialIdeal (IsLocalRing.ResidueField O) a b) (residueSeries O s) := by804  set k := IsLocalRing.ResidueField O805  set ψ : TwoSeries O →+* SpecialFiber k a b :=806    (Ideal.Quotient.mk (monomialIdeal k a b)).comp (residueSeries O) with hψdef807  have hψs : Function.Surjective ψ :=808    (Ideal.Quotient.mk_surjective).comp (residueSeries_surjective O)809  have hker : RingHom.ker ψ =810      Ideal.span {(MvPowerSeries.C pi : TwoSeries O), axisT O ^ a * axisX O ^ b} :=811    residueSeries_comp_monomial_ker O pi hpi a b812  have hmax : pi ∈ IsLocalRing.maximalIdeal O :=813    (IsLocalRing.mem_maximalIdeal _).2 hpi.not_isUnit814  have hle : surfaceIdeal O pi u a b ≤ RingHom.ker ψ := by815    rw [surfaceIdeal, Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe, RingHom.mem_ker,816      hψdef, RingHom.comp_apply, residueSeries_surfaceRelation O pi hmax u a b,817      Ideal.Quotient.eq_zero_iff_mem, Ideal.neg_mem_iff, mul_assoc]818    exact Ideal.mul_mem_left _ _ (Ideal.subset_span rfl)819  set χ : ConcreteSurface O pi u a b →+* SpecialFiber k a b :=820    Ideal.Quotient.lift (surfaceIdeal O pi u a b) ψ fun _ hx ↦ hle hx821  have hχs : Function.Surjective χ := Ideal.Quotient.lift_surjective_of_surjective _ _ hψs822  -- in the surface, `π = u t^a x^b`, so `(π, t^a x^b) = (π)`823  have hrel : surfaceMk O pi u a b (MvPowerSeries.C pi) =824      surfaceMk O pi u a b (u : TwoSeries O) *825        surfaceMk O pi u a b (axisT O ^ a * axisX O ^ b) := by826    rw [← map_mul, surfaceMk, Ideal.Quotient.eq, ← mul_assoc]827    exact Ideal.subset_span rfl828  have hkerχ : RingHom.ker χ = Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi} := by829    rw [show RingHom.ker χ = _ from Ideal.ker_quotient_lift _ _, hker, Ideal.map_span,830      Set.image_pair, Set.pair_comm]831    refine Submodule.span_insert_eq_span ?_832    obtain ⟨v, hv⟩ := u.isUnit.map (surfaceMk O pi u a b)833    refine Ideal.mem_span_singleton'.2 ⟨↑v⁻¹, ?_⟩834    change _ * surfaceMk O pi u a b _ = surfaceMk O pi u a b _835    rw [hrel, ← hv, ← mul_assoc, Units.inv_mul, one_mul]836  exact ⟨(Ideal.quotEquivOfEq hkerχ).symm.trans (RingHom.quotientKerEquivOfSurjective hχs),837    fun _ ↦ rfl⟩838 839/-- Transport of `powerSeries_quotient_length_eq_order` along an identification of the840concrete surface modulo `t` with `k[[X]]`. -/841theorem concrete_surface_equiv_curve_length_and_regular (S : Type) [CommRing S] (O' : Type)842    [CommRing O'] [IsDomain O'] [IsDiscreteValuationRing O'] (pi' : O')843    (u' : (TwoSeries O')ˣ) (a' b' : ℕ) (Eq : S ≃+* ConcreteSurface O' pi' u' a' b')844    (q : (ConcreteSurface O' pi' u' a' b' ⧸ Ideal.span {surfaceT O' pi' u' a' b'}) ≃+*845      PowerSeries (IsLocalRing.ResidueField O')) (g : S) :846    Module.length S (S ⧸ Ideal.span {g, Eq.symm (surfaceT O' pi' u' a' b')}) =847    (q (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'}) (Eq g))).order ∧848    (Function.Injective849      (fun w : S ⧸ Ideal.span {Eq.symm (surfaceT O' pi' u' a' b')} ↦ Ideal.Quotient.mk850        (Ideal.span {Eq.symm (surfaceT O' pi' u' a' b')}) g * w) ↔851      q (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'}) (Eq g)) ≠ 0) := by852  let f : S →+* PowerSeries (IsLocalRing.ResidueField O') :=853    (q.toRingHom.comp (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'}))).comp Eq.toRingHom854  have hfs : Function.Surjective f :=855    (q.surjective.comp Ideal.Quotient.mk_surjective).comp Eq.surjective856  have hfx : ∀ x, f x =857      q (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'}) (Eq x)) := fun x ↦ rfl858  have hker : RingHom.ker f = Ideal.span {Eq.symm (surfaceT O' pi' u' a' b')} := by859    ext x860    rw [RingHom.mem_ker, hfx, map_eq_zero_iff _ q.injective, Ideal.Quotient.eq_zero_iff_mem,861      Ideal.mem_span_singleton, Ideal.mem_span_singleton]862    constructor863    · rintro ⟨c, hc⟩; exact ⟨Eq.symm c, by rw [← Eq.symm_apply_apply x, hc]; simp⟩864    · rintro ⟨c, hc⟩; exact ⟨Eq c, by rw [hc]; simp⟩865  have hfe : f (Eq.symm (surfaceT O' pi' u' a' b')) = 0 := by866    rw [← RingHom.mem_ker, hker]; exact Ideal.mem_span_singleton_self _867  obtain ⟨hlen, hinj⟩ := powerSeries_quotient_length_eq_order (IsLocalRing.ResidueField O') (f g)868  change _ = (f g).order ∧ (_ ↔ f g ≠ 0)869  constructor870  · let _ : Algebra S (PowerSeries (IsLocalRing.ResidueField O')) := f.toAlgebra871    have hJ : Ideal.map f (Ideal.span {g, Eq.symm (surfaceT O' pi' u' a' b')}) =872        Ideal.span {f g} := by873      rw [Ideal.map_span, Set.image_pair, hfe, Set.pair_comm, Ideal.span_insert_zero]874    let L : S →ₗ[S] (PowerSeries (IsLocalRing.ResidueField O') ⧸ Ideal.span {f g}) :=875      (Ideal.Quotient.mkₐ S (Ideal.span {f g})).toLinearMap ∘ₗ Algebra.linearMap S _876    have hL : Function.Surjective L := Ideal.Quotient.mk_surjective.comp hfs877    have hLk : LinearMap.ker L = Ideal.span {g, Eq.symm (surfaceT O' pi' u' a' b')} := by878      ext x879      have h1 : L x = Ideal.Quotient.mk _ (f x) := rfl880      rw [LinearMap.mem_ker, h1, Ideal.Quotient.eq_zero_iff_mem, ← hJ, ← Ideal.mem_comap,881        Ideal.comap_map_of_surjective _ hfs, ← RingHom.ker_eq_comap_bot, hker]882      rw [sup_eq_left.mpr (Ideal.span_mono (by simp))]883    rw [((Submodule.quotEquivOfEq _ _ hLk.symm).trans (L.quotKerEquivOfSurjective hL)).length_eq,884      Module.length_eq_of_surjective hfs, hlen]885  · let ψ : (S ⧸ Ideal.span {Eq.symm (surfaceT O' pi' u' a' b')}) ≃+*886        PowerSeries (IsLocalRing.ResidueField O') :=887      (Ideal.quotEquivOfEq hker.symm).trans (RingHom.quotientKerEquivOfSurjective hfs)888    have hψ : ∀ x, ψ (Ideal.Quotient.mk _ x) = f x := fun x ↦ rfl889    have hfun : (fun w : S ⧸ Ideal.span {Eq.symm (surfaceT O' pi' u' a' b')} ↦890        Ideal.Quotient.mk (Ideal.span {Eq.symm (surfaceT O' pi' u' a' b')}) g * w) =891        ψ.symm ∘ (fun w ↦ f g * w) ∘ ψ := by892      funext w893      apply ψ.injective894      simp [map_mul, hψ]895    rw [hfun, ψ.symm.injective.of_comp_iff, Function.Injective.of_comp_iff' _ ψ.bijective, hinj]896 897/-- The concrete surface modulo `(t, x)` is the residue field of `O`. -/898theorem concrete_surface_quotient_parameters_equiv (O : Type) [CommRing O] [IsDomain O]899    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)900    (ha : 0 < a) :901    ∃ e : (ConcreteSurface O pi u a b ⧸ surfaceParameterIdeal O pi u a b) ≃+*902    IsLocalRing.ResidueField O, ∀ s :903    TwoSeries O, e (Ideal.Quotient.mk (surfaceParameterIdeal O pi u a b) (surfaceMk O pi u a b s)) =904    IsLocalRing.residue O (MvPowerSeries.constantCoeff s) := by905  set φ : TwoSeries O →+* IsLocalRing.ResidueField O :=906    (IsLocalRing.residue O).comp (MvPowerSeries.constantCoeff : TwoSeries O →+* O) with hφdef907  have hpim : pi ∈ IsLocalRing.maximalIdeal O :=908    (IsLocalRing.mem_maximalIdeal _).2 hpi.not_isUnit909  have hφ : ∀ s : TwoSeries O, φ s = IsLocalRing.residue O (MvPowerSeries.constantCoeff s) :=910    fun s ↦ rfl911  have hsurj : Function.Surjective φ := by912    intro y913    obtain ⟨c, rfl⟩ := IsLocalRing.residue_surjective y914    exact ⟨MvPowerSeries.C c, by simp [hφ]⟩915  have hkill : ∀ s ∈ surfaceIdeal O pi u a b, φ s = 0 := by916    intro s hs917    rw [surfaceIdeal, Ideal.mem_span_singleton] at hs918    obtain ⟨c, rfl⟩ := hs919    rw [map_mul, hφ, surfaceRelation_constantCoeff O pi u a b ha,920      (IsLocalRing.residue_eq_zero_iff pi).2 hpim, zero_mul]921  set ψ := Ideal.Quotient.lift (surfaceIdeal O pi u a b) φ hkill with hψdef922  have hψsurj : Function.Surjective ψ :=923    Ideal.Quotient.lift_surjective_of_surjective _ _ hsurj924  have hker : RingHom.ker ψ = surfaceParameterIdeal O pi u a b := by925    apply le_antisymm926    · have hk : RingHom.ker ψ = (RingHom.ker φ).map (Ideal.Quotient.mk _) :=927        Ideal.ker_quotient_lift φ hkill928      rw [hk, hφdef, constantCoeff_residue_ker O pi hpi,929        Ideal.map_span, Ideal.span_le]930      rintro _ ⟨y, hy, rfl⟩931      simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hy932      rcases hy with rfl | rfl | rfl933      · have : Ideal.Quotient.mk (surfaceIdeal O pi u a b) (MvPowerSeries.C pi) =934            surfaceMk O pi u a b ((u : TwoSeries O) * axisT O ^ a * axisX O ^ b) := by935          rw [surfaceMk, Ideal.Quotient.eq, surfaceIdeal]936          exact Ideal.subset_span rfl937        rw [SetLike.mem_coe, this, map_mul, map_mul, map_pow, map_pow]938        obtain ⟨a', rfl⟩ := Nat.exists_eq_add_of_lt ha939        apply Ideal.mul_mem_right940        apply Ideal.mul_mem_left941        apply Ideal.pow_mem_of_mem _ _ _ (by omega)942        exact Ideal.subset_span (by simp [surfaceT])943      · exact Ideal.subset_span (by simp [surfaceT, surfaceMk])944      · exact Ideal.subset_span (by simp [surfaceX, surfaceMk])945    · rw [surfaceParameterIdeal, Ideal.span_le]946      rintro _ (rfl | rfl)947      · simp [surfaceT, surfaceMk, hψdef, hφ, axisT]948      · simp [surfaceX, surfaceMk, hψdef, hφ, axisX]949  exact ⟨(Ideal.quotEquivOfEq hker).symm.trans (RingHom.quotientKerEquivOfSurjective hψsurj),950    fun _ ↦ rfl⟩951 952/-- The parameter ideal `(t, x)` of the concrete surface is maximal. -/953theorem concrete_surface_parameterIdeal_isMaximal (O : Type) [CommRing O] [IsDomain O]954    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)955    (ha : 0 < a) :956    (surfaceParameterIdeal O pi u a b).IsMaximal := by957  obtain ⟨e, -⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha958  exact Ideal.Quotient.maximal_of_isField _ (e.toMulEquiv.isField (Field.toIsField _))959 960/-- The maximal ideal of the (local) concrete surface is `(t, x)`. -/961theorem concrete_surface_maximalIdeal_eq (O : Type) [CommRing O] [IsDomain O]962    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)963    (ha : 0 < a) [IsLocalRing (ConcreteSurface O pi u a b)] :964    IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b) = surfaceParameterIdeal O pi u a b :=965  (IsLocalRing.eq_maximalIdeal (concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha)).symm966 967/-- The residue field of the concrete surface is that of `O`, compatibly with `O → R`. -/968theorem concrete_surface_residueField_equiv (O : Type) [CommRing O] [IsDomain O]969    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)970    (ha : 0 < a) [IsLocalRing (ConcreteSurface O pi u a b)] :971    ∃ e : IsLocalRing.ResidueField O ≃+*972    IsLocalRing.ResidueField (ConcreteSurface O pi u a b), ∀ c : O, e (IsLocalRing.residue O c) =973    IsLocalRing.residue (ConcreteSurface O pi u a b)974    (algebraMap O (ConcreteSurface O pi u a b) c) := by975  obtain ⟨f, hf⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha976  have hm := concrete_surface_maximalIdeal_eq O pi hpi u a b ha977  let g : IsLocalRing.ResidueField (ConcreteSurface O pi u a b) ≃+* IsLocalRing.ResidueField O :=978    (Ideal.quotEquivOfEq hm).trans f979  exact ⟨g.symm, fun c ↦ g.symm_apply_eq.2980    ((hf (.C c)).trans (congrArg _ (MvPowerSeries.constantCoeff_C ..))).symm⟩981 982/-- The maximal ideal of the concrete surface is generated by two elements. -/983theorem concrete_surface_spanFinrank_le_two (O : Type) [CommRing O] [IsDomain O]984    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)985    (ha : 0 < a) [IsLocalRing (ConcreteSurface O pi u a b)] :986    (IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b)).spanFinrank ≤ 2 := by987  rw [concrete_surface_maximalIdeal_eq O pi hpi u a b ha]988  unfold surfaceParameterIdeal989  refine (Submodule.spanFinrank_span_le_ncard_of_finite (Set.toFinite _)).trans ?_990  calc _ ≤ Set.ncard {surfaceX O pi u a b} + 1 := Set.ncard_insert_le _ _991    _ = 2 := by rw [Set.ncard_singleton]992 993/-- The surface ideal is proper when `π` is not a unit and `a > 0`. -/994theorem surfaceIdeal_ne_top (O : Type) [CommRing O] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ)995    (hpi : ¬ IsUnit pi) (ha : 0 < a) :996    surfaceIdeal O pi u a b ≠ ⊤ := by997  intro h998  rw [surfaceIdeal, Ideal.span_singleton_eq_top] at h999  exact hpi (surfaceRelation_constantCoeff O pi u a b ha ▸ MvPowerSeries.isUnit_constantCoeff _ h)1000 1001/-- The concrete surface over a local ring is local when `π` is not a unit and `a > 0`. -/1002theorem concrete_surface_isLocalRing (O : Type) [CommRing O] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ)1003    [IsLocalRing O] (hpi : ¬ IsUnit pi) (ha : 0 < a) :1004    IsLocalRing (ConcreteSurface O pi u a b) := by1005  have : Nontrivial (ConcreteSurface O pi u a b) :=1006    Ideal.Quotient.nontrivial_iff.mpr (surfaceIdeal_ne_top O pi u a b hpi ha)1007  exact IsLocalRing.of_surjective' (surfaceMk O pi u a b) Ideal.Quotient.mk_surjective1008 1009end SurfaceBlowup1010 1011end