Type events and divisor counts

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.Assembly.NullBridges7import SurfaceBlowup.Unramified.HomogeneousCells8 9/-!10# Type events and divisor counts11 12Type events of polynomials over a complete DVR `O` with finite residue field and the combinatorics13of exceptional divisors used to assemble the cell laws: unit scaling and the binary decomposition of14type events, type descent along unramified blocks, the array of a divisor and divisor counts, and15the law of a product of reduced forms.16 17## Main results18 19* `affine_type_event_unit_scaling`, `binary_type_event_decomposition`: elementary properties of20  type events.21* `descended_block_type_iff`: types of polynomials in a block cell.22* `divisor_array_exists_unique`, `divisor_count_of_point_set`,23  `divisor_count_eval_of_point_count`, `affine_divisor_count`: arrays and divisor counts.24* `monic_polynomial_divisor`: monic polynomials correspond to affine divisors.25* `form_product_type_event_law`: the law of a product of reduced forms.26 27Provenance: `Thm_SurfaceBlowupV2_{affine_type_event_unit_scaling, array_enumeration,28binary_type_event_decomposition, descended_block_type_iff, divisor_array_exists_unique,29divisor_count_of_point_set, affine_divisor_count, divisor_vector_properties, form_product_type_iff,30form_product_type_event_sets, form_product_type_event_law, monic_polynomial_divisor}`.31-/32 33namespace SurfaceBlowup34 35open scoped BigOperators ENNReal36 37private theorem directionDegree_mul_le_exceptionalDegree (k : Type) [Field k]38    (D : ExceptionalDivisor k) (Q : ClosedDirection k) :39    directionDegree k Q * D Q ≤ exceptionalDegree k D := by40  by_cases hQ : D Q = 041  · simp [hQ]42  · exact Finset.single_le_sum (f := fun Q => directionDegree k Q * D Q) (by intros; positivity)43      (Finsupp.mem_support_iff.mpr hQ)44 45/-! ### Affine and binary type events -/46 47/-- Affine type events are invariant under scaling by units; in particular, normalising a point of48a projective residue cell at a coordinate `μ` with `G μ = 1` does not change its type. -/49theorem affine_type_event_unit_scaling (O : Type) [CommRing O] [IsDomain O] [IsLocalRing O] (n : ℕ)50    (σ : FactorType) :51    (∀ (a : Fin (n+1) → O) (u : O), IsUnit u → (u • a ∈ affineTypeEvent O n σ ↔ a ∈ affineTypeEvent52      O n σ)) ∧ ∀ (G : Fin (n+1) → IsLocalRing.ResidueField O) (μ : Fin (n+1)), G μ = 1 → ∀ a ∈53      projectiveCell O n G, (insertOne μ (projectiveNormalize O n G μ a) ∈ affineTypeEvent O n σ ↔54      a ∈ affineTypeEvent O n σ) := by55  have key : ∀ (a : Fin (n+1) → O) (u : O), IsUnit u →56      (u • a ∈ affineTypeEvent O n σ ↔ a ∈ affineTypeEvent O n σ) := by57    intro a u hu58    have hu0 : u ≠ 0 := hu.ne_zero59    have hι : algebraMap O (BaseField O) u ≠ 0 := by60      intro h61      exact hu0 (IsFractionRing.injective O (BaseField O) (by simpa using h))62    have hP : affinePolynomial O (u • a) = Polynomial.C (algebraMap O (BaseField O) u) *63        affinePolynomial O a := by64      unfold affinePolynomial65      rw [Finset.mul_sum]66      refine Finset.sum_congr rfl fun i _ => ?_67      simp only [Pi.smul_apply, smul_eq_mul, map_mul, mul_assoc]68    have hlast : (u • a) (Fin.last n) ≠ 0 ↔ a (Fin.last n) ≠ 0 := by69      simp only [Pi.smul_apply, smul_eq_mul]70      rw [Ne, Ne, mul_eq_zero]; simp [hu0]71    have hn : Polynomial.C (algebraMap O (BaseField O) ((u • a) (Fin.last n)))⁻¹ *72          affinePolynomial O (u • a) =73        Polynomial.C (algebraMap O (BaseField O) (a (Fin.last n)))⁻¹ * affinePolynomial O a := by74      rw [hP]75      simp only [Pi.smul_apply, smul_eq_mul, map_mul, mul_inv]76      rw [← mul_assoc, mul_assoc (Polynomial.C (algebraMap O (BaseField O) u)⁻¹),77        mul_comm (Polynomial.C (algebraMap O (BaseField O) (a (Fin.last n)))⁻¹),78        ← mul_assoc, ← Polynomial.C_mul, inv_mul_cancel₀ hι]79      simp [mul_comm]80    exact ⟨fun ⟨h1, h2⟩ ↦ ⟨hlast.1 h1, by rwa [hn] at h2⟩, fun ⟨h1, h2⟩ ↦ ⟨hlast.2 h1, by rwa [hn]⟩⟩81  refine ⟨key, fun G μ hG a ha ↦ ?_⟩82  have ⟨_, c, hc, hres⟩ := ha83  have hres' : IsLocalRing.residue O (a μ) = c := by simpa [residueVector, hG] using congrFun hres μ84  have hunit : IsUnit (a μ) := by85    by_contra hnu86    exact hc (hres'.symm.trans ((IsLocalRing.residue_eq_zero_iff _).287      ((IsLocalRing.mem_maximalIdeal _).2 hnu)))88  have hpn : projectiveNormalize O n G μ a = dropCoord μ (normalizeAt μ a) := by89    unfold projectiveNormalize; rw [if_pos ha]90  have hins : insertOne μ (projectiveNormalize O n G μ a) = normalizeAt μ a := by91    rw [hpn]92    unfold insertOne dropCoord93    have h1 : normalizeAt μ a μ = 1 := by94      simp only [normalizeAt, Pi.smul_apply, smul_eq_mul]95      exact Ring.inverse_mul_cancel _ hunit96    rw [← h1]97    exact Fin.insertNth_self_removeNth μ _98  rw [hins]99  unfold normalizeAt100  apply key a101  obtain ⟨v, hv⟩ := hunit102  rw [← hv, Ring.inverse_unit]103  exact Units.isUnit _104 105/-- If the divisor `D` of degree `n` has array `m`, the non-root children of the pattern `m` are106enumerated by the support of `D`, the child at `Q` being `(deg Q, single 1 (D Q))`. -/107theorem array_enumeration (k : Type) [Field k] (n : ℕ) (D : ExceptionalDivisor k)108    (hD : exceptionalDegree k D = n) (m : Pattern n) (hm : HasArray k n D m) :109    ∃ e : Fin (otherChildren 1 m).length ≃ D.support, ∀ j, (otherChildren 1 m).get j =110      (directionDegree k (e j), State.single 1 (D (e j))) := by111  set Ls := otherChildren 1 m with hLs112  let ℓ₁ : Fin Ls.length → ℕ × State := fun j => Ls.get j113  let ℓ₂ : D.support → ℕ × State := fun Q => (directionDegree k Q, State.single 1 (D Q))114  have hdeg := directionDegree_pos k115  have hle : ∀ Q ∈ D.support, directionDegree k Q * D Q ≤ n := fun Q _ ↦ hD ▸116      directionDegree_mul_le_exceptionalDegree k D Q117  have hcard : ∀ x, Fintype.card {j // ℓ₁ j = x} = Fintype.card {Q // ℓ₂ Q = x} := by118    intro x119    rw [← Nat.card_eq_fintype_card, ← Nat.card_eq_fintype_card]120    have h1 : Nat.card {j // ℓ₁ j = x} = Ls.count x := by121      convert list_get_fiber_card _ Ls x using 2122      exact lawful_beq_subsingleton _ _123    rw [h1]124    by_cases hx : ∃ δ r, x = (δ, State.single 1 r)125    · obtain ⟨δ, r, rfl⟩ := hx126      rw [(other_children_count n m δ r).1]127      have hR : Nat.card {Q // ℓ₂ Q = (δ, State.single 1 r)} =128          Nat.card {Q : ClosedDirection k // directionDegree k Q = δ ∧ D Q = r ∧ 0 < r} := by129        apply Nat.card_congr130        exact131          { toFun := fun Q => ⟨Q.1.1, by132              have h := Q.2133              simp only [ℓ₂, Prod.mk.injEq, State.single.injEq, true_and] at h134              have hs := Finsupp.mem_support_iff.mp Q.1.2135              exact ⟨h.1, h.2, by omega⟩⟩136            invFun := fun Q => ⟨⟨Q.1, Finsupp.mem_support_iff.mpr (by omega)⟩, by137              simp only [ℓ₂, Prod.mk.injEq, State.single.injEq, true_and]138              exact ⟨Q.2.1, Q.2.2.1⟩⟩139            left_inv := fun Q => rfl140            right_inv := fun Q => rfl }141      rw [hR]142      split_ifs with h143      · rw [← hm (⟨δ - 1, by omega⟩, ⟨r - 1, by omega⟩)]144        apply Nat.card_congr145        apply Equiv.subtypeEquivRight146        intro Q147        simp only148        omega149      · symm; rw [Nat.card_eq_zero]150        left151        refine ⟨fun ⟨Q, hQ1, hQ2, hQ3⟩ => h ?_⟩152        have h1 := hdeg Q153        have hQs : Q ∈ D.support := Finsupp.mem_support_iff.mpr (by omega)154        have h2 := hle Q hQs155        rw [hQ1] at h1; rw [hQ1, hQ2] at h2156        refine ⟨h1, ?_, hQ3, ?_⟩157        · nlinarith158        · nlinarith159    · have hL : Ls.count x = 0 := by160        rw [List.count_eq_zero]161        intro hmem162        obtain ⟨ij, hij⟩ := (other_children_count n m 0 0).2.1 x hmem163        exact hx ⟨_, _, hij⟩164      rw [hL]165      symm166      rw [Nat.card_eq_zero]167      left168      exact ⟨fun ⟨Q, hQ⟩ => hx ⟨_, _, hQ.symm⟩⟩169  refine ⟨(Equiv.sigmaFiberEquiv ℓ₁).symm.trans170    ((Equiv.sigmaCongrRight fun x => Fintype.equivOfCardEq (hcard x)).trans171      (Equiv.sigmaFiberEquiv ℓ₂)), fun j => ?_⟩172  have := ((Fintype.equivOfCardEq (hcard (ℓ₁ j))) ⟨j, rfl⟩).2173  exact this.symm174 175section176 177open Polynomial178 179private lemma affinePolynomial_coeff (O : Type) [CommRing O] [IsDomain O] {n : ℕ}180    (a : Fin (n + 1) → O) (k : ℕ) :181    (affinePolynomial O a).coeff k = if h : k < n+1 then algebraMap O (BaseField O)182      (a ⟨k,h⟩) else 0 := by183  unfold affinePolynomial184  rw [finsetSum_coeff]185  simp only [coeff_C_mul, coeff_X_pow]186  split_ifs with h187  · rw [Finset.sum_eq_single ⟨k,h⟩]188    · simp189    · intro b _ hb; rw [if_neg]; · simp190      intro e; apply hb; ext; simp [e]191    · simp192  · apply Finset.sum_eq_zero; intro i _; rw [if_neg]; · simp193    omega194 195private lemma affinePolynomial_natDegree_le (O : Type) [CommRing O] [IsDomain O] {n : ℕ}196    (a : Fin (n + 1) → O) : (affinePolynomial O a).natDegree ≤ n := by197  rw [natDegree_le_iff_coeff_eq_zero]198  intro k hk; rw [affinePolynomial_coeff, dif_neg]; omega199 200private lemma affinePolynomial_natDegree_eq (O : Type) [CommRing O] [IsDomain O] {n : ℕ}201    (a : Fin (n + 1) → O) (h : a (Fin.last n) ≠ 0) :202    (affinePolynomial O a).natDegree = n ∧ (affinePolynomial O a).leadingCoeff = algebraMap O203      (BaseField O) (a (Fin.last n)) := by204  have hc : (affinePolynomial O a).coeff n = algebraMap O (BaseField O) (a (Fin.last n)) := by205    rw [affinePolynomial_coeff, dif_pos (by omega)]; rfl206  have hne : (affinePolynomial O a).coeff n ≠ 0 := by207    rw [hc]; exact (map_ne_zero_iff _ (IsFractionRing.injective O (BaseField O))).mpr h208  have hd := natDegree_eq_of_le_of_coeff_ne_zero (affinePolynomial_natDegree_le O a) hne209  exact ⟨hd, by rw [leadingCoeff, hd, hc]⟩210 211private lemma affinePolynomial_eq_init (O : Type) [CommRing O] [IsDomain O] {m : ℕ}212    (a : Fin (m + 2) → O) (h : a (Fin.last (m + 1)) = 0) :213    affinePolynomial O a = affinePolynomial O (Fin.init a) := by214  ext k; rw [affinePolynomial_coeff, affinePolynomial_coeff]215  by_cases hk : k < m + 1216  · rw [dif_pos (by omega), dif_pos hk]; rfl217  · rw [dif_neg hk]; split_ifs with h2218    · have : k = m+1 := by omega219      subst this220      have e : a ⟨m+1, h2⟩ = 0 := h221      rw [e, map_zero]222    · rfl223 224/-- Decomposition of the binary type event according to whether the top coefficient vanishes: if225it does not, it is the primitive affine type event; if it does, the type must contain a factor226`(1, 1)` at infinity and the remaining coefficients form an affine type event. -/227theorem binary_type_event_decomposition (O : Type) [CommRing O] [IsDomain O] (σ : FactorType) :228    (∀ n : ℕ, binaryTypeEvent O n σ ∩ {a | a (Fin.last n) ≠ 0} = affineTypeEvent O n σ ∩229      {a | primitive O a}) ∧ (binaryTypeEvent O 0 σ ∩ {a | a (Fin.last 0) = 0} = ∅) ∧ ∀ m : ℕ,230      binaryTypeEvent O (m+1) σ ∩ {a | a (Fin.last (m+1)) = 0} = {a | a (Fin.last (m+1)) = 0} ∩231      Fin.init ⁻¹' (if (1,1) ∈ σ then affineTypeEvent O m (σ.erase (1,1)) ∩ {b | primitive O b}232      else ∅) := by233  refine ⟨?_, ?_, ?_⟩234  · intro n; ext a235    simp only [binaryTypeEvent, affineTypeEvent, HasBinaryTypeF, Set.mem_inter_iff,236        Set.mem_ofPred_eq]237    constructor238    · rintro ⟨⟨hp, -, -, -, τ, hτ, hσ⟩, ha⟩239      obtain ⟨hd, hl⟩ := affinePolynomial_natDegree_eq O a ha240      rw [hd, Nat.sub_self, Multiset.replicate_zero, add_zero] at hσ241      subst hσ; rw [hl] at hτ; exact ⟨⟨ha, hτ⟩, hp⟩242    · rintro ⟨⟨ha, hτ⟩, hp⟩243      obtain ⟨hd, hl⟩ := affinePolynomial_natDegree_eq O a ha244      refine ⟨⟨hp, ?_, by omega, by omega, σ, by rwa [hl], by simp [hd]⟩, ha⟩245      intro h0; rw [h0, natDegree_zero] at hd; subst hd246      rw [h0] at hl; simp at hl247      exact ha ((map_eq_zero_iff _ (IsFractionRing.injective O (BaseField O))).mp hl.symm)248  · ext a249    simp only [binaryTypeEvent, primitive, Set.mem_inter_iff, Set.mem_ofPred_eq,250        Set.mem_empty_iff_false, iff_false]251    rintro ⟨⟨⟨i, hi⟩, -⟩, h0⟩252    obtain rfl : i = Fin.last 0 := Subsingleton.elim (α := Fin 1) _ _253    rw [h0] at hi; exact not_isUnit_zero hi254  · intro m; ext a255    simp only [Set.mem_inter_iff, Set.mem_ofPred_eq, Set.mem_preimage]256    have hprim : ∀ a : Fin (m+2) → O, a (Fin.last (m+1)) = 0 →257        (primitive O a ↔ primitive O (Fin.init a)) := by258      refine fun a h0 ↦ ⟨fun ⟨i, hi⟩ ↦ ?_, fun ⟨j, hj⟩ ↦ ⟨Fin.castSucc j, hj⟩⟩259      induction i using Fin.lastCases with260      | last => rw [h0] at hi; exact absurd hi not_isUnit_zero261      | cast j => exact ⟨j, hi⟩262    have hdeg : ∀ b : Fin (m+1) → O, affinePolynomial O b ≠ 0 →263        (affinePolynomial O b).natDegree = m → b (Fin.last m) ≠ 0 := fun b hne hd hb ↦ by264      refine hne (leadingCoeff_eq_zero.1 ?_)265      rw [leadingCoeff, hd, affinePolynomial_coeff, dif_pos (by omega)]266      exact (congrArg _ hb).trans (map_zero _)267    constructor268    · rintro ⟨⟨hp, hne, -, hle, τ, hτ, hσ⟩, h0⟩269      rw [affinePolynomial_eq_init O a h0] at hne hle hτ hσ270      have hd : (affinePolynomial O (Fin.init a)).natDegree = m := by271        have := affinePolynomial_natDegree_le O (Fin.init a); omega272      have hb := hdeg _ hne hd273      obtain ⟨-, hl⟩ := affinePolynomial_natDegree_eq O _ hb274      rw [hd, show m + 1 - m = 1 by omega, Multiset.replicate_one] at hσ275      have hmem : ((1:ℕ),(1:ℕ)) ∈ σ := by rw [hσ]; simp276      have her : σ.erase (1,1) = τ := by rw [hσ, add_comm, Multiset.singleton_add,277          Multiset.erase_cons_head]278      refine ⟨h0, ?_⟩279      rw [if_pos hmem]280      refine ⟨⟨hb, ?_⟩, (hprim a h0).mp hp⟩281      rw [her, ← hl]; exact hτ282    · rintro ⟨h0, hs⟩283      split_ifs at hs with hmem284      · obtain ⟨⟨hb, hτ⟩, hp⟩ := hs285        obtain ⟨hd, hl⟩ := affinePolynomial_natDegree_eq O _ hb286        refine ⟨⟨(hprim a h0).mpr hp, ?_⟩, h0⟩287        unfold HasBinaryTypeF288        rw [affinePolynomial_eq_init O a h0]; intro F; simp only [F]289        rw [hd, show m + 1 - m = 1 by omega, Multiset.replicate_one, hl]290        refine ⟨?_, by omega, le_refl _, σ.erase (1,1), hτ, ?_⟩291        · intro hz; rw [hz, leadingCoeff_zero] at hl292          exact hb ((map_eq_zero_iff _ (IsFractionRing.injective O (BaseField O))).mp hl.symm)293        · rw [add_comm, Multiset.singleton_add, Multiset.cons_erase hmem]294      · exact hs.elim295 296end297 298/-- For an unramified lift `Φ` and a monic polynomial in the residue cell of `(Φ mod π)^r`, its299`O`-type is `scaleType (deg Φ) τ` exactly when the translated block polynomial over `O[X]/(Φ)` has300type `τ`. -/301theorem descended_block_type_iff (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]302    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]303    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) [IsDomain (AdjoinRoot Φ)] (r : ℕ)304    (a : Fin (Φ.natDegree * r) → O) (ha : a ∈ residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r))305    (σ : FactorType) :306    HasPolynomialTypeF O (monicPolynomial O a) σ ↔ ∃ τ : FactorType, HasPolynomialTypeF307      (AdjoinRoot Φ) (monicPolynomial (AdjoinRoot Φ) (pointChart O Φ r a)) τ ∧ σ =308      scaleType Φ.natDegree τ := by309  obtain ⟨_, _, hDVR, -, -, hComp, hFin, -⟩ := unramified_is_dvr O Φ hΦ310  have hδ : 0 < Φ.natDegree := by311    have h1 := Polynomial.natDegree_pos_iff_degree_pos.mpr312        (Polynomial.degree_pos_of_irreducible hΦ.2)313    rwa [Polynomial.Monic.natDegree_map hΦ.1] at h1314  obtain ⟨hbij, hdesc, -, hdiv⟩ := block_descent_bijection O Φ hΦ r315  set b := selectBlock O Φ r a with hb_def316  have hb : b ∈ blockCell O Φ r := hbij.mapsTo ha317  set B := monicPolyO b with hB_def318  have hBm : B.Monic := (hdiv a ha).1319  have hBdvd : B ∣ (monicPolyO a).map (AdjoinRoot.of Φ) := (hdiv a ha).2320  -- translation321  have hB' : monicPolyO (pointChart O Φ r a) = Polynomial.taylor (AdjoinRoot.root Φ) B := by322    have hrec := monic_poly_reconstruct (AdjoinRoot Φ) r b323    have hBn : B.natDegree = r := hrec.2.1324    have hTm : (Polynomial.taylor (AdjoinRoot.root Φ) B).Monic := by325      unfold Polynomial.Monic; rw [Polynomial.leadingCoeff_taylor]; exact hBm326    exact hrec.2.2.2 _ hTm ((Polynomial.natDegree_taylor B _).trans hBn)327  have htrans : ∀ τ, HasPolynomialTypeF (AdjoinRoot Φ)328      (B.map (algebraMap _ (BaseField (AdjoinRoot Φ)))) τ ↔329      HasPolynomialTypeF (AdjoinRoot Φ) (monicPolynomial (AdjoinRoot Φ) (pointChart O Φ r a)) τ :=330          by331    intro τ332    rw [← monicPolyO_map_fraction, hB']333    exact block_translation_type_iff (AdjoinRoot Φ) B hBm _ τ334  have hG : (monicPolyO a).map (algebraMap O (AdjoinRoot Φ)) = conjugateProduct O Φ B := by335    have := (descend_block_mem_cell O Φ hΦ r b hb).2336    rw [hdesc a ha] at this337    rw [AdjoinRoot.algebraMap_eq]; exact this338  have hback : ∀ τ, HasPolynomialTypeF (AdjoinRoot Φ)339      (B.map (algebraMap _ (BaseField (AdjoinRoot Φ)))) τ →340      HasPolynomialTypeF O (monicPolynomial O a) (scaleType Φ.natDegree τ) := by341    intro τ hτ342    rw [← monicPolyO_map_fraction]343    exact descended_polynomial_type O Φ hΦ B τ hτ (block_conjugates_coprime O Φ hΦ r b hb) _ hG344  constructor345  · intro hσ346    -- ascend the type to `Oδ` (closure-finiteness ascent), then pass to the divisor `B`347    obtain ⟨ι, hι, -⟩ := unramified_fraction_field_lift O Φ hΦ348    have hmap : (monicPolynomial O a).map ι =349        ((monicPolyO a).map (algebraMap O (AdjoinRoot Φ))).map350          (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ))) := by351      rw [← monicPolyO_map_fraction, Polynomial.map_map, Polynomial.map_map]352      congr 1353      exact RingHom.ext hι354    have hdvd : B.map (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ))) ∣355        ((monicPolyO a).map (algebraMap O (AdjoinRoot Φ))).map356          (algebraMap (AdjoinRoot Φ) (BaseField (AdjoinRoot Φ))) :=357      Polynomial.map_dvd _ (by rw [AdjoinRoot.algebraMap_eq]; exact hBdvd)358    obtain ⟨τ', hτ'⟩ := polynomial_type_map_unramified O Φ hΦ ι hι _ σ hσ359    rw [hmap] at hτ'360    obtain ⟨τ, hτ⟩ := polynomial_type_dvd (AdjoinRoot Φ) _ _ τ' hτ' (hBm.map _) hdvd361    refine ⟨τ, (htrans τ).1 hτ, ?_⟩362    exact polynomial_type_unique O _ σ _ hσ (hback τ hτ)363  · rintro ⟨τ, hτ, rfl⟩364    exact hback τ ((htrans τ).2 hτ)365 366/-! ### Divisors, arrays and counts -/367 368/-- Every exceptional divisor of degree `n` has a unique array, and that array is a residue369pattern. -/370theorem divisor_array_exists_unique (k : Type) [Field k] (n : ℕ) (D : ExceptionalDivisor k)371    (hD : exceptionalDegree k D = n) :372    (∃ m : Pattern n, HasArray k n D m ∧ m ∈ residuePatterns n) ∧ ∀ m m' : Pattern n,373      HasArray k n D m → HasArray k n D m' → m = m' := by374  have hdeg := directionDegree_pos k375  have hsum : exceptionalDegree k D = ∑ Q ∈ D.support, directionDegree k Q * D Q := rfl376  set S : Fin n × Fin n → Finset (ClosedDirection k) := fun ij =>377    D.support.filter (fun Q => directionDegree k Q = ij.1.val + 1 ∧ D Q = ij.2.val + 1) with hS378  have hcard : ∀ ij : Fin n × Fin n,379      Nat.card {Q : ClosedDirection k // directionDegree k Q = ij.1.val + 1 ∧ D Q = ij.2.val + 1}380        = (S ij).card := by381    intro ij382    rw [← Nat.card_eq_finsetCard]383    apply Nat.card_congr384    apply Equiv.subtypeEquivRight385    intro Q386    simp only [hS, Finset.mem_filter, Finsupp.mem_support_iff]387    constructor388    · intro h; exact ⟨by omega, h⟩389    · intro h; exact h.2390  have hconst : ∀ ij : Fin n × Fin n,391      ∑ Q ∈ S ij, directionDegree k Q * D Q = (S ij).card * ((ij.1.val + 1) * (ij.2.val + 1)) := by392    intro ij393    rw [Finset.sum_congr rfl (g := fun _ => (ij.1.val + 1) * (ij.2.val + 1))]394    · simp395    · intro Q hQ396      simp only [hS, Finset.mem_filter] at hQ397      rw [hQ.2.1, hQ.2.2]398  have hbound : ∀ ij : Fin n × Fin n, (S ij).card ≤ n := by399    intro ij400    have h1 : ∑ Q ∈ S ij, directionDegree k Q * D Q ≤ n := by401      rw [← hD, hsum]402      exact Finset.sum_le_sum_of_subset_of_nonneg (Finset.filter_subset _ _) (by intros; positivity)403    rw [hconst] at h1404    have : 1 ≤ (ij.1.val + 1) * (ij.2.val + 1) := Nat.one_le_iff_ne_zero.mpr (by positivity)405    nlinarith406  refine ⟨⟨fun ij => ⟨(S ij).card, Nat.lt_succ_of_le (hbound ij)⟩, fun ij => hcard ij, ?_⟩, ?_⟩407  · rw [residuePatterns, Finset.mem_filter]408    refine ⟨Finset.mem_univ _, ?_⟩409    unfold patternWeight410    have step1 : ∀ ij : Fin n × Fin n, (ij.1.val + 1) * (ij.2.val + 1) * (S ij).card411        = ∑ Q ∈ D.support, if (directionDegree k Q = ij.1.val + 1 ∧ D Q = ij.2.val + 1)412            then directionDegree k Q * D Q else 0 := by413      intro ij414      rw [← Finset.sum_filter, hconst, mul_comm]415    simp only [step1]416    rw [Finset.sum_comm, ← hD, hsum]417    apply Finset.sum_congr rfl418    intro Q hQ419    have hle : directionDegree k Q * D Q ≤ n := hD ▸ directionDegree_mul_le_exceptionalDegree k D Q420    have hD1 : 1 ≤ D Q := Nat.one_le_iff_ne_zero.mpr (Finsupp.mem_support_iff.mp hQ)421    have hd1 := hdeg Q422    have hA : directionDegree k Q ≤ n := by nlinarith423    have hB : D Q ≤ n := by nlinarith424    rw [Finset.sum_eq_single_of_mem (⟨directionDegree k Q - 1, by omega⟩, ⟨D Q - 1, by omega⟩)425      (Finset.mem_univ _)]426    · rw [if_pos]; simp only; constructor <;> omega427    · intro ij _ hne428      rw [if_neg]429      rintro ⟨h1, h2⟩430      apply hne431      ext <;> simp <;> omega432  · intro m m' hm hm'433    funext ij434    exact Fin.ext ((hm ij).symm.trans (hm' ij))435 436private theorem finite_directions_of_degree (k : Type) [Field k] [Finite k]437    (p : ClosedDirection k → Prop) (n : ℕ) :438    Finite {Q : ClosedDirection k // p Q ∧ directionDegree k Q = n} := by439  let f : {Q : ClosedDirection k // p Q ∧ directionDegree k Q = n} → Option (Fin (n+1) → k) :=440    fun Q => Option.map (fun φ : AffineDirection k => fun i : Fin (n+1) => φ.val.coeff i) Q.1441  refine Finite.of_injective f ?_442  rintro ⟨Q, hQ⟩ ⟨Q', hQ'⟩ h443  apply Subtype.ext444  simp only [f] at h445  cases Q with446  | none =>447    cases Q' with448    | none => rfl449    | some _ => simp at h450  | some φ =>451    cases Q' with452    | none => simp at h453    | some ψ =>454      simp only [Option.map_some, Option.some.injEq] at h455      change some φ = some ψ456      congr 1457      apply Subtype.ext458      apply Polynomial.ext459      intro i460      by_cases hi : i < n + 1461      · exact congrFun h ⟨i, hi⟩462      · have h1 : φ.val.natDegree < i := by simp [directionDegree] at hQ; omega463        have h2 : ψ.val.natDegree < i := by simp [directionDegree] at hQ'; omega464        rw [Polynomial.coeff_eq_zero_of_natDegree_lt h1,465          Polynomial.coeff_eq_zero_of_natDegree_lt h2]466 467private theorem coloring_count (T : Type) [Finite T] (r : ℕ) (m : Fin r → ℕ) :468    Finite {f : T → Option (Fin r) // ∀ j : Fin r, Nat.card {x // f x = some j} = m j} ∧469      ((Nat.card {f : T → Option (Fin r) // ∀ j : Fin r, Nat.card {x // f x = some j} = m j} : ℕ) :470      ℚ) = ((List.range (∑ i : Fin r, m i)).map fun j => (Nat.card T : ℚ) - j).prod / ∏ i : Fin r,471      (Nat.factorial (m i) : ℚ) := by472  refine ⟨inferInstance, ?_⟩473  obtain e := Finite.equivFin T474  have key : {f : T → Option (Fin r) // ∀ j : Fin r, Nat.card {x // f x = some j} = m j} ≃475      {f : Fin (Nat.card T) → Option (Fin r) //476        ∀ i : Fin r, Nat.card {x : Fin (Nat.card T) // f x = some i} = m i} := by477    refine Equiv.subtypeEquiv (Equiv.arrowCongr e (Equiv.refl _)) ?_478    intro f479    refine forall_congr' fun j => ?_480    have : Nat.card {x // f x = some j} =481        Nat.card {x : Fin (Nat.card T) // (Equiv.arrowCongr e (Equiv.refl _) f) x = some j} := by482      apply Nat.card_congr483      refine e.subtypeEquiv ?_484      intro x485      simp [Equiv.arrowCongr_apply]486    rw [this]487  rw [Nat.card_congr key, colored_subset_count]488 489private theorem exceptionalDegree_eq_patternWeight (k : Type) [Field k] (n : ℕ)490    (D : ExceptionalDivisor k) (m : Pattern n)491    (hb : ∀ Q, D Q ≠ 0 → directionDegree k Q ≤ n ∧ D Q ≤ n) (hA : HasArray k n D m) :492    exceptionalDegree k D = patternWeight m := by493  have hsum : exceptionalDegree k D = ∑ Q ∈ D.support, directionDegree k Q * D Q := rfl494  set S : Fin n × Fin n → Finset (ClosedDirection k) := fun ij =>495    D.support.filter (fun Q => directionDegree k Q = ij.1.val + 1 ∧ D Q = ij.2.val + 1) with hS496  have hcard : ∀ ij : Fin n × Fin n, (m ij).val = (S ij).card := by497    intro ij498    rw [← hA ij, ← Nat.card_eq_finsetCard]499    apply Nat.card_congr500    apply Equiv.subtypeEquivRight501    intro Q502    simp only [hS, Finset.mem_filter, Finsupp.mem_support_iff]503    constructor504    · intro h; exact ⟨by omega, h⟩505    · intro h; exact h.2506  have hconst : ∀ ij : Fin n × Fin n,507      ∑ Q ∈ S ij, directionDegree k Q * D Q = (S ij).card * ((ij.1.val + 1) * (ij.2.val + 1)) := by508    intro ij509    rw [Finset.sum_congr rfl (g := fun _ => (ij.1.val + 1) * (ij.2.val + 1))]510    · simp511    · intro Q hQ512      simp only [hS, Finset.mem_filter] at hQ513      rw [hQ.2.1, hQ.2.2]514  unfold patternWeight515  have step1 : ∀ ij : Fin n × Fin n, (ij.1.val + 1) * (ij.2.val + 1) * (m ij).val516      = ∑ Q ∈ D.support, if (directionDegree k Q = ij.1.val + 1 ∧ D Q = ij.2.val + 1)517          then directionDegree k Q * D Q else 0 := by518    intro ij519    rw [← Finset.sum_filter, hcard, hconst, mul_comm]520  simp only [step1]521  rw [Finset.sum_comm, hsum]522  apply Finset.sum_congr rfl523  intro Q hQ524  have hD0 : D Q ≠ 0 := Finsupp.mem_support_iff.mp hQ525  have hd1 := directionDegree_pos k Q526  have hA' := (hb Q hD0).1527  have hB := (hb Q hD0).2528  rw [Finset.sum_eq_single_of_mem (⟨directionDegree k Q - 1, by omega⟩, ⟨D Q - 1, by omega⟩)529    (Finset.mem_univ _)]530  · rw [if_pos]; simp only; constructor <;> omega531  · intro ij _ hne532    rw [if_neg]533    rintro ⟨h1, h2⟩534    apply hne535    ext <;> simp <;> omega536 537section538variable (k : Type) [Field k] (S : Set (ClosedDirection k)) (n : ℕ)539 540private abbrev DegPoints (i : Fin n) : Type := {Q : ClosedDirection k // Q ∈ S ∧ directionDegree k541    Q =542    i.val + 1}543 544private def degreeFiberEquiv (D : ExceptionalDivisor k) (hS : ∀ Q, D Q ≠ 0 → Q ∈ S) (i j : Fin n) :545    {Q : ClosedDirection k // directionDegree k Q = i.val + 1 ∧ D Q = j.val + 1} ≃546      {q : DegPoints k S n i // D q.1 = j.val + 1} where547  toFun Q := ⟨⟨Q.1, hS Q.1 (by omega), Q.2.1⟩, Q.2.2⟩548  invFun q := ⟨q.1.1, q.1.2.2, q.2⟩549  left_inv _ := rfl550  right_inv _ := rfl551 552open scoped Classical in553private noncomputable def divisorOfColoringFun (g : ∀ i : Fin n, DegPoints k S n i → Option (Fin n))554    (Q : ClosedDirection k) : ℕ :=555  if h : ∃ i : Fin n, Q ∈ S ∧ directionDegree k Q = i.val + 1 then556    (g h.choose ⟨Q, h.choose_spec⟩).elim 0 (fun j => j.val + 1) else 0557 558private theorem divisorOfColoringFun_support_finite [Finite k]559    (g : ∀ i : Fin n, DegPoints k S n i → Option (Fin n)) :560    (Function.support (divisorOfColoringFun k S n g)).Finite := by561  have : ∀ i, Finite (DegPoints k S n i) := fun i => finite_directions_of_degree k _ _562  refine Set.Finite.subset (Set.finite_iUnion fun i => Set.finite_range563      (Subtype.val : DegPoints k S n i → _)) ?_564  intro Q hQ565  simp only [Function.mem_support, divisorOfColoringFun] at hQ566  split_ifs at hQ with h567  · obtain ⟨i, hi⟩ := h568    exact Set.mem_iUnion.mpr ⟨i, ⟨Q, hi⟩, rfl⟩569  · exact absurd rfl hQ570 571private noncomputable def divisorOfColoring [Finite k]572    (g : ∀ i : Fin n, DegPoints k S n i → Option (Fin n)) : ExceptionalDivisor k :=573  Finsupp.ofSupportFinite (divisorOfColoringFun k S n g)574      (divisorOfColoringFun_support_finite k S n g)575 576private theorem divisorOfColoring_apply [Finite k]577    (g : ∀ i : Fin n, DegPoints k S n i → Option (Fin n)) (i : Fin n) (q : DegPoints k S n i) :578    divisorOfColoring k S n g q.1 = (g i q).elim 0 (fun j => j.val + 1) := by579  change divisorOfColoringFun k S n g q.1 = _580  have hex : ∃ i : Fin n, q.1 ∈ S ∧ directionDegree k q.1 = i.val + 1 := ⟨i, q.2⟩581  simp only [divisorOfColoringFun, dif_pos hex]582  have key : ∀ (i' : Fin n) (hi' : q.1 ∈ S ∧ directionDegree k q.1 = i'.val + 1), i' = i →583      (g i' ⟨q.1, hi'⟩).elim 0 (fun j => j.val + 1) = (g i q).elim 0 (fun j => j.val + 1) := by584    rintro _ _ rfl; rfl585  apply key586  apply Fin.ext587  have h1 := hex.choose_spec.2588  have h2 := q.2.2589  omega590 591private theorem divisorOfColoring_eq_zero [Finite k]592    (g : ∀ i : Fin n, DegPoints k S n i → Option (Fin n)) (Q : ClosedDirection k)593    (h : ¬ (∃ i : Fin n, Q ∈ S ∧ directionDegree k Q = i.val + 1)) :594    divisorOfColoring k S n g Q = 0 := by595  change divisorOfColoringFun k S n g Q = 0596  simp only [divisorOfColoringFun, dif_neg h]597 598private theorem divisorOfColoring_supp [Finite k]599    (g : ∀ i : Fin n, DegPoints k S n i → Option (Fin n)) :600    ∀ Q, divisorOfColoring k S n g Q ≠ 0 → Q ∈ S := by601  intro Q hQ602  by_contra hS603  exact hQ (divisorOfColoring_eq_zero k S n g Q (fun ⟨i, hi⟩ => hS hi.1))604 605private theorem divisorOfColoring_bound [Finite k]606    (g : ∀ i : Fin n, DegPoints k S n i → Option (Fin n)) :607    ∀ Q, divisorOfColoring k S n g Q ≠ 0 → directionDegree k Q ≤ n ∧608      divisorOfColoring k S n g Q ≤ n := by609  intro Q hQ610  by_cases h : ∃ i : Fin n, Q ∈ S ∧ directionDegree k Q = i.val + 1611  · obtain ⟨i, hi⟩ := h612    have := divisorOfColoring_apply k S n g i ⟨Q, hi⟩613    simp only at this614    rw [this]615    refine ⟨by omega, ?_⟩616    cases g i ⟨Q, hi⟩ with617    | none => simp618    | some j => have := j.2; simp; try omega619  · exact absurd (divisorOfColoring_eq_zero k S n g Q h) hQ620 621private theorem divisorOfColoring_hasArray [Finite k] (m : Pattern n)622    (g : ∀ i : Fin n, DegPoints k S n i → Option (Fin n))623    (hg : ∀ i j, Nat.card {q // g i q = some j} = (m (i, j)).val) :624    HasArray k n (divisorOfColoring k S n g) m := by625  intro ij626  obtain ⟨i, j⟩ := ij627  rw [Nat.card_congr (degreeFiberEquiv k S n _ (divisorOfColoring_supp k S n _) i j), ← hg i j]628  apply Nat.card_congr (Equiv.subtypeEquivRight fun q => ?_)629  rw [divisorOfColoring_apply k S n g i q]630  cases g i q with631  | none => simp632  | some j' => simp [Fin.ext_iff]633 634private def coloringOfDivisor (D : ExceptionalDivisor k) (hb : ∀ Q, D Q ≤ n) (i : Fin n)635    (q : DegPoints k S n i) : Option (Fin n) :=636  if h : D q.1 = 0 then none else some ⟨D q.1 - 1, by have := hb q.1; omega⟩637 638private theorem coloringOfDivisor_eq_some (D : ExceptionalDivisor k) (hb : ∀ Q, D Q ≤ n)639    (i j : Fin n) (q : DegPoints k S n i) :640    coloringOfDivisor k S n D hb i q = some j ↔ D q.1 = j.val + 1 := by641  simp only [coloringOfDivisor]642  split_ifs with h643  · simp; omega644  · simp only [Option.some.injEq, Fin.ext_iff]; omega645 646private theorem le_of_exceptionalDegree_eq (D : ExceptionalDivisor k)647    (hD : exceptionalDegree k D = n) : ∀ Q, D Q ≤ n := by648  intro Q649  have := directionDegree_mul_le_exceptionalDegree k D Q650  have := directionDegree_pos k Q651  nlinarith652 653end654 655/-- Counting divisors of degree `n` with a given array `m` and support in a point set `S` that has656`c δ` points of degree `δ`: their number is the product of falling factorials over multinomial657factors. -/658theorem divisor_count_of_point_set (k : Type) [Field k] [Finite k] (S : Set (ClosedDirection k))659    (c : ℕ → ℕ)660    (hc : ∀ δ : ℕ, 0 < δ → Nat.card {Q : ClosedDirection k // Q ∈ S ∧ directionDegree k661      Q = δ} = c δ) (n : ℕ) (m : Pattern n) (hm : m ∈ residuePatterns n) :662    Finite {D : ExceptionalDivisor k // (∀ Q, D Q ≠ 0 → Q ∈ S) ∧ exceptionalDegree k D = n ∧663      HasArray k n D m} ∧664      ((Nat.card {D : ExceptionalDivisor k // (∀ Q, D Q ≠ 0 → Q ∈ S) ∧ exceptionalDegree k D = n ∧665      HasArray k n D m} : ℕ) : ℚ) = ∏ i : Fin n,666      (((List.range (∑ j : Fin n, (m (i, j)).val)).map fun t => ((c (i.val + 1) : ℕ) : ℚ) -667      (t : ℚ)).prod / ∏ j : Fin n, ((Nat.factorial (m (i, j)).val : ℕ) : ℚ)) := by668  have hw : patternWeight m = n := (Finset.mem_filter.mp hm).2669  have hPfin : ∀ i, Finite (DegPoints k S n i) := fun i => finite_directions_of_degree k _ _670  let X := {D : ExceptionalDivisor k // (∀ Q, D Q ≠ 0 → Q ∈ S) ∧ exceptionalDegree k D = n ∧671      HasArray k n D m}672  let Y := ∀ i : Fin n, {f : DegPoints k S n i → Option (Fin n) // ∀ j : Fin n, Nat.card673      {q // f q = some j} = (m (i, j)).val}674  have e : X ≃ Y :=675    { toFun := fun D i => ⟨coloringOfDivisor k S n D.1 (le_of_exceptionalDegree_eq k n D.1 D.2.2.1)676        i, fun j => by677        rw [← D.2.2.2 (i, j), Nat.card_congr (degreeFiberEquiv k S n D.1 D.2.1 i j)]678        exact Nat.card_congr (Equiv.subtypeEquivRight fun q => coloringOfDivisor_eq_some k S n _ _679            i j q)⟩680      invFun := fun g => ⟨divisorOfColoring k S n (fun i => (g i).1), divisorOfColoring_supp k S n681          _, by682        have hA := divisorOfColoring_hasArray k S n m (fun i => (g i).1) (fun i j => (g i).2 j)683        exact ⟨(exceptionalDegree_eq_patternWeight k n _ m (divisorOfColoring_bound k S n _)684            hA).trans hw, hA⟩⟩685      left_inv := by686        rintro ⟨D, hS, hD, hA⟩687        apply Subtype.ext688        ext Q689        by_cases h : ∃ i : Fin n, Q ∈ S ∧ directionDegree k Q = i.val + 1690        · obtain ⟨i, hi⟩ := h691          have := divisorOfColoring_apply k S n (fun i => coloringOfDivisor k S n D692              (le_of_exceptionalDegree_eq k n D hD) i) i ⟨Q, hi⟩693          simp only at this ⊢694          rw [this]695          simp only [coloringOfDivisor]696          split_ifs with h0697          · simp [h0]698          · simp; omega699        · simp only700          rw [divisorOfColoring_eq_zero k S n _ Q h]701          by_contra h0702          have h1 := directionDegree_mul_le_exceptionalDegree k D Q703          have h2 := directionDegree_pos k Q704          have h3 : directionDegree k Q ≤ n := by705            have : 1 ≤ D Q := by omega706            nlinarith707          exact h ⟨⟨directionDegree k Q - 1, by omega⟩, hS Q (Ne.symm h0), by simp; omega⟩708      right_inv := by709        intro g710        funext i711        apply Subtype.ext712        funext q713        have hb := divisorOfColoring_apply k S n (fun i => (g i).1) i q714        simp only [coloringOfDivisor]715        split_ifs with h0716        · rw [hb] at h0717          cases h : (g i).1 q with718          | none => rfl719          | some j => simp [h] at h0720        · cases h : (g i).1 q with721          | none => rw [hb, h] at h0; exact absurd rfl h0722          | some j =>723            simp only [Option.some.injEq]724            apply Fin.ext725            simp only726            rw [hb, h]727            simp }728  have hYfin : ∀ i, Finite {f : DegPoints k S n i → Option (Fin n) //729      ∀ j : Fin n, Nat.card {q // f q = some j} = (m (i, j)).val} :=730    fun i => (coloring_count _ _ _).1731  refine ⟨Finite.of_equiv _ e.symm, ?_⟩732  rw [Nat.card_congr e, Nat.card_pi, Nat.cast_prod]733  refine Finset.prod_congr rfl fun i _ => ?_734  rw [(coloring_count (DegPoints k S n i) n (fun j => (m (i, j)).val)).2, hc _ (Nat.succ_pos _)]735 736/-- If the points of `S` of each degree `δ > 0` are counted by `availablePoints offset δ` at737`q = |k|`, then the divisors of degree `n` supported on `S` with array `m` are counted by738`divisorCount offset m` at `q`. -/739theorem divisor_count_eval_of_point_count (k : Type) [Field k] [Finite k]740    (S : Set (ClosedDirection k)) (offset : ℤ)741    (hS : ∀ δ : ℕ, 0 < δ → ((Nat.card {Q : ClosedDirection k // Q ∈ S ∧ directionDegree k Q = δ} :742      ℕ) : ℚ) = (availablePoints offset δ).eval (Nat.card k))743    (n : ℕ) (m : Pattern n) (hm : m ∈ residuePatterns n) :744    Finite {D : ExceptionalDivisor k // (∀ Q, D Q ≠ 0 → Q ∈ S) ∧ exceptionalDegree k D = n ∧745      HasArray k n D m} ∧746      ((Nat.card {D : ExceptionalDivisor k // (∀ Q, D Q ≠ 0 → Q ∈ S) ∧ exceptionalDegree k D = n ∧747      HasArray k n D m} : ℕ) : ℚ) = (divisorCount offset m).eval (Nat.card k) := by748  obtain ⟨hfin, h⟩ := divisor_count_of_point_set k S _ (fun _ _ ↦ rfl) n m hm749  refine ⟨hfin, ?_⟩750  rw [h]751  unfold divisorCount752  rw [expression_prod_eval, List.map_map, ← Finset.prod_map_toList]753  congr 1754  apply List.map_congr_left755  intro i _756  simp only [Function.comp, Expr.eval, falling, expression_prod_eval, List.map_map,757      div_eq_mul_inv, one_mul]758  congr 1759  congr 1760  apply List.map_congr_left761  intro t _762  simp only [Function.comp, Expr.sub, Expr.neg, Expr.eval]763  rw [hS (i.val + 1) (Nat.succ_pos _)]764  ring_nf765 766/-- The number of affine divisors of degree `n` with array `m` is `divisorCount 0 m` evaluated at767the residue field size. -/768theorem affine_divisor_count (k : Type) [Field k] [Finite k] (n : ℕ) (m : Pattern n)769    (hm : m ∈ residuePatterns n) :770    Finite {D : ExceptionalDivisor k // AffineDivisor k n D ∧ HasArray k n D m} ∧771      ((Nat.card {D : ExceptionalDivisor k // AffineDivisor k n D ∧ HasArray k n D m} : ℕ) : ℚ) =772      (divisorCount 0 m).eval (Nat.card k) := by773  have hc : ∀ δ : ℕ, 0 < δ → ((Nat.card {Q : ClosedDirection k // Q ∈774      {Q : ClosedDirection k | Q ≠ none} ∧ directionDegree k Q = δ} : ℕ) : ℚ) =775      (availablePoints 0 δ).eval (Nat.card k) := by776    intro δ hδ777    have h915 := nonboundary_direction_count k (State.single 1 1) δ hδ778    simp only at h915779    rw [← h915]780    congr 1781  have h := divisor_count_eval_of_point_count k {Q : ClosedDirection k | Q ≠ none} 0 hc n m hm782  have e : ∀ D : ExceptionalDivisor k, ((∀ Q, D Q ≠ 0 → Q ∈ {Q : ClosedDirection k | Q ≠ none}) ∧783      exceptionalDegree k D = n ∧ HasArray k n D m) ↔ (AffineDivisor k n D ∧ HasArray k n D m) := by784    intro D785    simp only [AffineDivisor, infinityDirection, Set.mem_ofPred_eq]786    constructor787    · rintro ⟨h1, h2, h3⟩788      exact ⟨⟨by by_contra hh; exact h1 _ hh rfl, h2⟩, h3⟩789    · rintro ⟨⟨h1, h2⟩, h3⟩790      exact ⟨fun Q hQ hQn => hQ (hQn ▸ h1), h2, h3⟩791  have eq := Equiv.subtypeEquivRight e792  have := h.1793  exact ⟨Finite.of_equiv _ eq, by rw [← Nat.card_congr eq, h.2]⟩794 795/-- Basic properties of the divisor vector of a divisor `D` of degree `n`: the affine polynomial of796`D` is monic of degree `n - D ∞`, it is the form polynomial of the divisor vector, whose entry at797`n - D ∞` is `1` and whose higher entries vanish. -/798theorem divisor_vector_properties (k : Type) [Field k] (n : ℕ) (D : ExceptionalDivisor k)799    (hD : exceptionalDegree k D = n) :800    (divisorAffinePolynomial k D).Monic ∧ (divisorAffinePolynomial k D).natDegree = n - D801      (infinityDirection k) ∧ D (infinityDirection k) ≤ n ∧ formPoly (divisorVector k n D) =802      divisorAffinePolynomial k D ∧ divisorVector k n D (⟨n - D (infinityDirection k),803      Nat.lt_succ_of_le (Nat.sub_le _ _)⟩ :804      Fin (n+1)) = 1 ∧ (∀ i : Fin (n+1), n - D (infinityDirection k) < i.val → divisorVector k n D805      i = 0) ∧ divisorVector k n D ≠ 0 := by806  classical807  set g : ClosedDirection k → ℕ → Polynomial k :=808    fun P r => (match P with | none => 1 | some phi => phi.val ^ r) with hg809  have hmon : ∀ P r, (g P r).Monic := by810    intro P r811    cases P with812    | none => exact Polynomial.monic_one813    | some phi => exact phi.property.1.pow r814  have hM : (divisorAffinePolynomial k D).Monic := by815    unfold divisorAffinePolynomial816    exact Polynomial.monic_prod_of_monic _ _ (fun P _ => hmon P (D P))817  have hdeg : (divisorAffinePolynomial k D).natDegree = ∑ P ∈ D.support, (g P (D P)).natDegree := by818    unfold divisorAffinePolynomial819    exact Polynomial.natDegree_prod_of_monic _ _ (fun P _ => hmon P (D P))820  have hsum : exceptionalDegree k D = (divisorAffinePolynomial k D).natDegree + D none := by821    rw [hdeg]822    have : ∀ P ∈ D.support, directionDegree k P * D P = (g P (D P)).natDegree +823        (if none = P then D P else 0) := by824      intro P _825      cases P with826      | none => simp [directionDegree, hg]827      | some phi => simp [directionDegree, hg, Polynomial.natDegree_pow]; ring828    unfold exceptionalDegree Finsupp.sum829    rw [Finset.sum_congr rfl this, Finset.sum_add_distrib]830    congr 1831    by_cases h : none ∈ D.support832    · rw [Finset.sum_eq_single none]833      · simp834      · intro b _ hb; exact if_neg (Ne.symm hb)835      · intro h'; exact absurd h h'836    · have : D none = 0 := by simpa using h837      simp [this]838  have hinf : infinityDirection k = none := rfl839  simp only [hinf]840  have h1 : (divisorAffinePolynomial k D).natDegree = n - D none := by omega841  have h2 : D none ≤ n := by omega842  have hle : (divisorAffinePolynomial k D).natDegree < n + 1 := by omega843  have hcoef : divisorVector k n D (⟨n - D none, by omega⟩ : Fin (n+1)) = 1 := by844    change (divisorAffinePolynomial k D).coeff (n - D none) = 1845    rw [← h1]; exact hM846  refine ⟨hM, h1, h2, ?_, hcoef, ?_, ?_⟩847  · unfold formPoly848    conv_rhs => rw [Polynomial.as_sum_range' _ (n+1) hle]849    rw [← Fin.sum_univ_eq_sum_range (fun i => Polynomial.monomial i850        ((divisorAffinePolynomial k D).coeff i))]851    refine Finset.sum_congr rfl (fun i _ => ?_)852    rw [Polynomial.C_mul_X_pow_eq_monomial]; rfl853  · intro i hi854    exact Polynomial.coeff_eq_zero_of_natDegree_lt (by omega)855  · intro h0856    have := congrFun h0 ⟨n - D none, by omega⟩857    rw [hcoef] at this858    simp at this859 860section861open Polynomial862 863private lemma formPoly_coeff {A : Type} [CommRing A] {d : ℕ} (v : Fin (d + 1) → A)864    (i : Fin (d + 1)) :865    (formPoly v).coeff i = v i := by866  simp only [formPoly, finsetSum_coeff, coeff_C_mul, coeff_X_pow]867  rw [Finset.sum_eq_single i]868  · simp869  · intro b _ hb; rw [if_neg (fun h => hb (Fin.ext h).symm), mul_zero]870  · simp871 872/-- The form polynomial of a vector of length `d + 1` has degree at most `d`. -/873theorem formPoly_natDegree_le {A : Type} [CommRing A] {d : ℕ} (v : Fin (d + 1) → A) :874    (formPoly v).natDegree ≤ d := by875  unfold formPoly876  refine natDegree_sum_le_of_forall_le _ _ (fun i _ => ?_)877  exact (natDegree_C_mul_X_pow_le _ _).trans (Nat.lt_succ_iff.mp i.2)878 879private lemma formPoly_map {A B : Type} [CommRing A] [CommRing B] (f : A →+* B) {d : ℕ}880    (v : Fin (d + 1) → A) : (formPoly v).map f = formPoly (fun i => f (v i)) := by881  simp [formPoly, Polynomial.map_sum]882 883private lemma formPoly_insertOne_last {A : Type} [CommRing A] {d : ℕ} (b : Fin d → A) :884    formPoly (insertOne (Fin.last d) b) = monicPolyO b := by885  simp [formPoly, insertOne, monicPolyO, Fin.sum_univ_castSucc, Fin.insertNth_last', add_comm]886 887private lemma formPoly_single_zero {A : Type} [CommRing A] {d : ℕ} :888    formPoly (Pi.single (0 : Fin (d+1)) (1 : A)) = 1 := by889  unfold formPoly890  rw [Fintype.sum_eq_single 0]891  · simp892  · intro i hi; simp [hi]893 894private lemma coeff_prod_sum_of_natDegree_le {A ι : Type} [CommRing A] (s : Finset ι) (p : ι → A[X])895    (d : ι → ℕ) (h : ∀ i ∈ s, (p i).natDegree ≤ d i) :896    (∏ i ∈ s, p i).coeff (∑ i ∈ s, d i) = ∏ i ∈ s, (p i).coeff (d i) := by897  classical898  induction s using Finset.induction_on with899  | empty => simp900  | insert a s ha ih =>901    rw [Finset.prod_insert ha, Finset.sum_insert ha, Finset.prod_insert ha,902      coeff_mul_add_eq_of_natDegree_le (h a (by simp)), ih (fun i hi => h i (by simp [hi]))]903    exact (natDegree_prod_le _ _).trans (Finset.sum_le_sum fun i hi => h i (by simp [hi]))904 905end906 907/-! ### Type events on products of cells -/908 909section ProductCells910 911variable {ι Y : Type} [Fintype ι] {X : ι → Type}912 913/-- If `f` maps the product of the cells `C j` into `E₀`, and a point `a` of that product has914`f a ∈ P` exactly when `a j ∈ Ev j (τ j)` for some `τ` with `σ = ∑ j, τ j`, then the trace of915`f ⁻¹' (E₀ ∩ P)` on the product is a finite union of products of events. -/916theorem preimage_inter_pi_eq_biUnion (f : (∀ j, X j) → Y) (C : ∀ j, Set (X j))917    (E₀ P : Set Y) (hf : Set.MapsTo f (Set.pi Set.univ C) E₀) (Ev : ∀ j, FactorType → Set (X j))918    (W : ι → Finset FactorType) (hW : ∀ j τ, (C j ∩ Ev j τ).Nonempty → τ ∈ W j)919    (σ : FactorType) (hP : ∀ a ∈ Set.pi Set.univ C,920      f a ∈ P ↔ ∃ τ : ι → FactorType, (∀ j, a j ∈ Ev j (τ j)) ∧ σ = ∑ j, τ j)921    (T : Finset (ι → FactorType)) (hT : ∀ τ, τ ∈ T ↔ (∀ j, τ j ∈ W j) ∧ σ = ∑ j, τ j) :922    f ⁻¹' (E₀ ∩ P) ∩ Set.pi Set.univ C = ⋃ τ ∈ T, Set.pi Set.univ fun j ↦ C j ∩ Ev j (τ j) := by923  ext a924  simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_iUnion, hT, Set.mem_univ_pi,925    exists_prop, forall_and]926  constructor927  · rintro ⟨⟨-, haP⟩, haC⟩928    obtain ⟨τ, hτ, hσ⟩ := (hP a (Set.mem_univ_pi.2 haC)).1 haP929    exact ⟨τ, ⟨fun j ↦ hW j (τ j) ⟨a j, haC j, hτ j⟩, hσ⟩, haC, hτ⟩930  · rintro ⟨τ, ⟨-, hσ⟩, haC, hτ⟩931    have ha := Set.mem_univ_pi.2 haC932    exact ⟨⟨hf ha, (hP a ha).2 ⟨τ, hτ, hσ⟩⟩, haC⟩933 934omit [Fintype ι] in935/-- Products of events `Ev j (τ j)` are pairwise disjoint for distinct `τ` when each family936`Ev j` is pairwise disjoint. -/937theorem pairwiseDisjoint_pi_events (C : ∀ j, Set (X j)) (Ev : ∀ j, FactorType → Set (X j))938    (huniq : ∀ j τ τ' x, x ∈ Ev j τ → x ∈ Ev j τ' → τ = τ') (T : Set (ι → FactorType)) :939    T.PairwiseDisjoint fun τ ↦ Set.pi Set.univ fun j ↦ C j ∩ Ev j (τ j) :=940  fun _ _ _ _ hne ↦ Set.disjoint_left.2 fun _ ha ha' ↦ hne <| funext fun j ↦941    huniq j _ _ _ (ha j (Set.mem_univ _)).2 (ha' j (Set.mem_univ _)).2942 943/-- If `f` is continuous and bijective from a closed subset `C` of a compact space onto `E₀`, and944the trace on `C` of `f ⁻¹' (E₀ ∩ A)` is measurable, then `E₀ ∩ A` is measurable. -/945theorem measurableSet_inter_of_bijOn {Z : Type} [TopologicalSpace Z] [CompactSpace Z]946    [MeasurableSpace Z] [BorelSpace Z] [TopologicalSpace Y] [T2Space Y] [MeasurableSpace Y]947    [BorelSpace Y] {f : Z → Y} {C : Set Z} {E₀ A : Set Y} (hC : IsClosed C)948    (hf : ContinuousOn f C) (hbij : Set.BijOn f C E₀) (hA : MeasurableSet (f ⁻¹' (E₀ ∩ A) ∩ C)) :949    MeasurableSet (E₀ ∩ A) := by950  have := image_measurable_of_continuousOn_injOn_compact Z Y f C hC hf hbij.injOn _ hA951  rwa [Set.inter_assoc, Set.inter_self, Set.image_preimage_inter, hbij.image_eq,952    Set.inter_assoc, Set.inter_comm A, ← Set.inter_assoc, Set.inter_self] at this953 954open MeasureTheory in955/-- If `f` is measure preserving from `Measure.pi m` to `ν`, the product of the cells `C j` is956conull, and the trace on it of `f ⁻¹' E` is the finite union over `τ ∈ T` of products of the957measurable factor events `C j ∩ Ev j (τ j)` (each family `Ev j` being pairwise disjoint), then the958`ν`-mass of `E` is the sum over `T` of the products of the factor masses. -/959theorem measure_eq_sum_prod_of_preimage [∀ j, MeasurableSpace (X j)] [MeasurableSpace Y]960    (m : ∀ j, Measure (X j)) [∀ j, SigmaFinite (m j)] {ν : Measure Y} {f : (∀ j, X j) → Y}961    (hf : MeasurePreserving f (Measure.pi m) ν) (C : ∀ j, Set (X j))962    (hC : Measure.pi m (Set.pi Set.univ C)ᶜ = 0) (hm : ∀ j s, m j (C j ∩ s) = m j s)963    (Ev : ∀ j, FactorType → Set (X j)) (hEv : ∀ j τ, MeasurableSet (C j ∩ Ev j τ))964    (huniq : ∀ j τ τ' x, x ∈ Ev j τ → x ∈ Ev j τ' → τ = τ') {E : Set Y} (hE : MeasurableSet E)965    (T : Finset (ι → FactorType))966    (hpre : f ⁻¹' E ∩ Set.pi Set.univ C = ⋃ τ ∈ T, Set.pi Set.univ fun j ↦ C j ∩ Ev j (τ j)) :967    ν E = ∑ τ ∈ T, ∏ j, m j (Ev j (τ j)) := by968  rw [← hf.measure_preimage hE.nullMeasurableSet, ← measure_inter_conull hC, hpre,969    measure_biUnion_finset (pairwiseDisjoint_pi_events C Ev huniq _)970      fun τ _ ↦ .univ_pi fun j ↦ hEv j (τ j)]971  simp only [Measure.pi_pi, hm]972 973/-- The finite convolution of the factor densities over any finite sets of types `W j` containing974the supports of the laws `Dl j` is the density of the product law. -/975theorem sum_prod_densityValue_eq_lawProd {L : ℕ} (Dl : Fin L → Law) (q : ℕ)976    (hnn : ∀ j τ, 0 ≤ (lawCoeff (Dl j) τ).eval (q : ℚ)) (W : Fin L → Finset FactorType)977    (hW : ∀ j, ((Dl j).map Prod.fst).toFinset ⊆ W j) (σ : FactorType) :978    ∑ τ ∈ (Fintype.piFinset W).filter (fun τ ↦ σ = ∑ j, τ j),979      ∏ j, densityValue (lawCoeff (Dl j) (τ j)) q =980        densityValue (lawCoeff (lawProd (List.ofFn Dl)) σ) q := by981  have hy : ∀ j τ, (0 : ℝ) ≤ (((lawCoeff (Dl j) τ).eval (q : ℚ) : ℚ) : ℝ) := fun j τ ↦ by982    exact_mod_cast hnn j τ983  simp only [densityValue]984  rw [Finset.sum_congr rfl fun τ _ ↦ (ENNReal.ofReal_prod_of_nonneg fun j _ ↦ hy j (τ j)).symm,985    ← ENNReal.ofReal_sum_of_nonneg fun τ _ ↦ Finset.prod_nonneg fun j _ ↦ hy j (τ j)]986  obtain ⟨hform, hzero⟩ := law_coeff_prod_formula L Dl σ (q : ℚ)987  rw [hform, Finset.sum_filter]988  simp only [Rat.cast_sum, apply_ite (Rat.cast : ℚ → ℝ), Rat.cast_prod, Rat.cast_zero]989  refine congrArg _ (Finset.sum_subset (Fintype.piFinset_subset _ _ hW) fun τ _ hτ ↦ ?_).symm990  obtain ⟨j, hj⟩ := not_forall.1 (Fintype.mem_piFinset.not.1 hτ)991  rw [Finset.prod_eq_zero (Finset.mem_univ j) (by simp [hzero (Dl j) (τ j) hj]), ite_self]992 993end ProductCells994 995/-! ### Products of reduced forms -/996 997open Polynomial in998/-- A product of reduced forms has type `σ` iff all factor polynomials keep their top coefficient999and the product of the normalized factors has type `σ`. -/1000private theorem form_product_mem_affineTypeEvent_iff (O : Type) [CommRing O] [IsDomain O]1001    [IsDiscreteValuationRing O]1002    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (L : ℕ)1003    (d : Fin L → ℕ) (ν : ∀ j, Fin (d j + 1)) (g : ∀ j, Fin (d j + 1) → IsLocalRing.ResidueField O)1004    (μ : Fin ((∑ j, d j) + 1)) (hμ : formProd d g μ = 1) (a : ∀ j, Fin (d j) → O)1005    (ha : a ∈ Set.pi Set.univ (fun j => reducedFormCell O (d j) (ν j) (g j))) (σ : FactorType) :1006    insertOne μ (reducedFormProduct O d ν g μ a) ∈ affineTypeEvent O (∑ j, d j) σ ↔1007      (∀ j, (formPoly (insertOne (ν j) (a j))).coeff (d j) ≠ 0) ∧1008        HasPolynomialTypeF O (∏ j, C (algebraMap O (BaseField O)1009          ((formPoly (insertOne (ν j) (a j))).coeff (d j)))⁻¹ *1010          (formPoly (insertOne (ν j) (a j))).map (algebraMap O (BaseField O))) σ := by1011  have hcell : ∀ j, a j ∈ reducedFormCell O (d j) (ν j) (g j) := fun j ↦ ha j (Set.mem_univ _)1012  obtain ⟨-, -, hu, -⟩ := form_product_maps_to_and_preserves O (Fin L) d ν g μ hμ a a ha ha1013  set ι := algebraMap O (BaseField O)1014  have hι : ∀ {x : O}, x ≠ 0 → ι x ≠ 0 := (map_ne_zero_iff _ (IsFractionRing.injective O _)).21015  set p : Fin L → O[X] := fun j ↦ formPoly (insertOne (ν j) (a j))1016  set c : Fin L → O := fun j ↦ (p j).coeff (d j)1017  set F : Fin L → (BaseField O)[X] := fun j ↦ C (ι (c j))⁻¹ * (p j).map ι with hF1018  set Q := ∏ j, p j1019  change IsUnit (Q.coeff μ) at hu1020  set u := Ring.inverse (Q.coeff μ)1021  have hu0' : u ≠ 0 := left_ne_zero_of_mul_eq_one (Ring.inverse_mul_cancel _ hu)1022  have hu0 : ι u ≠ 0 := hι hu0'1023  have hQn : Q.coeff (∑ j, d j) = ∏ j, c j :=1024    coeff_prod_sum_of_natDegree_le _ _ _ fun j _ ↦ formPoly_natDegree_le _1025  have hred : insertOne μ (reducedFormProduct O d ν g μ a) =1026      fun i : Fin ((∑ j, d j) + 1) ↦ u * Q.coeff i := by1027    unfold reducedFormProduct1028    rw [if_pos hcell]1029    have := Fin.insertNth_self_removeNth μ1030      (normalizeAt μ (formProd d fun j ↦ insertOne (ν j) (a j)))1031    rw [normalizeAt, Pi.smul_apply, smul_eq_mul, Ring.inverse_mul_cancel1032      (formProd d (fun j ↦ insertOne (ν j) (a j)) μ) hu] at this1033    exact this1034  have hAff : affinePolynomial O (fun i : Fin ((∑ j, d j) + 1) ↦ u * Q.coeff i) =1035      C (ι u) * Q.map ι := by1036    have hlt : (Q.map ι).natDegree < ∑ j, d j + 1 := Nat.lt_succ_of_le (natDegree_map_le.trans1037      ((natDegree_prod_le _ _).trans (Finset.sum_le_sum fun j _ ↦ formPoly_natDegree_le _)))1038    conv_rhs => rw [as_sum_range' (Q.map ι) _ hlt]1039    rw [affinePolynomial, Finset.mul_sum, ← Fin.sum_univ_eq_sum_range]1040    refine Finset.sum_congr rfl fun i _ ↦ ?_1041    rw [← C_mul_X_pow_eq_monomial, coeff_map, map_mul, C_mul, mul_assoc]1042  have hprod : C (ι (u * Q.coeff (∑ j, d j)))⁻¹ * (C (ι u) * Q.map ι) = ∏ j, F j := by1043    rw [hF, Finset.prod_mul_distrib, ← map_prod C, ← Polynomial.map_prod, hQn, map_mul, mul_inv,1044      C_mul, mul_mul_mul_comm, ← C_mul, inv_mul_cancel₀ hu0, C_1, one_mul, map_prod,1045      Finset.prod_inv_distrib]1046  have hι' : algebraMap O (BaseField O) = ι := rfl1047  simp only [affineTypeEvent, hred, Set.mem_ofPred_eq, hAff, Fin.val_last, hι', hprod]1048  rw [hQn, mul_ne_zero_iff, Finset.prod_ne_zero_iff]1049  simp [hu0', c, p]1050 1051open Polynomial in1052/-- A product of reduced forms has type `σ` iff its factors have types `τ j` (block types at the1053infinity factor) with `σ = ∑ j, τ j`. -/1054private theorem form_product_type_iff (O : Type) [CommRing O] [IsDomain O]1055    [IsDiscreteValuationRing O]1056    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (L : ℕ)1057    (d : Fin L → ℕ) (ν : ∀ j, Fin (d j + 1)) (g : ∀ j, Fin (d j + 1) → IsLocalRing.ResidueField O)1058    (hc : FormsCoprime d g) (μ : Fin ((∑ j, d j) + 1))1059    (hμ : formProd d g μ = 1) (inf : Fin L → Bool)1060    (hclass : ∀ j, if inf j = true then (ν j = 0 ∧ g j = Pi.single 0 1) else ν j = Fin.last (d j))1061    (hone : ∀ i j, inf i = true → inf j = true → i = j) (a : ∀ j, Fin (d j) → O)1062    (ha : a ∈ Set.pi Set.univ (fun j => reducedFormCell O (d j) (ν j) (g j))) (σ : FactorType) :1063    insertOne μ (reducedFormProduct O d ν g μ a) ∈ affineTypeEvent O (∑ j, d j) σ ↔1064      ∃ τ : Fin L → FactorType, (∀ j, a j ∈1065        if inf j = true then infinityBlockEvent O (d j) (τ j) else typeEvent O (d j) (τ j)) ∧1066        σ = ∑ j, τ j := by1067  -- strategy: reduce to the normalized factors `F j`, which are pairwise coprime1068  rw [form_product_mem_affineTypeEvent_iff O L d ν g μ hμ a ha σ]1069  have hcell : ∀ j, a j ∈ reducedFormCell O (d j) (ν j) (g j) := fun j ↦ ha j (Set.mem_univ _)1070  set ι := algebraMap O (BaseField O)1071  have hι : ∀ {x : O}, x ≠ 0 → ι x ≠ 0 := (map_ne_zero_iff _ (IsFractionRing.injective O _)).21072  set p : Fin L → O[X] := fun j ↦ formPoly (insertOne (ν j) (a j))1073  set c : Fin L → O := fun j ↦ (p j).coeff (d j)1074  set F : Fin L → (BaseField O)[X] := fun j ↦ C (ι (c j))⁻¹ * (p j).map ι with hF1075  have hpred : ∀ j, (p j).map (IsLocalRing.residue O) = formPoly (g j) := fun j ↦ by1076    simp only [p, formPoly_map]; exact congrArg formPoly (hcell j).21077  have hpfin : ∀ j, inf j = false → p j = monicPolyO (a j) := fun j hj ↦ by1078    have hcl := hclass j1079    rw [if_neg (by simp [hj])] at hcl1080    simp only [p, hcl, formPoly_insertOne_last]1081  have hpinf : ∀ j, inf j = true → (p j).map (IsLocalRing.residue O) = 1 := fun j hj ↦ by1082    have hcl := hclass j1083    rw [if_pos hj] at hcl1084    rw [hpred, hcl.2, formPoly_single_zero]1085  have hmon : ∀ j, (monicPolyO (a j)).Monic := fun j ↦ (monic_poly_reconstruct O _ (a j)).11086  have hblock : ∀ j (t : FactorType),1087      (a j ∈ if inf j = true then infinityBlockEvent O (d j) t else typeEvent O (d j) t) ↔1088        c j ≠ 0 ∧ HasPolynomialTypeF O (F j) t := by1089    intro j t1090    by_cases hj : inf j = true1091    · have hcl := hclass j1092      rw [if_pos hj] at hcl ⊢1093      simp only [infinityBlockEvent, Set.mem_ofPred_eq, F, c, p, hcl.1, ι]1094    · rw [if_neg hj]1095      obtain ⟨hm, hd, -⟩ := monic_poly_reconstruct O _ (a j)1096      have hc1 : c j = 1 := by simp only [c, hpfin j (by simpa using hj), ← hd]; exact hm1097      simp [typeEvent, hF, hc1, hpfin j (by simpa using hj), ι, monicPolyO_map_fraction]1098  have hcop : (∀ j, c j ≠ 0) → ∀ i j, i ≠ j → IsCoprime (F i) (F j) := by1099    intro hall i j hij1100    have hU : ∀ k, IsUnit (C (ι (c k))⁻¹) := fun k ↦1101      isUnit_C.mpr (IsUnit.mk0 _ (inv_ne_zero (hι (hall k))))1102    rw [hF, isCoprime_mul_units_left (hU i) (hU j)]1103    rcases hi : inf i with _ | _ <;> rcases hj : inf j with _ | _1104    · rw [hpfin i hi, hpfin j hj]1105      refine coprime_of_coprime_residue_dvr O (BaseField O) _ _ (hmon i) (hmon j) ?_1106      rw [← hpfin i hi, ← hpfin j hj, hpred, hpred]1107      exact hc.1 i j hij1108    · rw [hpfin i hi]1109      exact coprime_of_monic_reduction_one O (BaseField O) _ _ (hmon i) (hpinf j hj)1110    · rw [hpfin j hj]1111      exact (coprime_of_monic_reduction_one O (BaseField O) _ _ (hmon j) (hpinf i hi)).symm1112    · exact absurd (hone i j hi hj) hij1113  simp only [hblock]1114  by_cases hall : ∀ j, c j ≠ 01115  · rw [coprime_family_type_iff O (Fin L) F (fun j ↦ ?_) (hcop hall) σ]1116    · exact ⟨fun ⟨_, τ, h1, h2⟩ ↦ ⟨τ, fun j ↦ ⟨hall j, h1 j⟩, h2⟩,1117        fun ⟨τ, h1, h2⟩ ↦ ⟨hall, τ, fun j ↦ (h1 j).2, h2⟩⟩1118    have hdeg : ((p j).map ι).natDegree = d j := natDegree_eq_of_le_of_coeff_ne_zero1119      (natDegree_map_le.trans (formPoly_natDegree_le _)) (by rw [coeff_map]; exact hι (hall j))1120    rw [Monic, hF, leadingCoeff_mul, leadingCoeff_C, leadingCoeff, hdeg, coeff_map,1121      inv_mul_cancel₀ (hι (hall j))]1122  · exact ⟨fun ⟨h, _⟩ ↦ absurd h hall, fun ⟨τ, h1, _⟩ ↦ absurd (fun j ↦ (h1 j).1) hall⟩1123 1124/-- A factorization type occurring in a block event of a cell of degree `d` has degree at most1125`d`, so it lies in a fixed finite set of types. -/1126private theorem type_mem_of_event_nonempty (O : Type) [CommRing O] [IsDomain O]1127    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1128    [Finite (IsLocalRing.ResidueField O)] (d : ℕ) (ν : Fin (d + 1))1129    (g : Fin (d + 1) → IsLocalRing.ResidueField O) (b : Bool) (τ : FactorType)1130    (h : (reducedFormCell O d ν g ∩1131      (if b = true then infinityBlockEvent O d τ else typeEvent O d τ)).Nonempty) :1132    τ ∈ (Finset.range (d + 1)).biUnion fun n ↦ (finite_types_of_degree n).toFinset := by1133  obtain ⟨a, _, ha⟩ := h1134  obtain ⟨F, hF, hdeg⟩ : ∃ F : Polynomial (BaseField O),1135      HasPolynomialTypeF O F τ ∧ F.natDegree ≤ d := by1136    split_ifs at ha1137    · exact ⟨_, ha.2, (Polynomial.natDegree_C_mul_le _ _).trans1138        (Polynomial.natDegree_map_le.trans (formPoly_natDegree_le _))⟩1139    · exact ⟨_, ha, (monic_polynomial_degree O d a).2.le⟩1140  obtain ⟨hv, htd⟩ := polynomial_type_degree O F τ hF1141  simp only [Finset.mem_biUnion, Finset.mem_range, Set.Finite.mem_toFinset]1142  exact ⟨typeDegree τ, by omega, hv, rfl⟩1143 1144section1145 1146open MeasureTheory1147 1148/-- **Product law.** If the factor cells have laws `Dl j`, then the product cell has law1149`lawProd (List.ofFn Dl)`. -/1150theorem form_product_type_event_law (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]1151    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]1152    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]1153    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]1154    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (L : ℕ) (d : Fin L → ℕ) (ν : ∀ j, Fin (d j + 1))1155    (g : ∀ j, Fin (d j + 1) → IsLocalRing.ResidueField O) (hgν : ∀ j, g j (ν j) = 1)1156    (hc : FormsCoprime d g) (μ : Fin ((∑ j, d j) + 1)) (hμ : formProd d g μ = 1)1157    (inf : Fin L → Bool)1158    (hclass : ∀ j, if inf j = true then (ν j = 0 ∧ g j = Pi.single 0 1) else ν j = Fin.last (d j))1159    (hone : ∀ i j, inf i = true → inf j = true → i = j) (Dl : Fin L → Law)1160    (hnn : ∀ (j : Fin L) (τ : FactorType), 0 ≤ (lawCoeff (Dl j) τ).eval1161      (Nat.card (IsLocalRing.ResidueField O)))1162    (hlaw : ∀ (j : Fin L) (τ : FactorType), MeasurableSet1163      (reducedFormCell O (d j) (ν j) (g j) ∩ (if inf j = true then infinityBlockEvent O (d j) τ1164      else typeEvent O (d j) τ)) ∧ cellMeasure O (d j) (reducedFormCell O (d j) (ν j) (g j))1165      (if inf j = true then infinityBlockEvent O (d j) τ else typeEvent O (d j) τ) = densityValue1166      (lawCoeff (Dl j) τ) (Nat.card (IsLocalRing.ResidueField O))) (σ : FactorType) :1167    MeasurableSet (reducedFormCell O (∑ j, d j) μ (formProd d g) ∩1168      (insertOne μ ⁻¹' affineTypeEvent O (∑ j, d j) σ)) ∧ cellMeasure O (∑ j, d j)1169      (reducedFormCell O (∑ j, d j) μ (formProd d g)) (insertOne μ ⁻¹' affineTypeEvent O (∑ j, d j)1170      σ) = densityValue (lawCoeff (lawProd (List.ofFn Dl)) σ)1171      (Nat.card (IsLocalRing.ResidueField O)) := by1172  have hcellj := fun j => normalized_form_cell_cylinder_mass O htop (d j) (ν j) (g j) (hgν j)1173  have hcellD := normalized_form_cell_cylinder_mass O htop (∑ j, d j) μ (formProd d g) hμ1174  have : ∀ j, IsProbabilityMeasure (cellMeasure O (d j) (reducedFormCell O (d j) (ν j) (g j))) :=1175    fun j => (hcellj j).2.2.2.2.2.11176  -- strategy: pull the event back along the form-product bijection to a finite disjoint union1177  -- of products of factor events, whose product measures multiply the factor laws1178  let W : Fin L → Finset FactorType := fun j => (Finset.range (d j + 1)).biUnion1179    (fun n => (finite_types_of_degree n).toFinset) ∪ ((Dl j).map Prod.fst).toFinset1180  have hW : ∀ j τ, (reducedFormCell O (d j) (ν j) (g j) ∩1181      (if inf j = true then infinityBlockEvent O (d j) τ else typeEvent O (d j) τ)).Nonempty → τ ∈1182      W j := fun j τ h ↦ Finset.mem_union_left _ (type_mem_of_event_nonempty O _ _ _ _ τ h)1183  have hmeas := fun j τ ↦ (hlaw j τ).11184  set T := (Fintype.piFinset W).filter (fun τ : Fin L → FactorType => σ = ∑ j, τ j) with hT1185  have hbij := form_product_bijection O (Fin L) d ν g hgν hc μ hμ1186  have hpre := preimage_inter_pi_eq_biUnion _ _ _ (insertOne μ ⁻¹' affineTypeEvent O (∑ j, d j) σ)1187    hbij.mapsTo (fun j τ ↦ if inf j = true then infinityBlockEvent O (d j) τ else1188      typeEvent O (d j) τ) W hW σ (form_product_type_iff O L d ν g hc μ hμ inf hclass hone · · σ) T1189    fun τ ↦ by rw [hT, Finset.mem_filter, Fintype.mem_piFinset]1190  have hE : MeasurableSet (reducedFormCell O (∑ j, d j) μ (formProd d g) ∩1191      (insertOne μ ⁻¹' affineTypeEvent O (∑ j, d j) σ)) := by1192    choose c hcc using fun j ↦ (hcellj j).2.2.11193    refine measurableSet_inter_of_bijOn ?_ ?_ hbij1194      (hpre ▸ Finset.measurableSet_biUnion _ fun τ _ ↦ .univ_pi fun j ↦ hmeas j (τ j))1195    · convert (coordinate_cylinder_clopen O (IsLocalRing.maximalIdeal O) htop 1).2.2 (Fin L) d c1196        using 3 with j1197      rw [pow_one]; exact (hcellj j).2.1 (c j) (hcc j)1198    · exact continuousOn_of_congruence_compatible O O (IsLocalRing.maximalIdeal O) htop1199        (IsLocalRing.maximalIdeal O) htop (Fin L) d (∑ j, d j) _ _ fun L' a ha a' ha' h ↦1200        (form_product_maps_to_and_preserves O (Fin L) d ν g μ hμ a a' ha ha').2.2.2 L' h1201  refine ⟨hE, ?_⟩1202  rw [← cellMeasure_cell_inter hcellD.2.2.2.1, measure_eq_sum_prod_of_preimage _1203    (form_cells_measure_preserving O htop (Fin L) d ν g hgν hc μ hμ) _1204    (form_cell_product_measure O htop (Fin L) d ν g hgν).2.11205    (fun j ↦ cellMeasure_cell_inter (hcellj j).2.2.2.1) _ hmeas (fun j τ τ' x h1 h2 ↦ by1206      split_ifs at h1 h21207      exacts [polynomial_type_unique O _ _ _ h1.2 h2.2, polynomial_type_unique O _ _ _ h1 h2])1208    hE T hpre, Finset.sum_congr rfl fun τ _ ↦ Finset.prod_congr rfl fun j _ ↦ (hlaw j (τ j)).2]1209  exact sum_prod_densityValue_eq_lawProd Dl _ hnn W (fun _ ↦ Finset.subset_union_right) σ1210 1211end1212 1213section1214 1215variable {k : Type} [Field k]1216 1217private noncomputable def directionPoly : ClosedDirection k → Polynomial k1218  | none => 11219  | some φ => φ.val1220 1221open scoped Classical in1222private noncomputable def directionOfPoly (p : Polynomial k) : ClosedDirection k :=1223  if hp : p.Monic ∧ Irreducible p then some ⟨p, hp⟩ else none1224 1225private lemma directionOfPoly_directionPoly (φ : AffineDirection k) :1226    directionOfPoly (directionPoly (some φ)) = some φ := by1227  simp [directionOfPoly, directionPoly, φ.2]1228 1229private lemma directionPoly_directionOfPoly (p : Polynomial k) (hp : p.Monic ∧ Irreducible p) :1230    directionPoly (directionOfPoly p) = p := by1231  simp [directionOfPoly, directionPoly, hp]1232 1233open scoped Classical in1234private lemma toFinsupp_prod_directionPoly (S : Multiset (ClosedDirection k)) :1235    (Multiset.toFinsupp S).prod (fun a r => directionPoly a ^ r) = (S.map directionPoly).prod := by1236  induction S using Multiset.induction with1237  | empty => simp1238  | cons a S ih =>1239    rw [← Multiset.singleton_add, Multiset.toFinsupp_add, Multiset.toFinsupp_singleton,1240        Finsupp.prod_add_index' (by simp) (by intros; rw [pow_add]),1241      ih]1242    simp1243 1244open scoped Classical in1245private lemma toFinsupp_sum_directionDegree (S : Multiset (ClosedDirection k)) :1246    (Multiset.toFinsupp S).sum (fun a r => directionDegree k a * r) =1247      (S.map (directionDegree k)).sum := by1248  induction S using Multiset.induction with1249  | empty => simp1250  | cons a S ih =>1251    rw [← Multiset.singleton_add, Multiset.toFinsupp_add, Multiset.toFinsupp_singleton,1252        Finsupp.sum_add_index' (by simp) (by intros; rw [mul_add]),1253      ih]1254    simp1255 1256private lemma divisorAffinePolynomial_eq_prod (D : ExceptionalDivisor k) :1257    divisorAffinePolynomial k D = D.prod (fun a r => directionPoly a ^ r) := by1258  unfold divisorAffinePolynomial1259  congr 11260  funext a r1261  cases a <;> simp [directionPoly]1262 1263end1264 1265/-- Every monic polynomial of degree `n` over `k` is the affine polynomial of a unique affine1266divisor of degree `n`. -/1267theorem monic_polynomial_divisor (k : Type) [Field k] (n : ℕ) (G : Polynomial k) (hG : G.Monic)1268    (hn : G.natDegree = n) :1269    ∃! D : ExceptionalDivisor k, AffineDivisor k n D ∧ divisorAffinePolynomial k D = G := by1270  classical1271  set N := UniqueFactorizationMonoid.normalizedFactors G with hN1272  have hG0 : G ≠ 0 := hG.ne_zero1273  have hNmi : ∀ p ∈ N, p.Monic ∧ Irreducible p := fun p hp =>1274    ⟨by rw [← UniqueFactorizationMonoid.normalize_normalized_factor p hp]; exact1275        Polynomial.monic_normalize (UniqueFactorizationMonoid.ne_zero_of_mem_normalizedFactors hp),1276     UniqueFactorizationMonoid.irreducible_of_normalized_factor p hp⟩1277  have hNprod : N.prod = G := by1278    have := Polynomial.eq_of_monic_of_associated1279      (Polynomial.monic_multiset_prod_of_monic N id (fun p hp => (hNmi p hp).1)) hG1280    simp only [Multiset.map_id] at this1281    apply this1282    exact UniqueFactorizationMonoid.prod_normalizedFactors hG01283  have hNg : (N.map directionOfPoly).map directionPoly = N := by1284    rw [Multiset.map_map]1285    conv_rhs => rw [← Multiset.map_id N]1286    exact Multiset.map_congr rfl (fun p hp => directionPoly_directionOfPoly p (hNmi p hp))1287  refine ⟨Multiset.toFinsupp (N.map directionOfPoly), ⟨⟨?_, ?_⟩, ?_⟩, ?_⟩1288  · change Multiset.toFinsupp (N.map directionOfPoly) none = 01289    rw [Multiset.toFinsupp_apply, Multiset.count_eq_zero, Multiset.mem_map]1290    rintro ⟨p, hp, hgp⟩1291    simp [directionOfPoly, hNmi p hp] at hgp1292  · unfold exceptionalDegree1293    rw [toFinsupp_sum_directionDegree, Multiset.map_map, ← hn, ← hNprod,1294      Polynomial.natDegree_multiset_prod_of_monic _ (fun p hp => (hNmi p hp).1)]1295    congr 11296    exact Multiset.map_congr rfl (fun p hp => by simp [directionOfPoly, hNmi p hp, directionDegree])1297  · rw [divisorAffinePolynomial_eq_prod, toFinsupp_prod_directionPoly, hNg, hNprod]1298  · rintro D ⟨⟨hinf, hdeg⟩, hprod⟩1299    set S := Finsupp.toMultiset D with hS1300    have hDS : D = Multiset.toFinsupp S := (Multiset.toFinsupp_eq_iff.2 rfl).symm1301    have hnone : none ∉ S := by1302      rw [hS, Finsupp.mem_toMultiset]1303      simpa [Finsupp.mem_support_iff, infinityDirection] using hinf1304    have hSmi : ∀ p ∈ S.map directionPoly, p.Monic ∧ Irreducible p := by1305      intro p hp1306      obtain ⟨a, ha, rfl⟩ := Multiset.mem_map.1 hp1307      cases a with1308      | none => exact absurd ha hnone1309      | some φ => exact φ.21310    have hSprod : (S.map directionPoly).prod = G := by1311      rw [← hprod, divisorAffinePolynomial_eq_prod, hDS, toFinsupp_prod_directionPoly]1312    have hrel : Multiset.Rel Associated (S.map directionPoly) N := by1313      apply UniqueFactorizationMonoid.factors_unique (fun p hp => (hSmi p hp).2)1314        (fun p hp => UniqueFactorizationMonoid.irreducible_of_normalized_factor p hp)1315      rw [hSprod, hNprod]1316      exact Associated.refl G1317    have hEq : S.map directionPoly = N := by1318      rw [← Multiset.rel_eq]1319      refine hrel.mono ?_1320      intro a ha b hb hab1321      exact Polynomial.eq_of_monic_of_associated (hSmi a ha).1 (hNmi b hb).1 hab1322    rw [hDS, ← hEq, Multiset.map_map]1323    congr 11324    conv_lhs => rw [← Multiset.map_id S]1325    refine Multiset.map_congr rfl (fun a ha => ?_)1326    cases a with1327    | none => exact absurd ha hnone1328    | some φ => exact (directionOfPoly_directionPoly φ).symm1329 1330end SurfaceBlowup