Lean sources / SurfaceBlowup / Blowup / FixedTangentCellBijection.lean
Strict transforms give a bijection on a fixed tangent cell
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.DivisorPoints7import SurfaceBlowup.Recursion.Termination8 9/-!10# Strict transforms give a bijection on a fixed tangent cell11 12For a regular local surface with regular parameters `t, x`, the level-one generators of the two13chart kernels of a two-chart curve datum glue (after normalization by a unit) to a global function14`f`. For the concrete surfaces `ConcreteSurface O pi u a b` this shows that the strict transform15map on the fixed tangent cell is injective; combined with the existence of curve data for16prescribed child ideals, it is a bijection onto the product of the child ideal sets.17 18## Main results19 20* `SurfaceBlowup.two_chart_global_function_exists`: a two-chart curve datum on a complete regular21 local surface comes from a global function.22* `SurfaceBlowup.concrete_two_chart_glued_generators_exist`: the same for the concrete surfaces.23* `SurfaceBlowup.strict_transform_injOn_fixed_tangent_cell`: the strict transform map is injective24 on the fixed tangent cell.25* `SurfaceBlowup.strict_transform_bijOn_child_ideals`: it is a bijection onto the product of the26 child ideal sets.27 28## Implementation notes29 30Statements about the concrete surfaces `ConcreteSurface O pi u a b` are written with the local31notations `tChart`, `tExc`, ... for the blow-up charts and their data; see the notation section.32 33Provenance: Lemma 4.2 and Proposition 5.1 of the source paper;34`Thm_SurfaceBlowupV2_{two_chart_level_one_coefficients_left,35two_chart_right_level_one_kernel_polynomial, two_chart_level_one_coefficients_right,36two_chart_level_one_normalization, two_chart_global_function_exists, concrete_two_chart_lemma_4_2,37prop_5_1_injOn, prop_5_1_bijOn}`.38-/39 40namespace SurfaceBlowup41 42open scoped BigOperators ENNReal43 44/-! ### Notation for the concrete surfaces45 46Local notations for the charts of the blow-up of `R = ConcreteSurface O pi u a b` at its47closed point `(t, x)`, taking the surface data as explicit arguments. -/48 49/-- The `t`-chart `R[x/t]` of the blow-up of the concrete surface at `(t, x)`. -/50local notation:max "tChart" O:max pi:max u:max a:max b:max =>51 BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)52 53/-- The structure map `R → R[x/t]`. -/54local notation:max "tBase" O:max pi:max u:max a:max b:max =>55 chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)56 57/-- The slope `x/t` in the `t`-chart. -/58local notation:max "tSlope" O:max pi:max u:max a:max b:max =>59 chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)60 61/-- The exceptional ideal `(t)` of the `t`-chart. -/62local notation:max "tExc" O:max pi:max u:max a:max b:max =>63 chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)64 65/-- The exceptional ideal `(x)` of the `x`-chart. -/66local notation:max "xExc" O:max pi:max u:max a:max b:max =>67 chartExceptional (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)68 69/-- If `e : A ⧸ J ≃ k[X]` (with `k = R ⧸ I` a field) sends constants to constants and `w` to `X`,70and the image of the principal ideal `(F mod J)` is generated by `P`, then `F` is congruent71mod `J` to `∑ cᵢ wⁱ` (`i ≤ deg P`) where `cᵢ mod I = u · P.coeff i` for a nonzero `u`. -/72private theorem exists_coeffs_of_map_span_eq {R A : Type} [CommRing R] [CommRing A] [Algebra R A]73 {I : Ideal R} [I.IsMaximal] {J : Ideal A} {w : A} (e : (A ⧸ J) ≃+* Polynomial (R ⧸ I))74 (he : ∀ r : R, e (Ideal.Quotient.mk J (algebraMap R A r)) =75 Polynomial.C (Ideal.Quotient.mk I r))76 (hw : e (Ideal.Quotient.mk J w) = Polynomial.X) (F : A) (P : Polynomial (R ⧸ I))77 (hker : (Ideal.span {Ideal.Quotient.mk J F}).map e = Ideal.span {P}) :78 ∃ c : Fin (P.natDegree + 1) → R,79 F - ∑ i : Fin (P.natDegree + 1), algebraMap R A (c i) * w ^ i.val ∈ J ∧80 ∃ u : R ⧸ I, u ≠ 0 ∧ ∀ i, Ideal.Quotient.mk I (c i) = P.coeff i * u := by81 let _ : Field (R ⧸ I) := Ideal.Quotient.field _82 rw [Ideal.map_span, Set.image_singleton, Ideal.span_singleton_eq_span_singleton] at hker83 obtain ⟨v, hv⟩ := hker84 obtain ⟨c, hc, hcv⟩ := Polynomial.isUnit_iff.mp v.isUnit85 choose a ha using fun i : Fin (P.natDegree + 1) =>86 Ideal.Quotient.mk_surjective (I := I) (P.coeff i.val * c⁻¹)87 refine ⟨a, ?_, c⁻¹, inv_ne_zero hc.ne_zero, ha⟩88 rw [← Ideal.Quotient.eq]89 apply e.injective90 have heF : e (Ideal.Quotient.mk J F) = P * Polynomial.C c⁻¹ := by91 rw [← hv, ← hcv, mul_assoc, ← Polynomial.C_mul, mul_inv_cancel₀ hc.ne_zero, Polynomial.C_1,92 mul_one]93 simp only [heF, map_sum, map_mul, map_pow, hw, he, ha]94 conv_lhs => rw [P.as_sum_range_C_mul_X_pow]95 rw [Finset.sum_mul, Fin.sum_univ_eq_sum_range96 (fun i => Polynomial.C (P.coeff i) * Polynomial.C c⁻¹ * Polynomial.X ^ i)]97 exact Finset.sum_congr rfl fun i _ => by ring98 99/-- Level-one coefficients in the left chart: the generator `FA` of the level-one left kernel is100congruent mod the exceptional ideal to `∑ cA i · slope^i`, whose first `r` coefficients lie in101`(t, x)`, with `r` the multiplicity at the points over `x/t = 0` and `m` the weighted degree. -/102private theorem two_chart_level_one_coefficients_left (R : Type) [CommRing R] (t x : R)103 (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)104 [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]105 (FA : BlowupChart R t x) (hFA : leftLevelKernel D 1 =106 Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R t x t})^1) FA}) :107 ∃ (m r : ℕ) (cA : Fin (m+1) → R), FA - ∑ i : Fin (m+1), algebraMap R (BlowupChart R t x) (cA i)108 * (chartSlope R t x)^i.val ∈ chartExceptional R t x ∧109 (∀ i : Fin (m+1), i.val < r → cA i ∈ Ideal.span {t,x}) ∧110 (∀ i : Fin (m+1), i.val = r → cA i ∉ Ideal.span {t,x}) ∧ r ≤ m ∧ r = ∑ᶠ k : D.ι0,111 leftMultiplicity D (Sum.inr k) ∧ m = ∑ᶠ s : D.ι ⊕ D.ι0, leftResidueDegree D s *112 leftMultiplicity D s := by113 classical114 let _ : Field (R ⧸ Ideal.span ({t,x} : Set R)) := Ideal.Quotient.field _115 have : Fintype D.ι := @Fintype.ofFinite _ D.fin116 have : Fintype D.ι0 := @Fintype.ofFinite _ D.fin0117 obtain ⟨e, he, heZ⟩ := exceptional_line_equiv_chart_exceptional R t x118 obtain ⟨φ, hφ, -, hne, hX, hdeg, -, hker⟩ :=119 two_chart_left_level_one_kernel_polynomial R t x beta D e he heZ120 have gen : ∀ J : Ideal (BlowupChart R t x), J = chartExceptional R t x →121 (leftKernel D 1).map (Ideal.Quotient.mk J) = Ideal.span {Ideal.Quotient.mk J FA} →122 (leftKernel D 1).map (Ideal.Quotient.mk (chartExceptional R t x)) =123 Ideal.span {Ideal.Quotient.mk (chartExceptional R t x) FA} := by124 rintro J rfl h; exact h125 set Pol := ∏ᶠ s, φ s ^ leftMultiplicity D s with hPol126 set r := ∑ᶠ k : D.ι0, leftMultiplicity D (Sum.inr k) with hr127 set Q := ∏ i : D.ι, φ (Sum.inl i) ^ leftMultiplicity D (Sum.inl i) with hQ128 rw [gen _ (pow_one _) hFA] at hker129 obtain ⟨cA, hgA, u, hu, hcA⟩ := exists_coeffs_of_map_span_eq e he heZ FA _ hker130 have hPolXQ : Pol = Polynomial.X ^ r * Q := by131 rw [hPol, finprod_eq_prod_of_fintype, Fintype.prod_sum_type, hr, finsum_eq_sum_of_fintype,132 mul_comm]133 congr 1134 simp only [hX]135 exact Finset.prod_pow_eq_pow_sum _ _ _136 have hQ0 : Q.coeff 0 ≠ 0 := by137 rw [Polynomial.coeff_zero_eq_eval_zero, hQ, Polynomial.eval_prod]138 refine Finset.prod_ne_zero_iff.mpr fun i _ => ?_139 rw [Polynomial.eval_pow]140 refine pow_ne_zero _ fun h0 => ?_141 rw [← Polynomial.coeff_zero_eq_eval_zero, ← Polynomial.X_dvd_iff] at h0142 obtain ⟨g, hg⟩ := h0143 obtain ⟨hmon, hirr⟩ := hφ (Sum.inl i)144 rcases hirr.isUnit_or_isUnit hg with h | h145 · exact Polynomial.not_isUnit_X h146 · rw [(Polynomial.monic_X.of_mul_monic_left (hg ▸ hmon)).isUnit_iff] at h147 exact hne i (by rw [hg, h, mul_one])148 have hrP : Pol.coeff r ≠ 0 := by149 rw [hPolXQ, Polynomial.coeff_X_pow_mul']; simpa using hQ0150 refine ⟨Pol.natDegree, r, cA, hgA, fun i hi => ?_, fun i hi => ?_,151 Polynomial.le_natDegree_of_ne_zero hrP, hr, ?_⟩152 · have hlow : ∀ j, j < r → Pol.coeff j = 0 := fun j hj => by153 rw [hPolXQ, Polynomial.coeff_X_pow_mul']; simp [Nat.not_le.mpr hj]154 rw [← Ideal.Quotient.eq_zero_iff_mem, hcA, hlow _ hi, zero_mul]155 · rw [← Ideal.Quotient.eq_zero_iff_mem, hcA, hi]156 exact mul_ne_zero hrP hu157 · rw [hPol, finprod_eq_prod_of_fintype, finsum_eq_sum_of_fintype,158 Polynomial.natDegree_prod_of_monic _ _ fun s _ => (hφ s).1.pow _]159 refine Finset.sum_congr rfl fun s _ => ?_160 rw [(hφ s).1.natDegree_pow, hdeg, mul_comm]161 162/-- The level-one right kernel, transported to `k[X]` along an identification of the right163exceptional line, is generated by `∏ ψₛ ^ multₛ` for distinct monic irreducibles `ψₛ`, with164`ψ = X` exactly at the points at infinity. -/165private theorem two_chart_right_level_one_kernel_polynomial (R : Type) [CommRing R] (t x : R)166 (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)167 [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R x t)]168 (eB : (BlowupChart R x t ⧸ chartExceptional R x t) ≃+*169 Polynomial (R ⧸ Ideal.span ({t,x} : Set R)))170 (heB : ∀ r : R, eB (Ideal.Quotient.mk (chartExceptional R x t) (chartBase R x t r)) =171 Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r))172 (heW : eB (Ideal.Quotient.mk (chartExceptional R x t) (chartSlope R x t)) = Polynomial.X) :173 ∃ ψ : D.ι ⊕ D.ιinf → Polynomial (R ⧸ Ideal.span ({t,x} : Set R)),174 (∀ s, (ψ s).Monic ∧ Irreducible (ψ s)) ∧ Function.Injective ψ ∧175 (∀ i, ψ (Sum.inl i) ≠ Polynomial.X) ∧ (∀ l, ψ (Sum.inr l) = Polynomial.X) ∧176 (∀ s, (ψ s).natDegree = rightResidueDegree D s) ∧ (∀ l, rightResidueDegree D (Sum.inr l) =177 1) ∧ ((rightKernel D 1).map (Ideal.Quotient.mk (chartExceptional R x t))).map eB =178 Ideal.span {∏ᶠ s, ψ s ^ rightMultiplicity D s} := by179 obtain ⟨hmax, hinjP, htP⟩ := two_chart_right_points_maximal R t x beta D180 obtain ⟨ψ, m, hψ, hinj, hslope, hlen, hm, hker⟩ := level_one_kernel_polynomial R x t _181 Ideal.span_pair_comm eB heB heW (rightPoint D) hinjP htP (rightData D)182 (two_chart_right_data_transverse_finite R t x beta D 1).2183 have hmult : rightMultiplicity D = m := funext fun s => by184 unfold rightMultiplicity rightLevelIdeal; rw [hm s]; rfl185 have hdeg : ∀ s, (ψ s).natDegree = rightResidueDegree D s := by186 intro s; unfold rightResidueDegree; rw [hlen s]; rfl187 have hX : ∀ l, ψ (Sum.inr l) = Polynomial.X := fun l => (hslope (Sum.inr l)).1 (D.slopeinf l)188 refine ⟨ψ, hψ, hinj, fun i hi => ?_, hX, hdeg, fun l => ?_, by rw [hmult]; exact hker⟩189 · have hQ := D.onE i190 have := D.maximal i191 exact (overlap_exceptional_point_comap_maximal_right R t x beta (D.Q i) hQ).2.1192 ((hslope (Sum.inl i)).2 hi)193 · rw [← hdeg, hX]; exact Polynomial.natDegree_X194 195/-- The exceptional line `R[t/x] ⧸ (x)` of the right chart is the affine line over196`R ⧸ (t, x)`, with coordinate the slope `t/x`. -/197private theorem exceptional_line_equiv_chart_exceptional_swap (R : Type) [CommRing R] (t x : R) :198 ∃ e : (BlowupChart R x t ⧸ chartExceptional R x t) ≃+*199 Polynomial (R ⧸ Ideal.span ({t,x} : Set R)),200 (∀ r : R, e (Ideal.Quotient.mk (chartExceptional R x t) (chartBase R x t r)) =201 Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r)) ∧202 e (Ideal.Quotient.mk (chartExceptional R x t) (chartSlope R x t)) = Polynomial.X := by203 have h := exceptional_line_equiv_chart_exceptional R x t204 rwa [Set.pair_comm x t] at h205 206/-- Level-one coefficients in the right chart: the generator `FB` of the level-one right kernel207is congruent mod the exceptional ideal to `∑ cB i · slope^i` with leading coefficient a unit and208`n` the weighted degree. -/209private theorem two_chart_level_one_coefficients_right (R : Type) [CommRing R] (t x : R)210 (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)211 [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R x t)]212 (FB : BlowupChart R x t) (hFB : rightLevelKernel D 1 =213 Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R x t x})^1) FB}) :214 ∃ (n : ℕ) (cB : Fin (n+1) → R), FB - ∑ i : Fin (n+1), algebraMap R (BlowupChart R x t) (cB i) *215 (chartSlope R x t)^i.val ∈ chartExceptional R x t ∧ cB (Fin.last n) ∉ Ideal.span {t,x} ∧ n =216 ∑ᶠ s : D.ι ⊕ D.ιinf, rightResidueDegree D s * rightMultiplicity D s := by217 classical218 let _ : Field (R ⧸ Ideal.span ({t,x} : Set R)) := Ideal.Quotient.field _219 have : Fintype D.ι := @Fintype.ofFinite _ D.fin220 have : Fintype D.ιinf := @Fintype.ofFinite _ D.fininf221 obtain ⟨e, he', heW⟩ := exceptional_line_equiv_chart_exceptional_swap R t x222 obtain ⟨φ, hφ, -, -, -, hdeg, -, hker⟩ :=223 two_chart_right_level_one_kernel_polynomial R t x beta D e he' heW224 have gen : ∀ J : Ideal (BlowupChart R x t), J = chartExceptional R x t →225 (rightKernel D 1).map (Ideal.Quotient.mk J) = Ideal.span {Ideal.Quotient.mk J FB} →226 (rightKernel D 1).map (Ideal.Quotient.mk (chartExceptional R x t)) =227 Ideal.span {Ideal.Quotient.mk (chartExceptional R x t) FB} := by228 rintro J rfl h; exact h229 set Pol := ∏ᶠ s, φ s ^ rightMultiplicity D s with hPol230 rw [gen _ (pow_one _) hFB] at hker231 obtain ⟨cB, hgB, u, hu, hcB⟩ := exists_coeffs_of_map_span_eq e he' heW FB _ hker232 have hPm : Pol.Monic := by233 rw [hPol, finprod_eq_prod_of_fintype]234 exact Polynomial.monic_prod_of_monic _ _ fun s _ => (hφ s).1.pow _235 refine ⟨Pol.natDegree, cB, hgB, ?_, ?_⟩236 · rw [← Ideal.Quotient.eq_zero_iff_mem, hcB, Fin.val_last, show Pol.coeff _ = 1 from hPm, one_mul]237 exact hu238 · rw [hPol, finprod_eq_prod_of_fintype, finsum_eq_sum_of_fintype,239 Polynomial.natDegree_prod_of_monic _ _ fun s _ => (hφ s).1.pow _]240 refine Finset.sum_congr rfl fun s _ => ?_241 rw [(hφ s).1.natDegree_pow, hdeg, mul_comm]242 243/-- Level-one normalization: the two level-one generators agree on the overlap up to a unit244`u` of `R` and the factor `slope^deg D`, modulo the overlap exceptional ideal. -/245private theorem two_chart_level_one_normalization (R : Type) [CommRing R] (t x : R)246 (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)247 [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsLocalRing R] [IsNoetherianRing (BlowupChart R t x)]248 [IsNoetherianRing (BlowupChart R x t)] (hreg : RegularParameterPair R t x)249 (hregSwap : RegularParameterPair R x t) (FA : ℕ → BlowupChart R t x)250 (hFA : ∀ j : ℕ, leftLevelKernel D j =251 Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R t x t})^j) (FA j)})252 (FB : ℕ → BlowupChart R x t) (hFB : ∀ j : ℕ, rightLevelKernel D j =253 Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R x t x})^j) (FB j)}) :254 ∃ u : Rˣ, (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (FA 1) - algebraMap255 R (BlowupOverlap R t x) (u : R) * ((overlapSlope R t x)^(curveDataDegree D) *256 beta.right (FB 1)) ∈ (Ideal.span {overlapException R t x}) := by257 have hpow : (Ideal.span {overlapException R t x})^1 = Ideal.span {overlapException R t x} :=258 pow_one _259 have hoverlap :260 Ideal.span {Ideal.Quotient.mk (Ideal.span {overlapException R t x})261 ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (FA 1))} =262 Ideal.span {Ideal.Quotient.mk (Ideal.span {overlapException R t x}) (beta.right (FB 1))} := by263 have := congrArg (Ideal.map (Ideal.quotEquivOfEq hpow).toRingHom)264 (two_chart_level_generators_agree_on_overlap R t x beta D FA hFA FB hFB 1)265 rwa [Ideal.map_span, Ideal.map_span, Set.image_singleton, Set.image_singleton] at this266 obtain ⟨hmaxR, -, hPe⟩ := two_chart_right_points_maximal R t x beta D267 have : ∀ s, (rightPoint D s).IsMaximal := hmaxR268 choose L hL using (two_chart_right_data_transverse_finite R t x beta D 1).2269 have hreg1 := overlap_level_generator_regular R t x hreg hregSwap beta (D.ι ⊕ D.ιinf)270 (rightPoint D) hPe (rightData D) L hL FB hFB 1271 have hregB : Function.Injective272 (fun c : BlowupOverlap R t x ⧸ (Ideal.span {overlapException R t x}) =>273 Ideal.Quotient.mk (Ideal.span {overlapException R t x}) (beta.right (FB 1)) * c) := by274 intro a b hab275 apply (Ideal.quotEquivOfEq hpow).symm.injective276 apply hreg1277 have key : ∀ y : BlowupOverlap R t x,278 Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^1) y =279 (Ideal.quotEquivOfEq hpow).symm (Ideal.Quotient.mk _ y) := fun _ ↦ rfl280 simp only [key, ← map_mul]281 exact congrArg _ hab282 obtain ⟨m, r, cA, hgA, hlow, hr, hrm, hrdef, hmdef⟩ :=283 two_chart_level_one_coefficients_left R t x beta D (FA 1) (hFA 1)284 obtain ⟨n, cB, hgB, htop, hndef⟩ :=285 two_chart_level_one_coefficients_right R t x beta D (FB 1) (hFB 1)286 have hdeg : r + n = curveDataDegree D := by287 obtain ⟨e, he, heZ⟩ := exceptional_line_equiv_chart_exceptional R t x288 obtain ⟨eB, heB, heW⟩ := exceptional_line_equiv_chart_exceptional_swap R t x289 obtain ⟨_, -, -, -, -, -, h0, -⟩ :=290 two_chart_left_level_one_kernel_polynomial R t x beta D e he heZ291 obtain ⟨_, -, -, -, -, -, hinf, -⟩ :=292 two_chart_right_level_one_kernel_polynomial R t x beta D eB heB heW293 have hδ : ∀ i, leftResidueDegree D (Sum.inl i) = rightResidueDegree D (Sum.inl i) := fun i ↦294 congrArg ENat.toNat (overlap_point_residue_field_equiv R t x beta (D.Q i) (D.onE i)).2.2295 have hμ : ∀ i, leftMultiplicity D (Sum.inl i) = rightMultiplicity D (Sum.inl i) := fun i ↦296 (two_chart_common_multiplicity_eq R t x beta D i).1.trans297 (two_chart_common_multiplicity_eq R t x beta D i).2.symm298 have := Fintype.ofFinite D.ι299 have := Fintype.ofFinite D.ι0300 have := Fintype.ofFinite D.ιinf301 unfold curveDataDegree302 rw [hrdef, hndef]303 simp only [finsum_eq_sum_of_fintype, Fintype.sum_sum_type, h0, hinf, hδ, hμ, one_mul]304 ring305 exact glued_level_one_normalization R t x hreg beta _ (FA 1) (FB 1) hoverlap hregB m n cA cB hgA306 hgB r hlow hr hrm htop hdeg307 308/-- A two-chart curve datum on a complete regular local surface comes309from a global function `f` whose glued level generators cut out the left and right level kernels. -/310theorem two_chart_global_function_exists (R : Type) [CommRing R] (t x : R) (beta : BlowupRestrictionLemma 4.3311 R t x) (D : TwoChartCurveData R t x beta) [(Ideal.span ({t,x} : Set R)).IsMaximal]312 [IsLocalRing R] [IsNoetherianRing (BlowupChart R t x)] [IsNoetherianRing (BlowupChart R x t)]313 [IsAdicComplete (Ideal.span {t,x}) R] (hreg : RegularParameterPair R t x)314 (hregSwap : RegularParameterPair R x t) :315 ∃ f : R, ∃ G : GluedGenerators R t x beta (curveDataDegree D),316 (∀ j : ℕ, surfaceToCechInput R t x j f = (cechInputLattice R t x j).mkQ (gluedFunctionPair R317 t x G j)) ∧ ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)}318 = leftLevelKernel D j ∧319 Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)} = rightLevelKernel D320 j := by321 obtain ⟨⟨FA, hFA⟩, ⟨FB, hFB⟩⟩ := two_chart_level_generators_exist R t x beta D322 exact global_function_of_two_chart_curve_data R t x beta D hreg hregSwap323 (curveDataDegree D) FA hFA FB hFB324 (two_chart_level_one_normalization R t x beta D hreg hregSwap FA hFA FB hFB)325 326/-- A two-chart curve datum on a concrete surface `ConcreteSurface O pi u a b` comes from a global327function `f` whose glued level generators cut out the left and right level kernels. -/328theorem concrete_two_chart_glued_generators_exist (O : Type) [CommRing O] [IsDomain O]Lemma 4.3329 [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]330 [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)331 (a b : ℕ) (ha : 0 < a) (beta : BlowupRestriction (ConcreteSurface O pi u a b)332 (surfaceT O pi u a b) (surfaceX O pi u a b))333 (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)334 beta) :335 ∃ f : ConcreteSurface O pi u a b, ∃ G : GluedGenerators (ConcreteSurface O pi u a b)336 (surfaceT O pi u a b) (surfaceX O pi u a b) beta (curveDataDegree D),337 (∀ j : ℕ, surfaceToCechInput (ConcreteSurface O pi u a b) (surfaceT O pi u a b)338 (surfaceX O pi u a b) j f =339 (cechInputLattice (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)340 j).mkQ (gluedFunctionPair (ConcreteSurface O pi u a b) (surfaceT O pi u a b)341 (surfaceX O pi u a b) G j)) ∧342 ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk (tExc O pi u a b^j) (G.left j)} = leftLevelKernel D j ∧343 Ideal.span {Ideal.Quotient.mk (xExc O pi u a b^j) (G.right j)} = rightLevelKernel D j := by344 have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set345 (ConcreteSurface O pi u a b))).IsMaximal :=346 concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha347 have := concrete_surface_isLocalRing O pi u a b hpi.not_isUnit ha348 have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)349 (surfaceX O pi u a b)350 have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)351 (surfaceT O pi u a b)352 have : IsAdicComplete (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set353 (ConcreteSurface O pi u a b))) (ConcreteSurface O pi u a b) :=354 concrete_surface_isAdicComplete_parameterIdeal O pi u a b355 exact two_chart_global_function_exists _ _ _ beta D356 (concrete_surface_regular_pair_tx O pi hpi.ne_zero u a b ha)357 (concrete_surface_regular_pair_xt O pi hpi.ne_zero u a b ha)358 359/-- On the fixed tangent cell, an ideal is determined by its360strict transforms at the points of the exceptional divisor `Dv`. -/361theorem strict_transform_injOn_fixed_tangent_cell (O : Type) [CommRing O] [IsDomain O]Proposition 4.4362 [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]363 [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)364 (a b : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a b)]365 [IsRegularLocalRing (ConcreteSurface O pi u a b)] (S : SurfaceData O366 (ConcreteSurface O pi u a b))367 (hS : S.t = surfaceT O pi u a b ∧ S.x = surfaceX O pi u a b ∧ S.a = a ∧ S.b = b)368 (e : (tChart O pi u a b ⧸ tExc O pi u a b) ≃+* Polynomial (IsLocalRing.ResidueField369 (ConcreteSurface O pi u a b)))370 (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)371 (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))372 (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)373 (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))374 (hinf : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)375 (surfaceX O pi u a b)).IsPrime) (s : State) (d : ℕ)376 (hdeg : exceptionalDegree (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) Dv = d) :377 Set.InjOn (fun J Q => divisorStrictTransform (ConcreteSurface O pi u a b) (surfaceT O pi u a b)378 (surfaceX O pi u a b) e Dv hinf d J Q)379 (fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv) := by380 intro J₁ h₁ J₂ h₂ hJ381 obtain ⟨beta⟩ := actual_blowup_restriction_exists (ConcreteSurface O pi u a b)382 (surfaceT O pi u a b) (surfaceX O pi u a b)383 obtain ⟨f₁, c, D, hJ₁, -, -, -, hst₁, hst₁r, hm, hdegD⟩ :=384 fixed_tangent_cell_curve_datum O pi hpi u a b ha S ⟨hS.1, hS.2.1⟩ e he heZ Dv s d J₁ h₁ beta385 obtain ⟨hst₂, hst₂r⟩ := cell_strict_transforms_agree_at_datum_points O pi hpi u a b ha S hS e he386 heZ Dv hinf s d J₁ J₂ h₁ h₂ (congrFun hJ) beta D hm hst₁ hst₁r387 obtain ⟨f, G, hf, hG⟩ := concrete_two_chart_glued_generators_exist O pi hpi u a b ha beta D388 have hdD : curveDataDegree D = d := hdegD.trans hdeg389 have hmax : IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b) = Ideal.span390 {surfaceT O pi u a b, surfaceX O pi u a b} := by391 rw [← S.parameters, hS.1, hS.2.1]392 have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set393 (ConcreteSurface O pi u a b))).IsMaximal := hmax ▸ IsLocalRing.maximalIdeal.isMaximal _394 have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)395 (surfaceX O pi u a b)396 have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)397 (surfaceT O pi u a b)398 have hreg := concrete_surface_regular_pair_tx O pi hpi.ne_zero u a b ha399 have hregSwap := concrete_surface_regular_pair_xt O pi hpi.ne_zero u a b ha400 obtain ⟨hinst1, hinst2, -⟩ := two_chart_datum_concrete_instances O pi hpi u a b ha beta D401 have hL := fun s ↦ (hinst1 s).2402 have hR := fun s ↦ (hinst2 s).2403 have hregS : RegularParameterPair (ConcreteSurface O pi u a b) S.t S.x := by404 rw [hS.1, hS.2.1]; exact hreg405 -- an ideal of the cell with the strict transforms of `D` is `(f)`406 have key : ∀ J ∈ fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv,407 (∀ s, strictTransformAt (ConcreteSurface O pi u a b) (surfaceT O pi u a b)408 (surfaceX O pi u a b) (leftPoint D s) d J = Ideal.span {leftData D s}) →409 (∀ s, strictTransformAt (ConcreteSurface O pi u a b) (surfaceX O pi u a b)410 (surfaceT O pi u a b) (rightPoint D s) d J = Ideal.span {rightData D s}) →411 J = Ideal.span {f} := by412 rintro J ⟨⟨⟨g, rfl⟩, -⟩, hJc⟩ hl hr413 have hmul := has_tangent_divisor_multiplicity O (ConcreteSurface O pi u a b) S hregS _ d Dv hJc414 rw [HasMultiplicity, hmax] at hmul415 subst hdD416 exact parent_ideal_unique_of_level_lattice (ConcreteSurface O pi u a b) (surfaceT O pi u a b)417 (surfaceX O pi u a b) hreg hregSwap beta _ G418 (two_chart_left_generators_regular_on_overlap (ConcreteSurface O pi u a b)419 (surfaceT O pi u a b) (surfaceX O pi u a b) beta D _ G hG hreg hregSwap) f hf g420 (strict_transforms_give_level_lattice_membership (ConcreteSurface O pi u a b)421 (surfaceT O pi u a b) (surfaceX O pi u a b) beta D _ G hG g422 ((Ideal.span_singleton_le_iff_mem _).1 hmul.1) hl hr)423 fun h ↦ hmul.2 ((Ideal.span_singleton_le_iff_mem _).2 h)424 exact (key J₁ h₁ hst₁ hst₁r).trans (key J₂ h₂ hst₂ hst₂r).symm425 426/-- The strict transform map is a bijection from the fixed tangent cell onto the427product of the child ideal sets over the support of `Dv`. -/428theorem strict_transform_bijOn_child_ideals (O : Type) [CommRing O] [IsDomain O]Proposition 4.4429 [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]430 [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)431 (a b : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a b)]432 [IsRegularLocalRing (ConcreteSurface O pi u a b)] (S : SurfaceData O433 (ConcreteSurface O pi u a b))434 (hS : S.t = surfaceT O pi u a b ∧ S.x = surfaceX O pi u a b ∧ S.a = a ∧ S.b = b)435 (e : (tChart O pi u a b ⧸ tExc O pi u a b) ≃+* Polynomial (IsLocalRing.ResidueField436 (ConcreteSurface O pi u a b)))437 (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)438 (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))439 (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)440 (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))441 (hinf : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)442 (surfaceX O pi u a b)).IsPrime) (s : State) (d : ℕ) (hd : 0 < d)443 (hs : (∃ c : ℕ, s = State.single a c ∧ b = 0) ∨ (∃ c h : ℕ, s = State.crossing a b c h ∧ 0 < b))444 (hdc : d ≤ stateContactT s) (hdh : ∀ h : ℕ, stateContactX s = some h → d ≤ h)445 (hDinf : 0 < Dv none ↔ d < stateContactT s)446 (hDzero : ∀ h : ℕ, stateContactX s = some h →447 (0 < Dv (zeroDirection (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) ↔ d < h))448 (hdeg : exceptionalDegree (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) Dv = d) :449 Set.BijOn (fun J Q => divisorStrictTransform (ConcreteSurface O pi u a b) (surfaceT O pi u a b)450 (surfaceX O pi u a b) e Dv hinf d J Q)451 (fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv)452 (Set.pi Set.univ (childIdealSet (ConcreteSurface O pi u a b) (surfaceT O pi u a b)453 (surfaceX O pi u a b) e Dv hinf s d)) := by454 refine ⟨strict_transform_mapsTo_child_ideals O pi hpi u a b ha S hS e he heZ Dv hinf s d,455 strict_transform_injOn_fixed_tangent_cell O pi hpi u a b ha S hS e he heZ Dv hinf s d hdeg,456 fun I hI ↦ ?_⟩457 rw [Set.mem_univ_pi] at hI458 obtain ⟨beta⟩ := actual_blowup_restriction_exists (ConcreteSurface O pi u a b)459 (surfaceT O pi u a b) (surfaceX O pi u a b)460 obtain ⟨D, hm, hcl⟩ := child_ideals_curve_datum O pi hpi u a b ha e he heZ Dv hinf s d beta I hI461 obtain ⟨ht, hx, ha', hb'⟩ := hS462 rcases S with ⟨p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15⟩463 dsimp only at ht hx ha' hb'464 subst ht hx465 have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)466 (surfaceX O pi u a b)467 have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)468 (surfaceT O pi u a b)469 have hdD : curveDataDegree D = d := hdeg ▸ (matches_divisor_degree O (ConcreteSurface O pi u a b)470 ⟨p1, p2, surfaceT O pi u a b, surfaceX O pi u a b, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14,471 p15⟩ beta D Dv e he heZ hm).symm472 obtain ⟨f, G, hf, hG⟩ := concrete_two_chart_glued_generators_exist O pi hpi u a b ha beta D473 obtain ⟨h1, h2⟩ := concrete_strict_transforms_are_prescribed O pi hpi u a b ha beta D f G hf hG474 rw [hdD] at h1 h2475 have hIf := hcl f h1 h2476 subst hdD477 exact ⟨_, global_function_mem_cell O pi hpi u a b ha _ ⟨rfl, rfl, ha', hb'⟩ e he heZ Dv hinf s _478 hd hs hdc hdh hDinf hDzero beta D hm rfl f G hf hG I hI hIf, funext hIf⟩479 480end SurfaceBlowup