Expression and law algebra, children of tangent patterns

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.Basic7import Mathlib.FieldTheory.Finite.GaloisField8import Mathlib.RingTheory.AdicCompletion.Algebra9import Mathlib.RingTheory.RegularLocalRing.Defs10 11/-!12# Expression and law algebra, children of tangent patterns13 14Basic algebra of the formal expressions `Expr` (evaluation and safety of sums, products,15powers, substitutions, rational fractions) and of the formal laws `Law` (coefficients of16products, scalings, descents and flat maps), together with the elementary combinatorics of17the children of a tangent pattern and a handful of algebraic and topological facts used18throughout (coordinate cylinders, coprimality of reductions, ramification of local19extensions, finiteness of types of bounded degree).20 21## Main results22 23* `SurfaceBlowup.children_degree_identity`: `∑ e · deg(child) = deg(s)` over the children.24* `SurfaceBlowup.children_valid`: children of a valid state are valid.25* `SurfaceBlowup.expression_fraction`: evaluating a safe expression via its fraction.26* `SurfaceBlowup.lawInterp_lawMul`, `SurfaceBlowup.lawInterp_lawProd`: the interpretation of a27  law in a monoid algebra (shared by the numerical and the rational-function readings) is28  multiplicative.29* `SurfaceBlowup.law_coeff_mul`, `SurfaceBlowup.law_coeff_prod_formula`,30  `SurfaceBlowup.law_coeff_prod_descend`: coefficient formulas for products of laws.31* `SurfaceBlowup.law_coeff_nonneg_closure`: nonnegativity of coefficients is preserved by32  the law operations.33* `SurfaceBlowup.coordinate_cylinder_clopen`: congruence cylinders are clopen.34* `SurfaceBlowup.finite_flat_local_ramification_degree`: `e · f = rank` for finite flat35  local extensions.36 37Provenance: `Def_SurfaceBlowupV2_StateContact` and `Thm_SurfaceBlowupV2_*` for38children_degree_identity, children_residue_degree_pos, child_degree_le, children_valid,39coordinate_cylinder_clopen, coprime_of_monic_reduction_one, density_value_arith,40divisor_count_safe, expression_{fraction, pow_eval, pow_safe, prod_eval, regular, subst_eval,41subst_safe, sum_eval, sum_safe}, divisor_probability_safe,42finite_flat_local_ramification_degree, finite_types_of_degree, geometric_exit_sum,43image_measurable_of_continuousOn_injOn_compact, integral_local_extension_unique_prime,44law_coeff_{descend, flatMap, mul, prod_descend, prod_formula, scale, nonneg_closure},45law_safe_{descend, mul, scale}, list_get_fiber_card, monic_polynomial_degree,46other_children_count, prime_power_ge_two, projective_normalizer_positive,47rank_lt_of_degree_lt.48-/49 50open scoped BigOperators ENNReal51 52namespace SurfaceBlowup53 54/-! ### The first contact of a state -/55 56namespace State57 58/-- The contact of a state with the old boundary t = 0 (paper: c in S(a;c) and T(a,b;c,h));59for a child produced by one blowup step this is its contact r_P with the exceptional divisor E,60equation (5.1). -/61def firstContact : State → ℕ62  | .single _ c => c63  | .crossing _ _ c _ => c64 65end State66 67/-! ### Evaluation and safety of expressions -/68 69/-- Evaluation of a formal power: `(x ^ n)(q) = x(q) ^ n`. -/70theorem expression_pow_eval (x : Expr) (q : ℚ) (n : ℕ) :71    (x.pow n).eval q = (x.eval q)^n := by72  induction n with73  | zero => simp [Expr.pow, Expr.eval]74  | succ n ih => simp [Expr.pow, Expr.eval, ih, pow_succ]75 76/-- A formal power of a safe expression is safe. -/77theorem expression_pow_safe (x : Expr) (q : ℚ) (n : ℕ) (hx : x.safe q) :78    (x.pow n).safe q := by79  induction n with80  | zero => simp [Expr.pow, Expr.safe]81  | succ n ih => exact ⟨ih, hx⟩82 83/-- Evaluation of a formal product is the product of the evaluations. -/84theorem expression_prod_eval (xs : List Expr) (q : ℚ) :85    (Expr.prod xs).eval q = (xs.map (Expr.eval q)).prod := by86  induction xs <;> simp_all [Expr.prod, Expr.eval]87 88/-- A formal product of safe expressions is safe. -/89private theorem expression_prod_safe (xs : List Expr) (q : ℚ) (h : ∀ x ∈ xs, x.safe q) :90    (Expr.prod xs).safe q := by91  induction xs <;> simp_all [Expr.prod, Expr.safe]92 93/-- Evaluation of a formal sum is the sum of the evaluations. -/94theorem expression_sum_eval (xs : List Expr) (q : ℚ) :95    (Expr.sum xs).eval q = (xs.map (Expr.eval q)).sum := by96  induction xs <;> simp_all [Expr.sum, Expr.eval]97 98/-- A formal sum of safe expressions is safe. -/99theorem expression_sum_safe (xs : List Expr) (q : ℚ) (h : ∀ x ∈ xs, x.safe q) :100    (Expr.sum xs).safe q := by101  induction xs <;> simp_all [Expr.sum, Expr.safe]102 103/-- Evaluation commutes with substitution: `(x ∘ y)(q) = x(y(q))`. -/104private theorem expression_subst_eval (x y : Expr) (q : ℚ) :105    (x.subst y).eval q = x.eval (y.eval q) := by106  induction x <;> simp_all [Expr.subst, Expr.eval]107 108/-- If `y` is safe at `q` and `x` is safe at `y(q)`, then `x ∘ y` is safe at `q`. -/109private theorem expression_subst_safe (x y : Expr) (q : ℚ) (hy : y.safe q)110    (hx : x.safe (y.eval q)) :111    (x.subst y).safe q := by112  induction x with113  | const r => trivial114  | var => exact hy115  | add a b iha ihb => exact ⟨iha hx.1, ihb hx.2⟩116  | mul a b iha ihb => exact ⟨iha hx.1, ihb hx.2⟩117  | inv a iha => exact ⟨iha hx.1, by rw [expression_subst_eval]; exact hx.2⟩118 119/-- At a point where `x` is safe, the denominator of `x.fraction` does not vanish and `x`120evaluates to numerator over denominator. -/121theorem expression_fraction (x : Expr) (q : ℚ) (hx : x.safe q) :122    x.fraction.2.eval q ≠ 0 ∧ x.eval q = x.fraction.1.eval q / x.fraction.2.eval q := by123  induction x with124  | const r => simp [Expr.fraction, Expr.eval]125  | var => simp [Expr.fraction, Expr.eval]126  | add x y ihx ihy =>127    obtain ⟨hx1, hx2⟩ := ihx hx.1128    obtain ⟨hy1, hy2⟩ := ihy hx.2129    simp only [Expr.fraction, Expr.eval, Polynomial.eval_mul, Polynomial.eval_add]130    refine ⟨mul_ne_zero hx1 hy1, ?_⟩131    rw [hx2, hy2]132    field_simp133  | mul x y ihx ihy =>134    obtain ⟨hx1, hx2⟩ := ihx hx.1135    obtain ⟨hy1, hy2⟩ := ihy hx.2136    simp only [Expr.fraction, Expr.eval, Polynomial.eval_mul]137    exact ⟨mul_ne_zero hx1 hy1, by rw [hx2, hy2, div_mul_div_comm]⟩138  | inv x ihx =>139    obtain ⟨hs, hne⟩ := hx140    obtain ⟨hx1, hx2⟩ := ihx hs141    simp only [Expr.fraction, Expr.eval]142    exact ⟨fun h ↦ hne (by rw [hx2, h, zero_div]), by rw [hx2, inv_div]⟩143 144/-- The rational function of an expression is regular at every point where it is safe. -/145theorem expression_regular (x : Expr) (q : ℚ) (hx : x.safe q) :146    RegularAt x.rational q :=147  ⟨x.fraction.1, x.fraction.2, (expression_fraction x q hx).1, rfl⟩148 149/-- Positivity of the projective normalizer `1 + q + ⋯ + qⁿ` at `q ≥ 0`. -/150theorem projective_normalizer_positive (n : ℕ) (q : ℚ) (hq : 0 ≤ q) :151    0 < (projectiveNormalizer n).eval q := by152  simp only [projectiveNormalizer, expression_sum_eval, List.map_map, Function.comp_def,153    expression_pow_eval, Expr.eval, List.range_succ_eq_map, List.map_cons, List.sum_cons,154    pow_zero]155  have : 0 ≤ ((List.range n).map fun x ↦ q ^ x.succ).sum :=156    List.sum_nonneg (by simp only [List.mem_map]; rintro _ ⟨_, _, rfl⟩; positivity)157  linarith158 159/-- A prime power is at least `2`. -/160theorem prime_power_ge_two (q : ℕ) (hq : PrimePower q) :161    2 ≤ q := by162  obtain ⟨p, r, hp, hr, rfl⟩ := hq163  exact hp.two_le.trans (Nat.le_self_pow hr.ne' p)164 165/-! ### Children of tangent patterns -/166 167/-- The degree-weighted size of the "other" children is `a` times the pattern weight. -/168private theorem otherChildren_degree_sum {n : ℕ} (a : ℕ) (m : Pattern n) :169    ((otherChildren a m).map fun z ↦ z.1 * z.2.degree).sum = a * patternWeight m := by170  unfold otherChildren patternWeight171  rw [List.map_flatMap, List.flatMap_def, List.sum_flatten, List.map_map, Finset.mul_sum,172    Finset.sum_map_toList]173  refine Finset.sum_congr rfl fun ij _ ↦ ?_174  simp [List.map_replicate, List.sum_replicate, State.degree]175  ring176 177/-- Degree identity for one blowup step: for an allowed pattern, `∑ e · deg(child) = deg(s)`178over the children `(e, child)`. -/179theorem children_degree_identity (s : State) (hs : s.Valid) (P : TangentPattern s.degree)(6.5)180    (hP : Allowed s P) :181    ((children s P).map fun z ↦ z.1 * z.2.degree).sum = s.degree := by182  obtain ⟨hd, hsum, hrest⟩ := hP183  cases s with184  | single a c =>185    obtain ⟨hdc, hrx, hrt⟩ := hrest186    obtain ⟨W, hW⟩ : ∃ W, patternWeight P.other = W := ⟨_, rfl⟩187    simp only [children, List.map_append, List.sum_append, otherChildren_degree_sum, hW]188    rw [hW] at hsum189    simp only [State.degree]190    generalize P.d.val = D at *191    generalize P.rt.val = R at *192    generalize P.rx.val = X at *193    subst hrx194    obtain ⟨k, rfl⟩ : ∃ k, c = D + k := ⟨c - D, by omega⟩195    subst hsum196    split_ifs with h0197    · obtain rfl : k = 0 := by omega198      subst h0; simp199    · simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]200      rw [Nat.add_sub_cancel_left]; ring201  | crossing a b c h =>202    obtain ⟨hdc, hdh, hrt, hrx⟩ := hrest203    obtain ⟨W, hW⟩ : ∃ W, patternWeight P.other = W := ⟨_, rfl⟩204    simp only [children, List.map_append, List.sum_append, otherChildren_degree_sum, hW]205    rw [hW] at hsum206    simp only [State.degree]207    generalize P.d.val = D at *208    generalize P.rt.val = R at *209    generalize P.rx.val = X at *210    obtain ⟨k, rfl⟩ : ∃ k, c = D + k := ⟨c - D, by omega⟩211    obtain ⟨l, rfl⟩ : ∃ l, h = D + l := ⟨h - D, by omega⟩212    subst hsum213    simp only [Nat.add_sub_cancel_left]214    have e1 : R = 0 → k = 0 := by omega215    have e2 : X = 0 → l = 0 := by omega216    split_ifs <;>217      simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil] <;>218      (try (obtain rfl := e1 ‹R = 0›; subst ‹R = 0›)) <;>219      (try (obtain rfl := e2 ‹X = 0›; subst ‹X = 0›)) <;> ring220 221/-- Every child of a tangent pattern has positive residue degree. -/222theorem children_residue_degree_pos (s : State) (P : TangentPattern s.degree) (z : ℕ × State)223    (hz : z ∈ children s P) :224    0 < z.1 := by225  have hO : ∀ (a : ℕ) (m : Pattern s.degree), z ∈ otherChildren a m → 0 < z.1 := by226    intro a m h227    simp only [otherChildren, List.mem_flatMap] at h228    obtain ⟨ij, _, h⟩ := h229    simp [List.eq_of_mem_replicate h]230  cases s <;> simp only [children, List.mem_append] at hz231  · exact hz.elim (fun hz ↦ by split_ifs at hz <;> simp_all) (hO _ _)232  · exact hz.elim (fun hz ↦ by rcases hz with hz | hz <;> split_ifs at hz <;> simp_all) (hO _ _)233 234/-- Each child of an allowed pattern has degree at most that of the parent state. -/235theorem child_degree_le (s : State) (hs : s.Valid) (P : TangentPattern s.degree)236    (hP : Allowed s P) (z : ℕ × State) (hz : z ∈ children s P) :237    z.2.degree ≤ s.degree := by238  calc z.2.degree ≤ z.1*z.2.degree :=239        Nat.le_mul_of_pos_left _ (children_residue_degree_pos s P z hz)240    _ ≤ ((children s P).map fun z ↦ z.1*z.2.degree).sum :=241        List.single_le_sum (by simp) _ (List.mem_map.2 ⟨z, hz, rfl⟩)242    _ = _ := children_degree_identity s hs P hP243 244/-- Children of an allowed pattern on a valid state are valid states. -/245theorem children_valid (s : State) (hs : s.Valid) (P : TangentPattern s.degree)246    (hP : Allowed s P) (z : ℕ × State) (hz : z ∈ children s P) :247    z.2.Valid := by248  have other : ∀ (a : ℕ) (m : Pattern s.degree), 0 < a → z ∈ otherChildren a m → z.2.Valid := by249    intro a m ha h250    simp only [otherChildren, List.mem_flatMap, List.mem_replicate] at h251    obtain ⟨ij, _, _, rfl⟩ := h252    exact ⟨ha, Nat.succ_pos _⟩253  obtain ⟨hd, hsum, hrest⟩ := hP254  cases s with255  | single a c =>256    obtain ⟨ha, hc⟩ := hs257    obtain ⟨hdc, hrx, hrt⟩ := hrest258    simp only [children, List.mem_append] at hz259    rcases hz with hz | hz260    · split_ifs at hz with h0261      · simp at hz262      · obtain rfl := List.mem_singleton.1 hz263        exact ⟨ha, ha, Nat.pos_of_ne_zero h0, by have := hrt.mp (Nat.pos_of_ne_zero h0); omega⟩264    · exact other a _ ha hz265  | crossing a b c h =>266    obtain ⟨ha, hb, hc, hh⟩ := hs267    obtain ⟨hdc, hdh, hrt, hrx⟩ := hrest268    simp only [children, List.mem_append] at hz269    rcases hz with (hz | hz) | hz270    · split_ifs at hz with h0271      · simp at hz272      · obtain rfl := List.mem_singleton.1 hz273        have := hrt.mp (Nat.pos_of_ne_zero h0)274        exact ⟨by omega, ha, Nat.pos_of_ne_zero h0, by omega⟩275    · split_ifs at hz with h0276      · simp at hz277      · obtain rfl := List.mem_singleton.1 hz278        have := hrx.mp (Nat.pos_of_ne_zero h0)279        exact ⟨by omega, hb, Nat.pos_of_ne_zero h0, by omega⟩280    · exact other (a+b) _ (by omega) hz281 282/-- Counting the "other" children of residue degree `δ` and contact `r` of a unit-weight283pattern, their shape, and their total number. -/284theorem other_children_count (n : ℕ) (m : Pattern n) (δ r : ℕ) :285    List.count (δ, State.single 1 r) (otherChildren 1 m) =286        (if h : 1 ≤ δ ∧ δ ≤ n ∧ 1 ≤ r ∧ r ≤ n then287          (m (⟨δ - 1, Nat.sub_one_lt_of_le h.1 h.2.1⟩,288            ⟨r - 1, Nat.sub_one_lt_of_le h.2.2.1 h.2.2.2⟩)).val else 0) ∧289      (∀ z ∈ otherChildren 1 m,290        ∃ ij : Fin n × Fin n, z = (ij.1.val + 1, State.single 1 (ij.2.val + 1))) ∧291      (otherChildren 1 m).length = ∑ ij : Fin n × Fin n, (m ij).val := by292  refine ⟨?_, fun z hz ↦ ?_, ?_⟩293  · unfold otherChildren294    rw [List.count_flatMap]295    simp only [Function.comp_def, List.count_replicate, beq_iff_eq]296    rw [Finset.sum_map_toList (Finset.univ : Finset (Fin n × Fin n))297      (fun ij ↦ if ((ij.1.val + 1, State.single 1 (ij.2.val + 1)) : ℕ × State) =298        (δ, State.single 1 r) then (m ij).val else 0)]299    split_ifs with h300    · rw [Finset.sum_eq_single (⟨δ - 1, by omega⟩, ⟨r - 1, by omega⟩)]301      · rw [if_pos]302        simp only [Prod.mk.injEq, State.single.injEq]303        exact ⟨by omega, trivial, by omega⟩304      · intro b _ hb305        rw [if_neg]306        simp only [Prod.mk.injEq, State.single.injEq]307        rintro ⟨h1, -, h2⟩308        apply hb309        ext <;> simp <;> omega310      · simp311    · refine Finset.sum_eq_zero fun ij _ ↦ if_neg ?_312      simp only [Prod.mk.injEq, State.single.injEq]313      have := ij.1.isLt314      have := ij.2.isLt315      omega316  · simp only [otherChildren, List.mem_flatMap] at hz317    obtain ⟨ij, _, h⟩ := hz318    exact ⟨ij, (List.mem_replicate.mp h).2⟩319  · simp [otherChildren, List.length_flatMap, Finset.sum_map_toList]320 321/-- Among valid states, smaller degree forces smaller rank. -/322theorem rank_lt_of_degree_lt (s u : State) (hu : u.Valid)323    (h : u.degree < s.degree) :324    u.rank < s.rank := by325  have ht : u.tag ≤ 1 := by cases u <;> simp [State.tag]326  have h1 : u.degree - u.weight ≤ u.degree := Nat.sub_le _ _327  unfold State.rank328  have h3 : (u.degree + 1) * (u.degree + 1) ≤ s.degree * s.degree := Nat.mul_le_mul h h329  nlinarith330 331/-! ### Density values and safety of divisor counts -/332 333/-- Arithmetic of `densityValue` (multiplicativity, additivity, values on `q⁻ⁿ` and `1`,334finiteness and positivity) and positivity of state volumes at an integer `q ≥ 2`. -/335theorem density_value_arith (q : ℕ) (hq : 2 ≤ q) (x y : Expr) (hx : 0 ≤ x.eval q)336    (hy : 0 ≤ y.eval q) (n : ℕ) (s : State) (hs : s.Valid) :337    densityValue (.mul x y) q = densityValue x q * densityValue y q ∧338      densityValue (.add x y) q = densityValue x q + densityValue y q ∧339      densityValue (.inv (.pow .var n)) q = (q : ℝ≥0∞)⁻¹ ^ n ∧340      densityValue (.const 1) q = 1 ∧ densityValue x q ≠ ⊤ ∧341      (0 < x.eval q → densityValue x q ≠ 0) ∧ 0 < (stateVolume s).eval q ∧342      (stateVolume s).eval q ≠ 0 := by343  have hqpos : (0 : ℚ) < q := by exact_mod_cast (by omega : 0 < q)344  have hvol : 0 < (stateVolume s).eval (q : ℚ) := by345    cases s with346    | single a c =>347      simp only [stateVolume, Expr.eval, expression_pow_eval]348      positivity349    | crossing a b c h =>350      have h1 : (1 : ℚ) < q := by exact_mod_cast (by omega : 1 < q)351      simp only [stateVolume, Expr.eval, expression_pow_eval, eminusOne, Expr.sub, Expr.neg]352      exact mul_pos (by linarith) (inv_pos.2 (pow_pos hqpos _))353  refine ⟨?_, ?_, ?_, ?_, ENNReal.ofReal_ne_top,354    fun h ↦ (ENNReal.ofReal_pos.2 (by exact_mod_cast h)).ne', hvol, hvol.ne'⟩355  · simp only [densityValue, Expr.eval]356    push_cast357    exact ENNReal.ofReal_mul (by exact_mod_cast hx)358  · simp only [densityValue, Expr.eval]359    push_cast360    exact ENNReal.ofReal_add (by exact_mod_cast hx) (by exact_mod_cast hy)361  · simp only [densityValue, Expr.eval, expression_pow_eval]362    push_cast363    rw [ENNReal.ofReal_inv_of_pos (by positivity), ENNReal.ofReal_pow (by positivity),364      ENNReal.ofReal_natCast, ENNReal.inv_pow]365  · simp [densityValue, Expr.eval]366 367/-- Every divisor count expression is safe at every integer `q ≥ 2`. -/368theorem divisor_count_safe (n : ℕ) (offset : ℤ) (m : Pattern n) :369    (divisorCount offset m).allSafe := by370  intro q _371  have hav : ∀ δ, (availablePoints offset δ).safe q := by372    intro δ373    unfold availablePoints374    split_ifs375    · exact ⟨trivial, trivial⟩376    · refine ⟨trivial, expression_sum_safe _ _ ?_⟩377      simp only [List.mem_map]378      rintro _ ⟨j, _, rfl⟩379      exact ⟨trivial, expression_pow_safe _ _ _ trivial⟩380  refine expression_prod_safe _ _ ?_381  simp only [List.mem_map]382  rintro _ ⟨i, _, rfl⟩383  refine ⟨expression_prod_safe _ _ ?_, trivial⟩384  simp only [List.mem_map]385  rintro _ ⟨j, _, rfl⟩386  exact ⟨hav _, trivial, trivial⟩387 388/-- Every divisor probability expression is safe at every integer `q ≥ 2`. -/389theorem divisor_probability_safe (s : State) (d : ℕ) :390    (divisorProbability s d).allSafe := by391  intro q hq392  have hq' : (2:ℚ) ≤ q := by exact_mod_cast hq393  have hE : eminusOne.safe q := by394    simp [eminusOne, Expr.sub, Expr.neg, Expr.safe]395  have hEv : eminusOne.eval q = (q:ℚ) - 1 := by396    simp [eminusOne, Expr.sub, Expr.neg, Expr.eval]; ring397  have hV : ∀ n : ℕ, ((Expr.var).pow n).safe q ∧ ((Expr.var).pow n).eval q ≠ 0 := fun n ↦398    ⟨expression_pow_safe _ _ _ trivial, by399      simpa [expression_pow_eval, Expr.eval] using pow_ne_zero n (by linarith : (q:ℚ) ≠ 0)⟩400  have hP : ∀ n : ℕ, (eminusOne.pow n).safe q := fun n ↦ expression_pow_safe _ _ _ hE401  cases s with402  | single a c => exact ⟨hV _, hP _⟩403  | crossing a b c h =>404    simp only [divisorProbability, Expr.safe]405    refine ⟨hV _, ?_⟩406    split_ifs407    all_goals first408      | exact hP _409      | exact ⟨hE, by rw [hEv]; linarith⟩410 411/-! ### Coefficients of laws -/412 413/-- Scaling types by `δ > 0` is injective. -/414private theorem scaleType_injective {δ : ℕ} (hδ : 0 < δ) : Function.Injective (scaleType δ) := by415  apply Multiset.map_injective416  rintro ⟨a, b⟩ ⟨c, d⟩ h417  simp only [Prod.mk.injEq] at h ⊢418  exact ⟨h.1, Nat.eq_of_mul_eq_mul_left hδ h.2⟩419 420/-- The value of a law coefficient is the sum of the values of the matching entries. -/421private theorem lawCoeff_eval (L : Law) (σ : FactorType) (q : ℚ) :422    (lawCoeff L σ).eval q = (L.map fun z ↦ if z.1 = σ then z.2.eval q else 0).sum := by423  simp only [lawCoeff, expression_sum_eval, List.map_map]424  congr 1425  refine List.map_congr_left fun z _ ↦ ?_426  split_ifs <;> simp [Expr.eval, *]427 428/-- Coefficients of a descended law: `lawDescend δ L` has coefficient `L_τ(q^δ)` at429`scaleType δ τ` and vanishing coefficients at types not of this form. -/430theorem law_coeff_descend (δ : ℕ) (hδ : 0 < δ) (L : Law) (τ : FactorType) (q : ℚ) :431    (lawCoeff (lawDescend δ L) (scaleType δ τ)).eval q = (lawCoeff L τ).eval (q ^ δ) ∧432      ∀ σ : FactorType, (∀ τ' : FactorType, σ ≠ scaleType δ τ') →433        (lawCoeff (lawDescend δ L) σ).eval q = 0 := by434  refine ⟨?_, fun σ hσ ↦ ?_⟩435  · simp only [lawCoeff_eval, lawDescend, List.map_map]436    congr 1437    refine List.map_congr_left fun z _ ↦ ?_438    simp [(scaleType_injective hδ).eq_iff, expression_subst_eval, expression_pow_eval, Expr.eval]439  · rw [lawCoeff_eval]440    refine List.sum_eq_zero fun x hx ↦ ?_441    simp only [lawDescend, List.map_map, List.mem_map, Function.comp_def] at hx442    obtain ⟨z, -, rfl⟩ := hx443    exact if_neg fun e ↦ hσ z.1 e.symm444 445/-! ### Interpretation of laws in a monoid algebra -/446 447/-- The interpretation of a law along a valuation `v` of expressions, as the element448`Σ_{z ∈ L} v(z.2) · Z^{z.1}` of the monoid algebra `S[FactorType]`. Numerical evaluation at `q`449and the rational-function interpretation of the reciprocity branch are both of this form. -/450noncomputable def lawInterp {S : Type*} [Semiring S] (v : Expr → S) (L : Law) :451    AddMonoidAlgebra S FactorType :=452  (L.map fun z ↦ AddMonoidAlgebra.single z.1 (v z.2)).sum453 454section lawInterp455 456variable {S : Type*} [Semiring S] (v : Expr → S)457 458/-- The interpretation of the empty law is `0`. -/459theorem lawInterp_nil : lawInterp v [] = 0 := rfl460 461/-- The interpretation is additive on concatenation. -/462theorem lawInterp_append (L M : Law) : lawInterp v (L ++ M) = lawInterp v L + lawInterp v M := by463  simp [lawInterp]464 465/-- The interpretation sends a `flatMap` to the sum of the pieces. -/466theorem lawInterp_flatMap {α : Type} (xs : List α) (g : α → Law) :467    lawInterp v (xs.flatMap g) = (xs.map fun u ↦ lawInterp v (g u)).sum := by468  simp [lawInterp, List.flatMap_def, List.map_flatten, List.sum_flatten, List.map_map,469    Function.comp_def]470 471/-- For a multiplicative valuation, the interpretation is multiplicative on `lawMul`. -/472theorem lawInterp_lawMul (hv : ∀ x y, v (.mul x y) = v x * v y) (L M : Law) :473    lawInterp v (lawMul L M) = lawInterp v L * lawInterp v M := by474  simp only [lawInterp, lawMul, List.flatMap_def, List.map_flatten, List.sum_flatten,475    List.map_map, Function.comp_def, ← List.sum_map_mul_right]476  simp [← List.sum_map_mul_left, AddMonoidAlgebra.single_mul_single, hv]477 478/-- For a multiplicative valuation, the interpretation turns `lawScale x` into multiplication479by the scalar `v x`. -/480theorem lawInterp_lawScale (hv : ∀ x y, v (.mul x y) = v x * v y) (x : Expr) (L : Law) :481    lawInterp v (lawScale x L) = AddMonoidAlgebra.single 0 (v x) * lawInterp v L := by482  simp [lawInterp, lawScale, List.map_map, Function.comp_def, ← List.sum_map_mul_left,483    AddMonoidAlgebra.single_mul_single, hv]484 485/-- For a multiplicative valuation with `v 1 = 1`, the interpretation is multiplicative on486finite products `lawProd`. -/487theorem lawInterp_lawProd (hv : ∀ x y, v (.mul x y) = v x * v y) (h1 : v (.const 1) = 1)488    (Ls : List Law) : lawInterp v (lawProd Ls) = (Ls.map (lawInterp v)).prod := by489  induction Ls with490  | nil => simp [lawProd, lawOne, lawInterp, h1, AddMonoidAlgebra.one_def]491  | cons L Ls ih => rw [lawProd, List.foldr_cons, ← lawProd, lawInterp_lawMul v hv, ih]; rfl492 493/-- The coefficients of the interpretation: the sum of the values of the matching entries. -/494theorem lawInterp_coeff (L : Law) (σ : FactorType) :495    (lawInterp v L).coeff σ = (L.map fun z ↦ if z.1 = σ then v z.2 else 0).sum := by496  rw [lawInterp, ← AddMonoidAlgebra.coeffAddEquiv_apply, map_list_sum,497    ← Finsupp.applyAddHom_apply, map_list_sum]498  simp [List.map_map, Function.comp_def, Finsupp.single_apply]499 500/-- The interpretation has no coefficients at types that do not occur in the law. -/501private theorem lawInterp_coeff_eq_zero (L : Law) (τ : FactorType)502    (h : τ ∉ (L.map Prod.fst).toFinset) : (lawInterp v L).coeff τ = 0 := by503  rw [lawInterp_coeff]504  refine List.sum_eq_zero fun x hx ↦ ?_505  obtain ⟨z, hz, rfl⟩ := List.mem_map.1 hx506  exact if_neg fun e ↦ h (List.mem_toFinset.2 (List.mem_map.2 ⟨z, hz, e⟩))507 508end lawInterp509 510/-- The value at `q` of a law coefficient is the coefficient of its numerical interpretation. -/511private theorem lawCoeff_eval_interp (L : Law) (σ : FactorType) (q : ℚ) :512    (lawCoeff L σ).eval q = (lawInterp (fun x ↦ x.eval q) L).coeff σ :=513  (lawCoeff_eval L σ q).trans (lawInterp_coeff _ L σ).symm514 515/-- Coefficients are additive under concatenation, vanish on the empty law, and sum over a516`flatMap`. -/517theorem law_coeff_flatMap (α : Type) (xs : List α) (f : α → Law) (L M : Law) (σ : FactorType)518    (q : ℚ) :519    (lawCoeff (L ++ M) σ).eval q = (lawCoeff L σ).eval q + (lawCoeff M σ).eval q ∧520      (lawCoeff ([] : Law) σ).eval q = 0 ∧521      (lawCoeff (xs.flatMap f) σ).eval q = (xs.map fun x ↦ (lawCoeff (f x) σ).eval q).sum := by522  simp only [lawCoeff_eval_interp, lawInterp_append, lawInterp_nil, lawInterp_flatMap,523    AddMonoidAlgebra.coeff_add, AddMonoidAlgebra.coeff_zero, Finsupp.coe_zero, Pi.zero_apply,524    Finsupp.coe_add, Pi.add_apply, true_and]525  rw [← AddMonoidAlgebra.coeffAddEquiv_apply, map_list_sum, ← Finsupp.applyAddHom_apply,526    map_list_sum, List.map_map, List.map_map]527  rfl528 529/-- Coefficient formula for a product of two laws: a convolution over the types of `L`. -/530theorem law_coeff_mul (L M : Law) (σ : FactorType) (q : ℚ) :531    (lawCoeff (lawMul L M) σ).eval q = ∑ τ ∈ (L.map Prod.fst).toFinset,532      (if τ ≤ σ then (lawCoeff L τ).eval q * (lawCoeff M (σ - τ)).eval q else 0) := by533  simp only [lawCoeff_eval_interp]534  set f := lawInterp (fun x ↦ x.eval q) L with hf0535  have hf : f = ∑ τ ∈ (L.map Prod.fst).toFinset, AddMonoidAlgebra.single τ (f.coeff τ) := by536    ext τ537    simp only [AddMonoidAlgebra.coeff_sum, Finsupp.finsetSum_apply, AddMonoidAlgebra.coeff_single,538      Finsupp.single_apply, Finset.sum_ite_eq']539    split_ifs with h540    exacts [rfl, lawInterp_coeff_eq_zero _ L τ h]541  rw [lawInterp_lawMul (fun x ↦ x.eval q) (fun _ _ ↦ rfl), ← hf0]542  conv_lhs => rw [hf, Finset.sum_mul, AddMonoidAlgebra.coeff_sum, Finsupp.finsetSum_apply]543  refine Finset.sum_congr rfl fun τ _ ↦ ?_544  split_ifs with h545  · obtain ⟨ρ, rfl⟩ := exists_add_of_le h546    rw [AddMonoidAlgebra.coeff_single_mul_add, add_tsub_cancel_left]547  · exact AddMonoidAlgebra.coeff_single_mul_of_forall_add_ne _ _ fun d e ↦ h (e ▸ le_self_add)548 549/-- Splitting a sum over `piFinset t` on `Fin (n + 1)` into the first coordinate and the550tail. -/551private theorem sum_piFinset_succ (n : ℕ) (t : Fin (n + 1) → Finset FactorType)552    (F : (Fin (n + 1) → FactorType) → ℚ) :553    ∑ τ ∈ Fintype.piFinset t, F τ554      = ∑ τ₀ ∈ t 0, ∑ τ' ∈ Fintype.piFinset (fun i ↦ t i.succ), F (Fin.cons τ₀ τ') := by555  rw [← Finset.sum_product']556  refine Finset.sum_nbij' (fun τ ↦ (τ 0, Fin.tail τ)) (fun p ↦ Fin.cons p.1 p.2) ?_ ?_ ?_ ?_ ?_557  · intro τ hτ558    simp only [Finset.mem_product, Fintype.mem_piFinset] at hτ ⊢559    exact ⟨hτ 0, fun i ↦ hτ i.succ⟩560  · intro p hp561    simp only [Finset.mem_product, Fintype.mem_piFinset] at hp ⊢562    exact fun i ↦ Fin.cases (by simpa using hp.1) (fun j ↦ by simpa using hp.2 j) i563  all_goals intros; simp564 565/-- Coefficient formula for a product of descended laws `∏ⱼ lawDescend δⱼ Lⱼ`. -/566theorem law_coeff_prod_descend (Ls : List (ℕ × Law)) (hδ : ∀ z ∈ Ls, 0 < z.1)567    (σ : FactorType) (q : ℚ) :568    (lawCoeff (lawProd (Ls.map fun z ↦ lawDescend z.1 z.2)) σ).eval q =569      ∑ τ ∈ Fintype.piFinset (fun j : Fin Ls.length ↦ ((Ls.get j).2.map Prod.fst).toFinset),570        (if σ = ∑ j, scaleType (Ls.get j).1 (τ j) then571          ∏ j, (lawCoeff (Ls.get j).2 (τ j)).eval (q ^ (Ls.get j).1) else 0) := by572  induction Ls generalizing σ with573  | nil =>574    simp [lawProd, lawOne, lawCoeff, expression_sum_eval, Fintype.piFinset_of_isEmpty,575      eq_comm, apply_ite, Expr.eval]576  | cons z Ls ih =>577    obtain ⟨δ, L⟩ := z578    have hδ0 : 0 < δ := hδ _ List.mem_cons_self579    have ih' := fun σ ↦ ih (fun w hw ↦ hδ w (List.mem_cons_of_mem _ hw)) σ580    rw [List.map_cons, lawProd, List.foldr_cons, ← lawProd, law_coeff_mul]581    have hmap : ((lawDescend δ L).map Prod.fst).toFinset582        = (L.map Prod.fst).toFinset.image (scaleType δ) := by583      ext x; simp [lawDescend]584    rw [hmap, Finset.sum_image fun x _ y _ h ↦ scaleType_injective hδ0 h]585    change _ = ∑ τ ∈ Fintype.piFinset (fun j : Fin (Ls.length + 1) ↦586      (((δ, L) :: Ls).get j).2.map Prod.fst |>.toFinset), _587    rw [sum_piFinset_succ]588    refine Finset.sum_congr rfl fun ρ _ ↦ ?_589    rw [(law_coeff_descend δ hδ0 L ρ q).1]590    -- `Fin.sum_univ_succ` stated for `Fin (Ls.length + 1)`, to be used up to defeq591    have hs : ∀ f : Fin (Ls.length + 1) → FactorType,592        ∑ j, f j = f 0 + ∑ j : Fin Ls.length, f j.succ := Fin.sum_univ_succ593    have hp : ∀ f : Fin (Ls.length + 1) → ℚ, ∏ j, f j = f 0 * ∏ j : Fin Ls.length, f j.succ :=594      Fin.prod_univ_succ595    have hg : ∀ i : Fin Ls.length, ((δ, L) :: Ls).get i.succ = Ls.get i := fun i ↦ rfl596    split_ifs with hle597    · rw [ih', Finset.mul_sum]598      refine Finset.sum_congr rfl fun τ' _ ↦ ?_599      erw [hs, hp]600      simp only [Fin.cons_zero, Fin.cons_succ, List.get_cons_zero, hg,601        tsub_eq_iff_eq_add_of_le hle, mul_ite, mul_zero, add_comm]602    · refine (Finset.sum_eq_zero fun τ' _ ↦ if_neg fun h ↦ ?_).symm603      erw [hs] at h604      simp only [Fin.cons_zero, List.get_cons_zero] at h605      exact hle (h ▸ le_self_add)606 607/-- Coefficient formula for a finite product of laws `∏ⱼ Dl j`, and vanishing of the608coefficients of a law at types that do not occur in it. -/609theorem law_coeff_prod_formula (L : ℕ) (Dl : Fin L → Law) (σ : FactorType) (q : ℚ) :610    ((lawCoeff (lawProd (List.ofFn Dl)) σ).eval q =611        ∑ τ ∈ Fintype.piFinset (fun j ↦ ((Dl j).map Prod.fst).toFinset),612          (if σ = ∑ j, τ j then ∏ j, (lawCoeff (Dl j) (τ j)).eval q else 0)) ∧613      ∀ (M : Law) (τ : FactorType), τ ∉ (M.map Prod.fst).toFinset →614        (lawCoeff M τ).eval q = 0 := by615  refine ⟨?_, fun M τ h ↦ ?_⟩616  · induction L generalizing σ with617    | zero =>618      simp [lawProd, lawOne, lawCoeff, expression_sum_eval, Fintype.piFinset_of_isEmpty,619        eq_comm, apply_ite, Expr.eval]620    | succ n ih =>621      rw [List.ofFn_succ, lawProd, List.foldr_cons, ← lawProd, law_coeff_mul, sum_piFinset_succ]622      refine Finset.sum_congr rfl fun τ₀ _ ↦ ?_623      rw [ih (fun i ↦ Dl i.succ)]624      split_ifs with hle625      · rw [Finset.mul_sum]626        refine Finset.sum_congr rfl fun τ' _ ↦ ?_627        simp only [Fin.sum_univ_succ, Fin.prod_univ_succ, Fin.cons_zero, Fin.cons_succ]628        simp only [tsub_eq_iff_eq_add_of_le hle, mul_ite, mul_zero, add_comm]629      · refine (Finset.sum_eq_zero fun τ' _ ↦ if_neg fun h ↦ hle ?_).symm630        rw [h, Fin.sum_univ_succ, Fin.cons_zero]631        exact le_self_add632  · rw [lawCoeff_eval_interp]633    exact lawInterp_coeff_eq_zero _ M τ h634 635/-- Coefficients of a scaled law: `(x · L)_σ = x · L_σ`. -/636theorem law_coeff_scale (x : Expr) (L : Law) (σ : FactorType) (q : ℚ) :637    (lawCoeff (lawScale x L) σ).eval q = x.eval q * (lawCoeff L σ).eval q := by638  rw [lawCoeff_eval_interp, lawCoeff_eval_interp,639    lawInterp_lawScale (fun x ↦ x.eval q) (fun _ _ ↦ rfl), AddMonoidAlgebra.coeff_single_zero_mul]640 641/-- Nonnegativity of law coefficients at `q` is preserved by scaling by nonnegative642expressions, products, finite products, flat maps and descents, and holds for atoms and the643unit law; the empty law has zero coefficients. -/644theorem law_coeff_nonneg_closure (q : ℚ) :645    (∀ (x : Expr) (L : Law), 0 ≤ x.eval q → (∀ σ : FactorType, 0 ≤ (lawCoeff L σ).eval q) →646      ∀ σ : FactorType, 0 ≤ (lawCoeff (lawScale x L) σ).eval q) ∧647    (∀ L M : Law, (∀ σ : FactorType, 0 ≤ (lawCoeff L σ).eval q) →648      (∀ σ : FactorType, 0 ≤ (lawCoeff M σ).eval q) →649      ∀ σ : FactorType, 0 ≤ (lawCoeff (lawMul L M) σ).eval q) ∧650    (∀ Ls : List Law, (∀ L ∈ Ls, (∀ σ : FactorType, 0 ≤ (lawCoeff L σ).eval q)) →651      ∀ σ : FactorType, 0 ≤ (lawCoeff (lawProd Ls) σ).eval q) ∧652    (∀ (α : Type) (xs : List α) (f : α → Law),653      (∀ x ∈ xs, ∀ σ : FactorType, 0 ≤ (lawCoeff (f x) σ).eval q) →654      ∀ σ : FactorType, 0 ≤ (lawCoeff (xs.flatMap f) σ).eval q) ∧655    (∀ (δ : ℕ), 0 < δ → ∀ L : Law, (∀ σ : FactorType, 0 ≤ (lawCoeff L σ).eval (q ^ δ)) →656      ∀ σ : FactorType, 0 ≤ (lawCoeff (lawDescend δ L) σ).eval q) ∧657    (∀ (a f : ℕ) (σ : FactorType), 0 ≤ (lawCoeff (lawAtom a f) σ).eval q) ∧658    (∀ σ : FactorType, 0 ≤ (lawCoeff lawOne σ).eval q) ∧659    (∀ σ : FactorType, (lawCoeff ([] : Law) σ).eval q = 0) := by660  have hmul : ∀ L M : Law, (∀ σ : FactorType, 0 ≤ (lawCoeff L σ).eval q) →661      (∀ σ : FactorType, 0 ≤ (lawCoeff M σ).eval q) →662      ∀ σ : FactorType, 0 ≤ (lawCoeff (lawMul L M) σ).eval q := by663    intro L M hL hM σ664    rw [law_coeff_mul]665    refine Finset.sum_nonneg fun τ _ ↦ ?_666    split_ifs667    · exact mul_nonneg (hL _) (hM _)668    · exact le_rfl669  have hone : ∀ σ : FactorType, 0 ≤ (lawCoeff lawOne σ).eval q := by670    intro σ671    simp only [lawCoeff_eval, lawOne, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]672    split_ifs <;> simp [Expr.eval]673  refine ⟨fun x L hx hL σ ↦ by rw [law_coeff_scale]; exact mul_nonneg hx (hL σ), hmul, ?_, ?_,674    ?_, ?_, hone, fun σ ↦ by simp [lawCoeff_eval]⟩675  · intro Ls676    induction Ls with677    | nil => exact fun _ ↦ hone678    | cons L Ls ih =>679      exact fun h ↦ hmul _ _ (h L (by simp)) (ih fun L' hL' ↦ h L' (by simp [hL']))680  · intro α xs f h σ681    rw [(law_coeff_flatMap α xs f [] [] σ q).2.2]682    refine List.sum_nonneg fun y hy ↦ ?_683    obtain ⟨x, hx, rfl⟩ := List.mem_map.mp hy684    exact h x hx σ685  · intro δ hδ L h σ686    by_cases hs : ∃ τ, σ = scaleType δ τ687    · obtain ⟨τ, rfl⟩ := hs688      rw [(law_coeff_descend δ hδ L τ q).1]689      exact h τ690    · push Not at hs691      rw [(law_coeff_descend δ hδ L 0 q).2 σ hs]692  · intro a f σ693    simp only [lawCoeff_eval, lawAtom, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]694    split_ifs <;> simp [Expr.eval]695 696/-- Descents of safe laws are safe. -/697theorem law_safe_descend (δ : ℕ) (hδ : 0 < δ) (L : Law) (hL : LawSafe L) :698    LawSafe (lawDescend δ L) := by699  intro z hz700  simp only [lawDescend, List.mem_map] at hz701  obtain ⟨w, hw, rfl⟩ := hz702  intro q hq703  refine expression_subst_safe _ _ _ (expression_pow_safe _ _ _ trivial) ?_704  rw [expression_pow_eval]705  have : ((q:ℚ))^δ = ((q^δ : ℕ) : ℚ) := by push_cast; rfl706  change w.2.safe _707  simp only [Expr.eval]708  rw [this]709  exact hL w hw _ (hq.trans (Nat.le_self_pow (by omega) q))710 711/-- Products of safe laws are safe. -/712theorem law_safe_mul (L M : Law) (hL : LawSafe L) (hM : LawSafe M) :713    LawSafe (lawMul L M) := by714  intro z hz715  simp only [lawMul, List.mem_flatMap, List.mem_map] at hz716  obtain ⟨a, ha, b, hb, rfl⟩ := hz717  exact fun q hq ↦ ⟨hL a ha q hq, hM b hb q hq⟩718 719/-- Scaling a safe law by an everywhere-safe expression gives a safe law. -/720theorem law_safe_scale (x : Expr) (L : Law) (hx : x.allSafe) (hL : LawSafe L) :721    LawSafe (lawScale x L) := by722  intro z hz723  simp only [lawScale, List.mem_map] at hz724  obtain ⟨w, hw, rfl⟩ := hz725  exact fun q hq ↦ ⟨hx q hq, hL w hw q hq⟩726 727/-! ### Algebraic and topological facts -/728 729/-- For an `I`-adic topology, the congruence cylinders `{b | ∀ j, b j - a j ∈ I ^ L}` are730clopen (hence compact when `O` is compact), and their products are closed. -/731theorem coordinate_cylinder_clopen (O : Type) [CommRing O] [TopologicalSpace O]732    [IsTopologicalRing O] (I : Ideal O) (htop : IsAdic I) (L : ℕ) :733    (∀ (n : ℕ) (a : Fin n → O), IsOpen {b : Fin n → O | ∀ j, b j - a j ∈ I ^ L} ∧734        IsClosed {b : Fin n → O | ∀ j, b j - a j ∈ I ^ L}) ∧735      (∀ (n : ℕ) (a : Fin n → O), CompactSpace O →736        IsCompact {b : Fin n → O | ∀ j, b j - a j ∈ I ^ L}) ∧737      (∀ (ι : Type) (d : ι → ℕ) (c : ∀ i, Fin (d i) → O),738        IsClosed (Set.pi Set.univ fun i ↦ {b : Fin (d i) → O | ∀ j, b j - c i j ∈ I ^ L})) := by739  have hopen : IsOpen (((I ^ L : Ideal O).toAddSubgroup : AddSubgroup O) : Set O) :=740    AddSubgroup.isOpen_of_mem_nhds _ ((htop.hasBasis_nhds_zero).mem_of_mem (i := L) trivial)741  have hclosed := AddSubgroup.isClosed_of_isOpen _ hopen742  have hcyl : ∀ (n : ℕ) (a : Fin n → O), IsOpen {b : Fin n → O | ∀ j, b j - a j ∈ I ^ L} ∧743      IsClosed {b : Fin n → O | ∀ j, b j - a j ∈ I ^ L} := by744    intro n a745    have e : {b : Fin n → O | ∀ j, b j - a j ∈ I ^ L} = ⋂ j, (fun b : Fin n → O ↦ b j - a j) ⁻¹'746        (((I ^ L : Ideal O).toAddSubgroup : AddSubgroup O) : Set O) := by747      ext b; simp748    have hc : ∀ j, Continuous fun b : Fin n → O ↦ b j - a j := fun j ↦749      (continuous_apply j).sub continuous_const750    rw [e]751    exact ⟨isOpen_iInter_of_finite fun j ↦ hopen.preimage (hc j),752      isClosed_iInter fun j ↦ hclosed.preimage (hc j)⟩753  exact ⟨hcyl, fun n a _ ↦ (hcyl n a).2.isCompact,754    fun ι d c ↦ isClosed_set_pi fun i _ ↦ (hcyl (d i) (c i)).2⟩755 756open Polynomial in757/-- Over a discrete valuation ring `R` with fraction field `K`, a monic polynomial `A` and a758polynomial `B` reducing to `1` modulo the maximal ideal are coprime over `K`. -/759theorem coprime_of_monic_reduction_one (R K : Type) [CommRing R] [IsDomain R]760    [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (A B : Polynomial R)761    (hA : A.Monic) (hB : B.map (IsLocalRing.residue R) = 1) :762    IsCoprime (A.map (algebraMap R K)) (B.map (algebraMap R K)) := by763  classical764  have hinj := IsFractionRing.injective R K765  by_contra hnc766  set A' := A.map (algebraMap R K)767  set B' := B.map (algebraMap R K)768  have hd : ¬ IsUnit (EuclideanDomain.gcd A' B') := by769    rwa [EuclideanDomain.gcd_isUnit_iff]770  have hd0 : EuclideanDomain.gcd A' B' ≠ 0 := fun h ↦771    (hA.map _).ne_zero (EuclideanDomain.gcd_eq_zero_iff.mp h).1772  obtain ⟨h, hirr, hdvd⟩ := WfDvdMonoid.exists_irreducible_factor hd hd0773  set g := C (h.leadingCoeff)⁻¹ * h774  have hlc : h.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr hirr.ne_zero775  have hgm : g.Monic := monic_C_mul_of_mul_leadingCoeff_eq_one (inv_mul_cancel₀ hlc)776  have hgh : g ∣ h := ⟨C h.leadingCoeff, by777    rw [mul_comm, ← mul_assoc, ← C_mul, mul_inv_cancel₀ hlc, C_1, one_mul]⟩778  have hgA : g ∣ A' := hgh.trans (hdvd.trans (EuclideanDomain.gcd_dvd_left _ _))779  have hgB : g ∣ B' := hgh.trans (hdvd.trans (EuclideanDomain.gcd_dvd_right _ _))780  have hgdeg : 0 < g.natDegree := by781    rw [natDegree_C_mul (inv_ne_zero hlc), natDegree_pos_iff_degree_pos]782    exact degree_pos_of_irreducible hirr783  obtain ⟨h₀, hh₀⟩ := IsIntegrallyClosed.eq_map_mul_C_of_dvd K hA hgA784  rw [hgm.leadingCoeff, C_1, mul_one] at hh₀785  have hh₀m : h₀.Monic := monic_of_injective hinj (hh₀ ▸ hgm)786  have hdeg : h₀.natDegree = g.natDegree := by787    rw [← hh₀, natDegree_map_eq_of_injective hinj]788  have hh₀B : h₀ ∣ B := by789    rw [← map_dvd_map (algebraMap R K) hinj hh₀m, hh₀]; exact hgB790  have hu : IsUnit (h₀.map (IsLocalRing.residue R)) :=791    isUnit_of_dvd_one (hB ▸ Polynomial.map_dvd (IsLocalRing.residue R) hh₀B)792  rw [(hh₀m.map _).isUnit_iff] at hu793  have := congrArg natDegree hu794  rw [hh₀m.natDegree_map, natDegree_one] at this795  omega796 797/-- For an integral extension of local rings, the maximal ideal of `B` lies over that of `O`,798and it is the only prime of `B` lying over it. -/799theorem integral_local_extension_unique_prime (O B : Type) [CommRing O] [IsLocalRing O]800    [CommRing B] [IsLocalRing B] [Algebra O B] [Algebra.IsIntegral O B] :801    (IsLocalRing.maximalIdeal B).comap (algebraMap O B) = IsLocalRing.maximalIdeal O ∧802      ∀ Q : Ideal B, Q.IsPrime → Q.comap (algebraMap O B) = IsLocalRing.maximalIdeal O →803        Q = IsLocalRing.maximalIdeal B := by804  refine ⟨IsLocalRing.eq_maximalIdeal (Ideal.isMaximal_comap_of_isIntegral_of_isMaximal _),805    fun Q hQ hc ↦ ?_⟩806  have hm : (Q.comap (algebraMap O B)).IsMaximal := by rw [hc]; infer_instance807  exact IsLocalRing.eq_maximalIdeal (Ideal.isMaximal_of_isIntegral_of_isMaximal_comap Q hm)808 809/-- For a finite flat extension of local rings `O → B`, `e · f = [B : O]`. -/810theorem finite_flat_local_ramification_degree (O B : Type) [CommRing O] [IsDomain O]811    [IsLocalRing O] [CommRing B] [IsLocalRing B] [Algebra O B] [Module.Finite O B]812    [Module.Flat O B] :813    (IsLocalRing.maximalIdeal B).ramificationIdx O * (IsLocalRing.maximalIdeal B).inertiaDeg O =814      Module.finrank O B := by815  have : Algebra.IsIntegral O B := Algebra.IsIntegral.of_finite O B816  obtain ⟨hcomap, huniq⟩ := integral_local_extension_unique_prime O B817  let m : (IsLocalRing.maximalIdeal O).primesOver B :=818    ⟨IsLocalRing.maximalIdeal B, inferInstance, ⟨(Ideal.under_def _ _).trans hcomap |>.symm⟩⟩819  let : Unique ((IsLocalRing.maximalIdeal O).primesOver B) :=820    { default := m821      uniq := fun q ↦ Subtype.ext (huniq q.1 q.2.1 (q.2.2.over.symm)) }822  have := Ideal.sum_ramification_inertia_eq_finrank (IsLocalRing.maximalIdeal O) (S := B)823  rwa [Fintype.sum_unique,824    show (default : (IsLocalRing.maximalIdeal O).primesOver B) = m from Subsingleton.elim _ _]825    at this826 827/-- There are finitely many valid factorization types of a given degree. -/828theorem finite_types_of_degree (n : ℕ) :829    Set.Finite {σ : FactorType | ValidType σ ∧ typeDegree σ = n} := by830  set s : Finset (ℕ × ℕ) := Finset.range (n+1) ×ˢ Finset.range (n+1)831  refine Set.Finite.subset ((n • s.val).powerset.toFinset.finite_toSet) ?_832  rintro σ ⟨hv, hd⟩833  simp only [Multiset.mem_toFinset, Multiset.mem_powerset, Finset.mem_coe]834  have hmem : ∀ z ∈ σ, z.1 * z.2 ≤ n := fun z hz ↦ hd ▸835    Multiset.le_sum_of_mem (Multiset.mem_map_of_mem (fun z : ℕ × ℕ ↦ z.1 * z.2) hz)836  have hcard : Multiset.card σ ≤ n := by837    rw [← hd, typeDegree]838    have : Multiset.card (σ.map fun z ↦ z.1 * z.2) • 1 ≤ (σ.map fun z ↦ z.1 * z.2).sum :=839      Multiset.card_nsmul_le_sum fun x hx ↦ by840        obtain ⟨z, hz, rfl⟩ := Multiset.mem_map.1 hx841        exact Nat.one_le_iff_ne_zero.2 (Nat.mul_ne_zero (hv z hz).1.ne' (hv z hz).2.ne')842    simpa using this843  refine Multiset.le_iff_count.2 fun z ↦ ?_844  rw [Multiset.count_nsmul]845  by_cases hz : z ∈ σ846  · have h1 := hv z hz847    have h2 := hmem z hz848    have hzs : z ∈ s := by849      have := Nat.le_mul_of_pos_right z.1 h1.2850      have := Nat.le_mul_of_pos_left z.2 h1.1851      simp only [s, Finset.mem_product, Finset.mem_range]852      omega853    rw [Multiset.count_eq_one_of_mem s.nodup hzs, mul_one]854    exact (Multiset.count_le_card _ _).trans hcard855  · simp [Multiset.count_eq_zero_of_notMem hz]856 857/-- Geometric series with an exit weight: `∑ⱼ λʲ G = G / (1 - λ)` for `0 ≤ λ < 1`. -/858theorem geometric_exit_sum (lam G : ℝ) (hlam : 0 ≤ lam) (hlam1 : lam < 1) :Proof of Theorem 6.2859    HasSum (fun j : ℕ ↦ lam^j * G) (G / (1 - lam)) := by860  have h : ‖lam‖ < 1 := by rwa [Real.norm_eq_abs, abs_of_nonneg hlam]861  rw [div_eq_inv_mul]862  exact (hasSum_geometric_of_norm_lt_one h).mul_right G863 864/-- The image of a measurable set under a map that is continuous and injective on a closed865subset of a compact space (into a Hausdorff space) is measurable. -/866theorem image_measurable_of_continuousOn_injOn_compact (X Y : Type) [TopologicalSpace X]867    [CompactSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [T2Space Y]868    [MeasurableSpace Y] [BorelSpace Y] (f : X → Y) (C : Set X) (hC : IsClosed C)869    (hf : ContinuousOn f C) (hinj : Set.InjOn f C) (U : Set X) (hU : MeasurableSet U) :870    MeasurableSet (f '' (U ∩ C)) := by871  have : CompactSpace C := isCompact_iff_compactSpace.mp hC.isCompact872  have hemb := (hf.domRestrict.isClosedEmbedding873    (Set.injOn_iff_injective.mp hinj)).measurableEmbedding874  have h := hemb.measurableSet_image.mpr (measurable_subtype_coe hU)875  rwa [Set.domRestrict_eq, Set.image_comp, Subtype.image_preimage_coe, Set.inter_comm] at h876 877/-- The number of positions at which a list takes the value `x` is `l.count x`. -/878theorem list_get_fiber_card (α : Type) [DecidableEq α] (l : List α) (x : α) :879    Nat.card {j : Fin l.length // l.get j = x} = l.count x := by880  induction l with881  | nil => simp882  | cons a l ih =>883    have e : {j : Fin (a :: l).length // (a :: l).get j = x} ≃884        {_u : Unit // a = x} ⊕ {j : Fin l.length // l.get j = x} :=885      { toFun := fun j ↦ Fin.cases (motive := fun i ↦ (a :: l).get i = x → _)886          (fun h ↦ Sum.inl ⟨(), h⟩) (fun i h ↦ Sum.inr ⟨i, h⟩) j.1 j.2887        invFun := fun888          | Sum.inl h => ⟨0, h.2⟩889          | Sum.inr h => ⟨Fin.succ h.1, h.2⟩890        left_inv := by891          rintro ⟨j, hj⟩892          induction j using Fin.cases <;> rfl893        right_inv := by894          rintro (h | h) <;> rfl }895    rw [Nat.card_congr e, Nat.card_sum, ih, List.count_cons]896    by_cases h : a = x897    · subst h898      simp [Nat.add_comm]899    · have : IsEmpty {_u : Unit // a = x} := ⟨fun u ↦ h u.2⟩900      simp [h]901 902/-- The polynomial `Xⁿ + ∑ aᵢ Xⁱ` is monic of degree `n`. -/903theorem monic_polynomial_degree (O : Type) [CommRing O] [IsDomain O] (n : ℕ) (a : Fin n → O) :904    (monicPolynomial O a).Monic ∧ (monicPolynomial O a).natDegree = n := by905  have hdeg : (∑ i : Fin n, Polynomial.C (algebraMap O (BaseField O) (a i)) *906      Polynomial.X^i.val).degree < (n : WithBot ℕ) := by907    refine (Polynomial.degree_sum_le _ _).trans_lt ((Finset.sup_lt_iff (WithBot.bot_lt_coe n)).2908      fun i _ ↦ (Polynomial.degree_C_mul_X_pow_le _ _).trans_lt (WithBot.coe_lt_coe.2 i.isLt))909  refine ⟨Polynomial.monic_X_pow_add hdeg, ?_⟩910  unfold monicPolynomial911  rw [Polynomial.natDegree_add_eq_left_of_degree_lt (by simpa using hdeg)]912  simp913 914end SurfaceBlowup