Intersection multiplicity as a determinant valuation

Mathematical statement

Let $a\ne b$ be rational points of $\mathbb P^1_{\mathbb Q}$, with associated sections $D_a,D_b\subset\mathbb P^1_{\mathbb Z}$. Let $y$ be a point of the fiber over a prime $p$ lying on $D_b$, and let $x$ be its image in $\mathbb P^1_{\mathbb Z}$. Then

$$\operatorname{length}_{\mathcal O_x}\!\left(\mathcal O_x/(I_a+I_b)_x\right)=v_p\!\left(\Delta(a,b)\right).$$

Lean code

`ShimizuYamaguchi26BranchedCoverings.rationalSectionIntersection_length_at_specialFiber_point`

Published library source ↗Same source in NYLL ↗

theorem rationalSectionIntersection_length_at_specialFiber_point
    (p : ℕ) [Fact p.Prime] (a b : Projectivization ℚ (ℚ × ℚ)) (hab : a ≠ b)
    (y : ProjectiveLine (ZMod p))
    (hy : ProjSpace.map ℤ (ZMod p) 1 y ∈ rationalSectionSupport b) :
    let x : ProjectiveLine ℤ := ProjSpace.map ℤ (ZMod p) 1 y
    Module.length ((ProjectiveLine ℤ).presheaf.stalk x)
      ((ProjectiveLine ℤ).presheaf.stalk x ⧸ rationalSectionIntersectionIdeal a b x) =
        (padicValInt p (rationalPointDelta a b) : ℕ∞) := by
  intro x
  have hpoint : x = rationalSection b (integerPrimePoint p) :=
    specialFiber_image_eq_rationalSection_primePoint p b y hy
  have hlength := congrArg (fun z : ProjectiveLine ℤ =>
    Module.length ((ProjectiveLine ℤ).presheaf.stalk z)
      ((ProjectiveLine ℤ).presheaf.stalk z ⧸ rationalSectionIntersectionIdeal a b z)) hpoint
  exact hlength.trans (rationalSectionIntersection_length p a b hab)

In-scope Lean context

noncomputable section

open AlgebraicGeometry CategoryTheory

namespace ShimizuYamaguchi26BranchedCoverings

Full declaration and proof

/-- The original local intersection length at the image of any
special-fibre point on the second section is the paper's determinant
valuation. A common point of the two sections is a special case; no choice
of coordinates or a preassigned equality of points is required. -/
theorem rationalSectionIntersection_length_at_specialFiber_point
    (p : ℕ) [Fact p.Prime] (a b : Projectivization ℚ (ℚ × ℚ)) (hab : a ≠ b)
    (y : ProjectiveLine (ZMod p))
    (hy : ProjSpace.map ℤ (ZMod p) 1 y ∈ rationalSectionSupport b) :
    let x : ProjectiveLine ℤ := ProjSpace.map ℤ (ZMod p) 1 y
    Module.length ((ProjectiveLine ℤ).presheaf.stalk x)
      ((ProjectiveLine ℤ).presheaf.stalk x ⧸ rationalSectionIntersectionIdeal a b x) =
        (padicValInt p (rationalPointDelta a b) : ℕ∞) := by
  intro x
  have hpoint : x = rationalSection b (integerPrimePoint p) :=
    specialFiber_image_eq_rationalSection_primePoint p b y hy
  have hlength := congrArg (fun z : ProjectiveLine ℤ =>
    Module.length ((ProjectiveLine ℤ).presheaf.stalk z)
      ((ProjectiveLine ℤ).presheaf.stalk z ⧸ rationalSectionIntersectionIdeal a b z)) hpoint
  exact hlength.trans (rationalSectionIntersection_length p a b hab)

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

Ryoji Shimizu and Naganori Yamaguchi. On branched coverings of the projective line over the integers. 2026. arXiv:2608.15057v1, submitted August 15, 2026.