Module

IsAffineOpen_range_algebraMap_functionField_eq_iInf.lean

Nyll.AlgebraicCurves.Geometry.Schemes.IsAffineOpen_range_algebraMap_functionField_eq_iInf

1 declaration indexed from sourceView source ↗

Module documentation

Sections on an affine open inside the function field

The image of the section ring of a nonempty affine open in the function field is the intersection of the images of the stalks at points of that open.

Imports1

Mathlib.AlgebraicGeometry.FunctionField

Imported by3

theorem

range_algebraMap_functionField_eq_iInf

L31 ↗

AlgebraicGeometry.IsAffineOpen.range_algebraMap_functionField_eq_iInf

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsAffineOpen_range_algebraMap_functionField_eq_iInf
open CategoryTheory AlgebraicGeometry
universe u

Lean source · statement

theorem _root_.AlgebraicGeometry.IsAffineOpen.range_algebraMap_functionField_eq_iInf
    {X : Scheme.{u}} [IsIntegral X] {U : X.Opens} (hU : IsAffineOpen U) [Nonempty U] :
    (algebraMap Γ(X, U) X.functionField).range =
      ⨅ (x : X) (_ : x ∈ U), (algebraMap (X.presheaf.stalk x) X.functionField).range

Module documentation

Sections on an affine open inside the function field

Declarations

range_algebraMap_functionField_eq_iInf