Module

FiniteEtaleFromBoundaryStalks.lean

Nyll.EtaleFundamentalGroups.Purity.FiniteEtaleFromBoundaryStalks

5 declarations indexed from sourceView source ↗

Module documentation

Finite etaleness from the punctured locus and boundary stalks

For a morphism of finite presentation, formal etaleness of every stalk is enough to recover etaleness. Combining this with the finite-presentation consequence of finiteness over a locally Noetherian target gives a boundary criterion: a finite morphism which is etale on an open set is finite etale as soon as its stalk maps at the complementary points are formally etale.

The local input is deliberately only formal etaleness. In applications to a normalization, this is the part supplied by punctured purity after identifying the localized normalization with the canonical local extension.

Imports4

Nyll.SchemeTheory.FiniteEtale.Local.OfTargetLocalizations
Nyll.SchemeTheory.LocalGeometry.EtaleStalkPrimeLocalization
Mathlib.AlgebraicGeometry.Noetherian
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic

Imported by5

lemma

of_bijective

L37 ↗

EtaleFundamentalGroups.RingHom.FormallyEtale.of_bijective

Documentation

A bijective ring map is formally etale.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace EtaleFundamentalGroups
universe u
open AlgebraicGeometry

Lean source · statement

lemma RingHom.FormallyEtale.of_bijective
    {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S)
    (hf : Function.Bijective f) : f.FormallyEtale

lemma

respectsIso

L44 ↗

EtaleFundamentalGroups.RingHom.FormallyEtale.respectsIso

Documentation

Formal etaleness of ring maps is invariant under isomorphisms of arrows.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace EtaleFundamentalGroups
universe u
open AlgebraicGeometry

Lean source · statement

lemma RingHom.FormallyEtale.respectsIso :
    RingHom.RespectsIso @RingHom.FormallyEtale

theorem

etale_of_stalkMap_formallyEtale

L55 ↗

EtaleFundamentalGroups.etale_of_stalkMap_formallyEtale

Documentation

A locally finitely presented scheme morphism whose stalk maps are all formally etale is etale.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace EtaleFundamentalGroups
universe u
open AlgebraicGeometry

Lean source · statement

theorem etale_of_stalkMap_formallyEtale
    {Y X : Scheme.{u}} (f : Y ⟶ X) [LocallyOfFinitePresentation f]
    (hstalk : ∀ y : Y, (f.stalkMap y).hom.FormallyEtale) :
    Etale f

theorem

isFiniteEtale_of_isFinite_of_stalkMap_formallyEtale

L90 ↗

EtaleFundamentalGroups.isFiniteEtale_of_isFinite_of_stalkMap_formallyEtale

Documentation

A finite morphism over a locally Noetherian target is finite etale if all of its stalk maps are formally etale.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace EtaleFundamentalGroups
universe u
open AlgebraicGeometry

Lean source · statement

theorem isFiniteEtale_of_isFinite_of_stalkMap_formallyEtale
    {Y X : Scheme.{u}} [IsLocallyNoetherian X]
    (f : Y ⟶ X) [IsFinite f]
    (hstalk : ∀ y : Y, (f.stalkMap y).hom.FormallyEtale) :
    IsFiniteEtale f

theorem

isFiniteEtale_of_isFinite_of_restrict_etale_of_boundary_stalkMap_formallyEtale

L101 ↗

EtaleFundamentalGroups.isFiniteEtale_of_isFinite_of_restrict_etale_of_boundary_stalkMap_formallyEtale

Documentation

Boundary criterion for finite etaleness. It is enough to know etaleness over an open set and formal etaleness of the original stalk maps over its complement.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace EtaleFundamentalGroups
universe u
open AlgebraicGeometry

Lean source · statement

theorem isFiniteEtale_of_isFinite_of_restrict_etale_of_boundary_stalkMap_formallyEtale
    {Y X : Scheme.{u}} [IsLocallyNoetherian X]
    (f : Y ⟶ X) [IsFinite f] (U : X.Opens)
    (hU : Etale (f ∣_ U))
    (hboundary : ∀ y : Y, f y ∉ U → (f.stalkMap y).hom.FormallyEtale) :
    IsFiniteEtale f

Module documentation

Finite etaleness from the punctured locus and boundary stalks

Declarations

of_bijective

respectsIso

etale_of_stalkMap_formallyEtale

isFiniteEtale_of_isFinite_of_stalkMap_formallyEtale

isFiniteEtale_of_isFinite_of_restrict_etale_of_boundary_stalkMap_formallyEtale