Documentation

Mathlib.AlgebraicGeometry.FunctionField

Function field of integral schemes #

We define the function field of an irreducible scheme as the stalk of the generic point. This is a field when the scheme is integral.

Main definition #

• AlgebraicGeometry.Scheme.functionField: The function field of an integral scheme.
• Algebraic_geometry.germToFunctionField: The canonical map from a component into the function field. This map is injective.
@[inline, reducible]
noncomputable abbrev AlgebraicGeometry.Scheme.functionField [IrreducibleSpace X.toPresheafedSpace] :

The function field of an irreducible scheme is the local ring at its generic point. Despite the name, this is a field only when the scheme is integral.

Instances For
@[inline, reducible]
noncomputable abbrev AlgebraicGeometry.Scheme.germToFunctionField [IrreducibleSpace X.toPresheafedSpace] (U : TopologicalSpace.Opens X.toPresheafedSpace) [h : Nonempty { x // x U }] :
X.presheaf.obj ()

The restriction map from a component to the function field.

Instances For
theorem AlgebraicGeometry.germ_injective_of_isIntegral {U : TopologicalSpace.Opens X.toPresheafedSpace} (x : { x // x U }) :
theorem AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion (f : X Y) [hX : IrreducibleSpace X.toPresheafedSpace] [IrreducibleSpace Y.toPresheafedSpace] :
f.val.base (genericPoint X.toPresheafedSpace) = genericPoint Y.toPresheafedSpace
noncomputable instance AlgebraicGeometry.stalkFunctionFieldAlgebra [IrreducibleSpace X.toPresheafedSpace] (x : X.toPresheafedSpace) :
Algebra ↑(TopCat.Presheaf.stalk X.presheaf x)
instance AlgebraicGeometry.functionField_isScalarTower [IrreducibleSpace X.toPresheafedSpace] (U : TopologicalSpace.Opens X.toPresheafedSpace) (x : { x // x U }) [Nonempty { x // x U }] :
IsScalarTower ↑(X.presheaf.obj ()) ↑(TopCat.Presheaf.stalk X.presheaf x)
@[simp]
theorem AlgebraicGeometry.genericPoint_eq_bot_of_affine (R : CommRingCat) [IsDomain R] :
genericPoint ().toPresheafedSpace = { asIdeal := 0, IsPrime := (_ : ) }
theorem AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) [h : Nonempty { x // x U }] :
AlgebraicGeometry.IsAffineOpen.primeIdealOf hU { val := genericPoint X.toPresheafedSpace, property := (_ : genericPoint X.toPresheafedSpace U) } = genericPoint (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj ()))).toPresheafedSpace
theorem AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen (U : TopologicalSpace.Opens X.toPresheafedSpace) (hU : ) [hU' : Nonempty { x // x U }] :
IsFractionRing ↑(X.presheaf.obj ())
instance AlgebraicGeometry.instIsAffineObjAffineCover (x : X.toPresheafedSpace) :