A perfect boundary kernel

Mathematical statement

Let $X$ be connected and locally Noetherian, and let $D$ be a horizontal effective Cartier divisor. Assume condition $(\dagger)$: $X$ is regular along $D$; each prime component contains a characteristic-$2$ normal-crossings point of $D$; and each reduced boundary component has geometrically integral generic fiber over $\mathbb Q$ after every connected finite étale cover of $X$. Put $U=X\setminus D$. The theorem proves that $U$ is connected. For a geometric point $\xi$ of $U$, let

$$f:\pi_1^{\mathrm{\acute et}}(U,\xi)\longrightarrow\pi_1^{\mathrm{\acute et}}(X,\xi),\qquad K=\ker(f).$$

Then $K=\overline{[K,K]}$, with closure taken in $K$, and the inclusion-induced map gives

$$\pi_1^{\mathrm{\acute et}}(U,\xi)^{\mathrm{solv}}\xrightarrow{\sim}\pi_1^{\mathrm{\acute et}}(X,\xi)^{\mathrm{solv}}.$$

Lean code

`Yamaguchi26SolvableCoverings.perfect_kernel_2_5`

Published library source ↗Same source in NYLL ↗

theorem perfect_kernel_2_5
    (D : X.EffectiveCartierDivisor) (hhor : IsHorizontal D)
    (hD : BoundaryCondition D) :
    ConnectedSpace D.1.supportComplement ∧
      ∀ (Ω : Type) [Field Ω] [IsSepClosed Ω]
        (point : Spec (CommRingCat.of Ω) ⟶ D.1.supportComplement),
        let f : π₁ᵉᵗ(point) →ₜ* π₁ᵉᵗ(point ≫ D.1.supportComplement.ι) :=
          fundamentalGroupHom D.1.supportComplement.ι point
        (commutator f.toMonoidHom.ker).topologicalClosure = ⊤ ∧
          ∃ e : Prosolvable π₁ᵉᵗ(point) ≃ₜ* Prosolvable π₁ᵉᵗ(point ≫ D.1.supportComplement.ι),
            ∀ g : π₁ᵉᵗ(point), e (QuotientGroup.mk g) = QuotientGroup.mk (f g) := by
  obtain ⟨hU, hboundary⟩ := boundary_quotient_1_1 D hD.1
  refine ⟨hU, ?_⟩
  let : ConnectedSpace D.1.supportComplement := hU
  intro Ω _ _ point
  let f : π₁ᵉᵗ(point) →ₜ* π₁ᵉᵗ(point ≫ D.1.supportComplement.ι) :=
    fundamentalGroupHom D.1.supportComplement.ι point
  have hf : Function.Surjective f := (hboundary Ω point).1
  have hAb : OpenNormalAbelianizationInjective f :=
    openNormalAbelianizationInjective_of_finiteDiscreteAbelianMapsKillKernel
      f hf (boundary_openNormalFiniteDiscreteAbelianMapsKillKernel D hhor hD point)
  refine ⟨kernel_topologicallyPerfect_of_openNormalAbelianizationInjective f hf hAb, ?_⟩
  refine ⟨prosolvableResidualQuotientContinuousMulEquiv f hf hAb, ?_⟩
  intro g
  rfl

In-scope Lean context

noncomputable section

open AlgebraicGeometry CategoryTheory

open AlgebraicGeometry.FiniteEtale

open ProCGroups.FiniteStepSolvableQuotients

namespace Yamaguchi26SolvableCoverings

variable {X : Scheme.{0}} [ConnectedSpace X] [IsLocallyNoetherian X]

Full declaration and proof

/-- 定理 2.5：条件 `(†)` の下で、補集合は連結、包含が誘導する
基本群の準同型の核は位相的完全であり、その最大 prosolvable 商への誘導写像は同型である。 -/
theorem perfect_kernel_2_5
    (D : X.EffectiveCartierDivisor) (hhor : IsHorizontal D)
    (hD : BoundaryCondition D) :
    ConnectedSpace D.1.supportComplement ∧
      ∀ (Ω : Type) [Field Ω] [IsSepClosed Ω]
        (point : Spec (CommRingCat.of Ω) ⟶ D.1.supportComplement),
        let f : π₁ᵉᵗ(point) →ₜ* π₁ᵉᵗ(point ≫ D.1.supportComplement.ι) :=
          fundamentalGroupHom D.1.supportComplement.ι point
        (commutator f.toMonoidHom.ker).topologicalClosure = ⊤ ∧
          ∃ e : Prosolvable π₁ᵉᵗ(point) ≃ₜ* Prosolvable π₁ᵉᵗ(point ≫ D.1.supportComplement.ι),
            ∀ g : π₁ᵉᵗ(point), e (QuotientGroup.mk g) = QuotientGroup.mk (f g) := by
  obtain ⟨hU, hboundary⟩ := boundary_quotient_1_1 D hD.1
  refine ⟨hU, ?_⟩
  let : ConnectedSpace D.1.supportComplement := hU
  intro Ω _ _ point
  let f : π₁ᵉᵗ(point) →ₜ* π₁ᵉᵗ(point ≫ D.1.supportComplement.ι) :=
    fundamentalGroupHom D.1.supportComplement.ι point
  have hf : Function.Surjective f := (hboundary Ω point).1
  have hAb : OpenNormalAbelianizationInjective f :=
    openNormalAbelianizationInjective_of_finiteDiscreteAbelianMapsKillKernel
      f hf (boundary_openNormalFiniteDiscreteAbelianMapsKillKernel D hhor hD point)
  refine ⟨kernel_topologicallyPerfect_of_openNormalAbelianizationInjective f hf hAb, ?_⟩
  refine ⟨prosolvableResidualQuotientContinuousMulEquiv f hf hAb, ?_⟩
  intro g
  rfl

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

Naganori Yamaguchi. Extension of solvable coverings across horizontal divisors over the integers. 2026. arXiv:2610.02948v1, submitted October 2, 2026.