At least seven sections force a quotient

Mathematical statement

Let $A\subset\mathbb P^1(\mathbb Q)$ be finite with $|A|\ge7$, and form the open complement $U_A\subset\mathbb P^1_{\mathbb Z}$ of the corresponding integral sections. For every geometric point $\xi$ of $U_A$,

$$\exists\,\phi:\pi_1^{\mathrm{\acute et}}(U_A,\xi)\twoheadrightarrow\mathbb Z/2\mathbb Z\quad\text{continuous}.$$

Lean code

`ShimizuYamaguchi26BranchedCoverings.large_boundary_quotient_2_7`

Published library source ↗Same source in NYLL ↗

theorem large_boundary_quotient_2_7
    (A : Finset (Projectivization ℚ (ℚ × ℚ))) (hcard : 7 ≤ A.card)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶
      (A.inf fun a => Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        (linearSectionEquation (rationalPointNumerator a)
          (rationalPointDenominator a))).toScheme) :
    ∃ φ : π₁ᵉᵗ(ξ) →ₜ* Multiplicative (ZMod 2), Function.Surjective φ := by
  classical
  have hsize : 6 < Fintype.card ↥A := by
    rw [Fintype.card_coe]
    exact lt_of_lt_of_le (by decide : 6 < 7) hcard
  obtain ⟨a, b, hab, hfour⟩ :=
    exists_four_dvd_coordinateDeterminant_of_six_lt_card
      (ι := ↥A) (fun a => rationalPointNumerator a.val)
      (fun a => rationalPointDenominator a.val)
      (fun a => rationalPointCoordinates_isCoprime a.val) hsize
  have hne : a.val ≠ b.val := fun h => hab (Subtype.ext h)
  exact exists_surjective_cyclicTwo_of_four_dvd_delta_in_boundary A
    a.val b.val a.property b.property hne
    ((rationalPointDelta_dvd_iff 4 a.val b.val).mpr hfour) ξ

In-scope Lean context

noncomputable section

open AlgebraicGeometry

namespace ShimizuYamaguchi26BranchedCoverings

attribute [local instance] MvPolynomial.gradedAlgebra

Full declaration and proof

/-- Corollary 2.7, large-boundary case: the complement of at least seven
rational sections has a continuous cyclic quotient of order two at every
geometric base point. The open is constructed as the finite intersection
of the complements of the actual section equations. -/
theorem large_boundary_quotient_2_7
    (A : Finset (Projectivization ℚ (ℚ × ℚ))) (hcard : 7 ≤ A.card)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶
      (A.inf fun a => Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        (linearSectionEquation (rationalPointNumerator a)
          (rationalPointDenominator a))).toScheme) :
    ∃ φ : π₁ᵉᵗ(ξ) →ₜ* Multiplicative (ZMod 2), Function.Surjective φ := by
  classical
  have hsize : 6 < Fintype.card ↥A := by
    rw [Fintype.card_coe]
    exact lt_of_lt_of_le (by decide : 6 < 7) hcard
  obtain ⟨a, b, hab, hfour⟩ :=
    exists_four_dvd_coordinateDeterminant_of_six_lt_card
      (ι := ↥A) (fun a => rationalPointNumerator a.val)
      (fun a => rationalPointDenominator a.val)
      (fun a => rationalPointCoordinates_isCoprime a.val) hsize
  have hne : a.val ≠ b.val := fun h => hab (Subtype.ext h)
  exact exists_surjective_cyclicTwo_of_four_dvd_delta_in_boundary A
    a.val b.val a.property b.property hne
    ((rationalPointDelta_dvd_iff 4 a.val b.val).mpr hfour) ξ

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.