Module

IsomorphismNeighborhood.lean

Nyll.SchemeTheory.Etale.IsomorphismNeighborhood

4 declarations indexed from sourceView source ↗

Module documentation

Isomorphism neighborhoods of finite étale morphisms

The rank-one locus of a finite flat finitely presented morphism is open, and the restriction to it is an isomorphism. For an étale morphism, a singleton fiber with unchanged residue field is an isomorphism: the residue-field point is a surjective étale monomorphism onto that fiber. Together these give an isomorphism neighborhood for finite étale morphisms.

Imports10

Mathlib.AlgebraicGeometry.Fiber
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Mathlib.FieldTheory.PurelyInseparable.Basic
Mathlib.RingTheory.RingHom.PurelyInseparable
Mathlib.AlgebraicGeometry.Restrict
Mathlib.Topology.LocallyConstant.Basic

Imported by2

theorem

exists_isIso_restrict_of_finrank_eq_one

L40 ↗

AlgebraicGeometry.Scheme.Hom.exists_isIso_restrict_of_finrank_eq_one

Documentation

Rank one at a point gives an actual open neighborhood on which a finite flat finitely presented morphism is an isomorphism.

Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits TopologicalSpace
universe u
namespace AlgebraicGeometry

Lean source · statement

theorem Scheme.Hom.exists_isIso_restrict_of_finrank_eq_one
    {X Y : Scheme.{u}} (p : X ⟶ Y)
    [Flat p] [IsFinite p] [LocallyOfFinitePresentation p]
    (y : Y) (hy : p.finrank y = 1) :
    ∃ U : Y.Opens, y ∈ U ∧ IsIso (p ∣_ U)

theorem

isIso_fiberToSpecResidueField_of_unique_preimage

L55 ↗

AlgebraicGeometry.Etale.isIso_fiberToSpecResidueField_of_unique_preimage

Documentation

A singleton étale fiber with unchanged residue field is an isomorphism over the residue field of the base point.

Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits TopologicalSpace
universe u
namespace AlgebraicGeometry

Lean source · statement

theorem Etale.isIso_fiberToSpecResidueField_of_unique_preimage
    {X Y : Scheme.{u}} (p : X ⟶ Y) [Etale p] (x : X)
    (hx : ∀ x' : X, p x' = p x → x' = x) [IsIso (p.residueFieldMap x)] :
    IsIso (p.fiberToSpecResidueField (p x))

theorem

exists_isIso_restrict_of_unique_preimage

L85 ↗

AlgebraicGeometry.Etale.exists_isIso_restrict_of_unique_preimage

Documentation

A finite étale morphism with a singleton fiber and unchanged residue field is an isomorphism on an open neighborhood of that fiber.

Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits TopologicalSpace
universe u
namespace AlgebraicGeometry

Lean source · statement

theorem Etale.exists_isIso_restrict_of_unique_preimage
    {X Y : Scheme.{u}} (p : X ⟶ Y) [IsFinite p] [Etale p] (x : X)
    (hx : ∀ x' : X, p x' = p x → x' = x) [IsIso (p.residueFieldMap x)] :
    ∃ U : Y.Opens, p x ∈ U ∧ IsIso (p ∣_ U)

theorem

exists_isIso_restrict_of_unique_preimage_of_isPurelyInseparable

L102 ↗

AlgebraicGeometry.Etale.exists_isIso_restrict_of_unique_preimage_of_isPurelyInseparable

Documentation

A finite étale morphism whose fiber is a single point with purely inseparable residue extension is an isomorphism on a neighborhood.

Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits TopologicalSpace
universe u
namespace AlgebraicGeometry

Lean source · statement

theorem Etale.exists_isIso_restrict_of_unique_preimage_of_isPurelyInseparable
    {X Y : Scheme.{u}} (p : X ⟶ Y) [IsFinite p] [Etale p] (x : X)
    (hx : ∀ x' : X, p x' = p x → x' = x)
    (hκ : (p.residueFieldMap x).hom.IsPurelyInseparable) :
    ∃ U : Y.Opens, p x ∈ U ∧ IsIso (p ∣_ U)

Module documentation

Isomorphism neighborhoods of finite étale morphisms

Declarations

exists_isIso_restrict_of_finrank_eq_one

isIso_fiberToSpecResidueField_of_unique_preimage

exists_isIso_restrict_of_unique_preimage

exists_isIso_restrict_of_unique_preimage_of_isPurelyInseparable