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 #

@[inline, reducible]

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 (X : AlgebraicGeometry.Scheme) [IrreducibleSpace X.toPresheafedSpace] (U : TopologicalSpace.Opens X.toPresheafedSpace) [h : Nonempty { x // x U }] :

    The restriction map from a component to the function field.

    Instances For
      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.val.base (genericPoint X.toPresheafedSpace) = genericPoint Y.toPresheafedSpace
      noncomputable instance AlgebraicGeometry.stalkFunctionFieldAlgebra (X : AlgebraicGeometry.Scheme) [IrreducibleSpace X.toPresheafedSpace] (x : X.toPresheafedSpace) :
      instance AlgebraicGeometry.functionField_isScalarTower (X : AlgebraicGeometry.Scheme) [IrreducibleSpace X.toPresheafedSpace] (U : TopologicalSpace.Opens X.toPresheafedSpace) (x : { x // x U }) [Nonempty { x // x U }] :
      @[simp]
      theorem AlgebraicGeometry.genericPoint_eq_bot_of_affine (R : CommRingCat) [IsDomain R] :
      genericPoint (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)).toPresheafedSpace = { asIdeal := 0, IsPrime := (_ : Ideal.IsPrime ) }
      theorem AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) [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 (Opposite.op U)))).toPresheafedSpace