NYLL
Module

Theorem1Dot3BoundaryInvariance.lean

Nyll.Yamaguchi26SolvableCoverings.Theorem1Dot3BoundaryInvariance
2 declarations indexed from sourceView source ↗

Module documentation

Proposition 1.3: boundary invariance

For a horizontal effective Cartier divisor on a connected locally Noetherian scheme regular along its support, assume that every component contains a normal crossings point in every prime residue characteristic. The complement is connected, and its inclusion induces an isomorphism on etale fundamental groups.

The isomorphism is required to agree with the homomorphism induced by the inclusion. The proof applies Lemma 1.2 to every prime divisor of each finite inertia group's order, then uses the kernel description in Lemma 1.1.

Source: Yamaguchi, arXiv:2610.02948v1, Proposition 1.3.

For a fixed finite Galois cover, only prime divisors of its deck group's order are needed. This refinement supplies the finite-inertia argument in Theorem 3.1 of Shimizu and Yamaguchi, On branched coverings of the projective line over the integers, arXiv:2608.15057v1.

Imports11
Imported by1

Declarations

theorem

boundaryUnramified_of_normalCrossingPoints_at_card_primes

L51 ↗
Yamaguchi26SolvableCoverings.boundaryUnramified_of_normalCrossingPoints_at_card_primes
Documentation

A finite Galois cover has trivial boundary stabilizers if each boundary component has a normal-crossings point in every prime residue characteristic dividing the order of its deck group.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [ConnectedSpace X] [IsLocallyNoetherian X]
Lean source · full declaration
theorem boundaryUnramified_of_normalCrossingPoints_at_card_primes
    (D : X.EffectiveCartierDivisor) (hhor : IsHorizontal D)
    (hreg : D.IsAmbientRegularAlongSupport) :
    let : ConnectedSpace D.1.supportComplement := boundaryComplement_connectedSpace D hreg
    ∀ (W : FiniteEtale D.1.supportComplement) (_hW : IsGalois W),
      (∀ p : ℕ, p.Prime → p ∣ Nat.card (Aut W) →
        D.HasNormalCrossingPointOfResidueCharacteristicOnEachComponent p) →
      IsBoundaryUnramified D W := by
  intro hConnected W hW hnc E z hz
  have hcard : Nat.card (finiteCoverInertia D W E z) = 1 := by
    apply Nat.eq_one_iff_not_exists_prime_dvd.mpr
    intro p hp hpdvd
    have hpW : p ∣ Nat.card (Aut W) :=
      hpdvd.trans (finiteCoverInertia D W E z).card_subgroup_dvd_card
    exact finite_inertia_control D hhor hreg E p hp
      (hnc p hp hpW E.val E.property) W hW z hz hpdvd
  have : Subsingleton (finiteCoverInertia D W E z) :=
    (Nat.card_eq_one_iff_unique.mp hcard).1
  apply le_antisymm ?_ bot_le
  intro σ hσ
  apply Subgroup.mem_bot.mpr
  exact congrArg Subtype.val
    (Subsingleton.elim (⟨σ, hσ⟩ : finiteCoverInertia D W E z) 1)
theorem

boundary_invariance_1_3

L78 ↗
Yamaguchi26SolvableCoverings.boundary_invariance_1_3
Documentation

命題 1.3。 水平境界の各成分に全ての素数についてその剰余標数の正規交差点があれば、 境界の補集合は連結であり、包含が étale 基本群の位相群同型を誘導する。

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [ConnectedSpace X] [IsLocallyNoetherian X]
Lean source · statement
theorem boundary_invariance_1_3
    (D : X.EffectiveCartierDivisor) (hhor : IsHorizontal D)
    (hreg : D.IsAmbientRegularAlongSupport)
    (hnc : ∀ p : ℕ, p.Prime →
      D.HasNormalCrossingPointOfResidueCharacteristicOnEachComponent p) :
    ConnectedSpace D.1.supportComplement ∧
      ∀ (Ω : Type) [Field Ω] [IsSepClosed Ω]
        (point : Spec (CommRingCat.of Ω) ⟶ D.1.supportComplement),
        ∃ e : π₁ᵉᵗ(point) ≃ₜ* π₁ᵉᵗ(point ≫ D.1.supportComplement.ι),
          ∀ g : π₁ᵉᵗ(point), e g = fundamentalGroupHom D.1.supportComplement.ι point g

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.