Module

BoundaryStalkNormalizationEtale.lean

Nyll.Yamaguchi26SolvableCoverings.Geometry.BoundaryStalkNormalizationEtale

3 declarations indexed from sourceView source ↗

Module documentation

Finite etale normalization at every boundary stalk

Choose an actual local Cartier equation. Every connected Galois component of the pulled-back cover has etale normalization by purity: height-one etaleness comes from the original boundary components, and regularity is transferred through the actual stalk-localization isomorphism. The normalized components cover the whole normalization. Its integral structure map is therefore finite etale, and the canonical localization comparison returns the actual base change of the original relative normalization.

Imports7

Imported by2

theorem

exists_nonzero_stalk_cartier_equation

L35 ↗

Yamaguchi26SolvableCoverings.exists_nonzero_stalk_cartier_equation

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open CategoryTheory.PreGaloisCategory AlgebraicGeometry.FiniteEtale
open EtaleFundamentalGroups EtaleFundamentalGroups.Inertia
namespace Yamaguchi26SolvableCoverings

Lean source · statement

theorem exists_nonzero_stalk_cartier_equation
    {X : Scheme.{0}} (D : X.EffectiveCartierDivisor) (x : X)
    [IsDomain (X.presheaf.stalk x)] :
    ∃ d : X.presheaf.stalk x, d ≠ 0 ∧ D.1.stalkIdeal x = Ideal.span {d}

theorem

normalization_boundaryStalk_finiteEtale_of_componentStalks

L57 ↗

Yamaguchi26SolvableCoverings.normalization_boundaryStalk_finiteEtale_of_componentStalks

Documentation

At every point of the regular Cartier boundary, the actual relative normalization of a Galois cover is finite etale if it is etale at each generic component stalk.

Source context 6 commands

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

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

Lean source · statement

theorem normalization_boundaryStalk_finiteEtale_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 (pullback.snd (W.hom ≫ D.1.supportComplement.ι).fromNormalization
        (X.fromSpecStalk (componentPoint D E))))
    (x : X) (hx : x ∈ D.1.support) :
    IsFiniteEtale (pullback.snd (W.hom ≫ D.1.supportComplement.ι).fromNormalization
      (X.fromSpecStalk x))

theorem

boundaryUnramified_normalization_boundaryStalk_finiteEtale

L142 ↗

Yamaguchi26SolvableCoverings.boundaryUnramified_normalization_boundaryStalk_finiteEtale

Documentation

At every point of the regular Cartier boundary, the actual relative normalization of a boundary-unramified Galois cover is finite etale.

Source context 6 commands

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

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

Lean source · statement

theorem boundaryUnramified_normalization_boundaryStalk_finiteEtale
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    (W : FiniteEtale D.1.supportComplement) (hW : IsGalois W)
    (hU : IsBoundaryUnramified D W) (x : X) (hx : x ∈ D.1.support) :
    IsFiniteEtale (pullback.snd (W.hom ≫ D.1.supportComplement.ι).fromNormalization
      (X.fromSpecStalk x))

Module documentation

Finite etale normalization at every boundary stalk

Declarations

exists_nonzero_stalk_cartier_equation

normalization_boundaryStalk_finiteEtale_of_componentStalks

boundaryUnramified_normalization_boundaryStalk_finiteEtale