mathlib3 documentation

algebraic_geometry.function_field

Function field of integral schemes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

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.