The presheaf of rational sections on an integral scheme

This file owns the presheaf of rational functions on an integral scheme, as a presheaf of modules over the structure presheaf. Sections on an open are proof-indexed: the function field on a nonempty open and the zero module on the empty open, which makes restriction definitional.

Nothing here mentions divisors. AssociatedSheaf.Construction builds the fractional subpresheaf of a Cartier divisor inside this presheaf.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.RationalSections (X : Scheme) [IsIntegral X] (U : X.Opens) : Type u

Rational sections on an open. The proof-indexed presentation is the function field on a nonempty open and the zero module on the empty open.

Equations

• X.RationalSections U = (PLift (Nonempty ↥↑U) → ↑X.functionField)

def AlgebraicGeometry.Scheme.rationalSectionsRes (X : Scheme) [IsIntegral X] {U V : X.Opens} (h : V ≤ U) : X.RationalSections U →+ X.RationalSections V

Restriction of rational sections.

Equations

• X.rationalSectionsRes h = { toFun := fun (s : X.RationalSections U) (hV : PLift (Nonempty ↥↑V)) => s { down := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

theorem AlgebraicGeometry.Scheme.germToFunctionField_res (X : Scheme) [IsIntegral X] {U V : X.Opens} (h : V ≤ U) (r : ↑(X.presheaf.obj (Opposite.op U))) (hV : PLift (Nonempty ↥↑V)) : (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField V)) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) r) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) r

Restriction commutes with the germ map to the function field.

theorem AlgebraicGeometry.Scheme.rationalSectionsRes_smul (X : Scheme) [IsIntegral X] {U V : X.Opens} (h : V ≤ U) (r : ↑(X.presheaf.obj (Opposite.op U))) (s : X.RationalSections U) : (X.rationalSectionsRes h) (r • s) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) r • (X.rationalSectionsRes h) s

Restriction of rational sections is semilinear over restriction of structure-sheaf sections.

noncomputable def AlgebraicGeometry.Scheme.rationalPresheaf (X : Scheme) [IsIntegral X] : X.PresheafOfModules

The presheaf of rational functions, as modules over the structure presheaf.

Equations

• One or more equations did not get rendered due to their size.