Local lengths and finite quotients of completions

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Blowup.Charts7import SurfaceBlowup.Surfaces.PowerSeries8import Mathlib.RingTheory.AdicCompletion.Completeness9 10/-!11# Local lengths and finite quotients of completions12 13Assorted local results: the length of a principal quotient of the model special fibre14`k[[T,X]]/(T^a X^b)` in terms of contact numbers; finite quotients `Â/m̂^L ≃ A/m^L` of the15completion of a Noetherian local ring and the resulting descent of finite-colength ideals.16 17## Main results18 19* `SurfaceBlowup.crossing_special_fiber_length`, `SurfaceBlowup.single_special_fiber_length`20* `SurfaceBlowup.local_completion_finite_quotient`,21  `SurfaceBlowup.finite_colength_completion_ideal_descent`,22  `SurfaceBlowup.finite_completed_point_quotient_surjective`23 24Provenance: Thm_SurfaceBlowupV2_{crossing_special_fiber_length, single_special_fiber_length,25local_completion_finite_quotient, completion_to_finite_quotient_surjective,26finite_colength_completion_ideal_descent,27finite_completed_point_quotient_surjective}.28-/29 30namespace SurfaceBlowup31 32 33/-! ### Lengths in the special fibre -/34 35/-- Let `Xₛ` be a variable dividing `T^a X^b`. If the images of `F` and `Xₛ` in the special fibre36`k[[T,X]]/(T^a X^b)` have finite contact `c`, then `Xₛ` is a nonzerodivisor modulo `F` and37`k[[T,X]]/(F, Xₛⁿ)` has length `n c`. -/38private theorem axis_contact (k : Type) [Field k] (a b : ℕ) (F : TwoSeries k) (s t : Fin 2)39    (hst : s ≠ t) (c : ℕ)40    (hdvd : (MvPowerSeries.X s : TwoSeries k) ∣ MvPowerSeries.X 0 ^ a * MvPowerSeries.X 1 ^ b)41    (hc : contact (Ideal.Quotient.mk (monomialIdeal k a b) F)42      (Ideal.Quotient.mk _ (MvPowerSeries.X s)) = c) :43    (∀ n x, (MvPowerSeries.X s : TwoSeries k) ^ n * x ∈ Ideal.span {F} → x ∈ Ideal.span {F}) ∧44    ∀ n : ℕ, Module.length (TwoSeries k) (TwoSeries k ⧸45      (Ideal.span {F} ⊔ Ideal.span {(MvPowerSeries.X s : TwoSeries k) ^ n})) = n * c := by46  have hc' : Module.length (TwoSeries k)47      (TwoSeries k ⧸ (Ideal.span {F} ⊔ Ideal.span {(MvPowerSeries.X s : TwoSeries k)})) = c := by48    have hJ : monomialIdeal k a b ≤ Ideal.span {F, MvPowerSeries.X s} :=49      (Ideal.span_singleton_le_span_singleton.2 hdvd).trans50        (Ideal.span_mono (Set.subset_insert F _))51    have h1 := length_double_quotient_eq (TwoSeries k) (monomialIdeal k a b)52      (Ideal.span {F, MvPowerSeries.X s})53    rw [Ideal.map_span, Set.image_pair, sup_eq_right.mpr hJ] at h154    rw [← Ideal.span_insert, ← h1]55    exact hc56  have hF : F ∉ Ideal.span {(MvPowerSeries.X s : TwoSeries k)} := fun hmem ↦ by57    rw [sup_eq_right.mpr ((Ideal.span_singleton_le_iff_mem _).mpr hmem),58      axis_quotient_length_top k s t hst] at hc'59    exact ENat.top_ne_natCast c hc'60  have hcan := axis_pow_mul_mem_span_cancel k s F hF61  refine ⟨hcan, fun n ↦ ?_⟩62  rw [length_quotient_sup_pow_eq_mul _ _ _ (fun x hx ↦ hcan 1 x (by simpa using hx)) n, hc']63 64/-- A principal quotient of `k[[T,X]]/(T^a X^b)` (with `a, b > 0`) by `f` has length `a c + b h`,65where `c` and `h` are the contacts of `f` with `T` and with `X`. -/66theorem crossing_special_fiber_length (k : Type) [Field k] (a b c h : ℕ) (ha : 0 < a) (hb : 0 < b)Lemma 2.167    (f : SpecialFiber k a b) (ht : contact f (fiberT k a b) = c)68    (hx : contact f (fiberX k a b) = h) :69    Module.length (SpecialFiber k a b) ((SpecialFiber k a b) ⧸ Ideal.span {f}) = a * c + b * h := by70  obtain ⟨F, rfl⟩ := Ideal.Quotient.mk_surjective f71  obtain ⟨-, hT⟩ := axis_contact k a b F 0 1 (by decide) c72    (dvd_mul_of_dvd_left (dvd_pow_self _ ha.ne') _) ht73  obtain ⟨hX, hX'⟩ := axis_contact k a b F 1 0 (by decide) h74    (dvd_mul_of_dvd_right (dvd_pow_self _ hb.ne') _) hx75  have h5 := length_double_quotient_eq (TwoSeries k) (monomialIdeal k a b) (Ideal.span {F})76  rw [Ideal.map_span, Set.image_singleton] at h577  rw [h5, monomialIdeal, axisT, axisX, sup_comm, length_quotient_sup_mul_eq_add _ _ _ _ (hX b), hT,78    hX']79 80/-- A principal quotient of `k[[T,X]]/(T^a)` (with `a > 0`) by `f` has length `a c`, where `c` is81the contact of `f` with `T`. -/82theorem single_special_fiber_length (k : Type) [Field k] (a c : ℕ) (ha : 0 < a)Lemma 2.183    (f : SpecialFiber k a 0) (hf : contact f (fiberT k a 0) = c) :84    Module.length (SpecialFiber k a 0) ((SpecialFiber k a 0) ⧸ Ideal.span {f}) = a * c := by85  obtain ⟨F, rfl⟩ := Ideal.Quotient.mk_surjective f86  obtain ⟨-, hT⟩ := axis_contact k a 0 F 0 1 (by decide) c87    (dvd_mul_of_dvd_left (dvd_pow_self _ ha.ne') _) hf88  have h5 := length_double_quotient_eq (TwoSeries k) (monomialIdeal k a 0) (Ideal.span {F})89  rw [Ideal.map_span, Set.image_singleton] at h590  rw [h5, monomialIdeal, pow_zero, mul_one, sup_comm, axisT, hT]91 92/-! ### Finite quotients of completions -/93 94/-- For a Noetherian local ring `(A, m)` with completion `Â`, the quotient `Â/(m Â)^L` is95`A`-isomorphic to `A/m^L`, compatibly with the maps from `A`. -/96theorem local_completion_finite_quotient (A : Type) [CommRing A] [IsNoetherianRing A]97    [IsLocalRing A] (L : ℕ) :98    ∃ E : (LocalCompletion A ⧸ ((IsLocalRing.maximalIdeal A).map (localCompletionMap A))^L) ≃ₐ[A]99      (A ⧸ (IsLocalRing.maximalIdeal A)^L), ∀ a : A,100      E (Ideal.Quotient.mk (((IsLocalRing.maximalIdeal A).map (localCompletionMap A))^L)101        (localCompletionMap A a)) = Ideal.Quotient.mk ((IsLocalRing.maximalIdeal A)^L) a := by102  set I := IsLocalRing.maximalIdeal A103  have fg : I.FG := (IsNoetherian.noetherian I)104  have hker : RingHom.ker (AdicCompletion.evalₐ I L) = (I.map (localCompletionMap A))^L := by105    ext x106    trans x ∈ (AdicCompletion.eval I A L).ker107    · have eq : I ^ L • (⊤ : Ideal A) = I ^ L := by simp108      have : Function.Injective (Ideal.Quotient.factor ((le_of_eq eq))) := by109        simpa [RingHom.injective_iff_ker_eq_bot, Ideal.Quotient.factor_ker]110          using Ideal.map_mk_eq_bot_of_le (le_of_eq eq.symm)111      rw [RingHom.mem_ker, ← AdicCompletion.factor_eval_eq_evalₐ I x (le_of_eq eq)]112      exact (map_eq_zero_iff _ this).trans LinearMap.mem_ker.symm113    · rw [← AdicCompletion.pow_smul_top_eq_ker_eval fg, Ideal.smul_top_eq_map, ← Ideal.map_pow]114      rfl115  refine ⟨(Ideal.quotientEquivAlgOfEq A hker.symm).trans116    (Ideal.quotientKerAlgEquivOfSurjective (AdicCompletion.surjective_evalₐ I L)), fun a ↦ ?_⟩117  simp only [AlgEquiv.trans_apply]118  exact AdicCompletion.evalₐ_of I L a119 120/-- For an ideal `J` of the completion `Â` containing `(m Â)^L`, the composite `A → Â → Â/J` is121surjective. -/122private theorem completion_to_finite_quotient_surjective (A : Type) [CommRing A]123    [IsNoetherianRing A]124    [IsLocalRing A] (L : ℕ) (J : Ideal (LocalCompletion A))125    (hJ : ((IsLocalRing.maximalIdeal A).map (localCompletionMap A)) ^ L ≤ J) :126    Function.Surjective ((Ideal.Quotient.mk J).comp (localCompletionMap A)) := by127  obtain ⟨E, hE⟩ := local_completion_finite_quotient A L128  intro q129  obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective q130  obtain ⟨a, ha⟩ := Ideal.Quotient.mk_surjective (E (Ideal.Quotient.mk _ b))131  refine ⟨a, Ideal.Quotient.eq.2 (hJ (Ideal.Quotient.eq.1 (E.injective ?_)))⟩132  rw [hE, ha]133 134/-- An ideal `J` of the completion `Â` containing `(m Â)^L` is extended from its contraction to135`A`. -/136theorem finite_colength_completion_ideal_descent (A : Type) [CommRing A] [IsNoetherianRing A]137    [IsLocalRing A] (L : ℕ) (J : Ideal (LocalCompletion A))138    (hJ : ((IsLocalRing.maximalIdeal A).map (localCompletionMap A)) ^ L ≤ J) :139    (J.comap (localCompletionMap A)).map (localCompletionMap A) = J := by140  refine le_antisymm Ideal.map_comap_le fun b hb ↦ ?_141  set M := (IsLocalRing.maximalIdeal A).map (localCompletionMap A)142  obtain ⟨E, hE⟩ := local_completion_finite_quotient A L143  obtain ⟨a, ha⟩ := Ideal.Quotient.mk_surjective (E (Ideal.Quotient.mk (M ^ L) b))144  have hdiff : b - localCompletionMap A a ∈ M ^ L :=145    Ideal.Quotient.eq.mp (E.injective (by rw [hE a, ha]))146  set I := J.comap (localCompletionMap A)147  have hML : M ^ L ≤ I.map (localCompletionMap A) := by148    rw [← Ideal.map_pow]149    exact Ideal.map_mono fun x hx ↦150      hJ ((Ideal.map_pow (localCompletionMap A) _ L).le (Ideal.mem_map_of_mem _ hx))151  simpa using (I.map (localCompletionMap A)).add_mem (hML hdiff)152    (Ideal.mem_map_of_mem (localCompletionMap A)153      (show a ∈ I from (by simpa using J.sub_mem hb (hJ hdiff) : localCompletionMap A a ∈ J)))154 155/-- At a maximal ideal `P` of a Noetherian ring `A`, an ideal `J` of the completed local ring156containing a power of its maximal ideal makes `A → Â_P → Â_P/J` surjective. -/157theorem finite_completed_point_quotient_surjective (A : Type) [CommRing A] [IsNoetherianRing A]158    (P : Ideal A) [P.IsMaximal] (L : ℕ) (J : Ideal (CompletedLocalAt A P))159    (hJ : ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map160      (localCompletionMap (Localization.AtPrime P))) ^ L ≤ J) :161    Function.Surjective ((Ideal.Quotient.mk J).comp (completedPointMap A P)) := by162  intro y163  obtain ⟨x, rfl⟩ := completion_to_finite_quotient_surjective (Localization.AtPrime P) L J hJ y164  set φ := (Ideal.Quotient.mk J).comp (localCompletionMap (Localization.AtPrime P)) with hφ165  obtain ⟨⟨a, s⟩, rfl⟩ := IsLocalization.mk'_surjective P.primeCompl x166  obtain ⟨b, u, hu, hbu⟩ := (inferInstance : P.IsMaximal).exists_inv s.2167  have hu' : u = 1 - b * s := by rw [← hbu]; ring168  have hgeom : (b * ∑ i ∈ Finset.range L, u ^ i) * s = 1 - u ^ L := by169    rw [← mul_neg_geom_sum, hu']; ring170  have huL : φ (algebraMap A _ (u ^ L)) = 0 := by171    simp only [hφ, RingHom.comp_apply, map_pow]172    rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]173    exact hJ (Ideal.pow_mem_pow (Ideal.mem_map_of_mem _174      ((IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime P) P u).2 hu)) _)175  have hone : φ (algebraMap A _ ((b * ∑ i ∈ Finset.range L, u ^ i) * s)) = 1 := by176    rw [hgeom, map_sub, map_sub, huL, map_one, map_one, sub_zero]177  refine ⟨a * (b * ∑ i ∈ Finset.range L, u ^ i), ?_⟩178  have hmk : IsLocalization.mk' (Localization.AtPrime P) a s * algebraMap A _ (s : A)179      = algebraMap A _ a := IsLocalization.mk'_spec _ _ _180  change φ (algebraMap A _ _) = φ _181  calc φ (algebraMap A _ (a * (b * ∑ i ∈ Finset.range L, u ^ i)))182      = φ (IsLocalization.mk' (Localization.AtPrime P) a s * algebraMap A _ (s : A))183          * φ (algebraMap A _ (b * ∑ i ∈ Finset.range L, u ^ i)) := by184        rw [hmk, map_mul, map_mul]185    _ = φ (IsLocalization.mk' (Localization.AtPrime P) a s)186          * φ (algebraMap A _ ((b * ∑ i ∈ Finset.range L, u ^ i) * s)) := by187        simp only [map_mul]; ring188    _ = _ := by rw [hone, mul_one]189 190end SurfaceBlowup