NYLL
Module

PunctureSectionSpreading.lean

Nyll.SchemeTheory.Descent.PunctureSectionSpreading
2 declarations indexed from sourceView source ↗

Module documentation

Spreading a morphism from a retrocompact part of a local spectrum

Base change the actual stalk inverse system by a retrocompact open. Its stages are quasi-compact and quasi-separated. Finite-presentation Hom descent then spreads the given morphism to the overlap with an actual neighborhood, retaining the original morphism on the local spectrum.

Imports4
Imported by2

Declarations

def

stalkOverlapToNeighborhood

L31 ↗
AlgebraicGeometry.Scheme.stalkOverlapToNeighborhood
Documentation

The actual map from the local-spectrum overlap to the overlap with an open neighborhood of the chosen point.

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.Scheme
Lean source · statement
def stalkOverlapToNeighborhood
    (X : Scheme.{u}) (x : X) (U N : X.Opens) (hxN : x ∈ N) :
    pullback (X.fromSpecStalk x) U.ι ⟶ pullback N.ι U.ι
theorem

exists_open_overlap_extension_fromSpecStalk

L44 ↗
AlgebraicGeometry.Scheme.exists_open_overlap_extension_fromSpecStalk
Documentation

A morphism on the retrocompact part of the actual local spectrum spreads to the intersection with an open neighborhood. The target needs only to be locally of finite presentation over the affine base.

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.Scheme
Lean source · statement
theorem exists_open_overlap_extension_fromSpecStalk
    {X Y : Scheme.{u}} [IsAffine X]
    (f : Y ⟶ X) [LocallyOfFinitePresentation f]
    (U : X.Opens) [QuasiCompact U.ι] (x : X)
    (a : pullback (X.fromSpecStalk x) U.ι ⟶ Y)
    (ha : a ≫ f = pullback.snd (X.fromSpecStalk x) U.ι ≫ U.ι) :
    ∃ (N : X.Opens) (hxN : x ∈ N) (b : pullback N.ι U.ι ⟶ Y),
      b ≫ f = pullback.snd N.ι U.ι ≫ U.ι ∧
        stalkOverlapToNeighborhood X x U N hxN ≫ b = a

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.