Strict transforms and the strict normalizer

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.NilpotentGluing7import SurfaceBlowup.Measure.StateVolumes8 9/-!10# Strict transforms and the strict normalizer11 12This file studies strict transforms of curves on the concrete surfaces13`O⟦t, x⟧ ⧸ (pi - u tᵃ xᵇ)` under the blow-up of the closed point. It computes the local14intersection data of a strict transform with the exceptional divisor, proves that functions of15finite contact on the special fiber are nonzerodivisors, and develops the *strict normalizer*:16the change of coordinates showing that, on a `pi`-adic coordinate box, strict transforms of a17perturbed generator `f + pi ^ (s + a) • ℓ(z)` are again perturbations of the strict transform18`g`, with an explicitly scaled coordinate map. It also computes the cokernel of the induced map19of quotient modules and transports strict transforms between the two blow-up charts.20 21## Main results22 23* `concrete_strict_transform_multiplicity`: intersection length with the exceptional divisor24  equals the multiplicity of the corresponding factor of the tangent form.25* `strict_transform_mapsTo_child_ideals`: strict transforms send a fixed tangent cell into the26  child ideal sets (Proposition 5.1, maps-to part).27* `special_fiber_crossing_contact_regular`, `special_fiber_single_contact_regular`.28* `strict_chart_coordinates_commute`, `strict_chart_preimage_set_identity`: the strict29  normalizer in chart coordinates.30* `strict_quotient_cokernel_length`: the cokernel length `s * N - tri d`.31* `cell_strict_transforms_agree_at_datum_points`,32  `strict_transforms_give_level_lattice_membership`.33 34Provenance: `Thm_SurfaceBlowupV2_*` nodes `concrete_strict_transform_{reduction_ne_zero,35transverse_finite, multiplicity}`, `prop_5_1_mapsTo`, `{scalar,power}_normalizer_*`,36`normalized_{coordinate_equation, quadratic_preserves_congruence}`, `scaled_{inverse_from_image_37containment, linear_image_index}`, `coordinate_scale_measure`, `special_fiber_{crossing,single}_38contact_regular`, `concrete_surface_single_curve_free`, `strict_{correction_raises_order,39normalizer_*, pullback_*, chart_*, quotient_*}`, `actual_strict_map_is_scaled_normalizer`,40`strict_transform_{common_point_transport, equation_from_levels}`,41`cell_strict_transforms_agree_at_datum_points`, `strict_transforms_give_level_lattice_membership`.42-/43 44open scoped BigOperators ENNReal45 46namespace SurfaceBlowup47 48/-! ### Strict transforms on concrete surfaces -/49 50/-- If the strict transform `FA` of `f` has nonzero reduction on the exceptional divisor, then51the completed local ring at an exceptional point is again a concrete surface in which the image52of `FA` has nonzero reduction modulo the new `t`. -/53private theorem concrete_strict_transform_reduction_ne_zero (O : Type) [CommRing O] [IsDomain O]54    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]55    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)56    (a b : ℕ) (ha : 0 < a) (FA : (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)57    (surfaceX O pi u a b))) (hne : Ideal.Quotient.mk58    (chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) FA ≠59    0) (P : Ideal (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)60    (surfaceX O pi u a b))) [P.IsMaximal] [P.IsPrime]61    (hP : (chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))62    (surfaceT O pi u a b) ∈ P) : ∃ (O' : Type) (_ : CommRing O') (_ : IsDomain O')63    (_ : IsDiscreteValuationRing O') (_ : IsAdicComplete (IsLocalRing.maximalIdeal O') O')64    (_ : Finite (IsLocalRing.ResidueField O')) (pi' : O') (u' : (TwoSeries O')ˣ) (a' b' : ℕ),65    Irreducible pi' ∧ 0 < a' ∧ ∃ (Eq : CompletedLocalAt66    (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) P ≃+*67    ConcreteSurface O' pi' u' a' b') (q : (ConcreteSurface O' pi' u' a' b' ⧸ Ideal.span68    {surfaceT O' pi' u' a' b'}) ≃+* PowerSeries (IsLocalRing.ResidueField O')), Eq69    (completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)70    (surfaceX O pi u a b)) P ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)71    (surfaceX O pi u a b)) (surfaceT O pi u a b))) = surfaceT O' pi' u' a' b' ∧ q72    (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'})73    (Eq (completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)74    (surfaceX O pi u a b)) P FA))) ≠ 0 := by75  have : IsLocalRing (ConcreteSurface O pi u a b) :=76    concrete_surface_isLocalRing O pi u a b hpi.not_isUnit ha77  have hm : IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b) =78      Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set _) :=79    concrete_surface_maximalIdeal_eq O pi hpi u a b ha80  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set _)).IsMaximal :=81    hm ▸ IsLocalRing.maximalIdeal.isMaximal _82  obtain ⟨e0, he0, he0Z⟩ := exceptional_line_equiv_chart_exceptional (ConcreteSurface O pi u a b)83      (surfaceT O pi u a b) (surfaceX O pi u a b)84  let iso : (ConcreteSurface O pi u a b ⧸ Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} :85      Set _)) ≃+* IsLocalRing.ResidueField (ConcreteSurface O pi u a b) :=86    Ideal.quotEquivOfEq hm.symm87  let e := e0.trans (Polynomial.mapEquiv iso)88  have he : ∀ r, e (Ideal.Quotient.mk _ (chartBase _ _ _ r)) =89      Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r) := fun r ↦ by90    simp only [e, RingEquiv.trans_apply, he0, Polynomial.mapEquiv_apply, Polynomial.map_C]91    rfl92  have heZ : e (Ideal.Quotient.mk _ (chartSlope _ _ _)) = Polynomial.X := by simp [e, he0Z]93  obtain ⟨φ, hmon, hirr, hPφ, -, -⟩ :=94    blowup_chart_exceptional_point_polynomial (ConcreteSurface O pi u a b) (surfaceT O pi u a b)95        (surfaceX O pi u a b) e0 he0 he0Z P hP96  have hφ' : (φ.map iso.toRingHom).Monic ∧ Irreducible (φ.map iso.toRingHom) :=97    ⟨hmon.map _, (MulEquiv.irreducible_iff (Polynomial.mapEquiv iso)).mpr hirr⟩98  have hPφ' : (P.map (Ideal.Quotient.mk _)).map e = Ideal.span {φ.map iso.toRingHom} := by99    have h1 : ∀ J : Ideal _, Ideal.map e J =100        Ideal.map (Polynomial.mapEquiv iso) (Ideal.map e0 J) := fun J ↦ by101      change Ideal.map e.toRingHom J =102        Ideal.map (Polynomial.mapEquiv iso).toRingHom (Ideal.map e0.toRingHom J)103      rw [Ideal.map_map]104      rfl105    rw [h1, hPφ, Ideal.map_span, Set.image_singleton]106    rfl107  obtain ⟨O', i1, i2, i3, i4, i5, pi', u', a', b', hpi', ha', Eq, q, ι, alphaBar, hT, -, hF⟩ :=108    concrete_strict_transform_residue_series O pi hpi u a b ha P hP e he heZ _ hφ' hPφ'109  refine ⟨O', i1, i2, i3, i4, i5, pi', u', a', b', hpi', ha', Eq, q, hT, ?_⟩110  rw [hF FA, Ne, Polynomial.coe_eq_zero_iff, ← Polynomial.taylor_apply]111  simpa [Polynomial.map_eq_zero_iff ι.injective] using hne112 113/-- At an exceptional point of the blow-up chart, the strict transform `FA` and the exceptional114equation `t` are mutually regular in the completed local ring, and some power of the maximal115ideal lies in the local curve ideal they cut out. -/116theorem concrete_strict_transform_transverse_finite (O : Type) [CommRing O] [IsDomain O]117    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]118    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)119    (a b : ℕ) (ha : 0 < a) (FA : (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)120    (surfaceX O pi u a b))) (hne : Ideal.Quotient.mk121    (chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) FA ≠122    0) (P : Ideal (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)123    (surfaceX O pi u a b))) [P.IsMaximal] [P.IsPrime]124    (hP : (chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))125    (surfaceT O pi u a b) ∈ P) : Function.Injective126    (fun w : CompletedLocalAt (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)127    (surfaceX O pi u a b)) P ⧸ Ideal.span {completedPointMap128    (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) P FA} =>129    Ideal.Quotient.mk (Ideal.span {completedPointMap130    (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) P FA})131    (completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)132    (surfaceX O pi u a b)) P ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)133    (surfaceX O pi u a b)) (surfaceT O pi u a b))) * w) ∧ Function.Injective134    (fun w : CompletedLocalAt (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)135    (surfaceX O pi u a b)) P ⧸ Ideal.span {completedPointMap136    (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) P137    ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))138    (surfaceT O pi u a b))} => Ideal.Quotient.mk139    (Ideal.span {completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)140    (surfaceX O pi u a b)) P ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)141    (surfaceX O pi u a b)) (surfaceT O pi u a b))})142    (completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)143    (surfaceX O pi u a b)) P FA) * w) ∧ ∃ L : ℕ,144    ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map145    (localCompletionMap (Localization.AtPrime P)))^L ≤ finiteLocalCurveIdeal146    (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) P147    ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))148    (surfaceT O pi u a b)) (completedPointMap149    (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) P FA)150    1 := by151  obtain ⟨hN, hD, hL, hC⟩ := concrete_left_point_completion_instances O pi hpi u a b ha P hP152  have hreg := concrete_left_point_exceptional_regular O pi hpi u a b ha P hP153  obtain ⟨O', c1, c2, c3, c4, c5, pi', u', a', b', hpi', ha', Eq, q, hEq, hq⟩ :=154    concrete_strict_transform_reduction_ne_zero O pi hpi u a b ha FA hne P hP155  let e1 := Ideal.quotientEquiv (Ideal.span {completedPointMap _ P156    (chartBase _ (surfaceT O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b))})157    (Ideal.span {surfaceT O' pi' u' a' b'}) Eq (by158      rw [Ideal.map_span, Set.image_singleton]; exact congrArg (Ideal.span {·}) hEq.symm)159  obtain ⟨k1, k2, L, hL'⟩ := transverse_of_reduction_ne_zero _ _ _ hreg160    (IsLocalRing.ResidueField O') (e1.trans q) hq161  refine ⟨k1, k2, L, ?_⟩162  rw [finiteLocalCurveIdeal, pow_one]163  convert hL' using 2164  all_goals exact (AdicCompletion.maximalIdeal_eq_map (R := Localization.AtPrime P)).symm165 166/-- The order of a nonzero polynomial viewed as a power series is its trailing degree. -/167private theorem order_coe_polynomial {K : Type} [Field K] (H : Polynomial K) (hH : H ≠ 0) :168    (H : PowerSeries K).order = (H.natTrailingDegree : ℕ∞) := by169  rw [PowerSeries.order_eq_nat]170  refine ⟨?_, ?_⟩171  · rw [Polynomial.coeff_coe]172    exact mt Polynomial.trailingCoeff_eq_zero.mp hH173  · intro i hi174    rw [Polynomial.coeff_coe]175    exact Polynomial.coeff_eq_zero_of_lt_natTrailingDegree hi176 177open scoped Classical in178/-- The local intersection length of the strict transform with the exceptional divisor at the179point `P` equals the multiplicity of the irreducible factor `φ` (defining `P`) in the reduced180tangent form `∑ cᵢ Xⁱ`. -/181theorem concrete_strict_transform_multiplicity (O : Type) [CommRing O] [IsDomain O](4.6)182    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]183    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)184    (a b : ℕ) (ha : 0 < a) (d : ℕ) (c : Fin (d + 1) → ConcreteSurface O pi u a b)185    (hne : ∃ i : Fin (d + 1), c i ∉ Ideal.span {(surfaceT O pi u a b), (surfaceX O pi u a b)})186    [IsLocalRing (ConcreteSurface O pi u a b)]187    (P : Ideal (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)188    (surfaceX O pi u a b))) [P.IsMaximal] [P.IsPrime]189    (hP : (chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))190    (surfaceT O pi u a b) ∈ P) (e : ((BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)191    (surfaceX O pi u a b)) ⧸ chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b)192    (surfaceX O pi u a b)) ≃+* Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))193    (he : ∀ r : (ConcreteSurface O pi u a b), e194    (Ideal.Quotient.mk (chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b)195    (surfaceX O pi u a b)) ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)196    (surfaceX O pi u a b)) r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))197    (heZ : e (Ideal.Quotient.mk (chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b)198    (surfaceX O pi u a b)) (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b)199    (surfaceX O pi u a b))) = Polynomial.X) (φ : Polynomial200    (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) (hφ : φ.Monic ∧ Irreducible φ)201    (hPφ : (P.map (Ideal.Quotient.mk (chartExceptional (ConcreteSurface O pi u a b)202    (surfaceT O pi u a b) (surfaceX O pi u a b)))).map e = Ideal.span {φ}) : Module.length203    (CompletedLocalAt (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)204    (surfaceX O pi u a b)) P) (CompletedLocalAt205    (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) P ⧸206    Ideal.span {completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)207    (surfaceX O pi u a b)) P (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)208    (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) (c i) *209    (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))^i.val),210    completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)211    (surfaceX O pi u a b)) P ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)212    (surfaceX O pi u a b)) (surfaceT O pi u a b))}) =213    (Multiset.count φ (UniqueFactorizationMonoid.normalizedFactors214    (∑ i : Fin (d+1), Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) (c i)) *215    Polynomial.X^i.val : Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))) :216    ℕ∞) := by217  have h461 := concrete_surface_maximalIdeal_eq O pi hpi u a b ha218  obtain ⟨e0, -⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha219  let κ : IsLocalRing.ResidueField (ConcreteSurface O pi u a b) ≃+* IsLocalRing.ResidueField O :=220    (Ideal.quotEquivOfEq h461).trans e0221  have : Finite (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) :=222    Finite.of_equiv _ κ.symm.toEquiv223  obtain ⟨O', i1, i2, i3, i4, i5, pi', u', a', b', hpi', ha', Eq, q, ι, alphaBar, hT, hroot, hF⟩ :=224    concrete_strict_transform_residue_series O pi hpi u a b ha P hP e he heZ φ hφ hPφ225  set FA := (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)226      (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) (c i) *227      (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))^i.val)228  set Fbar :=229      (∑ i : Fin (d+1), Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) (c i)) *230      Polynomial.X^i.val : Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))231  have hred : e (Ideal.Quotient.mk _ FA) = Fbar := by232    simp only [FA, Fbar, map_sum, map_mul, map_pow, heZ]233    exact Finset.sum_congr rfl fun i _ ↦ by rw [← he (c i)]; rfl234  have hFne : Fbar ≠ 0 := by235    obtain ⟨i, hi⟩ := hne236    intro h0237    have hc := congrArg (fun p => Polynomial.coeff p i.val) h0238    simp only [Fbar, Polynomial.finsetSum_coeff, Polynomial.coeff_C_mul_X_pow,239      Polynomial.coeff_zero] at hc240    rw [Finset.sum_eq_single i (fun j _ hj => if_neg fun hji => hj (Fin.ext hji.symm))241      (by simp)] at hc242    exact hi (by rw [← h461, ← IsLocalRing.residue_eq_zero_iff]; simpa using hc :243      c i ∈ surfaceParameterIdeal O pi u a b)244  have hL := (concrete_surface_equiv_curve_length_and_regular _ O' pi' u' a' b' Eq q245    (completedPointMap _ P FA)).1246  rw [show Eq.symm (surfaceT O' pi' u' a' b') = completedPointMap _ P (chartBase _ _ _247    (surfaceT O pi u a b)) by rw [← hT, RingEquiv.symm_apply_apply]] at hL248  rw [hL, hF FA, hred]249  have hH : (Fbar.map ι).comp (Polynomial.X + Polynomial.C alphaBar) ≠ 0 := by250    rw [← Polynomial.taylor_apply]251    simpa [Polynomial.map_eq_zero_iff ι.injective] using hFne252  rw [order_coe_polynomial _ hH, ← Polynomial.rootMultiplicity_eq_natTrailingDegree,253    rootMultiplicity_map_eq_count_normalizedFactors _ _ ι Fbar hFne φ hφ alphaBar hroot]254 255/-- Proposition 5.1 (maps-to part): taking strict transforms at all exceptional points sends the256fixed tangent cell of state `s` and degree `d` into the product of the child ideal sets. -/257theorem strict_transform_mapsTo_child_ideals (O : Type) [CommRing O] [IsDomain O](4.7)–(4.8)258    [IsDiscreteValuationRing O]259    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)260    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)261    [IsDomain (ConcreteSurface O pi u a b)] [IsRegularLocalRing (ConcreteSurface O pi u a b)]262    (S : SurfaceData O (ConcreteSurface O pi u a b))263    (hS : S.t = (surfaceT O pi u a b) ∧ S.x = (surfaceX O pi u a b) ∧ S.a = a ∧ S.b = b)264    (e : ((BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) ⧸265    chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) ≃+*266    Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))267    (he : ∀ r : (ConcreteSurface O pi u a b), e268    (Ideal.Quotient.mk269    (chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))270    ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) r)) =271    Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))272    (heZ : e (Ideal.Quotient.mk273    (chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))274    (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))) =275    Polynomial.X) (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))276    (hinf : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)277    (surfaceX O pi u a b)).IsPrime) (s : State) (d : ℕ) :278    Set.MapsTo (fun J Q => divisorStrictTransform (ConcreteSurface O pi u a b) (surfaceT O pi u a b)279      (surfaceX O pi u a b) e Dv hinf d J Q)280      (fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv)281      (Set.pi Set.univ282      (childIdealSet (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv283      hinf s d)) := by284  intro J hJ285  obtain ⟨f, c, H, hJf, hc, hH, hcH, hne⟩ :=286    fixed_tangent_cell_generator_coefficients O _ S s d Dv J hJ287  obtain ⟨hSt, hSx, -, hSb⟩ := hS288  rw [hSt, hSx] at hc hne289  have hstate := hJ.1290  subst hJf291  have hHBAR := reduced_form_eq_of_residue_coeff _ d c H hH.2.1 hcH292  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set _)).IsMaximal :=293    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha294  have hinfmax := infinity_point_maximal O _ S295  rw [hSt, hSx] at hinfmax296  have : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)297      (surfaceX O pi u a b)).IsMaximal := hinfmax.1298  have key : ∀ (n : ℕ) (ℓ : ℕ∞), (n : ℕ∞) = d + ℓ → ℓ = ((n - d : ℕ) : ℕ∞) := by299    intro n ℓ h300    lift ℓ to ℕ using (by rintro rfl; simp at h)301    norm_cast at h ⊢302    omega303  have hT : Module.length (ConcreteSurface O pi u a b) (ConcreteSurface O pi u a b ⧸304      (Ideal.span {f} ⊔ Ideal.span {surfaceT O pi u a b})) = (stateContactT s : ℕ∞) := by305    obtain ⟨_, _, hm⟩ := hstate306    cases s with307    | single a' c' => rw [← hSt]; exact hm.2.2308    | crossing a' b' c' h' => rw [← hSt]; exact hm.2.2.1309  have hdir := directionPoint_properties _ _ _ e he heZ310  rw [Set.mem_univ_pi]311  rintro ⟨_ | φ, hQ⟩312  · have := (hdir.1 (zeroAffine _)).1313    have hmul := concrete_infinity_strict_transform_multiplicity O pi hpi u a b ha d c hne _314      hinfmax.2.1 hinfmax.2.2.1315    rw [hHBAR, Ideal.span_insert, ← hH.2.2.1] at hmul316    simp only [childIdealSet, divisorStrictTransform]317    rw [(concrete_strict_transform_generators O pi hpi u a b ha d f c hc _318      (hdir.1 (zeroAffine _)).2.1 _ hinfmax.2.1 hinfmax.2.2.1).2]319    exact ⟨⟨_, rfl⟩, hmul, fun _ ↦ key _ _ (hT.symm.trans (concrete_infinity_boundary_contact320      O pi hpi u a b ha d f c hc _ hinfmax.2.1 hinfmax.2.2.1)),321      fun h ↦ absurd h (by simp [zeroDirection])⟩322  · have := (hdir.1 φ).1323    have hmul := concrete_strict_transform_multiplicity O pi hpi u a b ha d c hne _324      (hdir.1 φ).2.1 e he heZ φ.val φ.property (hdir.1 φ).2.2.2325    rw [hHBAR, hH.2.2.2, (count_normalizedFactors_divisorAffinePolynomial _ Dv _326      (Polynomial.leadingCoeff_ne_zero.mpr hH.1) φ).1, Ideal.span_insert] at hmul327    simp only [childIdealSet, divisorStrictTransform]328    rw [(concrete_strict_transform_generators O pi hpi u a b ha d f c hc _ (hdir.1 φ).2.1 _329      hinfmax.2.1 hinfmax.2.2.1).1]330    refine ⟨⟨_, rfl⟩, hmul, fun h ↦ absurd h (by simp), fun hz h hsh ↦ ?_⟩331    obtain rfl : φ = zeroAffine _ := Option.some.inj hz332    obtain ⟨_, hv, hm⟩ := hstate333    cases s with334    | single a' c' => simp [stateContactX] at hsh335    | crossing a' b' c' h' =>336      simp only [stateContactX, Option.some.injEq] at hsh337      subst hsh338      have hb : 0 < b := by rw [← hSb, hm.2.1]; exact hv.2.1339      exact key _ _ ((hSx ▸ hm.2.2.2).symm.trans340        (concrete_zero_boundary_contact O pi hpi u a b ha hb d f c hc _ hdir.2.2))341 342/-! ### Normal forms of perturbed generators -/343 344/-- For `rho ∈ I`, the coordinate remainder map `coordinateRemainder rho b E` raises the345`I`-adic order of congruences by one. -/346private theorem scalar_normalizer_raises_order (O R : Type) [CommRing O] [CommRing R] [Algebra O R]347    (n : ℕ)348    (I : Ideal O) (rho : O) (hrho : rho ∈ I) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R)) :349    RaisesAdicOrder I (coordinateRemainder rho b E) := by350  -- linear maps preserve I^j • ⊤351  have hlin : ∀ {M N : Type} [AddCommGroup M] [Module O M] [AddCommGroup N] [Module O N]352      (L : M →ₗ[O] N) (j : ℕ) (m : M), m ∈ (I ^ j • ⊤ : Submodule O M) →353      L m ∈ (I ^ j • ⊤ : Submodule O N) := by354    intro M N _ _ _ _ L j m hm355    have : L m ∈ Submodule.map L (I ^ j • ⊤ : Submodule O M) := ⟨m, hm, rfl⟩356    rw [Submodule.map_smul''] at this357    exact Submodule.smul_mono le_rfl le_top this358  -- I^j • ⊤ in R is closed under multiplication by R359  have hmul : ∀ (j : ℕ) (c u : R), u ∈ (I ^ j • ⊤ : Submodule O R) →360      c * u ∈ (I ^ j • ⊤ : Submodule O R) := fun j c u hu => hlin (LinearMap.mulLeft O c) j u hu361  -- rho raises order362  have hsmul : ∀ {M : Type} [AddCommGroup M] [Module O M] (j : ℕ) (m : M),363      m ∈ (I ^ j • ⊤ : Submodule O M) → rho • m ∈ (I ^ (j+1) • ⊤ : Submodule O M) := by364    intro M _ _ j m hm365    rw [pow_succ', Submodule.mul_smul]366    exact Submodule.smul_mem_smul hrho hm367  let Lb : (Fin n → O) →ₗ[O] R := ∑ i, (LinearMap.proj i).smulRight (b i)368  have hLb : ∀ z, coordinateLift b z = Lb z := fun z => by simp [Lb, coordinateLift]369  intro j x y hxy370  unfold adicCongr at hxy ⊢371  have h1 : x.1 - y.1 ∈ (I ^ j • ⊤ : Submodule O (Fin n → O)) := by372    simpa using hlin (LinearMap.fst O (Fin n → O) R) j _ hxy373  have h2 : x.2 - y.2 ∈ (I ^ j • ⊤ : Submodule O R) := by374    simpa using hlin (LinearMap.snd O (Fin n → O) R) j _ hxy375  have h3 : coordinateLift b x.1 - coordinateLift b y.1 ∈ (I ^ j • ⊤ : Submodule O R) := by376    simpa [hLb] using hlin Lb j _ h1377  have h4 : x.2 * coordinateLift b x.1 - y.2 * coordinateLift b y.1378      ∈ (I ^ j • ⊤ : Submodule O R) := by379    have : x.2 * coordinateLift b x.1 - y.2 * coordinateLift b y.1380        = x.2 * (coordinateLift b x.1 - coordinateLift b y.1)381          + coordinateLift b y.1 * (x.2 - y.2) := by ring382    rw [this]383    exact Submodule.add_mem _ (hmul _ _ _ h3) (hmul _ _ _ h2)384  have h5 := hsmul j _ (hlin E.toLinearMap j _ h4)385  unfold coordinateRemainder386  rw [← smul_sub]387  simpa using h5388 389/-- The generator normal form is a right inverse of the adic perturbation by the coordinate390remainder of `pi ^ a`: perturbing `generatorNormalForm h` recovers `E h`. -/391private theorem power_normalizer_inverse_equation (O R : Type) [CommRing O] [CommRing R]392    [Algebra O R]393    (n : ℕ) (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))394    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (ha : 0 < a) (h : R) :395    adicPerturb (coordinateRemainder (pi^a) b E) (generatorNormalForm (pi^a) b E h) = E h := by396  have hmem : pi ^ a ∈ Ideal.span {pi} :=397    Ideal.pow_mem_of_mem _ (Ideal.mem_span_singleton_self pi) a ha398  have hr := scalar_normalizer_raises_order O R n (Ideal.span {pi}) (pi ^ a) hmem b E399  have hbij := adic_perturb_bijective O ((Fin n → O) × R) (Ideal.span {pi}) _ hr400  exact Function.rightInverse_invFun hbij.2 (E h)401 402/-- Coordinate equation satisfied by the normal form of `H z`: its first component plus403`pi ^ a` times the normalization quadratic equals the linear part404`normalizationLinearPart E H z`. -/405private theorem normalized_coordinate_equation (O R : Type) [CommRing O] [CommRing R] [Algebra O R]406    (n : ℕ)407    (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))408    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (H : (Fin n → O) →ₗ[O] R) (ha : 0 < a)409    (z : Fin n → O) :410    (generatorNormalForm (pi^a) b E (H z)).1 + (pi^a) • normalizationQuadratic b E411      (generatorNormalForm (pi^a) b E (H z)) = normalizationLinearPart E H z := by412  have h := congrArg Prod.fst413    (power_normalizer_inverse_equation O R n pi a b E ha (H z))414  simpa [adicPerturb, coordinateRemainder, normalizationQuadratic,415    normalizationLinearPart] using h416 417/-- The generator normal form for `pi ^ a` (with `0 < a`) preserves `pi`-adic congruences. -/418private theorem power_normalizer_preserves_congruence (O R : Type) [CommRing O] [CommRing R]419    [Algebra O R]420    (n : ℕ) (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))421    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (ha : 0 < a) (j : ℕ) (h h2 : R)422    (hh : adicCongr (Ideal.span {pi}) j h h2) :423    adicCongr (Ideal.span {pi}) j (generatorNormalForm (pi^a) b E h)424      (generatorNormalForm (pi^a) b E h2) := by425  have h1 := linear_map_preserves_adic_congruence O R ((Fin n → O) × R)426    (Ideal.span {pi}) E.toLinearMap j h h2 hh427  have hmem : pi ^ a ∈ Ideal.span {pi} :=428    Ideal.pow_mem_of_mem _ (Ideal.mem_span_singleton_self pi) a ha429  have hr := scalar_normalizer_raises_order O R n (Ideal.span {pi}) (pi ^ a) hmem b E430  rwa [(adic_perturb_congruence_iff O ((Fin n → O) × R) (Ideal.span {pi}) _ hr j _ _).symm,431    power_normalizer_inverse_equation O R n pi a b E ha h,432    power_normalizer_inverse_equation O R n pi a b E ha h2]433 434/-- The normalization quadratic of the normal form of `H z` depends `pi`-adically continuously435on `z`: congruent inputs give congruent outputs. -/436private theorem normalized_quadratic_preserves_congruence (O R : Type) [CommRing O] [CommRing R]437    [Algebra O R] (n : ℕ) (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))438    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (H : (Fin n → O) →ₗ[O] R) (ha : 0 < a)439    (j : ℕ) (z w : Fin n → O) (hzw : adicCongr (Ideal.span {pi}) j z w) :440    adicCongr (Ideal.span {pi}) j441      (normalizationQuadratic b E (generatorNormalForm (pi^a) b E (H z)))442      (normalizationQuadratic b E (generatorNormalForm (pi^a) b E (H w))) := by443  have h1 := linear_map_preserves_adic_congruence O _ _ _ H j z w hzw444  have h2 := power_normalizer_preserves_congruence O R n pi a b E ha j _ _ h1445  set s := generatorNormalForm (pi^a) b E (H z)446  set t := generatorNormalForm (pi^a) b E (H w)447  have hs1 := linear_map_preserves_adic_congruence O _ _ _448    (LinearMap.fst O (Fin n → O) R) j s t h2449  have hs2 := linear_map_preserves_adic_congruence O _ _ _450    (LinearMap.snd O (Fin n → O) R) j s t h2451  let L : (Fin n → O) →ₗ[O] R :=452    { toFun := coordinateLift b453      map_add' := by454        intro x y; simp [coordinateLift, add_smul, Finset.sum_add_distrib]455      map_smul' := by456        intro c x; simp [coordinateLift, Finset.smul_sum, smul_smul] }457  have hL := linear_map_preserves_adic_congruence O _ _ _ L j _ _ hs1458  have hp := algebra_product_congruence O R _ j _ _ _ _ hs2 hL459  exact linear_map_preserves_adic_congruence O _ _ _460    ((LinearMap.fst O (Fin n → O) R).comp E.toLinearMap) j _ _ hp461 462/-- If `D` is injective and `pi ^ k • W ⊆ range D`, then there is a linear map `Q` with463`D ∘ Q = pi ^ k • id` and `Q ∘ D = pi ^ k • id`. -/464theorem scaled_inverse_from_image_containment (O V W : Type) [CommRing O] [AddCommGroup V]465    [Module O V] [AddCommGroup W] [Module O W] (pi : O) (k : ℕ) (D : V →ₗ[O] W)466    (hD : Function.Injective D) (himage : ∀ w : W, (pi^k) • w ∈ D.range) :467    ∃ Q : W →ₗ[O] V, (∀ w, D (Q w) = (pi^k) • w) ∧ ∀ v, Q (D v) = (pi^k) • v := by468  have hc : ∀ w : W, ∃ v : V, D v = (pi^k) • w := fun w => LinearMap.mem_range.mp (himage w)469  let f : W → V := fun w => Classical.choose (hc w)470  have hf : ∀ w, D (f w) = (pi^k) • w := fun w => Classical.choose_spec (hc w)471  let Q : W →ₗ[O] V :=472    { toFun := f473      map_add' := fun a b => hD (by rw [map_add, hf, hf, hf, smul_add])474      map_smul' := fun c a => hD (by475        rw [map_smul, hf, hf, RingHom.id_apply, smul_comm]) }476  exact ⟨Q, hf, fun v => hD <| (hf (D v)).trans (map_smul D _ v).symm⟩477 478/-- Over a DVR with finite residue field of size `q`, if `D` is injective on `Oⁿ` with cokernel479of length `k`, then the image of `pi ^ a • D` has index `q ^ (a * n + k)`. -/480theorem scaled_linear_image_index (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]481    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (n a k : ℕ)482    (D : (Fin n → O) →ₗ[O] (Fin n → O))483    (hk : Module.length O ((Fin n → O) ⧸ LinearMap.range D) = k) :484    (LinearMap.range ((pi^a) • D)).toAddSubgroup.index =485      (Nat.card (IsLocalRing.ResidueField O))^(a*n + k) := by486  set q := Nat.card (IsLocalRing.ResidueField O)487  have hpi0 : pi ^ a ≠ 0 := pow_ne_zero _ hpi.ne_zero488  set g : (Fin n → O) →ₗ[O] (Fin n → O) := (pi ^ a) • LinearMap.id with hg_def489  have hcomp : (pi ^ a) • D = g.comp D := by490    ext x i; simp [g]491  have hg : Function.Injective g := by492    intro x y h493    funext i494    have := congrFun h i495    simp [g] at this496    exact this.resolve_right (fun h => hpi.ne_zero h.1)497  have hD' : (LinearMap.range D).toAddSubgroup.index = q ^ k :=498    finite_length_module_card O ((Fin n → O) ⧸ LinearMap.range D) k hk499  have hrange : LinearMap.range g = Submodule.pi Set.univ500      (fun _ : Fin n => (IsLocalRing.maximalIdeal O) ^ a) := by501    have hm : (IsLocalRing.maximalIdeal O) ^ a = Ideal.span {pi ^ a} := by502      rw [hpi.maximalIdeal_eq, Ideal.span_singleton_pow]503    rw [hm]504    ext x505    simp only [LinearMap.mem_range, Submodule.mem_pi, Set.mem_univ, true_implies,506      Ideal.mem_span_singleton', g]507    constructor508    · rintro ⟨y, rfl⟩ i509      exact ⟨y i, by simp [mul_comm]⟩510    · intro h511      choose y hy using h512      exact ⟨y, by funext i; simp [← hy i, mul_comm]⟩513  have hg' : (LinearMap.range g).toAddSubgroup.index = q ^ (a * n) := by514    change Nat.card ((Fin n → O) ⧸ LinearMap.range g) = _515    rw [hrange, Nat.card_congr (Submodule.quotientPi _).toEquiv, Nat.card_pi]516    simp [residue_quotient_card, q, pow_mul]517  rw [hcomp, linear_composition_index _ _ _ _ D g hg, hD', hg', ← pow_add, add_comm]518 519/-- Scaling the coordinates by `pi ^ m` multiplies the Haar measure of a measurable subset of520`Oⁿ` by `q⁻¹ ^ (m * n)`. -/521theorem coordinate_scale_measure (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]522    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]523    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]524    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]525    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (pi : O) (hpi : Irreducible pi) (n m : ℕ)526    (S : Set (Fin n → O)) :527    coefficientMeasure O n (coordinateScale pi m '' S) =528      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^(m*n) * coefficientMeasure O n S := by529  obtain ⟨-, hHaar, hProb, -, -⟩ :=530    coefficient_space_strict_instances O htop pi hpi n531  let L : (Fin n → O) →ₗ[O] (Fin n → O) := (pi^m) • LinearMap.id532  have hidx := scaled_linear_image_index O pi hpi n m 0 LinearMap.id (by533      rw [Nat.cast_zero, Module.length_eq_zero_iff, LinearMap.range_id]534      infer_instance)535  have hpm : pi ^ m ≠ 0 := pow_ne_zero _ hpi.ne_zero536  have hinj : Function.Injective L.toAddMonoidHom := fun _ _ hxy => smul_right_injective _ hpm hxy537  have hcont : Continuous L.toAddMonoidHom :=538    finite_coordinate_linear_continuous O n n L539  have hrange : L.toAddMonoidHom.range = (LinearMap.range L).toAddSubgroup := rfl540  have hq : 0 < Nat.card (IsLocalRing.ResidueField O) := Nat.card_pos541  have hne : L.toAddMonoidHom.range.index ≠ 0 := by542    rw [hrange, hidx]; positivity543  have : L.toAddMonoidHom.range.FiniteIndex := ⟨hne⟩544  have key := compact_injective_image_measure (Fin n → O) (Fin n → O)545    L.toAddMonoidHom hcont hinj (coefficientMeasure O n) (coefficientMeasure O n) S546  have himg : coordinateScale pi m '' S = L.toAddMonoidHom '' S := rfl547  rw [himg, key, hrange, hidx]548  simp [ENNReal.inv_pow, Nat.cast_pow]549 550/-! ### Regularity on special fibers -/551 552/-- A function with finite contact `c` along the axis `X s` of a monomial special fiber is not553divisible by `X s` (otherwise the contact length would be infinite). -/554private theorem not_mem_axis_of_contact (k : Type) [Field k] (a b c : ℕ) (s t : Fin 2) (hst : s ≠ t)555    (F : TwoSeries k)556  (hle : monomialIdeal k a b ≤ Ideal.span {(MvPowerSeries.X s : TwoSeries k)})557  (hmem : F ∈ Ideal.span {(MvPowerSeries.X s : TwoSeries k)})558  (hf : contact (Ideal.Quotient.mk (monomialIdeal k a b) F)559    (Ideal.Quotient.mk (monomialIdeal k a b) (MvPowerSeries.X s)) = c) : False := by560  have hspan : Ideal.span {Ideal.Quotient.mk (monomialIdeal k a b) F,561      Ideal.Quotient.mk (monomialIdeal k a b) (MvPowerSeries.X s)}562      = (Ideal.span {(MvPowerSeries.X s : TwoSeries k)}).map563          (Ideal.Quotient.mkₐ (TwoSeries k) (monomialIdeal k a b)) := by564    rw [Ideal.map_span, Set.image_singleton]565    have h2 : Ideal.Quotient.mkₐ (TwoSeries k) (monomialIdeal k a b) (MvPowerSeries.X s)566      = Ideal.Quotient.mk (monomialIdeal k a b) (MvPowerSeries.X s) := rfl567    rw [h2]568    refine Submodule.span_insert_eq_span ?_569    rw [← h2]570    exact Ideal.mem_span_singleton.mpr571        (map_dvd (Ideal.Quotient.mkₐ (TwoSeries k) (monomialIdeal k a b))572        (Ideal.mem_span_singleton.mp hmem))573  have e := (DoubleQuot.quotQuotEquivQuotOfLEₐ (TwoSeries k) hle).toLinearEquiv574  have h1 := e.length_eq575  rw [axis_quotient_length_top k s t hst] at h1576  rw [contact, hspan] at hf577  rw [← Module.length_eq_of_surjective (S := TwoSeries k) Ideal.Quotient.mk_surjective] at hf578  exact ENat.top_ne_natCast c (h1.symm.trans hf)579 580/-- The axis variables of `k⟦t, x⟧` are nonzero. -/581private theorem axis_X_ne_zero (k : Type) [Field k] (s : Fin 2) :582    (MvPowerSeries.X s : TwoSeries k) ≠ 0 := fun h0 => by583  simpa [MvPowerSeries.coeff_X] using congrArg (MvPowerSeries.coeff (Finsupp.single s 1)) h0584 585/-- If `F` is not divisible by the axis variable `X s`, then `F * W ∈ (X s ^ n)` forces586`W ∈ (X s ^ n)`. -/587private theorem mem_axis_pow_of_mul_mem (k : Type) [Field k] (s : Fin 2) (F : TwoSeries k)588    (hF : F ∉ Ideal.span {(MvPowerSeries.X s : TwoSeries k)}) :589    ∀ n : ℕ, ∀ W : TwoSeries k, F * W ∈ Ideal.span {(MvPowerSeries.X s : TwoSeries k) ^ n} →590      W ∈ Ideal.span {(MvPowerSeries.X s : TwoSeries k) ^ n} := by591  have hprime := axis_span_isPrime k s592  have hT0 := axis_X_ne_zero k s593  intro n594  induction n with595  | zero => intro W _; simp596  | succ n ih =>597    intro W hW598    have hW1 : F * W ∈ Ideal.span {(MvPowerSeries.X s : TwoSeries k)} := by599      rw [Ideal.mem_span_singleton] at hW ⊢600      exact (dvd_pow_self _ n.succ_ne_zero).trans hW601    have hWT : W ∈ Ideal.span {(MvPowerSeries.X s : TwoSeries k)} :=602      (hprime.mem_or_mem hW1).resolve_left hF603    obtain ⟨W', rfl⟩ := Ideal.mem_span_singleton.mp hWT604    have h' : F * W' ∈ Ideal.span {(MvPowerSeries.X s : TwoSeries k) ^ n} := by605      rw [Ideal.mem_span_singleton] at hW ⊢606      obtain ⟨q, hq⟩ := hW607      refine ⟨q, mul_left_cancel₀ hT0 ?_⟩608      rw [pow_succ] at hq609      linear_combination hq610    have := ih W' h'611    rw [Ideal.mem_span_singleton] at this ⊢612    rw [pow_succ']613    exact mul_dvd_mul_left _ this614 615/-- On the crossing special fiber `k⟦t, x⟧ ⧸ (tᵃ xᵇ)` with `a, b > 0`, a function of finite616contact with both axes is a nonzerodivisor. -/617theorem special_fiber_crossing_contact_regular (k : Type) [Field k] (a b c h : ℕ) (ha : 0 < a)Lemma 2.1618    (hb : 0 < b) (f : SpecialFiber k a b) (ht : contact f (fiberT k a b) = c)619    (hx : contact f (fiberX k a b) = h) :620    Function.Injective (fun w : SpecialFiber k a b => f * w) := by621  have hI : monomialIdeal k a b = Ideal.span622      {(MvPowerSeries.X 0 : TwoSeries k) ^ a * (MvPowerSeries.X 1 : TwoSeries k) ^ b} := rfl623  have hle0 : monomialIdeal k a b ≤ Ideal.span {(MvPowerSeries.X 0 : TwoSeries k)} := by624    rw [hI, Ideal.span_singleton_le_iff_mem]625    exact Ideal.mem_span_singleton.mpr (Dvd.dvd.mul_right (dvd_pow_self _ ha.ne') _)626  have hle1 : monomialIdeal k a b ≤ Ideal.span {(MvPowerSeries.X 1 : TwoSeries k)} := by627    rw [hI, Ideal.span_singleton_le_iff_mem]628    exact Ideal.mem_span_singleton.mpr (Dvd.dvd.mul_left (dvd_pow_self _ hb.ne') _)629  obtain ⟨F, rfl⟩ := Ideal.Quotient.mk_surjective f630  have hF0 : F ∉ Ideal.span {(MvPowerSeries.X 0 : TwoSeries k)} := fun hmem =>631    not_mem_axis_of_contact k a b c 0 1 (by decide) F hle0 hmem ht632  have hF1 : F ∉ Ideal.span {(MvPowerSeries.X 1 : TwoSeries k)} := fun hmem =>633    not_mem_axis_of_contact k a b h 1 0 (by decide) F hle1 hmem hx634  have hTa : (MvPowerSeries.X 0 : TwoSeries k) ^ a ≠ 0 := pow_ne_zero _ (axis_X_ne_zero k 0)635  intro w₁ w₂ hw636  obtain ⟨W₁, rfl⟩ := Ideal.Quotient.mk_surjective w₁637  obtain ⟨W₂, rfl⟩ := Ideal.Quotient.mk_surjective w₂638  simp only [← map_mul] at hw639  rw [Ideal.Quotient.eq] at hw ⊢640  rw [hI] at hw ⊢641  rw [← mul_sub] at hw642  generalize W₁ - W₂ = W at hw ⊢643  obtain ⟨q, hq⟩ := Ideal.mem_span_singleton.mp hw644  have hWa : F * W ∈ Ideal.span {(MvPowerSeries.X 0 : TwoSeries k) ^ a} :=645    Ideal.mem_span_singleton.mpr ⟨(MvPowerSeries.X 1 : TwoSeries k) ^ b * q, by rw [hq]; ring⟩646  obtain ⟨W', rfl⟩ := Ideal.mem_span_singleton.mp (mem_axis_pow_of_mul_mem k 0 F hF0 a W hWa)647  have hW'b : F * W' ∈ Ideal.span {(MvPowerSeries.X 1 : TwoSeries k) ^ b} :=648    Ideal.mem_span_singleton.mpr ⟨q, mul_left_cancel₀ hTa (by linear_combination hq)⟩649  obtain ⟨r, rfl⟩ := Ideal.mem_span_singleton.mp (mem_axis_pow_of_mul_mem k 1 F hF1 b W' hW'b)650  exact Ideal.mem_span_singleton.mpr ⟨r, by ring⟩651 652/-- On the single special fiber `k⟦t, x⟧ ⧸ (tᵃ)` with `a > 0`, a function of finite contact with653the axis `t = 0` is a nonzerodivisor. -/654theorem special_fiber_single_contact_regular (k : Type) [Field k] (a c : ℕ) (ha : 0 < a)Lemma 2.1655    (f : SpecialFiber k a 0) (hf : contact f (fiberT k a 0) = c) :656    Function.Injective (fun w : SpecialFiber k a 0 => f * w) := by657  have hI : monomialIdeal k a 0 = Ideal.span {(MvPowerSeries.X 0 : TwoSeries k) ^ a} := by658    simp [monomialIdeal, axisT]659  have hle : monomialIdeal k a 0 ≤ Ideal.span {(MvPowerSeries.X 0 : TwoSeries k)} := by660    rw [hI, Ideal.span_singleton_le_iff_mem]661    exact Ideal.mem_span_singleton.mpr (dvd_pow_self _ ha.ne')662  obtain ⟨F, rfl⟩ := Ideal.Quotient.mk_surjective f663  have hF : F ∉ Ideal.span {(MvPowerSeries.X 0 : TwoSeries k)} := fun hmem =>664    not_mem_axis_of_contact k a 0 c 0 1 (by decide) F hle hmem hf665  intro w₁ w₂ h666  obtain ⟨W₁, rfl⟩ := Ideal.Quotient.mk_surjective w₁667  obtain ⟨W₂, rfl⟩ := Ideal.Quotient.mk_surjective w₂668  simp only [← map_mul] at h669  rw [Ideal.Quotient.eq] at h ⊢670  rw [hI] at h ⊢671  exact mem_axis_pow_of_mul_mem k 0 F hF a _ (by rwa [mul_sub])672 673/-- On the concrete surface with `b = 0`, if `f` reduces to a function of positive finite contact674`c` with the special fiber axis, then `O[f]` is free of rank `a * c` over `O`. -/675theorem concrete_surface_single_curve_free (O : Type) [CommRing O] [IsDomain O]676    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (pi : O)677    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a : ℕ) (ha : 0 < a)678    (f : ConcreteSurface O pi u a 0)679    (e : (ConcreteSurface O pi u a 0 ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi})680    ≃+* SpecialFiber (IsLocalRing.ResidueField O) a 0) (c : ℕ) (hc : 0 < c)681    (hcontact : contact682    (e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi}) f))683    (fiberT (IsLocalRing.ResidueField O) a 0) = c) :684    Module.Free O (ConcreteSurface O pi u a 0 ⧸ Ideal.span {f}) ∧ Module.Finite O685      (ConcreteSurface O pi u a 0 ⧸ Ideal.span {f}) ∧ Module.finrank O686      (ConcreteSurface O pi u a 0 ⧸ Ideal.span {f}) = a*c := by687  have hreg := special_fiber_single_contact_regular _ a c ha _ hcontact688  have hreg' := concrete_surface_residue_regular_of_special_fiber O pi u a 0 f e hreg689  have hlen := single_special_fiber_length _ a c ha _ hcontact690  have hN := (concrete_surface_special_fiber_length_transport O pi u a 0 f e).trans hlen691  have hfu : ¬ IsUnit f := by692    intro hu693    have hu' :=694        (hu.map (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi}))).map695        e696    have htop : Ideal.span697      {e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi}) f), fiberT698      (IsLocalRing.ResidueField O) a 0} = ⊤ := by699      exact Ideal.eq_top_of_isUnit_mem _ (Ideal.subset_span (by simp)) hu'700    rw [contact, htop] at hcontact701    have : Subsingleton702        (SpecialFiber (IsLocalRing.ResidueField O) a 0 ⧸703        (⊤ : Ideal (SpecialFiber (IsLocalRing.ResidueField O) a 0))) :=704        Ideal.Quotient.subsingleton_iff.mpr rfl705    rw [Module.length_eq_zero] at hcontact706    exact absurd hcontact.symm (by exact_mod_cast hc.ne')707  exact concrete_surface_curve_free_of_length O pi hpi u a 0 ha f hreg' (a*c)708      (by exact_mod_cast hN)709 710/-! ### The strict normalizer -/711 712/-- For `k < a`, the normalization correction map raises the `pi`-adic order of congruences. -/713theorem strict_correction_raises_order (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (n : ℕ)714    (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))715    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (H : (Fin n → O) →ₗ[O] R) (k : ℕ)716    (ha : k < a) (Q : (Fin n → O) →ₗ[O] (Fin n → O)) :717    RaisesAdicOrder (Ideal.span {pi}) (normalizationCorrection pi a k b E H Q) := by718  intro j x y hxy719  have h1 := normalized_quadratic_preserves_congruence O R n pi a b E H720    (by omega) j x y hxy721  have h2 := linear_map_preserves_adic_congruence O _ _ _ Q j _ _ h1722  unfold adicCongr at h2 ⊢723  unfold normalizationCorrection724  rw [← smul_sub]725  have hmem : -(pi ^ (a - k)) ∈ Ideal.span {pi} := (Submodule.neg_mem_iff _).mpr726    (Ideal.pow_mem_of_mem _ (Ideal.mem_span_singleton_self pi) _ (by omega))727  have := Submodule.smul_mem_smul hmem h2728  rwa [← Submodule.smul_assoc, smul_eq_mul, ← pow_succ'] at this729 730/-- The scaled strict map factors as `pi ^ a` times the normalization linear part composed with731the adic perturbation by the normalization correction. -/732theorem strict_normalizer_factors_through_linear (O R : Type) [CommRing O] [CommRing R]733    [Algebra O R] (n : ℕ) (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))734    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (H : (Fin n → O) →ₗ[O] R) (k : ℕ)735    (ha : k < a) (Q : (Fin n → O) →ₗ[O] (Fin n → O))736    (hQ : ∀ w, normalizationLinearPart E H (Q w) = (pi ^ k) • w) (z : Fin n → O) :737    scaledStrictMap pi a b E H z = (pi^a) • normalizationLinearPart E H738      (adicPerturb (normalizationCorrection pi a k b E H Q) z) := by739  have h := normalized_coordinate_equation O R n pi a b E H (by omega) z740  have hpow : pi ^ (a - k) * pi ^ k = pi ^ a := by741    rw [← pow_add, Nat.sub_add_cancel ha.le]742  unfold scaledStrictMap adicPerturb normalizationCorrection743  rw [map_add, neg_smul, map_neg, map_smul, hQ, smul_smul, hpow, ← h]744  congr 1745  abel746 747/-- When `pi` lies in the Jacobson radical, the perturbed principal ideal `(g + pi ^ a • H z)`748equals the normalized ideal at the scaled strict map of `z`. -/749private theorem strict_normalizer_ideal_jacobson (O R : Type) [CommRing O] [CommRing R]750    [Algebra O R]751    (n : ℕ) (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))752    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (H : (Fin n → O) →ₗ[O] R) (ha : 0 < a)753    (hpi : algebraMap O R pi ∈ Ideal.jacobson (⊥ : Ideal R)) (g : R)754    (hE : ∀ w, E.symm w = divisionMap g b w) (z : Fin n → O) :755    Ideal.span {g + (pi^a) • H z} = normalizedIdeal g b (scaledStrictMap pi a b E H z) := by756  set s := generatorNormalForm (pi^a) b E (H z) with hs757  have h1 := scaled_normalization_identity O R n (pi^a) g b E hE s758  rw [power_normalizer_inverse_equation O R n pi a b E ha (H z),759    LinearEquiv.symm_apply_apply] at h1760  have hu : IsUnit (1 + pi^a • s.2) := by761    apply Ideal.isUnit_of_sub_one_mem_jacobson_bot762    rw [add_sub_cancel_left, Algebra.smul_def, map_pow]763    exact Ideal.mul_mem_right _ _ (Ideal.pow_mem_of_mem _ hpi a ha)764  rw [← h1, ← hu.unit_spec, principal_ideal_unit_invariance]765  unfold normalizedIdeal normalizedGenerator scaledStrictMap coordinateLift766  congr 3767  rw [Finset.smul_sum]768  refine Finset.sum_congr rfl fun i _ => ?_769  rw [Pi.smul_apply, smul_assoc]770 771/-- The scaled strict map has the same image as the linear map `z ↦ pi ^ a • L z`, where `L` is772the normalization linear part. -/773theorem strict_normalizer_lattice_image (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (n : ℕ)774    (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))775    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (H : (Fin n → O) →ₗ[O] R) (k : ℕ)776    (ha : k < a) (Q : (Fin n → O) →ₗ[O] (Fin n → O))777    (hQ : ∀ w, normalizationLinearPart E H (Q w) = (pi ^ k) • w)778    [IsAdicComplete (Ideal.span {pi}) (Fin n → O)] :779    Set.range (scaledStrictMap pi a b E H) = Set.range780      (fun z : Fin n → O => (pi^a) • normalizationLinearPart E H z) := by781  have hbij := adic_perturb_bijective O (Fin n → O) (Ideal.span {pi}) _782    (strict_correction_raises_order O R n pi a b E H k ha Q)783  have hf := strict_normalizer_factors_through_linear O R n pi a b E H k ha Q hQ784  ext y785  constructor786  · rintro ⟨z, rfl⟩787    exact ⟨_, (hf z).symm⟩788  · rintro ⟨w, rfl⟩789    obtain ⟨z, hz⟩ := hbij.2 w790    exact ⟨z, by rw [hf z, hz]⟩791 792/-- Pullback identity: if `alpha f = e ^ d * g` and `pi ^ s = e ^ d * c` in `C`, then `alpha`793sends the perturbation `f + pi ^ (s + a) • ℓ(z)` to `e ^ d` times the pulled perturbation of `g`. -/794private theorem strict_pullback_perturbation_identity (O R C : Type) [CommRing O] [CommRing R]795    [CommRing C]796    [Algebra O R] [Algebra O C] (n : ℕ) (pi : O) (s a d : ℕ) (alpha : R →ₐ[O] C) (f : R) (g e c : C)797    (b : Fin n → R) (hf : alpha f = e ^ d * g) (hpi : (algebraMap O C pi) ^ s = e ^ d * c)798    (z : Fin n → O) :799    alpha (f + (pi^(s+a)) • coordinateLift b z) = e^d *800      (g + (pi^a) • pulledVariation alpha c b z) := by801  have hL : coordinateLinear (O := O) b z = coordinateLift b z := by802    simp [coordinateLinear, coordinateLift, LinearMap.sum_apply]803  have hP : pulledVariation alpha c b z = c * alpha (coordinateLift b z) := by804    simp [pulledVariation, hL]805  rw [hP, map_add, map_smul, hf, Algebra.smul_def, Algebra.smul_def, map_pow, map_pow, pow_add, hpi]806  ring807 808/-- The strict transform (colon by `e ^ d`) of the pulled-back perturbed principal ideal is the809principal ideal of the pulled perturbation of `g`. -/810private theorem strict_pullback_colon_perturbation (O R C : Type) [CommRing O] [CommRing R]811    [CommRing C]812    [Algebra O R] [Algebra O C] (n : ℕ) (pi : O) (s a d : ℕ) (alpha : R →ₐ[O] C) (f : R) (g e c : C)813    (b : Fin n → R) (hf : alpha f = e ^ d * g) (hpi : (algebraMap O C pi) ^ s = e ^ d * c)814    (he : Function.Injective (fun z : C => e*z)) (z : Fin n → O) :815    ((Ideal.span {f + (pi^(s+a)) • coordinateLift b z}).map alpha.toRingHom).colon {e^d} =816      Ideal.span {g + (pi^a) • pulledVariation alpha c b z} := by817  have hid := strict_pullback_perturbation_identity O R C n pi s a d alpha f g e c b hf hpi z818  rw [Ideal.map_span, Set.image_singleton]819  change (Ideal.span {alpha (f + (pi^(s+a)) • coordinateLift b z)}).colon {e^d} = _820  rw [hid]821  have hinj : IsLeftRegular (e ^ d) := IsLeftRegular.pow d he822  ext u823  rw [Submodule.mem_colon_singleton, Ideal.mem_span_singleton', Ideal.mem_span_singleton']824  constructor825  · rintro ⟨v, hv⟩826    refine ⟨v, hinj ?_⟩827    rw [smul_eq_mul] at hv828    linear_combination hv829  · rintro ⟨v, rfl⟩830    exact ⟨v, by rw [smul_eq_mul]; ring⟩831 832/-- The strict transform of a perturbed principal ideal is the normalized ideal at the scaled833strict map of the pulled variation. -/834private theorem actual_strict_map_is_scaled_normalizer (O R C : Type) [CommRing O] [CommRing R]835    [CommRing C]836    [Algebra O R] [Algebra O C] (n : ℕ) (pi : O) (s a d : ℕ) (alpha : R →ₐ[O] C) (f : R) (g e c : C)837    (b : Fin n → R) (hf : alpha f = e ^ d * g) (hpi : (algebraMap O C pi) ^ s = e ^ d * c)838    (he : Function.Injective (fun z : C => e*z)) (ha : 0 < a)839    (hjac : algebraMap O C pi ∈ Ideal.jacobson (⊥ : Ideal C)) (bc : Fin n → C)840    (E : C ≃ₗ[O] ((Fin n → O) × C)) (hE : ∀ w, E.symm w = divisionMap g bc w)841    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × C)] (z : Fin n → O) :842    ((Ideal.span {f + (pi^(s+a)) • coordinateLift b z}).map alpha.toRingHom).colon {e^d} =843      normalizedIdeal g bc (scaledStrictMap pi a bc E (pulledVariation alpha c b) z) := by844  rw [strict_pullback_colon_perturbation O R C n pi s a d alpha f g e c b hf hpi he z]845  exact strict_normalizer_ideal_jacobson O C n pi a bc E (pulledVariation alpha c b) ha hjac g hE z846 847/-- Chart coordinates commute with strict transforms: the strict transform of the coordinate848ideal at `pi ^ (s + a - 1) • z` is the coordinate ideal at the child coordinate map of `z`. -/849theorem strict_chart_coordinates_commute (O R C : Type) [CommRing O] [CommRing R] [CommRing C]850    [Algebra O R] [Algebra O C] (n : ℕ) (pi : O) (s a d : ℕ) (alpha : R →ₐ[O] C) (f : R) (g e c : C)851    (b : Fin n → R) (hf : alpha f = e ^ d * g) (hpi : (algebraMap O C pi) ^ s = e ^ d * c)852    (he : Function.Injective (fun z : C => e*z)) (ha : 0 < a)853    (hjac : algebraMap O C pi ∈ Ideal.jacobson (⊥ : Ideal C)) (bc : Fin n → C)854    (E : C ≃ₗ[O] ((Fin n → O) × C)) (hE : ∀ w, E.symm w = divisionMap g bc w)855    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × C)] (z : Fin n → O) :856    strictTransformIdeal alpha e d (coordinateIdeal pi f b (coordinateScale pi (s+a-1) z)) =857      coordinateIdeal pi g bc (childCoordinateMap pi a bc E (pulledVariation alpha c b) z) := by858  have h1 : coordinateIdeal pi f b (coordinateScale pi (s+a-1) z)859      = Ideal.span {f + (pi^(s+a)) • coordinateLift b z} := by860    have h2 : pi * pi^(s+a-1) = pi^(s+a) := by861      rw [← pow_succ' pi]; congr 1; omega862    have : coordinateLift b (pi • coordinateScale pi (s+a-1) z) = (pi^(s+a)) • coordinateLift b863      z := by864      simp only [coordinateLift, coordinateScale, Finset.smul_sum, Pi.smul_apply, smul_eq_mul,865          smul_smul, ← mul_assoc, h2]866    simp only [coordinateIdeal, normalizedIdeal, normalizedGenerator, this]867  have h3 : pi • childCoordinateMap pi a bc E (pulledVariation alpha c b) z868      = scaledStrictMap pi a bc E (pulledVariation alpha c b) z := by869    have h2 : pi * pi^(a-1) = pi^a := by870      rw [← pow_succ' pi]; congr 1; omega871    simp only [childCoordinateMap, scaledStrictMap, smul_smul, h2]872  rw [h1, strictTransformIdeal,873    actual_strict_map_is_scaled_normalizer O R C n pi s a d alpha f g e c b hf hpi he ha hjac bc E874        hE z,875    coordinateIdeal, ← h3]876 877/-- Preimage form of `strict_chart_coordinates_commute`: on the scaled coordinate lattice, the878preimage of a set of child coordinate ideals is the scaled preimage under the child map. -/879theorem strict_chart_preimage_set_identity (O R C : Type) [CommRing O] [CommRing R] [CommRing C]880    [Algebra O R] [Algebra O C] (n : ℕ) (pi : O) (s a d : ℕ) (alpha : R →ₐ[O] C) (f : R) (g e c : C)881    (b : Fin n → R) (hf : alpha f = e ^ d * g) (hpi : (algebraMap O C pi) ^ s = e ^ d * c)882    (he : Function.Injective (fun z : C => e*z)) (ha : 0 < a)883    (hjac : algebraMap O C pi ∈ Ideal.jacobson (⊥ : Ideal C)) (bc : Fin n → C)884    (E : C ≃ₗ[O] ((Fin n → O) × C)) (hE : ∀ w, E.symm w = divisionMap g bc w)885    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × C)]886    (hΨ : Function.Injective (coordinateIdeal pi g bc)) (T : Set (Fin n → O)) :887    coordinateIdeal pi f b ⁻¹' (strictTransformIdeal alpha e d ⁻¹' (coordinateIdeal pi g bc '' T)) ∩888      Set.range (coordinateScale pi (s+a-1)) = coordinateScale pi (s+a-1) ''889      (childCoordinateMap pi a bc E (pulledVariation alpha c b) ⁻¹' T) := by890  have key := fun z => strict_chart_coordinates_commute O R C n pi s a d alpha f g e c b hf hpi he891      ha hjac bc E hE z892  ext x893  constructor894  · rintro ⟨hx, z, rfl⟩895    refine ⟨z, ?_, rfl⟩896    obtain ⟨w, hw, hw2⟩ := hx897    rw [key] at hw2898    change _ ∈ T; rwa [← hΨ hw2]899  · rintro ⟨z, hz, rfl⟩900    refine ⟨?_, z, rfl⟩901    simp only [Set.mem_preimage]902    rw [key]903    exact ⟨_, hz, rfl⟩904 905/-! ### Strict quotient maps -/906 907/-- Additivity of cokernel lengths along a composition with injective second factor. -/908private theorem length_coker_comp (O : Type) [CommRing O] {M N P : Type} [AddCommGroup M]909    [Module O M]910    [AddCommGroup N] [Module O N] [AddCommGroup P] [Module O P]911    (u : M →ₗ[O] N) (v : N →ₗ[O] P) (hv : Function.Injective v) :912    Module.length O (P ⧸ LinearMap.range (v.comp u)) =913      Module.length O (N ⧸ LinearMap.range u) + Module.length O (P ⧸ LinearMap.range v) := by914  have h1 : LinearMap.range u ≤ (LinearMap.range (v.comp u)).comap v := by915    rintro _ ⟨m, rfl⟩916    exact ⟨m, rfl⟩917  have h2 : LinearMap.range (v.comp u) ≤ (LinearMap.range v).comap LinearMap.id := by918    rintro _ ⟨m, rfl⟩919    exact ⟨u m, rfl⟩920  refine Module.length_eq_add_of_exact (Submodule.mapQ _ _ v h1)921    (Submodule.mapQ _ _ LinearMap.id h2) ?_ ?_ ?_922  · rw [← LinearMap.ker_eq_bot, eq_bot_iff]923    intro x hx924    obtain ⟨n, rfl⟩ := Submodule.Quotient.mk_surjective _ x925    rw [LinearMap.mem_ker, Submodule.mapQ_apply, Submodule.Quotient.mk_eq_zero] at hx926    obtain ⟨m, hm⟩ := hx927    rw [Submodule.mem_bot, Submodule.Quotient.mk_eq_zero]928    exact ⟨m, hv hm⟩929  · intro y930    obtain ⟨p, rfl⟩ := Submodule.Quotient.mk_surjective _ y931    exact ⟨Submodule.Quotient.mk p, rfl⟩932  · intro y933    obtain ⟨p, rfl⟩ := Submodule.Quotient.mk_surjective _ y934    rw [Submodule.mapQ_apply, LinearMap.id_apply, Submodule.Quotient.mk_eq_zero]935    constructor936    · rintro ⟨n, rfl⟩937      exact ⟨Submodule.Quotient.mk n, rfl⟩938    · rintro ⟨x, hx⟩939      obtain ⟨n, rfl⟩ := Submodule.Quotient.mk_surjective _ x940      rw [Submodule.mapQ_apply, Submodule.Quotient.eq] at hx941      obtain ⟨m, hm⟩ := hx942      refine ⟨n - u m, ?_⟩943      simp only [LinearMap.comp_apply] at hm944      rw [map_sub, hm]; abel945 946/-- Cokernel length of `w ^ k` for an injective endomorphism `w`. -/947private theorem length_coker_pow (O : Type) [CommRing O] {P : Type} [AddCommGroup P] [Module O P]948    (w : Module.End O P) (hw : Function.Injective w) (k : ℕ) :949    Module.length O (P ⧸ LinearMap.range (w ^ k)) = k * Module.length O950      (P ⧸ LinearMap.range w) := by951  induction k with952  | zero =>953    rw [Nat.cast_zero, zero_mul, Module.length_eq_zero_iff, pow_zero, Module.End.one_eq_id,954      LinearMap.range_id]955    infer_instance956  | succ k ih =>957    rw [pow_succ', Module.End.mul_eq_comp, length_coker_comp O _ _ hw, ih]958    push_cast; ring959 960/-- `tri d = chooseTwo d + d`. -/961private theorem tri_eq_chooseTwo_add (d : ℕ) : tri d = chooseTwo d + d := by962  unfold tri chooseTwo963  cases d with964  | zero => rfl965  | succ n =>966    have : (n+1)*(n+1+1) = (n+1)*(n+1-1) + (n+1)*2 := by967      simp only [Nat.add_sub_cancel]; ring968    rw [this, Nat.add_mul_div_right _ _ (by norm_num)]969 970/-- Length of the cokernel of the strict quotient map `phi`: it equals `s * N - tri d`, computed971from the relation `e ^ d * phi = pi ^ s • iota` and the cokernel lengths of `iota`, `e`, `pi`. -/972theorem strict_quotient_cokernel_length (O R C : Type) [CommRing O] [CommRing R] [CommRing C]Theorem 5.1973    [Algebra O R] [Algebra O C] (alpha : R →ₐ[O] C) (f : R) (g e c : C) (d : ℕ)974    (pi : O) (s : ℕ) (hpi : (algebraMap O C pi) ^ s = e ^ d * c) (N : ℕ)975    (phi iota : (R ⧸ Ideal.span {f}) →ₗ[O] (C ⧸ Ideal.span {g}))976    (hphi : ∀ h : R, phi (Ideal.Quotient.mk (Ideal.span {f}) h) = Ideal.Quotient.mk (Ideal.span {g})977    (c * alpha h))978    (hiota : ∀ h : R, iota (Ideal.Quotient.mk (Ideal.span {f}) h) = Ideal.Quotient.mk979    (Ideal.span {g}) (alpha h))980    (hindex : Module.length O ((C ⧸ Ideal.span {g}) ⧸ LinearMap.range iota) = (chooseTwo d : ℕ∞))981    (hereg : Function.Injective982    (fun y : C ⧸ Ideal.span {g} => Ideal.Quotient.mk (Ideal.span {g}) e * y))983    (hechild : Module.length O984    ((C ⧸ Ideal.span {g}) ⧸ LinearMap.range985    (LinearMap.mulLeft O (Ideal.Quotient.mk (Ideal.span {g}) e))) = (d : ℕ∞))986    (hpireg : Function.Injective (fun y : C ⧸ Ideal.span {g} => (pi : O) • y))987    (hpiquot : Module.length O988    ((C ⧸ Ideal.span {g}) ⧸ LinearMap.range989    ((pi : O) • (LinearMap.id : (C ⧸ Ideal.span {g}) →ₗ[O] (C ⧸ Ideal.span {g})))) = (N : ℕ∞))990    (hsmall : tri d ≤ s*N) :991    Module.length O ((C ⧸ Ideal.span {g}) ⧸ LinearMap.range phi) = ((s*N - tri d : ℕ) : ℕ∞) := by992  set me : Module.End O (C ⧸ Ideal.span {g}) := LinearMap.mulLeft O993      (Ideal.Quotient.mk (Ideal.span {g}) e)994  set mp : Module.End O (C ⧸ Ideal.span {g}) := (pi : O) •995      (LinearMap.id : (C ⧸ Ideal.span {g}) →ₗ[O] (C ⧸ Ideal.span {g}))996  have hrel : (me ^ d).comp phi = (mp ^ s).comp iota := by997    apply LinearMap.ext998    intro u999    obtain ⟨h, rfl⟩ := Ideal.Quotient.mk_surjective u1000    have hme' : ∀ k y, (me ^ k) y = Ideal.Quotient.mk (Ideal.span {g}) (e ^ k) * y := fun k y ↦ by1001      simp [me]1002    have hmp' : ∀ k y, (mp ^ k) y = (pi ^ k) • y := fun k ↦ by1003      induction k with1004      | zero => simp1005      | succ k ih => intro y; simp [pow_succ', Module.End.mul_apply, ih, mp, mul_smul]1006    rw [LinearMap.comp_apply, LinearMap.comp_apply, hme', hmp', hphi, hiota,1007      Algebra.smul_def, ← Ideal.Quotient.mk_algebraMap, ← map_mul, ← map_mul, map_pow, hpi,1008      mul_assoc]1009  have hme : Function.Injective me := hereg1010  have hmp : Function.Injective mp := hpireg1011  have key := congrArg (fun F => Module.length O ((C ⧸ Ideal.span {g}) ⧸ LinearMap.range F)) hrel1012  rw [length_coker_comp O _ _ (hme.iterate d |> fun h => by simpa [Module.End.coe_pow] using h),1013    length_coker_comp O _ _ (hmp.iterate s |> fun h => by simpa [Module.End.coe_pow] using h),1014    length_coker_pow O _ hme, length_coker_pow O _ hmp, hindex, hechild, hpiquot] at key1015  have ht := tri_eq_chooseTwo_add d1016  have h2 : 2 * tri d = d * d + d := by1017    unfold tri1018    rw [Nat.mul_div_cancel' (Nat.even_mul_succ_self d).two_dvd]; ring1019  have hdd : d * d = chooseTwo d + tri d := by omega1020  have hL : Module.length O ((C ⧸ Ideal.span {g}) ⧸ LinearMap.range phi) ≠ ⊤ := fun h ↦ by1021    rw [h, top_add] at key1022    exact ENat.natCast_ne_top (chooseTwo d + s * N) (by rw [key]; push_cast; rfl)1023  obtain ⟨n, hn⟩ := ENat.ne_top_iff_exists.mp hL1024  rw [← hn] at key ⊢1025  norm_cast at key ⊢1026  omega1027 1028/-- If `alpha f = e ^ d * g`, then `alpha` descends to an `O`-linear map1029`R ⧸ (f) → C ⧸ (g)`. -/1030theorem strict_quotient_inclusion_exists (O R C : Type) [CommRing O] [CommRing R] [CommRing C]1031    [Algebra O R] [Algebra O C] (alpha : R →ₐ[O] C) (f : R) (g e : C) (d : ℕ)1032    (hf : alpha f = e ^ d * g) :1033    ∃ iota : (R ⧸ Ideal.span {f}) →ₗ[O] (C ⧸ Ideal.span {g}), ∀ h : R, iota1034      (Ideal.Quotient.mk (Ideal.span {f}) h) = Ideal.Quotient.mk (Ideal.span {g}) (alpha h) := by1035  have hle : Ideal.span {f} ≤ (Ideal.span {g}).comap alpha :=1036    (Ideal.span_singleton_le_iff_mem _).mpr <| by1037      rw [Ideal.mem_comap, hf]; exact Ideal.mul_mem_left _ _ (Ideal.mem_span_singleton_self g)1038  exact ⟨(Ideal.quotientMapₐ (Ideal.span {g}) alpha hle).toLinearMap, fun h => rfl⟩1039 1040/-- If `alpha f = e ^ d * g`, then `h ↦ c * alpha h` descends to an `O`-linear map1041`R ⧸ (f) → C ⧸ (g)`. -/1042theorem strict_quotient_map_exists (O R C : Type) [CommRing O] [CommRing R] [CommRing C]1043    [Algebra O R] [Algebra O C] (alpha : R →ₐ[O] C) (f : R) (g e c : C) (d : ℕ)1044    (hf : alpha f = e ^ d * g) :1045    ∃ phi : (R ⧸ Ideal.span {f}) →ₗ[O] (C ⧸ Ideal.span {g}), ∀ h : R, phi1046      (Ideal.Quotient.mk (Ideal.span {f}) h) = Ideal.Quotient.mk (Ideal.span {g})1047          (c * alpha h) := by1048  let L : R →ₗ[O] (C ⧸ Ideal.span {g}) :=1049    (Ideal.Quotient.mkₐ O (Ideal.span {g})).toLinearMap ∘ₗ (LinearMap.mulLeft O c) ∘ₗ1050        alpha.toLinearMap1051  have hL : (Ideal.span {f}).restrictScalars O ≤ LinearMap.ker L := by1052    intro x hx1053    rw [Submodule.restrictScalars_mem, Ideal.mem_span_singleton'] at hx1054    obtain ⟨r, rfl⟩ := hx1055    simp only [LinearMap.mem_ker, L, LinearMap.coe_comp, Function.comp_apply,1056      AlgHom.toLinearMap_apply, LinearMap.mulLeft_apply, map_mul, hf,1057      Ideal.Quotient.mkₐ_eq_mk]1058    rw [Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_span_singleton_self g)]1059    simp1060  exact ⟨((Ideal.span {f}).restrictScalars O).liftQ L hL, fun h => rfl⟩1061 1062/-- The strict quotient map `phi` and the inclusion `iota` satisfy `e ^ d * phi = pi ^ s • iota`. -/1063private theorem strict_quotient_maps_relation (O R C : Type) [CommRing O] [CommRing R] [CommRing C]1064    [Algebra O R] [Algebra O C] (alpha : R →ₐ[O] C) (f : R) (g e c : C) (d : ℕ)1065    (pi : O) (s : ℕ) (hpi : (algebraMap O C pi) ^ s = e ^ d * c)1066    (phi iota : (R ⧸ Ideal.span {f}) →ₗ[O] (C ⧸ Ideal.span {g}))1067    (hphi : ∀ h : R, phi (Ideal.Quotient.mk (Ideal.span {f}) h) = Ideal.Quotient.mk (Ideal.span {g})1068    (c * alpha h))1069    (hiota : ∀ h : R, iota (Ideal.Quotient.mk (Ideal.span {f}) h) = Ideal.Quotient.mk1070    (Ideal.span {g}) (alpha h)) (u : R ⧸ Ideal.span {f}) :1071    Ideal.Quotient.mk (Ideal.span {g}) (e^d) * phi u = (pi^s) • iota u := by1072  obtain ⟨h, rfl⟩ := Ideal.Quotient.mk_surjective u1073  rw [hphi, hiota, Algebra.smul_def, ← map_mul, ← Ideal.Quotient.mk_algebraMap, ← map_mul,1074    map_pow, hpi, mul_assoc]1075 1076/-- If `iota` is injective and `pi` is a nonzerodivisor on `C ⧸ (g)`, then the strict quotient1077map `phi` is injective. -/1078theorem strict_quotient_map_injective (O R C : Type) [CommRing O] [CommRing R] [CommRing C]1079    [Algebra O R] [Algebra O C] (alpha : R →ₐ[O] C) (f : R) (g e c : C) (d : ℕ)1080    (pi : O) (s : ℕ) (hpi : (algebraMap O C pi) ^ s = e ^ d * c)1081    (phi iota : (R ⧸ Ideal.span {f}) →ₗ[O] (C ⧸ Ideal.span {g}))1082    (hphi : ∀ h : R, phi (Ideal.Quotient.mk (Ideal.span {f}) h) = Ideal.Quotient.mk (Ideal.span {g})1083    (c * alpha h))1084    (hiota : ∀ h : R, iota (Ideal.Quotient.mk (Ideal.span {f}) h) = Ideal.Quotient.mk1085    (Ideal.span {g}) (alpha h)) (hiota_inj : Function.Injective iota)1086    (hpireg : Function.Injective (fun y : C ⧸ Ideal.span {g} => (pi : O) • y)) :1087    Function.Injective phi := by1088  have key : ∀ x : C ⧸ Ideal.span {g}, (pi ^ s) • x = 0 → x = 0 := fun x h =>1089    IsSMulRegular.pow s hpireg (h.trans (smul_zero _).symm)1090  rw [injective_iff_map_eq_zero]1091  intro u hu1092  have h := strict_quotient_maps_relation O R C alpha f g e c d pi s hpi phi iota hphi hiota u1093  rw [hu, mul_zero] at h1094  apply hiota_inj1095  rw [map_zero]1096  exact key _ h.symm1097 1098/-! ### Strict transforms across the two charts -/1099 1100/-- Ring isomorphisms commute with colon ideals. -/1101private theorem colon_map_ringEquiv {A B : Type*} [CommRing A] [CommRing B] (e : A ≃+* B)1102    (I : Ideal A) (y : A) :1103    (I.colon {y}).map (e : A →+* B) = (I.map (e : A →+* B)).colon {e y} := by1104  ext z1105  rw [Ideal.map_comap_of_equiv, Ideal.map_comap_of_equiv, Ideal.mem_comap,1106    Submodule.mem_colon_singleton, Submodule.mem_colon_singleton, Ideal.mem_comap]1107  simp only [smul_eq_mul, map_mul, RingEquiv.symm_apply_apply]1108 1109/-- Colon by `y * v` equals colon by `y` for a unit `v`. -/1110private theorem colon_singleton_mul_unit {B : Type*} [CommRing B] (K : Ideal B) (y v : B)1111    (hv : IsUnit v) :1112    K.colon {y * v} = K.colon {y} := by1113  ext z1114  rw [Submodule.mem_colon_singleton, Submodule.mem_colon_singleton, smul_eq_mul, smul_eq_mul,1115    ← mul_assoc, Ideal.mul_unit_mem_iff_mem _ hv]1116 1117/-- Transport of strict transforms along an isomorphism of completed local rings compatible1118with the base maps and with `x = t * unit`. -/1119private theorem strictTransformAt_map_of_compat (R : Type) [CommRing R] (t x : R)1120    (PA : Ideal (BlowupChart R t x)) [PA.IsPrime]1121    (PB : Ideal (BlowupChart R x t)) [PB.IsPrime]1122    (Ψ : CompletedLocalAt (BlowupChart R t x) PA ≃+* CompletedLocalAt (BlowupChart R x t) PB)1123    (u : CompletedLocalAt (BlowupChart R x t) PB) (hu : IsUnit u)1124    (hbase : ∀ r : R, Ψ (completedPointMap _ PA (chartBase R t x r)) = completedPointMap _ PB1125        (chartBase R x t r))1126    (hx : completedPointMap _ PB (chartBase R x t x) = Ψ1127        (completedPointMap _ PA (chartBase R t x t)) * u)1128    (d : ℕ) (J : Ideal R) :1129    (strictTransformAt R t x PA d J).map Ψ.toRingHom = strictTransformAt R x t PB d J := by1130  have hJ : (J.map ((completedPointMap (BlowupChart R t x) PA).comp (chartBase R t x))).map1131      (Ψ : _ →+* _) =1132      J.map ((completedPointMap (BlowupChart R x t) PB).comp (chartBase R x t)) := by1133    rw [Ideal.map_map]1134    congr 11135    exact RingHom.ext hbase1136  unfold strictTransformAt1137  have := colon_map_ringEquiv Ψ1138      (J.map ((completedPointMap (BlowupChart R t x) PA).comp (chartBase R t x)))1139    ((completedPointMap (BlowupChart R t x) PA (chartBase R t x t))^d)1140  refine this.trans ?_1141  rw [hJ, map_pow, hx, mul_pow, colon_singleton_mul_unit _ _ _ (hu.pow d)]1142 1143/-- At a common point of the two charts, the gluing isomorphism of completed local rings carries1144the left-chart strict transform of `J` to the right-chart strict transform. -/1145theorem strict_transform_common_point_transport (R : Type) [CommRing R] (t x : R)1146    (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta) (i : D.ι) (d : ℕ)1147    (J : Ideal R) :1148    (strictTransformAt R t x (leftPoint D (Sum.inl i)) d J).map1149      ((D.rightIso i).toRingHom.comp (D.leftIso i).symm.toRingHom) = strictTransformAt R x t1150      (rightPoint D (Sum.inl i)) d J := by1151  have key : ∀ a : BlowupChart R t x, ((D.leftIso i).symm.trans (D.rightIso i))1152      (completedPointMap _ ((D.Q i).comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))) a)1153          =1154      D.rightIso i1155          (completedPointMap _ (D.Q i)1156              (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) a)) := by1157    intro a1158    rw [RingEquiv.trans_apply, ← D.leftIso_compat i a, RingEquiv.symm_apply_apply]1159  have hR : ∀ r : R, algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x r) =1160      beta.right (chartBase R x t r) := by1161    intro r1162    have h1 : chartBase R x t r = algebraMap R (BlowupChart R x t) r := rfl1163    have h2 : chartBase R t x r = algebraMap R (BlowupChart R t x) r := rfl1164    rw [h1, h2, beta.right.commutes, ← IsScalarTower.algebraMap_apply]1165  have hbase : ∀ r : R, ((D.leftIso i).symm.trans (D.rightIso i))1166      (completedPointMap _ ((D.Q i).comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)))1167          (chartBase R t x r)) =1168      completedPointMap _ ((D.Q i).comap beta.right.toRingHom) (chartBase R x t r) := by1169    intro r1170    rw [key, hR]1171    exact D.rightIso_compat i _1172  have hrel : chartBase R t x t * chartSlope R t x = chartBase R t x x := by1173    unfold chartBase chartSlope1174    rw [RingHom.comp_apply, RingHom.comp_apply, ← map_mul, Ideal.Quotient.eq]1175    exact Ideal.subset_span rfl1176  have hx : completedPointMap _ ((D.Q i).comap beta.right.toRingHom) (chartBase R x t x) =1177      ((D.leftIso i).symm.trans (D.rightIso i))1178        (completedPointMap _ ((D.Q i).comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)))1179            (chartBase R t x t)) *1180      D.rightIso i1181          (completedPointMap _ (D.Q i)1182          (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartSlope R t x))) := by1183    rw [← hbase, ← hrel, key, key, map_mul, map_mul, map_mul]1184  have hunit : IsUnit1185      (D.rightIso i1186      (completedPointMap _ (D.Q i)1187      (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartSlope R t x)))) := by1188    exact ((IsLocalization.Away.algebraMap_isUnit (chartSlope R t x)).map _).map _1189  exact strictTransformAt_map_of_compat R t x _ _ ((D.leftIso i).symm.trans (D.rightIso i)) _ hunit1190      hbase hx d J1191 1192/-- If the local intersection length of `F` with `y ∈ P` vanishes, then `F` is a unit. -/1193private theorem span_eq_top_of_length_eq_zero {A : Type} [CommRing A] [IsNoetherianRing A]1194    (P : Ideal A) [P.IsPrime] (y : A) (hy : y ∈ P) (F : CompletedLocalAt A P)1195    (h : Module.length (CompletedLocalAt A P)1196        (CompletedLocalAt A P ⧸ Ideal.span {F, completedPointMap A P y}) = 0) :1197    Ideal.span {F} = ⊤ := by1198  have : IsNoetherianRing (Localization.AtPrime P) := IsLocalization.isNoetherianRing P.primeCompl _1199      inferInstance1200  rw [Module.length_eq_zero_iff, Ideal.Quotient.subsingleton_iff] at h1201  have hy' : completedPointMap A P y ∈ IsLocalRing.maximalIdeal (CompletedLocalAt A P) := by1202    have h1 : algebraMap A (Localization.AtPrime P) y ∈ IsLocalRing.maximalIdeal1203      (Localization.AtPrime P) := by1204      rw [← Localization.AtPrime.map_eq_maximalIdeal]1205      exact Ideal.mem_map_of_mem _ hy1206    rw [IsLocalRing.mem_maximalIdeal] at h1 ⊢1207    exact fun hu ↦ h1 ((isUnit_map_iff (algebraMap (Localization.AtPrime P) _) _).mp hu)1208  by_contra hF1209  have hF' : F ∈ IsLocalRing.maximalIdeal (CompletedLocalAt A P) :=1210    fun hu ↦ hF (Ideal.span_singleton_eq_top.mpr hu)1211  have : Ideal.span {F, completedPointMap A P y} ≤ IsLocalRing.maximalIdeal _ :=1212    Ideal.span_le.mpr (Set.pair_subset hF' hy')1213  exact (IsLocalRing.maximalIdeal.isMaximal _).ne_top (top_le_iff.mp (h ▸ this))1214 1215/-- For an ideal `J` of a fixed tangent cell, the strict transform of `J` at a point of the1216exceptional divisor where the tangent divisor `Dv` has multiplicity zero is the unit ideal. -/1217private theorem cell_strictTransformAt_eq_top (O : Type) [CommRing O] [IsDomain O]1218    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1219    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)1220    (a b : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a b)]1221    [IsRegularLocalRing (ConcreteSurface O pi u a b)]1222    (S : SurfaceData O (ConcreteSurface O pi u a b))1223    (hS : S.t = surfaceT O pi u a b ∧ S.x = surfaceX O pi u a b)1224    (e : ((BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) ⧸1225    chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) ≃+*1226    Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))1227    (he : ∀ r : (ConcreteSurface O pi u a b), e1228    (Ideal.Quotient.mk1229    (chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))1230    ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) r)) =1231    Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))1232    (heZ : e (Ideal.Quotient.mk1233    (chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))1234    (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))) =1235    Polynomial.X)1236    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))1237    (hinf : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1238    (surfaceX O pi u a b)).IsPrime) (s : State) (d : ℕ) (J : Ideal (ConcreteSurface O pi u a b))1239    (hJ : J ∈ fixedTangentCell O _ S s d Dv) :1240    (∀ φ, Dv (some φ) = 0 → strictTransformAt _ _ _1241      (directionPoint _ (surfaceT O pi u a b) (surfaceX O pi u a b) e φ) d J = ⊤) ∧1242    (Dv none = 0 → strictTransformAt _ (surfaceX O pi u a b) (surfaceT O pi u a b)1243      (infinityPoint _ (surfaceT O pi u a b) (surfaceX O pi u a b)) d J = ⊤) := by1244  rcases S with ⟨pi', hpi', t', x', v', a', b', ha', hpar, hdim, hcomp, hinj, hres, hrc, hvert⟩1245  simp only at hS1246  obtain ⟨rfl, rfl⟩ := hS1247  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set _)).IsMaximal := by1248    rw [hpar]; infer_instance1249  have hdp := directionPoint_properties (ConcreteSurface O pi u a b) _ _ e he heZ1250  have hinfP := infinity_point_maximal O _ ⟨pi', hpi', surfaceT O pi u a b,1251    surfaceX O pi u a b, v', a', b', ha', hpar, hdim, hcomp, hinj, hres, hrc, hvert⟩1252  have : (infinityPoint _ (surfaceT O pi u a b) (surfaceX O pi u a b)).IsMaximal := hinfP.11253  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)1254      (surfaceX O pi u a b)1255  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)1256      (surfaceT O pi u a b)1257  obtain ⟨f, c, H, rfl, hf, hH, hc, hne⟩ :=1258    fixed_tangent_cell_generator_coefficients O _ _ s d Dv J hJ1259  have hred := reduced_form_eq_of_residue_coeff _ d c H hH.2.1 hc1260  refine ⟨fun φ hz ↦ ?_, fun hz ↦ ?_⟩1261  · have : (directionPoint _ (surfaceT O pi u a b) (surfaceX O pi u a b) e φ).IsMaximal :=1262      (hdp.1 φ).11263    have hP := (hdp.1 φ).2.11264    rw [(concrete_strict_transform_generators O pi hpi u a b ha d f c hf _ hP _ hinfP.2.11265      hinfP.2.2.1).1]1266    refine span_eq_top_of_length_eq_zero _ _ hP _ ?_1267    rw [concrete_strict_transform_multiplicity O pi hpi u a b ha d c hne _ hP e he heZ φ.val1268      φ.property (hdp.1 φ).2.2.2, hred, hH.2.2.2, (count_normalizedFactors_divisorAffinePolynomial1269      _ Dv _ (Polynomial.leadingCoeff_ne_zero.mpr hH.1) φ).1, hz]1270    rfl1271  · have : (directionPoint _ (surfaceT O pi u a b) (surfaceX O pi u a b) e1272        (zeroAffine _)).IsMaximal := (hdp.1 _).11273    rw [(concrete_strict_transform_generators O pi hpi u a b ha d f c hf _1274      (hdp.1 (zeroAffine _)).2.1 _ hinfP.2.1 hinfP.2.2.1).2]1275    refine span_eq_top_of_length_eq_zero _ _ hinfP.2.1 _ ?_1276    rw [concrete_infinity_strict_transform_multiplicity O pi hpi u a b ha d c hne _ hinfP.2.11277      hinfP.2.2.1, hred, ← hH.2.2.1, hz]1278    rfl1279 1280/-- If two ideals of the same fixed tangent cell have equal strict transforms at the points of1281positive divisor multiplicity, and the first has the prescribed strict transforms at all datum1282points, then so does the second. -/1283theorem cell_strict_transforms_agree_at_datum_points (O : Type) [CommRing O] [IsDomain O]1284    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1285    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)1286    (a b : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a b)]1287    [IsRegularLocalRing (ConcreteSurface O pi u a b)]1288    (S : SurfaceData O (ConcreteSurface O pi u a b))1289    (hS : S.t = (surfaceT O pi u a b) ∧ S.x = (surfaceX O pi u a b) ∧ S.a = a ∧ S.b = b)1290    (e : ((BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) ⧸1291    chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) ≃+*1292    Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))1293    (he : ∀ r : (ConcreteSurface O pi u a b), e1294    (Ideal.Quotient.mk1295    (chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))1296    ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) r)) =1297    Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))1298    (heZ : e (Ideal.Quotient.mk1299    (chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))1300    (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))) =1301    Polynomial.X) (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))1302    (hinf : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1303    (surfaceX O pi u a b)).IsPrime) (s : State) (d : ℕ) (J₁ J₂ : Ideal (ConcreteSurface O pi u a b))1304    (h₁ : J₁ ∈ (fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv))1305    (h₂ : J₂ ∈ (fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv))1306    (heq : ∀ Q : divisorSupport Dv, divisorStrictTransform (ConcreteSurface O pi u a b)1307    (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf d J₁ Q = divisorStrictTransform1308    (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf d J₂ Q)1309    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1310    (surfaceX O pi u a b))1311    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)1312    beta) (hm : MatchesDivisor e D Dv)1313    (hst₁ : ∀ s : D.ι ⊕ D.ι0, strictTransformAt (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1314    (surfaceX O pi u a b) (leftPoint D s) d J₁ = Ideal.span {leftData D s})1315    (hst₁r : ∀ s : D.ι ⊕ D.ιinf, strictTransformAt (ConcreteSurface O pi u a b)1316    (surfaceX O pi u a b) (surfaceT O pi u a b) (rightPoint D s) d J₁ = Ideal.span {rightData D s})1317    :1318    (∀ s : D.ι ⊕ D.ι0, strictTransformAt (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1319      (surfaceX O pi u a b) (leftPoint D s) d J₂ = Ideal.span {leftData D s}) ∧ ∀ s : D.ι ⊕ D.ιinf,1320      strictTransformAt (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)1321      (rightPoint D s) d J₂ = Ideal.span {rightData D s} := by1322  rcases S with ⟨pi', hpi', t', x', v', a', b', ha', hpar, hdim, hcomp, hinj, hres, hrc, hvert⟩1323  simp only at hS1324  obtain ⟨rfl, rfl, -, -⟩ := hS1325  set S₀ : SurfaceData O (ConcreteSurface O pi u a b) := ⟨pi', hpi', surfaceT O pi u a b,1326    surfaceX O pi u a b, v', a', b', ha', hpar, hdim, hcomp, hinj, hres, hrc, hvert⟩1327  have htop := fun J (hJ : J ∈ fixedTangentCell O _ S₀ s d Dv) ↦1328    cell_strictTransformAt_eq_top O pi hpi u a b ha S₀ ⟨rfl, rfl⟩ e he heZ Dv hinf s d J hJ1329  have left_eq : ∀ φ, strictTransformAt _ _ _1330      (directionPoint _ (surfaceT O pi u a b) (surfaceX O pi u a b) e φ) d J₂ =1331      strictTransformAt _ _ _ (directionPoint _ (surfaceT O pi u a b) (surfaceX O pi u a b) e φ) d1332        J₁ := fun φ ↦ by1333    by_cases hpos : 0 < Dv (some φ)1334    · exact (heq ⟨some φ, hpos⟩).symm1335    · rw [(htop J₂ h₂).1 φ (by omega), (htop J₁ h₁).1 φ (by omega)]1336  have right_eq : strictTransformAt _ (surfaceX O pi u a b) (surfaceT O pi u a b)1337      (infinityPoint _ (surfaceT O pi u a b) (surfaceX O pi u a b)) d J₂ =1338      strictTransformAt _ (surfaceX O pi u a b) (surfaceT O pi u a b)1339        (infinityPoint _ (surfaceT O pi u a b) (surfaceX O pi u a b)) d J₁ := by1340    by_cases hpos : 0 < Dv none1341    · exact (heq ⟨none, hpos⟩).symm1342    · rw [(htop J₂ h₂).2 (by omega), (htop J₁ h₁).2 (by omega)]1343  -- Transport along an equality of points (the `IsPrime` instances block a plain `rw`).1344  have key : ∀ {T X : ConcreteSurface O pi u a b} (P P' : Ideal (BlowupChart _ T X)) [P.IsPrime]1345      [P'.IsPrime], P = P' → strictTransformAt _ T X P' d J₂ = strictTransformAt _ T X P' d J₁ →1346      strictTransformAt _ T X P d J₂ = strictTransformAt _ T X P d J₁ := by1347    intro T X P P' _ _ h; subst h; exact id1348  have hleft : ∀ s, strictTransformAt _ _ _ (leftPoint D s) d J₂ = strictTransformAt _ _ _1349      (leftPoint D s) d J₁ := by1350    rintro (i | k)1351    · obtain ⟨φ, hφ, hQ, -⟩ := hm.common i1352      refine key _ (directionPoint _ _ _ e φ) ?_ (left_eq φ)1353      change (D.Q i).comap _ = _1354      rw [hQ]1355      exact (direction_point_overlap_maximal O _ S₀ e he heZ φ hφ).2.21356    · exact key _ _ (hm.zero k).1 (left_eq _)1357  refine ⟨fun s ↦ (hleft s).trans (hst₁ s), ?_⟩1358  rintro (i | l)1359  · rw [← strict_transform_common_point_transport, hleft, strict_transform_common_point_transport]1360    exact hst₁r _1361  · rw [key (rightPoint D (Sum.inr l)) _ (hm.inf l).1 right_eq]1362    exact hst₁r _1363 1364/-- Recovering a strict transform equation from its truncations: if `φ ≡ e ^ d * F j` modulo1365`e ^ j` and `(F j, e ^ j) = (g, e ^ j)` for all `j`, then `φ = e ^ d * g * v` for a unit `v`. -/1366theorem strict_transform_equation_from_levels (S : Type) [CommRing S] [IsLocalRing S]1367    [IsNoetherianRing S] (e g : S) (he : e ∈ IsLocalRing.maximalIdeal S)1368    (hereg : Function.Injective (fun a : S => e * a))1369    (hg : Function.Injective1370    (fun a : S ⧸ Ideal.span {e} => Ideal.Quotient.mk (Ideal.span {e}) g * a)) (d : ℕ) (F : ℕ → S)1371    (hFideal : ∀ j : ℕ, Ideal.span {F j, e^j} = Ideal.span {g, e^j}) (φ : S)1372    (hφ : ∀ j : ℕ, φ - e^d * F j ∈ Ideal.span {e^j}) :1373    ∃ v : Sˣ, φ = e^d * g * (v : S) := by1374  -- injectivity of multiplication by e^n1375  have hpow : ∀ n : ℕ, ∀ a b : S, e ^ n * a = e ^ n * b → a = b := fun n _ _ h =>1376    IsLeftRegular.pow n hereg h1377  -- Step A: φ = e^d ψ1378  obtain ⟨t, ht⟩ := Ideal.mem_span_singleton'.mp (hφ d)1379  set ψ := F d + t with hψ1380  have hφψ : φ = e ^ d * ψ := by rw [hψ]; linear_combination -ht1381  -- Step B: ψ = F (d+k) + e^k s1382  have hB : ∀ k : ℕ, ∃ s : S, ψ = F (d + k) + e ^ k * s := by1383    intro k1384    obtain ⟨s, hs⟩ := Ideal.mem_span_singleton'.mp (hφ (d + k))1385    refine ⟨s, hpow d _ _ ?_⟩1386    rw [← hφψ]1387    linear_combination -hs1388  -- Step C: ψ ∈ span {g}1389  have hC : ψ ∈ Ideal.span {g} := by1390    have key := Ideal.iInf_pow_smul_eq_bot_of_isLocalRing (I := Ideal.span {e})1391      (M := S ⧸ Ideal.span {g})1392      (by rw [Ne, Ideal.span_singleton_eq_top]; exact (IsLocalRing.mem_maximalIdeal e).mp he)1393    rw [← Ideal.Quotient.eq_zero_iff_mem]1394    have : (Ideal.Quotient.mk (Ideal.span {g}) ψ) ∈1395        (⨅ i : ℕ, (Ideal.span {e}) ^ i • ⊤ : Submodule S (S ⧸ Ideal.span {g})) := by1396      rw [Submodule.mem_iInf]1397      intro k1398      obtain ⟨s, hs⟩ := hB k1399      have hF : F (d + k) ∈ Ideal.span {g, e ^ (d + k)} := by1400        rw [← hFideal]; exact Ideal.subset_span (by simp)1401      obtain ⟨a, b, hab⟩ := Ideal.mem_span_pair.mp hF1402      have : Ideal.Quotient.mk (Ideal.span {g}) ψ =1403          e ^ k • Ideal.Quotient.mk (Ideal.span {g}) (b * e ^ d + s) := by1404        rw [Algebra.smul_def, Ideal.Quotient.algebraMap_eq, ← map_mul,1405          Ideal.Quotient.eq, Ideal.mem_span_singleton']1406        refine ⟨a, ?_⟩1407        rw [hs, ← hab]; ring1408      rw [this]1409      exact Submodule.smul_mem_smul (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self e) k)1410        Submodule.mem_top1411    rw [key] at this1412    simpa using this1413  obtain ⟨v₀, hv₀⟩ := Ideal.mem_span_singleton'.mp hC1414  -- Step D: v₀ is a unit1415  obtain ⟨s, hs⟩ := hB 11416  have hg1 : g ∈ Ideal.span {F (d + 1), e ^ (d + 1)} := by1417    rw [hFideal]; exact Ideal.subset_span (by simp)1418  obtain ⟨a, b, hab⟩ := Ideal.mem_span_pair.mp hg11419  have hmem : 1 - a * v₀ ∈ Ideal.span {e} := by1420    rw [← Ideal.Quotient.eq_zero_iff_mem]1421    apply hg1422    simp only [mul_zero]1423    rw [← map_mul, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton']1424    refine ⟨b * e ^ d - a * s, ?_⟩1425    have : F (d + 1) = v₀ * g - e * s := by rw [hv₀]; linear_combination -hs1426    rw [this] at hab1427    linear_combination hab1428  have hv : IsUnit v₀ := isUnit_of_mul_isUnit_right <|1429    (IsLocalRing.isUnit_or_isUnit_one_sub_self (a * v₀)).resolve_right1430      ((IsLocalRing.mem_maximalIdeal _).1 ((Ideal.span_singleton_le_iff_mem _).2 he hmem))1431  refine ⟨hv.unit, ?_⟩1432  rw [IsUnit.unit_spec, hφψ, ← hv₀]; ring1433 1434/-- If `f' ∈ (t, x) ^ d` and its strict transform at `P` is `(g)`, then `f' ∈ (g)` locally. -/1435private theorem mem_strictTransform_of_mem_pow (R : Type) [CommRing R] (t x : R)1436    (P : Ideal (BlowupChart R t x)) [P.IsPrime]1437    (d : ℕ) (f' : R) (hd : f' ∈ (Ideal.span {t,x}) ^ d)1438    (g : CompletedLocalAt (BlowupChart R t x) P)1439    (h : strictTransformAt R t x P d (Ideal.span {f'}) = Ideal.span {g}) :1440    completedPointMap (BlowupChart R t x) P (algebraMap R (BlowupChart R t x) f') ∈ Ideal.span1441      {g} := by1442  have hmap : (Ideal.span ({t,x} : Set R)).map (chartBase R t x) ≤ Ideal.span1443      {chartBase R t x t} := by1444    rw [Ideal.map_span, Ideal.span_le]1445    rintro _ ⟨y, hy, rfl⟩1446    rcases hy with rfl | rfl1447    · exact Ideal.subset_span rfl1448    · rw [← blowup_chart_relation]1449      exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)1450  have h1 : chartBase R t x f' ∈ Ideal.span {chartBase R t x t ^ d} := by1451    rw [← Ideal.span_singleton_pow]1452    exact Ideal.pow_right_mono hmap d1453        (Ideal.map_pow (chartBase R t x) _ d ▸ Ideal.mem_map_of_mem _ hd)1454  obtain ⟨F, hF⟩ := Ideal.mem_span_singleton'.mp h11455  have halg : algebraMap R (BlowupChart R t x) f' = chartBase R t x f' := rfl1456  set ψ := completedPointMap (BlowupChart R t x) P1457  have hcol : ψ F ∈ strictTransformAt R t x P d (Ideal.span {f'}) := by1458    unfold strictTransformAt1459    rw [Submodule.mem_colon_singleton, smul_eq_mul, Ideal.map_span, Set.image_singleton]1460    refine Ideal.mem_span_singleton'.mpr ⟨1, ?_⟩1461    simp only [RingHom.comp_apply, one_mul]1462    rw [← hF, map_mul, map_pow]1463  rw [h] at hcol1464  rw [halg, ← hF, map_mul]1465  exact Ideal.mul_mem_right _ _ hcol1466 1467/-- If `f' ∈ (t, x) ^ d` has the given strict transforms at all datum points, then its image in1468the chart pair lies in the curve ideal lattice of every level `j`. -/1469theorem strict_transforms_give_level_lattice_membership (R : Type) [CommRing R] (t x : R)1470    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]1471    [IsNoetherianRing (BlowupChart R x t)] (beta : BlowupRestriction R t x)1472    (D : TwoChartCurveData R t x beta) (d : ℕ) (G : GluedGenerators R t x beta d)1473    (hG : ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)} =1474    leftLevelKernel D j ∧ Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)} =1475    rightLevelKernel D j) (f' : R) (hd : f' ∈ (Ideal.span {t,x})^d)1476    (hleft : ∀ s : D.ι ⊕ D.ι0, strictTransformAt R t x (leftPoint D s) d (Ideal.span {f'}) =1477    Ideal.span {leftData D s})1478    (hright : ∀ s : D.ι ⊕ D.ιinf, strictTransformAt R x t (rightPoint D s) d (Ideal.span {f'}) =1479    Ideal.span {rightData D s}) (j : ℕ) :1480    surfaceToChartPair R t x f' ∈ curveIdealLattice R t x beta G j := by1481  obtain ⟨hl, hr⟩ := curve_ideal_lattice_eq_kernels R t x beta D d G hG j1482  have hd' : f' ∈ (Ideal.span {x,t})^d := by rwa [Set.pair_comm]1483  unfold curveIdealLattice1484  rw [Submodule.mem_prod]1485  refine ⟨?_, ?_⟩1486  · change algebraMap R (BlowupChart R t x) f' ∈ leftCurveIdeal R t x beta G j1487    rw [hl, leftKernel, finiteSupportKernel, Ideal.mem_iInf]1488    intro s1489    rw [Ideal.mem_comap, leftLevelIdeal, finiteLocalCurveIdeal]1490    exact Ideal.span_mono (by simp) (mem_strictTransform_of_mem_pow R t x _ d f' hd _ (hleft s))1491  · change algebraMap R (BlowupChart R x t) f' ∈ rightCurveIdeal R t x beta G j1492    rw [hr, rightKernel, finiteSupportKernel, Ideal.mem_iInf]1493    intro s1494    rw [Ideal.mem_comap, rightLevelIdeal, finiteLocalCurveIdeal]1495    exact Ideal.span_mono (by simp) (mem_strictTransform_of_mem_pow R x t _ d f' hd' _ (hright s))1496 1497end SurfaceBlowup