Module

StalkSpreading.lean

Nyll.SchemeTheory.Descent.StalkSpreading

1 declaration indexed from sourceView source ↗

Module documentation

+# Spreading a stalk morphism with finitely presented target

The actual stalk is the colimit of the rings of sections over its open neighborhoods. Applying Spec gives an affine inverse system. A morphism from this limit into a locally finitely presented relative target descends to one stage; composition with the neighborhood's affinization gives an actual morphism on that neighborhood.

No injectivity of a germ map, Noetherianity, reducedness, or normality is required. This is the local morphism supplier needed for Stacks 0BQF.

Imports5

Mathlib.AlgebraicGeometry.AffineTransitionLimit
Mathlib.AlgebraicGeometry.Stalk
Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Mathlib.CategoryTheory.Limits.Opposites
Mathlib.Topology.Sheaves.Stalks

Imported by4

theorem

exists_open_extension_fromSpecStalk_of_isAffine

L35 ↗

AlgebraicGeometry.Scheme.exists_open_extension_fromSpecStalk_of_isAffine

Documentation

A morphism from an actual scheme stalk spreads over an affine base when its target is locally of finite presentation.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry

Lean source · statement

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

Module documentation

Declarations

exists_open_extension_fromSpecStalk_of_isAffine