Blow-up charts, the exceptional line, and 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.Directions7import SurfaceBlowup.Measure.AdicTransport8import SurfaceBlowup.Surfaces.Lengths9import SurfaceBlowup.Unramified.Extension10 11/-!12# Blow-up charts, the exceptional line, and curve data13 14For a commutative ring `R` and elements `t, x`, the blow-up of `(t, x)` is covered by the `t`-chart15`R[X]/(tX − x)` and the `x`-chart `R[W]/(xW − t)`, glued along the overlap where the slope is16invertible. This file sets up these charts together with their infinitesimal levels, the two-chart17Čech complex and its tower of levels, completed local rings at points, the local data of a curve18on the two charts (multiplicities, degree, curve orders and their limit, the child order), and the19colon strict transforms used to define child ideal sets.20It then proves the basic structural facts about these objects. Closed points and divisors on the21exceptional line `ℙ¹_k` are in `Blowup/Directions.lean`, and the adic congruence rules in22`Measure/AdicTransport.lean`.23 24## Main results25 26* `blowup_chart_universal`, `blowup_chart_ringHom_ext`: universal property of a chart.27* `blowup_exceptional_parameter_regular`: `t` is a nonzerodivisor on the `t`-chart when `(t, x)`28  is a regular sequence.29* `boundary_chart_quotient_equiv`: the `x`-chart modulo its slope is `R/(t)`.30* `actual_cech_preserves_exceptional_lattices`, `actual_cech_reductions_surjective`: the Čech31  differential respects the exceptional filtrations, whose reduction maps are surjective.32* `coordinate_coset_representatives_exist`, `coefficient_space_strict_instances`: adic33  congruences on coordinate spaces.34* `concrete_surface_special_fiber_length_transport`: lengths modulo `π` computed on the special35  fibre.36 37Provenance: `Def_SurfaceBlowupV2_{BlowupCharts, CompletedLocalPoints, FiniteBlowupCharts,38ActualCechLevels, ActualCechThreads, FiniteSupport, GluedGenerators, CurveSections,39PrincipalPowerLayers, StrictChartCoordinates, StrictNormalization, StrictPullback, SurfaceSections,40TangentCells, TwoChartCurveData, CurveDataDegree, CurveOrderLimit, ChildOrder, DivisorPoints,41ChildIdealSets}`; `Thm_SurfaceBlowupV2_{actual_cech_differentials_commute_with_reduction,42actual_cech_reductions_surjective, blowup_chart_relation,43actual_cech_preserves_exceptional_lattices, blowup_chart_ringHom_ext, blowup_chart_universal,44blowup_exceptional_parameter_regular, boundary_chart_quotient_equiv, child_coordinate_map_scaled,45coefficient_space_strict_instances, completed_point_power_contraction,46concrete_surface_special_fiber_length_transport, contracted_ideal_map_localization_top,47coordinate_coset_representatives_exist}`.48-/49 50noncomputable section51 52namespace SurfaceBlowup53 54/-! ### The two charts of a blow-up -/55 56section57variable (R : Type) [CommRing R]58/-- The relation `t·X − x` cutting out the `t`-chart of the blow-up of `(t, x)`. -/59def blowupRelation (t x : R) : Polynomial R := Polynomial.C t * Polynomial.X - Polynomial.C x60/-- The `t`-chart `R[X]/(tX − x)` of the blow-up of `R` at the ideal `(t, x)`. -/61abbrev BlowupChart (t x : R) := Polynomial R ⧸ Ideal.span {blowupRelation R t x}62/-- The structure map `R → R[X]/(tX − x)`. -/63def chartBase (t x : R) : R →+* BlowupChart R t x :=64  (Ideal.Quotient.mk (Ideal.span {blowupRelation R t x})).comp Polynomial.C65/-- The slope coordinate `X = x/t` on the `t`-chart. -/66def chartSlope (t x : R) : BlowupChart R t x :=67  Ideal.Quotient.mk (Ideal.span {blowupRelation R t x}) Polynomial.X68/-- The exceptional ideal `(t)` of the `t`-chart. -/69def chartExceptional (t x : R) : Ideal (BlowupChart R t x) :=70  Ideal.span {chartBase R t x t}71/-- The overlap of the two charts: the `t`-chart with its slope inverted. -/72abbrev BlowupOverlap (t x : R) := Localization.Away (chartSlope R t x)73end74 75/-! ### Completed local rings at points -/76 77section78section Completion79variable (A : Type) [CommRing A] [IsLocalRing A]80/-- The completion of a local ring at its maximal ideal. -/81abbrev LocalCompletion := AdicCompletion (IsLocalRing.maximalIdeal A) A82/-- The canonical map from a local ring to its completion. -/83def localCompletionMap : A →+* LocalCompletion A :=84  by exact @algebraMap A (LocalCompletion A) inferInstance inferInstance inferInstance85end Completion86section Point87variable (A : Type) [CommRing A] (P : Ideal A) [P.IsPrime]88/-- The completed local ring of `A` at the prime `P`. -/89abbrev CompletedLocalAt := LocalCompletion (Localization.AtPrime P)90/-- The canonical map `A → (A_P)^`. -/91def completedPointMap : A →+* CompletedLocalAt A P :=92  (localCompletionMap (Localization.AtPrime P)).comp (algebraMap A (Localization.AtPrime P))93/-- The ideal `(g, e^j)` of the completed local ring at `P`. -/94def finiteLocalCurveIdeal (e : A) (g : CompletedLocalAt A P) (j : ℕ) :95    Ideal (CompletedLocalAt A P) :=96  Ideal.span {g, (completedPointMap A P e)^j}97/-- The contraction to `A` of the ideal `(g, e^j)` of the completed local ring at `P`. -/98def contractedLocalCurveIdeal (e : A) (g : CompletedLocalAt A P) (j : ℕ) : Ideal A :=99  (finiteLocalCurveIdeal A P e g j).comap (completedPointMap A P)100/-- The local equation `g` at `P` is transverse to `e`: multiplication by `e` is injective101modulo `g`. -/102abbrev LocallyTransverse (e : A) (g : CompletedLocalAt A P) : Prop :=103  Function.Injective (fun a : CompletedLocalAt A P ⧸ Ideal.span {g} =>104    Ideal.Quotient.mk (Ideal.span {g}) (completedPointMap A P e) * a)105/-- The local equation `g` at `P` has finite contact with `e`: the ideal `(g, e)` contains a power106of the maximal ideal. -/107abbrev FiniteContact (e : A) (g : CompletedLocalAt A P) : Prop :=108  ∃ L : ℕ, ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map109    (localCompletionMap (Localization.AtPrime P)))^L ≤ finiteLocalCurveIdeal A P e g 1110end Point111end112 113/-! ### Infinitesimal levels of the charts; the ring Čech differential -/114 115section116section FiniteCharts117variable (R : Type) [CommRing R]118/-- The ideal `(t^j)` of the `t`-chart. -/119def exceptionalLevelIdeal (t x : R) (j : ℕ) : Ideal (BlowupChart R t x) :=120  Ideal.span {(chartBase R t x t)^j}121/-- The `j`-th infinitesimal level `A/(t^j)` of the `t`-chart. -/122abbrev ExceptionalChartLevel (t x : R) (j : ℕ) :=123  BlowupChart R t x ⧸ exceptionalLevelIdeal R t x j124/-- The structure map `R → A/(t^j)` of the `j`-th level of the `t`-chart. -/125def levelBase (t x : R) (j : ℕ) : R →+* ExceptionalChartLevel R t x j :=126  (Ideal.Quotient.mk (exceptionalLevelIdeal R t x j)).comp (chartBase R t x)127/-- The slope coordinate on the `j`-th level of the `t`-chart. -/128def levelSlope (t x : R) (j : ℕ) : ExceptionalChartLevel R t x j :=129  Ideal.Quotient.mk (exceptionalLevelIdeal R t x j) (chartSlope R t x)130/-- The `j`-th level of the overlap: the `j`-th chart level with its slope inverted. -/131abbrev ExceptionalOverlapLevel (t x : R) (j : ℕ) :=132  Localization.Away (levelSlope R t x j)133/-- The localization map from the `j`-th chart level to the `j`-th overlap level. -/134def levelOverlapMap (t x : R) (j : ℕ) :135    ExceptionalChartLevel R t x j →+* ExceptionalOverlapLevel R t x j :=136  by exact @algebraMap (ExceptionalChartLevel R t x j) (ExceptionalOverlapLevel R t x j)137      inferInstance inferInstance inferInstance138end FiniteCharts139section Complex140variable {O U V W : Type} [CommRing O] [CommRing U] [CommRing V] [CommRing W]141  [Algebra O U] [Algebra O V] [Algebra O W]142/-- The two-chart Čech differential `(u, v) ↦ left u − transition · right v`. -/143def ringCechDifferential (left : U →ₐ[O] W) (right : V →ₐ[O] W) (transition : W) :144    (U × V) →ₗ[O] W where145  toFun z := left z.1 - transition * right z.2146  map_add' := by147    intro z w148    simp only [Prod.fst_add, Prod.snd_add, map_add, mul_add]149    abel150  map_smul' := by151    intro c z152    simp [smul_sub]153end Complex154end155 156/-! ### Levels of the Čech complex -/157 158section159variable (R : Type) [CommRing R] (t x : R)160/-- A restriction map from the `x`-chart to the overlap, sending its slope to the inverse161of the slope of the `t`-chart. -/162structure BlowupRestriction where163  right : BlowupChart R x t →ₐ[R] BlowupOverlap R t x164  slope : right (chartSlope R x t) = IsLocalization.Away.invSelf (chartSlope R t x)165/-- The Čech differential of the two blow-up charts twisted by the `d`-th power of the166inverse slope. -/167def fullCechDifferential (beta : BlowupRestriction R t x) (d : ℕ) :168    (BlowupChart R t x × BlowupChart R x t) →ₗ[R] BlowupOverlap R t x :=169  ringCechDifferential (IsScalarTower.toAlgHom R (BlowupChart R t x) (BlowupOverlap R t x))170    beta.right ((IsLocalization.Away.invSelf (chartSlope R t x))^d)171/-- The lattice `(t^j) × (x^j)` in the product of the two charts. -/172def cechInputLattice (j : ℕ) : Submodule R (BlowupChart R t x × BlowupChart R x t) :=173  (((chartExceptional R t x)^j).restrictScalars R).prod174    (((chartExceptional R x t)^j).restrictScalars R)175/-- The lattice `(t^j)` in the overlap. -/176def cechOutputLattice (j : ℕ) : Submodule R (BlowupOverlap R t x) :=177  ((Ideal.span {algebraMap (BlowupChart R t x) (BlowupOverlap R t x)178      (chartBase R t x t)})^j).restrictScalars R179/-- The `j`-th level of the Čech source. -/180abbrev CechLevelInput (j : ℕ) :=181  (BlowupChart R t x × BlowupChart R x t) ⧸ cechInputLattice R t x j182/-- The `j`-th level of the Čech target. -/183abbrev CechLevelOutput (j : ℕ) :=184  BlowupOverlap R t x ⧸ cechOutputLattice R t x j185/-- The Čech differential induced on the `j`-th levels. -/186def finiteCechDifferential (beta : BlowupRestriction R t x) (d j : ℕ)187    (h : cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap188        (fullCechDifferential R t x beta d)) :189    CechLevelInput R t x j →ₗ[R] CechLevelOutput R t x j :=190  (cechInputLattice R t x j).mapQ (cechOutputLattice R t x j)191    (fullCechDifferential R t x beta d) h192/-- The reduction map from level `j + 1` to level `j` of the Čech source. -/193def cechInputReduction (j : ℕ) : CechLevelInput R t x (j+1) →ₗ[R] CechLevelInput R t x j :=194  (cechInputLattice R t x (j+1)).mapQ (cechInputLattice R t x j) LinearMap.id (by195    rintro z hz196    exact ⟨(Ideal.pow_le_pow_right (Nat.le_succ j)) hz.1,197      (Ideal.pow_le_pow_right (Nat.le_succ j)) hz.2⟩)198/-- The reduction map from level `j + 1` to level `j` of the Čech target. -/199def cechOutputReduction (j : ℕ) : CechLevelOutput R t x (j+1) →ₗ[R] CechLevelOutput R t x j :=200  (cechOutputLattice R t x (j+1)).mapQ (cechOutputLattice R t x j) LinearMap.id (by201    intro z hz202    exact (Ideal.pow_le_pow_right (Nat.le_succ j)) hz)203end204 205/-! ### Threads of the Čech complex -/206 207section208variable (R : Type) [CommRing R] (t x : R)209/-- Compatible threads in the tower of levels of the Čech source. -/210def CechInputThreads : Type :=211  towerThreads R (fun j => CechLevelInput R t x j) (cechInputReduction R t x)212/-- Additive group structure on Čech-source threads. -/213instance : AddCommGroup (CechInputThreads R t x) :=214  inferInstanceAs (AddCommGroup (towerThreads R (fun j => CechLevelInput R t x j)215      (cechInputReduction R t x)))216/-- `R`-module structure on Čech-source threads. -/217instance : Module R (CechInputThreads R t x) :=218  inferInstanceAs (Module R (towerThreads R (fun j => CechLevelInput R t x j)219      (cechInputReduction R t x)))220end221 222/-! ### Kernels of finitely supported local data -/223 224section225section FiniteSupport226variable (A : Type) [CommRing A] (ι : Type) (P : ι → Ideal A)227variable [∀ i, (P i).IsPrime]228variable (J : ∀ i, Ideal (CompletedLocalAt A (P i)))229/-- The kernel `⋂ᵢ J_i ∩ A` of the map from `A` to finitely many completed local230quotients. -/231def finiteSupportKernel : Ideal A :=232  ⨅ i, (J i).comap (completedPointMap A (P i))233/-- The map from `A` to the product of the completed local quotients `(A_{P_i})^/J_i`. -/234def finiteSupportQuotientMap : A →+* (∀ i, CompletedLocalAt A (P i) ⧸ J i) :=235  RingHom.pi fun i => (Ideal.Quotient.mk (J i)).comp (completedPointMap A (P i))236/-- The image of `finiteSupportKernel` in `A/(e)^j`. -/237def finiteSupportLevelKernel (e : A) (j : ℕ) : Ideal (A ⧸ (Ideal.span {e})^j) :=238  (finiteSupportKernel A ι P J).map (Ideal.Quotient.mk ((Ideal.span {e})^j))239end FiniteSupport240end241 242/-! ### Glued generators -/243 244section245variable (R : Type) [CommRing R] (t x : R)246/-- The slope of the `t`-chart, as an element of the overlap. -/247def overlapSlope : BlowupOverlap R t x :=248  algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartSlope R t x)249/-- The exceptional parameter `t`, as an element of the overlap. -/250def overlapException : BlowupOverlap R t x :=251  algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t)252/-- Compatible systems of local generators on the two charts that glue, up to the twist253`slope^d`, on the overlap modulo powers of the exceptional ideal. -/254structure GluedGenerators (beta : BlowupRestriction R t x) (d : ℕ) where255  left : ℕ → BlowupChart R t x256  right : ℕ → BlowupChart R x t257  left_compat : ∀ j : ℕ, left (j+1) - left j ∈ (chartExceptional R t x)^j258  right_compat : ∀ j : ℕ, right (j+1) - right j ∈ (chartExceptional R x t)^j259  overlap : ∀ j : ℕ, algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (left j) -260    (overlapSlope R t x)^d * beta.right (right j) ∈ (Ideal.span {overlapException R t x})^j261/-- The pair `(t^d · left j, x^d · right j)` of chart functions attached to glued generators. -/262def gluedFunctionPair {beta : BlowupRestriction R t x} {d : ℕ} (G : GluedGenerators R t x beta d)263    (j : ℕ) : BlowupChart R t x × BlowupChart R x t :=264  ((chartBase R t x t)^d * G.left j, (chartBase R x t x)^d * G.right j)265end266 267/-! ### Curve sections -/268 269section270variable (R : Type) [CommRing R] (t x : R) (beta : BlowupRestriction R t x) {d : ℕ}271  (G : GluedGenerators R t x beta d) (j : ℕ)272/-- The ideal `(left j) + (t)^j` of the `t`-chart. -/273def leftCurveIdeal : Ideal (BlowupChart R t x) :=274  Ideal.span {G.left j} ⊔ (chartExceptional R t x)^j275/-- The ideal `(right j) + (x)^j` of the `x`-chart. -/276def rightCurveIdeal : Ideal (BlowupChart R x t) :=277  Ideal.span {G.right j} ⊔ (chartExceptional R x t)^j278/-- The ideal `(left j) + (t)^j` of the overlap. -/279def overlapCurveIdeal : Ideal (BlowupOverlap R t x) :=280  Ideal.span {algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (G.left j)} ⊔281    (Ideal.span {overlapException R t x})^j282/-- The product lattice `leftCurveIdeal × rightCurveIdeal`. -/283def curveIdealLattice : Submodule R (BlowupChart R t x × BlowupChart R x t) :=284  ((leftCurveIdeal R t x beta G j).restrictScalars R).prod285    ((rightCurveIdeal R t x beta G j).restrictScalars R)286/-- Pairs of chart functions whose untwisted Čech difference lies in the overlap curve ideal. -/287def curveSections : Submodule R (BlowupChart R t x × BlowupChart R x t) :=288  ((overlapCurveIdeal R t x beta G j).restrictScalars R).comap (fullCechDifferential R t x beta 0)289/-- The image of `curveSections` modulo the curve ideal lattice. -/290def curveSectionsQuot : Submodule R ((BlowupChart R t x × BlowupChart R x t) ⧸ curveIdealLattice R t291    x beta G j) :=292  (curveSections R t x beta G j).map (curveIdealLattice R t x beta G j).mkQ293end294 295/-! ### Principal power layers -/296 297section298variable (A : Type) [CommRing A]299/-- `(t, x)` is a regular sequence: `t` is a nonzerodivisor on `A` and `x` on `A/(t)`. -/300def RegularParameterPair (t x : A) : Prop :=301  Function.Injective (fun a : A => t*a) ∧302    Function.Injective (fun a : A ⧸ Ideal.span {t} => Ideal.Quotient.mk (Ideal.span {t}) x * a)303/-- The quotient `A/(e)^j`. -/304abbrev PrincipalPowerQuotient (e : A) (j : ℕ) := A ⧸ (Ideal.span {e})^j305/-- The reduction `A/(e)^{j+1} → A/(e)^j`. -/306def principalPowerReduction (e : A) (j : ℕ) :307    PrincipalPowerQuotient A e (j+1) →ₐ[A] PrincipalPowerQuotient A e j :=308  Ideal.Quotient.factorₐ A (Ideal.pow_le_pow_right (Nat.le_succ j))309/-- The map `a ↦ a · e^j` into `A/(e)^{j+1}`. -/310def principalLayerMap (e : A) (j : ℕ) : A →ₗ[A] PrincipalPowerQuotient A e (j+1) :=311  LinearMap.toSpanSingleton A (PrincipalPowerQuotient A e (j+1))312    (Ideal.Quotient.mk ((Ideal.span {e})^(j+1)) (e^j))313/-- The layer `(e)^j/(e)^{j+1}`, as the kernel of the reduction map. -/314abbrev PrincipalLayer (e : A) (j : ℕ) :=315  LinearMap.ker (principalPowerReduction A e j).toLinearMap316end317 318/-! ### Strict chart coordinates -/319 320section321variable {O R : Type} [CommRing O] [CommRing R] [Algebra O R]322/-- The coordinate map of the child chart: the normal form of `H z`, rescaled by `π^(a−1)`. -/323def childCoordinateMap {n : ℕ} (pi : O) (a : ℕ) (b : Fin n → R)324    (E : R ≃ₗ[O] ((Fin n → O) × R)) (H : (Fin n → O) →ₗ[O] R) (z : Fin n → O) : Fin n → O :=325  (pi^(a-1)) • (generatorNormalForm (pi^a) b E (H z)).1326/-- Scaling a coordinate vector by `π^m`. -/327def coordinateScale {n : ℕ} (pi : O) (m : ℕ) (z : Fin n → O) : Fin n → O := (pi^m) • z328/-- The coset of coordinate vectors congruent to `z₀` modulo `π^m`. -/329def coordinateCoset {n : ℕ} (pi : O) (m : ℕ) (z₀ : Fin n → O) : Set (Fin n → O) :=330  {z | adicCongr (Ideal.span {pi}) m z z₀}331/-- The colon strict transform `(J·C) : e^d` of an ideal `J` along `alpha`. -/332def strictTransformIdeal {C : Type} [CommRing C] [Algebra O C] (alpha : R →ₐ[O] C) (e : C) (d : ℕ)333    (J : Ideal R) : Ideal C :=334  (J.map alpha.toRingHom).colon {e^d}335end336 337/-! ### Strict normalization -/338 339section340variable {O R : Type} [CommRing O] [CommRing R] [Algebra O R]341/-- The linear part `fst ∘ E ∘ H` of the strict normalization. -/342def normalizationLinearPart {n : ℕ}343    (E : R ≃ₗ[O] ((Fin n → O) × R)) (H : (Fin n → O) →ₗ[O] R) :344    (Fin n → O) →ₗ[O] (Fin n → O) :=345  (LinearMap.fst O (Fin n → O) R).comp (E.toLinearMap.comp H)346/-- The quadratic correction term of the strict normalization. -/347def normalizationQuadratic {n : ℕ} (b : Fin n → R)348    (E : R ≃ₗ[O] ((Fin n → O) × R)) (s : (Fin n → O) × R) : Fin n → O :=349  (E (s.2 * coordinateLift b s.1)).1350/-- The correction `−π^(a−k) · Q(quadratic term)` of the strict normalization. -/351def normalizationCorrection {n : ℕ} (pi : O) (a k : ℕ) (b : Fin n → R)352    (E : R ≃ₗ[O] ((Fin n → O) × R)) (H : (Fin n → O) →ₗ[O] R)353    (Q : (Fin n → O) →ₗ[O] (Fin n → O)) (z : Fin n → O) : Fin n → O :=354  -(pi^(a-k)) • Q (normalizationQuadratic b E355    (generatorNormalForm (pi^a) b E (H z)))356/-- The coordinate part of the normal form of `H z`, scaled by `π^a`. -/357def scaledStrictMap {n : ℕ} (pi : O) (a : ℕ) (b : Fin n → R)358    (E : R ≃ₗ[O] ((Fin n → O) × R)) (H : (Fin n → O) →ₗ[O] R)359    (z : Fin n → O) : Fin n → O :=360  (pi^a) • (generatorNormalForm (pi^a) b E (H z)).1361end362 363/-! ### Strict pullback -/364 365section366variable {O R C : Type} [CommRing O] [CommRing R] [CommRing C] [Algebra O R] [Algebra O C]367/-- The `O`-linear map `z ↦ Σ zᵢ bᵢ`. -/368def coordinateLinear {n : ℕ} (b : Fin n → R) : (Fin n → O) →ₗ[O] R :=369  ∑ i : Fin n, (LinearMap.proj i : (Fin n → O) →ₗ[O] O).smulRight (b i)370/-- The variation `z ↦ c · alpha (Σ zᵢ bᵢ)` pulled back along `alpha`. -/371def pulledVariation {n : ℕ} (alpha : R →ₐ[O] C) (c : C) (b : Fin n → R) :372    (Fin n → O) →ₗ[O] C :=373  (LinearMap.mulLeft O c).comp (alpha.toLinearMap.comp (coordinateLinear b))374end375 376/-! ### Surface sections -/377 378section379variable (R : Type) [CommRing R] (t x : R)380/-- The diagonal map from `R` to the product of the two charts. -/381def surfaceToChartPair : R →ₗ[R] (BlowupChart R t x × BlowupChart R x t) :=382  LinearMap.prod (Algebra.linearMap R (BlowupChart R t x)) (Algebra.linearMap R (BlowupChart R x t))383/-- The diagonal map from `R` to the `j`-th level of the Čech source. -/384def surfaceToCechInput (j : ℕ) : R →ₗ[R] CechLevelInput R t x j :=385  (cechInputLattice R t x j).mkQ.comp (surfaceToChartPair R t x)386/-- The `j`-th component of a thread of the Čech source. -/387def cechInputThreadLinear (j : ℕ) : CechInputThreads R t x →ₗ[R] CechLevelInput R t x j :=388  (LinearMap.proj j).comp389    (towerThreads R (fun j => CechLevelInput R t x j) (cechInputReduction R t x)).subtype390/-- The diagonal map from `R` to threads of the Čech source. -/391def surfaceThreads : R →ₗ[R] CechInputThreads R t x :=392  LinearMap.codRestrict393    (towerThreads R (fun j => CechLevelInput R t x j) (cechInputReduction R t x))394    (LinearMap.pi fun j => surfaceToCechInput R t x j) (fun r => by395      rw [towerThreads, LinearMap.mem_ker]396      ext j397      change surfaceToCechInput R t x j r -398        cechInputReduction R t x j (surfaceToCechInput R t x (j+1) r) = 0399      rw [sub_eq_zero]400      rfl)401end402 403/-! ### Tangent cells -/404 405section406variable (O R : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]407  [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]408/-- A chosen lift of a residue class. -/409def residueRepresentative (c : IsLocalRing.ResidueField R) : R :=410  Function.invFun (IsLocalRing.residue R) c411/-- A lift `Σ hᵢ t^(d−i) x^i` of a degree-`d` form with dehomogenization `H`. -/412def tangentLift (S : SurfaceData O R) (d : ℕ) (H : Polynomial (IsLocalRing.ResidueField R)) : R :=413  ∑ i : Fin (d+1), residueRepresentative R (H.coeff i.val) * S.t^(d-i.val) * S.x^i.val414/-- The principal ideal `J` has tangent cone of degree `d` with divisor `D` on the415exceptional line. -/416def HasTangentDivisor (S : SurfaceData O R) (J : Ideal R) (d : ℕ)Allowed residue ideals, cells, occupied points(4.6)417    (D : ExceptionalDivisor (IsLocalRing.ResidueField R)) : Prop :=418  ∃ f : R, ∃ H : Polynomial (IsLocalRing.ResidueField R),419    J = Ideal.span {f} ∧ HasHomogeneousDivisor (IsLocalRing.ResidueField R) d H D ∧420      f - tangentLift O R S d H ∈ (IsLocalRing.maximalIdeal R)^(d+1)421/-- Ideals in state `s` whose tangent cone has degree `d` and divisor `D`. -/422def fixedTangentCell (S : SurfaceData O R) (s : State) (d : ℕ)423    (D : ExceptionalDivisor (IsLocalRing.ResidueField R)) : Set (Ideal R) :=424  {J | J ∈ surfaceStateSet O R S s ∧ HasTangentDivisor O R S J d D}425end426 427/-! ### Curve data on the two charts -/428 429section430variable (R : Type) [CommRing R] (t x : R) (beta : BlowupRestriction R t x)431-- The generated injectivity and `SizeOf` declarations are unused and cost ~30 s of kernel time.432set_option genInjectivity false in433set_option genSizeOf false in434/-- Local data of a curve on the blow-up: finitely many points on the overlap, at `Z = 0` and435at infinity, with local equations transverse to the exceptional divisor and finite contact with it.436-/437structure TwoChartCurveData where438  ι : Type439  [fin : Finite ι]440  Q : ι → Ideal (BlowupOverlap R t x)441  [maximal : ∀ i, (Q i).IsMaximal]442  inj : Function.Injective Q443  onE : ∀ i, overlapException R t x ∈ Q i444  g : ∀ i, CompletedLocalAt (BlowupOverlap R t x) (Q i)445  transverse : ∀ i, LocallyTransverse (BlowupOverlap R t x) (Q i) (overlapException R t x) (g i)446  finite : ∀ i, FiniteContact (BlowupOverlap R t x) (Q i) (overlapException R t x) (g i)447  leftIso : ∀ i, CompletedLocalAt (BlowupOverlap R t x) (Q i) ≃+*448    CompletedLocalAt (BlowupChart R t x) ((Q i).comap (algebraMap (BlowupChart R t x)449        (BlowupOverlap R t x)))450  leftIso_compat : ∀ i (a : BlowupChart R t x), leftIso i451      (completedPointMap (BlowupOverlap R t x) (Q i)452    (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) a)) =453    completedPointMap (BlowupChart R t x) ((Q i).comap (algebraMap (BlowupChart R t x)454        (BlowupOverlap R t x))) a455  rightIso : ∀ i, CompletedLocalAt (BlowupOverlap R t x) (Q i) ≃+*456    CompletedLocalAt (BlowupChart R x t) ((Q i).comap beta.right.toRingHom)457  rightIso_compat : ∀ i (b : BlowupChart R x t), rightIso i458      (completedPointMap (BlowupOverlap R t x) (Q i)459    (beta.right b)) = completedPointMap (BlowupChart R x t) ((Q i).comap beta.right.toRingHom) b460  ι0 : Type461  [fin0 : Finite ι0]462  P0 : ι0 → Ideal (BlowupChart R t x)463  [maximal0 : ∀ k, (P0 k).IsMaximal]464  inj0 : Function.Injective P0465  slope0 : ∀ k, chartSlope R t x ∈ P0 k466  onE0 : ∀ k, chartBase R t x t ∈ P0 k467  g0 : ∀ k, CompletedLocalAt (BlowupChart R t x) (P0 k)468  transverse0 : ∀ k, LocallyTransverse (BlowupChart R t x) (P0 k) (chartBase R t x t) (g0 k)469  finite0 : ∀ k, FiniteContact (BlowupChart R t x) (P0 k) (chartBase R t x t) (g0 k)470  ιinf : Type471  [fininf : Finite ιinf]472  Pinf : ιinf → Ideal (BlowupChart R x t)473  [maximalinf : ∀ l, (Pinf l).IsMaximal]474  injinf : Function.Injective Pinf475  slopeinf : ∀ l, chartSlope R x t ∈ Pinf l476  onEinf : ∀ l, chartBase R x t x ∈ Pinf l477  ginf : ∀ l, CompletedLocalAt (BlowupChart R x t) (Pinf l)478  transverseinf : ∀ l, LocallyTransverse (BlowupChart R x t) (Pinf l) (chartBase R x t x) (ginf l)479  finiteinf : ∀ l, FiniteContact (BlowupChart R x t) (Pinf l) (chartBase R x t x) (ginf l)480attribute [instance] TwoChartCurveData.fin TwoChartCurveData.maximal TwoChartCurveData.fin0481  TwoChartCurveData.maximal0 TwoChartCurveData.fininf TwoChartCurveData.maximalinf482variable {R t x beta} (D : TwoChartCurveData R t x beta)483/-- The points of the curve on the `t`-chart. -/484def leftPoint : D.ι ⊕ D.ι0 → Ideal (BlowupChart R t x)485  | Sum.inl i => (D.Q i).comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))486  | Sum.inr k => D.P0 k487/-- The points of the curve on the `t`-chart are prime. -/488instance leftPoint_isPrime : ∀ s, (leftPoint D s).IsPrime489  | Sum.inl _ => Ideal.IsPrime.comap _490  | Sum.inr k => Ideal.IsMaximal.isPrime (D.maximal0 k)491/-- The local equations of the curve on the `t`-chart. -/492def leftData : ∀ s, CompletedLocalAt (BlowupChart R t x) (leftPoint D s)493  | Sum.inl i => D.leftIso i (D.g i)494  | Sum.inr k => D.g0 k495/-- The points of the curve on the `x`-chart. -/496def rightPoint : D.ι ⊕ D.ιinf → Ideal (BlowupChart R x t)497  | Sum.inl i => (D.Q i).comap beta.right.toRingHom498  | Sum.inr l => D.Pinf l499/-- The points of the curve on the `x`-chart are prime. -/500instance rightPoint_isPrime : ∀ s, (rightPoint D s).IsPrime501  | Sum.inl _ => Ideal.IsPrime.comap _502  | Sum.inr l => Ideal.IsMaximal.isPrime (D.maximalinf l)503/-- The local equations of the curve on the `x`-chart. -/504def rightData : ∀ s, CompletedLocalAt (BlowupChart R x t) (rightPoint D s)505  | Sum.inl i => D.rightIso i (D.g i)506  | Sum.inr l => D.ginf l507/-- The local ideal `(g, t^j)` at a point of the `t`-chart. -/508def leftLevelIdeal (j : ℕ) (s : D.ι ⊕ D.ι0) : Ideal (CompletedLocalAt (BlowupChart R t x)509    (leftPoint D s)) :=510  finiteLocalCurveIdeal (BlowupChart R t x) (leftPoint D s) (chartBase R t x t) (leftData D s) j511/-- The local ideal `(g, x^j)` at a point of the `x`-chart. -/512def rightLevelIdeal (j : ℕ) (s : D.ι ⊕ D.ιinf) : Ideal (CompletedLocalAt (BlowupChart R x t)513    (rightPoint D s)) :=514  finiteLocalCurveIdeal (BlowupChart R x t) (rightPoint D s) (chartBase R x t x) (rightData D s) j515/-- The local ideal `(g, t^j)` at a point of the overlap. -/516def commonLevelIdeal (j : ℕ) (i : D.ι) : Ideal (CompletedLocalAt (BlowupOverlap R t x) (D.Q i)) :=517  finiteLocalCurveIdeal (BlowupOverlap R t x) (D.Q i) (overlapException R t x) (D.g i) j518/-- The kernel of the `t`-chart in the product of its local level quotients. -/519def leftKernel (j : ℕ) : Ideal (BlowupChart R t x) :=520  finiteSupportKernel (BlowupChart R t x) (D.ι ⊕ D.ι0) (leftPoint D) (leftLevelIdeal D j)521/-- The kernel of the `x`-chart in the product of its local level quotients. -/522def rightKernel (j : ℕ) : Ideal (BlowupChart R x t) :=523  finiteSupportKernel (BlowupChart R x t) (D.ι ⊕ D.ιinf) (rightPoint D) (rightLevelIdeal D j)524/-- The kernel of the overlap in the product of its local level quotients. -/525def commonKernel (j : ℕ) : Ideal (BlowupOverlap R t x) :=526  finiteSupportKernel (BlowupOverlap R t x) D.ι D.Q (commonLevelIdeal D j)527/-- The image of `leftKernel` in `A/(t)^j`. -/528def leftLevelKernel (j : ℕ) : Ideal (BlowupChart R t x ⧸ (Ideal.span {chartBase R t x t})^j) :=529  finiteSupportLevelKernel (BlowupChart R t x) (D.ι ⊕ D.ι0) (leftPoint D) (leftLevelIdeal D j)530      (chartBase R t x t) j531/-- The image of `rightKernel` in `B/(x)^j`. -/532def rightLevelKernel (j : ℕ) : Ideal (BlowupChart R x t ⧸ (Ideal.span {chartBase R x t x})^j) :=533  finiteSupportLevelKernel (BlowupChart R x t) (D.ι ⊕ D.ιinf) (rightPoint D) (rightLevelIdeal D j)534      (chartBase R x t x) j535end536 537/-! ### Degree of curve data -/538 539section540variable {R : Type} [CommRing R] {t x : R} {beta : BlowupRestriction R t x}541    (D : TwoChartCurveData R t x beta)542/-- The local intersection multiplicity with the exceptional divisor at a `t`-chart point. -/543noncomputable def leftMultiplicity (s : D.ι ⊕ D.ι0) : ℕ :=544  (Module.length (CompletedLocalAt (BlowupChart R t x) (leftPoint D s))545    (CompletedLocalAt (BlowupChart R t x) (leftPoint D s) ⧸ leftLevelIdeal D 1 s)).toNat546/-- The local intersection multiplicity with the exceptional divisor at an `x`-chart point. -/547noncomputable def rightMultiplicity (s : D.ι ⊕ D.ιinf) : ℕ :=548  (Module.length (CompletedLocalAt (BlowupChart R x t) (rightPoint D s))549    (CompletedLocalAt (BlowupChart R x t) (rightPoint D s) ⧸ rightLevelIdeal D 1 s)).toNat550/-- The local intersection multiplicity with the exceptional divisor at an overlap point. -/551noncomputable def commonMultiplicity (i : D.ι) : ℕ :=552  (Module.length (CompletedLocalAt (BlowupOverlap R t x) (D.Q i))553    (CompletedLocalAt (BlowupOverlap R t x) (D.Q i) ⧸ commonLevelIdeal D 1 i)).toNat554/-- The residue degree of a `t`-chart point (length of its residue ring over `R`). -/555noncomputable def leftResidueDegree (s : D.ι ⊕ D.ι0) : ℕ :=556  (Module.length R (BlowupChart R t x ⧸ leftPoint D s)).toNat557/-- The residue degree of an `x`-chart point (length of its residue ring over `R`). -/558noncomputable def rightResidueDegree (s : D.ι ⊕ D.ιinf) : ℕ :=559  (Module.length R (BlowupChart R x t ⧸ rightPoint D s)).toNat560/-- The total intersection number of the curve with the exceptional divisor. -/561noncomputable def curveDataDegree : ℕ :=562  (∑ᶠ s : D.ι ⊕ D.ι0, leftResidueDegree D s * leftMultiplicity D s) +563    ∑ᶠ l : D.ιinf, rightMultiplicity D (Sum.inr l)564end565 566/-! ### The curve order limit -/567 568section569section Limit570variable (R : Type) [CommRing R] (t x : R) (beta : BlowupRestriction R t x) {d : ℕ}571  (G : GluedGenerators R t x beta d)572/-- The product of the two charts. -/573abbrev ChartPair := BlowupChart R t x × BlowupChart R x t574/-- Sequences of curve sections compatible modulo the curve ideal lattices. -/575def curveThreads : Submodule R (ℕ → ChartPair R t x) :=576  Submodule.pi Set.univ (fun j => curveSections R t x beta G j) ⊓577    (Submodule.pi Set.univ (fun j => curveIdealLattice R t x beta G j)).comap578      (towerDelta R (fun _ => ChartPair R t x) (fun _ => LinearMap.id))579/-- Sequences lying levelwise in the curve ideal lattices. -/580def curveNull : Submodule R (ℕ → ChartPair R t x) :=581  Submodule.pi Set.univ (fun j => curveIdealLattice R t x beta G j)582/-- Null sequences among the curve threads. -/583def curveNullThreads : Submodule R (curveThreads R t x beta G) :=584  (curveNull R t x beta G).comap (curveThreads R t x beta G).subtype585/-- The inverse limit of the curve orders: curve threads modulo null threads. -/586def CurveOrderLimit : Type := (curveThreads R t x beta G) ⧸ curveNullThreads R t x beta G587/-- Additive group structure on the curve order limit. -/588instance : AddCommGroup (CurveOrderLimit R t x beta G) :=589  inferInstanceAs (AddCommGroup ((curveThreads R t x beta G) ⧸ curveNullThreads R t x beta G))590/-- `R`-module structure on the curve order limit. -/591instance : Module R (CurveOrderLimit R t x beta G) :=592  inferInstanceAs (Module R ((curveThreads R t x beta G) ⧸ curveNullThreads R t x beta G))593/-- `O`-module structure on the curve order limit, by restriction of scalars. -/594instance (O : Type) [CommRing O] [Algebra O R] : Module O (CurveOrderLimit R t x beta G) :=595  inferInstanceAs (Module O ((curveThreads R t x beta G) ⧸ curveNullThreads R t x beta G))596/-- Scalar tower `O → R → CurveOrderLimit`. -/597instance (O : Type) [CommRing O] [Algebra O R] : IsScalarTower O R (CurveOrderLimit R t x beta G) :=598  inferInstanceAs (IsScalarTower O R ((curveThreads R t x beta G) ⧸ curveNullThreads R t x beta G))599/-- The quotient map from curve threads to the curve order limit. -/600def curveLimitMk : curveThreads R t x beta G →ₗ[R] CurveOrderLimit R t x beta G :=601  (curveNullThreads R t x beta G).mkQ602end Limit603section Product604variable {S : Type} [CommRing S]605/-- The reduction `S/(g, e^{j+1}) → S/(g, e^j)`. -/606def levelReduction (e g : S) (j : ℕ) : S ⧸ Ideal.span {g, e^(j+1)} →+* S ⧸ Ideal.span {g, e^j} :=607  Ideal.Quotient.factor (Ideal.span_le.mpr (by608    rintro y (rfl | rfl)609    · exact Ideal.subset_span (Set.mem_insert _ _)610    · rw [pow_succ]611      exact Ideal.mul_mem_right e _ (Ideal.subset_span (Set.mem_insert_of_mem _ rfl))))612end Product613section CurveProduct614variable {R : Type} [CommRing R] {t x : R} {beta : BlowupRestriction R t x}615  (D : TwoChartCurveData R t x beta)616/-- All points of the curve: overlap points, the point `Z = 0`, and the point at infinity. -/617abbrev AllPoints := D.ι ⊕ (D.ι0 ⊕ D.ιinf)618/-- The completed local ring at each point of the curve. -/619def localRing : AllPoints D → Type620  | Sum.inl i => CompletedLocalAt (BlowupOverlap R t x) (D.Q i)621  | Sum.inr (Sum.inl k) => CompletedLocalAt (BlowupChart R t x) (leftPoint D (Sum.inr k))622  | Sum.inr (Sum.inr l) => CompletedLocalAt (BlowupChart R x t) (rightPoint D (Sum.inr l))623/-- Ring structure on the completed local rings. -/624instance localRing_commRing : ∀ p, CommRing (localRing D p)625  | Sum.inl i => inferInstanceAs (CommRing (CompletedLocalAt (BlowupOverlap R t x) (D.Q i)))626  | Sum.inr (Sum.inl k) => inferInstanceAs (CommRing (CompletedLocalAt (BlowupChart R t x)627      (leftPoint D (Sum.inr k))))628  | Sum.inr (Sum.inr l) => inferInstanceAs (CommRing (CompletedLocalAt (BlowupChart R x t)629      (rightPoint D (Sum.inr l))))630/-- The local equation of the curve at each point. -/631def localCurve : ∀ p, localRing D p632  | Sum.inl i => D.g i633  | Sum.inr (Sum.inl k) => leftData D (Sum.inr k)634  | Sum.inr (Sum.inr l) => rightData D (Sum.inr l)635/-- The local exceptional parameter at each point. -/636def localException : ∀ p, localRing D p637  | Sum.inl i => completedPointMap (BlowupOverlap R t x) (D.Q i) (overlapException R t x)638  | Sum.inr (Sum.inl k) => completedPointMap (BlowupChart R t x) (leftPoint D (Sum.inr k))639      (chartBase R t x t)640  | Sum.inr (Sum.inr l) => completedPointMap (BlowupChart R x t) (rightPoint D (Sum.inr l))641      (chartBase R x t x)642/-- The localization map from pairs of chart functions to the completed local ring at each point643(through the `t`-chart at the overlap points and at `Z = 0`, through the `x`-chart at infinity). -/644def localSection : ∀ p, ChartPair R t x →+* localRing D p645  | Sum.inl i => ((completedPointMap (BlowupOverlap R t x) (D.Q i)).comp646      (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).comp (RingHom.fst _ _)647  | Sum.inr (Sum.inl k) =>648      (completedPointMap (BlowupChart R t x) (leftPoint D (Sum.inr k))).comp (RingHom.fst _ _)649  | Sum.inr (Sum.inr l) =>650      (completedPointMap (BlowupChart R x t) (rightPoint D (Sum.inr l))).comp (RingHom.snd _ _)651variable (j : ℕ)652/-- The local level quotient `(g, e^j)` at each point of the curve. -/653abbrev localQuotient (p : AllPoints D) : Type :=654  localRing D p ⧸ Ideal.span {localCurve D p, localException D p ^ j}655/-- The product of the local level quotients over all points of the curve. -/656abbrev curveProduct : Type := ∀ p : AllPoints D, localQuotient D j p657/-- The localization map from pairs of chart functions to the product of local quotients. -/658def sectionsToProduct : ChartPair R t x →+* curveProduct D j :=659  RingHom.pi fun p => (Ideal.Quotient.mk _).comp (localSection D p)660/-- The reduction from level `j + 1` to level `j` of the local product. -/661def curveProductReduction : curveProduct D (j + 1) →+* curveProduct D j :=662  RingHom.pi fun p => (levelReduction (localException D p) (localCurve D p) j).comp663    (Pi.evalRingHom _ p)664/-- Compatible threads in the tower of local products. -/665def curveProductThreads : Type :=666  {u : ∀ j, curveProduct D j // ∀ j, curveProductReduction D j (u (j+1)) = u j}667end CurveProduct668end669 670/-! ### The child order -/671 672section673variable {R : Type} [CommRing R] {t x : R} {beta : BlowupRestriction R t x}674    (D : TwoChartCurveData R t x beta)675/-- The map from `R` to the completed local ring at each point. -/676def localFromSurface : ∀ p, R →+* localRing D p677  | Sum.inl i => ((completedPointMap (BlowupOverlap R t x) (D.Q i)).comp678      (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).comp (chartBase R t x)679  | Sum.inr (Sum.inl k) => (completedPointMap (BlowupChart R t x) (leftPoint D (Sum.inr k))).comp680      (chartBase R t x)681  | Sum.inr (Sum.inr l) => (completedPointMap (BlowupChart R x t) (rightPoint D (Sum.inr l))).comp682      (chartBase R x t)683/-- The product of the completed local rings of the curve at its points. -/684def childOrder : Type := ∀ p : AllPoints D, localRing D p ⧸ Ideal.span {localCurve D p}685/-- Ring structure on the child order. -/686instance : CommRing (childOrder D) := inferInstanceAs (CommRing687    (∀ p : AllPoints D, localRing D p ⧸ Ideal.span {localCurve D p}))688/-- The diagonal map from `R` to the child order. -/689def childOrderMap : R →+* childOrder D :=690  RingHom.pi fun p => (Ideal.Quotient.mk (Ideal.span {localCurve D p})).comp (localFromSurface D p)691/-- Algebra structure on the child order. -/692instance (O : Type) [CommRing O] [∀ p : AllPoints D, Algebra O (localRing D p)] : Algebra O693    (childOrder D) :=694  inferInstanceAs (Algebra O (∀ p : AllPoints D, localRing D p ⧸ Ideal.span {localCurve D p}))695end696 697/-! ### Points above a divisor -/698 699section700section Points701variable (R : Type) [CommRing R] (t x : R) [IsLocalRing R]702/-- The point of the `t`-chart above an affine direction `φ` of the exceptional line. -/703def directionPoint (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial704    (IsLocalRing.ResidueField R))705    (φ : AffineDirection (IsLocalRing.ResidueField R)) : Ideal (BlowupChart R t x) :=706  (Ideal.span {φ.val}).comap (e.toRingHom.comp (Ideal.Quotient.mk (chartExceptional R t x)))707/-- The point at infinity `(x, W)` of the `x`-chart. -/708def infinityPoint : Ideal (BlowupChart R x t) := Ideal.span {chartBase R x t x, chartSlope R x t}709/-- The colon strict transform `(J·R_P) : t^d` at a point `P` of the `t`-chart. -/710def strictTransformAt (P : Ideal (BlowupChart R t x)) [P.IsPrime] (d : ℕ) (J : Ideal R) :711    Ideal (CompletedLocalAt (BlowupChart R t x) P) :=712  (J.map ((completedPointMap (BlowupChart R t x) P).comp (chartBase R t x))).colon713    {(completedPointMap (BlowupChart R t x) P (chartBase R t x t))^d}714end Points715section Matching716variable {R : Type} [CommRing R] {t x : R} [IsLocalRing R] {beta : BlowupRestriction R t x}717/-- The points and multiplicities of the curve data match the divisor `Dv` on the718exceptional line. -/719structure MatchesDivisor (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial720    (IsLocalRing.ResidueField R))721    (D : TwoChartCurveData R t x beta) (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R)) : Prop722        where723  common : ∀ i : D.ι, ∃ φ : AffineDirection (IsLocalRing.ResidueField R), φ ≠ zeroAffine724      (IsLocalRing.ResidueField R) ∧725    D.Q i = (directionPoint R t x e φ).map (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) ∧726    Dv (some φ) = commonMultiplicity D i727  common_surj : ∀ φ : AffineDirection (IsLocalRing.ResidueField R), φ ≠ zeroAffine728      (IsLocalRing.ResidueField R) →729    0 < Dv (some φ) → ∃ i : D.ι, D.Q i = (directionPoint R t x e φ).map730        (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))731  zero : ∀ k : D.ι0, D.P0 k = directionPoint R t x e (zeroAffine (IsLocalRing.ResidueField R)) ∧732    Dv (zeroDirection (IsLocalRing.ResidueField R)) = leftMultiplicity D (Sum.inr k)733  zero_surj : 0 < Dv (zeroDirection (IsLocalRing.ResidueField R)) → Nonempty D.ι0734  inf : ∀ l : D.ιinf, D.Pinf l = infinityPoint R t x ∧ Dv none = rightMultiplicity D (Sum.inr l)735  inf_surj : 0 < Dv none → Nonempty D.ιinf736end Matching737end738 739/-! ### Child ideal sets -/740 741section742section StateContacts743/-- The contact with the old boundary t = 0 recorded by a state (N002). -/744def stateContactT : State → ℕ745  | .single _ c => c746  | .crossing _ _ c _ => c747/-- The contact with the old boundary x = 0 recorded by a crossing state; `none` for a748single-boundary state. -/749def stateContactX : State → Option ℕ750  | .single _ _ => none751  | .crossing _ _ _ h => some h752end StateContacts753section Points754variable (R : Type) [CommRing R] (t x : R) [IsLocalRing R]755  (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (IsLocalRing.ResidueField R))756/-- The point above a monic irreducible φ (N881) is prime: it is the preimage of the maximal ideal757(φ) of k[Z]. -/758instance directionPoint_isPrime (φ : AffineDirection (IsLocalRing.ResidueField R)) :759    (directionPoint R t x e φ).IsPrime := by760  have : (Ideal.span {φ.val}).IsPrime :=761    (PrincipalIdealRing.isMaximal_of_irreducible φ.property.2).isPrime762  exact Ideal.IsPrime.comap _763variable (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R))764    (hinf : (infinityPoint R t x).IsPrime)765/-- The completed local ring (N274) at a point of the support: of the right chart B = R[W]/(xW − t)766at the point767∞ = (x, W), of the left chart A = R[Z]/(tZ − x) at the point above an affine direction φ. -/768def divisorLocalRing : divisorSupport Dv → Type769  | ⟨none, _⟩ => @CompletedLocalAt (BlowupChart R x t) _ (infinityPoint R t x) hinf770  | ⟨some φ, _⟩ => CompletedLocalAt (BlowupChart R t x) (directionPoint R t x e φ)771/-- Ring structure on the completed local rings at the support points. -/772instance divisorLocalRing_commRing : ∀ Q, CommRing (divisorLocalRing R t x e Dv hinf Q)773  | ⟨none, _⟩ => inferInstanceAs (CommRing (@CompletedLocalAt (BlowupChart R x t) _774      (infinityPoint R t x) hinf))775  | ⟨some φ, _⟩ => inferInstanceAs (CommRing (CompletedLocalAt (BlowupChart R t x)776      (directionPoint R t x e φ)))777/-- The exceptional equation at a point of the support: the image of x at ∞, the image of t778elsewhere. -/779def divisorException : ∀ Q, divisorLocalRing R t x e Dv hinf Q780  | ⟨none, _⟩ => @completedPointMap (BlowupChart R x t) _ (infinityPoint R t x) hinf781      (chartBase R x t x)782  | ⟨some φ, _⟩ => completedPointMap (BlowupChart R t x) (directionPoint R t x e φ)783      (chartBase R t x t)784/-- The boundary equation at a point of the support: the image of the slope W at ∞ (there W = 0 is785the strict786transform of the old boundary t = 0) and the image of the slope Z at an affine point (at Z = 0 this787is the strict788transform of the old boundary x = 0; at every other affine point Z is a unit of the local ring). -/789def divisorBoundary : ∀ Q, divisorLocalRing R t x e Dv hinf Q790  | ⟨none, _⟩ => @completedPointMap (BlowupChart R x t) _ (infinityPoint R t x) hinf791      (chartSlope R x t)792  | ⟨some φ, _⟩ => completedPointMap (BlowupChart R t x) (directionPoint R t x e φ)793      (chartSlope R t x)794/-- The colon strict transform (J·R_P) : e_P^d (N881) of a parent ideal J at each point of the795support. -/796def divisorStrictTransform (d : ℕ) (J : Ideal R) : ∀ Q, Ideal (divisorLocalRing R t x e Dv hinf Q)797  | ⟨none, _⟩ => @strictTransformAt R _ x t (infinityPoint R t x) hinf d J798  | ⟨some φ, _⟩ => strictTransformAt R t x (directionPoint R t x e φ) d J799/-- The child ideal set at a point Q of the support, for the parent state s and multiplicity d:800principal ideals I801whose contact with the exceptional equation is the multiplicity Dv Q, whose contact with the old802boundary W = 0 is803c − d at ∞ (c the t-contact of s), and whose contact with the old boundary Z = 0 is h − d at the804point Z = 0 when805s is a crossing state with x-contact h. -/806def childIdealSet (s : State) (d : ℕ) (Q : divisorSupport Dv) :807    Set (Ideal (divisorLocalRing R t x e Dv hinf Q)) :=808  {I | (∃ g, I = Ideal.span {g}) ∧809    Module.length (divisorLocalRing R t x e Dv hinf Q)810      (divisorLocalRing R t x e Dv hinf Q ⧸ (I ⊔ Ideal.span {divisorException R t x e Dv hinf Q})) =811        (Dv Q.val : ℕ∞) ∧812    (Q.val = none → Module.length (divisorLocalRing R t x e Dv hinf Q)813      (divisorLocalRing R t x e Dv hinf Q ⧸ (I ⊔ Ideal.span {divisorBoundary R t x e Dv hinf Q})) =814        ((stateContactT s - d : ℕ) : ℕ∞)) ∧815    (Q.val = zeroDirection (IsLocalRing.ResidueField R) → ∀ h : ℕ, stateContactX s = some h →816      Module.length (divisorLocalRing R t x e Dv hinf Q)817        (divisorLocalRing R t x e Dv hinf Q ⧸ (I ⊔ Ideal.span {divisorBoundary R t x e Dv hinf Q}))818            =819          ((h - d : ℕ) : ℕ∞))}820end Points821end822 823/-! ### Blow-up charts -/824 825/-- On the `t`-chart, `t · X = x`. -/826theorem blowup_chart_relation (R : Type) [CommRing R] (t x : R) :827    chartBase R t x t * chartSlope R t x = chartBase R t x x := by828  have h : Ideal.Quotient.mk (Ideal.span {blowupRelation R t x}) (blowupRelation R t x) = 0 :=829    Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span rfl)830  simp only [blowupRelation] at h831  exact sub_eq_zero.mp h832 833/-- Ring maps out of a blow-up chart agree once they agree on `R` and on the slope. -/834theorem blowup_chart_ringHom_ext (R S : Type) [CommRing R] [CommRing S] (t x : R)835    (f g : BlowupChart R t x →+* S) (hbase : ∀ r : R, f (chartBase R t x r) = g (chartBase R t x r))836    (hslope : f (chartSlope R t x) = g (chartSlope R t x)) :837    f = g :=838  Ideal.Quotient.ringHom_ext (Polynomial.ringHom_ext hbase hslope)839 840/-- Universal property of the `t`-chart: a map `φ : R → S` with an element `z` satisfying841`φ t · z = φ x` extends uniquely through `R[X]/(tX − x)` sending the slope to `z`. -/842theorem blowup_chart_universal (R S : Type) [CommRing R] [CommRing S] (t x : R) (phi : R →+* S)843    (z : S) (hz : phi t * z = phi x) :844    ∃ psi : BlowupChart R t x →+* S, (∀ a : R, psi (chartBase R t x a) = phi a) ∧ psi845        (chartSlope R t x) = z := by846  have hker : ∀ p ∈ Ideal.span {blowupRelation R t x}, Polynomial.eval₂RingHom phi z p = 0 := by847    intro p hp848    rw [Ideal.mem_span_singleton'] at hp849    obtain ⟨q, rfl⟩ := hp850    simp [blowupRelation, hz]851  exact ⟨Ideal.Quotient.lift _ (Polynomial.eval₂RingHom phi z) hker, fun a => by simp [chartBase],852    by simp [chartSlope]⟩853 854/-- If `(t, x)` is a regular sequence, then `t` is a nonzerodivisor on the `t`-chart. -/855theorem blowup_exceptional_parameter_regular (R : Type) [CommRing R] (t x : R)856    (hreg : RegularParameterPair R t x) :857    Function.Injective (fun a : BlowupChart R t x => chartBase R t x t * a) := by858  obtain ⟨ht, hx⟩ := hreg859  have hCt : ∀ P P' : Polynomial R, Polynomial.C t * P = Polynomial.C t * P' → P = P' :=860    fun P P' h ↦ Polynomial.ext fun n ↦861      ht (by simpa only [Polynomial.coeff_C_mul] using congrArg (Polynomial.coeff · n) h)862  have key : ∀ P : Polynomial R,863      Ideal.Quotient.mk (Ideal.span {blowupRelation R t x}) (Polynomial.C t * P) = 0 →864      Ideal.Quotient.mk (Ideal.span {blowupRelation R t x}) P = 0 := by865    intro P hP866    rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton'] at hP867    obtain ⟨Q, hQ⟩ := hP868    have hQt : Q ∈ Ideal.map Polynomial.C (Ideal.span {t}) := by869      rw [Ideal.mem_map_C_iff]870      intro i871      have e : Polynomial.C x * Q = Polynomial.C t * (Polynomial.X * Q - P) := by872        unfold blowupRelation at hQ873        linear_combination -hQ874      have := congrArg (fun F => Polynomial.coeff F i) e875      simp only [Polynomial.coeff_C_mul] at this876      have h0 : Ideal.Quotient.mk (Ideal.span {t}) x * Ideal.Quotient.mk (Ideal.span {t})877          (Q.coeff i) = Ideal.Quotient.mk (Ideal.span {t}) x * 0 := by878        rw [← map_mul, this, mul_zero, Ideal.Quotient.eq_zero_iff_mem]879        exact Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self t)880      exact Ideal.Quotient.eq_zero_iff_mem.1 (hx h0)881    rw [Ideal.map_span, Set.image_singleton, Ideal.mem_span_singleton'] at hQt882    obtain ⟨Q1, hQ1⟩ := hQt883    rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton']884    refine ⟨Q1, hCt _ _ ?_⟩885    rw [← hQ, ← hQ1]; ring886  intro a b hab887  obtain ⟨P, rfl⟩ := Ideal.Quotient.mk_surjective a888  obtain ⟨P', rfl⟩ := Ideal.Quotient.mk_surjective b889  simp only [chartBase, RingHom.comp_apply, ← map_mul] at hab890  rw [← sub_eq_zero, ← map_sub]891  exact key _ (by rw [mul_sub, map_sub, hab, sub_self])892 893/-- The `x`-chart modulo its slope `W` is `R/(t)`, compatibly with the structure maps. -/894theorem boundary_chart_quotient_equiv (R : Type) [CommRing R] (t x : R) :895    ∃ ρ : (BlowupChart R x t ⧸ Ideal.span {chartSlope R x t}) ≃+* (R ⧸ Ideal.span {t}),896        (∀ r : R, ρ (Ideal.Quotient.mk (Ideal.span {chartSlope R x t}) (chartBase R x t r)) =897        Ideal.Quotient.mk (Ideal.span {t}) r) ∧ ρ (Ideal.Quotient.mk (Ideal.span {chartSlope R x t})898        (chartSlope R x t)) = 0 := by899  let φ : Polynomial R →+* R ⧸ Ideal.span {t} :=900    Polynomial.eval₂RingHom (Ideal.Quotient.mk (Ideal.span {t})) 0901  have hφ : ∀ r, φ (Polynomial.C r) = Ideal.Quotient.mk (Ideal.span {t}) r := fun r => by902    simp [φ]903  have hX : φ Polynomial.X = 0 := by simp [φ]904  have hrel : φ (blowupRelation R x t) = 0 := by905    simp [blowupRelation, φ]906  let f1 : BlowupChart R x t →+* R ⧸ Ideal.span {t} :=907    Ideal.Quotient.lift _ φ (fun a ha => by908      obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.1 ha909      simp [hrel])910  have hf1 : ∀ p, f1 (Ideal.Quotient.mk _ p) = φ p := fun p => rfl911  let f : (BlowupChart R x t ⧸ Ideal.span {chartSlope R x t}) →+* R ⧸ Ideal.span {t} :=912    Ideal.Quotient.lift _ f1 (fun a ha => by913      obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.1 ha914      obtain ⟨p, rfl⟩ := Ideal.Quotient.mk_surjective b915      simp [chartSlope, hf1, hX])916  let g0 : R →+* (BlowupChart R x t ⧸ Ideal.span {chartSlope R x t}) :=917    (Ideal.Quotient.mk _).comp (chartBase R x t)918  have hW : Ideal.Quotient.mk (Ideal.span {chartSlope R x t}) (chartSlope R x t) = 0 :=919    Ideal.Quotient.eq_zero_iff_mem.2 (Ideal.mem_span_singleton_self _)920  have hgt : g0 t = 0 := by921    change Ideal.Quotient.mk _ (chartBase R x t t) = 0922    rw [← blowup_chart_relation R x t, map_mul, hW]923    exact mul_zero (Ideal.Quotient.mk (Ideal.span {chartSlope R x t}) (chartBase R x t x))924  let g : (R ⧸ Ideal.span {t}) →+* (BlowupChart R x t ⧸ Ideal.span {chartSlope R x t}) :=925    Ideal.Quotient.lift _ g0 (fun a ha => by926      obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.1 ha927      change g0 (b * t) = 0928      rw [map_mul, hgt]; exact mul_zero (g0 b))929  have hfg : f.comp g = RingHom.id _ := by930    apply Ideal.Quotient.ringHom_ext931    ext r932    simp [f, g, g0, f1, φ, chartBase]933  have hgf : g.comp f = RingHom.id _ := by934    refine Ideal.Quotient.ringHom_ext <| Ideal.Quotient.ringHom_ext <| Polynomial.ringHom_ext935      (fun r ↦ by simp [f, g, g0, f1, φ, chartBase]) ?_936    · change g (f (Ideal.Quotient.mk _ (chartSlope R x t))) = _937      rw [hW, map_zero, map_zero]938      exact hW.symm939  refine ⟨RingEquiv.ofRingHom f g hfg hgf, fun r ↦ by simp [f, f1, φ, chartBase], ?_⟩940  change f (Ideal.Quotient.mk _ (chartSlope R x t)) = 0941  rw [hW, map_zero]942 943/-! ### The Čech complex of the two charts -/944 945/-- The twisted Čech differential maps the lattice `(t^j) × (x^j)` into `(t^j)`. -/946theorem actual_cech_preserves_exceptional_lattices (R : Type) [CommRing R] (t x : R)947    (beta : BlowupRestriction R t x) (d j : ℕ) :948    cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap (fullCechDifferential R t x beta d)949        := by950  rintro ⟨a, b⟩ ⟨ha, hb⟩951  have ha' : a ∈ Ideal.span {chartBase R t x t ^ j} := by952    rw [← Ideal.span_singleton_pow]; exact ha953  have hb' : b ∈ Ideal.span {chartBase R x t x ^ j} := by954    rw [← Ideal.span_singleton_pow]; exact hb955  rw [Ideal.mem_span_singleton'] at ha' hb'956  clear ha hb957  obtain ⟨a0, rfl⟩ := ha'958  obtain ⟨b0, rfl⟩ := hb'959  simp only [Submodule.mem_comap, cechOutputLattice, Submodule.restrictScalars_mem,960    Ideal.span_singleton_pow, fullCechDifferential, ringCechDifferential]961  change (IsScalarTower.toAlgHom R (BlowupChart R t x) (BlowupOverlap R t x)) _ -962    IsLocalization.Away.invSelf (chartSlope R t x) ^ d * beta.right _ ∈ _963  have hx : beta.right (chartBase R x t x) =964      algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x t) *965        algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartSlope R t x) := by966    rw [← map_mul, blowup_chart_relation]967    exact beta.right.commutes x968  apply Ideal.sub_mem969  · rw [Ideal.mem_span_singleton']970    refine ⟨IsScalarTower.toAlgHom R (BlowupChart R t x) (BlowupOverlap R t x) a0, ?_⟩971    simp972  · rw [Ideal.mem_span_singleton']973    refine ⟨IsLocalization.Away.invSelf (chartSlope R t x) ^ d *974      (algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartSlope R t x)) ^ j *975      beta.right b0, ?_⟩976    rw [map_mul, map_pow, hx]977    ring978 979/-- The level Čech differentials commute with the reduction maps. -/980theorem actual_cech_differentials_commute_with_reduction (R : Type) [CommRing R] (t x : R)981    (beta : BlowupRestriction R t x) (d j : ℕ) (hnext : cechInputLattice R t x (j + 1) ≤982    (cechOutputLattice R t x (j + 1)).comap (fullCechDifferential R t x beta d))983    (hnow : cechInputLattice R t x j ≤ (cechOutputLattice R t x j).comap984    (fullCechDifferential R t x beta d)) :985    (cechOutputReduction R t x j).comp (finiteCechDifferential R t x beta d (j+1) hnext) =986        (finiteCechDifferential R t x beta d j hnow).comp (cechInputReduction R t x j) :=987  LinearMap.ext fun q => Submodule.Quotient.induction_on _ q fun _ => rfl988 989/-- The reduction maps of the Čech source and target towers are surjective. -/990theorem actual_cech_reductions_surjective (R : Type) [CommRing R] (t x : R) (j : ℕ) :Lemma 4.1Appendix A991    Function.Surjective (cechInputReduction R t x j) ∧ Function.Surjective992        (cechOutputReduction R t x j) := by993  constructor <;>994  · intro y995    obtain ⟨z, rfl⟩ := Submodule.mkQ_surjective _ y996    exact ⟨Submodule.mkQ _ z, rfl⟩997 998/-! ### Coordinates and adic cylinders -/999 1000/-- Coordinate vectors over a DVR with finite residue field admit a finite set of unique1001representatives modulo `π^M`. -/1002theorem coordinate_coset_representatives_exist (O : Type) [CommRing O] [IsDomain O]1003    [IsDiscreteValuationRing O] [Finite (IsLocalRing.ResidueField O)] (pi : O)1004    (hpi : Irreducible pi) (n M : ℕ) :1005    ∃ reps : Finset (Fin n → O), ∀ z : Fin n → O, ∃! z₀, z₀ ∈ reps ∧ adicCongr (Ideal.span {pi}) M z1006        z₀ := by1007  classical1008  have hmax : IsLocalRing.maximalIdeal O = Ideal.span {pi} := hpi.maximalIdeal_eq1009  have hc := residue_quotient_card O M1010  rw [hmax] at hc1011  have : Finite (O ⧸ (Ideal.span {pi})^M) := by1012    apply Nat.finite_of_card_ne_zero1013    rw [hc]1014    have : 0 < Nat.card (IsLocalRing.ResidueField O) := Nat.card_pos1015    positivity1016  have : Finite (((Fin n → O)) ⧸ ((Ideal.span {pi})^M • ⊤ : Submodule O (Fin n → O))) :=1017    finite_free_residue_quotient O (Fin n → O) ((Ideal.span {pi})^M)1018  have := Fintype.ofFinite (((Fin n → O)) ⧸ ((Ideal.span {pi})^M • ⊤ : Submodule O (Fin n → O)))1019  refine ⟨Finset.univ.image (fun c : ((Fin n → O)) ⧸ ((Ideal.span {pi})^M • ⊤ : Submodule O1020      (Fin n → O)) => Quotient.out c), fun z => ?_⟩1021  have key : ∀ w : Fin n → O, adicCongr (Ideal.span {pi}) M z w ↔1022      Submodule.Quotient.mk z = (Submodule.Quotient.mk w :1023        ((Fin n → O)) ⧸ ((Ideal.span {pi})^M • ⊤ : Submodule O (Fin n → O))) := by1024    intro w1025    rw [Submodule.Quotient.eq]1026    rfl1027  refine ⟨Quotient.out (Submodule.Quotient.mk z :1028    ((Fin n → O)) ⧸ ((Ideal.span {pi})^M • ⊤ : Submodule O (Fin n → O))), ⟨?_, ?_⟩, ?_⟩1029  · exact Finset.mem_image.2 ⟨_, Finset.mem_univ _, rfl⟩1030  · rw [key]1031    exact (Submodule.Quotient.mk_out _).symm1032  · rintro y ⟨hy, hz⟩1033    obtain ⟨c, -, rfl⟩ := Finset.mem_image.1 hy1034    rw [key] at hz1035    have : Submodule.Quotient.mk z = c := by1036      rw [hz]; exact Submodule.Quotient.mk_out c1037    rw [this]1038 1039/-- Structural facts on the coefficient space `O^n`: its Borel σ-algebra is generated by1040`π`-adic cylinders, the coefficient measure is a Haar probability measure, its `π`-adic quotients1041are finite, and scaled linear maps are continuous. -/1042theorem coefficient_space_strict_instances (O : Type) [CommRing O] [IsDomain O]1043    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1044    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]1045    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]1046    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (pi : O) (hpi : Irreducible pi) (n : ℕ) :1047    (inferInstance : MeasurableSpace (Fin n → O)) = adicCylinderSpace (Ideal.span {pi}) (Fin n → O)1048        ∧ MeasureTheory.Measure.IsAddHaarMeasure (coefficientMeasure O n) ∧1049        MeasureTheory.IsProbabilityMeasure (coefficientMeasure O n) ∧1050        (∀ j, Finite (AdicQuotient (Ideal.span {pi}) (Fin n → O) j)) ∧ ∀ (a : ℕ)1051        (L : (Fin n → O) →ₗ[O] (Fin n → O)), Continuous (fun z : Fin n → O => (pi^a) • L z) := by1052  have hm : IsLocalRing.maximalIdeal O = Ideal.span {pi} := hpi.maximalIdeal_eq1053  refine ⟨?_, ?_, ?_, ?_, ?_⟩1054  · rw [← hm]1055    exact finite_coordinate_borel_cylinders O _ htop n1056  · have h1 : MeasureTheory.Measure.addHaar (G := Fin n → O) Set.univ ≠ ⊤ :=1057      isCompact_univ.measure_lt_top.ne1058    have h2 : MeasureTheory.Measure.addHaar (G := Fin n → O) Set.univ ≠ 0 :=1059      (MeasureTheory.Measure.measure_pos_of_nonempty_interior _ (by simp)).ne'1060    unfold coefficientMeasure1061    exact MeasureTheory.Measure.IsAddHaarMeasure.smul _ (by simp [h1]) (by simp [h2])1062  · exact coefficient_measure_probability O htop n1063  · intro j1064    have : Finite (O ⧸ (Ideal.span {pi}) ^ j) := by1065      rw [← hm]1066      have hpos : 0 < Nat.card (IsLocalRing.ResidueField O) := Nat.card_pos1067      exact Nat.finite_of_card_ne_zero (by rw [residue_quotient_card O j]; positivity)1068    exact finite_free_residue_quotient O (Fin n → O) ((Ideal.span {pi}) ^ j)1069  · exact fun a L => finite_coordinate_linear_continuous O n n ((pi ^ a) • L)1070 1071/-- The scaled strict map is `π` times the child coordinate map; hence its range and1072preimages are those of the child coordinate map transported by `w ↦ π • w`. -/1073theorem child_coordinate_map_scaled (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (n : ℕ)1074    (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R)) (H : (Fin n → O) →ₗ[O] R)1075    (ha : 1 ≤ a) (hinj : Function.Injective (fun w : Fin n → O => pi • w)) :1076    (∀ z : Fin n → O, pi • childCoordinateMap pi a b E H z = scaledStrictMap pi a b E H z) ∧1077        Set.range (scaledStrictMap pi a b E H) = (fun w : Fin n → O => pi • w) '' Set.range1078        (childCoordinateMap pi a b E H) ∧ ∀ T : Set (Fin n → O), scaledStrictMap pi a b E H ⁻¹'1079        ((fun w : Fin n → O => pi • w) '' T) = childCoordinateMap pi a b E H ⁻¹' T := by1080  have h1 : ∀ z : Fin n → O, pi • childCoordinateMap pi a b E H z = scaledStrictMap pi a b E H z :=1081      by1082    intro z1083    obtain ⟨k, rfl⟩ : ∃ k, a = k + 1 := ⟨a - 1, by omega⟩1084    simp only [childCoordinateMap, scaledStrictMap, Nat.add_sub_cancel, smul_smul, pow_succ,1085        mul_comm]1086  refine ⟨h1, ?_, ?_⟩1087  · rw [← Set.range_comp]1088    ext x; constructor <;> rintro ⟨z, rfl⟩ <;> exact ⟨z, by simp [Function.comp, h1]⟩1089  · intro T1090    ext z1091    simp only [Set.mem_preimage, ← h1]1092    exact hinj.mem_set_image1093 1094/-! ### Completed local rings and lengths -/1095 1096/-- If `m̂^L ⊆ J` in the completed local ring at a maximal ideal `P`, then `P^L` is contained1097in the contraction of `J`. -/1098theorem completed_point_power_contraction (A : Type) [CommRing A] (P : Ideal A) [P.IsMaximal]1099    (L : ℕ) (J : Ideal (CompletedLocalAt A P)) (hJ : ((IsLocalRing.maximalIdeal1100    (Localization.AtPrime P)).map (localCompletionMap (Localization.AtPrime P))) ^ L ≤ J) :1101    P^L ≤ J.comap (completedPointMap A P) := by1102  rw [← Ideal.map_le_iff_le_comap, Ideal.map_pow]1103  refine le_trans (le_of_eq ?_) hJ1104  congr 11105  unfold completedPointMap1106  rw [← Ideal.map_map, Localization.AtPrime.map_eq_maximalIdeal]1107 1108/-- If `P^L ⊆ I` and `P` meets the localizing submonoid, then `I` extends to the unit ideal. -/1109theorem contracted_ideal_map_localization_top (A S : Type) [CommRing A] [CommRing S] [Algebra A S]1110    (M : Submonoid A) [IsLocalization M S] (P I : Ideal A) (L : ℕ) (hPI : P ^ L ≤ I) (m : A)1111    (hm : m ∈ M) (hmP : m ∈ P) :1112    I.map (algebraMap A S) = ⊤ := by1113  refine Ideal.eq_top_of_isUnit_mem _ (Ideal.mem_map_of_mem _ (hPI (Ideal.pow_mem_pow hmP L))) ?_1114  rw [map_pow]1115  exact (IsLocalization.map_units S ⟨m, hm⟩).pow L1116 1117/-- The length of `R/(π, f)` for a concrete surface `R` equals the length of the special fibre1118modulo the image of `f`. -/1119theorem concrete_surface_special_fiber_length_transport (O : Type) [CommRing O] [IsDomain O]1120    [IsDiscreteValuationRing O] (pi : O) (u : (TwoSeries O)ˣ) (a b : ℕ)1121    (f : ConcreteSurface O pi u a b) (e : (ConcreteSurface O pi u a b ⧸ Ideal.span1122    {algebraMap O (ConcreteSurface O pi u a b) pi}) ≃+* SpecialFiber (IsLocalRing.ResidueField O) a1123    b) :1124    Module.length (ConcreteSurface O pi u a b) (ConcreteSurface O pi u a b ⧸ Ideal.span1125        {algebraMap O (ConcreteSurface O pi u a b) pi, f}) = Module.length1126        (SpecialFiber (IsLocalRing.ResidueField O) a b) (SpecialFiber (IsLocalRing.ResidueField O) a1127        b ⧸ Ideal.span {e (Ideal.Quotient.mk (Ideal.span1128        {algebraMap O (ConcreteSurface O pi u a b) pi}) f)}) := by1129  let R := ConcreteSurface O pi u a b1130  let SF := SpecialFiber (IsLocalRing.ResidueField O) a b1131  let I : Ideal R := Ideal.span {algebraMap O R pi}1132  let g : SF := e (Ideal.Quotient.mk I f)1133  let φ : R →+* SF := e.toRingHom.comp (Ideal.Quotient.mk I)1134  have hφ : Function.Surjective φ :=1135    e.surjective.comp Ideal.Quotient.mk_surjective1136  let _ : Algebra R SF := φ.toAlgebra1137  have hsurj : Function.Surjective (algebraMap R SF) := hφ1138  rw [← Module.length_eq_of_surjective (S := R) hsurj]1139  let ψ : R →ₐ[R] SF ⧸ Ideal.span {g} := Algebra.ofId R _1140  have hψ : Function.Surjective ψ := fun y ↦ by1141    obtain ⟨z, rfl⟩ := Ideal.Quotient.mk_surjective y1142    obtain ⟨x, rfl⟩ := hφ z1143    exact ⟨x, rfl⟩1144  have hker : RingHom.ker ψ = Ideal.span {algebraMap O R pi, f} := by1145    ext x1146    rw [RingHom.mem_ker]1147    change Ideal.Quotient.mk _ (φ x) = 0 ↔ _1148    rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]1149    change e (Ideal.Quotient.mk I f) ∣ e (Ideal.Quotient.mk I x) ↔ _1150    rw [map_dvd_iff]1151    have h1 : Ideal.span {Ideal.Quotient.mk I f} = (Ideal.span {f}).map (Ideal.Quotient.mk I) := by1152      rw [Ideal.map_span, Set.image_singleton]1153    refine (Ideal.mem_span_singleton (x := Ideal.Quotient.mk I x)).symm.trans ?_1154    rw [h1, Ideal.mem_quotient_iff_mem_sup, Ideal.span_insert, sup_comm]1155  exact ((Submodule.quotEquivOfEq _ _ hker).symm.trans1156    (Ideal.quotientKerAlgEquivOfSurjective hψ).toLinearEquiv).length_eq1157 1158end SurfaceBlowup