Lean sources / SurfaceBlowup / Surfaces / ConcreteAtlas.lean
Ideal atlases and curve data 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.CurveSections7import SurfaceBlowup.Blowup.StrictNormalizer8import SurfaceBlowup.Measure.Normalizer9 10/-!11# Ideal atlases and curve data on the concrete surface12 13We build ideal atlases of the crossing and single states of the concrete surface from residue14ideals of the special fiber, and we turn a form `∑ cᵢ t^(d-i) x^i` into two-chart curve data on15the blow-up.16 17## Main results18 19* `concrete_crossing_state_atlas_exists`, `concrete_single_state_atlas_exists`.20* `curve_datum_of_parent_function`.21 22Provenance: `concrete_{crossing,single}_state_atlas_exists`, `curve_datum_of_parent_function`.23-/24 25 26namespace SurfaceBlowup27 28/-- A unit of the special fiber has contact `0` with `t`. -/29private theorem contact_fiberT_eq_zero_of_isUnit (k : Type) [Field k] (a b : ℕ)30 {fb : SpecialFiber k a b} (hu : IsUnit fb) : contact fb (fiberT k a b) = 0 := by31 unfold contact32 rw [Ideal.eq_top_of_isUnit_mem _ (Ideal.subset_span (by simp)) hu]33 have : Subsingleton (SpecialFiber k a b ⧸ (⊤ : Ideal (SpecialFiber k a b))) :=34 Ideal.Quotient.subsingleton_iff.2 rfl35 exact Module.length_eq_zero36 37/-! ### Ideal atlases for crossing and single states -/38 39/-- The crossing state `(a, b, c, h)` of the concrete surface admits an ideal atlas indexed by the40crossing residue ideals of the special fiber. -/41theorem concrete_crossing_state_atlas_exists (O : Type) [CommRing O] [IsDomain O]42 [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]43 [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)44 (a b : ℕ) (ha : 0 < a) (hb : 0 < b) [IsDomain (ConcreteSurface O pi u a b)]45 [IsRegularLocalRing (ConcreteSurface O pi u a b)]46 (S : SurfaceData O (ConcreteSurface O pi u a b))47 (hSt : S.t = surfaceT O pi u a b) (hSx : S.x = surfaceX O pi u a b) (hSa : S.a = a)48 (hSb : S.b = b)49 (e : (ConcreteSurface O pi u a b ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})50 ≃+* SpecialFiber (IsLocalRing.ResidueField O) a b)51 (he : ∀ s : TwoSeries O,52 e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})53 (surfaceMk O pi u a b s)) = Ideal.Quotient.mk (monomialIdeal (IsLocalRing.ResidueField O) a b)54 (residueSeries O s)) (c h : ℕ) (hc : 0 < c) (hh : 0 < h) :55 ∃ A : IdealAtlas O (ConcreteSurface O pi u a b) pi (a*c+b*h)56 (surfaceStateSet O (ConcreteSurface O pi u a b) S (State.crossing a b c h)),57 Nonempty (A.ι ≃ crossingResidueIdeals (IsLocalRing.ResidueField O) a b c h) := by58 set k := IsLocalRing.ResidueField O59 have hcard := crossing_residue_ideal_count k a b c h ha hb hc hh60 have hfin : Finite (crossingResidueIdeals k a b c h) := by61 apply Nat.finite_of_card_ne_zero62 rw [hcard]63 have : 1 < Nat.card k := Finite.one_lt_card64 have h2 : Nat.card k - 1 ≠ 0 := by omega65 have h3 : 0 < Nat.card k := by omega66 positivity67 let : Fintype (crossingResidueIdeals k a b c h) := Fintype.ofFinite _68 have key : ∀ I : crossingResidueIdeals k a b c h,69 ∃ ch : IdealChart O (ConcreteSurface O pi u a b) pi (a*c+b*h),70 Ideal.span71 {e ((Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a b) pi})) ch.f)}72 = I.val := by73 intro I74 obtain ⟨fb, hI, hct, hcx⟩ := I.275 have hnu : ¬ IsUnit fb := fun hu ↦76 hc.ne' (by exact_mod_cast hct.symm.trans (contact_fiberT_eq_zero_of_isUnit k _ _ hu))77 have hreg := special_fiber_crossing_contact_regular k a b c h ha hb fb hct hcx78 have hlen := crossing_special_fiber_length k a b c h ha hb fb hct hcx79 obtain ⟨ch, hch⟩ := concrete_residue_ideal_chart_exists O pi hpi u a b ha e fb hnu hreg80 (a*c+b*h) hlen81 exact ⟨ch, by rw [hch, hI]⟩82 choose ch hch using key83 have hcov :=84 concrete_crossing_state_eq_union_cells O pi u a b ha hb S hSt hSx hSa hSb e he c h hc85 hh (fun I => (ch I).f) hch86 exact ⟨{ ι := crossingResidueIdeals k a b c h, chart := ch, cover := hcov.1, disjoint := hcov.2 },87 ⟨Equiv.refl _⟩⟩88 89/-- The single state `(a, c)` of the concrete surface (with `b = 0`) admits an ideal atlas indexed90by the single residue ideals of the special fiber. -/91theorem concrete_single_state_atlas_exists (O : Type) [CommRing O] [IsDomain O]92 [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]93 [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)94 (a : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a 0)]95 [IsRegularLocalRing (ConcreteSurface O pi u a 0)]96 (S : SurfaceData O (ConcreteSurface O pi u a 0))97 (hSt : S.t = surfaceT O pi u a 0) (hSa : S.a = a) (hSb : S.b = 0)98 (e : (ConcreteSurface O pi u a 0 ⧸ Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi})99 ≃+* SpecialFiber (IsLocalRing.ResidueField O) a 0)100 (he : ∀ s : TwoSeries O,101 e (Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi})102 (surfaceMk O pi u a 0 s)) = Ideal.Quotient.mk (monomialIdeal (IsLocalRing.ResidueField O) a 0)103 (residueSeries O s)) (c : ℕ) (hc : 0 < c) :104 ∃ A : IdealAtlas O (ConcreteSurface O pi u a 0) pi (a*c)105 (surfaceStateSet O (ConcreteSurface O pi u a 0) S (State.single a c)),106 Nonempty (A.ι ≃ singleResidueIdeals (IsLocalRing.ResidueField O) a c) := by107 set k := IsLocalRing.ResidueField O108 have hcard := single_residue_ideal_count k a c ha109 have hfin : Finite (singleResidueIdeals k a c) := by110 apply Nat.finite_of_card_ne_zero111 rw [hcard]112 have : 0 < Nat.card k := Nat.card_pos113 positivity114 let : Fintype (singleResidueIdeals k a c) := Fintype.ofFinite _115 have key : ∀ I : singleResidueIdeals k a c,116 ∃ ch : IdealChart O (ConcreteSurface O pi u a 0) pi (a*c),117 Ideal.span118 {e ((Ideal.Quotient.mk (Ideal.span {algebraMap O (ConcreteSurface O pi u a 0) pi})) ch.f)}119 = I.val := by120 intro I121 obtain ⟨fb, hI, hct⟩ := I.2122 have hnu : ¬ IsUnit fb := fun hu ↦123 hc.ne' (by exact_mod_cast hct.symm.trans (contact_fiberT_eq_zero_of_isUnit k _ _ hu))124 have hreg := special_fiber_single_contact_regular k a c ha fb hct125 have hlen := single_special_fiber_length k a c ha fb hct126 obtain ⟨ch, hch⟩ := concrete_residue_ideal_chart_exists O pi hpi u a 0 ha e fb hnu hreg127 (a*c) hlen128 exact ⟨ch, by rw [hch, hI]⟩129 choose ch hch using key130 have hcov := concrete_single_state_eq_union_cells O pi u a ha S hSt hSa hSb e he c hc131 (fun I => (ch I).f) hch132 exact ⟨{ ι := singleResidueIdeals k a c, chart := ch, cover := hcov.1, disjoint := hcov.2 },133 ⟨Equiv.refl _⟩⟩134 135section General136variable {R : Type} [CommRing R] (t x : R)137 138/-! ### Curve data from a parent function -/139 140/-- The chart structure map is the algebra map. -/141theorem chartBase_apply_eq_algebraMap (r : R) : chartBase R t x r = algebraMap R142 (BlowupChart R t x) r := rfl143 144/-- In `R[x/t]`, a form `∑ cᵢ t^(d-i) x^i` factors as `t^d ∑ cᵢ (x/t)^i`. -/145private theorem algebraMap_sum_eq_left (d : ℕ) (c : Fin (d + 1) → R) :146 algebraMap R (BlowupChart R t x) (∑ i : Fin (d+1), c i * t^(d - i.val) * x^i.val) =147 (chartBase R t x t)^d * ∑ i : Fin (d+1), algebraMap R (BlowupChart R t x) (c i) *148 (chartSlope R t x)^i.val := by149 rw [map_sum, Finset.mul_sum]150 refine Finset.sum_congr rfl fun i _ => ?_151 have hx : algebraMap R (BlowupChart R t x) x = chartBase R t x t * chartSlope R t x :=152 (blowup_chart_relation R t x).symm153 have hd : (chartBase R t x t)^d = (chartBase R t x t)^(d - i.val) *154 (chartBase R t x t)^i.val := by155 rw [← pow_add, Nat.sub_add_cancel (Nat.lt_succ_iff.mp i.isLt)]156 rw [map_mul, map_mul, map_pow, map_pow, hx, hd]; simp only [← chartBase_apply_eq_algebraMap]157 ring158 159/-- In `R[t/x]`, a form `∑ cᵢ t^(d-i) x^i` factors as `x^d ∑ cᵢ (t/x)^(d-i)`. -/160private theorem algebraMap_sum_eq_right (d : ℕ) (c : Fin (d + 1) → R) :161 algebraMap R (BlowupChart R x t) (∑ i : Fin (d+1), c i * t^(d - i.val) * x^i.val) =162 (chartBase R x t x)^d * ∑ i : Fin (d+1), algebraMap R (BlowupChart R x t) (c i) *163 (chartSlope R x t)^(d - i.val) := by164 rw [map_sum, Finset.mul_sum]165 refine Finset.sum_congr rfl fun i _ => ?_166 have ht : algebraMap R (BlowupChart R x t) t = chartBase R x t x * chartSlope R x t :=167 (blowup_chart_relation R x t).symm168 have hd : (chartBase R x t x)^d = (chartBase R x t x)^(d - i.val) *169 (chartBase R x t x)^i.val := by170 rw [← pow_add, Nat.sub_add_cancel (Nat.lt_succ_iff.mp i.isLt)]171 rw [map_mul, map_mul, map_pow, map_pow, ht, hd]; simp only [← chartBase_apply_eq_algebraMap]172 ring173 174/-- For a non-zero-divisor `e`, `(e^d g) : e^d = (g)`. -/175theorem span_pow_mul_colon_eq {S : Type} [CommRing S] (e g : S) (d : ℕ)176 (he : Function.Injective (fun y : S => e * y)) :177 (Ideal.span {e^d * g}).colon {e^d} = Ideal.span {g} := by178 have hed : IsLeftRegular (e^d) := IsLeftRegular.pow d (show IsLeftRegular e from he)179 ext y180 rw [Submodule.mem_colon_singleton, smul_eq_mul, Ideal.mem_span_singleton,181 Ideal.mem_span_singleton]182 constructor183 · rintro ⟨z, hz⟩184 refine ⟨z, hed ?_⟩185 simp only186 rw [mul_comm (e^d) y, hz]; ring187 · rintro ⟨z, rfl⟩188 exact ⟨z, by ring⟩189 190/-- If `f = t^d F` in the chart and `t` is regular at `P`, the strict transform of `(f)` is191`(F)`. -/192private theorem strictTransformAt_span_eq (P : Ideal (BlowupChart R t x)) [P.IsPrime] (d : ℕ)193 (f : R) (F : BlowupChart R t x)194 (hF : algebraMap R (BlowupChart R t x) f = (chartBase R t x t) ^ d * F)195 (he : Function.Injective (fun y : CompletedLocalAt (BlowupChart R t x) P =>196 completedPointMap (BlowupChart R t x) P (chartBase R t x t) * y)) :197 strictTransformAt R t x P d (Ideal.span {f}) =198 Ideal.span {completedPointMap (BlowupChart R t x) P F} := by199 unfold strictTransformAt200 rw [Ideal.map_span, Set.image_singleton, RingHom.comp_apply, chartBase_apply_eq_algebraMap, hF,201 map_mul, map_pow]202 exact span_pow_mul_colon_eq _ _ d he203 204/-- Ideals containing `I` are determined by their images in `S ⧸ I`. -/205private theorem quot_ext_eq {S : Type} [CommRing S] (I P1 P2 : Ideal S) (h1 : I ≤ P1) (h2 : I ≤ P2)206 (h : P1.map (Ideal.Quotient.mk I) = P2.map (Ideal.Quotient.mk I)) : P1 = P2 := by207 have k : ∀ P : Ideal S,208 I ≤ P → (P.map (Ideal.Quotient.mk I)).comap (Ideal.Quotient.mk I) = P := by209 intro P hP210 rw [Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective, ← RingHom.ker_eq_comap_bot,211 Ideal.mk_ker]212 exact sup_eq_left.mpr hP213 rw [← k P1 h1, ← k P2 h2, h]214 215/-- A maximal ideal avoiding `z` stays maximal in the localization away from `z`. -/216private theorem localization_map_maximal {A S : Type} [CommRing A] [CommRing S] [Algebra A S]217 (z : A)218 [IsLocalization.Away z S] (P : Ideal A) [hP : P.IsMaximal]219 (hz : z ∉ P) : (P.map (algebraMap A S)).IsMaximal ∧ (P.map (algebraMap A S)).comap220 (algebraMap A S) = P := by221 have hdisj : Disjoint ((Submonoid.powers z : Submonoid A) : Set A) P := by222 rw [Set.disjoint_left]223 rintro _ ⟨n, rfl⟩ hn224 exact hz (hP.isPrime.mem_of_pow_mem n hn)225 have hu := IsLocalization.under_map_of_isPrime_disjoint (Submonoid.powers z) S hP.isPrime hdisj226 refine ⟨?_, hu⟩227 rw [Ideal.isMaximal_def]228 refine ⟨fun htop => hP.ne_top ?_, fun J hJ => ?_⟩229 · rw [← hu, htop]; exact Ideal.comap_top230 · have hlt : P < J.under A := by231 rw [← hu]232 exact (IsLocalization.orderEmbedding (Submonoid.powers z) S).strictMono hJ233 have htop : J.under A = ⊤ := hP.out.2 _ hlt234 rw [← IsLocalization.map_under (Submonoid.powers z) S J, htop, Ideal.map_top]235 236/-- The reduction of the strict transform `∑ cᵢ (x/t)^i` to the exceptional line is nonzero. -/237private theorem reduction_ne_zero [(Ideal.span ({t,x} : Set R)).IsMaximal]238 (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial239 (R ⧸ Ideal.span ({t,x} : Set R)))240 (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =241 Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r))242 (heZ : e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X)243 (d : ℕ) (c : Fin (d+1) → R) (hne : ∃ i : Fin (d+1), c i ∉ Ideal.span {t, x}) :244 e (Ideal.Quotient.mk (chartExceptional R t x)245 (∑ i : Fin (d+1), algebraMap R (BlowupChart R t x) (c i) *246 (chartSlope R t x)^i.val)) ≠ 0 := by247 obtain ⟨i0, hi0⟩ := hne248 intro h249 apply hi0250 have h2 := congrArg (fun p => Polynomial.coeff p i0.val) h251 simp only [← chartBase_apply_eq_algebraMap, map_sum, map_mul, map_pow, he, heZ,252 Polynomial.finsetSum_coeff,253 Polynomial.coeff_C_mul_X_pow, Polynomial.coeff_zero] at h2254 rw [Finset.sum_eq_single i0] at h2255 · simpa [Ideal.Quotient.eq_zero_iff_mem] using h2256 · intro j _ hj257 rw [if_neg]258 intro hv; exact hj (Fin.ext hv.symm)259 · simp260 261/-- Finite contact transports along `Φ : (A_z)^_Q ≃ A^_P`, `P` the contraction of `Q`. -/262private theorem transport_finite {A : Type} [CommRing A] (z : A) (Q : Ideal (Localization.Away z))263 [Q.IsPrime] (Φ : CompletedLocalAt (Localization.Away z) Q ≃+*264 CompletedLocalAt A (Q.comap (algebraMap A (Localization.Away z))))265 (hΦ : ∀ a, Φ (completedPointMap _ Q (algebraMap A _ a)) = completedPointMap A _ a) (e : A)266 (g : CompletedLocalAt A (Q.comap (algebraMap A _)))267 (h : ∃ L, ((IsLocalRing.maximalIdeal (Localization.AtPrime (Q.comap (algebraMap A _)))).map268 (localCompletionMap _)) ^ L ≤ finiteLocalCurveIdeal A _ e g 1) :269 ∃ L, ((IsLocalRing.maximalIdeal (Localization.AtPrime Q)).map (localCompletionMap _)) ^ L ≤270 finiteLocalCurveIdeal _ Q (algebraMap A _ e) (Φ.symm g) 1 := by271 refine exists_pow_le_span_pair_transport _ isUnit_one ?_ ?_ h 1272 · rw [mul_one, RingEquiv.symm_apply_eq]; exact (hΦ e).symm273 rw [Ideal.map_symm, ← Ideal.map_le_iff_le_comap, map_maximalIdeal_localCompletion Q,274 ← map_maximalIdeal_localCompletion_transport _ _ Q Φ hΦ]275 exact Ideal.map_mono (Ideal.map_mono (IsLocalization.map_under (.powers z) _ Q).ge)276 277/-- A prime of the chart containing `t` contains the exceptional ideal. -/278private theorem chartExceptional_le (P : Ideal (BlowupChart R t x))279 (hP : chartBase R t x t ∈ P) : chartExceptional R t x ≤ P := by280 unfold chartExceptional281 rw [Ideal.span_le, Set.singleton_subset_iff]; exact hP282 283/-- A curve with nonzero reduction meets the exceptional line in finitely many overlap points. -/284private theorem points_finite [(Ideal.span ({t,x} : Set R)).IsMaximal]285 (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial286 (R ⧸ Ideal.span ({t,x} : Set R)))287 (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =288 Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r))289 (heZ : e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X)290 (F : BlowupChart R t x) (hF : e (Ideal.Quotient.mk (chartExceptional R t x) F) ≠ 0) :291 Finite {Q : Ideal (BlowupOverlap R t x) // Q.IsMaximal ∧292 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) ∈ Q ∧293 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) F ∈ Q} := by294 classical295 let := Ideal.Quotient.field (Ideal.span ({t,x} : Set R))296 set g := e (Ideal.Quotient.mk (chartExceptional R t x) F) with hg297 have key : ∀ Q : {Q : Ideal (BlowupOverlap R t x) // Q.IsMaximal ∧298 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) ∈ Q ∧299 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) F ∈ Q},300 ∃ φ ∈ UniqueFactorizationMonoid.normalizedFactors g,301 ((Q.1.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).map302 (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {φ} := by303 rintro ⟨Q, hQm, hQt, hQF⟩304 have := hQm305 obtain ⟨hPm, -, hPt⟩ := overlap_exceptional_point_comap_maximal R t x Q hQt306 have := hPm307 obtain ⟨ψ, -, hirr, hmap, -, -⟩ := blowup_chart_exceptional_point_polynomial R t x e he heZ308 (Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))) hPt309 have hmem : g ∈ Ideal.span {ψ} := by310 rw [← hmap]311 exact Ideal.mem_map_of_mem _ (Ideal.mem_map_of_mem _ hQF)312 rw [Ideal.mem_span_singleton] at hmem313 obtain ⟨q, hq, hassoc⟩ :=314 UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd hF hirr hmem315 refine ⟨q, hq, ?_⟩316 rw [hmap]317 exact Ideal.span_singleton_eq_span_singleton.mpr hassoc318 choose φ hφ hφeq using key319 refine Finite.of_injective (β := (UniqueFactorizationMonoid.normalizedFactors g).toFinset)320 (fun Q => ⟨φ Q, Multiset.mem_toFinset.mpr (hφ Q)⟩) ?_321 intro Q1 Q2 h12322 have h12' : φ Q1 = φ Q2 := congrArg Subtype.val h12323 have hmaps := (hφeq Q1).trans (h12' ▸ (hφeq Q2).symm)324 rw [← Ideal.comap_symm, ← Ideal.comap_symm] at hmaps325 have hmaps' := Ideal.comap_injective_of_surjective _ e.symm.surjective hmaps326 have ht : ∀ Q : {Q : Ideal (BlowupOverlap R t x) // Q.IsMaximal ∧327 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) ∈ Q ∧328 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) F ∈ Q},329 chartExceptional R t x ≤ Q.1.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) :=330 fun Q => chartExceptional_le t x _ Q.2.2.1331 have hc := quot_ext_eq _ _ _ (ht Q1) (ht Q2) hmaps'332 apply Subtype.ext333 rw [← IsLocalization.map_under (Submonoid.powers (chartSlope R t x)) (BlowupOverlap R t x) Q1.1,334 ← IsLocalization.map_under (Submonoid.powers (chartSlope R t x)) (BlowupOverlap R t x) Q2.1]335 exact congrArg _ hc336 337/-- There is at most one maximal ideal of the chart containing `t`, `x/t` and a given `F`. -/338private theorem zero_points_subsingleton [(Ideal.span ({t,x} : Set R)).IsMaximal]339 (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial340 (R ⧸ Ideal.span ({t,x} : Set R)))341 (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =342 Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r))343 (heZ : e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X)344 (F : BlowupChart R t x) :345 Subsingleton {P : Ideal (BlowupChart R t x) // P.IsMaximal ∧ chartBase R t x t ∈ P ∧346 chartSlope R t x ∈ P ∧ F ∈ P} := by347 constructor348 have key : ∀ P : {P : Ideal (BlowupChart R t x) // P.IsMaximal ∧ chartBase R t x t ∈ P ∧349 chartSlope R t x ∈ P ∧ F ∈ P},350 (P.1.map (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {Polynomial.X} := by351 rintro ⟨P, hPm, hPt, hPZ, -⟩352 have := hPm353 obtain ⟨ψ, -, -, hmap, hZ, -⟩ := blowup_chart_exceptional_point_polynomial R t x e he heZ P hPt354 rw [hmap, hZ.mp hPZ]355 intro P1 P2356 have hmaps := (key P1).trans (key P2).symm357 rw [← Ideal.comap_symm, ← Ideal.comap_symm] at hmaps358 have hmaps' := Ideal.comap_injective_of_surjective _ e.symm.surjective hmaps359 exact Subtype.ext360 (quot_ext_eq _ _ _ (chartExceptional_le t x _ P1.2.2.1)361 (chartExceptional_le t x _ P2.2.2.1) hmaps')362 363section Overlap364variable (beta : BlowupRestriction R t x)365 366/-- If `f = t^d F_A` on the `t`-chart and `f = x^d F_B` on the `x`-chart, then `F_A = Z^d F_B`367on the overlap, where `Z = x/t`. -/368private theorem overlap_relation (d : ℕ) (f : R) (FA : BlowupChart R t x) (FB : BlowupChart R x t)369 (hFA : algebraMap R (BlowupChart R t x) f = (chartBase R t x t) ^ d * FA)370 (hFB : algebraMap R (BlowupChart R x t) f = (chartBase R x t x) ^ d * FB)371 (hreg : Function.Injective (fun y : BlowupOverlap R t x =>372 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) * y)) :373 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) FA =374 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartSlope R t x)) ^ d *375 beta.right FB := by376 apply IsLeftRegular.pow d (show IsLeftRegular _ from hreg)377 have h1 : algebraMap (BlowupChart R t x) (BlowupOverlap R t x)378 (algebraMap R (BlowupChart R t x) f) = beta.right (algebraMap R (BlowupChart R x t) f) := by379 rw [AlgHom.commutes, ← IsScalarTower.algebraMap_apply]380 have hx : beta.right (chartBase R x t x) =381 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) *382 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartSlope R t x) := by383 rw [← map_mul, blowup_chart_relation, chartBase_apply_eq_algebraMap,384 chartBase_apply_eq_algebraMap, AlgHom.commutes, ← IsScalarTower.algebraMap_apply]385 simp only386 rw [hFA, hFB, map_mul, map_mul, map_pow, map_pow, hx] at h1387 rw [h1]; ring388 389variable {beta} in390/-- At a maximal ideal `Q` of the overlap containing `F_A = Z^d F_B`, the transported local391equation of `F_A` generates the same ideal as `F_B` on the `x`-chart, and `F_B ∈ Q`. -/392private theorem right_common_point_span (d : ℕ) (FA : BlowupChart R t x)393 (FB : BlowupChart R x t)394 (hrel : algebraMap (BlowupChart R t x) (BlowupOverlap R t x) FA =395 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartSlope R t x)) ^ d *396 beta.right FB)397 (Q : Ideal (BlowupOverlap R t x)) [hQ : Q.IsMaximal]398 (hQF : algebraMap (BlowupChart R t x) (BlowupOverlap R t x) FA ∈ Q)399 (Ψ : CompletedLocalAt (BlowupOverlap R t x) Q ≃+*400 CompletedLocalAt (BlowupChart R x t) (Q.comap beta.right.toRingHom))401 (hΨ : ∀ b : BlowupChart R x t, Ψ (completedPointMap (BlowupOverlap R t x) Q (beta.right b)) =402 completedPointMap (BlowupChart R x t) (Q.comap beta.right.toRingHom) b) :403 Ideal.span {Ψ (completedPointMap (BlowupOverlap R t x) Q404 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) FA))} =405 Ideal.span {completedPointMap (BlowupChart R x t) (Q.comap beta.right.toRingHom) FB} ∧406 beta.right FB ∈ Q := by407 have hZu : IsUnit ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)408 (chartSlope R t x)) ^ d) := (IsLocalization.Away.algebraMap_isUnit _).pow d409 rw [hrel] at hQF ⊢410 refine ⟨?_, (hQ.isPrime.mem_or_mem hQF).resolve_left411 fun h => hQ.ne_top (Ideal.eq_top_of_isUnit_mem _ h hZu)⟩412 rw [map_mul, map_mul, hΨ]413 exact Ideal.span_singleton_mul_left_unit ((hZu.map _).map Ψ) _414 415variable {beta} in416/-- A maximal ideal of the `x`-chart containing `x` and `F_B` but not the slope `t/x` is the417contraction of a maximal ideal of the overlap containing `t` and `F_A = Z^d F_B`. -/418private theorem right_point_of_overlap (d : ℕ) (FA : BlowupChart R t x) (FB : BlowupChart R x t)419 (hrel : algebraMap (BlowupChart R t x) (BlowupOverlap R t x) FA =420 (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartSlope R t x)) ^ d *421 beta.right FB)422 (P : Ideal (BlowupChart R x t)) [P.IsMaximal] (hPx : chartBase R x t x ∈ P) (hPF : FB ∈ P)423 (hW : chartSlope R x t ∉ P) :424 ∃ Q : Ideal (BlowupOverlap R t x), (Q.IsMaximal ∧425 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) ∈ Q ∧426 algebraMap (BlowupChart R t x) (BlowupOverlap R t x) FA ∈ Q) ∧427 Q.comap beta.right.toRingHom = P := by428 let : Algebra (BlowupChart R x t) (BlowupOverlap R t x) := beta.right.toRingHom.toAlgebra429 have := blowup_overlap_isLocalization_right R t x beta430 obtain ⟨hQm, hQc⟩ := localization_map_maximal (S := BlowupOverlap R t x) (chartSlope R x t) P hW431 have ht : algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) =432 beta.right (chartBase R x t t) := by433 rw [chartBase_apply_eq_algebraMap, chartBase_apply_eq_algebraMap, AlgHom.commutes,434 ← IsScalarTower.algebraMap_apply]435 refine ⟨_, ⟨hQm, ?_, ?_⟩, hQc⟩436 · rw [ht, ← blowup_chart_relation]437 exact Ideal.mem_map_of_mem _ (Ideal.mul_mem_right _ _ hPx)438 · rw [hrel]439 exact Ideal.mul_mem_left _ _ (Ideal.mem_map_of_mem (algebraMap _ _) hPF)440 441end Overlap442 443end General444 445section Concrete446variable (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]447 [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]448 (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ)449 450local notation "RR" => ConcreteSurface O pi u a b451local notation "TT" => surfaceT O pi u a b452local notation "XX" => surfaceX O pi u a b453local notation "AA" =>454 BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)455local notation "BB" =>456 BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)457local notation "CC" =>458 BlowupOverlap (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)459 460section Form461variable (d : ℕ) (c : Fin (d + 1) → ConcreteSurface O pi u a b)462 463/-- The strict transform `F_A = ∑ cᵢ Z^i` of `∑ cᵢ t^(d-i) x^i` on the `t`-chart, `Z = x/t`. -/464private noncomputable abbrev leftForm : AA :=465 ∑ i : Fin (d+1), algebraMap RR AA (c i) * (chartSlope RR TT XX)^i.val466 467/-- The strict transform `F_B = ∑ cᵢ W^(d-i)` of `∑ cᵢ t^(d-i) x^i` on the `x`-chart,468`W = t/x`. -/469private noncomputable abbrev rightForm : BB :=470 ∑ i : Fin (d+1), algebraMap RR BB (c i) * (chartSlope RR XX TT)^(d - i.val)471 472local notation "FA" => leftForm O pi u a b d c473local notation "FB" => rightForm O pi u a b d c474 475/-- The local data of the curve `∑ cᵢ t^(d-i) x^i = 0` on the blow-up: its points on the476exceptional divisor (on the overlap, at `Z = 0` and at infinity), all of them listed, with local477equations `F_A = ∑ cᵢ Z^i` and `F_B = ∑ cᵢ W^(d-i)`. -/478private theorem exists_curve_datum_points (hpi : Irreducible pi) (ha : 0 < a)479 (hne : ∃ i : Fin (d + 1), c i ∉ Ideal.span {TT, XX}) (beta : BlowupRestriction RR TT XX) :480 ∃ D : TwoChartCurveData RR TT XX beta,481 (∀ i, D.g i = completedPointMap CC (D.Q i) (algebraMap AA CC FA) ∧482 algebraMap AA CC FA ∈ D.Q i) ∧483 (∀ Q : Ideal CC, Q.IsMaximal → algebraMap AA CC (chartBase RR TT XX TT) ∈ Q →484 algebraMap AA CC FA ∈ Q → ∃ i, D.Q i = Q) ∧485 (∀ k, D.g0 k = completedPointMap AA (D.P0 k) FA ∧ FA ∈ D.P0 k) ∧486 (∀ P : Ideal AA, P.IsMaximal → chartBase RR TT XX TT ∈ P → chartSlope RR TT XX ∈ P →487 FA ∈ P → ∃ k, D.P0 k = P) ∧488 (∀ l, D.ginf l = completedPointMap BB (D.Pinf l) FB ∧ FB ∈ D.Pinf l) ∧489 ∀ P : Ideal BB, P.IsMaximal → chartBase RR XX TT XX ∈ P → chartSlope RR XX TT ∈ P →490 FB ∈ P → ∃ l, D.Pinf l = P := by491 have : (Ideal.span ({TT, XX} : Set RR)).IsMaximal :=492 concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha493 have : IsNoetherianRing AA := blowupChart_concrete_isNoetherianRing O pi u a b TT XX494 have : IsNoetherianRing BB := blowupChart_concrete_isNoetherianRing O pi u a b XX TT495 obtain ⟨e, he, heZ⟩ := exceptional_line_equiv_chart_exceptional RR TT XX496 have hgne := reduction_ne_zero TT XX e he heZ d c hne497 -- transversality and finiteness at the points of the `t`-chart on the exceptional divisor498 have hL : ∀ (P : Ideal AA) [P.IsMaximal], chartBase RR TT XX TT ∈ P → _ := fun P _ hP =>499 concrete_strict_transform_transverse_finite O pi hpi u a b ha FA500 (fun h => hgne (by rw [h, map_zero])) P hP501 -- common points on the overlap502 let ι := {Q : Ideal CC // Q.IsMaximal ∧503 algebraMap AA CC (chartBase RR TT XX TT) ∈ Q ∧ algebraMap AA CC FA ∈ Q}504 have hιmax : ∀ i : ι, i.1.IsMaximal := fun i => i.2.1505 have hιP (i : ι) := overlap_exceptional_point_comap_maximal RR TT XX i.1 i.2.2.1506 choose Φ hΦ using fun i : ι => completed_point_transport_left RR TT XX i.1507 choose Ψ hΨ using fun i : ι => completed_point_transport_right RR TT XX beta i.1508 have heT (i : ι) : (Φ i).symm (completedPointMap AA _ (chartBase RR TT XX TT)) * 1 =509 completedPointMap CC i.1 (overlapException RR TT XX) := by510 rw [mul_one, RingEquiv.symm_apply_eq]; exact (hΦ i _).symm511 -- points at `Z = 0` and at infinity512 let ι0 := {P : Ideal AA // P.IsMaximal ∧ chartBase RR TT XX TT ∈ P ∧ chartSlope RR TT XX ∈ P ∧513 FA ∈ P}514 have : Subsingleton ι0 := zero_points_subsingleton TT XX e he heZ FA515 have hι0max : ∀ k : ι0, k.1.IsMaximal := fun k => k.2.1516 let ιinf :=517 {P : Ideal BB // P.IsMaximal ∧ chartBase RR XX TT XX ∈ P ∧ chartSlope RR XX TT ∈ P ∧ FB ∈ P}518 have hιinfmax : ∀ l : ιinf, l.1.IsMaximal := fun l => l.2.1519 have hinf (l : ιinf) :=520 concrete_infinity_point_completion O pi hpi u a b ha l.1 l.2.2.1 l.2.2.2.1521 have : Subsingleton ιinf := ⟨fun l1 l2 => Subtype.ext ((hinf l1).1.trans (hinf l2).1.symm)⟩522 have hinf' (l : ιinf) :=523 concrete_infinity_strict_transform_transverse_finite O pi hpi u a b ha d c hne l.1 l.2.2.1524 l.2.2.2.1525 let D : TwoChartCurveData RR TT XX beta :=526 { ι := ι527 fin := points_finite TT XX e he heZ FA hgne528 Q := fun i => i.1529 inj := Subtype.val_injective530 onE := fun i => i.2.2.1531 g := fun i => (Φ i).symm (completedPointMap AA _ FA)532 transverse := fun i =>533 have := (hιP i).1534 mul_injective_quotient_transport _ isUnit_one (heT i) (hL _ (hιP i).2.2).1535 finite := fun i =>536 have := (hιP i).1537 transport_finite _ i.1 (Φ i) (hΦ i) _ _ (hL _ (hιP i).2.2).2.2538 leftIso := Φ539 leftIso_compat := hΦ540 rightIso := Ψ541 rightIso_compat := hΨ542 ι0 := ι0543 fin0 := Finite.of_subsingleton544 P0 := fun k => k.1545 maximal0 := fun k => k.2.1546 inj0 := Subtype.val_injective547 slope0 := fun k => k.2.2.2.1548 onE0 := fun k => k.2.2.1549 g0 := fun k => completedPointMap AA k.1 FA550 transverse0 := fun k => (hL k.1 k.2.2.1).1551 finite0 := fun k => (hL k.1 k.2.2.1).2.2552 ιinf := ιinf553 fininf := Finite.of_subsingleton554 Pinf := fun l => l.1555 maximalinf := fun l => l.2.1556 injinf := Subtype.val_injective557 slopeinf := fun l => l.2.2.2.1558 onEinf := fun l => l.2.2.1559 ginf := fun l => completedPointMap BB l.1 FB560 transverseinf := fun l => (hinf' l).1561 finiteinf := fun l => (hinf' l).2.2 }562 refine ⟨D, fun i => ⟨(Φ i).symm_apply_eq.2 (hΦ i FA).symm, i.2.2.2⟩,563 fun Q hQm hQt hQF => ⟨⟨Q, hQm, hQt, hQF⟩, rfl⟩,564 fun k => ⟨rfl, k.2.2.2.2⟩, fun P hPm hPt hPZ hPF => ⟨⟨P, hPm, hPt, hPZ, hPF⟩, rfl⟩,565 fun l => ⟨rfl, l.2.2.2.2⟩, fun P hPm hPx hPW hPF => ⟨⟨P, hPm, hPx, hPW, hPF⟩, rfl⟩⟩566 567/-- `curve_datum_of_parent_function` in the section notation, with the strict transforms568`F_A`, `F_B` of the form on the two charts. -/569private theorem exists_curve_datum_of_sum (hpi : Irreducible pi) (ha : 0 < a) (f : RR)570 (hc : f = ∑ i : Fin (d + 1), c i * TT ^ (d - i.val) * XX ^ i.val)571 (hne : ∃ i : Fin (d + 1), c i ∉ Ideal.span {TT, XX}) (beta : BlowupRestriction (RR) TT XX) :572 ∃ D : TwoChartCurveData (RR) TT XX beta,573 (∀ s : D.ι ⊕ D.ι0, leftData D s = completedPointMap AA (leftPoint D s) FA ∧574 FA ∈ leftPoint D s) ∧575 (∀ P : Ideal AA, P.IsMaximal → (chartBase (RR) TT XX) TT ∈ P → FA ∈ P →576 ∃ s : D.ι ⊕ D.ι0, leftPoint D s = P) ∧577 (∀ s : D.ι ⊕ D.ιinf, Ideal.span {rightData D s} =578 Ideal.span {completedPointMap BB (rightPoint D s) FB} ∧ FB ∈ rightPoint D s) ∧579 (∀ P : Ideal BB, P.IsMaximal → (chartBase (RR) XX TT) XX ∈ P → FB ∈ P →580 ∃ s : D.ι ⊕ D.ιinf, rightPoint D s = P) ∧581 (∀ s : D.ι ⊕ D.ι0,582 strictTransformAt (RR) TT XX (leftPoint D s) d (Ideal.span {f}) = Ideal.span {leftData D s})583 ∧ ∀ s : D.ι ⊕ D.ιinf,584 strictTransformAt (RR) XX TT (rightPoint D s) d (Ideal.span {f}) =585 Ideal.span {rightData D s} := by586 -- Take the curve datum of `exists_curve_datum_points`; on each chart `f = t^d F_A = x^d F_B`587 -- with `t` (resp. `x`) regular, so the strict transforms are `(F_A)` and `(F_B)`.588 have : (Ideal.span ({TT, XX} : Set RR)).IsMaximal :=589 concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha590 have hFA : algebraMap RR AA f = (chartBase RR TT XX TT)^d * FA := by591 rw [hc]; exact algebraMap_sum_eq_left _ _ d c592 have hFB : algebraMap RR BB f = (chartBase RR XX TT XX)^d * FB := by593 rw [hc]; exact algebraMap_sum_eq_right _ _ d c594 have hrel := overlap_relation TT XX beta d f _ _ hFA hFB595 (nonzerodivisor_survives_localization AA (chartBase RR TT XX TT) (chartSlope RR TT XX)596 (blowup_exceptional_parameter_regular RR TT XX597 (concrete_surface_regular_pair_tx O pi hpi.ne_zero u a b ha)))598 obtain ⟨D, hg, hQ, hg0, hP0, hginf, hPinf⟩ :=599 exists_curve_datum_points O pi u a b d c hpi ha hne beta600 have hleftP : ∀ s : D.ι ⊕ D.ι0,601 (leftPoint D s).IsMaximal ∧ chartBase RR TT XX TT ∈ leftPoint D s := by602 rintro (i | k)603 · obtain ⟨h1, -, h2⟩ := overlap_exceptional_point_comap_maximal RR TT XX (D.Q i) (D.onE i)604 exact ⟨h1, h2⟩605 · exact ⟨D.maximal0 k, D.onE0 k⟩606 have c1 : ∀ s : D.ι ⊕ D.ι0, leftData D s = completedPointMap AA (leftPoint D s) FA ∧607 FA ∈ leftPoint D s := by608 rintro (i | k)609 · exact ⟨(congrArg (D.leftIso i) (hg i).1).trans (D.leftIso_compat i _), (hg i).2⟩610 · exact hg0 k611 have c5 : ∀ s : D.ι ⊕ D.ι0, strictTransformAt RR TT XX (leftPoint D s) d (Ideal.span {f}) =612 Ideal.span {leftData D s} := by613 intro s614 have := (hleftP s).1615 rw [(c1 s).1]616 exact strictTransformAt_span_eq TT XX (leftPoint D s) d f FA hFA617 (concrete_left_point_exceptional_regular O pi hpi u a b ha (leftPoint D s) (hleftP s).2)618 refine ⟨D, c1, ?_, ?_, ?_, c5, ?_⟩619 · intro P hPm hPt hPF620 by_cases hZ : chartSlope RR TT XX ∈ P621 · obtain ⟨k, hk⟩ := hP0 P hPm hPt hZ hPF622 exact ⟨Sum.inr k, hk⟩623 · obtain ⟨hQm, hQc⟩ := localization_map_maximal (S := CC) (chartSlope RR TT XX) P hZ624 obtain ⟨i, hi⟩ := hQ _ hQm (Ideal.mem_map_of_mem _ hPt) (Ideal.mem_map_of_mem _ hPF)625 exact ⟨Sum.inl i, (congrArg (Ideal.comap _) hi).trans hQc⟩626 · rintro (i | l)627 · change Ideal.span {D.rightIso i (D.g i)} = _ ∧ _628 rw [(hg i).1]629 exact right_common_point_span TT XX d _ _ hrel (D.Q i) (hg i).2 _ (D.rightIso_compat i)630 · exact ⟨congrArg (fun y => Ideal.span {y}) (hginf l).1, (hginf l).2⟩631 · intro P hPm hPx hPF632 by_cases hW : chartSlope RR XX TT ∈ P633 · obtain ⟨l, hl⟩ := hPinf P hPm hPx hW hPF634 exact ⟨Sum.inr l, hl⟩635 · obtain ⟨Q, ⟨hQm, hQt, hQF⟩, hQc⟩ := right_point_of_overlap TT XX d _ _ hrel P hPx hPF hW636 obtain ⟨i, rfl⟩ := hQ Q hQm hQt hQF637 exact ⟨Sum.inl i, hQc⟩638 · rintro (i | l)639 · rw [← strict_transform_common_point_transport RR TT XX beta D i d (Ideal.span {f}),640 c5 (Sum.inl i)]641 refine (Ideal.map_span _ _).trans ?_642 rw [Set.image_singleton]643 exact congrArg (fun y => Ideal.span {D.rightIso i y}) ((D.leftIso i).symm_apply_apply _)644 · change _ = Ideal.span {D.ginf l}645 rw [(hginf l).1]646 exact strictTransformAt_span_eq XX TT (D.Pinf l) d f FB hFB647 (concrete_infinity_point_completion O pi hpi u a b ha (D.Pinf l) (D.onEinf l)648 (D.slopeinf l)).2.2.2.2649 650end Form651 652end Concrete653 654/-- A form `f = ∑ cᵢ t^(d-i) x^i` on the concrete surface with some `cᵢ` a unit yields two-chart655curve data: its strict transforms on the two blow-up charts, located at finitely many points of656the exceptional divisor. -/657theorem curve_datum_of_parent_function (O : Type) [CommRing O] [IsDomain O]658 [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]659 [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)660 (a b : ℕ) (ha : 0 < a) (d : ℕ) (f : ConcreteSurface O pi u a b)661 (c : Fin (d + 1) → ConcreteSurface O pi u a b)662 (hc : f = ∑ i : Fin (d + 1),663 c i * (surfaceT O pi u a b) ^ (d - i.val) * (surfaceX O pi u a b) ^ i.val)664 (hne : ∃ i : Fin (d + 1), c i ∉ Ideal.span {(surfaceT O pi u a b), (surfaceX O pi u a b)})665 (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)666 (surfaceX O pi u a b)) :667 ∃ D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b)668 (surfaceX O pi u a b) beta,669 (∀ s : D.ι ⊕ D.ι0,670 leftData D s = completedPointMap671 (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))672 (leftPoint D s)673 (∑ i : Fin (d+1),674 algebraMap (ConcreteSurface O pi u a b)675 (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))676 (c i) * (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b)677 (surfaceX O pi u a b))^i.val) ∧678 (∑ i : Fin (d+1),679 algebraMap (ConcreteSurface O pi u a b)680 (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))681 (c i) * (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b)682 (surfaceX O pi u a b))^i.val) ∈ leftPoint D s) ∧683 (∀ P : Ideal684 (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)),685 P.IsMaximal →686 (chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))687 (surfaceT O pi u a b) ∈ P →688 (∑ i : Fin (d+1),689 algebraMap (ConcreteSurface O pi u a b)690 (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))691 (c i) * (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b)692 (surfaceX O pi u a b))^i.val) ∈ P → ∃ s : D.ι ⊕ D.ι0, leftPoint D s = P) ∧693 (∀ s : D.ι ⊕ D.ιinf,694 Ideal.span {rightData D s} = Ideal.span695 {completedPointMap696 (BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b))697 (rightPoint D s)698 (∑ i : Fin (d+1),699 algebraMap (ConcreteSurface O pi u a b)700 (BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b))701 (c i) * (chartSlope (ConcreteSurface O pi u a b) (surfaceX O pi u a b)702 (surfaceT O pi u a b))^(d - i.val))} ∧703 (∑ i : Fin (d+1),704 algebraMap (ConcreteSurface O pi u a b)705 (BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b))706 (c i) * (chartSlope (ConcreteSurface O pi u a b) (surfaceX O pi u a b)707 (surfaceT O pi u a b))^(d - i.val)) ∈ rightPoint D s) ∧708 (∀ P : Ideal709 (BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)),710 P.IsMaximal →711 (chartBase (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b))712 (surfaceX O pi u a b) ∈ P →713 (∑ i : Fin (d+1),714 algebraMap (ConcreteSurface O pi u a b)715 (BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b))716 (c i) * (chartSlope (ConcreteSurface O pi u a b) (surfaceX O pi u a b)717 (surfaceT O pi u a b))^(d - i.val)) ∈ P → ∃ s : D.ι ⊕ D.ιinf, rightPoint D s = P) ∧718 (∀ s : D.ι ⊕ D.ι0,719 strictTransformAt (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)720 (leftPoint D s) d (Ideal.span {f}) = Ideal.span {leftData D s}) ∧ ∀ s : D.ι ⊕ D.ιinf,721 strictTransformAt (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)722 (rightPoint D s) d (Ideal.span {f}) = Ideal.span {rightData D s} := by723 exact exists_curve_datum_of_sum O pi u a b d c hpi ha f hc hne beta724 725end SurfaceBlowup