# mathlibdocumentation

algebraic_geometry.function_field

# 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 #

• algebraic_geometry.Scheme.function_field: The function field of an integral scheme.
• algebraic_geometry.germ_to_function_field: The canonical map from a component into the function field. This map is injective.

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.

The restriction map from a component to the function field.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[simp]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]