Module

FiniteNormalizationExtension.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteNormalizationExtension

1 declaration indexed from sourceView source ↗

Module documentation

The actual finite étale extension supplied by normalization

When the relative normalization of a finite étale cover of an open subscheme is finite étale, it is an extension of the original cover. The restriction isomorphism comes from the actual open pullback and normalization comparison, using that a finite cover is already its own relative normalization.

Imports5

Nyll.EtaleFundamentalGroups.Inertia.NormalizationSourceIso
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Mathlib.AlgebraicGeometry.Normalization
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Mathlib.CategoryTheory.MorphismProperty.Comma

Imported by2

theorem

exists_finiteEtale_extension_of_normalization

L32 ↗

EtaleFundamentalGroups.Inertia.exists_finiteEtale_extension_of_normalization

Documentation

Finite étale relative normalization gives an actual extending object, together with an isomorphism from its restriction to the original cover.

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 exists_finiteEtale_extension_of_normalization
    {X : Scheme.{u}} (U : X.Opens) [QuasiCompact U.ι]
    (W : FiniteEtale U)
    [IsFiniteEtale (W.hom ≫ U.ι).fromNormalization] :
    ∃ V : FiniteEtale X, Nonempty ((FiniteEtale.pullback U.ι).obj V ≅ W)

Module documentation

The actual finite étale extension supplied by normalization

Declarations

exists_finiteEtale_extension_of_normalization