Module

ClosedNeighborhoodLift.lean

Nyll.SchemeTheory.Etale.ClosedNeighborhoodLift

2 declarations indexed from sourceView source ↗

Module documentation

Lifting pointed étale neighborhoods across closed immersions

Choose an affine open in the ambient scheme containing the image of the point, then an affine open in the restricted étale neighborhood. The affine lifting theorem supplies an ambient étale scheme; the pullback pasting isomorphism identifies its restriction with the chosen open neighborhood.

The construction works for any nonempty one-point test scheme, hence for geometric points without imposing a base field on the ambient scheme.

Imports9

Nyll.SchemeTheory.Etale.AffineClosedLift
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Mathlib.AlgebraicGeometry.Cover.Open
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Imported by3

theorem

exists_affineCover_factor

L41 ↗

AlgebraicGeometry.Etale.exists_affineCover_factor

Source context 5 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry TensorProduct
namespace AlgebraicGeometry.Etale

Lean source · statement

theorem exists_affineCover_factor
    {P W : Scheme.{u}} [Subsingleton P] [Nonempty P] (w : P ⟶ W) :
    ∃ (a : W.affineCover.I₀) (w' : P ⟶ W.affineCover.X a),
      w' ≫ W.affineCover.f a = w

theorem

exists_neighborhood_lift_of_closedImmersion

L55 ↗

AlgebraicGeometry.Etale.exists_neighborhood_lift_of_closedImmersion

Documentation

A pointed étale neighborhood of a closed subscheme contains an open neighborhood which is the restriction of an affine étale scheme over the ambient scheme. The chosen point factors through that restriction.