Module

StalkSpreadingOpen.lean

Nyll.SchemeTheory.Descent.StalkSpreadingOpen

1 declaration indexed from sourceView source ↗

Module documentation

Spreading a stalk morphism on an arbitrary scheme

The actual affine-neighborhood stalk is identified by its canonical stalk isomorphism. Finite-presentation spreading on that affine neighborhood then produces a morphism on an actual open of the original scheme, with the original stalk factorization retained. No finiteness assumption on the ambient scheme is needed.

Imports2

Nyll.SchemeTheory.Descent.StalkSpreading
Mathlib.AlgebraicGeometry.Restrict

Imported by2

theorem

exists_open_extension_fromSpecStalk

L30 ↗

AlgebraicGeometry.Scheme.exists_open_extension_fromSpecStalk

Documentation

A relative morphism from an actual stalk into a locally finitely presented scheme extends over an open neighborhood of that point.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme

Lean source · statement

theorem exists_open_extension_fromSpecStalk
    {X Y : Scheme.{u}} (f : Y ⟶ X) [LocallyOfFinitePresentation f]
    (x : X) (a : Spec (X.presheaf.stalk x) ⟶ Y)
    (ha : a ≫ f = X.fromSpecStalk x) :
    ∃ (W : X.Opens) (hxW : x ∈ W) (b : W.toScheme ⟶ Y),
      W.fromSpecStalkOfMem x hxW ≫ b = a ∧ b ≫ f = W.ι

Module documentation

Spreading a stalk morphism on an arbitrary scheme

Declarations

exists_open_extension_fromSpecStalk