Generator normalization and residue-ideal counts

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Blowup.CurveOrders7import SurfaceBlowup.Surfaces.TruncatedSeries8 9/-!10# Generator normalization and residue-ideal counts11 12We study the normal form `(1 + π u) (f + π Σ zᵢ bᵢ) = f + π h` of a perturbed generator, show that13it is unique, continuous for the `π`-adic topology and injective on coordinates, and count the14residue ideals of a crossing state `k⟦T, X⟧ ⧸ (T^a X^b)` with prescribed contacts. We also collect15length/cardinality relations for finite modules over local rings with finite residue field.16 17## Main results18 19* `unique_scaled_generator_normalization`20* `coordinate_ideal_injective`21* `crossing_residue_ideal_count`22* `crossing_state_volume`23* `finite_module_length_card`24* `pi_mul_cokernel_length`25 26Provenance: normalizer_inverse_equation, normalizer_generator_equation,27normalizer_preserves_adic_congruence, coordinate_transition_congruence,28unique_scaled_generator_normalization, coordinate_ideal_injective, crossing_residue_ideal_count,29crossing_state_volume, finite_module_length_card, length_scaling_of_residue_card,30pi_module_length_sum, pi_mul_cokernel_length.31-/32 33open scoped BigOperators ENNReal34 35namespace SurfaceBlowup36 37/-- The generator normal form of `h` is the preimage of `E h` under the adic perturbation by38  `coordinateRemainder pi b E`. -/39private theorem normalizer_inverse_equation (O R : Type) [CommRing O] [CommRing R] [Algebra O R]40    (n : ℕ)41    (pi : O) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))42    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (h : R) :43    adicPerturb (coordinateRemainder pi b E) (generatorNormalForm pi b E h) = E h := by44  have hb := adic_perturb_bijective O ((Fin n → O) × R) (Ideal.span {pi})45    (coordinateRemainder pi b E)46    (coordinate_remainder_raises_order O R n pi b E)47  exact Function.rightInverse_invFun hb.2 (E h)48 49/-- The normal-form coordinates `(z, u)` of `h` satisfy `(1 + π u) (f + π Σ zᵢ bᵢ) = f + π h`. -/50theorem normalizer_generator_equation (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (n : ℕ)51    (pi : O) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))52    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (f : R)53    (hE : ∀ s, E.symm s = divisionMap f b s) (h : R) :54    (1 + pi • (generatorNormalForm pi b E h).2) *55      (f + pi • coordinateLift b (generatorNormalForm pi b E h).1) = f + pi • h := by56  rw [scaled_normalization_identity O R n pi f b E hE,57    normalizer_inverse_equation O R n pi b E h, LinearEquiv.symm_apply_apply]58 59/-- The generator normal form preserves congruence modulo `(π)^j`. -/60private theorem normalizer_preserves_adic_congruence (O R : Type) [CommRing O] [CommRing R]Lemma 3.161    [Algebra O R]62    (n : ℕ) (pi : O) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))63    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (j : ℕ) (h k : R)64    (hhk : adicCongr (Ideal.span {pi}) j h k) :65    adicCongr (Ideal.span {pi}) j (generatorNormalForm pi b E h)66      (generatorNormalForm pi b E k) := by67  have hE := linear_map_preserves_adic_congruence O R ((Fin n → O) × R)68    (Ideal.span {pi}) E.toLinearMap j h k hhk69  simp only [LinearEquiv.coe_coe] at hE70  rw [← normalizer_inverse_equation O R n pi b E h,71    ← normalizer_inverse_equation O R n pi b E k] at hE72  exact (adic_perturb_congruence_iff O ((Fin n → O) × R) (Ideal.span {pi})73    (coordinateRemainder pi b E)74    (coordinate_remainder_raises_order O R n pi b E) j _ _).mp hE75 76/-- The transition between the coordinates of two normalizations preserves congruence modulo77  `(π)^j`. -/78theorem coordinate_transition_congruence (O R : Type) [CommRing O] [CommRing R] [Algebra O R]Lemma 3.179    (n : ℕ) (pi : O) (b : Fin n → R)80    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (c : Fin n → R)81    (F : R ≃ₗ[O] ((Fin n → O) × R)) (h0 : R) (j : ℕ) (z w : Fin n → O)82    (hzw : adicCongr (Ideal.span {pi}) j z w) :83    adicCongr (Ideal.span {pi}) j (idealTransition pi b c F h0 z)84      (idealTransition pi b c F h0 w) := by85  let L : (Fin n → O) →ₗ[O] R :=86    { toFun := fun z => coordinateLift b z87      map_add' := by88        intro x y89        simp [coordinateLift, add_smul, Finset.sum_add_distrib]90      map_smul' := by91        intro r x92        simp [coordinateLift, Finset.smul_sum, smul_smul] }93  have h1 := linear_map_preserves_adic_congruence O _ _ (Ideal.span {pi}) L j z w hzw94  have h2 : adicCongr (Ideal.span {pi}) j (h0 + coordinateLift b z) (h0 + coordinateLift b w) := by95    unfold adicCongr at h1 ⊢96    have : h0 + coordinateLift b z - (h0 + coordinateLift b w) = L z - L w := by97      simp only [add_sub_add_left_eq_sub]; rfl98    rw [this]; exact h199  have h3 := normalizer_preserves_adic_congruence O R n pi c F j _ _ h2100  exact linear_map_preserves_adic_congruence O _ _ (Ideal.span {pi})101    (LinearMap.fst O (Fin n → O) R) j _ _ h3102 103/-- Every `f + π h` is uniquely of the form `(1 + π u) (f + π Σ zᵢ bᵢ)`. -/104theorem unique_scaled_generator_normalization (O R : Type) [CommRing O] [CommRing R] [Algebra O R]Lemma 3.1105    (n : ℕ) [IsDomain R] (pi : O) (hpi : algebraMap O R pi ≠ 0) (f : R) (b : Fin n → R)106    (E : R ≃ₗ[O] ((Fin n → O) × R)) (hE : ∀ s, E.symm s = divisionMap f b s)107    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (h : R) :108    ∃! s : (Fin n → O) × R, (1 + pi • s.2) * (f + pi • coordinateLift b s.1) = f + pi • h := by109  have hbij := adic_perturb_bijective O _ (Ideal.span {pi})110    (coordinateRemainder pi b E)111    (coordinate_remainder_raises_order O R n pi b E)112  have key : ∀ s : (Fin n → O) × R,113      (1 + pi • s.2) * (f + pi • coordinateLift b s.1) = f + pi • h ↔114        adicPerturb (coordinateRemainder pi b E) s = E h := by115    intro s116    rw [scaled_normalization_identity O R n pi f b E hE s]117    constructor118    · intro hs119      have h1 := add_left_cancel hs120      rw [Algebra.smul_def, Algebra.smul_def] at h1121      have h2 := mul_left_cancel₀ hpi h1122      rw [← h2]; simp123    · intro hs124      rw [hs]; simp125  obtain ⟨s, hs⟩ := hbij.2 (E h)126  refine ⟨s, (key s).2 hs, fun t ht => hbij.1 (((key t).1 ht).trans hs.symm)⟩127 128/-- Over a local domain in which `π` is a nonzero nonunit, the normalized ideal129  `coordinateIdeal pi f b z` determines the coordinates `z`. -/130theorem coordinate_ideal_injective (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (n : ℕ)131    (pi : O) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))132    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] [IsDomain R] [IsLocalRing R]133    (hp0 : algebraMap O R pi ≠ 0) (hpm : algebraMap O R pi ∈ IsLocalRing.maximalIdeal R) (f : R)134    (hE : ∀ s, E.symm s = divisionMap f b s)135    (hf : Function.Injective (fun x : R ⧸ Ideal.span {algebraMap O R pi} =>136      x * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f))137    :138    Function.Injective (coordinateIdeal pi f b) := by139  set I := Ideal.span {algebraMap O R pi} with hI140  have hIne : I ≠ ⊤ := by141    intro h142    have : I ≤ IsLocalRing.maximalIdeal R := by143      rw [hI, Ideal.span_le]; simpa using hpm144    exact IsLocalRing.maximalIdeal.isMaximal R |>.ne_top (top_le_iff.mp (h ▸ this))145  have : Nontrivial (R ⧸ I) := Ideal.Quotient.nontrivial_iff.mpr hIne146  have hfbar : Ideal.Quotient.mk I f ≠ 0 := by147    intro h0148    have := @hf 0 1 (by simp [h0])149    exact zero_ne_one this150  have hmk : ∀ z : Fin n → O,151      Ideal.Quotient.mk I (f + pi • coordinateLift b z) = Ideal.Quotient.mk I f := by152    intro z153    rw [Ideal.Quotient.eq]154    simp only [add_sub_cancel_left, Algebra.smul_def]155    exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)156  intro z1 z2 hz157  simp only [coordinateIdeal, normalizedIdeal, normalizedGenerator, coordinateLift_smul_eq_mul,158    ← Algebra.smul_def] at hz159  have hg1 : f + pi • coordinateLift b z1 ≠ 0 := by160    intro h0161    apply hfbar162    rw [← hmk z1, h0, map_zero]163  obtain ⟨u, hu⟩ := regular_principal_generators_associated R _ _164    (fun x y hxy => mul_right_cancel₀ hg1 hxy) hz165  have hubar : Ideal.Quotient.mk I (u : R) = 1 := by166    apply hf167    have := congrArg (Ideal.Quotient.mk I) hu168    rw [map_mul, hmk, hmk] at this169    simpa using this.symm170  have : (u : R) - 1 ∈ I := by171    rw [← Ideal.Quotient.eq, hubar, map_one]172  obtain ⟨v, hv⟩ := Ideal.mem_span_singleton'.mp this173  obtain ⟨s, _, huniq⟩ := unique_scaled_generator_normalization O R n pi hp0 f b E hE174    (coordinateLift b z2)175  have e1 := huniq (z1, v) (by176    simp only [Algebra.smul_def] at hu ⊢177    rw [hu]; congr 1; linear_combination hv)178  have e2 := huniq (z2, 0) (by simp)179  exact congrArg Prod.fst (e1.trans e2.symm)180 181/-- The number of crossing residue ideals of `k⟦T, X⟧ ⧸ (T^a X^b)` with contacts `c` with `T` and182  `h` with `X` is `(q - 1) q^(ac + bh - c - h)`, where `q = #k`. -/183theorem crossing_residue_ideal_count (k : Type) [Field k] [Finite k] (a b c h : ℕ) (ha : 0 < a)Proposition 3.3184    (hb : 0 < b) (hc : 0 < c) (hh : 0 < h) :185    Nat.card (crossingResidueIdeals k a b c h) = (Nat.card k-1)*(Nat.card k)^(a*c+b*h-c-h) := by186  have hcN : c ≤ a * c := Nat.le_mul_of_pos_left c ha187  have hhN : h ≤ b * h := Nat.le_mul_of_pos_left h hb188  set N := a*c+b*h with hNdef189  let P : TwoSeries k → Prop := fun F => axisQuotientLength k 0 F = c ∧ axisQuotientLength k 1 F = h190  have hlen : ∀ F, P F →191      Module.length (TwoSeries k) (TwoSeries k ⧸ (monomialIdeal k a b ⊔ Ideal.span {F})) = N := by192    intro F hF193    have h5 := length_double_quotient_eq (TwoSeries k) (monomialIdeal k a b) (Ideal.span {F})194    rw [Ideal.map_span, Set.image_singleton] at h5195    rw [← h5, crossing_special_fiber_length k a b c h ha hb _196      (by rw [contact_fiberT_eq_axisQuotientLength k a b ha, hF.1])197      (by rw [contact_fiberX_eq_axisQuotientLength k a b hb, hF.2]), hNdef]198    push_cast; rfl199  have : Finite (IsLocalRing.ResidueField (TwoSeries k)) :=200    .of_equiv _ (twoSeriesResidueEquiv k).toEquiv.symm201  have hmemS : ∀ j < N+1, ((0:ℕ), j) ∈ truncIndex a b (N+1) := by202    intro j hj; simp [truncIndex]; omega203  have hmemS' : ∀ i < N+1, (i, (0:ℕ)) ∈ truncIndex a b (N+1) := by204    intro i hi; simp [truncIndex]; omega205  have hEj : ∀ j, truncExponent ((0:ℕ), j) = Finsupp.single 1 j := by simp [truncExponent]206  have hEi : ∀ i, truncExponent (i, (0:ℕ)) = Finsupp.single 0 i := by simp [truncExponent]207  let A1 : Finset (truncIndex a b (N+1)) := Finset.univ.filter (fun s => s.1.1 = 0 ∧ s.1.2 < c)208  let A2 : Finset (truncIndex a b (N+1)) := Finset.univ.filter (fun s => s.1.2 = 0 ∧ s.1.1 < h)209  let B : Finset (truncIndex a b (N+1)) :=210    {⟨(0,c), hmemS c (by omega)⟩, ⟨(h,0), hmemS' h (by omega)⟩}211  have hA1 : A1.card = c := card_truncIndex_axis_segment a b _ c Prod.fst Prod.snd ((0, ·))212    (fun _ => ⟨rfl, rfl⟩) (fun x h => Prod.ext h.symm rfl) fun j hj => hmemS j (by omega)213  have hA2 : A2.card = h := card_truncIndex_axis_segment a b _ h Prod.snd Prod.fst ((·, 0))214    (fun _ => ⟨rfl, rfl⟩) (fun x h => Prod.ext rfl h.symm) fun i hi => hmemS' i (by omega)215  have hA12 : (A1 ∩ A2).card = 1 := by216    rw [Finset.card_eq_one]; refine ⟨⟨(0,0), hmemS 0 (by omega)⟩, ?_⟩217    ext ⟨⟨i, j⟩, hij⟩218    simp only [A1, A2, Finset.mem_inter, Finset.mem_filter, Finset.mem_univ, true_and,219      Finset.mem_singleton, Subtype.mk.injEq, Prod.mk.injEq]220    omega221  have hA := Finset.card_union_add_card_inter A1 A2222  have hB : B.card = 2 := by223    rw [Finset.card_pair]224    simp only [ne_eq, Subtype.mk.injEq, Prod.mk.injEq]225    omega226  have hAB : Disjoint (A1 ∪ A2) B := by227    rw [Finset.disjoint_left]228    rintro ⟨⟨i, j⟩, hij⟩ hs hs'229    simp only [A1, A2, B, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, true_and,230      Finset.mem_insert, Finset.mem_singleton, Subtype.mk.injEq, Prod.mk.injEq] at hs hs'231    omega232  have hcrit : ∀ F, P F ↔ (∀ s ∈ A1 ∪ A2, truncCoeffs k a b (N+1) F s = 0) ∧233      (∀ s ∈ B, truncCoeffs k a b (N+1) F s ≠ 0) := by234    intro F235    change axisQuotientLength k 0 F = c ∧ axisQuotientLength k 1 F = h ↔ _236    rw [axisQuotientLength_eq_iff k (by decide : (0 : Fin 2) ≠ 1),237      axisQuotientLength_eq_iff k (by decide : (1 : Fin 2) ≠ 0)]238    simp only [B, Finset.mem_insert, Finset.mem_singleton, forall_eq_or_imp, forall_eq,239      truncCoeffs_apply, hEj, hEi]240    constructor241    · rintro ⟨⟨h1, h2⟩, ⟨h1', h2'⟩⟩242      refine ⟨fun ⟨⟨i, j⟩, hij⟩ hs => ?_, h2, h2'⟩243      simp only [A1, A2, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, true_and] at hs244      rcases hs with ⟨rfl, hj⟩ | ⟨rfl, hi⟩245      · rw [hEj]; exact h1 j hj246      · rw [hEi]; exact h1' i hi247    · rintro ⟨h1, h2, h2'⟩248      refine ⟨⟨fun j hj => ?_, h2⟩, ⟨fun i hi => ?_, h2'⟩⟩249      · simpa [hEj] using h1 ⟨(0, j), hmemS j (by omega)⟩ (by simp [A1, hj])250      · simpa [hEi] using h1 ⟨(i, 0), hmemS' i (by omega)⟩ (by simp [A2, hi])251  have key := principal_residue_ideal_count k a b N ha P252    (fun f => contact f (fiberT k a b) = c ∧ contact f (fiberX k a b) = h)253    (fun F => by254      rw [contact_fiberT_eq_axisQuotientLength k a b ha,255        contact_fiberX_eq_axisQuotientLength k a b hb])256    (fun U F hU hF => by257      change axisQuotientLength k 0 _ = c ∧ axisQuotientLength k 1 _ = h258      rwa [axisQuotientLength, axisQuotientLength, Ideal.span_singleton_mul_left_unit hU])259    hlen (fun F hF => by260      rw [finite_length_module_card (TwoSeries k) _ _ (hlen F hF),261        Nat.card_congr (twoSeriesResidueEquiv k).toEquiv])262    (A1 ∪ A2) B hAB (Finset.insert_nonempty _ _) hcrit263  rw [show (A1 ∪ A2).card + B.card - 1 = c + h by omega, hB,264    show N = c + h + (N - c - h) by omega, pow_add _ (c + h)] at key265  have hp : 0 < Nat.card k - 1 := by have := Finite.one_lt_card (α := k); omega266  have hpos : 0 < (Nat.card k - 1) * Nat.card k ^ (c + h) :=267    Nat.mul_pos hp (pow_pos Nat.card_pos _)268  unfold crossingResidueIdeals269  refine Nat.eq_of_mul_eq_mul_left hpos ?_270  rw [sq] at key271  linarith [key]272 273/-- The total state measure of a crossing state with contacts `c` and `h` is `(q - 1) q^(-(c + h))`,274  where `q` is the residue cardinality. -/275theorem crossing_state_volume (O R : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Proposition 3.3276    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]277    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]278    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]279    (htop : IsAdic (IsLocalRing.maximalIdeal O)) [CommRing R] [Algebra O R]280    [MeasurableSpace (Ideal R)] (pi : O) (X : Set (Ideal R))281    (a b c h : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hh : 0 < h)282    (A : IdealAtlas O R pi (a * c + b * h) X)283    (hA : ∀ i, Measurable (coordinateIdeal pi (A.chart i).f (A.chart i).b))284    (hcount : Nonempty (A.ι ≃ crossingResidueIdeals (IsLocalRing.ResidueField O) a b c h)) :285    stateMeasure O R pi (a*c+b*h) (Nat.card (IsLocalRing.ResidueField O)) A Set.univ =286      ((Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞) - 1) *287        (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^(c+h) := by288  rw [state_measure_total_mass O R htop pi (a*c+b*h) X A hA]289  obtain ⟨e⟩ := hcount290  have hcard : Fintype.card A.ι = (Nat.card (IsLocalRing.ResidueField O) - 1) *291      (Nat.card (IsLocalRing.ResidueField O)) ^ (a*c+b*h-c-h) := by292    rw [← Nat.card_eq_fintype_card, Nat.card_congr e]293    exact crossing_residue_ideal_count _ a b c h ha hb hc hh294  rw [hcard]295  set q := Nat.card (IsLocalRing.ResidueField O)296  have hq : 1 ≤ q := Nat.card_pos297  have hN : a*c+b*h = (a*c+b*h-c-h) + (c+h) := by298    have : c ≤ a*c := Nat.le_mul_of_pos_left c ha299    have : h ≤ b*h := Nat.le_mul_of_pos_left h hb300    omega301  have hq0 : (q:ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : q ≠ 0)302  have hqt : (q:ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top q303  set m := a*c+b*h-c-h304  rw [hN, pow_add, Nat.cast_mul, ENNReal.natCast_sub, Nat.cast_pow, Nat.cast_one]305  have : (q:ℝ≥0∞)^m * (q:ℝ≥0∞)⁻¹^m = 1 := by306    rw [← mul_pow, ENNReal.mul_inv_cancel hq0 hqt, one_pow]307  calc ((q:ℝ≥0∞) - 1) * (q:ℝ≥0∞)^m * ((q:ℝ≥0∞)⁻¹^m * (q:ℝ≥0∞)⁻¹^(c+h))308      = ((q:ℝ≥0∞) - 1) * ((q:ℝ≥0∞)^m * (q:ℝ≥0∞)⁻¹^m) * (q:ℝ≥0∞)⁻¹^(c+h) := by ring309    _ = _ := by rw [this, mul_one]310 311/-- A finite module over a local ring with residue field of cardinality `q` has finite length `ℓ`312  and cardinality `q ^ ℓ`. -/313theorem finite_module_length_card (O : Type) [CommRing O] [IsLocalRing O]314    [Finite (IsLocalRing.ResidueField O)] (M : Type) [AddCommGroup M] [Module O M] [Finite M] :315    ∃ ℓ : ℕ, Module.length O M = ℓ ∧ Nat.card M = Nat.card (IsLocalRing.ResidueField O) ^ ℓ := by316  have hN : IsNoetherian O M := isNoetherian_of_finite O M317  have hA : IsArtinian O M := isArtinian_of_finite318  have hF : IsFiniteLength O M := isFiniteLength_iff_isNoetherian_isArtinian.mpr ⟨hN, hA⟩319  have hne : Module.length O M ≠ ⊤ := Module.length_ne_top_iff.mpr hF320  obtain ⟨ℓ, hℓ⟩ := ENat.ne_top_iff_exists.mp hne321  exact ⟨ℓ, hℓ.symm, finite_length_module_card O M ℓ hℓ.symm⟩322 323/-- If `#k(O') = #k(O) ^ δ`, then a module of `O'`-length `ℓ` has `O`-length `δ ℓ`. -/324theorem length_scaling_of_residue_card (O : Type) [CommRing O] [IsLocalRing O]325    [Finite (IsLocalRing.ResidueField O)] (O' : Type) [CommRing O'] [IsLocalRing O']326    [Finite (IsLocalRing.ResidueField O')] (δ : ℕ)327    (hδ : Nat.card (IsLocalRing.ResidueField O') = Nat.card (IsLocalRing.ResidueField O) ^ δ)328    (M : Type) [AddCommGroup M] [Module O M] [Module O' M] (ℓ : ℕ) (hℓ : Module.length O' M = ℓ) :329    Module.length O M = ((δ * ℓ : ℕ) : ℕ∞) := by330  have h1 := finite_length_module_card O' M ℓ hℓ331  have hq : 2 ≤ Nat.card (IsLocalRing.ResidueField O) := by332    have := Finite.one_lt_card (α := IsLocalRing.ResidueField O)333    omega334  have hne : Nat.card M ≠ 0 := by335    rw [h1, hδ, ← pow_mul]336    exact pow_ne_zero _ (by omega)337  have : Finite M := Nat.finite_of_card_ne_zero hne338  obtain ⟨l, hl, hc⟩ := finite_module_length_card O M339  rw [hl]340  congr 1341  rw [h1, hδ, ← pow_mul] at hc342  exact (Nat.pow_right_injective hq hc).symm343 344/-- The length of a finite product of finite-length modules is the sum of the lengths. -/345private theorem pi_module_length_sum (O : Type) [CommRing O] [IsLocalRing O]346    [Finite (IsLocalRing.ResidueField O)] (ι : Type) [Fintype ι] (M : ι → Type)347    [∀ j, AddCommGroup (M j)] [∀ j, Module O (M j)] (ℓ : ι → ℕ)348    (hℓ : ∀ j, Module.length O (M j) = ℓ j) :349    Module.length O (∀ j, M j) = ((∑ j, ℓ j : ℕ) : ℕ∞) := by350  have hc := fun j => finite_length_module_card O (M j) (ℓ j) (hℓ j)351  set q := Nat.card (IsLocalRing.ResidueField O) with hq352  have hq2 : 2 ≤ q := by353    have : Nontrivial (IsLocalRing.ResidueField O) := inferInstance354    have : Finite (IsLocalRing.ResidueField O) := inferInstance355    exact Nat.succ_le_of_lt (Finite.one_lt_card)356  have hfin : ∀ j, Finite (M j) := fun j =>357    Nat.finite_of_card_ne_zero (by rw [hc j]; positivity)358  have : Finite (∀ j, M j) := inferInstance359  obtain ⟨l, hl, hcard⟩ := finite_module_length_card O (∀ j, M j)360  have h2 : Nat.card (∀ j, M j) = q ^ (∑ j, ℓ j) := by361    rw [Nat.card_pi, ← Finset.prod_pow_eq_pow_sum]362    exact Finset.prod_congr rfl (fun j _ => hc j)363  rw [hl]364  have : l = ∑ j, ℓ j := Nat.pow_right_injective hq2 (hcard.symm.trans h2)365  rw [this]366 367/-- The cokernel of multiplication by `e` on `(Π C_j) ⧸ (g)` has length368  `Σ_j length (C_j ⧸ (g_j, e_j))`. -/369theorem pi_mul_cokernel_length (O : Type) [CommRing O] [IsLocalRing O]370    [Finite (IsLocalRing.ResidueField O)] (ι : Type) [Fintype ι] (C : ι → Type)371    [∀ j, CommRing (C j)] [∀ j, Algebra O (C j)] (g e : ∀ j, C j) (ℓ : ι → ℕ)372    (hℓ : ∀ j, Module.length O (C j ⧸ (Ideal.span {g j} ⊔ Ideal.span {e j})) = ℓ j) :373    Module.length O (((∀ j, C j) ⧸ Ideal.span {g}) ⧸374      LinearMap.range (LinearMap.mulLeft O (Ideal.Quotient.mk (Ideal.span {g}) e))) =375      ((∑ j, ℓ j : ℕ) : ℕ∞) := by376  obtain ⟨φ, -⟩ := quotient_mul_range_equiv O (∀ j, C j) (Ideal.span {g}) e377  obtain ⟨-, ψ', -⟩ := pi_quotient_span_linearEquiv O ι C g e378  rw [φ.length_eq, ψ'.length_eq]379  exact pi_module_length_sum O ι _ ℓ hℓ380 381end SurfaceBlowup