NYLL
Module

BoundaryHeightOneEtale.lean

Nyll.Yamaguchi26SolvableCoverings.Geometry.BoundaryHeightOneEtale
5 declarations indexed from sourceView source ↗

Module documentation

Height-one étaleness over arbitrary boundary stalks

A height-one prime containing the Cartier ideal represents a generic point of an actual component of the boundary. The previously constructed étale normalization over that component's DVR therefore remains étale after passing to the chosen prime localization of the original stalk.

Imports7
Imported by2

Declarations

theorem

localizationAtPrimeTo_factor

L32 ↗
Yamaguchi26SolvableCoverings.localizationAtPrimeTo_factor
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
namespace Yamaguchi26SolvableCoverings
Lean source · statement
theorem localizationAtPrimeTo_factor
    (X : Scheme.{0}) (x : X) (q : Spec (X.presheaf.stalk x))
    [hq : q.asIdeal.IsPrime] :
    (Spec.map (Spec.stalkIso (X.presheaf.stalk x) q).hom ≫
      Spec.map ((X.fromSpecStalk x).stalkMap q)) ≫
        X.fromSpecStalk (X.fromSpecStalk x q) =
      Scheme.localizationAtPrimeTo X x q.asIdeal
theorem

etale_pullback_snd_comp

L59 ↗
Yamaguchi26SolvableCoverings.etale_pullback_snd_comp
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
namespace Yamaguchi26SolvableCoverings
Lean source · statement
theorem etale_pullback_snd_comp
    {N X S T : Scheme.{0}} (g : N ⟶ X) (b : S ⟶ X) (l : T ⟶ S)
    [Etale (pullback.snd g b)] : Etale (pullback.snd g (l ≫ b))
theorem

normalization_heightOne_etale_of_componentStalks

L77 ↗
Yamaguchi26SolvableCoverings.normalization_heightOne_etale_of_componentStalks
Documentation

Height-one points on a Cartier boundary come from its generic component points. Etaleness of the actual normalization at those component stalks therefore supplies every height-one stalk localization needed by purity.

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
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]
Lean source · statement
theorem normalization_heightOne_etale_of_componentStalks
    (D : X.EffectiveCartierDivisor) (W : FiniteEtale D.1.supportComplement)
    (hgeneric : ∀ E : Component D,
      Etale (pullback.snd (W.hom ≫ D.1.supportComplement.ι).fromNormalization
        (X.fromSpecStalk (componentPoint D E))))
    (x : X) (p : Ideal (X.presheaf.stalk x)) [p.IsPrime]
    (hp : p.height = 1) (hDp : D.1.stalkIdeal x ≤ p) :
    Etale (pullback.snd (W.hom ≫ D.1.supportComplement.ι).fromNormalization
      (Scheme.localizationAtPrimeTo X x p))
theorem

boundaryUnramified_normalization_componentStalk_etale

L105 ↗
Yamaguchi26SolvableCoverings.boundaryUnramified_normalization_componentStalk_etale
Documentation

Trivial finite boundary inertia gives etaleness at each component stalk; the domain and DVR structures are transported to the paper's component point.

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
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]
Lean source · statement
theorem boundaryUnramified_normalization_componentStalk_etale
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    (W : FiniteEtale D.1.supportComplement) (hW : IsGalois W)
    (hU : IsBoundaryUnramified D W) (E : Component D) :
    Etale (pullback.snd (W.hom ≫ D.1.supportComplement.ι).fromNormalization
      (X.fromSpecStalk (componentPoint D E)))
theorem

boundaryUnramified_normalization_heightOne_etale

L129 ↗
Yamaguchi26SolvableCoverings.boundaryUnramified_normalization_heightOne_etale
Documentation

The actual relative normalization is étale over every height-one prime localization of a stalk whose prime contains the Cartier boundary ideal.

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
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [IsLocallyNoetherian X]
Lean source · statement
theorem boundaryUnramified_normalization_heightOne_etale
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    [ConnectedSpace D.1.supportComplement]
    (W : FiniteEtale D.1.supportComplement) (hW : IsGalois W)
    (hU : IsBoundaryUnramified D W)
    (x : X) (p : Ideal (X.presheaf.stalk x)) [p.IsPrime]
    (hp : p.height = 1) (hDp : D.1.stalkIdeal x ≤ p) :
    Etale (pullback.snd (W.hom ≫ D.1.supportComplement.ι).fromNormalization
      (Scheme.localizationAtPrimeTo X x p))

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