definition · Research papers
The arithmetic boundary condition
A local condition at characteristic two is combined with a geometric-integrality condition that survives every connected finite étale cover.
Persistence after finite étale base change lets the same abelian argument be applied to open subgroups of the fundamental group. This is the mechanism for reaching conclusions about all solvable coverings. Definition 2.2 of Yamaguchi's 2026 paper introduces the condition after an abelian invariance result and explains why geometric integrality of the original boundary alone does not suffice.
Mathematical statement
Let $X$ be connected and locally Noetherian, and let $D$ be a horizontal effective Cartier divisor: each prime component dominates $\operatorname{Spec}\mathbb Z$. Condition $(\dagger)$ requires all three of the following.
The scheme $X$ is regular along $D$. Every prime component of $D$ contains a residue-characteristic-$2$ point where $D$ has normal crossings. After every connected finite étale cover $X'\to X$, each reduced prime component of the pulled-back boundary has geometrically integral generic fiber over $\mathbb Q$.
Lean code
Yamaguchi26SolvableCoverings.BoundaryCondition
Published library source ↗Same source in NYLL ↗
def BoundaryCondition {X : Scheme.{0}} (D : X.EffectiveCartierDivisor) : Prop
In-scope Lean context
open AlgebraicGeometry
namespace Yamaguchi26SolvableCoverings
Full declaration and proof
/-- Definition 2.2: 支持上の正則性、各成分の標数 `2`
の normal-crossings 点、および全連結有限 étale 被覆後の一般成分の幾何的整性。 -/
def BoundaryCondition {X : Scheme.{0}} (D : X.EffectiveCartierDivisor) : Prop :=
D.IsAmbientRegularAlongSupport ∧
D.HasNormalCrossingPointOfResidueCharacteristicOnEachComponent 2 ∧
HasGeometricallyIntegralGenericComponentsAfterCovers D
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)
Related Lean sources
Published source: a1a5a03f.
← All selected results in Research papers