Volumes and strict transforms on 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.Blowup.TwoChartCurveData7import SurfaceBlowup.Measure.Atlas8import SurfaceBlowup.Surfaces.ConcreteAtlas9 10/-!11# Volumes and strict transforms on the concrete surface12 13We compute the measures of the crossing and single states of the concrete surface and verify14the local conditions on two-chart curve data on its blow-up: noetherian completions, regular15exceptional equations, transversality, and the identification of strict transforms.16 17## Main results18 19* `concrete_crossing_state_volume`, `concrete_single_state_volume`.20* `two_chart_datum_concrete_instances`, `two_chart_datum_concrete_transverse`.21* `concrete_strict_transforms_are_prescribed`.22 23Provenance: `coordinate_ideal_measurable_chart_sigma`, `concrete_{crossing,single}_state_volume`,24`two_chart_datum_concrete_{instances,transverse}`, `concrete_strict_transforms_are_prescribed`.25-/26 27open scoped ENNReal28 29namespace SurfaceBlowup30 31/-! ### Notation32 33Local notations for the charts of the blow-up of `R = ConcreteSurface O pi u a b` at its34closed point, taking the surface data as explicit arguments. -/35 36/-- The `t`-chart `R[x/t]` of the blow-up of the concrete surface `R` at `(t, x)`. -/37local notation:max "tChart" O:max pi:max u:max a:max b:max =>38  BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)39 40/-- The structure map `R → R[x/t]` of the `t`-chart. -/41local notation:max "tBase" O:max pi:max u:max a:max b:max =>42  chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)43 44/-- The slope `x/t` in the `t`-chart. -/45local notation:max "tSlope" O:max pi:max u:max a:max b:max =>46  chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)47 48/-- The `x`-chart `R[t/x]` of the blow-up of the concrete surface `R` at `(t, x)`. -/49local notation:max "xChart" O:max pi:max u:max a:max b:max =>50  BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)51 52/-- The structure map `R → R[t/x]` of the `x`-chart. -/53local notation:max "xBase" O:max pi:max u:max a:max b:max =>54  chartBase (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)55 56/-- The overlap of the two charts of the blow-up of the concrete surface at `(t, x)`. -/57local notation:max "tOverlap" O:max pi:max u:max a:max b:max =>58  BlowupOverlap (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)59 60/-! ### Volumes of crossing and single states -/61 62/-- The coordinate-ideal map of a division chart is measurable for the ideal-chart σ-algebra. -/63theorem coordinate_ideal_measurable_chart_sigma (O : Type) [CommRing O] [IsDomain O]64    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]65    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]66    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]67    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (R : Type) [CommRing R] [Algebra O R] [IsDomain R]68    [IsLocalRing R] (pi : O) (hpi : Irreducible pi) (hp0 : algebraMap O R pi ≠ 0)69    (hpm : algebraMap O R pi ∈ IsLocalRing.maximalIdeal R) (n : ℕ) (f : R) (b : Fin n → R)70    (hchart : IsDivisionChart O R pi f b) [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] :71    @Measurable (Fin n → O) (Ideal R) inferInstance (idealChartSigma O R pi)72      (coordinateIdeal pi f b) := by73  refine @measurable_generateFrom _ _ inferInstance _ _ ?_74  rintro T ⟨n', g, c, S, hc, hS, rfl⟩75  exact division_chart_preimage_image_measurable O htop R pi hpi hp0 hpm n n' f g b c hchart hc S hS76 77/-- The crossing state `(a, b, c, h)` of the concrete surface has measure78`(q - 1) q^(-(c + h))`, where `q` is the size of the residue field. -/79theorem concrete_crossing_state_volume (O : Type) [CommRing O] [IsDomain O]Proposition 3.380    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]81    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)82    (a b : ℕ) (ha : 0 < a) (hb : 0 < b) [IsDomain (ConcreteSurface O pi u a b)]83    [IsRegularLocalRing (ConcreteSurface O pi u a b)]84    (S : SurfaceData O (ConcreteSurface O pi u a b)) (hSpi : S.pi = pi)85    (hSt : S.t = surfaceT O pi u a b) (hSx : S.x = surfaceX O pi u a b) (hSa : S.a = a)86    (hSb : S.b = b)87    (e : (ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})88      ≃+* SpecialFiber (IsLocalRing.ResidueField O) a b)89    (he : ∀ s : TwoSeries O,90      e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})91      (surfaceMk O pi u a b s)) = Ideal.Quotient.mk (monomialIdeal (IsLocalRing.ResidueField O) a b)92      (residueSeries O s)) (c h : ℕ) (hc : 0 < c) (hh : 0 < h) [TopologicalSpace O]93    [IsTopologicalRing O] [CompactSpace O] [T2Space O] [SecondCountableTopology O]94    [MeasurableSpace O] [BorelSpace O] (htop : IsAdic (IsLocalRing.maximalIdeal O)) :95    (letI : MeasurableSpace (Ideal (ConcreteSurface O pi u a b)) := idealChartSigma O96        (ConcreteSurface O pi u a b) pi; ∃ A : IdealAtlas O (ConcreteSurface O pi u a b) pi97        (a*c+b*h) (surfaceStateSet O (ConcreteSurface O pi u a b) S (State.crossing a b c h)),98        stateMeasure O (ConcreteSurface O pi u a b) pi (a*c+b*h)99        (Nat.card (IsLocalRing.ResidueField O)) A Set.univ =100        ((Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞) - 1) *101        (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^(c+h)) := by102  let : MeasurableSpace (Ideal (ConcreteSurface O pi u a b)) := idealChartSigma O103      (ConcreteSurface O pi u a b) pi104  change ∃ A : IdealAtlas _ _ _ _ _, _105  obtain ⟨A, hA⟩ :=106      concrete_crossing_state_atlas_exists O pi hpi u a b ha hb S hSt hSx hSa hSb e he c h hc107      hh108  refine ⟨A, ?_⟩109  obtain ⟨hp0, hpm⟩ := surface_vertical_parameter O (ConcreteSurface O pi u a b) S110  rw [hSpi] at hp0 hpm111  refine crossing_state_volume O112      (ConcreteSurface O pi u a b) htop pi _ a b c h ha hb hc hh A ?_ hA113  intro i114  have := division_coordinate_module_isAdicComplete O pi hpi u a b ha (a*c+b*h)115  exact coordinate_ideal_measurable_chart_sigma O htop116      (ConcreteSurface O pi u a b) pi hpi hp0 hpm _ _ _ (A.chart i).isDivisionChart117 118/-- The single state `(a, c)` of the concrete surface (with `b = 0`) has measure `q^(-c)`, where119`q` is the size of the residue field. -/120theorem concrete_single_state_volume (O : Type) [CommRing O] [IsDomain O]Proposition 3.3121    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]122    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)123    (a : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a 0)]124    [IsRegularLocalRing (ConcreteSurface O pi u a 0)]125    (S : SurfaceData O (ConcreteSurface O pi u a 0)) (hSpi : S.pi = pi)126    (hSt : S.t = surfaceT O pi u a 0) (hSa : S.a = a) (hSb : S.b = 0)127    (e : (ConcreteSurface O pi u a 0 ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi})128      ≃+* SpecialFiber (IsLocalRing.ResidueField O) a 0)129    (he : ∀ s : TwoSeries O,130      e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi})131      (surfaceMk O pi u a 0 s)) = Ideal.Quotient.mk (monomialIdeal (IsLocalRing.ResidueField O) a 0)132      (residueSeries O s)) (c : ℕ) (hc : 0 < c) [TopologicalSpace O] [IsTopologicalRing O]133    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]134    (htop : IsAdic (IsLocalRing.maximalIdeal O)) :135    (letI : MeasurableSpace (Ideal (ConcreteSurface O pi u a 0)) := idealChartSigma O136        (ConcreteSurface O pi u a 0) pi; ∃ A : IdealAtlas O (ConcreteSurface O pi u a 0) pi (a*c)137        (surfaceStateSet O (ConcreteSurface O pi u a 0) S (State.single a c)),138        stateMeasure O (ConcreteSurface O pi u a 0) pi (a*c)139        (Nat.card (IsLocalRing.ResidueField O)) A Set.univ =140        (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^c) := by141  let : MeasurableSpace (Ideal (ConcreteSurface O pi u a 0)) := idealChartSigma O142      (ConcreteSurface O pi u a 0) pi143  obtain ⟨A, hA⟩ := concrete_single_state_atlas_exists O pi hpi u a ha S hSt hSa hSb e he c hc144  refine ⟨A, ?_⟩145  obtain ⟨hp0, hpm⟩ := surface_vertical_parameter O (ConcreteSurface O pi u a 0) S146  rw [hSpi] at hp0 hpm147  refine single_state_volume O (ConcreteSurface O pi u a 0) htop pi _ a c ha A ?_ hA148  intro i149  have := division_coordinate_module_isAdicComplete O pi hpi u a 0 ha (a*c)150  exact coordinate_ideal_measurable_chart_sigma O htop (ConcreteSurface O pi u a 0) pi hpi hp0 hpm151      _ _ _ (A.chart i).isDivisionChart152 153/-! ### Two-chart curve data on the concrete surface -/154 155/-- The completion at a prime `P` of a noetherian ring is a noetherian complete local ring whose156maximal ideal contains the image of any `e ∈ P`. -/157private theorem completion_isNoetherian_isDomain_of_equiv (A : Type) [CommRing A]158    [IsNoetherianRing A] (P : Ideal A) [P.IsPrime]159    (e : A) (he : e ∈ P) :160    ∃ _ : IsLocalRing (CompletedLocalAt A P), IsAdicComplete (IsLocalRing.maximalIdeal161      (CompletedLocalAt A P)) (CompletedLocalAt A P) ∧162      completedPointMap A P e ∈ IsLocalRing.maximalIdeal (CompletedLocalAt A P) := by163  refine ⟨inferInstance, inferInstance, ?_⟩164  rw [AdicCompletion.maximalIdeal_eq_map]165  exact Ideal.mem_map_of_mem _166    ((IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime P) P e).2 he)167 168/-- Injectivity of multiplication by `x` follows from that of multiplication by `z` along a ring169isomorphism sending `x` to `z` times a unit. -/170private theorem injective_mul_of_ringEquiv {A B : Type} [CommRing A] [CommRing B] (φ : A ≃+* B)171    {x : A} {z w : B} (h : φ x = z * w) (hw : IsUnit w)172    (hz : Function.Injective (fun y : B => z * y)) :173    Function.Injective (fun y : A => x * y) := by174  intro y y' hyy175  have h' := congrArg φ hyy176  simp only [map_mul, h, mul_assoc] at h'177  exact φ.injective (hw.mul_left_cancel (hz h'))178 179/-- At every point of two-chart curve data on the blow-up of the concrete surface, the completed180local ring is noetherian (complete local) and the exceptional equation is a non-zero-divisor. -/181theorem two_chart_datum_concrete_instances (O : Type) [CommRing O] [IsDomain O]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)185    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)186      (surfaceX O pi u a b))187    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b)188      (surfaceX O pi u a b) beta) :189    (∀ s : D.ι ⊕ D.ι0,190        IsNoetherianRing (CompletedLocalAt (tChart O pi u a b) (leftPoint D s)) ∧191        Function.Injective (fun y : (CompletedLocalAt (tChart O pi u a b) (leftPoint D s)) =>192          (completedPointMap (tChart O pi u a b) (leftPoint D s))193            (tBase O pi u a b (surfaceT O pi u a b)) * y)) ∧194      (∀ s : D.ι ⊕ D.ιinf,195        IsNoetherianRing (CompletedLocalAt (xChart O pi u a b) (rightPoint D s)) ∧196        Function.Injective (fun y : (CompletedLocalAt (xChart O pi u a b) (rightPoint D s)) =>197          (completedPointMap (xChart O pi u a b) (rightPoint D s))198            (xBase O pi u a b (surfaceX O pi u a b)) * y)) ∧199      ∀ p : AllPoints D, IsNoetherianRing (localRing D p) ∧ ∃ _ : IsLocalRing (localRing D p),200      IsAdicComplete (IsLocalRing.maximalIdeal (localRing D p)) (localRing D p) ∧201      localException D p ∈ IsLocalRing.maximalIdeal (localRing D p) := by202  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} :203      Set (ConcreteSurface O pi u a b))).IsMaximal :=204    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha205  obtain ⟨hLmax, -, hLt⟩ := two_chart_left_points_maximal _ _ _ beta D206  have hL : ∀ s, IsNoetherianRing (CompletedLocalAt (tChart O pi u a b) (leftPoint D s)) ∧207      Function.Injective (fun y : CompletedLocalAt (tChart O pi u a b) (leftPoint D s) =>208        completedPointMap _ (leftPoint D s) (tBase O pi u a b (surfaceT O pi u a b)) * y) := by209    intro s210    have := hLmax s211    exact ⟨(concrete_left_point_completion_instances O pi hpi u a b ha (leftPoint D s) (hLt s)).1,212      concrete_left_point_exceptional_regular O pi hpi u a b ha (leftPoint D s) (hLt s)⟩213  have hInf : ∀ l, IsNoetherianRing214      (CompletedLocalAt (xChart O pi u a b) (rightPoint D (Sum.inr l))) ∧215      Function.Injective (fun y : CompletedLocalAt (xChart O pi u a b) (rightPoint D (Sum.inr l)) =>216        completedPointMap _ (rightPoint D (Sum.inr l))217          (xBase O pi u a b (surfaceX O pi u a b)) * y) := by218    intro l219    have : (rightPoint D (Sum.inr l)).IsMaximal := D.maximalinf l220    have h := concrete_infinity_point_completion O pi hpi u a b ha (rightPoint D (Sum.inr l))221      (D.onEinf l) (D.slopeinf l)222    exact ⟨h.2.2.1, h.2.2.2.2⟩223  -- at an overlap point, transport from the `t`-chart along `φ = rightIso⁻¹ ≫ leftIso`224  have hR : ∀ i : D.ι, IsNoetherianRing225      (CompletedLocalAt (xChart O pi u a b) (rightPoint D (Sum.inl i))) ∧226      Function.Injective (fun y : CompletedLocalAt (xChart O pi u a b) (rightPoint D (Sum.inl i)) =>227        completedPointMap _ (rightPoint D (Sum.inl i))228          (xBase O pi u a b (surfaceX O pi u a b)) * y) := by229    intro i230    let P := (D.Q i).comap (algebraMap (tChart O pi u a b) (tOverlap O pi u a b))231    obtain ⟨hLn, hLinj⟩ : IsNoetherianRing (CompletedLocalAt _ P) ∧232        Function.Injective (fun y : CompletedLocalAt _ P =>233          completedPointMap _ P (tBase O pi u a b (surfaceT O pi u a b)) * y) := hL (Sum.inl i)234    let φ := (D.rightIso i).symm.trans (D.leftIso i)235    have hbeta : beta.right (xBase O pi u a b (surfaceX O pi u a b)) =236        algebraMap (tChart O pi u a b) (tOverlap O pi u a b)237          (tBase O pi u a b (surfaceX O pi u a b)) :=238      beta.right.commutes (surfaceX O pi u a b)239    have hφ : φ (completedPointMap (xChart O pi u a b) ((D.Q i).comap beta.right.toRingHom)240        (xBase O pi u a b (surfaceX O pi u a b))) =241        completedPointMap _ P (tBase O pi u a b (surfaceT O pi u a b)) *242          completedPointMap _ P (tSlope O pi u a b) := by243      have h1 := D.rightIso_compat i (xBase O pi u a b (surfaceX O pi u a b))244      rw [hbeta] at h1245      rw [← map_mul, blowup_chart_relation, ← h1]246      change D.leftIso i ((D.rightIso i).symm _) = _247      rw [RingEquiv.symm_apply_apply]248      exact D.leftIso_compat i _249    have hWnot : tSlope O pi u a b ∉ P := fun hW => (D.maximal i).ne_top250      (Ideal.eq_top_of_isUnit_mem _ hW (IsLocalization.Away.algebraMap_isUnit _))251    have hWunit : IsUnit (completedPointMap _ P (tSlope O pi u a b)) :=252      (IsLocalization.map_units (Localization.AtPrime P)253        (⟨_, hWnot⟩ : P.primeCompl)).map (localCompletionMap _)254    exact ⟨isNoetherianRing_of_ringEquiv _ φ.symm, injective_mul_of_ringEquiv φ hφ hWunit hLinj⟩255  have hNC : ∀ i : D.ι, IsNoetherianRing (CompletedLocalAt (tOverlap O pi u a b) (D.Q i)) :=256    fun i => by257      have : IsNoetherianRing (CompletedLocalAt (tChart O pi u a b)258        ((D.Q i).comap (algebraMap (tChart O pi u a b) (tOverlap O pi u a b)))) :=259        (hL (Sum.inl i)).1260      exact isNoetherianRing_of_ringEquiv _ (D.leftIso i).symm261  have : IsNoetherianRing (tChart O pi u a b) :=262    blowupChart_concrete_isNoetherianRing O pi u a b _ _263  have : IsNoetherianRing (xChart O pi u a b) :=264    blowupChart_concrete_isNoetherianRing O pi u a b _ _265  refine ⟨hL, fun s => s.casesOn hR hInf, ?_⟩266  rintro (i | k | l)267  · exact ⟨hNC i, completion_isNoetherian_isDomain_of_equiv _ (D.Q i) _ (D.onE i)⟩268  · exact ⟨(hL (Sum.inr k)).1,269      completion_isNoetherian_isDomain_of_equiv _ (leftPoint D (Sum.inr k)) _ (D.onE0 k)⟩270  · exact ⟨(hInf l).1,271      completion_isNoetherian_isDomain_of_equiv _ (rightPoint D (Sum.inr l)) _ (D.onEinf l)⟩272 273/-- Multiplication by `g` is injective modulo `e` iff `e ∣ g w` implies `e ∣ w`. -/274private theorem injective_mul_iff {S : Type} [CommRing S] (e g : S) :275    Function.Injective (fun w : S ⧸ Ideal.span {e} => Ideal.Quotient.mk (Ideal.span {e}) g * w) ↔276      ∀ w : S, e ∣ g * w → e ∣ w := by277  constructor278  · intro h w hw279    have h1 : Ideal.Quotient.mk (Ideal.span {e}) g * Ideal.Quotient.mk (Ideal.span {e}) w =280        Ideal.Quotient.mk (Ideal.span {e}) g * 0 := by281      rw [mul_zero, ← map_mul, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]282      exact hw283    have h2 := h h1284    rwa [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton] at h2285  · intro h x y hxy286    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x287    obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y288    simp only at hxy289    rw [← map_mul, ← map_mul, Ideal.Quotient.eq, Ideal.mem_span_singleton, ← mul_sub] at hxy290    rw [Ideal.Quotient.eq, Ideal.mem_span_singleton]291    exact h _ hxy292 293/-- At a point whose completion is a concrete surface with `e ↦ t`, a curve of finite colength294with `e` is transverse to `e`. -/295private theorem transverse_of_regular_local (A : Type) [CommRing A] [IsNoetherianRing A]296    (P : Ideal A) [P.IsMaximal]297    (e g : CompletedLocalAt A P)298    (O' : Type) [CommRing O'] [IsDomain O'] [IsDiscreteValuationRing O'] (pi' : O')299    (hpi' : Irreducible pi') (u' : (TwoSeries O')ˣ) (a' b' : ℕ) (ha' : 0 < a')300    (Eq : CompletedLocalAt A P ≃+* ConcreteSurface O' pi' u' a' b')301    (hE : Eq e = surfaceT O' pi' u' a' b') (L : ℕ)302    (hL : ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map303      (localCompletionMap (Localization.AtPrime P))) ^ L ≤ Ideal.span {g, e ^ 1}) :304    ∀ w, e ∣ g * w → e ∣ w := by305  obtain ⟨q, -⟩ := concrete_surface_quotient_T_equiv O' pi' hpi' u' a' b' ha'306  have hsymm : Eq.symm (surfaceT O' pi' u' a' b') = e := by rw [← hE]; simp307  have hreg := (concrete_surface_equiv_curve_length_and_regular (CompletedLocalAt A P) O' pi'308    u' a' b' Eq q g).2309  rw [hsymm] at hreg310  rw [← injective_mul_iff]311  refine hreg.mpr ?_312  intro h0313  have hmk : Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'}) (Eq g) = 0 := by314    simpa using h0315  rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton] at hmk316  have hge : e ∣ g := by317    have := map_dvd Eq.symm hmk318    rwa [hsymm, RingEquiv.symm_apply_apply] at this319  have hL' : ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map320      (localCompletionMap (Localization.AtPrime P)))^L ≤ Ideal.span {e} := by321    refine hL.trans (Ideal.span_le.mpr ?_)322    rintro z (rfl | rfl)323    · exact Ideal.mem_span_singleton.mpr hge324    · simp325  have hsurj := finite_completed_point_quotient_surjective A P L (Ideal.span {e}) hL'326  let θ : CompletedLocalAt A P ⧸ Ideal.span {e} →+* PowerSeries (IsLocalRing.ResidueField O') :=327    Ideal.Quotient.lift (Ideal.span {e})328      (q.toRingHom.comp329            ((Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'})).comp Eq.toRingHom))330      (fun z hz => by331        have := hE ▸ map_dvd Eq (Ideal.mem_span_singleton.mp hz)332        simp [Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_span_singleton.mpr this)])333  have hθ : Function.Surjective θ := by334    intro f335    obtain ⟨z, hz⟩ := q.surjective f336    obtain ⟨z, rfl⟩ := Ideal.Quotient.mk_surjective z337    refine ⟨Ideal.Quotient.mk _ (Eq.symm z), ?_⟩338    simp [θ, hz]339  let ψ : A →+* PowerSeries (IsLocalRing.ResidueField O') :=340    θ.comp ((Ideal.Quotient.mk (Ideal.span {e})).comp (completedPointMap A P))341  have hψ : Function.Surjective ψ := hθ.comp hsurj342  have hP : ∀ p ∈ P, ψ p = 0 := by343    intro p hp344    have hm : completedPointMap A P p ∈ (IsLocalRing.maximalIdeal (Localization.AtPrime P)).map345        (localCompletionMap (Localization.AtPrime P)) := Ideal.mem_map_of_mem _346      ((IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime P) P p).mpr hp)347    have hpow := hL' (Ideal.pow_mem_pow hm L)348    have : ψ p ^ L = 0 := by349      rw [← map_pow]350      simp only [ψ, RingHom.comp_apply]351      rw [map_pow, Ideal.Quotient.eq_zero_iff_mem.mpr hpow, map_zero]352    exact pow_eq_zero_iff'.mp this |>.1353  obtain ⟨c, hc⟩ := hψ PowerSeries.X354  have hcP : c ∉ P := fun hcP => PowerSeries.X_ne_zero (hc ▸ hP c hcP)355  obtain ⟨y, i, hi, hyi⟩ := Ideal.IsMaximal.exists_inv ‹P.IsMaximal› hcP356  have := congrArg ψ hyi357  rw [map_add, map_mul, hP i hi, hc, add_zero, map_one] at this358  have := congrArg PowerSeries.constantCoeff this359  simp at this360 361/-- Regularity of `g` modulo `e` transports along a ring isomorphism `Θ` to regularity of `Θ g`362modulo any unit multiple of `Θ e`. -/363private theorem dvd_transport {S T : Type} [CommRing S] [CommRing T] (Θ : S ≃+* T) {e g : S}364    {eT gT u : T} (hu : IsUnit u) (he : Θ e * u = eT) (hg : Θ g = gT)365    (h : ∀ w, e ∣ g * w → e ∣ w) : ∀ w, eT ∣ gT * w → eT ∣ w := by366  subst he hg367  intro w hw368  rw [hu.mul_right_dvd] at hw ⊢369  simpa using map_dvd Θ (h (Θ.symm w) (by simpa using map_dvd Θ.symm hw))370 371/-- The strict transforms in two-chart curve data on the blow-up of the concrete surface are372transverse to the exceptional divisor at every point. -/373theorem two_chart_datum_concrete_transverse (O : Type) [CommRing O] [IsDomain O]374    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]375    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)376    (a b : ℕ) (ha : 0 < a)377    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)378      (surfaceX O pi u a b))379    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b)380      (surfaceX O pi u a b) beta) :381    (∀ s : D.ι ⊕ D.ι0,382        Function.Injective383        (fun w : (CompletedLocalAt (tChart O pi u a b) (leftPoint D s)) ⧸ Ideal.span384          {(completedPointMap (tChart O pi u a b) (leftPoint D s))385            (tBase O pi u a b (surfaceT O pi u a b))} =>386          Ideal.Quotient.mk (Ideal.span {(completedPointMap (tChart O pi u a b) (leftPoint D s))387            (tBase O pi u a b (surfaceT O pi u a b))}) (leftData D s) * w)) ∧388      ∀ s : D.ι ⊕ D.ιinf,389      Function.Injective390      (fun w : (CompletedLocalAt (xChart O pi u a b) (rightPoint D s)) ⧸ Ideal.span391        {(completedPointMap (xChart O pi u a b) (rightPoint D s))392          (xBase O pi u a b (surfaceX O pi u a b))} =>393        Ideal.Quotient.mk (Ideal.span {(completedPointMap (xChart O pi u a b) (rightPoint D s))394          (xBase O pi u a b (surfaceX O pi u a b))}) (rightData D s) * w) := by395  have hmaxTX : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} :396      Set (ConcreteSurface O pi u a b))).IsMaximal :=397    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha398  have : IsNoetherianRing (ConcreteSurface O pi u a b) :=399    concrete_surface_isNoetherianRing O pi u a b400  obtain ⟨hLmax, -, hLmem⟩ := two_chart_left_points_maximal _ _ _ beta D401  obtain ⟨hRmax, -, hRmem⟩ := two_chart_right_points_maximal _ _ _ beta D402  obtain ⟨-, hLfin⟩ := two_chart_left_data_transverse_finite _ _ _ beta D 1403  obtain ⟨-, hRfin⟩ := two_chart_right_data_transverse_finite _ _ _ beta D 1404  have hleft : ∀ s : D.ι ⊕ D.ι0, ∀ w,405      completedPointMap _ (leftPoint D s) (tBase O pi u a b (surfaceT O pi u a b)) ∣406        leftData D s * w →407      completedPointMap _ (leftPoint D s) (tBase O pi u a b (surfaceT O pi u a b)) ∣ w := by408    intro s409    have := hLmax s410    obtain ⟨O', _, _, _, _, _, pi', u', a', b', hpi', ha', Eq, hEq⟩ :=411      concrete_left_point_completion_is_surface O pi hpi u a b ha (leftPoint D s) (hLmem s)412    obtain ⟨L, hL⟩ := hLfin s413    exact transverse_of_regular_local _ (leftPoint D s) _ _ O' pi' hpi' u' a' b' ha'414      Eq hEq L hL415  refine ⟨fun s => (injective_mul_iff _ _).mpr (hleft s), fun s => ?_⟩416  rw [injective_mul_iff]417  rcases s with i | l418  · refine dvd_transport ((D.leftIso i).symm.trans (D.rightIso i))419      (e := D.leftIso i (completedPointMap _ (D.Q i) (algebraMap _ _ (chartBase _ _ _ _))))420      (u := D.rightIso i (completedPointMap _ (D.Q i) (overlapSlope _ _ _)))421      (((IsLocalization.Away.algebraMap_isUnit _).map _).map _) ?_422      (congrArg (D.rightIso i) ((D.leftIso i).symm_apply_apply _))423      (by rw [D.leftIso_compat i]; exact hleft (Sum.inl i))424    rw [RingEquiv.trans_apply, RingEquiv.symm_apply_apply, ← map_mul, ← map_mul]425    exact (congrArg (fun z => D.rightIso i (completedPointMap _ _ z))426      (beta_right_chartBase_self (beta := beta)).symm).trans (D.rightIso_compat i _)427  · have := hRmax (Sum.inr l)428    obtain ⟨-, ⟨Eq, hEq⟩, -⟩ := concrete_infinity_point_completion O pi hpi u a b ha429      (rightPoint D (Sum.inr l)) (hRmem (Sum.inr l)) (D.slopeinf l)430    obtain ⟨L, hL⟩ := hRfin (Sum.inr l)431    exact transverse_of_regular_local _ (rightPoint D (Sum.inr l)) _ _ O pi hpi432      (xSubstUnit O u) (a + b) a (by omega) Eq hEq L hL433 434/-- The strict transforms of a curve `(f)` at the points of two-chart curve data are the435prescribed local equations. -/436theorem concrete_strict_transforms_are_prescribed (O : Type) [CommRing O] [IsDomain O]437    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]438    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)439    (a b : ℕ) (ha : 0 < a)440    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)441      (surfaceX O pi u a b))442    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b)443      (surfaceX O pi u a b) beta) (f : ConcreteSurface O pi u a b)444    (G : GluedGenerators (ConcreteSurface O pi u a b) (surfaceT O pi u a b)445      (surfaceX O pi u a b) beta (curveDataDegree D))446    (hf : ∀ j : ℕ,447      surfaceToCechInput (ConcreteSurface O pi u a b) (surfaceT O pi u a b)448      (surfaceX O pi u a b) j f =449      (cechInputLattice (ConcreteSurface O pi u a b) (surfaceT O pi u a b)450      (surfaceX O pi u a b) j).mkQ451      (gluedFunctionPair (ConcreteSurface O pi u a b) (surfaceT O pi u a b)452      (surfaceX O pi u a b) G j))453    (hG : ∀ j : ℕ,454      Ideal.span455      {Ideal.Quotient.mk456      ((chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b)457      (surfaceX O pi u a b))^j) (G.left j)} = leftLevelKernel D j ∧ Ideal.span458      {Ideal.Quotient.mk459      ((chartExceptional (ConcreteSurface O pi u a b) (surfaceX O pi u a b)460      (surfaceT O pi u a b))^j) (G.right j)} = rightLevelKernel D j) :461    (∀ s : D.ι ⊕ D.ι0,462        strictTransformAt (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)463        (leftPoint D s) (curveDataDegree D) (Ideal.span {f}) = Ideal.span {leftData D s}) ∧464      ∀ s : D.ι ⊕ D.ιinf,465      strictTransformAt (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)466      (rightPoint D s) (curveDataDegree D) (Ideal.span {f}) = Ideal.span {rightData D s} := by467  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} :468      Set (ConcreteSurface O pi u a b))).IsMaximal :=469    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha470  have h1 := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)471      (surfaceX O pi u a b)472  have h2 := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)473      (surfaceT O pi u a b)474  obtain ⟨hI1, hI2, -⟩ := two_chart_datum_concrete_instances O pi hpi u a b ha beta D475  obtain ⟨hT1, hT2⟩ := two_chart_datum_concrete_transverse O pi hpi u a b ha beta D476  refine ⟨fun s => ?_, fun s => ?_⟩477  · obtain ⟨_, hereg⟩ := hI1 s478    obtain ⟨v, hv⟩ := strict_transform_left_point_equation _ _ _ beta D _ G hG f hf s hereg (hT1 s)479    unfold strictTransformAt480    rw [principal_ideal_image, RingHom.comp_apply, chartBase_apply_eq_algebraMap, hv,481      Ideal.span_singleton_mul_right_unit v.isUnit]482    exact span_pow_mul_colon_eq _ _ _ hereg483  · obtain ⟨_, hreg⟩ := hI2 s484    exact global_function_strict_transform_at_right_point _ _ _ beta D _ G hG f hf s hreg (hT2 s)485 486end SurfaceBlowup