NYLL
Module

StalkBaseChangeSections.lean

Nyll.SchemeTheory.Affine.StalkBaseChangeSections
1 declaration indexed from sourceView source ↗

Module documentation

Scalar sections after base change to a stalk

For a qcqs morphism whose structure-sheaf map is an isomorphism, flat base change to the spectrum of a target stalk preserves the global-section map as an isomorphism. The section pushout is computed on an affine neighborhood of the chosen point.

Imports4
Imported by2

Declarations

theorem

isIso_appTop_pullback_fromSpecStalk_of_isIso_c

L31 ↗
AlgebraicGeometry.isIso_appTop_pullback_fromSpecStalk_of_isIso_c
Documentation

If the structure sheaf is the pushforward along a qcqs morphism, the base change to a target stalk induces an isomorphism on global sections.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem isIso_appTop_pullback_fromSpecStalk_of_isIso_c
    {X S : Scheme.{u}} (f : X ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    [IsIso f.c] (y : S) :
    IsIso (pullback.snd f (S.fromSpecStalk y)).appTop

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