Module

Scheme_Opens_range_algebraMap_functionField_eq_iInf.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Opens_range_algebraMap_functionField_eq_iInf

2 declarations indexed from sourceView source ↗

Module documentation

Sections as an intersection of stalks in the function field

For a nonempty open of an integral scheme, the image of its section ring in the function field equals the intersection of the images of the stalks at its points.

Imports1

Nyll.AlgebraicCurves.Geometry.Schemes.IsAffineOpen_range_algebraMap_functionField_eq_iInf

Imported by3

theorem

germToFunctionField_map

L41 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Opens_range_algebraMap_functionField_eq_iInf.AlgebraicGeometry.EngineOpen.germToFunctionField_map

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Opens_range_algebraMap_functionField_eq_iInf
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace EngineOpen
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} [IsIntegral X]

Lean source · statement

theorem germToFunctionField_map {U V : X.Opens} [Nonempty U] [Nonempty V] (i : V ⟶ U) (s : Γ(X,
    U)) :
    (X.germToFunctionField V).hom ((X.presheaf.map i.op).hom s) = (X.germToFunctionField U).hom
        s

theorem

range_algebraMap_functionField_eq_iInf

L51 ↗

AlgebraicGeometry.Scheme.Opens.range_algebraMap_functionField_eq_iInf

Source context 9 commands