Order defects and child data for the blowup recursion

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.Formula.PatternCounts7import SurfaceBlowup.Recursion.Termination8 9/-!10# Order defects and child data for the blowup recursion11 12The order defect `orderDefect O A` (the `O`-length of the generic closure of `A` modulo the13image of `A`) controls termination of the blowup recursion. This file proves its additivity14along finite-cokernel injections into products and its monotonicity in the children; the15combinatorics matching children of a tangent pattern with points of an exceptional divisor;16and the explicit completed local rings (child data) at points of the exceptional line of the17`t`-chart, including the one-chart atlas for repeated-root states.18 19## Main results20 21* `order_defect_children_sum`, `order_defect_child_le`, `etale_invariant_children`:22  `δ(A) = Σⱼ δ(Bⱼ) + ℓ` and the resulting strict decrease of the order defect.23* `cell_assignment_exists`, `concrete_member_divisor_count`: children ↔ divisor points, and24  the count of divisors with a given tangent pattern.25* `series_quotient_equiv_adjoinRoot`, `repeated_root_chart_type`,26  `repeated_root_one_chart_atlas`: the repeated-root chart.27* `t_chart_rational_point_child_data`, `t_chart_nonrational_point_child_data`,28  `cell_child_Phi_eq_map`: child data at closed points of the exceptional line.29 30Provenance: `Thm_SurfaceBlowupV2_` nodes `order_defect_{transport,children_sum,child_le}`,31`order_image_free`, `order_defect_ne_top_of_type`, `etale_invariant_children`,32`otherChildren_count`, `cell_assignment_exists`, `pattern_divisors_finite`,33`concrete_member_divisor_count`, `pi_field_quotient_equiv`, `root_cell_clauses_reindex`,34`scaled_strict_map_measurable`, `series_quotient_equiv_adjoinRoot`,35`repeated_root_{chart_type,one_chart_atlas}`, `strict_transform_map_along_point_equiv`,36`divisor_strict_transform_map_along_equiv`, `cell_child_Phi_eq_map`,37`t_chart_{nonrational,rational}_point_child_data`.38-/39 40open scoped BigOperators ENNReal TensorProduct41 42namespace SurfaceBlowup43 44/-! ### Order defects -/45 46private theorem length_quotient_map_add (O : Type) [CommRing O] (N C : Type) [AddCommGroup N]47    [Module O N]48    [AddCommGroup C] [Module O C] (j : N →ₗ[O] C) (hj : Function.Injective j) (P : Submodule O N) :49    Module.length O (C ⧸ P.map j) = Module.length O (N ⧸ P) +50        Module.length O (C ⧸ LinearMap.range j) := by51  have hle : P.map j ≤ LinearMap.range j := by52    rintro _ ⟨x, _, rfl⟩; exact ⟨x, rfl⟩53  let f : (N ⧸ P) →ₗ[O] (C ⧸ P.map j) := P.mapQ (P.map j) j (fun x hx ↦ ⟨x, hx, rfl⟩)54  let g : (C ⧸ P.map j) →ₗ[O] (C ⧸ LinearMap.range j) := Submodule.factor hle55  refine Module.length_eq_add_of_exact f g ?_ ?_ ?_56  · rw [← LinearMap.ker_eq_bot, eq_bot_iff]57    intro x hx58    induction x using Submodule.Quotient.induction_on with59    | H y =>60    rw [LinearMap.mem_ker] at hx61    change Submodule.Quotient.mk (j y) = 0 at hx62    rw [Submodule.Quotient.mk_eq_zero] at hx63    obtain ⟨z, hz, hzy⟩ := hx64    rw [hj hzy] at hz65    simpa using hz66  · exact Submodule.factor_surjective hle67  · intro x68    induction x using Submodule.Quotient.induction_on with69    | H c =>70    change Submodule.Quotient.mk c = 0 ↔ _71    rw [Submodule.Quotient.mk_eq_zero]72    constructor73    · rintro ⟨y, rfl⟩74      exact ⟨Submodule.Quotient.mk y, rfl⟩75    · rintro ⟨y, hy⟩76      induction y using Submodule.Quotient.induction_on with77      | H y =>78      change Submodule.Quotient.mk (j y) = Submodule.Quotient.mk c at hy79      rw [Submodule.Quotient.eq] at hy80      obtain ⟨z, _, hz⟩ := hy81      refine ⟨y - z, ?_⟩82      rw [map_sub, hz]; abel83 84private noncomputable def genericInclusion (O : Type) [CommRing O] [IsDomain O] (B : Type)85    [CommRing B]86    [Algebra O B]87    [Module.Finite O B] : B →ₗ[O] GenericClosure O B where88  toFun b := (⟨(1 : BaseField O) ⊗ₜ[O] b,89    (Algebra.IsIntegral.isIntegral (R := O) b).map90      (Algebra.TensorProduct.includeRight : B →ₐ[O] BaseField O ⊗[O] B)⟩ :91      integralClosure O (BaseField O ⊗[O] B))92  map_add' _ _ := Subtype.ext (TensorProduct.tmul_add _ _ _)93  map_smul' _ _ := Subtype.ext (TensorProduct.tmul_smul _ _ _)94 95private theorem orderImage_eq_range (O : Type) [CommRing O] [IsDomain O] (B : Type) [CommRing B]96    [Algebra O B]97    [Module.Finite O B] : orderImage O B = LinearMap.range (genericInclusion O B) := by98  ext x99  exact ⟨fun ⟨b, hb⟩ ↦ ⟨b, Subtype.ext hb⟩, fun ⟨b, hb⟩ ↦ ⟨b, hb ▸ rfl⟩⟩100 101private theorem genericInclusion_injective (O : Type) [CommRing O] [IsDomain O] (B : Type)102    [CommRing B] [Algebra O B]103    [Module.Finite O B] [Module.Free O B] : Function.Injective (genericInclusion O B) := by104  intro x y h105  have h2 : (1 : BaseField O) ⊗ₜ[O] x = (1 : BaseField O) ⊗ₜ[O] y := congrArg Subtype.val h106  have hinj : Function.Injective (LinearMap.rTensor B (Algebra.linearMap O (BaseField O))) :=107    Module.Flat.rTensor_preserves_injective_linearMap _ (IsFractionRing.injective O (BaseField O))108  exact (TensorProduct.lid O B).symm.injective (hinj (by simpa using h2))109 110 111/-- If `ψ : A →ₐ[O] N` is injective with `N` finite free and `ψ` becomes bijective after base112change to the fraction field, then `orderDefect O A = orderDefect O N + ℓ`, where `ℓ` is the113`O`-length of the cokernel of `ψ`. -/114private theorem order_defect_transport (O : Type) [CommRing O] [IsDomain O] (A N : Type)115    [CommRing A]116    [CommRing N] [Algebra O A] [Algebra O N] [Module.Finite O A] [Module.Finite O N]117    [Module.Free O N] (ψ : A →ₐ[O] N)118    (hbij : Function.Bijective119        (Algebra.TensorProduct.map (AlgHom.id (BaseField O) (BaseField O)) ψ))120    (ℓ : ℕ) (hℓ : Module.length O (N ⧸ LinearMap.range ψ.toLinearMap) = ℓ) :121    orderDefect O A = orderDefect O N + ℓ := by122  let Ψ := AlgEquiv.ofBijective _ hbij123  let φ : GenericClosure O A ≃ₐ[O] GenericClosure O N := (Ψ.restrictScalars O).mapIntegralClosure124  have hφ : ∀ a, φ (genericInclusion O A a) = genericInclusion O N (ψ a) := by125    intro a126    apply Subtype.ext127    change Ψ ((1 : BaseField O) ⊗ₜ[O] a) = (1 : BaseField O) ⊗ₜ[O] ψ a128    simp [Ψ]129  have hS : (orderImage O A).map φ.toLinearEquiv.toLinearMap130      = (LinearMap.range ψ.toLinearMap).map (genericInclusion O N) := by131    rw [orderImage_eq_range, LinearMap.range_eq_map, LinearMap.range_eq_map, ← Submodule.map_comp,132      ← Submodule.map_comp]133    congr 1134  have h1 : orderDefect O A = Module.length O (GenericClosure O N ⧸135      (LinearMap.range ψ.toLinearMap).map (genericInclusion O N)) := by136    unfold orderDefect137    rw [← hS]138    exact (Submodule.Quotient.equiv _ _ φ.toLinearEquiv rfl).length_eq139  rw [h1, length_quotient_map_add O N _ (genericInclusion O N) (genericInclusion_injective O N), hℓ,140    orderDefect, orderImage_eq_range, add_comm]141 142/-- Additivity of the order defect over a DVR: for an injection `ψ : A → ∏ⱼ Bⱼ` with cokernel143of length `ℓ`, `orderDefect O A = Σⱼ orderDefect O (Bⱼ) + ℓ`. -/144theorem order_defect_children_sum (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]145    (A : Type) [CommRing A] [Algebra O A] [Module.Finite O A] (n : ℕ) (B : Fin n → Type)146    [∀ j, CommRing (B j)] [∀ j, Algebra O (B j)] [∀ j, Module.Finite O (B j)]147    [∀ j, Module.Free O (B j)] (ψ : A →ₐ[O] ∀ j, B j) (hinj : Function.Injective ψ) (ℓ : ℕ)148    (hℓ : Module.length O ((∀ j, B j) ⧸ LinearMap.range ψ.toLinearMap) = ℓ) :149    orderDefect O A = ∑ j, orderDefect O (B j) + ℓ := by150  have h := baseChange_bijective_of_finite_cokernel O A (∀ j, B j) ψ.toLinearMap hinj ℓ hℓ151  have hbij : Function.Bijective152      (Algebra.TensorProduct.map (AlgHom.id (BaseField O) (BaseField O)) ψ) := by153    have : ⇑(Algebra.TensorProduct.map (AlgHom.id (BaseField O) (BaseField O)) ψ) =154      ⇑(LinearMap.baseChange (BaseField O) ψ.toLinearMap) := by155      funext x156      induction x using TensorProduct.induction_on with157      | zero => simp158      | tmul a b => simp159      | add x y hx hy => simp only [map_add, hx, hy]160    exact this ▸ h161  rw [order_defect_transport O A (∀ j, B j) ψ hbij ℓ hℓ,162    order_defect_pi]163 164/-- If `A ↪ ∏ⱼ Bⱼ` has cokernel of length `ℓ` and `A` has finite order defect, then each `Bⱼ` has165finite order defect at most that of `A`, strictly smaller when `ℓ ≥ 1`. -/166theorem order_defect_child_le (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]167    (A : Type) [CommRing A] [Algebra O A] [Module.Finite O A] (n : ℕ) (B : Fin n → Type)168    [∀ j, CommRing (B j)] [∀ j, Algebra O (B j)] [∀ j, Module.Finite O (B j)]169    [∀ j, Module.Free O (B j)] (ψ : A →ₐ[O] ∀ j, B j) (hinj : Function.Injective ψ) (ℓ : ℕ)170    (hℓ : Module.length O ((∀ j, B j) ⧸ LinearMap.range ψ.toLinearMap) = ℓ)171    (hA : orderDefect O A ≠ ⊤) :172    ∀ j, orderDefect O (B j) ≤ orderDefect O A ∧ orderDefect O (B j) ≠ ⊤ ∧173    (1 ≤ ℓ → orderDefect O (B j) < orderDefect O A) := by174  intro j175  have h := order_defect_children_sum O A n B ψ hinj ℓ hℓ176  have h1 : orderDefect O (B j) ≤ ∑ j', orderDefect O (B j') :=177    Finset.single_le_sum (f := fun j' ↦ orderDefect O (B j')) (fun _ _ ↦ zero_le)178      (Finset.mem_univ j)179  have h2 : orderDefect O (B j) ≤ orderDefect O A := h ▸ h1.trans le_self_add180  have hS : ∑ j', orderDefect O (B j') ≠ ⊤ := ne_top_of_le_ne_top hA (h ▸ le_self_add)181  refine ⟨h2, ne_top_of_le_ne_top hA h2, fun hl ↦ ?_⟩182  obtain ⟨m, hm⟩ := ENat.ne_top_iff_exists.mp hS183  refine lt_of_le_of_lt h1 ?_184  rw [h, ← hm]185  have : m < m + ℓ := by omega186  exact_mod_cast this187 188/-- For a finite free `O`-algebra `B`: `B → K ⊗[O] B` is injective, the order image of `B` is189finite free of rank `rank B`, and `K ⊗[O] B` has `K`-dimension `rank B` (`K = BaseField O`). -/190private theorem order_image_free (O : Type) [CommRing O] [IsDomain O] (B : Type) [CommRing B]191    [Algebra O B]192    [Module.Finite O B] [Module.Free O B] :193    Function.Injective194      (Algebra.TensorProduct.includeRight : B →ₐ[O] TensorProduct O (BaseField O) B) ∧195    Module.Finite O (orderImage O B) ∧ Module.Free O (orderImage O B) ∧196    Module.finrank O (orderImage O B) = Module.finrank O B ∧197    Module.finrank (BaseField O) (TensorProduct O (BaseField O) B) = Module.finrank O B := by198  have hinj : Function.Injective199      (Algebra.TensorProduct.includeRight : B →ₐ[O] TensorProduct O (BaseField O) B) :=200    Algebra.TensorProduct.includeRight_injective (IsFractionRing.injective O (FractionRing O))201  have hint : ∀ b : B,202      (Algebra.TensorProduct.includeRight : B →ₐ[O] TensorProduct O (BaseField O) B) b ∈203      integralClosure O (TensorProduct O (BaseField O) B) := fun b ↦204    (IsIntegral.of_finite O b).map _205  let ρ : B →ₗ[O] GenericClosure O B :=206    LinearMap.codRestrict (integralClosure O (TensorProduct O (BaseField O) B)).toSubmodule207      (Algebra.TensorProduct.includeRight :208        B →ₐ[O] TensorProduct O (BaseField O) B).toLinearMap hint209  have hρ : Function.Injective ρ := fun x y h ↦ hinj (congrArg Subtype.val h)210  have hrange : LinearMap.range ρ = orderImage O B := by211    ext z212    exact ⟨fun ⟨b, hb⟩ ↦ ⟨b, hb ▸ rfl⟩, fun ⟨b, hb⟩ ↦ ⟨b, Subtype.ext hb⟩⟩213  let e : B ≃ₗ[O] orderImage O B :=214    (LinearEquiv.ofInjective ρ hρ).trans (LinearEquiv.ofEq _ _ hrange)215  exact ⟨hinj, Module.Finite.equiv e, Module.Free.of_equiv e, (LinearEquiv.finrank_eq e).symm,216    Module.finrank_baseChange⟩217 218/-- A finite free algebra admitting a factorization type, over a DVR with finite residue field,219has finite order defect. -/220private theorem order_defect_ne_top_of_type (O : Type) [CommRing O] [IsDomain O]221    [IsDiscreteValuationRing O]222    [Finite (IsLocalRing.ResidueField O)] (B : Type) [CommRing B] [Algebra O B] [Module.Finite O B]223    [Module.Free O B] (σ : FactorType) (h : HasAlgebraType O B σ) :224    orderDefect O B ≠ ⊤ := by225  obtain ⟨_, _, hr⟩ := generic_closure_free_of_type O B σ h226  obtain ⟨_, _, _, hr2, hr3⟩ := order_image_free O B227  exact full_rank_free_submodule_finite_length O (GenericClosure O B) (orderImage O B)228    (by rw [hr2, hr, hr3])229 230/-- The order defects of the children `Bⱼ`, measured over their own DVRs `Oⱼ` (in which `π` stays231a uniformizer), are at most the order defect of `A`, and strictly smaller when `ℓ ≥ 1`. -/232theorem etale_invariant_children (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]233    [Finite (IsLocalRing.ResidueField O)] (n : ℕ) (Oj : Fin n → Type) [∀ j, CommRing (Oj j)]234    [∀ j, IsDomain (Oj j)] [∀ j, IsDiscreteValuationRing (Oj j)] [∀ j, Algebra O (Oj j)]235    [∀ j, Module.Finite O (Oj j)] [∀ j, Module.Free O (Oj j)] (δ : Fin n → ℕ)236    (hrank : ∀ j, Module.finrank O (Oj j) = δ j) (pi : O) (hpi : Irreducible pi)237    (hpiδ : ∀ j, Irreducible (algebraMap O (Oj j) pi)) (A : Type) [CommRing A] [Algebra O A]238    [Module.Finite O A] [Module.Free O A] (B : Fin n → Type) [∀ j, CommRing (B j)]239    [∀ j, Algebra O (B j)] [∀ j, Module.Finite O (B j)] [∀ j, Module.Free O (B j)]240    [∀ j, Algebra (Oj j) (B j)] [∀ j, IsScalarTower O (Oj j) (B j)] (ψ : A →ₐ[O] ∀ j, B j)241    (hinj : Function.Injective ψ) (ℓ : ℕ)242    (hℓ : Module.length O ((∀ j, B j) ⧸ LinearMap.range ψ.toLinearMap) = ℓ) (σ : FactorType)243    (hσ : HasAlgebraType O A σ) :244    ∀ j, (orderDefect (Oj j) (B j)).toNat ≤ (orderDefect O A).toNat ∧245    (1 ≤ ℓ → (orderDefect (Oj j) (B j)).toNat < (orderDefect O A).toNat) := by246  have hA : orderDefect O A ≠ ⊤ := order_defect_ne_top_of_type O A σ hσ247  intro j248  have h₁ := order_defect_le_of_tower O (Oj j) (δ j) (hrank j) pi hpi (hpiδ j) (B j)249  obtain ⟨h₂, _, h₃⟩ := order_defect_child_le O A n B ψ hinj ℓ hℓ hA j250  refine ⟨ENat.toNat_le_toNat (h₁.trans h₂) hA, fun h ↦ ?_⟩251  have hlt := h₁.trans_lt (h₃ h)252  have hne := ne_top_of_lt hlt253  rw [← ENat.natCast_toNat_eq_self.2 hne, ← ENat.natCast_toNat_eq_self.2 hA] at hlt254  exact_mod_cast hlt255 256/-! ### Children of a tangent pattern and exceptional divisors -/257 258/-- Multiplicities in `otherChildren w mm`: the child `(δ, single w r)` occurs `mm (δ-1, r-1)`259times (zero outside the index range), and no other single or crossing state occurs. -/260private theorem otherChildren_count (n : ℕ) (w : ℕ) (mm : Pattern n) (δ r : ℕ) :261    (otherChildren w mm).count (δ, State.single w r) =262        (if h : 1 ≤ δ ∧ δ ≤ n ∧ 1 ≤ r ∧ r ≤ n then263          (mm (⟨δ - 1, by omega⟩, ⟨r - 1, by omega⟩)).val else 0) ∧264    (∀ w' r', w' ≠ w → (otherChildren w mm).count (δ, State.single w' r') = 0) ∧265    ∀ (a' b' c' h' : ℕ), (otherChildren w mm).count (δ, State.crossing a' b' c' h') = 0 := by266  have key : ∀ v : ℕ × State, (otherChildren w mm).count v =267      ∑ ij : Fin n × Fin n,268        if (ij.1.val+1, State.single w (ij.2.val+1)) = v then (mm ij).val else 0 := by269    intro v270    unfold otherChildren271    rw [List.count_flatMap]272    rw [← Finset.sum_map_toList Finset.univ273      (fun ij : Fin n × Fin n ↦274        if (ij.1.val+1, State.single w (ij.2.val+1)) = v then (mm ij).val else 0)]275    congr 1276    apply List.map_congr_left277    intro ij _278    simp only [Function.comp, List.count_replicate]279    by_cases h : (ij.1.val+1, State.single w (ij.2.val+1)) = v <;> simp [h]280  refine ⟨?_, ?_, ?_⟩281  · rw [key]282    split_ifs with h283    · rw [Finset.sum_eq_single (⟨δ - 1, by omega⟩, ⟨r - 1, by omega⟩)]284      · rw [if_pos]285        simp [Prod.ext_iff]; omega286      · rintro ⟨i, j⟩ _ hne287        rw [if_neg]288        intro he289        simp only [Prod.mk.injEq, State.single.injEq] at he290        apply hne291        ext <;> simp <;> omega292      · simp293    · apply Finset.sum_eq_zero294      rintro ⟨i, j⟩ _295      rw [if_neg]296      intro he297      simp only [Prod.mk.injEq, State.single.injEq] at he298      have := i.2; have := j.2299      apply h; omega300  · intro w' r' hw301    rw [key]302    refine Finset.sum_eq_zero fun ij _ ↦ if_neg fun he ↦ ?_303    simp only [Prod.mk.injEq, State.single.injEq] at he304    exact hw he.2.1.symm305  · intro a b c h306    rw [key]307    exact Finset.sum_eq_zero fun ij _ ↦ if_neg (by simp)308 309open scoped Classical in310private lemma natCard_subtype_eq_filter_card {α : Type} (T : Finset α) (p : α → Prop)311    (h : ∀ x, p x → x ∈ T) :312    Nat.card {x // p x} = (T.filter p).card := by313  rw [← Nat.card_eq_finsetCard]314  exact Nat.card_congr (Equiv.subtypeEquivRight (fun x ↦ by315    simp only [Finset.mem_filter]; exact ⟨fun hp ↦ ⟨h x hp, hp⟩, fun hp ↦ hp.2⟩))316 317private lemma directionDegree_mul_le (k : Type) [Field k] (Dv : ExceptionalDivisor k)318    (Q : ClosedDirection k) : directionDegree k Q * Dv Q ≤ exceptionalDegree k Dv := by319  unfold exceptionalDegree Finsupp.sum320  by_cases hQ : Q ∈ Dv.support321  · exact Finset.single_le_sum (f := fun P ↦ directionDegree k P * Dv P)322      (fun _ _ ↦ Nat.zero_le _) hQ323  · simp [Finsupp.notMem_support_iff.mp hQ]324 325open scoped Classical in326private lemma otherChildren_count_eq_card (k : Type) [Field k] (s : State)327    (P : TangentPattern s.degree)328    (Dv : ExceptionalDivisor k)329    (hDv : HasPattern k s Dv P) (w : ℕ)330    (hw : ∀ Q, Q ∉ boundaryDirections k s → pointChildState k s P.d.val Dv Q =331        State.single w (Dv Q))332    (c : ℕ × State) :333    (otherChildren w P.other).count c =334      (Dv.support.filter (fun Q ↦ (directionDegree k Q, pointChildState k s P.d.val Dv Q) = c ∧335        Q ∉ boundaryDirections k s)).card := by336  have hfc : Dv.support.filter337      (fun Q ↦ (directionDegree k Q, pointChildState k s P.d.val Dv Q) = c ∧338        Q ∉ boundaryDirections k s) = Dv.support.filter (fun Q ↦ Q ∉ boundaryDirections k s ∧339        (directionDegree k Q, State.single w (Dv Q)) = c) :=340    Finset.filter_congr fun Q _ ↦ by341      by_cases h : Q ∈ boundaryDirections k s <;> simp [h, hw Q, and_comm]342  rw [hfc]343  have hOC := otherChildren_count s.degree w P.other344  obtain ⟨δ, st⟩ := c345  have hempty : ∀ (p : ClosedDirection k → Prop) [DecidablePred p],346      (∀ Q, Dv Q ≠ 0 → ¬ p Q) → (Dv.support.filter p).card = 0 := fun p _ hp ↦347    Finset.card_eq_zero.2 (Finset.filter_eq_empty_iff.2 fun Q hQ ↦348      hp Q (Finsupp.mem_support_iff.mp hQ))349  rcases st with ⟨w', r⟩ | ⟨a', b', c', h'⟩350  · by_cases hww : w' = w351    · subst hww352      rw [(hOC δ r).1]353      split_ifs with hc354      · have := hDv.2.2.2 (⟨δ - 1, by omega⟩, ⟨r - 1, by omega⟩)355        rw [natCard_subtype_eq_filter_card Dv.support _356          (fun Q hQ ↦ Finsupp.mem_support_iff.mpr (by simp at hQ; omega))] at this357        rw [← this]358        congr 1359        ext Q360        simp only [Finset.mem_filter, Prod.mk.injEq, State.single.injEq, true_and]361        exact ⟨fun ⟨h1, h2, _, _⟩ ↦ ⟨h1, h2, by omega⟩,362          fun ⟨h1, h2, _⟩ ↦ ⟨h1, h2, by omega, by omega⟩⟩363      · refine (hempty _ ?_).symm364        rintro Q hQ ⟨_, h2⟩365        simp only [Prod.mk.injEq, State.single.injEq, true_and] at h2366        have h5 := directionDegree_mul_le k Dv Q367        rw [hDv.1] at h5368        have := Nat.le_mul_of_pos_left (Dv Q) (directionDegree_pos k Q)369        have := Nat.le_mul_of_pos_right (directionDegree k Q) (Nat.pos_of_ne_zero hQ)370        have := P.d.isLt371        have := directionDegree_pos k Q372        exact hc (by omega)373    · rw [(hOC δ r).2.1 w' r hww]374      refine (hempty _ ?_).symm375      rintro Q _ ⟨_, h2⟩376      simp only [Prod.mk.injEq, State.single.injEq] at h2377      exact hww h2.2.1.symm378  · rw [(hOC δ 0).2.2 a' b' c' h']379    exact (hempty _ fun Q _ ⟨_, h2⟩ ↦ by simp at h2).symm380 381private lemma beq_inst_eq : (instBEqOfDecidableEq : BEq (ℕ × State)) = instBEqProd :=382  lawful_beq_subsingleton _ _383 384/-- For a divisor `Dv` with the allowed tangent pattern `P`, the children of `(s, P)` can be385matched bijectively with the support points of `Dv`, respecting degrees and child states. -/386theorem cell_assignment_exists (k : Type) [Field k] [Finite k] (s : State) (hs : s.Valid)387    (P : TangentPattern s.degree) (hP : Allowed s P) (Dv : ExceptionalDivisor k)388    (hDv : HasPattern k s Dv P) :389    Nonempty (CellAssignment k s P Dv) := by390  classical391  let g' : ClosedDirection k → ℕ × State :=392    fun Q ↦ (directionDegree k Q, pointChildState k s P.d.val Dv Q)393  let g : {Q // 0 < Dv Q} → ℕ × State := fun Q ↦ g' Q.1394  have : Finite {Q // 0 < Dv Q} :=395    (Dv.support.finite_toSet.subset fun Q hQ ↦396      Finsupp.mem_support_iff.2 (Nat.pos_iff_ne_zero.1 hQ)).to_subtype397  have hlist (b : Prop) [Decidable b] (x c : ℕ × State) :398      (if b then [] else [x]).count c = if (¬ b ∧ x = c) then 1 else 0 := by399    by_cases hb : b <;> by_cases hx : x = c <;> simp [hb, hx]400  have hnz : zeroDirection k ≠ infinityDirection k := by simp [zeroDirection, infinityDirection]401  have key : ∀ c, (children s P).count c = (Dv.support.filter (fun Q ↦ g' Q = c)).card := by402    intro c403    rw [← Finset.card_filter_add_card_filter_not (s := Dv.support.filter (fun Q ↦ g' Q = c))404      (fun Q ↦ Q ∈ boundaryDirections k s), Finset.filter_filter, Finset.filter_filter]405    have hB := otherChildren_count_eq_card k s P Dv hDv s.weight ?_ c406    rotate_left407    · intro Q hQ408      cases s <;> simp_all [pointChildState, boundaryDirections, State.weight]409    rw [← hB]410    have hA : ∀ (T : Finset (ClosedDirection k)), (∀ Q, Q ∈ boundaryDirections k s ↔ Q ∈ T) →411        (Dv.support.filter (fun Q ↦ g' Q = c ∧ Q ∈ boundaryDirections k s)).card =412          ∑ Q ∈ T, if (0 < Dv Q ∧ g' Q = c) then 1 else 0 := by413      intro T hT414      rw [← Finset.card_filter]415      congr 1416      ext Q417      simp only [Finset.mem_filter, Finsupp.mem_support_iff, hT, Nat.pos_iff_ne_zero]418      tauto419    obtain ⟨hdeg, hrt, hrx, -⟩ := hDv420    cases s with421    | single a c0 =>422      rw [hA {infinityDirection k} (by intro Q; simp [boundaryDirections])]423      simp only [children, List.count_append, hlist, Finset.sum_singleton]424      congr 1425      simp only [g', pointChildState, if_true, hrt]426      simp only [infinityDirection, directionDegree] at hrt ⊢427      simp only [Nat.pos_iff_ne_zero]428    | crossing a b c0 h0 =>429      rw [hA {infinityDirection k, zeroDirection k} (by intro Q; simp [boundaryDirections]),430        Finset.sum_pair hnz.symm]431      simp only [children, List.count_append, hlist]432      simp only at hrx433      congr 1434      have hzi : zeroDirection k = infinityDirection k ↔ False := ⟨hnz, False.elim⟩435      simp only [g', pointChildState, if_true, hzi, if_false, hrt, hrx]436      simp only [infinityDirection, directionDegree, zeroDirection, Polynomial.natDegree_X,437        Nat.pos_iff_ne_zero]438  obtain ⟨e, he⟩ := equiv_of_fiber_card_eq (Fin (children s P).length) {Q // 0 < Dv Q} (ℕ × State)439    (children s P).get g (fun c ↦ by440      rw [list_get_fiber_card_count]441      refine Eq.trans (by rw [beq_inst_eq]) ((key c).trans ?_)442      rw [Nat.card_congr443          (Equiv.subtypeSubtypeEquivSubtypeInter (fun Q ↦ 0 < Dv Q) (fun Q ↦ g' Q = c)),444        natCard_subtype_eq_filter_card Dv.support _445          (fun Q hQ ↦ Finsupp.mem_support_iff.mpr (by omega))]446      congr 1447      ext Q448      simp only [Finset.mem_filter, Finsupp.mem_support_iff, Nat.pos_iff_ne_zero]449      tauto)450  exact ⟨{ pt := fun j ↦ (e j).1451           inj := fun i j hij ↦ e.injective (Subtype.ext hij)452           supp := fun Q ↦ ⟨fun hQ ↦ ⟨e.symm ⟨Q, hQ⟩, by simp⟩, by rintro ⟨j, rfl⟩; exact (e j).2⟩453           deg := fun j ↦ congrArg Prod.fst (he j)454           state := fun j ↦ (congrArg Prod.snd (he j)).symm }⟩455 456/-- Over a finite field there are only finitely many exceptional divisors with a given tangent457pattern. -/458private theorem pattern_divisors_finite (k : Type) [Field k] [Finite k] (s : State)459    (P : TangentPattern s.degree) :460    Finite (patternDivisors k s P) := by461  set n := P.d.val with hn462  have hpos := directionDegree_pos k463  have key : ∀ D : patternDivisors k s P, ∀ Q, directionDegree k Q * D.1 Q ≤ n :=464    fun D Q ↦ (directionDegree_mul_le k D.1 Q).trans_eq D.2.1465  have hTfin : Finite {Q : ClosedDirection k // directionDegree k Q ≤ n} := by466    let f : {Q : ClosedDirection k // directionDegree k Q ≤ n} → Option (Fin (n+1) → k) :=467      fun Q ↦ Option.map (fun φ : AffineDirection k ↦ fun i : Fin (n+1) ↦ φ.val.coeff i) Q.1468    refine Finite.of_injective f ?_469    rintro ⟨_ | φ, hQ⟩ ⟨_ | ψ, hQ'⟩ h470    · rfl471    all_goals simp only [f, Option.map_some, Option.map_none, reduceCtorEq,472      Option.some.injEq] at h473    refine Subtype.ext (congrArg some (Subtype.ext (Polynomial.ext fun i ↦ ?_)))474    by_cases hi : i < n + 1475    · exact congrFun h ⟨i, hi⟩476    · simp only [directionDegree] at hQ hQ'477      rw [Polynomial.coeff_eq_zero_of_natDegree_lt (by omega),478        Polynomial.coeff_eq_zero_of_natDegree_lt (by omega)]479  have := hTfin480  refine Finite.of_injective481    (fun (D : patternDivisors k s P) (Q : {Q : ClosedDirection k // directionDegree k Q ≤ n}) ↦482      (⟨min (D.1 Q.1) n, by omega⟩ : Fin (n+1))) ?_483  intro D D' h484  apply Subtype.ext485  apply Finsupp.ext486  intro Q487  have hb : ∀ E : patternDivisors k s P, E.1 Q ≤ n := by488    intro E489    have := key E Q490    have := hpos Q491    nlinarith492  by_cases hQ : directionDegree k Q ≤ n493  · have := congrFun h ⟨Q, hQ⟩494    simp only [Fin.mk.injEq] at this495    have := hb D; have := hb D'496    omega497  · have z : ∀ E : patternDivisors k s P, E.1 Q = 0 := by498      intro E499      by_contra hne500      have := key E Q501      have : 1 ≤ E.1 Q := Nat.pos_of_ne_zero hne502      nlinarith503    rw [z D, z D']504 505/-- For a concrete member the pattern-divisor sets are finite, and for nonterminal states the506number of divisors with an allowed pattern `P` is `tangentCount s P` evaluated at `q`. -/507theorem concrete_member_divisor_count (m : ConcreteMember) :508    (∀ P : TangentPattern m.s.degree,509        Finite (patternDivisors (IsLocalRing.ResidueField m.R) m.s P)) ∧510    (m.s.terminal = false → ∀ P : TangentPattern m.s.degree, Allowed m.s P →511        ((Nat.card (patternDivisors (IsLocalRing.ResidueField m.R) m.s P) : ℕ) : ℚ) =512        (tangentCount m.s P).eval (m.toMeasured.q : ℚ)) := by513  have hfin : Finite (IsLocalRing.ResidueField m.R) :=514    Finite.of_equiv _ m.S.residueEquiv.toEquiv515  refine ⟨fun P ↦ pattern_divisors_finite _ m.s P, fun _ P hP ↦ ?_⟩516  rw [(pattern_divisor_count _ m.s P hP).2]517  congr 2518  exact Nat.card_congr m.S.residueEquiv.toEquiv.symm519 520/-! ### Auxiliary algebra and measurability -/521 522/-- Every quotient of a finite product of fields `∏ᵢ Lᵢ` is the product of the factors over some523subset `S`, compatibly with the coordinate projections. -/524theorem pi_field_quotient_equiv (K : Type) [Field K] (ι : Type) [Finite ι] (L : ι → Type)525    [∀ i, Field (L i)] [∀ i, Algebra K (L i)] (I : Ideal (∀ i, L i)) :526    ∃ (S : Finset ι) (e : ((∀ i, L i) ⧸ I) ≃ₐ[K] (∀ i : S, L i.1)), ∀ (x : ∀ i, L i) (i : S),527    e (Ideal.Quotient.mk I x) i = x i.1 := by528  have := Fintype.ofFinite ι529  classical530  let S : Finset ι := Finset.univ.filter (fun i ↦ (Pi.single i (1 : L i) : ∀ j, L j) ∉ I)531  let π : (∀ i, L i) →ₐ[K] (∀ i : S, L i.1) :=532    AlgHom.pi (fun i : S ↦ Pi.evalAlgHom K L i.1)533  have hπ : ∀ x i, π x i = x i.1 := fun x i ↦ rfl534  have hsurj : Function.Surjective π := by535    intro y536    refine ⟨fun i ↦ if h : i ∈ S then y ⟨i, h⟩ else 0, ?_⟩537    funext i538    rw [hπ]539    simp [i.2]540  have hker : I = RingHom.ker π := by541    ext x542    rw [RingHom.mem_ker]543    constructor544    · intro hx545      funext i546      rw [hπ]547      by_contra hne548      have hi := i.2549      simp only [S, Finset.mem_filter, Finset.mem_univ, true_and] at hi550      apply hi551      have : (Pi.single i.1 (1 : L i.1) : ∀ j, L j) = Pi.single i.1 ((x i.1)⁻¹) * x := by552        funext j553        by_cases hj : j = i.1554        · subst hj; simp [inv_mul_cancel₀ hne]555        · simp [hj]556      rw [this]557      exact I.mul_mem_left _ hx558    · intro hx559      rw [← Finset.univ_sum_single x]560      refine I.sum_mem fun i _ ↦ ?_561      by_cases hi : i ∈ S562      · rw [show x i = 0 from congrFun hx ⟨i, hi⟩, Pi.single_zero]563        exact I.zero_mem564      simp only [S, Finset.mem_filter, Finset.mem_univ, true_and, not_not] at hi565      rw [← mul_one (x i), Pi.single_mul]566      exact I.mul_mem_left _ hi567  refine ⟨S, (Ideal.quotientEquivAlgOfEq K hker).trans568    (Ideal.quotientKerAlgEquivOfSurjective hsurj), fun x i ↦ ?_⟩569  simp [Ideal.quotientEquivAlgOfEq_mk, hπ]570 571/-- The measurability and mass clauses for the set of `z` with `HasPolynomialTypeF` of the monic572polynomial of `π • z` transport along an equality of dimensions `n = r`. -/573theorem root_cell_clauses_reindex (O : Type) [CommRing O] [IsDomain O] [TopologicalSpace O]574    [IsTopologicalRing O] [CompactSpace O] [T2Space O] [SecondCountableTopology O]575    [MeasurableSpace O] [BorelSpace O] (pi : O) (σ : FactorType) (v : ℝ≥0∞) (n r : ℕ) (h : n = r)576    (hn : MeasurableSet {z : Fin n → O | HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ} ∧577        coefficientMeasure O n578          {z : Fin n → O | HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ} = v) :579    MeasurableSet {z : Fin r → O | HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ} ∧580    coefficientMeasure O r {z : Fin r → O | HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ} =581        v := by582  subst h; exact hn583 584/-- The scaled strict normalizer map is measurable for the adic cylinder σ-algebra: it factors as585a continuous linear part after a measurable adic perturbation. -/586theorem scaled_strict_map_measurable (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (n : ℕ)587    (pi : O) (a : ℕ) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))588    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (H : (Fin n → O) →ₗ[O] R) (k : ℕ)589    (ha : k < a) (Q : (Fin n → O) →ₗ[O] (Fin n → O))590    (hQ : ∀ w, normalizationLinearPart E H (Q w) = (pi ^ k) • w)591    [IsAdicComplete (Ideal.span {pi}) (Fin n → O)] [TopologicalSpace (Fin n → O)]592    [MeasurableSpace (Fin n → O)] [BorelSpace (Fin n → O)]593    (hgen : ‹MeasurableSpace (Fin n → O)› = adicCylinderSpace (Ideal.span {pi}) (Fin n → O))594    (hcont : Continuous (fun z : Fin n → O ↦ (pi^a) • normalizationLinearPart E H z)) :595    Measurable (scaledStrictMap pi a b E H) := by596  have h1 : scaledStrictMap pi a b E H =597    (fun z : Fin n → O ↦ (pi^a) • normalizationLinearPart E H z) ∘598    adicPerturb (normalizationCorrection pi a k b E H Q) := by599    funext z600    exact strict_normalizer_factors_through_linear O R n pi a b E H k ha Q hQ z601  rw [h1]602  exact hcont.measurable.comp603    (adic_perturb_measurable O (Fin n → O) (Ideal.span {pi}) _604      (strict_correction_raises_order O R n pi a b E H k ha Q) hgen)605 606/-! ### The repeated-root chart -/607 608/-- The powers `1, x, …, x^(r-1)` form a residue basis of `R/(f)` as soon as some reduction609map `φ : R → k⟦X⟧` is surjective, sends `x` to `X`, `f` to `X^r`, scalars to their residues,610and has kernel `π R`. -/611private theorem residue_basis_of_reduction {O R : Type} [CommRing O] [IsDomain O]612    [IsDiscreteValuationRing O]613    [CommRing R] [Algebra O R] (pi : O) (hpi : Irreducible pi) (x f : R) (r : ℕ)614    (φ : R →+* PowerSeries (IsLocalRing.ResidueField O)) (hφs : Function.Surjective φ)615    (hφx : φ x = PowerSeries.X)616    (hφc : ∀ c : O, φ (algebraMap O R c) = PowerSeries.C (IsLocalRing.residue O c))617    (hφker : ∀ w : R, φ w = 0 → ∃ m' : R, w = pi • m') (hφf : φ f = PowerSeries.X ^ r) :618    ResidueBasisFamily pi (fun i : Fin r ↦ Ideal.Quotient.mk (Ideal.span {f}) (x ^ (i : ℕ))) := by619  have hφsmul (c : O) (y : R) : φ (c • y) = PowerSeries.C (IsLocalRing.residue O c) * φ y := by620    rw [show c • y = algebraMap O R c * y from Algebra.smul_def c y, map_mul, hφc]621  have hres0 (c : O) : IsLocalRing.residue O c = 0 ↔ pi ∣ c := by622    rw [IsLocalRing.residue_eq_zero_iff, hpi.maximalIdeal_eq, Ideal.mem_span_singleton]623  have hlin (c : O) (y : R) : c • Ideal.Quotient.mk (Ideal.span {f}) y =624      Ideal.Quotient.mk (Ideal.span {f}) (c • y) :=625    (map_smul (Ideal.Quotient.mkₐ O (Ideal.span {f})) c y).symm626  refine ⟨fun m ↦ ?_, fun z ⟨m', hm'⟩ i ↦ ?_⟩627  · obtain ⟨w, rfl⟩ := Ideal.Quotient.mk_surjective m628    set g := φ w with hgdef629    choose z' hz' using fun n ↦ IsLocalRing.residue_surjective (PowerSeries.coeff n g)630    obtain ⟨h', hh'⟩ : ∃ h', φ h' = PowerSeries.mk fun i ↦ PowerSeries.coeff (i + r) g :=631      hφs _632    have htr : ((PowerSeries.trunc r g : Polynomial _) : PowerSeries _) =633        ∑ i : Fin r, PowerSeries.C (PowerSeries.coeff (i : ℕ) g) * PowerSeries.X ^ (i : ℕ) := by634      rw [PowerSeries.trunc_apply, ← Finset.range_eq_Ico, Fin.sum_univ_eq_sum_range635        (fun n ↦ PowerSeries.C (PowerSeries.coeff n g) * PowerSeries.X ^ n),636        ← Polynomial.coeToPowerSeries.ringHom_apply, map_sum]637      refine Finset.sum_congr rfl fun n _ ↦ ?_638      rw [Polynomial.coeToPowerSeries.ringHom_apply, Polynomial.coe_monomial,639        PowerSeries.monomial_eq_C_mul_X_pow]640    have key : φ (w - ∑ i : Fin r, z' i • x ^ (i : ℕ) - f * h') = 0 := by641      rw [map_sub, map_sub, map_mul, hφf, hh', map_sum]642      simp_rw [hφsmul, hz', map_pow, hφx]643      rw [← hgdef]644      linear_combination PowerSeries.eq_X_pow_mul_shift_add_trunc r g + htr645    obtain ⟨m', hm'⟩ := hφker _ key646    refine ⟨fun i ↦ z' i, Ideal.Quotient.mk _ m', ?_⟩647    simp_rw [hlin, ← map_sum, ← map_add]648    rw [Ideal.Quotient.eq, Ideal.mem_span_singleton']649    exact ⟨h', by linear_combination -hm'⟩650  · obtain ⟨w', rfl⟩ := Ideal.Quotient.mk_surjective m'651    simp_rw [hlin, ← map_sum] at hm'652    obtain ⟨c, hc⟩ := Ideal.mem_span_singleton'.1 (Ideal.Quotient.eq.1 hm')653    have h2 := congrArg φ hc654    rw [map_mul, map_sub, hφsmul, map_sum, hφf, (hres0 pi).2 dvd_rfl, map_zero, zero_mul,655      sub_zero] at h2656    have h3 := congrArg (PowerSeries.coeff (i : ℕ)) h2657    rw [PowerSeries.coeff_mul_X_pow', if_neg (by omega), map_sum] at h3658    simp_rw [hφsmul, map_pow, hφx, PowerSeries.coeff_C_mul_X_pow] at h3659    rw [Finset.sum_eq_single i (fun j _ hj ↦ if_neg (fun h ↦ hj (Fin.ext h).symm))660      (by simp), if_pos rfl] at h3661    exact (hres0 _).1 h3.symm662 663/-- For monic `F` of degree `r > 0` whose lower coefficients lie in the maximal ideal, the664quotient of the concrete surface `(1, 1, 0)` by `F(x)` is `O`-isomorphic to `AdjoinRoot F`,665compatibly with evaluation of polynomials at `x`. -/666theorem series_quotient_equiv_adjoinRoot (O : Type) [CommRing O] [IsDomain O](7.1)667    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (pi : O)668    (hpi : Irreducible pi) (F : Polynomial O) (hF : F.Monic) (r : ℕ) (hr : 0 < r)669    (hdeg : F.natDegree = r) (hred : ∀ i : ℕ, i < r → F.coeff i ∈ IsLocalRing.maximalIdeal O) :670    ∃ e : (ConcreteSurface O pi 1 1 0 ⧸671        Ideal.span {Polynomial.aeval (surfaceX O pi 1 1 0) F}) ≃ₐ[O] AdjoinRoot F,672      ∀ P : Polynomial O, e (Ideal.Quotient.mk673        (Ideal.span {Polynomial.aeval (surfaceX O pi 1 1 0) F})674        (Polynomial.aeval (surfaceX O pi 1 1 0) P)) = AdjoinRoot.mk F P := by675  set R := ConcreteSurface O pi 1 1 0676  set x : R := surfaceX O pi 1 1 0677  set f : R := Polynomial.aeval x F with hfdef678  obtain ⟨hC, -, hX, -, -⟩ := residueKillT_apply_ker O pi hpi679  have hT : algebraMap O R pi = surfaceT O pi 1 1 0 := by680    rw [concrete_surface_vertical]; simp [surfaceUnit]681  -- `φ : R → k⟦X⟧` is reduction modulo `T = π`.682  obtain ⟨q, hq⟩ := concrete_surface_quotient_T_equiv O pi hpi 1 1 0 one_pos683  let φ : R →+* PowerSeries (IsLocalRing.ResidueField O) :=684    q.toRingHom.comp (Ideal.Quotient.mk (Ideal.span {surfaceT O pi 1 1 0}))685  have hφx : φ x = PowerSeries.X := (hq _).trans hX686  have hφc (c : O) : φ (algebraMap O R c) = PowerSeries.C (IsLocalRing.residue O c) :=687    (hq (MvPowerSeries.C c)).trans (hC c)688  have hφker (w : R) (hw : φ w = 0) : ∃ m' : R, w = pi • m' := by689    obtain ⟨m', hm'⟩ := Ideal.mem_span_singleton'.1690      (Ideal.Quotient.eq_zero_iff_mem.1 (q.injective (hw.trans (map_zero q).symm)))691    exact ⟨m', by rw [← hm', ← hT, mul_comm]; exact (Algebra.smul_def _ _).symm⟩692  have hφf : φ f = PowerSeries.X ^ r := by693    have hFbar : F.map (IsLocalRing.residue O) = Polynomial.X ^ r := by694      ext i695      rw [Polynomial.coeff_map, Polynomial.coeff_X_pow]696      rcases lt_trichotomy i r with h | rfl | h697      · rw [if_neg h.ne, (IsLocalRing.residue_eq_zero_iff _).2 (hred i h)]698      · rw [if_pos rfl, ← hdeg, hF.coeff_natDegree, map_one]699      · rw [if_neg h.ne', Polynomial.coeff_eq_zero_of_natDegree_lt (hdeg ▸ h), map_zero]700    rw [hfdef, Polynomial.aeval_def, Polynomial.hom_eval₂, hφx,701      show φ.comp (algebraMap O R) = PowerSeries.C.comp (IsLocalRing.residue O) from702        RingHom.ext hφc, ← Polynomial.eval₂_map, hFbar]703    simp704  have hf : Function.Injective fun w : R ⧸ Ideal.span {algebraMap O R pi} ↦705      Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f * w := by706    rw [hT]707    refine fun w w' h ↦ q.injective (mul_left_cancel₀ (a := q (Ideal.Quotient.mk _ f)) ?_708      (by simpa only [map_mul] using congrArg q h))709    change φ f ≠ 0710    rw [hφf]; exact pow_ne_zero _ PowerSeries.X_ne_zero711  have hβ := residue_basis_of_reduction pi hpi x f r φ712    (q.surjective.comp Ideal.Quotient.mk_surjective) hφx hφc hφker hφf713  obtain ⟨B, hB⟩ := concrete_surface_curve_basis O pi hpi 1 1 0 one_pos f hf _ hβ714  subst hdeg715  let ψ : AdjoinRoot F →ₐ[O] R ⧸ Ideal.span {f} :=716    AdjoinRoot.liftAlgHom F (Algebra.ofId O _) (Ideal.Quotient.mk _ x)717      ((Polynomial.aeval_algHom_apply (Ideal.Quotient.mkₐ O _) x F).trans718        (Ideal.Quotient.eq_zero_iff_mem.2 (Ideal.subset_span rfl)))719  have hψ (P : Polynomial O) :720      ψ (AdjoinRoot.mk F P) = Ideal.Quotient.mk (Ideal.span {f}) (Polynomial.aeval x P) :=721    (AdjoinRoot.liftAlgHom_mk ..).trans (Polynomial.aeval_algHom_apply (Ideal.Quotient.mkₐ O _) x P)722  let pb := AdjoinRoot.powerBasis' hF723  let L : AdjoinRoot F ≃ₗ[O] R ⧸ Ideal.span {f} := pb.basis.equiv B (Equiv.refl _)724  have hψL : ψ.toLinearMap = L.toLinearMap := pb.basis.ext fun i ↦ by725    rw [AlgHom.toLinearMap_apply, LinearEquiv.coe_coe,726      show L (pb.basis i) = B i from Module.Basis.equiv_apply _ _ _ _]727    refine Eq.trans ?_ (hB i).symm728    rw [pb.basis_eq_pow, AdjoinRoot.powerBasis'_gen, ← AdjoinRoot.mk_X, ← map_pow, hψ, map_pow,729      Polynomial.aeval_X]730  have hbij : Function.Bijective ψ := by731    rw [show ⇑ψ = ⇑L from congrArg DFunLike.coe hψL]; exact L.bijective732  refine ⟨(AlgEquiv.ofBijective ψ hbij).symm, fun P ↦ ?_⟩733  rw [AlgEquiv.symm_apply_eq, AlgEquiv.ofBijective_apply, hψ]734 735/-- In the repeated-root chart `x^r` with basis `(x^i)`, the coordinate ideal of `z` has algebra736type `σ` iff the monic polynomial with lower coefficients `π • z` has polynomial type `σ`. -/737theorem repeated_root_chart_type (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]738    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)739    (hpi : Irreducible pi) (r : ℕ) (hr : 0 < r) (z : Fin r → O) (σ : FactorType) :740    HasAlgebraType O (ConcreteSurface O pi 1 1 0 ⧸ coordinateIdeal pi (surfaceX O pi 1 1 0 ^ r)741        (fun i : Fin r ↦ surfaceX O pi 1 1 0 ^ i.val) z) σ ↔742    HasPolynomialTypeF O (monicPolynomial O (pi • z)) σ := by743  obtain ⟨hm, hd, hc, -⟩ := monic_poly_reconstruct O r (pi • z)744  have hI : coordinateIdeal pi (surfaceX O pi 1 1 0 ^ r)745      (fun i : Fin r ↦ surfaceX O pi 1 1 0 ^ i.val) z746      = Ideal.span {Polynomial.aeval (surfaceX O pi 1 1 0) (monicPolyO (pi • z))} := by747    unfold coordinateIdeal normalizedIdeal normalizedGenerator coordinateLift748    congr 2749    simp [monicPolyO, Polynomial.aeval_add, Algebra.smul_def, mul_assoc]750  have hred : ∀ i : ℕ, i < r → (monicPolyO (pi • z)).coeff i ∈ IsLocalRing.maximalIdeal O := by751    intro i hi752    have := hc ⟨i, hi⟩753    simp only at this754    rw [this, (IsDiscreteValuationRing.irreducible_iff_uniformizer pi).1 hpi]755    exact Ideal.mem_span_singleton.2 ⟨z ⟨i, hi⟩, by simp⟩756  obtain ⟨e, -⟩ := series_quotient_equiv_adjoinRoot O pi hpi _ hm r hr hd hred757  rw [hI, ← monicPolyO_map_fraction, polynomial_type_iff_algebra_type O _ hm]758  exact ⟨algebra_type_algEquiv O _ _ e σ, algebra_type_algEquiv O _ _ e.symm σ⟩759 760/-- The quotient of the concrete surface `(1, 1, 0)` by `x^n` (`n > 0`) has the `O`-basis761`1, x, …, x^(n-1)`. -/762private theorem surface_quotient_xpow_basis (O : Type) [CommRing O] [IsDomain O]763    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] (pi : O)764    (hpi : Irreducible pi) (n : ℕ) (hn : 0 < n) :765    ∃ B : Module.Basis (Fin n) O766        (ConcreteSurface O pi 1 1 0 ⧸ Ideal.span {surfaceX O pi 1 1 0 ^ n}),767      ∀ i, B i = Ideal.Quotient.mk (Ideal.span {surfaceX O pi 1 1 0 ^ n})768        (surfaceX O pi 1 1 0 ^ i.val) := by769  set x := surfaceX O pi 1 1 0770  obtain ⟨φ, hφ⟩ := series_quotient_equiv_adjoinRoot O pi hpi (Polynomial.X ^ n)771    (Polynomial.monic_X_pow n) n hn (Polynomial.natDegree_X_pow n)772    (fun i hi ↦ by simp [Polynomial.coeff_X_pow, hi.ne])773  generalize hg : Polynomial.aeval x (Polynomial.X ^ n : Polynomial O) = g at φ hφ774  simp only [map_pow, Polynomial.aeval_X] at hg775  subst hg776  let pb := AdjoinRoot.powerBasis' (Polynomial.monic_X_pow (R := O) n)777  refine ⟨(pb.basis.reindex (finCongr (Polynomial.natDegree_X_pow n))).map778    φ.symm.toLinearEquiv, fun i ↦ ?_⟩779  apply φ.injective780  have := hφ (Polynomial.X ^ i.val)781  simp only [Polynomial.aeval_X_pow] at this782  rw [this, Module.Basis.map_apply, Module.Basis.reindex_apply, pb.basis_eq_pow]783  simp [pb, map_pow, AdjoinRoot.mk_X]784  rfl785 786/-- The state `single 1 r` on the concrete surface `(1, 1, 0)` admits a one-chart ideal atlas,787with chart `x^r` and basis `(x^i)`, whose state measure is `q⁻ʳ` times the pushforward of the788coefficient measure under the coordinate ideal map. -/789theorem repeated_root_one_chart_atlas (O : Type) [CommRing O] [IsDomain O](7.1)790    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]791    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]792    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]793    (pi : O) (hpi : Irreducible pi)794    [IsDomain (ConcreteSurface O pi 1 1 0)] [IsRegularLocalRing (ConcreteSurface O pi 1 1 0)]795    (S : SurfaceData O (ConcreteSurface O pi 1 1 0)) (hSpi : S.pi = pi)796    (hSt : S.t = surfaceT O pi 1 1 0) (hSa : S.a = 1)797    (hSb : S.b = 0) (r : ℕ) (hr : 0 < r) :798    ∃ A : IdealAtlas O (ConcreteSurface O pi 1 1 0) S.pi (State.single 1 r).degree799      (surfaceStateSet O (ConcreteSurface O pi 1 1 0) S (State.single 1 r)),800    ∃ i₀ : A.ι, (∀ i, i = i₀) ∧801    (A.chart i₀).f = (surfaceX O pi 1 1 0) ^ (State.single 1 r).degree ∧802    (A.chart i₀).b = (fun i : Fin (State.single 1 r).degree ↦ (surfaceX O pi 1 1 0) ^ i.val) ∧803    (letI : MeasurableSpace (Ideal (ConcreteSurface O pi 1 1 0)) :=804      idealChartSigma O (ConcreteSurface O pi 1 1 0) S.pi805    stateMeasure O (ConcreteSurface O pi 1 1 0) S.pi (State.single 1 r).degree806      (Nat.card (IsLocalRing.ResidueField O)) A =807    ((Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ (State.single 1 r).degree) •808      (coefficientMeasure O (State.single 1 r).degree).map809        (coordinateIdeal S.pi ((surfaceX O pi 1 1 0) ^ (State.single 1 r).degree)810          (fun i : Fin (State.single 1 r).degree ↦ (surfaceX O pi 1 1 0) ^ i.val))) := by811  set n := (State.single 1 r).degree with hn_def812  have hn : n = r := by simp [n, State.degree]813  set R := ConcreteSurface O pi 1 1 0814  set k := IsLocalRing.ResidueField O815  set x : R := surfaceX O pi 1 1 0816  obtain ⟨e, he⟩ := concrete_surface_special_fiber_equiv O pi hpi 1 1 0817  have hpar := concrete_surface_special_fiber_equiv_parameters O pi 1 1 0 e he818  -- the image of `x^n` in the special fibre819  have hex : e (Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) (x ^ n)) =820      Ideal.Quotient.mk (monomialIdeal k 1 0) (axisX k ^ n) := by821    rw [map_pow, map_pow, hpar.2.1, fiberX, map_pow]822  have hcont : contact (Ideal.Quotient.mk (monomialIdeal k 1 0) (axisX k ^ n))823      (fiberT k 1 0) = r := by824    rw [contact_fiberT_eq_axisQuotientLength _ 1 0 one_pos,825      axisQuotientLength_eq _ (by decide : (0 : Fin 2) ≠ 1) _ n, hn]826    · intro j hj827      rw [axisX, MvPowerSeries.coeff_X_pow, if_neg]828      intro h829      have := congrArg (fun m ↦ m 1) h830      simp at this; omega831    · rw [axisX, MvPowerSeries.coeff_X_pow, if_pos rfl]; exact one_ne_zero832  have hxne : x ^ n ≠ 0 := by833    intro h834    rw [h, map_zero, map_zero, ← map_zero (Ideal.Quotient.mk (monomialIdeal k 1 0))] at hex835    rw [← hex, contact_fiberT_eq_axisQuotientLength _ 1 0 one_pos,836      axisQuotientLength_eq_top _ (by decide : (0 : Fin 2) ≠ 1) _ (fun j ↦ by simp)] at hcont837    exact ENat.top_ne_natCast r hcont838  have hreg : Function.Injective fun y : R ⧸ Ideal.span {algebraMap O R pi} ↦839      y * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) (x ^ n) := by840    have h501 := concrete_surface_residue_regular_of_special_fiber O pi 1 1 0 _ e841      (special_fiber_single_contact_regular k 1 r one_pos _ (hex ▸ hcont))842    intro a b hab843    apply h501844    change _ * a = _ * b845    rw [mul_comm _ a, mul_comm _ b]; exact hab846  obtain ⟨B, hB⟩ := surface_quotient_xpow_basis O pi hpi n (hn ▸ hr)847  obtain ⟨E, hE⟩ := division_linear_equivalence O R n (x ^ n) B (fun i ↦ x ^ i.val)848    (fun i ↦ (hB i).symm) hxne849  let c₀ : IdealChart O R pi n := ⟨x ^ n, fun i ↦ x ^ i.val, E, hE, hreg⟩850  have hcover : surfaceStateSet O R S (State.single 1 r) =851      residueIdealCell (algebraMap O R pi) (x ^ n) := by852    have hcard := single_residue_ideal_count k 1 r one_pos853    rw [one_mul, Nat.sub_self, pow_zero, Nat.card_eq_one_iff_unique] at hcard854    obtain ⟨hsub, hne⟩ := hcard855    let I0 : singleResidueIdeals k 1 r :=856      ⟨Ideal.span {Ideal.Quotient.mk (monomialIdeal k 1 0) (axisX k ^ n)}, _, rfl, hcont⟩857    obtain ⟨h1, -⟩ := concrete_single_state_eq_union_cells O pi 1 1 one_pos S hSt hSa hSb e he r hr858      (fun _ ↦ x ^ n) (fun I ↦ by859        rw [hex]; exact congrArg Subtype.val (Subsingleton.elim I0 I))860    rw [h1]861    exact Set.iUnion_const _862  rw [hSpi]863  refine ⟨⟨Unit, fun _ ↦ c₀, ?_, ?_⟩, (), fun _ ↦ rfl, rfl, rfl, ?_⟩864  · rw [hcover]; exact (Set.iUnion_const _).symm865  · exact Subsingleton.pairwise866  · simp only [stateMeasure, Fintype.sum_unique]; rfl867 868/-! ### Child data at points of the exceptional line -/869 870/-- Transporting the strict transform at a point of a blowup chart along a ring isomorphism of871its completed local ring gives the strict transform ideal for the composite map. -/872private theorem strict_transform_map_along_point_equiv (O R : Type) [CommRing O] [CommRing R]873    [Algebra O R]874    (t x : R) (P : Ideal (BlowupChart R t x)) [P.IsPrime] (S' : Type) [CommRing S'] [Algebra O S']875    (Eq : CompletedLocalAt (BlowupChart R t x) P ≃+* S') (alpha : R →ₐ[O] S')876    (halpha : ∀ r : R, alpha r = Eq (completedPointMap (BlowupChart R t x) P (chartBase R t x r)))877    (d : ℕ) (J : Ideal R) :878    Ideal.map (Eq : CompletedLocalAt (BlowupChart R t x) P →+* S') (strictTransformAt R t x P d J) =879        strictTransformIdeal alpha880        (Eq (completedPointMap (BlowupChart R t x) P (chartBase R t x t))) d J := by881  unfold strictTransformAt strictTransformIdeal882  have h1 : J.map alpha.toRingHom =883    (J.map ((completedPointMap (BlowupChart R t x) P).comp884    (chartBase R t x))).map (Eq : CompletedLocalAt (BlowupChart R t x) P →+* S') := by885    rw [Ideal.map_map]886    congr 1887    ext r888    exact halpha r889  rw [h1, ← map_pow]890  generalize J.map ((completedPointMap (BlowupChart R t x) P).comp (chartBase R t x)) = I891  generalize (completedPointMap (BlowupChart R t x) P (chartBase R t x t)) ^ d = z892  ext y893  have key : ∀ (K : Ideal (CompletedLocalAt (BlowupChart R t x) P)) w, w ∈894    K.map (Eq : CompletedLocalAt (BlowupChart R t x) P →+* S') ↔ Eq.symm w ∈ K := by895    intro K w896    have := Ideal.comap_symm (I := K) Eq897    exact (Iff.of_eq (congrArg (w ∈ ·) this.symm))898  rw [key, Submodule.mem_colon_singleton, Submodule.mem_colon_singleton, key, smul_eq_mul,899    smul_eq_mul]900  simp901 902/-- The divisor strict transform at a support point, transported along a ring isomorphism of its903local ring, is the strict transform ideal for the composite map. -/904private theorem divisor_strict_transform_map_along_equiv (R : Type) [CommRing R] (t x : R)905    [IsLocalRing R]906    (e : (BlowupChart R t x ⧸ chartExceptional R t x) ≃+* Polynomial (IsLocalRing.ResidueField R))907    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R)) (hinf : (infinityPoint R t x).IsPrime)908    (Q : divisorSupport Dv) (O S' : Type) [CommRing O] [Algebra O R] [CommRing S'] [Algebra O S']909    (E : divisorLocalRing R t x e Dv hinf Q ≃+* S') (alpha : R →ₐ[O] S')910    (halpha : ∀ r : R, alpha r = E (divisorFromSurface R t x e Dv hinf Q r)) (d : ℕ) (J : Ideal R) :911    Ideal.map (E : divisorLocalRing R t x e Dv hinf Q →+* S')912        (divisorStrictTransform R t x e Dv hinf d J Q) =913        strictTransformIdeal alpha (E (divisorException R t x e Dv hinf Q)) d J := by914  rcases Q with ⟨_ | φ, h⟩915  · exact @strict_transform_map_along_point_equiv O R _ _ _ x t (infinityPoint R t x) hinf S' _ _916      E alpha halpha d J917  · exact @strict_transform_map_along_point_equiv O R _ _ _ t x (directionPoint R t x e φ)918      (directionPoint_isPrime R t x e φ) S' _ _ E alpha halpha d J919 920/-- The child map `D.Φ` of cell child data is the image of the divisor strict transform under921the identification `D.Eq j` of local rings. -/922theorem cell_child_Phi_eq_map (m : ConcreteMember) (c : m.cellIndex) (D : CellChildData m c)923    (J : Ideal m.R) (j : m.toMeasured.childIdx c) :924    D.Φ J j = Ideal.map (D.Eq j : divisorLocalRing m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j) →+*925        (D.mc j).R) (divisorStrictTransform m.R m.S.t m.S.x D.e c.2.1 D.hinf926        (m.toMeasured.cellDegree c) J (D.point j)) := by927  rw [divisor_strict_transform_map_along_equiv m.R m.S.t m.S.x D.e c.2.1 D.hinf (D.point j) m.O928    (D.mc j).R (D.Eq j) (D.alpha j) (fun r ↦ rfl), D.hEq_e j]929  rfl930 931private theorem natDegree_eq_of_span_eq (R : Type) [CommRing R] (t x : R)932    [(Ideal.span ({t,x} : Set R)).IsMaximal]933    (O : Type) [CommRing O] (f : O →+* R)934    (P : Ideal (BlowupChart R t x)) [P.IsMaximal] (hP : chartBase R t x t ∈ P)935    (Φ : Polynomial O) (hΦ : Φ.Monic)936    (hspan : P = Ideal.span {chartBase R t x t,937      Polynomial.eval₂ ((chartBase R t x).comp f) (chartSlope R t x) Φ}) (δ : ℕ)938    (hdeg : Module.length R (BlowupChart R t x ⧸ P) = (δ : ℕ∞)) : Φ.natDegree = δ := by939  obtain ⟨e, he, heZ⟩ := exceptional_line_equiv_chart_exceptional R t x940  obtain ⟨φ, hmon, hirr, himg, -, hlen⟩ :=941    blowup_chart_exceptional_point_polynomial R t x e he heZ P hP942  rw [hdeg] at hlen943  have hδ : φ.natDegree = δ := by exact_mod_cast hlen.symm944  set g : O →+* (R ⧸ Ideal.span ({t,x} : Set R)) :=945    (Ideal.Quotient.mk _).comp f with hg946  have key : (P.map (Ideal.Quotient.mk (chartExceptional R t x))).map e = Ideal.span {Φ.map g} := by947    rw [hspan, Ideal.map_span, Ideal.map_span]948    have h0 : e (Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x t)) = 0 := by949      have : Ideal.Quotient.mk (chartExceptional R t x) (chartBase R t x t) = 0 :=950        Ideal.Quotient.eq_zero_iff_mem.2 (Ideal.subset_span rfl)951      rw [this, map_zero]952    have h1 : e (Ideal.Quotient.mk (chartExceptional R t x)953        (Polynomial.eval₂ ((chartBase R t x).comp f) (chartSlope R t x) Φ)) = Φ.map g := by954      have := Polynomial.hom_eval₂ Φ ((chartBase R t x).comp f)955        (e.toRingHom.comp (Ideal.Quotient.mk (chartExceptional R t x))) (chartSlope R t x)956      change (e.toRingHom.comp (Ideal.Quotient.mk (chartExceptional R t x))) _ = _957      rw [this]958      change Polynomial.eval₂ _959        (e (Ideal.Quotient.mk (chartExceptional R t x) (chartSlope R t x))) Φ =960        Polynomial.eval₂ (Polynomial.C.comp g) Polynomial.X Φ961      rw [heZ]962      congr 1963      ext r964      simp [he, hg]965    rw [Set.image_pair, Set.image_pair, h0, h1]966    simp967  rw [himg] at key968  have hassoc : Associated φ (Φ.map g) := by969    rwa [Ideal.span_singleton_eq_span_singleton] at key970  have := Polynomial.eq_of_monic_of_associated hmon (hΦ.map g) hassoc971  rw [← hδ, this, hΦ.natDegree_map]972 973/-- A closed point of degree `δ ≥ 2` on the exceptional line of the `t`-chart is cut out by an974unramified lift `Φ` of degree `δ`, and its completed local ring is a concrete surface over975`AdjoinRoot Φ` with explicit `t`-parameter and `O`-structure. -/976theorem t_chart_nonrational_point_child_data (O : Type) [CommRing O] [IsDomain O]977    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]978    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)979    (a b : ℕ) (ha : 0 < a)980    (P : Ideal (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)981        (surfaceX O pi u a b)))982    [P.IsMaximal] [P.IsPrime]983    (hP : (chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))984        (surfaceT O pi u a b) ∈ P)985    (δ : ℕ)986    (hdeg : Module.length (ConcreteSurface O pi u a b)987        ((BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) ⧸988          P) = (δ : ℕ∞))989    (h2 : 2 ≤ δ) :990    ∃ Φ : Polynomial O, IsUnramifiedLift O Φ ∧ Φ.natDegree = δ ∧991    P = Ideal.span {(chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)992        (surfaceX O pi u a b)) (surfaceT O pi u a b),993        Polynomial.eval₂ ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)994        (surfaceX O pi u a b)).comp (algebraMap O (ConcreteSurface O pi u a b)))995        (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) Φ} ∧996    ∃ (hθ : IsUnit (AdjoinRoot.root Φ))997        (Eq : CompletedLocalAt (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)998        (surfaceX O pi u a b)) P ≃+*999        ConcreteSurface (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)1000        (substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)1001        (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) *1002        shiftUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ) hθ ^ b) (a + b) 0),1003    Eq ((completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1004        (surfaceX O pi u a b)) P) ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1005        (surfaceX O pi u a b)) (surfaceT O pi u a b))) =1006        surfaceT (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)1007        (substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)1008        (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) *1009        shiftUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ) hθ ^ b) (a + b) 0 ∧1010    ∀ c : O,1011    Eq ((completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1012        (surfaceX O pi u a b)) P) ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1013        (surfaceX O pi u a b)) (algebraMap O (ConcreteSurface O pi u a b) c))) =1014        algebraMap (AdjoinRoot Φ) (ConcreteSurface (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi)1015        (substUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ)1016        (baseChangeUnit O (algebraMap O (AdjoinRoot Φ)) u) *1017        shiftUnit (AdjoinRoot Φ) (AdjoinRoot.root Φ) hθ ^ b) (a + b) 0)1018        (algebraMap O (AdjoinRoot Φ) c) := by1019  obtain ⟨e459, -⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha1020  have hmax : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} :1021      Set (ConcreteSurface O pi u a b))).IsMaximal :=1022    Ideal.Quotient.maximal_of_isField _ (e459.toMulEquiv.isField (Field.toIsField _))1023  have hspanform := concrete_chart_point_span_form O pi hpi u a b ha P hP1024  have hdeg' := natDegree_eq_of_span_eq (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1025    (surfaceX O pi u a b)1026    O (algebraMap O (ConcreteSurface O pi u a b)) P hP1027  rcases hspanform with h | ⟨α, -, h⟩ | ⟨Φ, hΦ, h2Φ, hPΦ⟩1028  · exfalso1029    have := hdeg' Polynomial.X (Polynomial.monic_X) (by simpa using h) δ hdeg1030    simp at this; omega1031  · exfalso1032    have := hdeg' (Polynomial.X - Polynomial.C α) (Polynomial.monic_X_sub_C α)1033      (by simpa [sub_eq_add_neg] using h) δ hdeg1034    rw [Polynomial.natDegree_X_sub_C] at this; omega1035  · have hnd : Φ.natDegree = δ := hdeg' Φ hΦ.1 hPΦ δ hdeg1036    have hθ := unramified_root_isUnit_of_two_le_natDegree O Φ hΦ h2Φ1037    obtain ⟨Eq, hs, -, hc, -⟩ :=1038      t_chart_nonrational_point_completion_equiv O pi hpi u a b ha Φ hΦ hθ P hPΦ1039    refine ⟨Φ, hΦ, hnd, hPΦ, hθ, Eq, ?_, hc⟩1040    have := hs (axisT O)1041    obtain ⟨-, h2, -⟩ := chartSubst_apply_generators (AdjoinRoot Φ) (AdjoinRoot.root Φ)1042    have hm : MvPowerSeries.map (algebraMap O (AdjoinRoot Φ)) (axisT O) = axisT (AdjoinRoot Φ) := by1043      simp [axisT, MvPowerSeries.map_X]1044    rwa [hm, h2] at this1045 1046private theorem not_two_le_natDegree_of_length_one (O R : Type) [CommRing O] [CommRing R]1047    (f : O →+* R) (t x : R)1048    [(Ideal.span ({t, x} : Set R)).IsMaximal] (P : Ideal (BlowupChart R t x)) [P.IsMaximal]1049    (Φ : Polynomial O) (hΦ : Φ.Monic) (h2 : 2 ≤ Φ.natDegree)1050    (hPeq : P = Ideal.span {chartBase R t x t,1051      Polynomial.eval₂ ((chartBase R t x).comp f) (chartSlope R t x) Φ})1052    (hdeg : Module.length R (BlowupChart R t x ⧸ P) = (1 : ℕ∞)) : False := by1053  obtain ⟨e1, he, heZ⟩ := exceptional_line_equiv_chart_exceptional R t x1054  have hP : chartBase R t x t ∈ P := hPeq ▸ Ideal.subset_span (by simp)1055  obtain ⟨φ, hmon, hirr, hmap, -, hlen⟩ :=1056    blowup_chart_exceptional_point_polynomial R t x e1 he heZ P hP1057  rw [hdeg] at hlen1058  have hφ : φ.natDegree = 1 := by exact_mod_cast hlen.symm1059  have hk : (Ideal.Quotient.mk (chartExceptional R t x)) (chartBase R t x t) = 0 :=1060    Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span rfl)1061  rw [hPeq, Ideal.map_span, Set.image_pair, hk, Ideal.map_span] at hmap1062  simp only [Set.image_pair] at hmap1063  have hev : e1 ((Ideal.Quotient.mk (chartExceptional R t x))1064      (Polynomial.eval₂ ((chartBase R t x).comp f) (chartSlope R t x) Φ))1065      = Φ.map ((Ideal.Quotient.mk (Ideal.span ({t, x} : Set R))).comp f) := by1066    have := Polynomial.hom_eval₂ Φ ((chartBase R t x).comp f)1067      (((e1 : _ ≃+* _).toRingHom).comp1068        (Ideal.Quotient.mk (chartExceptional R t x))) (chartSlope R t x)1069    simp only [RingHom.coe_comp, Function.comp_apply, RingEquiv.toRingHom_eq_coe,1070      RingHom.coe_coe] at this1071    rw [this, heZ]1072    simp only [Polynomial.map]1073    congr 11074    ext c1075    simp [he]1076  simp only [hev, map_zero] at hmap1077  have h0 : ∀ (K : Type) [CommRing K] (p : K), Ideal.span ({0, p} : Set K) = Ideal.span {p} := by1078    intro K _ p1079    rw [Ideal.span_insert, Ideal.span_singleton_eq_bot.mpr rfl, bot_sup_eq]1080  rw [h0] at hmap1081  obtain ⟨w, hw⟩ := Ideal.span_singleton_eq_span_singleton.mp hmap1082  have hne : (Φ.map ((Ideal.Quotient.mk (Ideal.span ({t, x} : Set R))).comp f)) ≠ 0 :=1083    (hΦ.map _).ne_zero1084  have := congrArg Polynomial.natDegree hw1085  rw [Polynomial.natDegree_mul hne w.ne_zero, Polynomial.natDegree_coe_units,1086    hΦ.natDegree_map, hφ] at this1087  omega1088 1089open scoped Classical in1090/-- A degree-one point on the exceptional line of the `t`-chart has slope `α` with `α = 0` or a1091unit, and its completed local ring is a concrete surface over `O` with explicit parameters. -/1092theorem t_chart_rational_point_child_data (O : Type) [CommRing O] [IsDomain O]1093    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1094    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)1095    (a b : ℕ) (ha : 0 < a)1096    (P : Ideal (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1097        (surfaceX O pi u a b)))1098    [P.IsMaximal] [P.IsPrime]1099    (hP : (chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))1100        (surfaceT O pi u a b) ∈ P)1101    (hdeg : Module.length (ConcreteSurface O pi u a b)1102        ((BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) ⧸1103          P) = (1 : ℕ∞)) :1104    ∃ α : O, (α = 0 ∨ IsUnit α) ∧1105    P = Ideal.span {(chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1106        (surfaceX O pi u a b)) (surfaceT O pi u a b),1107        (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) -1108        (chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b))1109        (algebraMap O (ConcreteSurface O pi u a b) α)} ∧1110    ∃ (u' : (TwoSeries O)ˣ) (Eq : CompletedLocalAt1111        (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)) P ≃+*1112        ConcreteSurface O pi u' (a + b) (if α = 0 then b else 0)),1113    Eq ((completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1114        (surfaceX O pi u a b)) P) ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1115        (surfaceX O pi u a b)) (surfaceT O pi u a b))) =1116        surfaceT O pi u' (a + b) (if α = 0 then b else 0) ∧1117    Eq ((completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1118        (surfaceX O pi u a b)) P) (chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1119        (surfaceX O pi u a b))) = surfaceX O pi u' (a + b) (if α = 0 then b else 0) +1120        algebraMap O (ConcreteSurface O pi u' (a + b) (if α = 0 then b else 0)) α ∧1121    ∀ c : O,1122    Eq ((completedPointMap (BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1123        (surfaceX O pi u a b)) P) ((chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b)1124        (surfaceX O pi u a b)) (algebraMap O (ConcreteSurface O pi u a b) c))) =1125        algebraMap O (ConcreteSurface O pi u' (a + b) (if α = 0 then b else 0)) c := by1126  obtain ⟨e, -⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha1127  have hmax : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} :1128      Set (ConcreteSurface O pi u a b))).IsMaximal :=1129    Ideal.Quotient.maximal_of_isField _ (e.toMulEquiv.isField (Field.toIsField _))1130  obtain ⟨h1, h2, h3, h4, h5, h6, -⟩ := chartSubst_apply_generators O 01131  rcases concrete_chart_point_span_form O pi hpi u a b ha P hP with h | ⟨α, hα, h⟩ | ⟨Φ, hΦ, h2', h⟩1132  · have hb : (if (0 : O) = 0 then b else 0) = b := if_pos rfl1133    obtain ⟨E, hE1, hE2, hE3⟩ := t_chart_origin_completion_equiv O pi hpi u a b ha P h1134    refine ⟨0, Or.inl rfl, ?_, ?_⟩1135    · simpa using h1136    · rw [hb]1137      refine ⟨substUnit O 0 u, E, ?_, ?_, hE3⟩1138      · have := hE1 (axisT O)1139        rwa [h2] at this1140      · simpa using hE21141  · have hα0 : α ≠ 0 := hα.ne_zero1142    have hb : (if α = 0 then b else 0) = 0 := if_neg hα01143    obtain ⟨E, hE1, hE2, hE3⟩ := t_chart_unit_point_completion_equiv O pi hpi u a b ha α hα P h1144    refine ⟨α, Or.inr hα, h, ?_⟩1145    rw [hb]1146    refine ⟨_, E, ?_, hE2, hE3⟩1147    have := hE1 (axisT O)1148    rwa [(chartSubst_apply_generators O α).2.1] at this1149  · exact (not_two_le_natDegree_of_length_one O _ (algebraMap O _) _ _ P Φ hΦ.1 h2' h hdeg).elim1150 1151end SurfaceBlowup