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 #

@[reducible, inline]

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.

Equations
  • X.functionField = X.presheaf.stalk (genericPoint X.toPresheafedSpace)
Instances For
    @[reducible, inline]
    noncomputable abbrev AlgebraicGeometry.Scheme.germToFunctionField (X : AlgebraicGeometry.Scheme) [IrreducibleSpace X.toPresheafedSpace] (U : X.Opens) [h : Nonempty (↑U).toPresheafedSpace] :
    X.presheaf.obj (Opposite.op U) X.functionField

    The restriction map from a component to the function field.

    Equations
    • X.germToFunctionField U = X.presheaf.germ U (genericPoint X.toPresheafedSpace)
    Instances For
      theorem AlgebraicGeometry.germ_injective_of_isIntegral (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] {U : X.Opens} (x : X.toPresheafedSpace) (hx : x U) :
      Function.Injective (X.presheaf.germ U x hx)
      theorem AlgebraicGeometry.Scheme.germToFunctionField_injective (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (U : X.Opens) [Nonempty (↑U).toPresheafedSpace] :
      Function.Injective (X.germToFunctionField U)
      theorem AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) [H : AlgebraicGeometry.IsOpenImmersion f] [hX : IrreducibleSpace X.toPresheafedSpace] [IrreducibleSpace Y.toPresheafedSpace] :
      f.base (genericPoint X.toPresheafedSpace) = genericPoint Y.toPresheafedSpace
      noncomputable instance AlgebraicGeometry.stalkFunctionFieldAlgebra (X : AlgebraicGeometry.Scheme) [IrreducibleSpace X.toPresheafedSpace] (x : X.toPresheafedSpace) :
      Algebra (X.presheaf.stalk x) X.functionField
      Equations
      instance AlgebraicGeometry.functionField_isScalarTower (X : AlgebraicGeometry.Scheme) [IrreducibleSpace X.toPresheafedSpace] (U : X.Opens) (x : U) [Nonempty (↑U).toPresheafedSpace] :
      IsScalarTower (X.presheaf.obj (Opposite.op U)) (X.presheaf.stalk x) X.functionField
      Equations
      • =
      Equations
      • One or more equations did not get rendered due to their size.
      theorem AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) [h : Nonempty (↑U).toPresheafedSpace] :
      hU.primeIdealOf genericPoint X.toPresheafedSpace, = genericPoint (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).toPresheafedSpace
      theorem AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (U : X.Opens) (hU : AlgebraicGeometry.IsAffineOpen U) [Nonempty (↑U).toPresheafedSpace] :
      IsFractionRing (X.presheaf.obj (Opposite.op U)) X.functionField
      Equations
      • =
      Equations
      • =