Module

BoundaryExtension.lean

Nyll.Yamaguchi26SolvableCoverings.Geometry.BoundaryExtension

2 declarations indexed from sourceView source ↗

Module documentation

Boundary inertia of finite etale extensions

A cover which extends over the ambient scheme has trivial geometric-point inertia at every boundary component. This proves one inclusion in the kernel formula of Lemma 1.1 without requiring ambient normality or integrality.

Imports4

Imported by2

theorem

isBoundaryUnramified_of_extension

L31 ↗

Yamaguchi26SolvableCoverings.isBoundaryUnramified_of_extension

Documentation

An actual finite etale extension kills every normalized-point boundary stabilizer. Boundary regularity supplies full faithfulness of restriction.

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 isBoundaryUnramified_of_extension
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement)
    (W : FiniteEtale D.1.supportComplement) [IsConnected W]
    (hW : ∃ V : FiniteEtale X,
      Nonempty ((FiniteEtale.pullback D.1.supportComplement.ι).obj V ≅ W)) :
    IsBoundaryUnramified D W

theorem

boundaryUnramifiedKernelIntersection_le_kernel

L50 ↗

Yamaguchi26SolvableCoverings.boundaryUnramifiedKernelIntersection_le_kernel