Completeness of the concrete surface

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Surfaces.PowerSeries7import SurfaceBlowup.Unramified.FrobeniusDescent8import Mathlib.Algebra.Azumaya.Basic9import Mathlib.RingTheory.AdicCompletion.Completeness10import Mathlib.RingTheory.AdicCompletion.RingHom11import Mathlib.RingTheory.TotallySplit12 13/-!14# Completeness of the concrete surface15 16We study the concrete surface `O[[T,X]] / (π - u T^a X^b)` over a discrete valuation ring `O`:17the quotient by `t` is the power series ring over the residue field, ring maps out of18`O[[T,X]]` are determined by their values on constants and on nilpotent images of `T`, `X`,19and the surface (as well as its curve quotients) is adically complete for the parameter20ideal, the maximal ideal and the ideal `(π)`.21 22## Main results23 24* `concrete_surface_quotient_T_equiv`: `R / (t) ≃+* k[[X]]`.25* `concrete_surface_span_T_isPrime`: `(t)` is a prime ideal of the surface.26* `transverse_of_reduction_ne_zero`: a criterion for `g, e` to form a transverse pair.27* `twoSeries_ringHom_ext_of_isNilpotent`, `twoSeries_eval_exists_of_isAdicComplete`:28  uniqueness and existence of evaluations of two-variable power series.29* `concrete_surface_isAdicComplete_maximalIdeal`, `concrete_surface_isAdicComplete_span_pi`,30  `division_coordinate_module_isAdicComplete`: adic completeness statements.31 32Provenance: `surfaceRelation_span_axisT_{eq,isPrime}`, `concrete_surface_{quotient_T_equiv,33span_T_isPrime, ringHom_ext_of_isNilpotent, curve_isAdicComplete}`,34`transverse_of_reduction_ne_zero`, `twoSeries_{mem_variableIdeal_pow_of_coeff_eq_zero,35ringHom_ext_of_isNilpotent, eval_exists_of_isAdicComplete, isAdicComplete_variableIdeal}`,36`unramified_{lift_map_parameter_quotient_irreducible, root_isUnit_of_two_le_natDegree}`,37`variableIdeal_{eq_span_range_X, ne_top}`, `concrete_surface_isAdicComplete_{parameterIdeal,38maximalIdeal, span_pi, span_pi_base}`, `division_coordinate_module_isAdicComplete`.39-/40 41namespace SurfaceBlowup42 43/-! ### The quotient by `t` -/44 45/-- For `0 < a`, the ideals `(π - u T^a X^b, T)` and `(π, T)` of `O[[T,X]]` coincide. -/46private theorem surfaceRelation_span_axisT_eq (O : Type) [CommRing O] (pi : O) (u : (TwoSeries O)ˣ)47    (a b : ℕ) (ha : 0 < a) :48    Ideal.span {surfaceRelation O pi u a b, axisT O} =49      Ideal.span {(MvPowerSeries.C pi : TwoSeries O), axisT O} := by50  obtain ⟨a', rfl⟩ : ∃ a', a = a' + 1 := ⟨a - 1, by omega⟩51  rw [show surfaceRelation O pi u (a' + 1) b = MvPowerSeries.C pi +52      -((u : TwoSeries O) * axisT O ^ a' * axisX O ^ b) * axisT O by rw [surfaceRelation]; ring,53    Ideal.span_pair_add_mul_right]54 55/-- The quotient of the concrete surface by `t` is the power series ring `k[[X]]` over the56residue field, compatibly with `residueKillT`. -/57theorem concrete_surface_quotient_T_equiv (O : Type) [CommRing O] [IsDomain O]58    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)59    (ha : 0 < a) :60    ∃ q : (ConcreteSurface O pi u a b ⧸ Ideal.span {surfaceT O pi u a b}) ≃+*61        PowerSeries (IsLocalRing.ResidueField O),62      ∀ s : TwoSeries O, q (Ideal.Quotient.mk (Ideal.span {surfaceT O pi u a b})63        (surfaceMk O pi u a b s)) = residueKillT O s := by64  obtain ⟨-, -, -, hsurj, hker⟩ := residueKillT_apply_ker O pi hpi65  set I := surfaceIdeal O pi u a b66  set J : Ideal (TwoSeries O) := Ideal.span {axisT O}67  have h1 : Ideal.span {surfaceT O pi u a b} = J.map (Ideal.Quotient.mk I) := by68    rw [Ideal.map_span, Set.image_singleton]; rfl69  have h2 : I ⊔ J = RingHom.ker (residueKillT O) := by70    rw [hker, ← surfaceRelation_span_axisT_eq O pi u a b ha, Ideal.span_insert]; rfl71  exact ⟨((Ideal.quotEquivOfEq h1).trans (DoubleQuot.quotQuotEquivQuotSup I J)).trans72    ((Ideal.quotEquivOfEq h2).trans (RingHom.quotientKerEquivOfSurjective hsurj)), fun _ ↦ rfl⟩73 74/-- The ideal `(π - u T^a X^b, T)` of `O[[T,X]]` is prime when `π` is a uniformizer. -/75private theorem surfaceRelation_span_axisT_isPrime (O : Type) [CommRing O] [IsDomain O]76    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)77    (ha : 0 < a) :78    (Ideal.span {surfaceRelation O pi u a b, axisT O}).IsPrime := by79  rw [surfaceRelation_span_axisT_eq O pi u a b ha]80  simpa [axisT] using mvPowerSeries_fin_two_span_C_var_isPrime O pi81    (by rw [← hpi.maximalIdeal_eq]; infer_instance) 082 83/-- The ideal `(t)` of the concrete surface is prime. -/84theorem concrete_surface_span_T_isPrime (O : Type) [CommRing O] [IsDomain O]85    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)86    (ha : 0 < a) :87    (Ideal.span {surfaceT O pi u a b}).IsPrime := by88  have := surfaceRelation_span_axisT_isPrime O pi hpi u a b ha89  have hker : RingHom.ker (surfaceMk O pi u a b) ≤90      Ideal.span {surfaceRelation O pi u a b, axisT O} := by91    rw [surfaceMk, Ideal.mk_ker]92    exact Ideal.span_mono (by simp)93  have h0 : surfaceMk O pi u a b (surfaceRelation O pi u a b) = 0 :=94    Ideal.Quotient.eq_zero_iff_mem.2 (Ideal.subset_span rfl)95  have himg : (Ideal.span {surfaceRelation O pi u a b, axisT O}).map (surfaceMk O pi u a b) =96      Ideal.span {surfaceT O pi u a b} := by97    rw [Ideal.map_span, Set.image_pair, h0, Ideal.span_insert_zero]; rfl98  exact himg ▸ Ideal.map_isPrime_of_surjective Ideal.Quotient.mk_surjective hker99 100/-- Let `e` be a non-zero-divisor of a noetherian local ring `S` with `S / (e) ≃ k[[X]]`, and101let `g` have nonzero image in `k[[X]]`. Then `e` is a non-zero-divisor modulo `g`, `g` is a102non-zero-divisor modulo `e`, and `(g, e)` contains a power of the maximal ideal. -/103theorem transverse_of_reduction_ne_zero (S : Type) [CommRing S] [IsLocalRing S]104    [IsNoetherianRing S] (e g : S) (hereg : Function.Injective (fun y : S ↦ e * y)) (k : Type)105    [Field k] (q : (S ⧸ Ideal.span {e}) ≃+* PowerSeries k)106    (hg : q (Ideal.Quotient.mk (Ideal.span {e}) g) ≠ 0) :107    Function.Injective (fun a : S ⧸ Ideal.span {g} ↦ Ideal.Quotient.mk (Ideal.span {g}) e * a) ∧108      Function.Injective109        (fun a : S ⧸ Ideal.span {e} ↦ Ideal.Quotient.mk (Ideal.span {e}) g * a) ∧110      ∃ L : ℕ, (IsLocalRing.maximalIdeal S)^L ≤ Ideal.span {g, e} := by111  set π := Ideal.Quotient.mk (Ideal.span {e})112  have hker : ∀ x : S, q (π x) = 0 ↔ ∃ c, x = e * c := fun x ↦ by113    rw [map_eq_zero_iff q q.injective, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]114    exact Iff.rfl115  refine ⟨fun a a' h ↦ ?_, fun a a' h ↦ q.injective (mul_left_cancel₀ hg (by116    simpa only [map_mul] using congrArg q h)), ?_⟩117  · induction a using Quotient.inductionOn' with | h a => ?_118    induction a' using Quotient.inductionOn' with | h a' => ?_119    change Ideal.Quotient.mk _ e * Ideal.Quotient.mk _ a =120      Ideal.Quotient.mk _ e * Ideal.Quotient.mk _ a' at h121    change Ideal.Quotient.mk _ a = Ideal.Quotient.mk _ a'122    rw [← map_mul, ← map_mul, Ideal.Quotient.eq, Ideal.mem_span_singleton'] at h123    obtain ⟨b, hb⟩ := h124    have h0 : q (π g) * q (π b) = 0 := by125      rw [← map_mul, ← map_mul, mul_comm, hb, ← mul_sub]126      exact (hker _).2 ⟨_, rfl⟩127    obtain ⟨c, rfl⟩ := (hker b).1 ((mul_eq_zero.1 h0).resolve_left hg)128    rw [Ideal.Quotient.eq, Ideal.mem_span_singleton']129    exact ⟨c, hereg (by simp only; rw [mul_sub, ← hb]; ring)⟩130  · -- `(g, e)` contains `𝔪^L` with `L = ord_X (q ḡ)`: `𝔪^L` maps into `(X^L) = (q ḡ)` in `k[[X]]`.131    set p := q (π g)132    have hu : IsUnit p.divXPowOrder := by133      rw [PowerSeries.isUnit_iff_constantCoeff, isUnit_iff_ne_zero]134      exact fun h ↦ hg (PowerSeries.constantCoeff_divXPowOrder_eq_zero_iff.1 h)135    let f : S →+* PowerSeries k := (q : (S ⧸ Ideal.span {e}) →+* PowerSeries k).comp π136    have hfs : Function.Surjective f := q.surjective.comp Ideal.Quotient.mk_surjective137    refine ⟨p.order.toNat, fun x hx ↦ ?_⟩138    have hx' := Ideal.mem_map_of_mem f hx139    rw [Ideal.map_pow, IsLocalRing.map_maximalIdeal_of_surjective f hfs,140      PowerSeries.maximalIdeal_eq_span_X, Ideal.span_singleton_pow,141      Ideal.mem_span_singleton] at hx'142    obtain ⟨y, hy⟩ : f g ∣ f x := dvd_trans ⟨↑hu.unit⁻¹, by143      change _ = p * _144      rw [← mul_one (_ ^ _), ← hu.mul_val_inv, ← mul_assoc,145        PowerSeries.X_pow_order_mul_divXPowOrder]⟩ hx'146    obtain ⟨y, rfl⟩ := hfs y147    obtain ⟨c, hc⟩ := (hker _).1 (by148      change f (x - g * y) = 0149      rw [map_sub, map_mul, hy, sub_self])150    exact Ideal.mem_span_pair.2 ⟨y, c, by linear_combination -hc⟩151 152/-! ### Ring maps out of `O[[T,X]]` -/153 154/-- A two-variable power series all of whose coefficients of total degree `< N` vanish lies in155`(T, X)^N`. -/156private theorem twoSeries_mem_variableIdeal_pow_of_coeff_eq_zero (O : Type) [CommRing O] (N : ℕ)157    (g : TwoSeries O) (hg : ∀ m : Fin 2 →₀ ℕ, m 0 + m 1 < N → MvPowerSeries.coeff m g = 0) :158    g ∈ variableIdeal O ^ N :=159  (axis_ideal_pow_mem_iff O N g).2 hg160 161/-- Two ring maps out of `O[[T,X]]` that agree on constants, `T` and `X`, and send `T` and162`X` to nilpotent elements, are equal. -/163theorem twoSeries_ringHom_ext_of_isNilpotent (O S : Type) [CommRing O] [CommRing S]164    (φ ψ : TwoSeries O →+* S) (hC : ∀ c : O, φ (MvPowerSeries.C c) = ψ (MvPowerSeries.C c))165    (hT : φ (axisT O) = ψ (axisT O)) (hX : φ (axisX O) = ψ (axisX O))166    (hTn : IsNilpotent (φ (axisT O))) (hXn : IsNilpotent (φ (axisX O))) :167    φ = ψ := by168  obtain ⟨N, hN⟩ : IsNilpotent (Ideal.span {φ (axisT O), φ (axisX O)}) := by169    rw [Ideal.FG.isNilpotent_iff_le_nilradical (Submodule.fg_span (Set.toFinite _)),170      Ideal.span_le]171    rintro x (rfl | rfl)172    exacts [hTn, hXn]173  -- both maps kill `(T, X)^N`, whose image is generated by powers of `φ T, φ X`174  have kill (χ : TwoSeries O →+* S) (hχT : χ (axisT O) = φ (axisT O))175      (hχX : χ (axisX O) = φ (axisX O)) (g) (hg : g ∈ variableIdeal O ^ N) : χ g = 0 := by176    have : χ g ∈ ((variableIdeal O) ^ N).map χ := Ideal.mem_map_of_mem _ hg177    rw [Ideal.map_pow, variableIdeal, Ideal.map_span, Set.image_pair, hχT, hχX, hN] at this178    simpa using this179  have hpoly : φ.comp (MvPolynomial.coeToMvPowerSeries.ringHom (σ := Fin 2) (R := O)) =180      ψ.comp (MvPolynomial.coeToMvPowerSeries.ringHom) := by181    apply MvPolynomial.ringHom_ext182    · intro c183      simpa using hC c184    · intro s185      fin_cases s186      · simpa [axisT] using hT187      · simpa [axisX] using hX188  ext f189  set p := MvPowerSeries.truncTotal N f190  have hg : f - (p : TwoSeries O) ∈ variableIdeal O ^ N := by191    apply twoSeries_mem_variableIdeal_pow_of_coeff_eq_zero192    intro m hm193    rw [map_sub, MvPolynomial.coeff_coe, MvPowerSeries.coeff_truncTotal, sub_self]194    simpa [Finsupp.degree_eq_sum, Fin.sum_univ_two] using hm195  have h1 := kill φ rfl rfl _ hg196  have h2 := kill ψ hT.symm hX.symm _ hg197  rw [map_sub, sub_eq_zero] at h1 h2198  rw [h1, h2]199  exact congrArg (fun F ↦ F p) hpoly200 201/-- Two ring maps out of the concrete surface that agree on constants, `t` and `x`, and send202`t` and `x` to nilpotent elements, are equal. -/203theorem concrete_surface_ringHom_ext_of_isNilpotent (O S : Type) [CommRing O] [CommRing S]204    (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) (φ ψ : ConcreteSurface O pi u a b →+* S)205    (hC : ∀ c : O, φ (algebraMap O (ConcreteSurface O pi u a b) c) =206      ψ (algebraMap O (ConcreteSurface O pi u a b) c))207    (hT : φ (surfaceT O pi u a b) = ψ (surfaceT O pi u a b))208    (hX : φ (surfaceX O pi u a b) = ψ (surfaceX O pi u a b))209    (hTn : IsNilpotent (φ (surfaceT O pi u a b))) (hXn : IsNilpotent (φ (surfaceX O pi u a b))) :210    φ = ψ :=211  Ideal.Quotient.ringHom_ext212    (twoSeries_ringHom_ext_of_isNilpotent O S _ _ (fun c ↦ hC c) hT hX hTn hXn)213 214/-- Over a ring `S` complete for an ideal `I`, any ring map `O' → S` extends to an evaluation215`O'[[T,X]] → S` sending `T ↦ e` and `X ↦ z` for given `e, z ∈ I`. -/216theorem twoSeries_eval_exists_of_isAdicComplete (S : Type) [CommRing S] (I : Ideal S)217    [IsAdicComplete I S] (O' : Type) [CommRing O'] (κ : O' →+* S) (e z : S) (he : e ∈ I)218    (hz : z ∈ I) :219    ∃ Θ : TwoSeries O' →+* S,220      (∀ c : O', Θ (MvPowerSeries.C c) = κ c) ∧ Θ (axisT O') = e ∧ Θ (axisX O') = z := by221  have nil : ∀ (n : ℕ) (a : S), a ∈ I → IsNilpotent (Ideal.Quotient.mk (I ^ n) a) :=222    fun n a ha ↦ ⟨n, by223      rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]; exact Ideal.pow_mem_pow ha n⟩224  let f : (n : ℕ) → TwoSeries O' →+* S ⧸ I ^ n := fun n ↦225    nilpotentEval ((Ideal.Quotient.mk (I ^ n)).comp κ) (Ideal.Quotient.mk (I ^ n) e)226      (Ideal.Quotient.mk (I ^ n) z) (nil n e he) (nil n z hz)227  have hgen := fun n ↦ nilpotentEval_apply_generators O' (S ⧸ I ^ n)228      ((Ideal.Quotient.mk (I ^ n)).comp κ) (Ideal.Quotient.mk (I ^ n) e)229      (Ideal.Quotient.mk (I ^ n) z) (nil n e he) (nil n z hz)230  have hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m := by231    intro m n hle232    obtain ⟨hC, hT, hX⟩ := hgen n233    obtain ⟨hC', hT', hX'⟩ := hgen m234    apply twoSeries_ringHom_ext_of_isNilpotent235    · intro c; simp only [RingHom.comp_apply, f, hC, hC']; rfl236    · simp only [RingHom.comp_apply, f, hT, hT']; rfl237    · simp only [RingHom.comp_apply, f, hX, hX']; rfl238    · simp only [RingHom.comp_apply, f, hT]; exact (nil n e he).map _239    · simp only [RingHom.comp_apply, f, hX]; exact (nil n z hz).map _240  have hsep : ∀ a b : S, (∀ n : ℕ, Ideal.Quotient.mk (I ^ n) a = Ideal.Quotient.mk (I ^ n) b) →241      a = b := by242    intro a b h243    rw [IsHausdorff.eq_iff_smodEq (I := I)]244    intro n245    rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top, ← Ideal.Quotient.eq]246    exact h n247  refine ⟨IsAdicComplete.liftRingHom I f hf, fun c ↦ hsep _ _ fun n ↦ ?_,248    hsep _ _ fun n ↦ ?_, hsep _ _ fun n ↦ ?_⟩ <;> rw [IsAdicComplete.mk_liftRingHom]249  exacts [(hgen n).1 c, (hgen n).2.1, (hgen n).2.2]250 251/-! ### Unramified extensions -/252 253/-- The reduction of an unramified lift `Φ` to the quotient of the concrete surface by its254parameter ideal `(t, x)` is irreducible. -/255theorem unramified_lift_map_parameter_quotient_irreducible (O : Type) [CommRing O] [IsDomain O]256    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)257    (ha : 0 < a) (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) :258    Irreducible (Φ.map ((Ideal.Quotient.mk (Ideal.span ({surfaceT O pi u a b,259      surfaceX O pi u a b} : Set (ConcreteSurface O pi u a b)))).comp260        (algebraMap O (ConcreteSurface O pi u a b)))) := by261  have key : ∀ (R : Type) [CommRing R] (alg : O →+* R) (I : Ideal R)262      (e : R ⧸ I ≃+* IsLocalRing.ResidueField O),263      (∀ c, e (Ideal.Quotient.mk I (alg c)) = IsLocalRing.residue O c) →264      Irreducible (Φ.map ((Ideal.Quotient.mk I).comp alg)) := by265    intro R _ alg I e hc266    have hc' : e.toRingHom.comp ((Ideal.Quotient.mk I).comp alg) = IsLocalRing.residue O := by267      ext c; exact hc c268    have h := hΦ.2269    rw [residuePoly, ← hc', ← Polynomial.map_map] at h270    exact (MulEquiv.irreducible_iff (Polynomial.mapEquiv e).toMulEquiv).mp (by simpa using h)271  obtain ⟨e, he⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha272  exact key _ _ _ e fun c ↦ (he (.C c)).trans (congrArg _ (MvPowerSeries.constantCoeff_C ..))273 274/-- If `Φ` is an unramified lift of degree at least `2` over a complete local ring with finite275residue field, then the root of `Φ` in `O[X]/(Φ)` is a unit. -/276theorem unramified_root_isUnit_of_two_le_natDegree (O : Type) [CommRing O] [IsLocalRing O]277    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]278    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) (h2 : 2 ≤ Φ.natDegree) :279    IsUnit (AdjoinRoot.root Φ) := by280  obtain ⟨_, hunit, _⟩ := base_ideal_maximal_local O Φ hΦ281  apply hunit282  obtain ⟨hfield, _, _⟩ := residue_extension_field O Φ hΦ283  obtain ⟨e, he, _⟩ := residue_extension_equiv O Φ284  have hne : baseReduce O Φ (AdjoinRoot.root Φ) ≠ 0 := by285    intro h0286    have h1 : e (baseReduce O Φ (AdjoinRoot.mk Φ Polynomial.X)) = 0 := by287      rw [AdjoinRoot.mk_X, h0]; simp288    rw [he, Polynomial.map_X, AdjoinRoot.mk_eq_zero] at h1289    exact Polynomial.X_ne_zero (Polynomial.eq_zero_of_dvd_of_natDegree_lt h1290      (by rw [Polynomial.natDegree_X, hΦ.1.natDegree_map]; omega))291  let := hfield.toField292  exact isUnit_iff_ne_zero.mpr hne293 294/-! ### Adic completeness -/295 296/-- The ideal `(T, X)` is the span of the two variables of `O[[T,X]]`. -/297private theorem variableIdeal_eq_span_range_X (O : Type) [CommRing O] :298    variableIdeal O = Ideal.span (Set.range (MvPowerSeries.X : Fin 2 → TwoSeries O)) := by299  unfold variableIdeal300  congr 1301  ext x302  simp [axisT, axisX, Fin.exists_fin_two, eq_comm]303 304/-- `O[[T,X]]` is complete for the ideal `(T, X)`. -/305private theorem twoSeries_isAdicComplete_variableIdeal (O : Type) [CommRing O] :306    IsAdicComplete (variableIdeal O) (TwoSeries O) := by307  rw [variableIdeal_eq_span_range_X]308  infer_instance309 310/-- Over a nontrivial ring, `(T, X)` is a proper ideal of `O[[T,X]]`. -/311private theorem variableIdeal_ne_top (O : Type) [CommRing O] [Nontrivial O] :312    variableIdeal O ≠ ⊤ := by313  intro h314  have h1 : (1 : TwoSeries O) ∈ variableIdeal O := h ▸ Submodule.mem_top315  rw [variableIdeal, axisT, axisX, mvPowerSeries_fin_two_mem_variableIdeal_iff] at h1316  simp at h1317 318/-- The concrete surface is complete for its parameter ideal `(t, x)`. -/319theorem concrete_surface_isAdicComplete_parameterIdeal (O : Type) [CommRing O] [IsLocalRing O]320    [IsNoetherianRing O] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ) :321    IsAdicComplete (surfaceParameterIdeal O pi u a b) (ConcreteSurface O pi u a b) := by322  have := twoSeries_isAdicComplete_variableIdeal O323  have e : surfaceParameterIdeal O pi u a b =324      (variableIdeal O).map (Ideal.Quotient.mk (surfaceIdeal O pi u a b)) := by325    unfold surfaceParameterIdeal variableIdeal326    rw [Ideal.map_span, Set.image_pair]327    rfl328  exact e ▸ isAdicComplete_quotient_of_iInf_sup_pow (TwoSeries O) (variableIdeal O)329    (surfaceIdeal O pi u a b)330    (iInf_sup_pow_eq_of_isLocalRing (TwoSeries O) _ _ (variableIdeal_ne_top O))331 332/-- The concrete surface is complete for its maximal ideal. -/333theorem concrete_surface_isAdicComplete_maximalIdeal (O : Type) [CommRing O] [IsDomain O]334    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)335    (ha : 0 < a) [IsLocalRing (ConcreteSurface O pi u a b)] :336    IsAdicComplete (IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b))337      (ConcreteSurface O pi u a b) := by338  rw [concrete_surface_maximalIdeal_eq O pi hpi u a b ha]339  exact concrete_surface_isAdicComplete_parameterIdeal O pi u a b340 341/-- The concrete surface is complete for the ideal generated by the image of `π`. -/342theorem concrete_surface_isAdicComplete_span_pi (O : Type) [CommRing O] [IsDomain O]343    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)344    (ha : 0 < a) :345    IsAdicComplete (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})346      (ConcreteSurface O pi u a b) := by347  have : IsLocalRing (ConcreteSurface O pi u a b) :=348    concrete_surface_isLocalRing O pi u a b hpi.not_isUnit ha349  have : IsNoetherianRing (ConcreteSurface O pi u a b) :=350    concrete_surface_isNoetherianRing O pi u a b351  have := concrete_surface_isAdicComplete_maximalIdeal O pi hpi u a b ha352  apply isAdicComplete_of_isAdicComplete_maximalIdeal353  have hle : Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi} ≤354      IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b) := by355    rw [Ideal.span_singleton_le_iff_mem, concrete_surface_maximalIdeal_eq O pi hpi u a b ha]356    have h2 : surfaceMk O pi u a b (surfaceRelation O pi u a b) = 0 :=357      Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span rfl)358    have h3 : surfaceMk O pi u a b (MvPowerSeries.C pi) =359        (surfaceUnit O pi u a b : ConcreteSurface O pi u a b) * surfaceT O pi u a b ^ a *360          surfaceX O pi u a b ^ b := by361      have := sub_eq_zero.mp (by simpa [surfaceRelation, map_sub, map_mul, map_pow] using h2)362      simpa [surfaceUnit, surfaceT, surfaceX, map_mul, map_pow] using this363    rw [show algebraMap O (ConcreteSurface O pi u a b) pi =364      surfaceMk O pi u a b (MvPowerSeries.C pi) from rfl, h3]365    exact Ideal.mul_mem_right _ _ (Ideal.mul_mem_left _ _366      (Ideal.pow_mem_of_mem _ (Ideal.subset_span (by simp)) a ha))367  exact ne_top_of_le_ne_top (IsLocalRing.maximalIdeal.isMaximal _).ne_top hle368 369/-- Every principal quotient of the concrete surface is `π`-adically complete. -/370theorem concrete_surface_curve_isAdicComplete (O : Type) [CommRing O] [IsDomain O]371    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)372    (ha : 0 < a) (f : ConcreteSurface O pi u a b) :373    IsAdicComplete (Ideal.span {pi} : Ideal O) (ConcreteSurface O pi u a b ⧸ Ideal.span {f}) := by374  have : IsLocalRing (ConcreteSurface O pi u a b) :=375    concrete_surface_isLocalRing O pi u a b hpi.not_isUnit ha376  have : IsNoetherianRing (ConcreteSurface O pi u a b) :=377    concrete_surface_isNoetherianRing O pi u a b378  have hI := concrete_surface_isAdicComplete_span_pi O pi hpi u a b ha379  have hItop : Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi} ≠ ⊤ := fun h ↦ by380    have hH := hI.toIsHausdorff381    rw [h] at hH382    exact not_subsingleton _ hH.subsingleton383  have hc := isAdicComplete_quotient_of_iInf_sup_pow _ _ (Ideal.span {f})384    (iInf_sup_pow_eq_of_isLocalRing _ _ (Ideal.span {f}) hItop)385  rw [← IsAdicComplete.map_algebraMap_iff (S := ConcreteSurface O pi u a b ⧸ Ideal.span {f}),386    Ideal.map_span]387  rw [Ideal.map_span] at hc388  simp only [Set.image_singleton] at hc ⊢389  convert hc using 2390  rfl391 392/-- The concrete surface is `π`-adically complete as an `O`-module. -/393theorem concrete_surface_isAdicComplete_span_pi_base (O : Type) [CommRing O] [IsDomain O]394    [IsDiscreteValuationRing O] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ)395    (ha : 0 < a) :396    IsAdicComplete (Ideal.span {pi} : Ideal O) (ConcreteSurface O pi u a b) :=397  (IsAdicComplete.map_algebraMap_iff (S := ConcreteSurface O pi u a b) _ _).1 <| by398    rw [Ideal.map_span, Set.image_singleton]399    exact concrete_surface_isAdicComplete_span_pi O pi hpi u a b ha400 401/-- Over a complete discrete valuation ring, `Oⁿ × R` is `π`-adically complete, where `R` is the402concrete surface. -/403theorem division_coordinate_module_isAdicComplete (O : Type) [CommRing O] [IsDomain O]404    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (pi : O)405    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a) (n : ℕ) :406    IsAdicComplete (Ideal.span {pi} : Ideal O) ((Fin n → O) × ConcreteSurface O pi u a b) := by407  have : IsAdicComplete (Ideal.span {pi} : Ideal O) O :=408    dvr_isAdicComplete_span_uniformizer O pi hpi409  have : IsAdicComplete (Ideal.span {pi} : Ideal O) (Fin n → O) :=410    finite_free_adic_complete O (Fin n → O) _411  have := concrete_surface_isAdicComplete_span_pi_base O pi hpi u a b ha412  exact isAdicComplete_prod O _ _ _413 414end SurfaceBlowup