Module

NormalizationOpenStalk.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationOpenStalk

1 declaration indexed from sourceView source ↗

Module documentation

Relative normalization at a point inside the original open

At a point of the open, the map from the spectrum of the stalk factors through that open. The original finite etale cover is therefore already integral after base change, so its relative normalization is itself. The actual normalization-localization comparison returns the assertion for the original normalization's base change.

Imports4

Nyll.EtaleFundamentalGroups.Inertia.NormalizationStalkLocalization
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Mathlib.AlgebraicGeometry.Stalk
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Imported by2

theorem

finiteEtale_normalization_stalk_of_mem_open

L32 ↗

EtaleFundamentalGroups.Inertia.finiteEtale_normalization_stalk_of_mem_open

Documentation

Inside the original open, the relative normalization of a finite etale cover has finite etale base change to the actual ambient stalk.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

theorem finiteEtale_normalization_stalk_of_mem_open
    {X : Scheme.{u}} (U : X.Opens) [QuasiCompact U.ι]
    (W : FiniteEtale U) (x : X) (hx : x ∈ U) :
    IsFiniteEtale (pullback.snd (W.hom ≫ U.ι).fromNormalization (X.fromSpecStalk x))

Module documentation

Relative normalization at a point inside the original open

Declarations

finiteEtale_normalization_stalk_of_mem_open