Module

BoundaryStrictExtension.lean

Nyll.Yamaguchi26SolvableCoverings.Geometry.BoundaryStrictExtension

2 declarations indexed from sourceView source ↗

Module documentation

Extending covers killed by strict local inertia

A finite Galois quotient killing the transported strict inertia generators has trivial action on every strict generic fiber. The actual strict-local normalization criterion supplies etaleness at each component stalk. Purity and affine spreading then extend the original cover over the ambient scheme. The finite Galois quotient criterion identifies the closed normal inertia subgroup with the kernel of the inclusion-induced fundamental-group map.

Imports3

Imported by2

theorem

exists_finiteEtale_extension_of_strictGenerators_subset_kernel

L34 ↗

Yamaguchi26SolvableCoverings.exists_finiteEtale_extension_of_strictGenerators_subset_kernel

Documentation

A Galois cover killed by all actual strict inertia generators extends across the regular Cartier boundary.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups.StrictHenselian
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]

Lean source · statement

theorem exists_finiteEtale_extension_of_strictGenerators_subset_kernel
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement)
    (W : FiniteEtale D.1.supportComplement) [IsGalois W]
    (w : (fiber point).obj W)
    (hs : boundaryStrictInertiaGenerators D hreg point ⊆
      (galoisObjectQuotientMonoidHom (fiber point) π₁ᵉᵗ(point) W w).ker) :
    ∃ V : FiniteEtale X,
      Nonempty ((FiniteEtale.pullback D.1.supportComplement.ι).obj V ≅ W)

theorem

kernel_le_boundaryStrictInertiaClosure

L61 ↗

Yamaguchi26SolvableCoverings.kernel_le_boundaryStrictInertiaClosure