NYLL
Module

BoundaryUnramifiedExtension.lean

Nyll.Yamaguchi26SolvableCoverings.Geometry.BoundaryUnramifiedExtension
3 declarations indexed from sourceView source ↗

Module documentation

Extending covers with trivial boundary stabilizers

Purity supplies finite etaleness over every boundary stalk. Affine spreading then makes the actual relative normalization finite etale globally. Its restriction is the original cover, so the finite-cover kernel criterion supplies the remaining inclusion in the boundary quotient formula.

Imports4
Imported by2

Declarations

theorem

exists_finiteEtale_extension_of_componentStalks

L33 ↗
Yamaguchi26SolvableCoverings.exists_finiteEtale_extension_of_componentStalks
Documentation

A Galois cover whose normalization is etale at every component stalk extends across the regular Cartier boundary as the actual relative normalization.

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
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]
Lean source · statement
theorem exists_finiteEtale_extension_of_componentStalks
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    (W : FiniteEtale D.1.supportComplement) (hW : IsGalois W)
    (hgeneric : ∀ E : Component D,
      Etale (CategoryTheory.Limits.pullback.snd
        (W.hom ≫ D.1.supportComplement.ι).fromNormalization
        (X.fromSpecStalk (componentPoint D E)))) :
    ∃ V : FiniteEtale X,
      Nonempty ((FiniteEtale.pullback D.1.supportComplement.ι).obj V ≅ W)
theorem

exists_finiteEtale_extension_of_boundaryUnramified

L50 ↗
Yamaguchi26SolvableCoverings.exists_finiteEtale_extension_of_boundaryUnramified
Documentation

A Galois cover with trivial boundary stabilizers extends across the regular Cartier boundary as the actual relative normalization.

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
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]
Lean source · statement
theorem exists_finiteEtale_extension_of_boundaryUnramified
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    (W : FiniteEtale D.1.supportComplement) (hW : IsGalois W)
    (hU : IsBoundaryUnramified D W) :
    ∃ V : FiniteEtale X,
      Nonempty ((FiniteEtale.pullback D.1.supportComplement.ι).obj V ≅ W)
theorem

kernel_le_boundaryUnramifiedKernelIntersection

L62 ↗
Yamaguchi26SolvableCoverings.kernel_le_boundaryUnramifiedKernelIntersection
Documentation

Every element killed by the ambient fundamental-group map is killed by each Galois quotient with trivial boundary stabilizers.

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
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]
Lean source · statement
theorem kernel_le_boundaryUnramifiedKernelIntersection
    [ConnectedSpace X]
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement) :
    (fundamentalGroupHom D.1.supportComplement.ι point).toMonoidHom.ker ≤
      boundaryUnramifiedKernelIntersection D point

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