Truncations of `k⟦T, X⟧` and contacts on the special fibre

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.Surfaces.PowerSeries7 8/-!9# Truncations of `k⟦T, X⟧` and contacts on the special fibre10 11Elementary facts about the two-variable power series ring `k⟦T, X⟧` over a field, shared by the12residue-ideal counts of the crossing state `k⟦T, X⟧ ⧸ (T^a X^b)` and the single state13`k⟦T, X⟧ ⧸ (T^a)`: the maximal ideal `(T, X)` and residue field; the length14`ℓ(k⟦T, X⟧ ⧸ (F, X_s))` as the order of `F` along the other axis, and its identification with15the contact of `F` with an axis of the special fibre; the truncation16`k⟦T, X⟧ ⧸ ((T^a X^b) + (T, X)^L) ≃ k^(truncIndex a b L)` by coefficients; and the common17counting argument for principal ideals of the special fibre whose generators are described by18vanishing and non-vanishing of truncated coefficients.19 20## Main results21 22* `maximalIdeal_twoSeries`, `twoSeriesResidueEquiv`: the maximal ideal and the residue field.23* `axisQuotientLength_eq_iff`, `contact_fiberT_eq_axisQuotientLength`,24  `contact_fiberX_eq_axisQuotientLength`: contacts as orders along an axis.25* `isUnit_mk_truncIdeal_iff`: units of the truncated quotient (which is identified with its26  coefficient vectors by the linear equivalence `truncEval`).27* `card_mul_eq_zero_eq_card_quotient`: annihilator and quotient of a finite ring have equal size.28* `principal_residue_ideal_count`: the shared core of the crossing and single residue-ideal counts.29 30Provenance: the shared helpers of `crossing_residue_ideal_count` and `single_residue_ideal_count`31(formerly duplicated as `crc_*` in `Measure/Normalizer.lean` and `sric_*` in32`Measure/StateVolumes.lean`).33-/34 35namespace SurfaceBlowup36 37/-- A series lies in the ideal `(T, X)` of `k⟦T, X⟧` iff its constant coefficient vanishes. -/38private theorem mem_axisIdeal_iff (k : Type) [Field k] (φ : TwoSeries k) :39    φ ∈ Ideal.span {axisT k, axisX k} ↔ MvPowerSeries.constantCoeff φ = 0 :=40  mvPowerSeries_fin_two_mem_variableIdeal_iff k φ41 42/-- The ideal `(T, X)` of `k⟦T, X⟧` is maximal. -/43private theorem axisIdeal_isMaximal (k : Type) [Field k] :44    (Ideal.span {axisT k, axisX k}).IsMaximal := by45  have : Ideal.span {axisT k, axisX k} =46      RingHom.ker (MvPowerSeries.constantCoeff (σ := Fin 2) (R := k)) := by47    ext φ; rw [mem_axisIdeal_iff, RingHom.mem_ker]48  rw [this]49  exact RingHom.ker_isMaximal_of_surjective _ (fun x => ⟨MvPowerSeries.C x, by simp⟩)50 51/-- The maximal ideal of `k⟦T, X⟧` is `(T, X)`. -/52theorem maximalIdeal_twoSeries (k : Type) [Field k] :53    IsLocalRing.maximalIdeal (TwoSeries k) = Ideal.span {axisT k, axisX k} :=54  (IsLocalRing.eq_maximalIdeal (axisIdeal_isMaximal k)).symm55 56private theorem fin_two_eq_or {s t : Fin 2} (hst : s ≠ t) (i : Fin 2) : i = s ∨ i = t := by57  omega58 59/-- An exponent vector vanishing at `s` is supported on the other axis `t`. -/60private theorem eq_single_of_apply_eq_zero {s t : Fin 2} (hst : s ≠ t) {m : Fin 2 →₀ ℕ}61    (hm : m s = 0) : m = Finsupp.single t (m t) := by62  ext i; rcases fin_two_eq_or hst i with rfl | rfl <;> simp [hm, hst]63 64/-- The length of `k⟦T, X⟧ ⧸ (F, X_s)`, where `X_0 = T` and `X_1 = X`. -/65noncomputable def axisQuotientLength (k : Type) [Field k] (s : Fin 2) (F : TwoSeries k) : ℕ∞ :=66  Module.length (TwoSeries k) (TwoSeries k ⧸ (Ideal.span {F} ⊔ Ideal.span {MvPowerSeries.X s}))67 68/-- If `F` vanishes on the axis `X_t`, then `ℓ(k⟦T, X⟧ ⧸ (F, X_s)) = ⊤`. -/69theorem axisQuotientLength_eq_top (k : Type) [Field k] {s t : Fin 2} (hst : s ≠ t)70    (F : TwoSeries k)71    (h : ∀ j, MvPowerSeries.coeff (Finsupp.single t j) F = 0) : axisQuotientLength k s F = ⊤ := by72  have hdvd : MvPowerSeries.X s ∣ F := by73    rw [MvPowerSeries.X_dvd_iff]74    intro m hm75    rw [eq_single_of_apply_eq_zero hst hm]; exact h _76  rw [axisQuotientLength, sup_eq_right.mpr (Ideal.span_singleton_le_span_singleton.mpr hdvd)]77  exact axis_quotient_length_top k s t hst78 79/-- If the restriction of `F` to the axis `X_t` has order `d`, then80`ℓ(k⟦T, X⟧ ⧸ (F, X_s)) = d`. -/81theorem axisQuotientLength_eq (k : Type) [Field k] {s t : Fin 2} (hst : s ≠ t)82    (F : TwoSeries k)83    (d : ℕ) (hlow : ∀ j < d, MvPowerSeries.coeff (Finsupp.single t j) F = 0)84    (hd : MvPowerSeries.coeff (Finsupp.single t d) F ≠ 0) : axisQuotientLength k s F = d := by85  set Xs : TwoSeries k := MvPowerSeries.X s86  set Xt : TwoSeries k := MvPowerSeries.X t87  let F0 : TwoSeries k := fun m => if m s = 0 then MvPowerSeries.coeff m F else 088  have hF0 : ∀ m, MvPowerSeries.coeff m F0 = if m s = 0 then MvPowerSeries.coeff m F else 0 :=89    fun m => rfl90  have hT : Xs ∣ F - F0 := by91    rw [MvPowerSeries.X_dvd_iff]92    intro m hm93    rw [map_sub, hF0, if_pos hm, sub_self]94  have hX : Xt ^ d ∣ F0 := by95    rw [MvPowerSeries.X_pow_dvd_iff]96    intro m hm97    rw [hF0]98    split_ifs with h099    · rw [eq_single_of_apply_eq_zero hst h0]; exact hlow _ hm100    · rfl101  obtain ⟨U, hU⟩ := hX102  obtain ⟨G, hG⟩ := hT103  have hU0 : MvPowerSeries.constantCoeff U ≠ 0 := by104    have := congrArg (MvPowerSeries.coeff (Finsupp.single t d)) hU105    rw [hF0, if_pos (by simp [hst]), MvPowerSeries.X_pow_eq,106      MvPowerSeries.coeff_monomial_mul, if_pos le_rfl, one_mul, tsub_self,107      MvPowerSeries.coeff_zero_eq_constantCoeff_apply] at this108    rw [← this]; exact hd109  have hUu : IsUnit U := MvPowerSeries.isUnit_iff_constantCoeff.mpr (isUnit_iff_ne_zero.mpr hU0)110  have hFe : F = Xs * G + Xt ^ d * U := by111    rw [← hG, ← hU]; ring112  have hid : Ideal.span {F} ⊔ Ideal.span {Xs} = Ideal.span {Xs} ⊔ Ideal.span {Xt ^ d} := by113    have hXs := Ideal.mem_span_singleton_self Xs114    simp only [le_antisymm_iff, sup_le_iff, Ideal.span_singleton_le_iff_mem]115    refine ⟨⟨?_, Ideal.mem_sup_left hXs⟩, Ideal.mem_sup_right hXs, ?_⟩116    · rw [hFe]117      exact Ideal.add_mem _ (Ideal.mul_mem_right _ _ (Ideal.mem_sup_left hXs))118        (Ideal.mul_mem_right _ _ (Ideal.mem_sup_right (Ideal.mem_span_singleton_self _)))119    · obtain ⟨V, hV⟩ := hUu.exists_right_inv120      rw [show Xt ^ d = (F - Xs * G) * V by rw [hFe, add_sub_cancel_left, mul_assoc, hV, mul_one]]121      exact Ideal.mul_mem_right _ _ (Ideal.sub_mem _122        (Ideal.mem_sup_left (Ideal.mem_span_singleton_self _))123        (Ideal.mul_mem_right _ _ (Ideal.mem_sup_right hXs)))124  have hcancel : ∀ x, Xt * x ∈ Ideal.span {Xs} → x ∈ Ideal.span {Xs} := by125    intro x hx126    refine axis_pow_mul_mem_span_cancel k t Xs ?_ 1 x (by rwa [pow_one])127    intro hmem128    rw [Ideal.mem_span_singleton, MvPowerSeries.X_dvd_iff] at hmem129    simpa [Xs, MvPowerSeries.coeff_X] using hmem (Finsupp.single s 1) (by simp [hst])130  have h1 :131      Module.length (TwoSeries k) (TwoSeries k ⧸ (Ideal.span {Xs} ⊔ Ideal.span {Xt})) = 1 := by132    have : Ideal.span {Xs} ⊔ Ideal.span {Xt} = Ideal.span {axisT k, axisX k} := by133      rw [Ideal.span_insert]134      fin_cases s <;> fin_cases t <;> first | exact absurd rfl hst | rfl | exact sup_comm _ _135    rw [this, Module.length_eq_one_iff, isSimpleModule_iff_isCoatom]136    exact (axisIdeal_isMaximal k).out137  rw [axisQuotientLength, hid, length_quotient_sup_pow_eq_mul _ _ _ hcancel d, h1, mul_one]138 139/-- `ℓ(k⟦T, X⟧ ⧸ (F, X_s)) = c` iff the restriction of `F` to the other axis `X_t` has order140exactly `c`. -/141theorem axisQuotientLength_eq_iff (k : Type) [Field k] {s t : Fin 2} (hst : s ≠ t) (F : TwoSeries k)142    (c : ℕ) : axisQuotientLength k s F = c ↔143      (∀ j < c, MvPowerSeries.coeff (Finsupp.single t j) F = 0) ∧144      MvPowerSeries.coeff (Finsupp.single t c) F ≠ 0 := by145  classical146  refine ⟨fun h => ?_, fun ⟨h1, h2⟩ => axisQuotientLength_eq k hst F c h1 h2⟩147  by_cases hex : ∃ j, MvPowerSeries.coeff (Finsupp.single t j) F ≠ 0148  · have hmin : ∀ j < Nat.find hex, MvPowerSeries.coeff (Finsupp.single t j) F = 0 :=149      fun j hj => not_not.mp (Nat.find_min hex hj)150    have hc : Nat.find hex = c := by151      exact_mod_cast (axisQuotientLength_eq k hst F _ hmin (Nat.find_spec hex)).symm.trans h152    exact hc ▸ ⟨hmin, Nat.find_spec hex⟩153  · push Not at hex154    exact absurd (h.symm.trans (axisQuotientLength_eq_top k hst F hex)) (ENat.natCast_ne_top c)155 156/-- On the special fibre `k⟦T, X⟧ ⧸ (T^a X^b)` with `0 < a`, the contact of `F` with `T` is157`ℓ(k⟦T, X⟧ ⧸ (F, T))`. -/158theorem contact_fiberT_eq_axisQuotientLength (k : Type) [Field k] (a b : ℕ) (ha : 0 < a)159    (F : TwoSeries k) :160    contact (Ideal.Quotient.mk (monomialIdeal k a b) F) (fiberT k a b) =161      axisQuotientLength k 0 F := by162  have hJT : monomialIdeal k a b ≤ Ideal.span {F, axisT k} := by163    refine le_trans ?_ (Ideal.span_mono (Set.subset_insert F {axisT k}))164    rw [monomialIdeal, Ideal.span_singleton_le_span_singleton]165    exact Dvd.dvd.mul_right (dvd_pow_self _ ha.ne') _166  have h1 := length_double_quotient_eq (TwoSeries k) (monomialIdeal k a b) (Ideal.span {F, axisT k})167  rw [Ideal.map_span, Set.image_pair, sup_eq_right.mpr hJT] at h1168  rw [contact, fiberT, h1, axisQuotientLength, ← Ideal.span_insert]; rfl169 170/-- On the special fibre `k⟦T, X⟧ ⧸ (T^a X^b)` with `0 < b`, the contact of `F` with `X` is171`ℓ(k⟦T, X⟧ ⧸ (F, X))`. -/172theorem contact_fiberX_eq_axisQuotientLength (k : Type) [Field k] (a b : ℕ) (hb : 0 < b)173    (F : TwoSeries k) :174    contact (Ideal.Quotient.mk (monomialIdeal k a b) F) (fiberX k a b) =175      axisQuotientLength k 1 F := by176  have hJT : monomialIdeal k a b ≤ Ideal.span {F, axisX k} := by177    refine le_trans ?_ (Ideal.span_mono (Set.subset_insert F {axisX k}))178    rw [monomialIdeal, Ideal.span_singleton_le_span_singleton]179    exact dvd_mul_of_dvd_right (dvd_pow_self _ hb.ne') _180  have h1 := length_double_quotient_eq (TwoSeries k) (monomialIdeal k a b) (Ideal.span {F, axisX k})181  rw [Ideal.map_span, Set.image_pair, sup_eq_right.mpr hJT] at h1182  rw [contact, fiberX, h1, axisQuotientLength, ← Ideal.span_insert]; rfl183 184/-- The exponents `(i, j)` with `i + j < L` outside the quadrant `i ≥ a, j ≥ b`: the monomials185surviving in `k⟦T, X⟧ ⧸ ((T^a X^b) + (T, X)^L)`. -/186def truncIndex (a b L : ℕ) : Finset (ℕ × ℕ) :=187  (Finset.range L ×ˢ Finset.range L).filter fun ij => ij.1+ij.2<L ∧ ¬(a ≤ ij.1 ∧ b ≤ ij.2)188 189/-- An initial segment `{e 0, …, e (c - 1)}` of an axis `f = 0` (parametrized by `g`) inside190`truncIndex a b L` has `c` elements. -/191theorem card_truncIndex_axis_segment (a b L c : ℕ) (f g : ℕ × ℕ → ℕ) (e : ℕ → ℕ × ℕ)192    (hfe : ∀ j, f (e j) = 0 ∧ g (e j) = j) (hef : ∀ x, f x = 0 → e (g x) = x)193    (hmem : ∀ j < c, e j ∈ truncIndex a b L) :194    (Finset.univ.filter fun s : truncIndex a b L => f s.1 = 0 ∧ g s.1 < c).card = c := by195  refine (Finset.card_bij (t := Finset.range c) (fun s _ => g s.1) ?_ ?_ ?_).trans196    (Finset.card_range c)197  · intro s hs198    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hs199    simpa using hs.2200  · intro s₁ h₁ s₂ h₂ h201    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at h₁ h₂202    exact Subtype.ext (by rw [← hef _ h₁.1, ← hef _ h₂.1, h])203  · intro j hj204    rw [Finset.mem_range] at hj205    exact ⟨⟨e j, hmem j hj⟩, by simp [hfe, hj], (hfe j).2⟩206 207/-- The ideal `(T^a X^b) + (T, X)^L` of `k⟦T, X⟧`. -/208private noncomputable def truncIdeal (k : Type) [Field k] (a b L : ℕ) : Ideal (TwoSeries k) :=209  monomialIdeal k a b ⊔ (Ideal.span {axisT k, axisX k})^L210 211/-- The exponent vector `T^i X^j` of a pair `(i, j)`. -/212noncomputable def truncExponent (ij : ℕ × ℕ) : Fin 2 →₀ ℕ :=213  Finsupp.single 0 ij.1 + Finsupp.single 1 ij.2214 215/-- The coefficients of a series at the exponents of `truncIndex a b L`. -/216noncomputable def truncCoeffs (k : Type) [Field k] (a b L : ℕ) : TwoSeries k →ₗ[k]217    (truncIndex a b L → k) :=218  LinearMap.pi (fun s => MvPowerSeries.coeff (truncExponent s.1))219 220/-- Evaluation of `truncCoeffs`. -/221theorem truncCoeffs_apply (k : Type) [Field k] (a b L : ℕ) (F : TwoSeries k)222    (s : truncIndex a b L) :223    truncCoeffs k a b L F s = MvPowerSeries.coeff (truncExponent s.1) F := rfl224 225private theorem truncCoeffs_surjective_and_ker (k : Type) [Field k] (a b L : ℕ) :226    Function.Surjective (truncCoeffs k a b L) ∧227      ∀ φ, truncCoeffs k a b L φ = 0 ↔ φ ∈ truncIdeal k a b L := by228  let e : ℕ × ℕ → (Fin 2 →₀ ℕ) := truncExponent229  have e0 : ∀ ij, e ij 0 = ij.1 := fun ij => by simp [e, truncExponent]230  have e1 : ∀ ij, e ij 1 = ij.2 := fun ij => by simp [e, truncExponent]231  have eeq : ∀ m : Fin 2 →₀ ℕ, e (m 0, m 1) = m := fun m => by232    ext i; fin_cases i <;> simp [e0, e1]233  have einj : Function.Injective e := fun p q h => by234    have h0 := congrArg (fun m => m 0) h235    have h1 := congrArg (fun m => m 1) h236    simp only [e0, e1] at h0 h1237    exact Prod.ext h0 h1238  refine ⟨?_, ?_⟩239  · intro v240    refine ⟨∑ s, MvPowerSeries.monomial (e s.1) (v s), ?_⟩241    funext s₀242    simp only [truncCoeffs, LinearMap.pi_apply, map_sum, MvPowerSeries.coeff_monomial]243    rw [Finset.sum_eq_single s₀]244    · simp [e]245    · intro s _ hs246      rw [if_neg]247      intro h248      exact hs (Subtype.ext (einj h.symm))249    · simp250  · intro φ251    constructor252    · intro hφ253      have hz : ∀ s : truncIndex a b L, MvPowerSeries.coeff (e s.1) φ = 0 :=254        fun s => congrFun hφ s255      let x : TwoSeries k := fun m => if a ≤ m 0 ∧ b ≤ m 1 then MvPowerSeries.coeff m φ else 0256      have hx : ∀ m, MvPowerSeries.coeff m x =257          if a ≤ m 0 ∧ b ≤ m 1 then MvPowerSeries.coeff m φ else 0 :=258        fun m => rfl259      rw [show φ = x + (φ - x) by ring]260      refine Submodule.add_mem_sup ?_ ?_261      · rw [monomialIdeal_mem_iff]262        intro m hm263        rw [hx, if_neg hm]264      · rw [axis_ideal_pow_mem_iff]265        intro m hm266        rw [map_sub, hx]267        split_ifs with h268        · simp269        · have := hz ⟨(m 0, m 1), by270            simp only [truncIndex, Finset.mem_filter, Finset.mem_product, Finset.mem_range]271            exact ⟨⟨by omega, by omega⟩, hm, h⟩⟩272          simp only [eeq] at this273          simp [this]274    · intro hφ275      obtain ⟨x, hx, y, hy, rfl⟩ := Submodule.mem_sup.mp hφ276      rw [monomialIdeal_mem_iff] at hx277      rw [axis_ideal_pow_mem_iff] at hy278      funext s279      obtain ⟨ij, hij⟩ := s280      simp only [truncIndex, Finset.mem_filter, Finset.mem_product, Finset.mem_range] at hij281      simp only [truncCoeffs, LinearMap.pi_apply, map_add, Pi.zero_apply]282      rw [hx _ (by rw [e0, e1]; exact hij.2.2), hy _ (by rw [e0, e1]; exact hij.2.1), add_zero]283 284/-- The coefficient vector of a class in `k⟦T, X⟧ ⧸ truncIdeal k a b L`, as a linear285equivalence (first isomorphism theorem for `truncCoeffs`). -/286private noncomputable def truncEval (k : Type) [Field k] (a b L : ℕ) :287    (TwoSeries k ⧸ truncIdeal k a b L) ≃ₗ[k] (truncIndex a b L → k) :=288  (Submodule.Quotient.restrictScalarsEquiv k (truncIdeal k a b L)).symm ≪≫ₗ289    Submodule.quotEquivOfEq _ (LinearMap.ker _) (Submodule.ext fun φ ↦290      ((truncCoeffs_surjective_and_ker k a b L).2 φ).symm) ≪≫ₗ291    (truncCoeffs k a b L).quotKerEquivOfSurjective (truncCoeffs_surjective_and_ker k a b L).1292 293/-- `truncEval` on the class of a series `F` is the coefficient vector of `F`. -/294private theorem truncEval_mk (k : Type) [Field k] (a b L : ℕ) (F : TwoSeries k) :295    truncEval k a b L (Ideal.Quotient.mk _ F) = truncCoeffs k a b L F :=296  rfl297 298private theorem truncIdeal_le_axisIdeal (k : Type) [Field k] (a b L : ℕ) (ha : 0 < a) (hL : 0 < L) :299    truncIdeal k a b L ≤ Ideal.span {axisT k, axisX k} := by300  apply sup_le301  · rw [monomialIdeal, Ideal.span_singleton_le_iff_mem]302    exact Ideal.mul_mem_right _ _ (Ideal.pow_mem_of_mem _ (Ideal.subset_span (by simp)) _ ha)303  · exact Ideal.pow_le_self hL.ne'304 305/-- For `0 < a` and `0 < L`, the class of `F` in `k⟦T, X⟧ ⧸ truncIdeal k a b L` is a unit iff306the constant coefficient of `F` is nonzero. -/307theorem isUnit_mk_truncIdeal_iff (k : Type) [Field k] (a b L : ℕ) (ha : 0 < a) (hL : 0 < L)308    (F : TwoSeries k) :309    IsUnit (Ideal.Quotient.mk (truncIdeal k a b L) F) ↔ MvPowerSeries.constantCoeff F ≠ 0 := by310  constructor311  · intro h hF312    obtain ⟨y, hy⟩ := h.exists_right_inv313    obtain ⟨Y, rfl⟩ := Ideal.Quotient.mk_surjective y314    rw [← map_mul, ← map_one (Ideal.Quotient.mk (truncIdeal k a b L)), Ideal.Quotient.eq] at hy315    have := (mem_axisIdeal_iff k _).mp (truncIdeal_le_axisIdeal k a b L ha hL hy)316    simp [hF] at this317  · intro h318    exact (MvPowerSeries.isUnit_iff_constantCoeff.mpr (isUnit_iff_ne_zero.mpr h)).map _319 320/-- For `0 < a` and `0 < L`, the ideal `truncIdeal k a b L` is proper. -/321private theorem truncIdeal_ne_top (k : Type) [Field k] (a b L : ℕ) (ha : 0 < a) (hL : 0 < L) :322    truncIdeal k a b L ≠ ⊤ := fun h =>323  (axisIdeal_isMaximal k).ne_top (top_le_iff.mp (h ▸ truncIdeal_le_axisIdeal k a b L ha hL))324 325/-- In a finite commutative ring, the annihilator of `x` and `B ⧸ (x)` have the same cardinality. -/326theorem card_mul_eq_zero_eq_card_quotient (B : Type) [CommRing B] [Finite B] (x : B) :327    Nat.card {r : B // r * x = 0} = Nat.card (B ⧸ Ideal.span {x}) := by328  let μ := LinearMap.toSpanSingleton B B x329  have hker : Nat.card {r : B // r * x = 0} = Nat.card (LinearMap.ker μ) := by330    apply Nat.card_congr331    exact Equiv.subtypeEquivRight (fun r => by simp [μ, LinearMap.mem_ker])332  have hrange : LinearMap.range μ = Ideal.span {x} := (LinearMap.span_singleton_eq_range B B x).symm333  have h1 := Submodule.card_eq_card_quotient_mul_card (LinearMap.ker μ)334  have h2 := Submodule.card_eq_card_quotient_mul_card (Ideal.span {x} : Submodule B B)335  have h3 : Nat.card (B ⧸ LinearMap.ker μ) = Nat.card (Ideal.span {x} : Submodule B B) := by336    rw [← hrange]; exact Nat.card_congr μ.quotKerEquivRange.toEquiv337  rw [h3] at h1338  have hpos : 0 < Nat.card (Ideal.span {x} : Submodule B B) := Nat.card_pos339  rw [hker]340  have : Nat.card (LinearMap.ker μ) * Nat.card (Ideal.span {x} : Submodule B B) =341      Nat.card (B ⧸ Ideal.span {x}) * Nat.card (Ideal.span {x} : Submodule B B) := by342    rw [← h1, mul_comm, ← h2]343  exact Nat.eq_of_mul_eq_mul_right hpos this344 345/-- The residue field of `k⟦T, X⟧` is `k`, via the constant coefficient. -/346noncomputable def twoSeriesResidueEquiv (k : Type) [Field k] :347    IsLocalRing.ResidueField (TwoSeries k) ≃+* k :=348  (Ideal.quotEquivOfEq (by349    rw [maximalIdeal_twoSeries]; ext φ; rw [mem_axisIdeal_iff, RingHom.mem_ker])).trans350    (RingHom.quotientKerEquivOfSurjective (f := (MvPowerSeries.constantCoeff (σ := Fin 2) (R := k)))351      (fun x => ⟨MvPowerSeries.C x, by simp⟩))352 353/-- If `k⟦T, X⟧ ⧸ ((T^a X^b) + (F))` has length `N`, then it is already a quotient of the354truncation `k⟦T, X⟧ ⧸ ((T^a X^b) + (T, X)^(N + 1))`. -/355private theorem truncIdeal_le_of_length (k : Type) [Field k] (a b N : ℕ) (F : TwoSeries k)356    (hlen : Module.length (TwoSeries k)357      (TwoSeries k ⧸ (monomialIdeal k a b ⊔ Ideal.span {F})) = N) :358    truncIdeal k a b (N + 1) ≤ monomialIdeal k a b ⊔ Ideal.span {F} := by359  have h65 := maximal_ideal_power_kills (TwoSeries k) _ N hlen360  refine sup_le le_sup_left ?_361  rw [← maximalIdeal_twoSeries]362  refine (Ideal.pow_le_pow_right N.le_succ).trans fun x hx => ?_363  have := Submodule.smul_mem_smul hx364    (Submodule.mem_top (x := Ideal.Quotient.mk (monomialIdeal k a b ⊔ Ideal.span {F}) 1))365  rw [h65, Submodule.mem_bot] at this366  rw [← Ideal.Quotient.eq_zero_iff_mem]367  simpa [Algebra.smul_def] using this368 369/-- With `q = #k`, the truncation `k⟦T, X⟧ ⧸ truncIdeal k a b L` (for `0 < a`, `0 < L`) has370`(q - 1) q^(#truncIndex a b L - 1)` units: those with nonzero constant coefficient. -/371private theorem card_units_truncQuotient (k : Type) [Field k] [Finite k] (a b L : ℕ) (ha : 0 < a)372    (hL : 0 < L) : Nat.card (TwoSeries k ⧸ truncIdeal k a b L)ˣ =373      (Nat.card k - 1) * Nat.card k ^ (Fintype.card (truncIndex a b L) - 1) := by374  have : Fintype k := Fintype.ofFinite k375  have h00 : ((0 : ℕ), (0 : ℕ)) ∈ truncIndex a b L := by simp [truncIndex]; omega376  have h61 := coordinate_constraint_count k (truncIndex a b L) ∅ {⟨_, h00⟩}377    (Finset.disjoint_empty_left _)378  rw [Finset.card_singleton, Finset.card_empty, pow_one, Nat.sub_zero,379    ← Nat.card_eq_fintype_card] at h61380  rw [← h61]381  have hunit : ∀ x : TwoSeries k ⧸ truncIdeal k a b L, IsUnit x ↔382      (∀ s ∈ (∅ : Finset (truncIndex a b L)), truncEval k a b L x s = 0) ∧383        ∀ s ∈ ({⟨_, h00⟩} : Finset (truncIndex a b L)), truncEval k a b L x s ≠ 0 := by384    intro x; obtain ⟨F, rfl⟩ := Ideal.Quotient.mk_surjective x385    rw [isUnit_mk_truncIdeal_iff k a b _ ha hL, truncEval_mk]386    simp [truncCoeffs_apply, truncExponent, MvPowerSeries.coeff_zero_eq_constantCoeff_apply]387  refine Nat.card_congr (.ofBijective (fun u => ⟨truncEval k a b L u, (hunit u).mp u.isUnit⟩)388    ⟨?_, ?_⟩)389  · exact fun u v h => Units.ext ((truncEval k a b L).injective (by simpa using h))390  · rintro ⟨g, hg⟩391    obtain ⟨x, rfl⟩ := (truncEval k a b L).surjective g392    exact ⟨((hunit x).mpr hg).unit, rfl⟩393 394/-- Fibre counting for `x ↦ (x)` on a set `G` of elements of a finite ring that is closed under395generating the same principal ideal: if every fibre has `u / c` elements, then396`#G * c = #{(x) : x ∈ G} * u`. -/397private theorem card_mul_eq_card_principal_mul {B : Type} [CommRing B] [Finite B] (G : Set B)398    (c u : ℕ) (hfib : ∀ x ∈ G, Nat.card {g : B // Ideal.span {g} = Ideal.span {x}} * c = u)399    (hclos : ∀ x ∈ G, ∀ y : B, Ideal.span {y} = Ideal.span {x} → y ∈ G) :400    Nat.card G * c = Nat.card {I : Ideal B // ∃ x ∈ G, I = Ideal.span {x}} * u := by401  have : Fintype B := Fintype.ofFinite B402  let Pr := {I : Ideal B // ∃ x ∈ G, I = Ideal.span {x}}403  let π : G → Pr := fun x => ⟨Ideal.span {x.1}, x.1, x.2, rfl⟩404  have : Finite Pr := Finite.of_surjective π fun ⟨_, x, hx, h⟩ => ⟨⟨x, hx⟩, Subtype.ext h.symm⟩405  have : Fintype Pr := Fintype.ofFinite Pr406  have hfib' : ∀ I : Pr, Nat.card {z : G // π z = I} * c = u := by407    rintro ⟨I, x, hx, rfl⟩408    rw [← hfib x hx]409    congr 1410    exact Nat.card_congr411      { toFun := fun z => ⟨z.1.1, congrArg Subtype.val z.2⟩412        invFun := fun g => ⟨⟨g.1, hclos x hx g.1 g.2⟩, Subtype.ext g.2⟩413        left_inv := fun _ => rfl414        right_inv := fun _ => rfl }415  rw [← Nat.card_congr (Equiv.sigmaFiberEquiv π), Nat.card_sigma, Finset.sum_mul,416    Finset.sum_congr rfl (fun I _ => hfib' I), Finset.sum_const, Finset.card_univ, smul_eq_mul,417    Nat.card_eq_fintype_card (α := Pr)]418 419/-- In a local ring, two generators of the same nonzero principal ideal differ by a unit. -/420private theorem exists_isUnit_mul_eq_of_span_eq {B : Type} [CommRing B] [IsLocalRing B] {x y : B}421    (hx : x ≠ 0) (hy : Ideal.span {y} = Ideal.span {x}) : ∃ r, IsUnit r ∧ r * x = y := by422  obtain ⟨r, hr⟩ := Ideal.mem_span_singleton'.mp (hy ▸ Ideal.mem_span_singleton_self y)423  obtain ⟨s, hs⟩ := Ideal.mem_span_singleton'.mp (hy.symm ▸ Ideal.mem_span_singleton_self x)424  refine ⟨r, ?_, hr⟩425  by_contra hnu426  have h1 := IsLocalRing.isUnit_one_sub_self_of_mem_nonunits _427    (Ideal.mul_mem_left _ s ((IsLocalRing.mem_maximalIdeal r).mpr hnu))428  refine hx (h1.mul_right_eq_zero.mp ?_)429  rw [sub_mul, one_mul, mul_assoc, hr, hs, sub_self]430 431/-- If `I ≤ J ≤ I + (F)`, then the principal ideal `(F)` of `S ⧸ I` is the preimage of the432principal ideal `(F)` of `S ⧸ J`. -/433private theorem comap_factor_span_singleton {S : Type} [CommRing S] {I J : Ideal S} (h : I ≤ J)434    {F : S} (hJ : J ≤ I ⊔ Ideal.span {F}) :435    Ideal.comap (Ideal.Quotient.factor h) (Ideal.span {Ideal.Quotient.mk J F}) =436      Ideal.span {Ideal.Quotient.mk I F} := by437  rw [← Ideal.Quotient.factor_mk h, ← Set.image_singleton, ← Ideal.map_span,438    Ideal.comap_map_of_surjective _ (Ideal.Quotient.factor_surjective h), sup_eq_left]439  intro z hz440  obtain ⟨Z, rfl⟩ := Ideal.Quotient.mk_surjective z441  rw [Ideal.mem_comap, Ideal.mem_bot, Ideal.Quotient.factor_mk,442    Ideal.Quotient.eq_zero_iff_mem] at hz443  obtain ⟨M, hM, Y, hY, rfl⟩ := Submodule.mem_sup.mp (hJ hz)444  obtain ⟨r, rfl⟩ := Ideal.mem_span_singleton'.mp hY445  rw [map_add, Ideal.Quotient.eq_zero_iff_mem.mpr hM, zero_add, map_mul]446  exact Ideal.mul_mem_left _ _ (Ideal.mem_span_singleton_self _)447 448/-- Count of the principal ideals `(f)` of the special fibre `k⟦T, X⟧ ⧸ (T^a X^b)` whose generator449satisfies a unit-invariant condition `P` of colength `N` that, read on the truncation450`k⟦T, X⟧ ⧸ truncIdeal k a b (N + 1)`, says: the coefficients on `A` vanish and those on `B` do not.451With `q = #k`, the count times `(q - 1) q^(#A + #B - 1)` is `(q - 1)^#B q^N`. -/452theorem principal_residue_ideal_count (k : Type) [Field k] [Finite k] (a b N : ℕ) (ha : 0 < a)453    (P : TwoSeries k → Prop) (Q : SpecialFiber k a b → Prop)454    (hQ : ∀ F, Q (Ideal.Quotient.mk _ F) ↔ P F) (hunit : ∀ U F, IsUnit U → P F → P (U * F))455    (hlen : ∀ F, P F → Module.length (TwoSeries k)456      (TwoSeries k ⧸ (monomialIdeal k a b ⊔ Ideal.span {F})) = N)457    (hcard : ∀ F, P F →458      Nat.card (TwoSeries k ⧸ (monomialIdeal k a b ⊔ Ideal.span {F})) = Nat.card k ^ N)459    (A B : Finset (truncIndex a b (N + 1))) (hAB : Disjoint A B) (hB : B.Nonempty)460    (hcrit : ∀ F, P F ↔ (∀ s ∈ A, truncCoeffs k a b (N + 1) F s = 0) ∧461      ∀ s ∈ B, truncCoeffs k a b (N + 1) F s ≠ 0) :462    Nat.card {I : Ideal (SpecialFiber k a b) // ∃ f, I = Ideal.span {f} ∧ Q f} *463        ((Nat.card k - 1) * Nat.card k ^ (A.card + B.card - 1)) =464      (Nat.card k - 1) ^ B.card * Nat.card k ^ N := by465  -- Work in the finite local truncation `R' = k⟦T, X⟧ ⧸ truncIdeal k a b (N + 1)`: count the466  -- generators `G` by coefficients, the fibres of `x ↦ (x)` by units, and transport to `Q`.467  have : Fintype k := Fintype.ofFinite k468  have hL0 : 0 < N + 1 := N.succ_pos469  let J := truncIdeal k a b (N + 1)470  let R' := TwoSeries k ⧸ J471  let mk' : TwoSeries k →+* R' := Ideal.Quotient.mk J472  have hmk' : Function.Surjective mk' := Ideal.Quotient.mk_surjective473  have : Nontrivial R' := Ideal.Quotient.nontrivial_iff.mpr (truncIdeal_ne_top k a b _ ha hL0)474  have : IsLocalRing R' := .of_surjective' mk' hmk'475  let ev := truncEval k a b (N + 1)476  have hev : ∀ F, ev (mk' F) = truncCoeffs k a b (N + 1) F := truncEval_mk k a b (N + 1)477  let eqv : R' ≃ (truncIndex a b (N + 1) → k) := ev.toEquiv478  have : Fintype R' := .ofEquiv _ eqv.symm479  have hmonJ : monomialIdeal k a b ≤ J := le_sup_left480  have hkill : ∀ F, P F → J ≤ monomialIdeal k a b ⊔ Ideal.span {F} := fun F hF ↦481    truncIdeal_le_of_length k a b N F (hlen F hF)482  have hcardq : ∀ F, P F → Nat.card (R' ⧸ Ideal.span {mk' F}) = Nat.card k ^ N := by483    intro F hF484    have e := DoubleQuot.quotQuotEquivQuotSup J (Ideal.span {F})485    rw [Ideal.map_span, Set.image_singleton, le_antisymm (sup_le (hkill F hF) le_sup_right)486      (sup_le_sup_right hmonJ _)] at e487    rw [Nat.card_congr e.toEquiv, hcard F hF]488  -- the generators, the units and the fibres of `x ↦ (x)`489  let G : Set R' := {x | (∀ s ∈ A, ev x s = 0) ∧ ∀ s ∈ B, ev x s ≠ 0}490  have hPG : ∀ F, mk' F ∈ G ↔ P F := fun F => by rw [hcrit]; simp only [G, Set.mem_ofPred_eq, hev]491  have hcardG : Nat.card G =492      (Nat.card k - 1) ^ B.card * Nat.card k ^ (Fintype.card (truncIndex a b (N + 1)) -493        A.card - B.card) := by494    rw [Nat.card_eq_fintype_card (α := k), ← coordinate_constraint_count k _ A B hAB]495    exact Nat.card_congr (eqv.subtypeEquiv fun _ => Iff.rfl)496  have hne0 : ∀ x ∈ G, x ≠ 0 := by497    rintro x ⟨-, h⟩ rfl498    obtain ⟨s, hs⟩ := hB499    exact h s hs (by rw [← map_zero mk', hev, map_zero]; rfl)500  have hfib : ∀ x ∈ G,501      Nat.card {g : R' // Ideal.span {g} = Ideal.span {x}} * Nat.card k ^ N = Nat.card R'ˣ := by502    intro x hx503    obtain ⟨F, rfl⟩ := hmk' x504    rw [← hcardq F ((hPG F).1 hx), ← card_mul_eq_zero_eq_card_quotient]505    exact principal_generator_orbit_count R' _ (hne0 _ hx)506  have hclos : ∀ x ∈ G, ∀ y : R', Ideal.span {y} = Ideal.span {x} → y ∈ G := by507    intro x hx y hy508    obtain ⟨F, rfl⟩ := hmk' x509    obtain ⟨r, hru, hr⟩ := exists_isUnit_mul_eq_of_span_eq (hne0 _ hx) hy510    obtain ⟨Gr, rfl⟩ := hmk' r511    have hGu : IsUnit Gr := MvPowerSeries.isUnit_iff_constantCoeff.mpr512      (isUnit_iff_ne_zero.mpr ((isUnit_mk_truncIdeal_iff k a b _ ha hL0 Gr).mp hru))513    rw [← hr, ← map_mul, hPG]514    exact hunit _ _ hGu ((hPG F).1 hx)515  have hU := card_units_truncQuotient k a b (N + 1) ha hL0516  -- counting the principal ideals of `R'` generated in `G`517  have hGP := card_mul_eq_card_principal_mul G _ _ hfib hclos518  -- residue ideals correspond to principal ideals of `R'` generated in `G`519  let ψ := Ideal.Quotient.factor hmonJ520  have hmapI : ∀ F, Ideal.map ψ (Ideal.span {Ideal.Quotient.mk (monomialIdeal k a b) F}) =521      Ideal.span {mk' F} := fun F => by522    rw [Ideal.map_span, Set.image_singleton, Ideal.Quotient.factor_mk]523  let Φ : {I : Ideal (SpecialFiber k a b) // ∃ f, I = Ideal.span {f} ∧ Q f} →524      {I : Ideal R' // ∃ x ∈ G, I = Ideal.span {x}} :=525    fun I => ⟨Ideal.map ψ I.1, by526      obtain ⟨_, f, rfl, hf⟩ := I527      obtain ⟨F, rfl⟩ := Ideal.Quotient.mk_surjective f528      exact ⟨mk' F, (hPG F).2 ((hQ F).1 hf), hmapI F⟩⟩529  have hΦ : Function.Bijective Φ := by530    refine ⟨?_, ?_⟩531    · rintro ⟨_, f₁, rfl, hf₁⟩ ⟨_, f₂, rfl, hf₂⟩ h532      obtain ⟨F₁, rfl⟩ := Ideal.Quotient.mk_surjective f₁533      obtain ⟨F₂, rfl⟩ := Ideal.Quotient.mk_surjective f₂534      have h' := congrArg Subtype.val h535      simp only [Φ, hmapI] at h'536      apply Subtype.ext537      change Ideal.span {_} = Ideal.span {_}538      rw [← comap_factor_span_singleton hmonJ (hkill F₁ ((hQ F₁).1 hf₁)),539        ← comap_factor_span_singleton hmonJ (hkill F₂ ((hQ F₂).1 hf₂))]540      exact congrArg _ h'541    · rintro ⟨_, x, hx, rfl⟩542      obtain ⟨F, rfl⟩ := hmk' x543      exact ⟨⟨_, _, rfl, (hQ F).2 ((hPG F).1 hx)⟩, Subtype.ext (hmapI F)⟩544  rw [Nat.card_congr (Equiv.ofBijective Φ hΦ)]545  rw [hcardG, hU] at hGP546  have hℓ : A.card + B.card ≤ Fintype.card (truncIndex a b (N + 1)) :=547    Finset.card_union_of_disjoint hAB ▸ Finset.card_le_univ _548  have hB1 := hB.card_pos549  set m := Fintype.card (truncIndex a b (N + 1)) - A.card - B.card550  have hpos : 0 < Nat.card k ^ m := pow_pos Nat.card_pos _551  refine Nat.eq_of_mul_eq_mul_left hpos ?_552  rw [show Fintype.card (truncIndex a b (N + 1)) - 1 = m + (A.card + B.card - 1) by omega,553    pow_add] at hGP554  linarith555 556end SurfaceBlowup