A quadratic quotient from failure at 2

Mathematical statement

For finite $A\subset\mathbb P^1(\mathbb Q)$, put $U_A=\mathbb P^1_{\mathbb Z}\setminus D_A$. If $(D_A)_{\mathbb Z_2}$ is not a normal-crossings divisor, then for every geometric point $\xi$ of $U_A$ there is a continuous surjection

$$\pi_1^{\mathrm{\acute et}}(U_A,\xi)\twoheadrightarrow\mathbb Z/2\mathbb Z.$$

Lean code

`ShimizuYamaguchi26BranchedCoverings.exists_surjective_cyclicTwo_of_not_normalCrossings_at_two`

Published library source ↗Same source in NYLL ↗

theorem exists_surjective_cyclicTwo_of_not_normalCrossings_at_two
    (A : Finset (Projectivization ℚ (ℚ × ℚ)))
    (hbad : ¬ (rationalSectionPadicDivisor 2 A).IsNormalCrossings)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶
      (∏ a ∈ A, (rationalSection a).ker).supportComplement.toScheme) :
    ∃ φ : π₁ᵉᵗ(ξ) →ₜ* Multiplicative (ZMod 2), Function.Surjective φ

In-scope Lean context

noncomputable section

open AlgebraicGeometry

open scoped BigOperators

namespace ShimizuYamaguchi26BranchedCoverings

Full declaration and proof

/-- Proposition 2.5: if the actual rational-section divisor is not normal
crossings after base change to the 2-adic integers, its original integral
complement admits a continuous quotient of order two, at every geometric
base point. -/
theorem exists_surjective_cyclicTwo_of_not_normalCrossings_at_two
    (A : Finset (Projectivization ℚ (ℚ × ℚ)))
    (hbad : ¬ (rationalSectionPadicDivisor 2 A).IsNormalCrossings)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶
      (∏ a ∈ A, (rationalSection a).ker).supportComplement.toScheme) :
    ∃ φ : π₁ᵉᵗ(ξ) →ₜ* Multiplicative (ZMod 2), Function.Surjective φ := by
  apply exists_surjective_cyclicTwo_of_not_strictNormalCrossings_over_two A ?_ ξ
  intro hstrict
  have hpadic : (rationalSectionPadicDivisor 2 A).IsStrictNormalCrossings :=
    (rationalSectionPadicDivisor_isStrictNormalCrossings_iff_integer 2 A).mpr hstrict
  exact hbad hpadic.isNormalCrossings

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.