Closed points and divisors on the exceptional line

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.Basic7 8/-!9# Closed points and divisors on the exceptional line10 11For a field `k`, the closed points of the exceptional line `ℙ¹_k` (monic irreducible polynomials12plus the point at infinity), effective divisors on it with their degree and affine polynomial,13the boundary directions of a state and the divisors with a given tangent pattern. These are14elementary definitions, kept apart from the blow-up charts so that counting divisors does not15depend on the chart constructions.16 17## Main results18 19* `SurfaceBlowup.count_normalizedFactors_divisorAffinePolynomial`: multiplicities in the affine20  polynomial of a divisor.21 22Provenance: `Def_SurfaceBlowupV2_{ClosedDirections, DivisorPatterns}`;23`Thm_SurfaceBlowupV2_{count_normalizedFactors_divisorAffinePolynomial}` (moved from24`Blowup/Charts.lean`).25-/26 27noncomputable section28 29namespace SurfaceBlowup30 31/-! ### Closed points and divisors on the exceptional line -/32 33section34variable (k : Type) [Field k]35/-- Affine closed points of the exceptional line over `k`: monic irreducible polynomials. -/36abbrev AffineDirection := {phi : Polynomial k // phi.Monic ∧ Irreducible phi}37/-- Closed points of the exceptional line `ℙ¹_k`: affine points plus the point at infinity. -/38abbrev ClosedDirection := Option (AffineDirection k)39/-- The residue degree of a closed point of `ℙ¹_k` (`1` at infinity). -/40def directionDegree : ClosedDirection k → ℕ41  | none => 142  | some phi => phi.val.natDegree43/-- The point at infinity of the exceptional line. -/44def infinityDirection : ClosedDirection k := none45/-- The affine point `Z = 0` of the exceptional line. -/46def zeroDirection : ClosedDirection k :=47  some ⟨Polynomial.X, Polynomial.monic_X, Polynomial.irreducible_X⟩48/-- Effective divisors on the exceptional line `ℙ¹_k`. -/49abbrev ExceptionalDivisor := ClosedDirection k →₀ ℕ50/-- The degree `Σ deg(P)·D(P)` of an effective divisor on `ℙ¹_k`. -/51def exceptionalDegree (D : ExceptionalDivisor k) : ℕ :=52  D.sum fun P r => directionDegree k P * r53/-- The monic polynomial `Π φ^{D(φ)}` over the affine points of a divisor `D`. -/54def divisorAffinePolynomial (D : ExceptionalDivisor k) : Polynomial k :=55  D.prod fun P r => match P with | none => 1 | some phi => phi.val ^ r56/-- The nonzero dehomogenized form `H` of degree `≤ d` has divisor `D` on `ℙ¹_k`57(its affine part is `divisorAffinePolynomial D`, the multiplicity at infinity is `d − deg H`). -/58def HasHomogeneousDivisor (d : ℕ) (H : Polynomial k) (D : ExceptionalDivisor k) : Prop :=59  H ≠ 0 ∧ H.natDegree ≤ d ∧ D none = d - H.natDegree ∧60    H = Polynomial.C H.leadingCoeff * divisorAffinePolynomial k D61end62 63/-- The affine direction `Z`. -/64def zeroAffine (k : Type) [Field k] : AffineDirection k :=65  ⟨Polynomial.X, Polynomial.monic_X, Polynomial.irreducible_X⟩66 67/-! ### Divisor patterns -/68 69section70variable (k : Type) [Field k]71/-- The boundary points of the exceptional line: the old t-boundary is the direction at infinity;72at a crossing the old x-boundary is the direction Z = 0 as well (N184: on the t-chart z = x/t,73t = 0 is infinity and x = 0 is zeroDirection). -/74def boundaryDirections (s : State) : Set (ClosedDirection k) :=75  match s with76  | .single _ _ => {infinityDirection k}77  | .crossing _ _ _ _ => {infinityDirection k, zeroDirection k}78/-- `HasPattern k s D P`: the effective divisor D on the exceptional line has degree P.d,79multiplicity P.rt at the t-boundary (infinity), multiplicity P.rx at the x-boundary (only at a80crossing), and for every (δ, r) exactly P.other (δ−1, r−1) nonboundary closed points of degree δ81and multiplicity r. -/82def HasPattern (s : State) (D : ExceptionalDivisor k) (P : TangentPattern s.degree) : Prop :=83  exceptionalDegree k D = P.d.val ∧ D (infinityDirection k) = P.rt.val ∧84  (match s with85   | .single _ _ => True86   | .crossing _ _ _ _ => D (zeroDirection k) = P.rx.val) ∧87  ∀ ij : Fin s.degree × Fin s.degree,88    Nat.card {Q : ClosedDirection k // Q ∉ boundaryDirections k s ∧89      directionDegree k Q = ij.1.val + 1 ∧ D Q = ij.2.val + 1} = (P.other ij).val90/-- The divisors of the pattern P, as a type. -/91abbrev patternDivisors (s : State) (P : TangentPattern s.degree) : Type :=92  {D : ExceptionalDivisor k // HasPattern k s D P}93end94 95/-! ### Support of a divisor -/96 97section98variable {k : Type} [Field k]99/-- The closed points of the exceptional line carrying positive multiplicity in `Dv` (N184). -/100def divisorSupport (Dv : ExceptionalDivisor k) : Type := {Q : ClosedDirection k // 0 < Dv Q}101/-- The support of an effective divisor is finite. -/102instance divisorSupport_finite (Dv : ExceptionalDivisor k) : Finite (divisorSupport Dv) :=103  Finite.of_injective (fun Q : divisorSupport Dv =>104      (⟨Q.val, Finsupp.mem_support_iff.mpr (Nat.pos_iff_ne_zero.mp Q.property)⟩ : Dv.support))105    (fun _ _ h => by106      have h' := congrArg Subtype.val h107      exact Subtype.ext h')108end109 110/-! ### Exceptional divisors -/111 112open scoped Classical in113/-- The multiplicity of an affine direction `φ` in `c · divisorAffinePolynomial Dv` is `Dv φ`;114in particular `φ` divides it iff `Dv φ > 0`. -/115theorem count_normalizedFactors_divisorAffinePolynomial (k : Type) [Field k]116    (Dv : ExceptionalDivisor k) (lc : k) (hlc : lc ≠ 0) (φ : AffineDirection k) :117    Multiset.count φ.val (UniqueFactorizationMonoid.normalizedFactors118        (Polynomial.C lc * divisorAffinePolynomial k Dv)) = Dv (some φ) ∧119        (φ.val ∣ divisorAffinePolynomial k Dv ↔ 0 < Dv (some φ)) := by120  set g : ClosedDirection k → ℕ → Polynomial k :=121    fun P r => match P with | none => 1 | some phi => phi.val ^ r with hg122  have hg0 : ∀ P, g P 0 = 1 := by intro P; cases P <;> simp [hg]123  set r := Dv (some φ) with hr124  set Q := (Dv.erase (some φ)).prod g with hQ125  have hG : divisorAffinePolynomial k Dv = φ.val ^ r * Q :=126    (Finsupp.mul_prod_erase' Dv (some φ) g hg0).symm127  have hirr : Irreducible φ.val := φ.2.2128  have hprime : Prime φ.val := hirr.prime129  have hnQ : ¬ φ.val ∣ Q := by130    intro h131    rw [hQ, Finsupp.prod, hprime.dvd_finsetProd_iff] at h132    obtain ⟨P, hP, hd⟩ := h133    have hPne : P ≠ some φ := by rintro rfl; simp at hP134    cases P with135    | none => exact hirr.not_isUnit (isUnit_of_dvd_unit hd isUnit_one)136    | some ψ =>137      exact hPne (congrArg some (Subtype.ext (Polynomial.eq_of_monic_of_associated φ.2.1 ψ.2.1138        (hirr.associated_of_dvd ψ.2.2 (hprime.dvd_of_dvd_pow hd)))).symm)139  refine ⟨?_, ?_⟩140  · apply UniqueFactorizationMonoid.count_normalizedFactors_eq hirr (φ.2.1.normalize_eq_self)141    · rw [hG]; exact Dvd.intro (Polynomial.C lc * Q) (by ring)142    · rintro ⟨c, hc⟩143      rw [hG, pow_succ, mul_assoc] at hc144      have h3 : φ.val ∣ Polynomial.C lc * Q :=145        ⟨c, mul_left_cancel₀ (pow_ne_zero r hirr.ne_zero) (by rw [← hc]; ring)⟩146      rcases hprime.dvd_or_dvd h3 with h | h147      · exact hirr.not_isUnit (isUnit_of_dvd_unit h (Polynomial.isUnit_C.mpr148          (isUnit_iff_ne_zero.mpr hlc)))149      · exact hnQ h150  · refine ⟨fun h ↦ Nat.pos_of_ne_zero fun h0 ↦ hnQ ?_,151      fun h ↦ hG ▸ dvd_mul_of_dvd_left (dvd_pow_self _ h.ne') _⟩152    rwa [hG, h0, pow_zero, one_mul] at h153 154end SurfaceBlowup