Exceptional divisor points of two-chart curve data

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.Surfaces.ConcreteAtlas8 9/-!10# Exceptional divisor points of two-chart curve data11 12For the blow-up of a regular local surface at its closed point, this file relates two-chart curve13data (finitely many points of the two charts with local curve generators) to divisors on the14exceptional line `ℙ¹_k`. It computes level-one kernels as products of powers of irreducible15polynomials, shows that a curve datum matching a divisor `Dv` has degree `deg Dv`, constructs curve16data realizing prescribed child ideals, and proves that the glued global function lies in the fixed17tangent cell.18 19## Main results20 21* `SurfaceBlowup.level_one_kernel_polynomial`: the level-one kernel on a blow-up chart maps to the22  ideal of `k[X]` generated by a product of powers of distinct monic irreducibles;23  `SurfaceBlowup.two_chart_left_level_one_kernel_polynomial` specialises it to the left chart.24* `SurfaceBlowup.child_ideals_curve_datum`: prescribed child ideals are realized by a curve datum.25* `SurfaceBlowup.fixed_tangent_cell_curve_datum`: every ideal of the fixed tangent cell comes from26  a curve datum matching `Dv`.27* `SurfaceBlowup.matches_divisor_degree`: a curve datum matching `Dv` has degree `deg Dv`.28* `SurfaceBlowup.matches_divisor_level_one_polynomial`: its level-one left kernel is generated by29  the affine polynomial of `Dv`.30* `SurfaceBlowup.global_function_has_tangent_divisor`, `SurfaceBlowup.global_function_mem_cell`:31  the glued global function has tangent divisor `Dv` and lies in the fixed tangent cell.32 33## Implementation notes34 35Statements about the concrete surfaces `ConcreteSurface O pi u a b` are written with the local36notations `tChart`, `tExc`, ... for the blow-up charts and their data; see the notation section.37 38Provenance: `Thm_SurfaceBlowupV2_{boundary_contact_of_twisted_generator,39contracted_level_one_ideal_is_irreducible_power, two_chart_common_multiplicity_eq,40child_ideals_curve_datum, curve_datum_common_and_zero_clauses, curve_datum_matches_divisor,41matches_divisor_degree, fixed_tangent_cell_curve_datum, two_chart_left_level_one_kernel_polynomial,42matches_divisor_level_one_polynomial, global_function_has_tangent_divisor,43global_function_mem_cell}`.44-/45 46namespace SurfaceBlowup47 48open scoped BigOperators ENNReal49 50/-! ### Notation for the concrete surfaces51 52Local notations for the charts of the blow-up of `R = ConcreteSurface O pi u a b` at its53closed point `(t, x)`, taking the surface data as explicit arguments. -/54 55/-- The `t`-chart `R[x/t]` of the blow-up of the concrete surface at `(t, x)`. -/56local notation:max "tChart" O:max pi:max u:max a:max b:max =>57  BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)58 59/-- The structure map `R → R[x/t]`. -/60local notation:max "tBase" O:max pi:max u:max a:max b:max =>61  chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)62 63/-- The slope `x/t` in the `t`-chart. -/64local notation:max "tSlope" O:max pi:max u:max a:max b:max =>65  chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)66 67/-- The exceptional ideal `(t)` of the `t`-chart. -/68local notation:max "tExc" O:max pi:max u:max a:max b:max =>69  chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)70 71/-- The overlap of the two charts. -/72local notation:max "tOverlap" O:max pi:max u:max a:max b:max =>73  BlowupOverlap (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)74 75/-- The `x`-chart `R[t/x]` of the blow-up of the concrete surface at `(t, x)`. -/76local notation:max "xChart" O:max pi:max u:max a:max b:max =>77  BlowupChart (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)78 79/-- The structure map `R → R[t/x]`. -/80local notation:max "xBase" O:max pi:max u:max a:max b:max =>81  chartBase (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)82 83/-- The slope `t/x` in the `x`-chart. -/84local notation:max "xSlope" O:max pi:max u:max a:max b:max =>85  chartSlope (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)86 87/-- The exceptional ideal `(x)` of the `x`-chart. -/88local notation:max "xExc" O:max pi:max u:max a:max b:max =>89  chartExceptional (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)90 91/-- If `f ≡ g` modulo the ideal `I`, then `(f) + I = I + (g)`. -/92private theorem span_sup_eq_sup_span {A : Type} [CommRing A] {I : Ideal A} {f g : A}93    (h : f - g ∈ I) : Ideal.span {f} ⊔ I = I ⊔ Ideal.span {g} := by94  refine le_antisymm (sup_le ?_ le_sup_left) (sup_le le_sup_right ?_) <;>95    rw [Ideal.span_singleton_le_iff_mem]96  · rw [← sub_add_cancel f g]97    exact add_mem (Ideal.mem_sup_left h) (Ideal.mem_sup_right (Ideal.mem_span_singleton_self g))98  · rw [← sub_sub_cancel f g]99    exact sub_mem (Ideal.mem_sup_left (Ideal.mem_span_singleton_self f)) (Ideal.mem_sup_right h)100 101/-- If `f = ∑ cᵢ t^(d-i) xⁱ`, then in the chart `R[t/x]` the function `f` factors as102`x^d · ∑ cᵢ (t/x)^(d-i)`, and the boundary contact of `f` with `t = 0` is `d` plus the contact103of the strict transform with the slope divisor. -/104theorem boundary_contact_of_twisted_generator (R : Type) [CommRing R] (t x : R)105    [(Ideal.span ({t,x} : Set R)).IsMaximal] (hreg : RegularParameterPair R t x) (d : ℕ) (f : R)106    (c : Fin (d + 1) → R) (hc : f = ∑ i : Fin (d + 1), c i * t ^ (d - i.val) * x ^ i.val) :107    algebraMap R (BlowupChart R x t) f = (chartBase R x t x)^d *108        ∑ i : Fin (d+1), algebraMap R (BlowupChart R x t) (c i) * (chartSlope R x t)^(d - i.val) ∧109      Module.length R (R ⧸ (Ideal.span {f} ⊔ Ideal.span {t})) = (d : ℕ∞) +110        Module.length (BlowupChart R x t) (BlowupChart R x t ⧸111          (Ideal.span {∑ i : Fin (d+1), algebraMap R (BlowupChart R x t) (c i) *112            (chartSlope R x t)^(d - i.val)} ⊔ Ideal.span {chartSlope R x t})) := by113  have hal : ∀ r : R, algebraMap R (BlowupChart R x t) r = chartBase R x t r := fun _ ↦ rfl114  set B := BlowupChart R x t115  set W := chartSlope R x t116  set g : B := ∑ i : Fin (d+1), algebraMap R B (c i) * W^(d - i.val) with hg117  refine ⟨?_, ?_⟩118  · rw [hc, map_sum, Finset.mul_sum]119    refine Finset.sum_congr rfl fun i _ ↦ ?_120    simp only [map_mul, map_pow, hal, ← blowup_chart_relation R x t]121    rw [← pow_mul_pow_sub _ (Nat.le_of_lt_succ i.isLt), hal]122    ring123  set I : Ideal R := Ideal.span {t}124  have hfI : f - c (Fin.last d) * x ^ d ∈ I := by125    rw [hc, Fin.sum_univ_castSucc]126    simp only [Fin.val_last, Nat.sub_self, pow_zero, mul_one, add_sub_cancel_right]127    exact Ideal.sum_mem _ fun i _ ↦ Ideal.mul_mem_right _ _ (Ideal.mul_mem_left _ _128      (Ideal.pow_mem_of_mem _ (Ideal.mem_span_singleton_self t) _ (Nat.sub_pos_of_lt i.isLt)))129  have hx (y) (hy : x * y ∈ I) : y ∈ I := by130    rw [← Ideal.Quotient.eq_zero_iff_mem] at hy ⊢131    apply hreg.2132    simpa using hy133  have hxd (n : ℕ) : ∀ y, x ^ n * y ∈ I → y ∈ I := by134    induction n with135    | zero => simp136    | succ n ih => exact fun y hy ↦ hx _ (ih _ (by rwa [pow_succ, mul_assoc] at hy))137  have hone : Module.length R (R ⧸ (I ⊔ Ideal.span {x})) = 1 := by138    rw [← Ideal.span_insert t {x}]139    have : IsSimpleModule R (R ⧸ Ideal.span ({t, x} : Set R)) :=140      isSimpleModule_iff_quot_maximal.mpr ⟨_, inferInstance, ⟨LinearEquiv.refl _ _⟩⟩141    exact Module.length_eq_one R _142  rw [span_sup_eq_sup_span hfI, length_quotient_sup_mul_eq_add R I (x ^ d) (c (Fin.last d)) (hxd d),143    length_quotient_sup_pow_eq_mul R I x hx d, hone, mul_one, add_comm]144  congr 1145  have hgW : g - algebraMap R B (c (Fin.last d)) ∈ Ideal.span {W} := by146    rw [hg, Fin.sum_univ_castSucc]147    simp only [Fin.val_last, Nat.sub_self, pow_zero, mul_one, add_sub_cancel_right]148    exact Ideal.sum_mem _ fun i _ ↦ Ideal.mul_mem_left _ _149      (Ideal.pow_mem_of_mem _ (Ideal.mem_span_singleton_self W) _ (Nat.sub_pos_of_lt i.isLt))150  rw [span_sup_eq_sup_span hgW]151  obtain ⟨ρ, hρ, -⟩ := boundary_chart_quotient_equiv R t x152  symm153  apply quotient_ring_length_intrinsic154  refine (DoubleQuot.quotQuotEquivQuotSup _ _).symm.trans155    ((Ideal.quotientEquiv _ _ ρ ?_).trans (DoubleQuot.quotQuotEquivQuotSup _ _))156  simp only [Ideal.map_span, Set.image_singleton]157  congr 2158  exact (hρ _).symm159 160/-- At a point `P` of the exceptional line corresponding to the irreducible `φ`, the image of the161contracted level-one curve ideal in `k[X]` is `(φ^r)`, where `r ≤ L` is the length of the162completed level-one quotient. -/163private theorem contracted_level_one_ideal_is_irreducible_power (R : Type) [CommRing R] (t x : R)164    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]165    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+*166      Polynomial (R ⧸ Ideal.span ({t,x} : Set R)))167    (P : Ideal (BlowupChart R t x)) [P.IsMaximal]168    (φ : Polynomial (R ⧸ Ideal.span ({t,x} : Set R)))169    (hφ : (P.map (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {φ})170    (hirr : Irreducible φ) (g : CompletedLocalAt (BlowupChart R t x) P) (L : ℕ)171    (hL : ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map172      (localCompletionMap (Localization.AtPrime P))) ^ L ≤ finiteLocalCurveIdeal (BlowupChart R t x)173      P (chartBase R t x t) g 1) :174    ∃ r : ℕ, r ≤ L ∧175        ((contractedLocalCurveIdeal (BlowupChart R t x) P (chartBase R t x t) g 1).map176        (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {φ^r} ∧177        Module.length (CompletedLocalAt (BlowupChart R t x) P) (CompletedLocalAt (BlowupChart R t x)178        P ⧸ finiteLocalCurveIdeal (BlowupChart R t x) P (chartBase R t x t) g 1) = (r : ℕ∞) := by179  set A := BlowupChart R t x180  set I := finiteLocalCurveIdeal A P (chartBase R t x t) g 1 with hIdef181  set J := contractedLocalCurveIdeal A P (chartBase R t x t) g 1 with hJdef182  have hPL : P ^ L ≤ J := completed_point_power_contraction A P L I hL183  have hTJ : chartExceptional R t x ≤ J := by184    rw [show chartExceptional R t x = Ideal.span {chartBase R t x t} from rfl, Ideal.span_le]185    rintro _ rfl186    change completedPointMap A P (chartBase R t x t) ∈ I187    rw [hIdef, finiteLocalCurveIdeal, pow_one]188    exact Ideal.subset_span (by simp)189  have hle : Ideal.span {φ ^ L} ≤ (J.map (Ideal.Quotient.mk (chartExceptional R t x))).map e := by190    have h1 := Ideal.map_pow e (Ideal.map (Ideal.Quotient.mk (chartExceptional R t x)) P) L191    have h0 := Ideal.map_pow (Ideal.Quotient.mk (chartExceptional R t x)) P L192    rw [← Ideal.span_singleton_pow, ← hφ, ← h1, ← h0]193    exact Ideal.map_mono (Ideal.map_mono hPL)194  have hK : RingHom.ker ((Ideal.Quotient.mk I).comp (completedPointMap A P)) = J := by195    rw [← RingHom.comap_ker, Ideal.mk_ker]; rfl196  have E1 : (A ⧸ J) ≃+* (CompletedLocalAt A P ⧸ I) :=197    (Ideal.quotEquivOfEq hK.symm).trans (RingHom.quotientKerEquivOfSurjective198      (finite_completed_point_quotient_surjective A P L I hL))199  have hlen := quotient_ring_length_intrinsic _ _ _ _ E1200  obtain ⟨r, hrL, hr⟩ : ∃ r ≤ L,201      (J.map (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {φ ^ r} := by202    let _ := Ideal.Quotient.field (Ideal.span ({t,x} : Set R))203    exact polynomial_ideal_of_irreducible_pow_le _ φ hirr _ L hle204  have hφ : Module.length (Polynomial (R ⧸ Ideal.span ({t,x} : Set R)))205      (Polynomial (R ⧸ Ideal.span ({t,x} : Set R)) ⧸ Ideal.span {φ ^ r}) = r := by206    let _ := Ideal.Quotient.field (Ideal.span ({t,x} : Set R))207    exact (polynomial_quotient_irreducible_pow_length _ φ hirr r).1208  refine ⟨r, hrL, hr, ?_⟩209  rw [← hlen, ← hφ]210  exact quotient_ring_length_intrinsic _ _ _ _211    ((DoubleQuot.quotQuotEquivQuotOfLE hTJ).symm.trans (Ideal.quotientEquiv _ _ e hr.symm))212 213private theorem length_quot_span_pair_toNat_eq {S S' : Type} [CommRing S] [CommRing S']214    (Φ : S ≃+* S') (g e : S) (g' e' : S')215    (hg : Φ g = g') (he : Ideal.span {Φ e} = Ideal.span {e'}) :216    (Module.length S (S ⧸ Ideal.span {g, e ^ 1})).toNat =217      (Module.length S' (S' ⧸ Ideal.span {g', e' ^ 1})).toNat := by218  rw [pow_one, pow_one]219  have h : Ideal.span {g', e'} = (Ideal.span {g, e}).map Φ := by220    rw [Ideal.map_span, Set.image_pair, hg, Ideal.span_insert, Ideal.span_insert, he]221  rw [quotient_ring_length_intrinsic S S' (Ideal.span {g, e}) (Ideal.span {g', e'})222    (Ideal.quotientEquiv _ _ Φ h)]223 224/-- At a common point of the two charts, the left and right multiplicities agree with the225multiplicity computed on the overlap. -/226theorem two_chart_common_multiplicity_eq (R : Type) [CommRing R] (t x : R)227    (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta) (i : D.ι) :228    leftMultiplicity D (Sum.inl i) = commonMultiplicity D i ∧229      rightMultiplicity D (Sum.inl i) = commonMultiplicity D i := by230  constructor231  · unfold leftMultiplicity commonMultiplicity leftLevelIdeal commonLevelIdeal finiteLocalCurveIdeal232    symm233    refine length_quot_span_pair_toNat_eq (D.leftIso i) _ _ _ _ rfl ?_234    have := D.leftIso_compat i (chartBase R t x t)235    unfold overlapException236    rw [this]; rfl237  · unfold rightMultiplicity commonMultiplicity rightLevelIdeal commonLevelIdeal238      finiteLocalCurveIdeal239    symm240    refine length_quot_span_pair_toNat_eq (D.rightIso i) _ _ _ _ rfl ?_241    have hx := D.rightIso_compat i (chartBase R x t x)242    have hrel : beta.right (chartBase R x t x) = overlapException R t x * overlapSlope R t x := by243      have h1 : beta.right (chartBase R x t x) = algebraMap R (BlowupOverlap R t x) x :=244        beta.right.commutes x245      have h2 := congrArg (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))246        (blowup_chart_relation R t x)247      rw [h1]248      unfold overlapException overlapSlope249      rw [← map_mul, h2]250      exact (IsScalarTower.algebraMap_apply R (BlowupChart R t x) (BlowupOverlap R t x) x).symm251    have hu : IsUnit (overlapSlope R t x) := IsLocalization.Away.algebraMap_isUnit _252    have hu' : IsUnit (D.rightIso i253        (completedPointMap (BlowupOverlap R t x) (D.Q i) (overlapSlope R t x))) :=254      (hu.map _).map _255    rw [hrel, map_mul, map_mul] at hx256    refine Eq.trans ?_ (congrArg Ideal.span (congrArg _ hx))257    exact Ideal.span_singleton_mul_right_unit hu' _ |>.symm258 259private noncomputable def completedLocalCast {A : Type} [CommRing A] {P' P : Ideal A} [P'.IsPrime]260    [P.IsPrime] (h : P' = P) :261    CompletedLocalAt A P' ≃+* CompletedLocalAt A P := by262  subst h; exact RingEquiv.refl _263 264private theorem completedLocalCast_completedPointMap {A : Type} [CommRing A] {P' P : Ideal A}265    [P'.IsPrime] [P.IsPrime] (h : P' = P) (a : A) :266    completedLocalCast h (completedPointMap A P' a) = completedPointMap A P a := by267  subst h; rfl268 269private theorem length_finiteLocalCurveIdeal_transport {A S : Type} [CommRing A] [CommRing S]270    {P' P : Ideal A} [P'.IsPrime] [P.IsPrime]271    (Φ : S ≃+* CompletedLocalAt A P') (h : P' = P) (gC : CompletedLocalAt A P) (e0 : A) (n : ℕ∞)272    (hl : Module.length (CompletedLocalAt A P) (CompletedLocalAt A P ⧸273      (Ideal.span {gC} ⊔ Ideal.span {completedPointMap A P e0})) = n) :274    Module.length (CompletedLocalAt A P') (CompletedLocalAt A P' ⧸275      finiteLocalCurveIdeal A P' e0 (Φ ((Φ.trans (completedLocalCast h)).symm gC)) 1) = n := by276  rw [RingEquiv.symm_trans_apply, RingEquiv.apply_symm_apply]277  subst h278  rw [finiteLocalCurveIdeal, pow_one, Ideal.span_insert]279  exact hl280 281private theorem strictTransformAt_transport (R : Type) [CommRing R] (t x : R)282    {S : Type} [CommRing S]283    {P' P : Ideal (BlowupChart R t x)} [P'.IsPrime] [P.IsPrime]284    (Φ : S ≃+* CompletedLocalAt (BlowupChart R t x) P') (h : P' = P)285    (gC : CompletedLocalAt (BlowupChart R t x) P) (d : ℕ) (J : Ideal R)286    (hs : strictTransformAt R t x P' d J =287        Ideal.span {Φ ((Φ.trans (completedLocalCast h)).symm gC)}) :288    strictTransformAt R t x P d J = Ideal.span {gC} := by289  rw [RingEquiv.symm_trans_apply, RingEquiv.apply_symm_apply] at hs290  subst h291  exact hs292 293private theorem length_finiteLocalCurveIdeal_toNat {A : Type} [CommRing A] {P : Ideal A} [P.IsPrime]294    (g : CompletedLocalAt A P) (e0 : A) (n : ℕ)295    (hl : Module.length (CompletedLocalAt A P) (CompletedLocalAt A P ⧸296      (Ideal.span {g} ⊔ Ideal.span {completedPointMap A P e0})) = n) :297    n = (Module.length (CompletedLocalAt A P) (CompletedLocalAt A P ⧸298      finiteLocalCurveIdeal A P e0 g 1)).toNat := by299  rw [finiteLocalCurveIdeal, pow_one, Ideal.span_insert, hl, ENat.toNat_natCast]300 301/-- At the prime `P` of `A`, every element `g` of the completed local ring such that `(g, z)` has302finite colength `n` is transverse to `z` (multiplication by `z` is injective modulo `g`), and the303ideal `(g, z)` contains a power of the maximal ideal. -/304private def TransverseFiniteAt (A : Type) [CommRing A] (P : Ideal A) [P.IsPrime] (z : A) : Prop :=305  ∀ (g : CompletedLocalAt A P) (n : ℕ),306    Module.length (CompletedLocalAt A P) (CompletedLocalAt A P ⧸307      (Ideal.span {g} ⊔ Ideal.span {completedPointMap A P z})) = n →308    Function.Injective (fun w : CompletedLocalAt A P ⧸ Ideal.span {g} =>309      Ideal.Quotient.mk (Ideal.span {g}) (completedPointMap A P z) * w) ∧310    ∃ L : ℕ, ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map311      (localCompletionMap (Localization.AtPrime P)))^L ≤ finiteLocalCurveIdeal A P z g 1312 313/-- The nonzero affine directions in the support of the divisor `Dv`. -/314private abbrev CommonDirections {k : Type} [Field k] (Dv : ExceptionalDivisor k) : Type :=315  {φ : AffineDirection k // φ ≠ zeroAffine k ∧ 0 < Dv (some φ)}316 317/-- The overlap point of a nonzero direction (a named function, so that the instance arguments318in the curve datum built below stay syntactically uniform). -/319private noncomputable def commonPoint (R : Type) [CommRing R] [IsLocalRing R] (t x : R)320    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (IsLocalRing.ResidueField R))321    {Dv : ExceptionalDivisor (IsLocalRing.ResidueField R)} (i : CommonDirections Dv) :322    Ideal (BlowupOverlap R t x) :=323  (directionPoint R t x e i.1).map (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))324 325/-- Generic form of `child_ideals_curve_datum`: the points of the exceptional line are assumed to326have the expected properties, and child-ideal generators are assumed transverse and finite. -/327private theorem child_ideals_curve_datum_of_points (R : Type) [CommRing R] [IsLocalRing R] (t x : R)328    [IsNoetherianRing (BlowupChart R t x)] [IsNoetherianRing (BlowupChart R x t)]329    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (IsLocalRing.ResidueField R))330    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R)) (hinf : (infinityPoint R t x).IsPrime)331    (s : State) (d : ℕ) (beta : BlowupRestriction R t x)332    (I : ∀ Q : divisorSupport Dv, Ideal (divisorLocalRing R t x e Dv hinf Q))333    (hI : ∀ Q : divisorSupport Dv, I Q ∈ childIdealSet R t x e Dv hinf s d Q)334    (hdir : ∀ φ, (directionPoint R t x e φ).IsMaximal ∧335      chartBase R t x t ∈ directionPoint R t x e φ ∧336      (chartSlope R t x ∈ directionPoint R t x e φ ↔ φ = zeroAffine (IsLocalRing.ResidueField R)))337    (hinj : Function.Injective (directionPoint R t x e))338    (hover : ∀ φ, φ ≠ zeroAffine (IsLocalRing.ResidueField R) →339      ((directionPoint R t x e φ).map340        (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).IsMaximal ∧341      ((directionPoint R t x e φ).map (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).comap342        (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) = directionPoint R t x e φ)343    (hinfmax : (infinityPoint R t x).IsMaximal ∧ chartBase R x t x ∈ infinityPoint R t x ∧344      chartSlope R x t ∈ infinityPoint R t x)345    (htrL : ∀ (P : Ideal (BlowupChart R t x)) [P.IsMaximal], chartBase R t x t ∈ P →346      TransverseFiniteAt (BlowupChart R t x) P (chartBase R t x t))347    (htrR : ∀ (P : Ideal (BlowupChart R x t)) [P.IsMaximal], chartBase R x t x ∈ P →348      chartSlope R x t ∈ P → TransverseFiniteAt (BlowupChart R x t) P (chartBase R x t x)) :349    ∃ D : TwoChartCurveData R t x beta, MatchesDivisor e D Dv ∧ ∀ f : R,350      (∀ s : D.ι ⊕ D.ι0, strictTransformAt R t x (leftPoint D s) d (Ideal.span {f}) =351          Ideal.span {leftData D s}) →352      (∀ s : D.ι ⊕ D.ιinf, strictTransformAt R x t (rightPoint D s) d (Ideal.span {f}) =353          Ideal.span {rightData D s}) →354      ∀ Q : divisorSupport Dv, divisorStrictTransform R t x e Dv hinf355          d (Ideal.span {f}) Q = I Q := by356  set k := IsLocalRing.ResidueField R357  set alpha := algebraMap (BlowupChart R t x) (BlowupOverlap R t x)358  choose gen hgen using fun Q ↦ (hI Q).1359  have hlen : ∀ Q : divisorSupport Dv, Module.length (divisorLocalRing R t x e Dv hinf Q)360      (divisorLocalRing R t x e Dv hinf Q ⧸ (Ideal.span {gen Q} ⊔361        Ideal.span {divisorException R t x e Dv hinf Q})) = (Dv Q.val : ℕ∞) :=362    fun Q ↦ hgen Q ▸ (hI Q).2.1363  have hQmax : ∀ i : CommonDirections Dv, (commonPoint R t x e i).IsMaximal :=364    fun i ↦ (hover i.1 i.2.1).1365  have hcomap (i : CommonDirections Dv) : (commonPoint R t x e i).comap alpha =366      directionPoint R t x e i.1 := (hover i.1 i.2.1).2367  have hinfM : (infinityPoint R t x).IsMaximal := hinfmax.1368  have hdirM : ∀ φ, (directionPoint R t x e φ).IsMaximal := fun φ ↦ (hdir φ).1369  have := divisorSupport_finite Dv370  choose Φ hΦ using fun i : CommonDirections Dv ↦371    completed_point_transport_left R t x (commonPoint R t x e i)372  choose Ψ hΨ using fun i : CommonDirections Dv ↦373    completed_point_transport_right R t x beta (commonPoint R t x e i)374  -- `Θ i` identifies the completion at the overlap point `i` with the one at the chart point375  let Θ (i : CommonDirections Dv) := (Φ i).trans (completedLocalCast (hcomap i))376  have hΘ (i : CommonDirections Dv) (a) : Θ i (completedPointMap _ _ (alpha a)) =377      completedPointMap (BlowupChart R t x) (directionPoint R t x e i.1) a := by378    rw [RingEquiv.trans_apply, hΦ i a, completedLocalCast_completedPointMap]379  let gC (i : CommonDirections Dv) : CompletedLocalAt _ (directionPoint R t x e i.1) :=380    gen ⟨some i.1, i.2.2⟩381  have htrC (i : CommonDirections Dv) := @htrL (directionPoint R t x e i.1) (hdirM _)382    (hdir i.1).2.1 (gC i) _ (hlen ⟨some i.1, i.2.2⟩)383  have htr0 (l : {_u : Unit // 0 < Dv (zeroDirection k)}) := @htrL _ (hdirM (zeroAffine k))384    (hdir _).2.1 (gen ⟨zeroDirection k, l.2⟩) _ (hlen ⟨zeroDirection k, l.2⟩)385  have htrI (l : {_u : Unit // 0 < Dv none}) := @htrR (infinityPoint R t x) hinfM hinfmax.2.1386    hinfmax.2.2 (gen ⟨none, l.2⟩) _ (hlen ⟨none, l.2⟩)387  have he (i : CommonDirections Dv) : (Θ i).symm (completedPointMap _ _ (chartBase R t x t)) * 1 =388      completedPointMap _ (commonPoint R t x e i) (overlapException R t x) := by389    rw [mul_one, RingEquiv.symm_apply_eq]; exact (hΘ i _).symm390  have hM (i : CommonDirections Dv) :391      (IsLocalRing.maximalIdeal (Localization.AtPrime (commonPoint R t x e i))).map392        (localCompletionMap _) ≤393      ((IsLocalRing.maximalIdeal (Localization.AtPrime (directionPoint R t x e i.1))).map394        (localCompletionMap _)).map (Θ i).symm := by395    rw [Ideal.map_symm, ← Ideal.map_le_iff_le_comap,396      map_maximalIdeal_localCompletion (commonPoint R t x e i)]397    exact (map_maximalIdeal_localCompletion_transport alpha _ _ (Θ i) (hΘ i)).le398  let D : TwoChartCurveData R t x beta :=399    { ι := CommonDirections Dv400      fin := Finite.of_injective (β := divisorSupport Dv) (fun i ↦ ⟨some i.1, i.2.2⟩)401          fun i j h ↦ Subtype.ext (Option.some_injective _ (congrArg Subtype.val h))402      Q := commonPoint R t x e403      maximal := hQmax404      inj := fun i j h ↦ Subtype.ext <| hinj <|405        (hcomap i).symm.trans <| (congrArg (Ideal.comap alpha) h).trans (hcomap j)406      onE := fun i ↦ Ideal.mem_map_of_mem _ (hdir i.1).2.1407      g := fun i ↦ (Θ i).symm (gC i)408      transverse := fun i ↦ mul_injective_quotient_transport _ isUnit_one (he i) (htrC i).1409      finite := fun i ↦ exists_pow_le_span_pair_transport _ isUnit_one (he i) (hM i) (htrC i).2 1410      leftIso := Φ411      leftIso_compat := hΦ412      rightIso := Ψ413      rightIso_compat := hΨ414      ι0 := {_u : Unit // 0 < Dv (zeroDirection k)}415      P0 := fun _ ↦ directionPoint R t x e (zeroAffine k)416      maximal0 := fun _ ↦ hdirM _417      inj0 := fun a b _ ↦ Subsingleton.elim a b418      slope0 := fun _ ↦ ((hdir _).2.2).2 rfl419      onE0 := fun _ ↦ (hdir _).2.1420      g0 := fun l ↦ gen ⟨zeroDirection k, l.2⟩421      transverse0 := fun l ↦ (htr0 l).1422      finite0 := fun l ↦ (htr0 l).2423      ιinf := {_u : Unit // 0 < Dv none}424      Pinf := fun _ ↦ infinityPoint R t x425      maximalinf := fun _ ↦ hinfM426      injinf := fun a b _ ↦ Subsingleton.elim a b427      slopeinf := fun _ ↦ hinfmax.2.2428      onEinf := fun _ ↦ hinfmax.2.1429      ginf := fun l ↦ gen ⟨none, l.2⟩430      transverseinf := fun l ↦ (htrI l).1431      finiteinf := fun l ↦ (htrI l).2 }432  refine ⟨D, ⟨fun i ↦ ⟨i.1, i.2.1, rfl, ?_⟩, fun φ hφ hpos ↦ ⟨⟨φ, hφ, hpos⟩, rfl⟩,433    fun l ↦ ⟨rfl, length_finiteLocalCurveIdeal_toNat (P := directionPoint R t x e (zeroAffine k))434      _ _ _ (hlen ⟨zeroDirection k, l.2⟩)⟩, fun h ↦ ⟨⟨(), h⟩⟩,435    fun l ↦ ⟨rfl, length_finiteLocalCurveIdeal_toNat (P := infinityPoint R t x) _ _ _436      (hlen ⟨none, l.2⟩)⟩, fun h ↦ ⟨⟨(), h⟩⟩⟩, fun f hL hR ↦ ?_⟩437  · rw [← (two_chart_common_multiplicity_eq R t x beta D i).1]438    exact ((congrArg ENat.toNat (length_finiteLocalCurveIdeal_transport (Φ i) (hcomap i) (gC i)439      (chartBase R t x t) _ (hlen ⟨some i.1, i.2.2⟩))).trans (ENat.toNat_natCast _)).symm440  rintro ⟨_ | φ, hQ⟩441  · exact (hR (Sum.inr ⟨(), hQ⟩)).trans (hgen _).symm442  by_cases hφ : φ = zeroAffine k443  · subst hφ444    exact (hL (Sum.inr ⟨(), hQ⟩)).trans (hgen _).symm445  · exact (strictTransformAt_transport R t x (Φ ⟨φ, hφ, hQ⟩) (hcomap ⟨φ, hφ, hQ⟩) (gC ⟨φ, hφ, hQ⟩)446      d _ (hL (Sum.inl ⟨φ, hφ, hQ⟩))).trans (hgen _).symm447 448private theorem directionPoint_overlap_facts (O R : Type) [CommRing O] [IsDomain O]449    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]450    (S : SurfaceData O R) (t x : R) (ht : S.t = t) (hx : S.x = x)451    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (IsLocalRing.ResidueField R))452    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =453      Polynomial.C (IsLocalRing.residue R r))454    (heZ : e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X)455    (φ : AffineDirection (IsLocalRing.ResidueField R))456    (hφ : φ ≠ zeroAffine (IsLocalRing.ResidueField R)) :457    ((directionPoint R t x e φ).map458        (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).IsMaximal ∧459      ((directionPoint R t x e φ).map (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).comap460        (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) = directionPoint R t x e φ := by461  subst ht hx462  obtain ⟨h1, -, h2⟩ := direction_point_overlap_maximal O R S e he heZ φ hφ463  exact ⟨h1, h2⟩464 465private theorem infinityPoint_facts (O R : Type) [CommRing O] [IsDomain O]466    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]467    (S : SurfaceData O R) (t x : R) (ht : S.t = t) (hx : S.x = x) :468    (infinityPoint R t x).IsMaximal ∧ chartBase R x t x ∈ infinityPoint R t x ∧469      chartSlope R x t ∈ infinityPoint R t x := by470  subst ht hx471  obtain ⟨h1, h2, h3, -⟩ := infinity_point_maximal O R S472  exact ⟨h1, h2, h3⟩473 474private theorem length_quot_span_one_sup {A : Type} [CommRing A] (P : Ideal A) [P.IsPrime]475    (y : CompletedLocalAt A P) :476    Module.length (CompletedLocalAt A P) (CompletedLocalAt A P ⧸477      (Ideal.span {(1 : CompletedLocalAt A P)} ⊔ Ideal.span {y})) = ((0 : ℕ) : ℕ∞) := by478  rw [Ideal.span_singleton_one, top_sup_eq, Nat.cast_zero, Module.length_eq_zero_iff]479  exact Ideal.Quotient.subsingleton_iff.mpr rfl480 481/-- Every family of child ideals over the support of `Dv` is realized by a two-chart curve datum482matching `Dv`: any global function with the prescribed chart strict transforms has strict483transform `I Q` at every point `Q`. -/484theorem child_ideals_curve_datum (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Lemma 4.3485    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)486    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)487        [IsLocalRing (ConcreteSurface O pi u a b)]488    (e : (tChart O pi u a b ⧸ tExc O pi u a b) ≃+* Polynomial (IsLocalRing.ResidueField489        (ConcreteSurface O pi u a b)))490    (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)491        (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))492    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)493    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))494    (hinf : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)495        (surfaceX O pi u a b)).IsPrime) (s : State) (d : ℕ)496    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)497        (surfaceX O pi u a b))498    (I : ∀ Q : divisorSupport Dv, Ideal (divisorLocalRing (ConcreteSurface O pi u a b)499        (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf Q))500    (hI : ∀ Q : divisorSupport Dv, I Q ∈ childIdealSet (ConcreteSurface O pi u a b)501        (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf s d Q) :502    ∃ D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)503        beta, MatchesDivisor e D Dv ∧ ∀ f : ConcreteSurface O pi u a b,504      (∀ s : D.ι ⊕ D.ι0,505        strictTransformAt (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)506            (leftPoint D s) d (Ideal.span {f}) = Ideal.span {leftData D s}) →507      (∀ s : D.ι ⊕ D.ιinf, strictTransformAt (ConcreteSurface O pi u a b) (surfaceX O pi u a b)508          (surfaceT O pi u a b) (rightPoint D s) d (Ideal.span {f}) =509        Ideal.span {rightData D s}) →510      ∀ Q : divisorSupport Dv, divisorStrictTransform (ConcreteSurface O pi u a b)511          (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf d (Ideal.span {f}) Q =512        I Q := by513  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)514      (surfaceX O pi u a b)515  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)516      (surfaceT O pi u a b)517  obtain ⟨hDom, hReg, S, -, hSt, hSx, -⟩ :=518    concrete_surface_data_exists_unconditional O pi hpi u a b ha519  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set520      (ConcreteSurface O pi u a b))).IsMaximal :=521    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha522  obtain ⟨hdir, hinj, -⟩ := directionPoint_properties _ _ _ e he heZ523  have hinfmax := infinityPoint_facts O _ S _ _ hSt hSx524  refine child_ideals_curve_datum_of_points _ _ _ e Dv hinf s d beta I hI525    (fun φ ↦ ⟨(hdir φ).1, (hdir φ).2.1, (hdir φ).2.2.1⟩) hinj526    (directionPoint_overlap_facts O _ S _ _ hSt hSx e he heZ) hinfmax527    (fun P _ hP g n hg ↦ ?_) (fun P _ hP hW g n hg ↦ ?_)528  · have := @child_ideal_generator_transverse_finite O _ _ _ _ _ pi hpi u a b ha P _ _ hP g n hg529      (infinityPoint _ _ _) hinfmax.1 hinfmax.1.isPrime hinfmax.2.1 hinfmax.2.2 1530      0 (length_quot_span_one_sup _ _)531    exact ⟨this.1.1, this.1.2.2⟩532  · have := @child_ideal_generator_transverse_finite O _ _ _ _ _ pi hpi u a b ha533      (directionPoint _ _ _ e (zeroAffine _)) (hdir _).1 (hdir _).1.isPrime (hdir _).2.1 1 0534      (length_quot_span_one_sup _ _) P _ _ hP hW g n hg535    exact ⟨this.2.1, this.2.2.2⟩536 537/-- For a curve datum built from `f = ∑ cᵢ tᵈ⁻ⁱ xⁱ` with residue form `H` of divisor `Dv`, the538common points are nonzero affine directions with the right multiplicities, and the zero-slope539points sit at the zero direction with multiplicity `Dv 0`. -/540private theorem curve_datum_common_and_zero_clauses (O : Type) [CommRing O] [IsDomain O]541    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]542    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)543    (a b : ℕ) (ha : 0 < a) (d : ℕ) (c : Fin (d + 1) → ConcreteSurface O pi u a b)544    [IsLocalRing (ConcreteSurface O pi u a b)]545    (H : Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))546    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))547    (hH : HasHomogeneousDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) d H Dv)548    (hcH : ∀ i : Fin (d+1), IsLocalRing.residue (ConcreteSurface O pi u a b) (c i) = H.coeff i.val)549    (e : (tChart O pi u a b ⧸ tExc O pi u a b) ≃+*550      Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))551    (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)552      (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))553    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)554    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)555      (surfaceX O pi u a b))556    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)557      beta)558    (hleft : ∀ s : D.ι ⊕ D.ι0,559      leftData D s = completedPointMap (tChart O pi u a b) (leftPoint D s)560        (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *561            tSlope O pi u a b^i.val) ∧562      (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *563          tSlope O pi u a b^i.val) ∈ leftPoint D s) :564    (∀ i : D.ι, ∃ φ : AffineDirection (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)),565      φ ≠ zeroAffine (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) ∧566      D.Q i = (directionPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)567          (surfaceX O pi u a b) e φ).map (algebraMap (tChart O pi u a b) (tOverlap O pi u a b)) ∧568      Dv (some φ) = commonMultiplicity D i) ∧569    ∀ k : D.ι0, D.P0 k = directionPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)570        (surfaceX O pi u a b) e571          (zeroAffine (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) ∧572      Dv (zeroDirection (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) =573        leftMultiplicity D (Sum.inr k) := by574  have hmax : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set575      (ConcreteSurface O pi u a b))).IsMaximal :=576    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha577  have hne : ∃ i : Fin (d+1), c i ∉ Ideal.span {surfaceT O pi u a b, surfaceX O pi u a b} := by578    obtain ⟨j, hj⟩ : ∃ j, H.coeff j ≠ 0 := by579      by_contra! h; exact hH.1 (Polynomial.ext h)580    have hjd : j < d + 1 := Nat.lt_succ_of_le ((Polynomial.le_natDegree_of_ne_zero hj).trans hH.2.1)581    refine ⟨⟨j, hjd⟩, fun hmem ↦ hj ?_⟩582    rw [← hcH ⟨j, hjd⟩]583    exact (IsLocalRing.residue_eq_zero_iff _).2 (IsLocalRing.le_maximalIdeal hmax.ne_top hmem)584  have hHBAR := reduced_form_eq_of_residue_coeff (ConcreteSurface O pi u a b) d c H hH.2.1 hcH585  have hlc : H.leadingCoeff ≠ 0 := Polynomial.leadingCoeff_ne_zero.2 hH.1586  obtain ⟨hlm, -, hlt⟩ := two_chart_left_points_maximal _ _ _ beta D587  have : ∀ s, (leftPoint D s).IsMaximal := hlm588  have mult (s : D.ι ⊕ D.ι0) (φ : AffineDirection (IsLocalRing.ResidueField589      (ConcreteSurface O pi u a b)))590      (hPφ : ((leftPoint D s).map (Ideal.Quotient.mk (tExc O pi u a b))).map e = Ideal.span591          {φ.val}) :592      Dv (some φ) = leftMultiplicity D s := by593    unfold leftMultiplicity leftLevelIdeal finiteLocalCurveIdeal594    rw [(hleft s).1, pow_one, concrete_strict_transform_multiplicity O pi hpi u a b ha d c hne595      (leftPoint D s) (hlt s) e he heZ φ.val φ.property hPφ, hHBAR, ENat.toNat_natCast]596    conv_rhs => rw [hH.2.2.2]597    exact ((count_normalizedFactors_divisorAffinePolynomial _ Dv _ hlc φ).1).symm598  refine ⟨fun i ↦ ?_, fun k ↦ ?_⟩599  · obtain ⟨φ, hφ, himg, hslope⟩ :=600      chart_point_eq_directionPoint _ _ _ e he heZ (leftPoint D (Sum.inl i)) (hlt (Sum.inl i))601    have hZ := (overlap_exceptional_point_comap_maximal _ _ _ (D.Q i) (D.onE i)).2.1602    refine ⟨φ, fun h0 ↦ hZ (hslope.2 h0), ?_, ?_⟩603    · rw [← show leftPoint D (Sum.inl i) = _ from hφ]604      exact (IsLocalization.map_under (Submonoid.powers (tSlope O pi u a b)) _ (D.Q i)).symm605    · rw [mult (Sum.inl i) φ himg]606      exact (two_chart_common_multiplicity_eq _ _ _ beta D i).1607  · obtain ⟨φ, hφ, himg, hslope⟩ :=608      chart_point_eq_directionPoint _ _ _ e he heZ (leftPoint D (Sum.inr k)) (hlt (Sum.inr k))609    obtain rfl : φ = zeroAffine _ := hslope.1 (D.slope0 k)610    exact ⟨hφ, mult (Sum.inr k) _ himg⟩611 612/-- A curve datum built from `f = ∑ cᵢ tᵈ⁻ⁱ xⁱ`, whose residue form has divisor `Dv`, matches613`Dv`. -/614private theorem curve_datum_matches_divisor (O : Type) [CommRing O] [IsDomain O]615    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]616    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)617    (a b : ℕ) (ha : 0 < a) (d : ℕ) (f : ConcreteSurface O pi u a b)618    (c : Fin (d + 1) → ConcreteSurface O pi u a b)619    (hc : f = ∑ i : Fin (d + 1), c i * surfaceT O pi u a b ^ (d - i.val) *620      surfaceX O pi u a b ^ i.val)621    [IsLocalRing (ConcreteSurface O pi u a b)]622    (H : Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))623    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))624    (hH : HasHomogeneousDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) d H Dv)625    (hcH : ∀ i : Fin (d+1), IsLocalRing.residue (ConcreteSurface O pi u a b) (c i) = H.coeff i.val)626    (e : (tChart O pi u a b ⧸ tExc O pi u a b) ≃+*627      Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))628    (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)629      (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))630    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)631    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)632      (surfaceX O pi u a b))633    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)634      beta)635    (hleft : ∀ s : D.ι ⊕ D.ι0, leftData D s = completedPointMap (tChart O pi u a b) (leftPoint D s)636      (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *637        tSlope O pi u a b^i.val) ∧ (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)638          (tChart O pi u a b) (c i) * tSlope O pi u a b^i.val) ∈ leftPoint D s)639    (hleftsurj : ∀ P : Ideal (tChart O pi u a b), P.IsMaximal →640      tBase O pi u a b (surfaceT O pi u a b) ∈ P → (∑ i : Fin (d+1), algebraMap641        (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) * tSlope O pi u a b^i.val) ∈ P →642      ∃ s : D.ι ⊕ D.ι0, leftPoint D s = P)643    (hright : ∀ s : D.ι ⊕ D.ιinf, Ideal.span {rightData D s} = Ideal.span {completedPointMap644      (xChart O pi u a b) (rightPoint D s) (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b)645        (xChart O pi u a b) (c i) * xSlope O pi u a b^(d - i.val))} ∧ (∑ i : Fin (d+1), algebraMap646          (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) * xSlope O pi u a b^(d - i.val)) ∈647        rightPoint D s)648    (hrightsurj : ∀ P : Ideal (xChart O pi u a b), P.IsMaximal →649      xBase O pi u a b (surfaceX O pi u a b) ∈ P → (∑ i : Fin (d+1), algebraMap650        (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) * xSlope O pi u a b^(d - i.val)) ∈651          P → ∃ s : D.ι ⊕ D.ιinf, rightPoint D s = P) :652    MatchesDivisor e D Dv := by653  have h1 := curve_datum_common_and_zero_clauses O pi hpi u a b ha d c H Dv hH hcH e he heZ beta D654    hleft655  have h2 := curve_datum_surj_and_inf_clauses O pi hpi u a b ha d f c hc H Dv hH hcH e he heZ beta D656    hleft hleftsurj hright hrightsurj657  exact ⟨h1.1, h2.1, h1.2, h2.2.1, h2.2.2.1, h2.2.2.2⟩658 659/-- If a two-chart curve datum matches the divisor `Dv`, the degree of `Dv` is the curve datum660degree. -/661theorem matches_divisor_degree (O R : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Lemma 4.3662    [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R] (S : SurfaceData O R)663    (beta : BlowupRestriction R S.t S.x) (D : TwoChartCurveData R S.t S.x beta)664    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R))665    (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+*666      Polynomial (IsLocalRing.ResidueField R))667    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =668      Polynomial.C (IsLocalRing.residue R r))669    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)670    (hm : MatchesDivisor e D Dv) [IsNoetherianRing (BlowupChart R S.t S.x)]671    [IsNoetherianRing (BlowupChart R S.x S.t)] :672    exceptionalDegree (IsLocalRing.ResidueField R) Dv = curveDataDegree D := by673  classical674  set F := IsLocalRing.ResidueField R675  have hP := direction_point_maximal O R S e he heZ676  have hO := direction_point_overlap_maximal O R S e he heZ677  have hinjdir : Function.Injective (directionPoint R S.t S.x e) := (hP (zeroAffine F)).2.2.2.2.2678  choose φ hφ0 hφQ hφm using hm.common679  have hleft (i) : leftPoint D (Sum.inl i) = directionPoint R S.t S.x e (φ i) := by680    change (D.Q i).comap _ = _681    rw [hφQ i]; exact (hO (φ i) (hφ0 i)).2.2682  have hφinj : Function.Injective φ := fun i j h ↦ D.inj (by rw [hφQ i, hφQ j, h])683  have hsurj : ∀ ψ : AffineDirection F, ψ ≠ zeroAffine F → 0 < Dv (some ψ) → ∃ i, φ i = ψ := by684    intro ψ hψ hpos685    obtain ⟨i, hi⟩ := hm.common_surj ψ hψ hpos686    refine ⟨i, hinjdir ?_⟩687    rw [← hleft i]688    change (D.Q i).comap _ = _689    rw [hi]; exact (hO ψ hψ).2.2690  have hdeg (ψ : AffineDirection F) :691      (Module.length R (BlowupChart R S.t S.x ⧸ directionPoint R S.t S.x e ψ)).toNat =692        ψ.val.natDegree := by693    rw [(hP ψ).2.2.2.2.1]; rfl694  have : Fintype D.ι := Fintype.ofFinite _695  have : Fintype D.ι0 := Fintype.ofFinite _696  have : Fintype D.ιinf := Fintype.ofFinite _697  unfold curveDataDegree698  rw [finsum_eq_sum_of_fintype, finsum_eq_sum_of_fintype, Fintype.sum_sum_type]699  have hc : ∀ i, leftResidueDegree D (Sum.inl i) * leftMultiplicity D (Sum.inl i) =700      directionDegree F (some (φ i)) * Dv (some (φ i)) := by701    intro i702    unfold leftResidueDegree703    rw [hleft i, hdeg, (two_chart_common_multiplicity_eq R _ _ beta D i).1, hφm i]704    rfl705  have hz : ∑ k : D.ι0, leftResidueDegree D (Sum.inr k) * leftMultiplicity D (Sum.inr k) =706      directionDegree F (zeroDirection F) * Dv (zeroDirection F) := by707    by_cases hne : Nonempty D.ι0708    · obtain ⟨k⟩ := hne709      have : Subsingleton D.ι0 := ⟨fun a b => D.inj0 ((hm.zero a).1.trans (hm.zero b).1.symm)⟩710      rw [Fintype.sum_subsingleton _ k]711      unfold leftResidueDegree712      change (Module.length R (BlowupChart R S.t S.x ⧸ D.P0 k)).toNat * _ = _713      rw [(hm.zero k).1, hdeg, ← (hm.zero k).2]714      rfl715    · have h0 : Dv (zeroDirection F) = 0 := by716        by_contra h; exact hne (hm.zero_surj (Nat.pos_of_ne_zero h))717      rw [h0, mul_zero]718      have : IsEmpty D.ι0 := not_nonempty_iff.mp hne719      simp720  have hi : ∑ l : D.ιinf, rightMultiplicity D (Sum.inr l) =721      directionDegree F none * Dv none := by722    by_cases hne : Nonempty D.ιinf723    · obtain ⟨l⟩ := hne724      have : Subsingleton D.ιinf := ⟨fun a b => D.injinf ((hm.inf a).1.trans (hm.inf b).1.symm)⟩725      rw [Fintype.sum_subsingleton _ l, ← (hm.inf l).2]726      change _ = 1 * _727      rw [one_mul]728    · have h0 : Dv none = 0 := by729        by_contra h; exact hne (hm.inf_surj (Nat.pos_of_ne_zero h))730      rw [h0, mul_zero]731      have : IsEmpty D.ιinf := not_nonempty_iff.mp hne732      simp733  rw [Finset.sum_congr rfl (fun i _ => hc i), hz, hi]734  have hz1 : ∀ i, (some (φ i) : ClosedDirection F) ≠ zeroDirection F := by735    intro i h736    exact hφ0 i (Option.some_injective _ h)737  unfold exceptionalDegree738  rw [Finsupp.sum_of_support_subset Dv (s := insert none (insert (zeroDirection F)739      (Finset.univ.image (fun i => (some (φ i) : ClosedDirection F))))) ?_ _ (by simp)]740  · rw [Finset.sum_insert (by simp [zeroDirection]), Finset.sum_insert (by simpa using hz1),741      Finset.sum_image (fun a _ b _ h => hφinj (Option.some_injective _ h))]742    ring743  · intro P hPm744    rw [Finsupp.mem_support_iff] at hPm745    rcases P with _ | ψ746    · simp747    · by_cases hψ : ψ = zeroAffine F748      · subst hψ; simp [zeroDirection, zeroAffine]749      · obtain ⟨i, rfl⟩ := hsurj ψ hψ (Nat.pos_of_ne_zero hPm)750        simp751 752/-- Every ideal `J` of the fixed tangent cell is principal, generated by a degree-`d` form `f`753whose chart strict transforms define a two-chart curve datum matching `Dv` of degree `deg Dv`. -/754theorem fixed_tangent_cell_curve_datum (O : Type) [CommRing O] [IsDomain O]755    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]756    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)757    (a b : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a b)]758        [IsRegularLocalRing (ConcreteSurface O pi u a b)] (S : SurfaceData O759            (ConcreteSurface O pi u a b))760    (hS : S.t = surfaceT O pi u a b ∧ S.x = surfaceX O pi u a b) (e :761        (tChart O pi u a b ⧸ tExc O pi u a b) ≃+* Polynomial (IsLocalRing.ResidueField762            (ConcreteSurface O pi u a b)))763    (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)764        (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))765    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)766    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) (s : State)767        (d : ℕ) (J : Ideal (ConcreteSurface O pi u a b))768    (hJ : J ∈ fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv)769        (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)770            (surfaceX O pi u a b)) :771    ∃ (f : ConcreteSurface O pi u a b) (c : Fin (d+1) → ConcreteSurface O pi u a b)772        (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b)773            (surfaceX O pi u a b) beta), J = Ideal.span {f} ∧774      f = ∑ i : Fin (d+1), c i * surfaceT O pi u a b^(d - i.val) * surfaceX O pi u a b^i.val ∧775      (∀ s : D.ι ⊕ D.ι0,776        leftData D s = completedPointMap (tChart O pi u a b) (leftPoint D s)777          (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *778              tSlope O pi u a b^i.val) ∧779        (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (tChart O pi u a b) (c i) *780            tSlope O pi u a b^i.val) ∈ leftPoint D s) ∧781      (∀ s : D.ι ⊕ D.ιinf,782        Ideal.span {rightData D s} = Ideal.span {completedPointMap (xChart O pi u a b)783            (rightPoint D s)784          (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *785              xSlope O pi u a b^(d - i.val))} ∧786        (∑ i : Fin (d+1), algebraMap (ConcreteSurface O pi u a b) (xChart O pi u a b) (c i) *787            xSlope O pi u a b^(d - i.val)) ∈ rightPoint D s) ∧788      (∀ s : D.ι ⊕ D.ι0,789        strictTransformAt (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)790            (leftPoint D s) d J = Ideal.span {leftData D s}) ∧791      (∀ s : D.ι ⊕ D.ιinf,792        strictTransformAt (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)793            (rightPoint D s) d J = Ideal.span {rightData D s}) ∧794      MatchesDivisor e D Dv ∧795      curveDataDegree D = exceptionalDegree (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))796          Dv := by797  obtain ⟨ht, hx⟩ := hS798  cases S with | mk a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15799  dsimp only at ht hx800  subst ht hx801  obtain ⟨f, c, H, hJf, hf, hH, hcH, hne⟩ :=802    fixed_tangent_cell_generator_coefficients O _ _ s d Dv J hJ803  obtain ⟨D, hl, hls, hr, hrs, hst1, hst2⟩ :=804    curve_datum_of_parent_function O pi hpi u a b ha d f c hf hne beta805  have hm : MatchesDivisor e D Dv :=806    curve_datum_matches_divisor O pi hpi u a b ha d f c hf H Dv hH hcH e he heZ beta D hl hls hr hrs807  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)808      (surfaceX O pi u a b)809  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)810      (surfaceT O pi u a b)811  have hd := matches_divisor_degree O (ConcreteSurface O pi u a b)812    ⟨a1, a2, surfaceT O pi u a b, surfaceX O pi u a b, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14,813        a15⟩ beta D Dv e he heZ hm814  subst hJf815  exact ⟨f, c, D, rfl, hf, hl, hr, hst1, hst2, hm, hd.symm⟩816 817/-- **Level-one kernels on a blow-up chart.** Let `e` identify the exceptional line of the chart818`R[x/t]` with `k[X]` (`k = R ⧸ I`, `I = (t, x)`), and let `P s` be finitely many distinct819closed points of the exceptional line carrying finite-length level-one curve data `g s`. Then the820points correspond to distinct monic irreducibles `φ s` (with `φ s = X` exactly at the points where821the slope vanishes, and `deg φ s` the residue degree), the level-one lengths are finite numbers822`m s`, and the intersection of the contracted level-one ideals maps to `(∏ φ s ^ m s)`. -/823theorem level_one_kernel_polynomial (R : Type) [CommRing R] (t x : R) (I : Ideal R) [I.IsMaximal]824    (hI : Ideal.span ({t,x} : Set R) = I) [IsNoetherianRing (BlowupChart R t x)]825    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (R ⧸ I))826    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =827      Polynomial.C (Ideal.Quotient.mk I r))828    (heZ : e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X)829    {ι : Type} [Finite ι] (P : ι → Ideal (BlowupChart R t x)) [∀ s, (P s).IsMaximal]830    (hinjP : Function.Injective P) (htP : ∀ s, chartBase R t x t ∈ P s)831    (g : ∀ s, CompletedLocalAt (BlowupChart R t x) (P s))832    (hfin : ∀ s, ∃ L : ℕ, ((IsLocalRing.maximalIdeal (Localization.AtPrime (P s))).map833      (localCompletionMap (Localization.AtPrime (P s))))^L ≤834      finiteLocalCurveIdeal (BlowupChart R t x) (P s) (chartBase R t x t) (g s) 1) :835    ∃ (φ : ι → Polynomial (R ⧸ I)) (m : ι → ℕ), (∀ s, (φ s).Monic ∧ Irreducible (φ s)) ∧836      Function.Injective φ ∧ (∀ s, chartSlope R t x ∈ P s ↔ φ s = Polynomial.X) ∧837      (∀ s, Module.length R (BlowupChart R t x ⧸ P s) = ((φ s).natDegree : ℕ∞)) ∧838      (∀ s, Module.length (CompletedLocalAt (BlowupChart R t x) (P s))839        (CompletedLocalAt (BlowupChart R t x) (P s) ⧸840          finiteLocalCurveIdeal (BlowupChart R t x) (P s) (chartBase R t x t) (g s) 1) =841        (m s : ℕ∞)) ∧842      ((⨅ s, contractedLocalCurveIdeal (BlowupChart R t x) (P s) (chartBase R t x t) (g s) 1).map843        (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {∏ᶠ s, φ s ^ m s} := by844  subst hI845  choose φ hmon hirr hφ hslope hlen using fun s ↦846    blowup_chart_exceptional_point_polynomial R t x e he heZ (P s) (htP s)847  -- the exceptional ideal lies in each point and in each contracted ideal848  have hker_le (J : Ideal (BlowupChart R t x)) (hJ : chartBase R t x t ∈ J) :849      (J.map (Ideal.Quotient.mk (chartExceptional R t x))).comap850        (Ideal.Quotient.mk (chartExceptional R t x)) = J := by851    rw [Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective, ← RingHom.ker_eq_comap_bot,852      Ideal.mk_ker]853    refine sup_eq_left.mpr ?_854    unfold chartExceptional855    rw [Ideal.span_le]; simpa using hJ856  have hemap_inj (J J' : Ideal (BlowupChart R t x ⧸ chartExceptional R t x))857      (h : J.map e = J'.map e) : J = J' := by858    rw [← Ideal.comap_map_of_bijective e e.bijective (I := J),859      ← Ideal.comap_map_of_bijective e e.bijective (I := J'), h]860  have hinj : Function.Injective φ := fun s s' h ↦ hinjP <| by861    rw [← hker_le _ (htP s), ← hker_le _ (htP s'), hemap_inj _ _ ((hφ s).trans (h ▸ (hφ s').symm))]862  -- multiplicities863  have hpow : ∀ s, ∃ r : ℕ, ((contractedLocalCurveIdeal (BlowupChart R t x) (P s)864      (chartBase R t x t) (g s) 1).map (Ideal.Quotient.mk (chartExceptional R t x))).map e =865        Ideal.span {φ s ^ r} ∧866      Module.length (CompletedLocalAt (BlowupChart R t x) (P s))867        (CompletedLocalAt (BlowupChart R t x) (P s) ⧸868          finiteLocalCurveIdeal (BlowupChart R t x) (P s) (chartBase R t x t) (g s) 1) =869        (r : ℕ∞) := fun s => by870    obtain ⟨L, hL⟩ := hfin s871    obtain ⟨r, -, hr, hrlen⟩ := contracted_level_one_ideal_is_irreducible_power R t x e872      (P s) (φ s) (hφ s) (hirr s) (g s) L hL873    exact ⟨r, hr, hrlen⟩874  choose m hmult hm using hpow875  refine ⟨φ, m, fun s => ⟨hmon s, hirr s⟩, hinj, hslope, hlen, hm, ?_⟩876  set J : ι → Ideal (BlowupChart R t x) := fun s =>877    contractedLocalCurveIdeal (BlowupChart R t x) (P s) (chartBase R t x t) (g s) 1878  have hJt : ∀ s, chartBase R t x t ∈ J s := by879    intro s880    change completedPointMap (BlowupChart R t x) (P s) (chartBase R t x t) ∈881      finiteLocalCurveIdeal (BlowupChart R t x) (P s) (chartBase R t x t) (g s) 1882    unfold finiteLocalCurveIdeal883    exact Ideal.subset_span (by simp)884  have h1 : (⨅ s, J s).map (Ideal.Quotient.mk (chartExceptional R t x)) =885      ⨅ s, (J s).map (Ideal.Quotient.mk (chartExceptional R t x)) := by886    rw [show (⨅ s, J s) = ⨅ s, ((J s).map (Ideal.Quotient.mk (chartExceptional R t x))).comap887        (Ideal.Quotient.mk (chartExceptional R t x)) from888        iInf_congr (fun s => (hker_le _ (hJt s)).symm)]889    exact Ideal.map_iInf_comap_of_surjective _ Ideal.Quotient.mk_surjective _890  have h2 (K : ι → Ideal (BlowupChart R t x ⧸ chartExceptional R t x)) :891      (⨅ s, K s).map e = ⨅ s, (K s).map e := by892    rw [show (⨅ s, K s) = ⨅ s, ((K s).map e).comap e from893        iInf_congr (fun s => (Ideal.comap_map_of_bijective e e.bijective).symm)]894    exact Ideal.map_iInf_comap_of_surjective _ e.surjective _895  let _ : Fintype ι := Fintype.ofFinite _896  rw [h1, h2, iInf_congr hmult, finprod_eq_prod_of_fintype]897  let _ := Ideal.Quotient.field (Ideal.span ({t,x} : Set R))898  exact pairwise_distinct_irreducible_pow_iInf (R ⧸ Ideal.span ({t,x} : Set R)) ι φ hmon hirr hinj m899 900/-- The level-one left kernel, transported to `k[X]` along an identification of the exceptional901line, is generated by `∏ φₛ ^ multₛ` for distinct monic irreducibles `φₛ`, with `φ = X`902exactly at the zero-slope points. -/903theorem two_chart_left_level_one_kernel_polynomial (R : Type) [CommRing R] (t x : R)904    (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)905    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]906    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+*907      Polynomial (R ⧸ Ideal.span ({t,x} : Set R)))908    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x r)) =909      Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r))910    (heZ : e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x)) = Polynomial.X) :911    ∃ φ : D.ι ⊕ D.ι0 → Polynomial (R ⧸ Ideal.span ({t,x} : Set R)),912        (∀ s, (φ s).Monic ∧ Irreducible (φ s)) ∧ Function.Injective φ ∧913        (∀ i, φ (Sum.inl i) ≠ Polynomial.X) ∧ (∀ k, φ (Sum.inr k) = Polynomial.X) ∧914        (∀ s, (φ s).natDegree = leftResidueDegree D s) ∧ (∀ k, leftResidueDegree D (Sum.inr k) = 1)915        ∧ ((leftKernel D 1).map (Ideal.Quotient.mk (chartExceptional R t x))).map e =916        Ideal.span {∏ᶠ s, φ s ^ leftMultiplicity D s} := by917  obtain ⟨hmax, hinjP, htP⟩ := two_chart_left_points_maximal R t x beta D918  obtain ⟨φ, m, hφ, hinj, hslope, hlen, hm, hker⟩ := level_one_kernel_polynomial R t x _ rfl e he919    heZ (leftPoint D) hinjP htP (leftData D)920    (two_chart_left_data_transverse_finite R t x beta D 1).2921  have hmult : leftMultiplicity D = m := funext fun s => by922    unfold leftMultiplicity leftLevelIdeal; rw [hm s]; rfl923  have hdeg : ∀ s, (φ s).natDegree = leftResidueDegree D s := by924    intro s; unfold leftResidueDegree; rw [hlen s]; rfl925  have hX : ∀ k, φ (Sum.inr k) = Polynomial.X := fun k => (hslope (Sum.inr k)).1 (D.slope0 k)926  refine ⟨φ, hφ, hinj, fun i hi => ?_, hX, hdeg, fun k => ?_, by rw [hmult]; exact hker⟩927  · have hQ := D.onE i928    have := D.maximal i929    exact (overlap_exceptional_point_comap_maximal R t x (D.Q i) hQ).2.1 ((hslope (Sum.inl i)).2 hi)930  · rw [← hdeg, hX]; exact Polynomial.natDegree_X931 932private noncomputable def restrictLeftData {R : Type} [CommRing R] {t x : R}933    {beta : BlowupRestriction R t x}934    (D : TwoChartCurveData R t x beta) (p : D.ι → Prop) (q : D.ι0 → Prop) :935    TwoChartCurveData R t x beta where936  ι := {i // p i}937  fin := inferInstance938  Q := fun i => D.Q i.1939  maximal := fun i => D.maximal i.1940  inj := fun _ _ h => Subtype.ext (D.inj h)941  onE := fun i => D.onE i.1942  g := fun i => D.g i.1943  transverse := fun i => D.transverse i.1944  finite := fun i => D.finite i.1945  leftIso := fun i => D.leftIso i.1946  leftIso_compat := fun i => D.leftIso_compat i.1947  rightIso := fun i => D.rightIso i.1948  rightIso_compat := fun i => D.rightIso_compat i.1949  ι0 := {k // q k}950  fin0 := inferInstance951  P0 := fun k => D.P0 k.1952  maximal0 := fun k => D.maximal0 k.1953  inj0 := fun _ _ h => Subtype.ext (D.inj0 h)954  slope0 := fun k => D.slope0 k.1955  onE0 := fun k => D.onE0 k.1956  g0 := fun k => D.g0 k.1957  transverse0 := fun k => D.transverse0 k.1958  finite0 := fun k => D.finite0 k.1959  ιinf := D.ιinf960  fininf := D.fininf961  Pinf := D.Pinf962  maximalinf := D.maximalinf963  injinf := D.injinf964  slopeinf := D.slopeinf965  onEinf := D.onEinf966  ginf := D.ginf967  transverseinf := D.transverseinf968  finiteinf := D.finiteinf969 970private theorem leftKernel_le_restrictLeftData {R : Type} [CommRing R] {t x : R}971    {beta : BlowupRestriction R t x}972    (D : TwoChartCurveData R t x beta) (p : D.ι → Prop) (q : D.ι0 → Prop) :973    leftKernel D 1 ≤ leftKernel (restrictLeftData D p q) 1 := by974  unfold leftKernel finiteSupportKernel975  refine le_iInf ?_976  rintro (i | k)977  exacts [iInf_le _ (Sum.inl i.1), iInf_le _ (Sum.inr k.1)]978 979private theorem left_kernel_polynomial_residueField (O R : Type) [CommRing O] [IsDomain O]980    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]981    (S : SurfaceData O R) (beta : BlowupRestriction R S.t S.x) (D : TwoChartCurveData R S.t S.x982      beta) (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+*983      Polynomial (IsLocalRing.ResidueField R))984    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =985      Polynomial.C (IsLocalRing.residue R r))986    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)987    [IsNoetherianRing (BlowupChart R S.t S.x)] :988    ∃ ψ : D.ι ⊕ D.ι0 → Polynomial (IsLocalRing.ResidueField R),989        (∀ s, (ψ s).Monic ∧ Irreducible (ψ s)) ∧ (∀ s, (ψ s).natDegree = leftResidueDegree D s) ∧990      ((leftKernel D 1).map (Ideal.Quotient.mk (chartExceptional R S.t S.x))).map e =991          Ideal.span {∏ᶠ s, ψ s ^ leftMultiplicity D s} := by992  have : (Ideal.span ({S.t, S.x} : Set R)).IsMaximal := by993    rw [S.parameters]; exact IsLocalRing.maximalIdeal.isMaximal R994  let κ : (R ⧸ Ideal.span ({S.t, S.x} : Set R)) ≃+* IsLocalRing.ResidueField R :=995    Ideal.quotEquivOfEq S.parameters996  let e₀ := e.trans (Polynomial.mapEquiv κ).symm997  have he₀ : ∀ r : R, e₀ (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =998      Polynomial.C (Ideal.Quotient.mk (Ideal.span ({S.t,S.x} : Set R)) r) := by999    intro r1000    simp only [e₀, RingEquiv.trans_apply, he]1001    rw [Polynomial.mapEquiv_symm_apply, Polynomial.map_C]1002    congr 11003  have heZ₀ : e₀ (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) =1004      Polynomial.X := by1005    simp only [e₀, RingEquiv.trans_apply, heZ]1006    rw [Polynomial.mapEquiv_symm_apply, Polynomial.map_X]1007  obtain ⟨φ, hφ, -, -, -, hdeg, -, hK⟩ :=1008    two_chart_left_level_one_kernel_polynomial R S.t S.x beta D e₀ he₀ heZ₀1009  refine ⟨fun s => (φ s).map (κ : _ →+* _), fun s => ⟨(hφ s).1.map _, ?_⟩, fun s => ?_, ?_⟩1010  · exact (MulEquiv.irreducible_iff (Polynomial.mapEquiv κ).toMulEquiv).2 (hφ s).21011  · rw [Polynomial.natDegree_map_eq_of_injective κ.injective, hdeg]1012  · have hmap : ∀ I : Ideal (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x),1013        I.map e = (I.map e₀).map (Polynomial.mapEquiv κ) := by1014      intro I1015      rw [← Ideal.map_coe e, ← Ideal.map_coe e₀, ← Ideal.map_coe (Polynomial.mapEquiv κ),1016          Ideal.map_map]1017      congr 11018      exact RingHom.ext fun a => by1019        simp only [e₀, RingHom.coe_comp, Function.comp_apply, RingEquiv.coe_toRingHom,1020          RingEquiv.trans_apply, RingEquiv.apply_symm_apply]1021    rw [hmap, hK, Ideal.map_span, Set.image_singleton]1022    congr 21023    have : Fintype (D.ι ⊕ D.ι0) := Fintype.ofFinite _1024    rw [finprod_eq_prod_of_fintype, finprod_eq_prod_of_fintype, map_prod]1025    simp [Polynomial.mapEquiv_apply, Polynomial.map_pow]1026 1027private theorem pow_le_comap_completedPointMap (A : Type) [CommRing A] (P : Ideal A) [P.IsPrime]1028    (J : Ideal (CompletedLocalAt A P)) (L : ℕ)1029    (hL : ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map1030        (localCompletionMap (Localization.AtPrime P))) ^ L ≤ J) :1031    P^L ≤ J.comap (completedPointMap A P) := by1032  rw [← Ideal.map_le_iff_le_comap, Ideal.map_pow]1033  refine le_trans (le_of_eq ?_) hL1034  congr 11035  unfold completedPointMap1036  rw [← Ideal.map_map, Localization.AtPrime.map_eq_maximalIdeal]1037 1038/-- The image in `k[X]` of the level-one left kernel lies in `(ψ₀ ^ mult s₀)` whenever the left1039point `s₀` is the direction point of `ψ₀`; proved by restricting `D` to the point `s₀`. -/1040private theorem left_kernel_map_le_span_direction_pow (O R : Type) [CommRing O] [IsDomain O]1041    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]1042    (S : SurfaceData O R) (beta : BlowupRestriction R S.t S.x)1043    (D : TwoChartCurveData R S.t S.x beta)1044    (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+*1045      Polynomial (IsLocalRing.ResidueField R))1046    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =1047      Polynomial.C (IsLocalRing.residue R r))1048    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)1049    [IsNoetherianRing (BlowupChart R S.t S.x)] (s₀ : D.ι ⊕ D.ι0)1050    (ψ₀ : AffineDirection (IsLocalRing.ResidueField R))1051    (hP : leftPoint D s₀ = directionPoint R S.t S.x e ψ₀) :1052    ((leftKernel D 1).map (Ideal.Quotient.mk (chartExceptional R S.t S.x))).map e ≤1053      Ideal.span {ψ₀.val ^ leftMultiplicity D s₀} := by1054  have hmax : (Ideal.span ({S.t, S.x} : Set R)).IsMaximal := by1055    rw [S.parameters]; exact IsLocalRing.maximalIdeal.isMaximal R1056  set q := Ideal.Quotient.mk (chartExceptional R S.t S.x)1057  let D' := restrictLeftData D (fun i ↦ Sum.inl i = s₀) (fun j ↦ Sum.inr j = s₀)1058  have hsub : ∀ s s' : D'.ι ⊕ D'.ι0, s = s' := by1059    rintro (⟨i, hi⟩ | ⟨j, hj⟩) (⟨i', hi'⟩ | ⟨j', hj'⟩) <;>1060      first1061      | (cases hi.trans hi'.symm; rfl) | cases hi.trans hj'.symm1062      | cases hj.trans hi'.symm | (cases hj.trans hj'.symm; rfl)1063  obtain ⟨s₁, hm₁⟩ : ∃ s₁ : D'.ι ⊕ D'.ι0, leftMultiplicity D' s₁ = leftMultiplicity D s₀ := by1064    rcases s₀ with i | j1065    exacts [⟨.inl ⟨i, rfl⟩, rfl⟩, ⟨.inr ⟨j, rfl⟩, rfl⟩]1066  obtain ⟨ψ, hψ, -, hK'⟩ := left_kernel_polynomial_residueField O R S beta D' e he heZ1067  rw [finprod_eq_single _ s₁ (fun s hs ↦ absurd (hsub s s₁) hs), hm₁] at hK'1068  have hmono : ((leftKernel D 1).map q).map e ≤ ((leftKernel D' 1).map q).map e :=1069    Ideal.map_mono (Ideal.map_mono (leftKernel_le_restrictLeftData D _ _))1070  rcases Nat.eq_zero_or_pos (leftMultiplicity D s₀) with h0 | hpos1071  · rw [h0, pow_zero, Ideal.span_singleton_one]; exact le_top1072  obtain ⟨L, hL⟩ := (two_chart_left_data_transverse_finite R S.t S.x beta D 1).2 s₀1073  have hPL : (leftPoint D s₀)^L ≤ leftKernel D' 1 := by1074    unfold leftKernel finiteSupportKernel1075    have h := pow_le_comap_completedPointMap _ _ _ L hL1076    refine le_iInf fun s ↦ ?_1077    rcases s with ⟨i, rfl⟩ | ⟨j, rfl⟩ <;> exact h1078  have hmemP : ψ₀.val ∈ ((leftPoint D s₀).map q).map e := by1079    rw [hP, (direction_point_maximal O R S e he heZ ψ₀).2.2.2.1]; exact Ideal.subset_span rfl1080  have hsurj : Function.Surjective (fun a ↦ e (q a)) :=1081    e.surjective.comp Ideal.Quotient.mk_surjective1082  rw [← Ideal.map_coe e, Ideal.map_map] at hmemP1083  obtain ⟨a, ha, hae⟩ := (Ideal.mem_map_iff_of_surjective _ hsurj).1 hmemP1084  have h1 : Ideal.span {ψ₀.val ^ L} ≤ Ideal.span {ψ s₁ ^ leftMultiplicity D s₀} := by1085    rw [← hK', Ideal.span_singleton_le_iff_mem, ← hae, ← map_pow]1086    exact Ideal.mem_map_of_mem _ (Ideal.mem_map_of_mem _ (hPL (Ideal.pow_mem_pow ha L)))1087  rw [Ideal.span_singleton_le_span_singleton] at h11088  have h4 : ψ s₁ = ψ₀.val := Polynomial.eq_of_monic_of_associated (hψ s₁).1 ψ₀.2.11089    ((hψ s₁).2.associated_of_dvd ψ₀.2.21090      ((hψ s₁).2.prime.dvd_of_dvd_pow ((dvd_pow_self _ hpos.ne').trans h1)))1091  rw [← h4, ← hK']1092  exact hmono1093 1094/-- If a curve datum matches `Dv`, the level-one left kernel maps to the ideal of `k[X]` generated1095by the affine polynomial of `Dv`. -/1096theorem matches_divisor_level_one_polynomial (O R : Type) [CommRing O] [IsDomain O]1097    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]1098    (S : SurfaceData O R) (beta : BlowupRestriction R S.t S.x)1099    (D : TwoChartCurveData R S.t S.x beta) (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R))1100    (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+*1101      Polynomial (IsLocalRing.ResidueField R))1102    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =1103      Polynomial.C (IsLocalRing.residue R r))1104    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)1105    (hm : MatchesDivisor e D Dv) [IsNoetherianRing (BlowupChart R S.t S.x)] :1106    ((leftKernel D 1).map (Ideal.Quotient.mk (chartExceptional R S.t S.x))).map e =1107      Ideal.span {divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv} := by1108  classical1109  have hmax : (Ideal.span ({S.t, S.x} : Set R)).IsMaximal := by1110    rw [S.parameters]; exact IsLocalRing.maximalIdeal.isMaximal R1111  set k := IsLocalRing.ResidueField R1112  set q := Ideal.Quotient.mk (chartExceptional R S.t S.x)1113  have hdp := direction_point_maximal O R S e he heZ1114  have hQ {i : D.ι} {ψ : AffineDirection k} (hψ : ψ ≠ zeroAffine k)1115      (h : D.Q i = (directionPoint R S.t S.x e ψ).map1116        (algebraMap (BlowupChart R S.t S.x) (BlowupOverlap R S.t S.x))) :1117      leftPoint D (Sum.inl i) = directionPoint R S.t S.x e ψ := by1118    change (D.Q i).comap _ = _1119    rw [h]; exact (direction_point_overlap_maximal O R S e he heZ ψ hψ).2.21120  choose φ hφne hφQ hφDv using hm.common1121  -- the direction of each left point1122  let dir : D.ι ⊕ D.ι0 → AffineDirection k := Sum.elim φ (fun _ ↦ zeroAffine k)1123  have hdirP : ∀ s, leftPoint D s = directionPoint R S.t S.x e (dir s) := by1124    rintro (i | j)1125    exacts [hQ (hφne i) (hφQ i), (hm.zero j).1]1126  have hdirM : ∀ s, Dv (some (dir s)) = leftMultiplicity D s := by1127    rintro (i | j)1128    exacts [(hφDv i).trans (two_chart_common_multiplicity_eq R S.t S.x beta D i).1.symm,1129      (hm.zero j).2]1130  have hdirDeg (s) : (dir s).val.natDegree = leftResidueDegree D s := by1131    rw [leftResidueDegree, hdirP, (hdp (dir s)).2.2.2.2.1, ENat.toNat_natCast]1132  have hdirInj : Function.Injective dir := fun s s' h ↦1133    (two_chart_left_points_maximal R S.t S.x beta D).2.1 (by rw [hdirP, hdirP, h])1134  have hmonic_eq {p p' : AffineDirection k} (h : p.val ∣ p'.val) : p.val = p'.val :=1135    Polynomial.eq_of_monic_of_associated p.2.1 p'.2.1 (p.2.2.associated_of_dvd p'.2.2 h)1136  have hC (s₀) : ((leftKernel D 1).map q).map e ≤1137      Ideal.span {(dir s₀).val ^ leftMultiplicity D s₀} :=1138    left_kernel_map_le_span_direction_pow O R S beta D e he heZ s₀ _ (hdirP s₀)1139  have : Fintype (D.ι ⊕ D.ι0) := Fintype.ofFinite _1140  obtain ⟨ψ, hψ, hψdeg, hK⟩ := left_kernel_polynomial_residueField O R S beta D e he heZ1141  rw [finprod_eq_prod_of_fintype] at hK1142  -- `∏ dir s ^ mult s ∣ ∏ ψ s ^ mult s`, and both are monic of the same degree1143  have hdvd : (∏ s, (dir s).val ^ leftMultiplicity D s) ∣ ∏ s, ψ s ^ leftMultiplicity D s := by1144    refine Finset.prod_dvd_of_coprime (fun s _ s' _ hne ↦ IsCoprime.pow ?_) fun s _ ↦1145      Ideal.mem_span_singleton.1 (hC s (by rw [hK]; exact Ideal.subset_span rfl))1146    rw [Irreducible.coprime_iff_not_dvd (dir s).2.2]1147    exact fun hd ↦ hne (hdirInj (Subtype.ext (hmonic_eq hd)))1148  have hGP := Polynomial.eq_of_monic_of_dvd_of_natDegree_le1149    (Polynomial.monic_prod_of_monic _ _ fun s _ ↦ (dir s).2.1.pow _)1150    (Polynomial.monic_prod_of_monic _ _ fun s _ ↦ (hψ s).1.pow _) hdvd <| by1151      rw [Polynomial.natDegree_prod_of_monic _ _ fun s _ ↦ (hψ s).1.pow _,1152        Polynomial.natDegree_prod_of_monic _ _ fun s _ ↦ (dir s).2.1.pow _]1153      refine le_of_eq (Finset.sum_congr rfl fun s _ ↦ ?_)1154      rw [Polynomial.natDegree_pow, Polynomial.natDegree_pow, hψdeg, hdirDeg]1155  rw [hK, hGP]1156  refine congrArg (fun p ↦ Ideal.span {p}) ?_1157  unfold divisorAffinePolynomial1158  -- finally, the support of `Dv` consists of `∞` and the directions of the left points1159  have hsub : Dv.support ⊆ insert none (Finset.univ.image (fun s ↦ some (dir s))) := by1160    rintro (_ | ψ0) hP1161    · exact Finset.mem_insert_self _ _1162    rw [Finsupp.mem_support_iff] at hP1163    refine Finset.mem_insert_of_mem (Finset.mem_image.2 ?_)1164    by_cases hz : ψ0 = zeroAffine k1165    · subst hz1166      obtain ⟨j⟩ := hm.zero_surj (Nat.pos_of_ne_zero hP)1167      exact ⟨Sum.inr j, Finset.mem_univ _, rfl⟩1168    · obtain ⟨i, hi⟩ := hm.common_surj ψ0 hz (Nat.pos_of_ne_zero hP)1169      exact ⟨Sum.inl i, Finset.mem_univ _,1170        congrArg some ((hdp ψ0).2.2.2.2.2 ((hdirP _).symm.trans (hQ hz hi)))⟩1171  symm1172  rw [Finsupp.prod_of_support_subset Dv hsub _ (by rintro (_ | ψ0) _ <;> simp),1173    Finset.prod_insert (by simp),1174    Finset.prod_image (fun a _ b _ h ↦ hdirInj (Option.some_injective _ h))]1175  simp only [one_mul]1176  exact Finset.prod_congr rfl fun s _ ↦ by rw [hdirM]1177 1178/-- The common computation behind `global_function_has_tangent_divisor`: the glued function is1179`f = ∑ cᵢ tᵈ⁻ⁱ xⁱ` with residue form `P · a`, where `P` is the (monic) affine polynomial of `Dv`1180and `a ≠ 0`. -/1181private theorem glued_level_one_data (O R : Type) [CommRing O] [IsDomain O]1182    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]1183    (S : SurfaceData O R) (beta : BlowupRestriction R S.t S.x)1184    (D : TwoChartCurveData R S.t S.x beta) (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R))1185    (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+*1186      Polynomial (IsLocalRing.ResidueField R))1187    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =1188      Polynomial.C (IsLocalRing.residue R r))1189    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)1190    (hm : MatchesDivisor e D Dv) [IsNoetherianRing (BlowupChart R S.t S.x)]1191    [IsNoetherianRing (BlowupChart R S.x S.t)] (hreg : RegularParameterPair R S.t S.x)1192    (hregSwap : RegularParameterPair R S.x S.t) (f : R)1193    (G : GluedGenerators R S.t S.x beta (curveDataDegree D))1194    (hf : ∀ j : ℕ, surfaceToCechInput R S.t S.x j f =1195      (cechInputLattice R S.t S.x j).mkQ (gluedFunctionPair R S.t S.x G j))1196    (hG : ∀ j : ℕ,1197      Ideal.span {Ideal.Quotient.mk ((chartExceptional R S.t S.x)^j) (G.left j)} =1198        leftLevelKernel D j ∧1199      Ideal.span {Ideal.Quotient.mk ((chartExceptional R S.x S.t)^j) (G.right j)} =1200        rightLevelKernel D j) :1201    ∃ (c : Fin (curveDataDegree D+1) → R) (a : IsLocalRing.ResidueField R),1202      f = ∑ i : Fin (curveDataDegree D+1), c i * S.t^(curveDataDegree D - i.val) * S.x^i.val ∧1203      a ≠ 0 ∧ (divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv).Monic ∧1204      (divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv).natDegree + Dv none =1205        curveDataDegree D ∧1206      ∀ i : Fin (curveDataDegree D+1),1207        (divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv * Polynomial.C a).coeff i.val =1208          IsLocalRing.residue R (c i) := by1209  classical1210  obtain ⟨c, hfc, hGc, -⟩ := glued_function_initial_form R S.t S.x beta _ G hreg hregSwap f hf1211  set k := IsLocalRing.ResidueField R1212  set H : Polynomial k := ∑ i : Fin (curveDataDegree D+1),1213    Polynomial.C (IsLocalRing.residue R (c i)) * Polynomial.X ^ i.val with hHdef1214  set P := divisorAffinePolynomial k Dv with hPdef1215  -- `e` maps the class of `G.left 1` to `H`, which therefore generates the same ideal as `P`1216  have hal (r : R) : algebraMap R (BlowupChart R S.t S.x) r = chartBase R S.t S.x r := rfl1217  have heG : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (G.left 1)) = H := by1218    rw [Ideal.Quotient.eq.mpr hGc, map_sum, map_sum]1219    exact Finset.sum_congr rfl fun i _ ↦ by rw [map_mul, map_mul, map_pow, map_pow, hal, he, heZ]1220  have hspan : Ideal.span {H} = Ideal.span {P} := by1221    have hle : (chartExceptional R S.t S.x) ^ 1 ≤ chartExceptional R S.t S.x := by rw [pow_one]1222    have h2 := congrArg (fun I ↦ (I.map (Ideal.Quotient.factor hle)).map e) (hG 1).11223    rw [Ideal.map_span, Set.image_singleton, Ideal.map_span, Set.image_singleton] at h21224    have hψ : Ideal.Quotient.factor hle (Ideal.Quotient.mk _ (G.left 1)) =1225        Ideal.Quotient.mk (chartExceptional R S.t S.x) (G.left 1) := rfl1226    rw [hψ, heG] at h21227    rw [h2, ← matches_divisor_level_one_polynomial O R S beta D Dv e he heZ hm]1228    congr 11229    unfold leftLevelKernel finiteSupportLevelKernel1230    exact Ideal.map_map _ _1231  -- `P = ∏ g Q ^ Dv Q` is monic of degree `deg Dv - Dv ∞`1232  set g : ClosedDirection k → ℕ → Polynomial k := fun Q r ↦ Option.elim Q 1 (fun phi ↦ phi.val ^ r)1233  have hPprod : P = ∏ Q ∈ Dv.support, g Q (Dv Q) := by1234    rw [hPdef, divisorAffinePolynomial, Finsupp.prod]1235    exact Finset.prod_congr rfl fun Q _ ↦ by cases Q <;> rfl1236  have hterm (Q : ClosedDirection k) (r : ℕ) : (g Q r).Monic ∧1237      directionDegree k Q * r = (g Q r).natDegree + (if Q = none then r else 0) := by1238    cases Q with1239    | none => simp [g, directionDegree]1240    | some phi =>1241      exact ⟨phi.2.1.pow r, by simp [g, directionDegree, phi.2.1.natDegree_pow, mul_comm]⟩1242  have hPmon : P.Monic := hPprod ▸ Polynomial.monic_prod_of_monic _ _ fun Q _ ↦ (hterm Q _).11243  have hPdeg : P.natDegree + Dv none = exceptionalDegree k Dv := by1244    rw [hPprod, exceptionalDegree, Finsupp.sum,1245      Polynomial.natDegree_prod_of_monic (h := fun Q _ ↦ (hterm Q (Dv Q)).1),1246      Finset.sum_congr rfl fun Q _ ↦ (hterm Q (Dv Q)).2, Finset.sum_add_distrib, Finset.sum_ite_eq']1247    split_ifs with h1248    · rfl1249    · rw [Finsupp.notMem_support_iff.mp h]1250  -- hence `H = P * C a` with `a ≠ 0`1251  obtain ⟨u, hu⟩ := Ideal.span_singleton_eq_span_singleton.mp hspan.symm1252  obtain ⟨a, ha, hau⟩ := Polynomial.isUnit_iff.mp u.isUnit1253  have hHP : H = P * Polynomial.C a := by rw [← hu, hau]1254  refine ⟨c, a, hfc, ha.ne_zero, hPmon,1255    hPdeg.trans (matches_divisor_degree O R S beta D Dv e he heZ hm), fun i ↦ ?_⟩1256  rw [← hHP, hHdef, Polynomial.finsetSum_coeff, Finset.sum_eq_single i (fun b _ hb ↦ ?_) (by simp)]1257  · simp1258  · rw [Polynomial.coeff_C_mul_X_pow, if_neg fun h ↦ hb (Fin.ext h.symm)]1259 1260/-- A global function glued from the generators of a curve datum matching `Dv` has tangent1261divisor `Dv` in degree `deg D`. -/1262theorem global_function_has_tangent_divisor (O R : Type) [CommRing O] [IsDomain O]1263    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]1264    (S : SurfaceData O R) (beta : BlowupRestriction R S.t S.x)1265    (D : TwoChartCurveData R S.t S.x beta) (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R))1266    (e : (BlowupChart R S.t S.x ⧸ chartExceptional R S.t S.x) ≃+*1267      Polynomial (IsLocalRing.ResidueField R))1268    (he : ∀ r : R, e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartBase R S.t S.x r)) =1269      Polynomial.C (IsLocalRing.residue R r))1270    (heZ : e (Ideal.Quotient.mk (chartExceptional R S.t S.x) (chartSlope R S.t S.x)) = Polynomial.X)1271    (hm : MatchesDivisor e D Dv) [IsNoetherianRing (BlowupChart R S.t S.x)]1272    [IsNoetherianRing (BlowupChart R S.x S.t)] (hreg : RegularParameterPair R S.t S.x)1273    (hregSwap : RegularParameterPair R S.x S.t) (f : R)1274    (G : GluedGenerators R S.t S.x beta (curveDataDegree D))1275    (hf : ∀ j : ℕ, surfaceToCechInput R S.t S.x j f =1276      (cechInputLattice R S.t S.x j).mkQ (gluedFunctionPair R S.t S.x G j))1277    (hG : ∀ j : ℕ,1278      Ideal.span {Ideal.Quotient.mk ((chartExceptional R S.t S.x)^j) (G.left j)} =1279        leftLevelKernel D j ∧1280      Ideal.span {Ideal.Quotient.mk ((chartExceptional R S.x S.t)^j) (G.right j)} =1281        rightLevelKernel D j) :1282    HasTangentDivisor O R S (Ideal.span {f}) (curveDataDegree D) Dv := by1283  obtain ⟨c, a, hfc, ha0, hPmon, hPdeg, hcoeff⟩ :=1284    glued_level_one_data O R S beta D Dv e he heZ hm hreg hregSwap f G hf hG1285  set P := divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv1286  have hnd : (P * Polynomial.C a).natDegree = P.natDegree := Polynomial.natDegree_mul_C ha01287  refine ⟨f, P * Polynomial.C a, rfl, ⟨?_, ?_, ?_, ?_⟩, ?_⟩1288  · exact mul_ne_zero hPmon.ne_zero (Polynomial.C_ne_zero.2 ha0)1289  · rw [hnd]; omega1290  · rw [hnd]; omega1291  · rw [Polynomial.leadingCoeff_mul, hPmon.leadingCoeff, Polynomial.leadingCoeff_C,1292      one_mul, mul_comm]1293  · rw [hfc]1294    unfold tangentLift1295    apply initial_form_lift_independent1296    intro i1297    rw [hcoeff i, ← IsLocalRing.residue_eq_zero_iff, map_sub, sub_eq_zero]1298    unfold residueRepresentative1299    exact (Function.invFun_eq (IsLocalRing.residue_surjective _)).symm1300 1301private theorem span_sup_eq_top_of_isUnit_coeff {R B C : Type} [CommRing R] [CommRing B]1302    [CommRing C] [Algebra R B] (φ : B →+* C) (w : B)1303    (d : ℕ) (c : Fin (d + 1) → R) (n : Fin (d + 1) → ℕ) (j : Fin (d + 1)) (hj : IsUnit (c j))1304        (hnj : n j = 0)1305    (hn : ∀ i, i ≠ j → n i ≠ 0) :1306    Ideal.span {φ (∑ i : Fin (d+1), algebraMap R B (c i) * w^(n i))} ⊔ Ideal.span {φ w} = ⊤ := by1307  set J := Ideal.span {φ (∑ i : Fin (d+1), algebraMap R B (c i) * w^(n i))} ⊔ Ideal.span {φ w}1308  have hw : Ideal.Quotient.mk J (φ w) = 0 :=1309    Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_sup_right (Ideal.subset_span rfl))1310  have hF : Ideal.Quotient.mk J (φ (∑ i : Fin (d+1), algebraMap R B (c i) * w^(n i))) = 0 :=1311    Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_sup_left (Ideal.subset_span rfl))1312  have hF' : Ideal.Quotient.mk J (φ (∑ i : Fin (d+1), algebraMap R B (c i) * w^(n i))) =1313      Ideal.Quotient.mk J (φ (algebraMap R B (c j))) := by1314    simp only [map_sum, map_mul, map_pow, hw]1315    rw [Finset.sum_eq_single j]1316    · rw [hnj, pow_zero, mul_one]1317    · intro i _ hi1318      rw [zero_pow (hn i hi), mul_zero]1319    · intro h; exact absurd (Finset.mem_univ j) h1320  rw [hF] at hF'1321  have hmem : φ (algebraMap R B (c j)) ∈ J := Ideal.Quotient.eq_zero_iff_mem.mp hF'.symm1322  exact Ideal.eq_top_of_isUnit_mem _ hmem ((hj.map (algebraMap R B)).map φ)1323 1324/-- If the residues of `c₀, …, c_n` are the coefficients of `P · κ` (`κ ≠ 0`), where `P` is the1325monic affine polynomial of `Dv` and `deg P + Dv ∞ = n`, then `c_n` is a unit when `Dv` avoids1326`∞`, and `c₀` is a unit when `Dv` avoids the zero direction. -/1327private theorem isUnit_coeffs_of_residue_eq {R : Type} [CommRing R] [IsLocalRing R]1328    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R)) {n : ℕ} (c : Fin (n + 1) → R)1329    (κ : IsLocalRing.ResidueField R) (hκ : κ ≠ 0)1330    (hPmon : (divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv).Monic)1331    (hPdeg : (divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv).natDegree + Dv none = n)1332    (hcoeff : ∀ i : Fin (n + 1), (divisorAffinePolynomial (IsLocalRing.ResidueField R) Dv *1333      Polynomial.C κ).coeff i.val = IsLocalRing.residue R (c i)) :1334    (Dv none = 0 → IsUnit (c (Fin.last n))) ∧1335      (Dv (zeroDirection (IsLocalRing.ResidueField R)) = 0 → IsUnit (c 0)) := by1336  refine ⟨fun h0 ↦ ?_, fun h0 ↦ ?_⟩ <;>1337    rw [← IsLocalRing.notMem_maximalIdeal, ← IsLocalRing.residue_eq_zero_iff, ← hcoeff,1338      Polynomial.coeff_mul_C]1339  · rw [Fin.val_last, ← hPdeg, h0, add_zero, ← Polynomial.leadingCoeff, hPmon.leadingCoeff,1340      one_mul]1341    exact hκ1342  · refine mul_ne_zero (fun hP ↦ ?_) hκ1343    rw [Fin.val_zero, ← Polynomial.X_dvd_iff] at hP1344    exact (Nat.pos_iff_ne_zero.mp ((count_normalizedFactors_divisorAffinePolynomial _ Dv 11345      one_ne_zero (zeroAffine _)).2.mp hP)) h01346 1347/-- A global function glued from a curve datum matching `Dv`, whose strict transforms are the1348prescribed child ideals, generates an ideal of the fixed tangent cell. -/1349theorem global_function_mem_cell (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]1350    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)1351    (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)1352    [IsDomain (ConcreteSurface O pi u a b)] [IsRegularLocalRing (ConcreteSurface O pi u a b)]1353    (S : SurfaceData O (ConcreteSurface O pi u a b))1354    (hS : S.t = surfaceT O pi u a b ∧ S.x = surfaceX O pi u a b ∧ S.a = a ∧ S.b = b)1355    (e : (tChart O pi u a b ⧸ tExc O pi u a b) ≃+*1356      Polynomial (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))1357    (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)1358      (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))1359    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)1360    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))1361    (hinf : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1362      (surfaceX O pi u a b)).IsPrime) (s : State) (d : ℕ) (hd : 0 < d)1363    (hs : (∃ c : ℕ, s = State.single a c ∧ b = 0) ∨ (∃ c h : ℕ, s = State.crossing a b c h ∧ 0 < b))1364    (hdc : d ≤ stateContactT s) (hdh : ∀ h : ℕ, stateContactX s = some h → d ≤ h)1365    (hDinf : 0 < Dv none ↔ d < stateContactT s)1366    (hDzero : ∀ h : ℕ, stateContactX s = some h →1367      (0 < Dv (zeroDirection (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) ↔ d < h))1368    (beta : BlowupRestriction (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1369      (surfaceX O pi u a b))1370    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)1371      beta)1372    (hm : MatchesDivisor e D Dv) (hdD : curveDataDegree D = d) (f : ConcreteSurface O pi u a b)1373    (G : GluedGenerators (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)1374      beta d)1375    (hf : ∀ j : ℕ, surfaceToCechInput (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1376      (surfaceX O pi u a b) j f = (cechInputLattice (ConcreteSurface O pi u a b)1377        (surfaceT O pi u a b) (surfaceX O pi u a b) j).mkQ (gluedFunctionPair1378          (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b) G j))1379    (hG : ∀ j : ℕ,1380      Ideal.span {Ideal.Quotient.mk (tExc O pi u a b^j) (G.left j)} = leftLevelKernel D j ∧1381      Ideal.span {Ideal.Quotient.mk (xExc O pi u a b^j) (G.right j)} = rightLevelKernel D j)1382    (I : ∀ Q : divisorSupport Dv, Ideal (divisorLocalRing (ConcreteSurface O pi u a b)1383      (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf Q))1384    (hI : ∀ Q : divisorSupport Dv, I Q ∈ childIdealSet (ConcreteSurface O pi u a b)1385      (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf s d Q)1386    (hIf : ∀ Q : divisorSupport Dv, divisorStrictTransform (ConcreteSurface O pi u a b)1387      (surfaceT O pi u a b) (surfaceX O pi u a b) e Dv hinf d (Ideal.span {f}) Q = I Q) :1388    Ideal.span {f} ∈ (fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv) := by1389  classical1390  have hreg := concrete_surface_regular_pair_tx O pi hpi.ne_zero u a b ha1391  have hregSwap := concrete_surface_regular_pair_xt O pi hpi.ne_zero u a b ha1392  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)1393      (surfaceX O pi u a b)1394  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)1395      (surfaceT O pi u a b)1396  obtain ⟨ht, hx, hA, hB⟩ := hS1397  rcases S with ⟨pi', hpi', t0, x0, un, a0, b0, ha0, hpar, hdim, hcomp, hinj, rE, rC, hvert⟩1398  dsimp only at ht hx hA hB1399  subst t0 x0 a0 b0 hdD1400  set S' : SurfaceData O (ConcreteSurface O pi u a b) :=1401    ⟨pi', hpi', _, _, un, a, b, ha0, hpar, hdim, hcomp, hinj, rE, rC, hvert⟩1402  -- the coefficients of `f` at `x^d` and `t^d` are units when `Dv` avoids `∞`, resp. `0`1403  obtain ⟨c, κ, hfc, hκ, hPmon, hPdeg, hcoeff⟩ :=1404    glued_level_one_data O _ S' beta D Dv e he heZ hm hreg hregSwap f G hf hG1405  obtain ⟨hcT, hcX⟩ := isUnit_coeffs_of_residue_eq Dv c κ hκ hPmon hPdeg hcoeff1406  refine ⟨⟨⟨f, rfl⟩, ?_⟩, global_function_has_tangent_divisor O _ S' beta D Dv e he heZ hm hreg1407    hregSwap f G hf hG⟩1408  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set1409      (ConcreteSurface O pi u a b))).IsMaximal := hpar ▸ IsLocalRing.maximalIdeal.isMaximal _1410  obtain ⟨hdir, -, hdz⟩ := directionPoint_properties (ConcreteSurface O pi u a b) _ _ e he heZ1411  obtain ⟨hP0max, hP0t, -, -⟩ := hdir (zeroAffine _)1412  obtain ⟨hinfmax, hxinf, hWinf, -⟩ := infinity_point_maximal O _ S'1413  have : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1414      (surfaceX O pi u a b)).IsMaximal := hinfmax1415  obtain ⟨hstA, hstB⟩ := concrete_strict_transform_generators O pi hpi u a b ha _ f c hfc _ hP0t1416    (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) hxinf1417      hWinf1418  -- the contact orders of `f` with `t = 0` and `x = 0`1419  have htc : Module.length (ConcreteSurface O pi u a b) (ConcreteSurface O pi u a b ⧸1420      (Ideal.span {f} ⊔ Ideal.span {surfaceT O pi u a b})) = stateContactT s := by1421    rw [concrete_infinity_boundary_contact O pi hpi u a b ha _ f c hfc1422        (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))1423      hxinf hWinf]1424    by_cases hpos : 0 < Dv none1425    · have h1 := (hI ⟨none, hpos⟩).2.2.1 rfl1426      rw [← hIf ⟨none, hpos⟩] at h11427      rw [← hstB]1428      exact (congrArg ((curveDataDegree D : ℕ∞) + ·) h1).trans1429        (by rw [← Nat.cast_add, Nat.add_sub_cancel' hdc])1430    · have hcd : stateContactT s = curveDataDegree D := by have := hDinf.not.mp hpos; omega1431      rw [span_sup_eq_top_of_isUnit_coeff _ _ _ c (fun i ↦ curveDataDegree D - i.val) (Fin.last _)1432        (hcT (by omega)) (by simp) (fun i hi ↦ by have := Fin.val_lt_last hi; omega),1433        Module.length_eq_zero, add_zero, hcd]1434  have hxc (h' : ℕ) (hsx : stateContactX s = some h') (hb : 0 < b) :1435      Module.length (ConcreteSurface O pi u a b) (ConcreteSurface O pi u a b ⧸1436          (Ideal.span {f} ⊔ Ideal.span {surfaceX O pi u a b})) = h' := by1437    rw [concrete_zero_boundary_contact O pi hpi u a b ha hb _ f c hfc1438      (directionPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b) e1439          (zeroAffine _)) hdz]1440    by_cases hpos : 0 < Dv (zeroDirection (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))1441    · have h1 := (hI ⟨_, hpos⟩).2.2.2 rfl h' hsx1442      rw [← hIf ⟨_, hpos⟩] at h11443      rw [← hstA]1444      exact (congrArg ((curveDataDegree D : ℕ∞) + ·) h1).trans1445        (by rw [← Nat.cast_add, Nat.add_sub_cancel' (hdh h' hsx)])1446    · have h0 : Dv (zeroDirection (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) = 0 := by1447        omega1448      have hcd : h' = curveDataDegree D := by1449        have := hdh h' hsx; have := (hDzero h' hsx).not.mp hpos; omega1450      rw [span_sup_eq_top_of_isUnit_coeff _ _ _ c (fun i ↦ i.val) 0 (hcX h0) (by simp)1451        (fun i hi h ↦ hi (Fin.ext h)), Module.length_eq_zero, add_zero, hcd]1452  rcases hs with ⟨c', rfl, hb0⟩ | ⟨c', h', rfl, hb⟩1453  · have hdc' : curveDataDegree D ≤ c' := hdc1454    exact ⟨⟨ha, by omega⟩, rfl, hb0, htc⟩1455  · have hdc' : curveDataDegree D ≤ c' := hdc1456    have hdh' := hdh h' rfl1457    exact ⟨⟨ha, hb, by omega, by omega⟩, rfl, rfl, htc, hxc h' rfl hb⟩1458 1459end SurfaceBlowup