Normal crossings from rational sections

Mathematical statement

Let $A\subset\mathbb P^1(\mathbb Q)$ be finite, and let $D_A$ be the divisor formed by the integral sections corresponding to its points. For primitive coordinates $a=[u_a:v_a]$ and $b=[u_b:v_b]$, put $\Delta(a,b)=u_av_b-u_bv_a$, up to the harmless sign of the chosen primitive representatives.

For a prime $p$, the divisor $(D_A)_{\mathbb Z_p}$ has normal crossings if and only if every closed point of $\mathbb P^1_{\mathbb F_p}$ lies on at most two labelled sections and every distinct pair meeting there satisfies

$$v_p\!\left(\Delta(a,b)\right)=1.$$

Lean code

`ShimizuYamaguchi26BranchedCoverings.rationalSectionPadicDivisor_isNormalCrossings_iff_specialFiber_conditions`

Published library source ↗Same source in NYLL ↗

theorem rationalSectionPadicDivisor_isNormalCrossings_iff_specialFiber_conditions
    (p : ℕ) [Fact p.Prime] (A : Finset (Projectivization ℚ (ℚ × ℚ))) :
    (rationalSectionPadicDivisor p A).IsNormalCrossings ↔
      (∀ y : ProjectiveLine (ZMod p),
        IsClosed ({y} : Set (ProjectiveLine (ZMod p))) →
          ({c : Projectivization ℚ (ℚ × ℚ) | c ∈ A ∧
            ProjSpace.map ℤ (ZMod p) 1 y ∈ rationalSectionSupport c} :
              Set (Projectivization ℚ (ℚ × ℚ))).ncard ≤ 2) ∧
      (∀ y : ProjectiveLine (ZMod p),
        IsClosed ({y} : Set (ProjectiveLine (ZMod p))) →
          ∀ a ∈ A, ∀ b ∈ A, a ≠ b →
            ProjSpace.map ℤ (ZMod p) 1 y ∈ rationalSectionSupport a →
            ProjSpace.map ℤ (ZMod p) 1 y ∈ rationalSectionSupport b →
              padicValInt p (rationalPointDelta a b) = 1)

In-scope Lean context

noncomputable section

open AlgebraicGeometry

namespace ShimizuYamaguchi26BranchedCoverings

Full declaration and proof

/-- The normal-crossings assertion of Lemma 2.3, stated on the actual
p-adic divisor and the closed points of the original prime special fibre. -/
theorem rationalSectionPadicDivisor_isNormalCrossings_iff_specialFiber_conditions
    (p : ℕ) [Fact p.Prime] (A : Finset (Projectivization ℚ (ℚ × ℚ))) :
    (rationalSectionPadicDivisor p A).IsNormalCrossings ↔
      (∀ y : ProjectiveLine (ZMod p),
        IsClosed ({y} : Set (ProjectiveLine (ZMod p))) →
          ({c : Projectivization ℚ (ℚ × ℚ) | c ∈ A ∧
            ProjSpace.map ℤ (ZMod p) 1 y ∈ rationalSectionSupport c} :
              Set (Projectivization ℚ (ℚ × ℚ))).ncard ≤ 2) ∧
      (∀ y : ProjectiveLine (ZMod p),
        IsClosed ({y} : Set (ProjectiveLine (ZMod p))) →
          ∀ a ∈ A, ∀ b ∈ A, a ≠ b →
            ProjSpace.map ℤ (ZMod p) 1 y ∈ rationalSectionSupport a →
            ProjSpace.map ℤ (ZMod p) 1 y ∈ rationalSectionSupport b →
              padicValInt p (rationalPointDelta a b) = 1) := by
  classical
  rw [rationalSectionPadicDivisor_isNormalCrossings_iff_isStrictNormalCrossings]
  constructor
  · intro hNC
    obtain ⟨hcard, hval⟩ :=
      (rationalSectionPadicDivisor_isStrictNormalCrossings_iff p A).mp hNC
    constructor
    · intro y _hy
      rw [← Finset.coe_filter, Set.ncard_coe_finset]
      let S := A.filter (fun c =>
        ProjSpace.map ℤ (ZMod p) 1 y ∈ rationalSectionSupport c)
      change S.card ≤ 2
      by_cases hS : S.Nonempty
      · obtain ⟨b, hbS⟩ := hS
        obtain ⟨hb, hyb⟩ := Finset.mem_filter.mp hbS
        apply (Finset.card_le_card (show S ⊆
          A.filter (fun c => (p : ℤ) ∣ rationalPointDelta c b) from ?_)).trans (hcard b hb)
        intro c hcS
        obtain ⟨hc, hyc⟩ := Finset.mem_filter.mp hcS
        exact Finset.mem_filter.mpr ⟨hc,
          (specialFiber_intersection_nonempty_iff p c b).mp ⟨y, hyc, hyb⟩⟩
      · rw [Finset.not_nonempty_iff_eq_empty.mp hS, Finset.card_empty]
        exact Nat.zero_le 2
    · intro y _hy a ha b hb hab hya hyb
      exact hval a ha b hb hab
        ((specialFiber_intersection_nonempty_iff p a b).mp ⟨y, hya, hyb⟩)
  · rintro ⟨hcard, hval⟩
    apply (rationalSectionPadicDivisor_isStrictNormalCrossings_iff_integer p A).mpr
    exact rationalSectionFamily_isStrictNormalCrossingsAt_of_specialFiber_conditions
      p A hcard hval

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.