NYLL
Module

CartierNormalizationSpreading.lean

Nyll.EtaleFundamentalGroups.Purity.CartierNormalizationSpreading
4 declarations indexed from sourceView source ↗

Module documentation

Spreading finite étale normalization along a Cartier boundary

Choose actual principal Cartier charts. Stalk-localization isomorphisms, normalization under open base change, and the principal complement square transport the given local finite étaleness to the affine normalization. The principal spreading theorem and locality on the target then give finite étaleness of the original relative normalization.

Imports13
Imported by2

Declarations

theorem

finiteEtale_pullback_snd_comp

L40 ↗
EtaleFundamentalGroups.finiteEtale_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 AlgebraicGeometry.FiniteEtale EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem finiteEtale_pullback_snd_comp
    {N X S T : Scheme.{u}} (g : N ⟶ X) (b : S ⟶ X) (a : T ⟶ S)
    [IsFiniteEtale (pullback.snd g b)] :
    IsFiniteEtale (pullback.snd g (a ≫ b))
theorem

finiteEtale_iterated_pullback_snd

L48 ↗
EtaleFundamentalGroups.finiteEtale_iterated_pullback_snd
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry.FiniteEtale EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem finiteEtale_iterated_pullback_snd
    {N X S T : Scheme.{u}} (g : N ⟶ X) (b : S ⟶ X) (a : T ⟶ S)
    [IsFiniteEtale (pullback.snd g (a ≫ b))] :
    IsFiniteEtale (pullback.snd (pullback.snd g b) a)
theorem

finiteEtale_normalization_affineChart

L58 ↗
EtaleFundamentalGroups.finiteEtale_normalization_affineChart
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry.FiniteEtale EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}} [IsLocallyNoetherian X]
Lean source · statement
theorem finiteEtale_normalization_affineChart
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    (W : FiniteEtale D.1.supportComplement)
    (hboundary : ∀ x : X, x ∈ D.1.support →
      IsFiniteEtale (pullback.snd (W.hom ≫ D.1.supportComplement.ι).fromNormalization
        (X.fromSpecStalk x)))
    {U : X.Opens} (hU : IsAffineOpen U) (d : Γ(X, U))
    (hd : D.1.ideal ⟨U, hU⟩ = Ideal.span {d}) :
    IsFiniteEtale (pullback.snd (W.hom ≫ D.1.supportComplement.ι).fromNormalization
      hU.fromSpec)
theorem

finiteEtale_normalization_of_cartier_boundary_stalks

L139 ↗
EtaleFundamentalGroups.finiteEtale_normalization_of_cartier_boundary_stalks
Documentation

A finite étale cover of a Cartier complement extends by its actual relative normalization when that normalization is finite étale at every boundary stalk. Only regularity along the boundary is used.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry.FiniteEtale EtaleFundamentalGroups.Inertia
namespace EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}} [IsLocallyNoetherian X]
Lean source · statement
theorem finiteEtale_normalization_of_cartier_boundary_stalks
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    (W : FiniteEtale D.1.supportComplement)
    (hboundary : ∀ x : X, x ∈ D.1.support →
      IsFiniteEtale (pullback.snd (W.hom ≫ D.1.supportComplement.ι).fromNormalization
        (X.fromSpecStalk x))) :
    IsFiniteEtale (W.hom ≫ D.1.supportComplement.ι).fromNormalization

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