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 #

source
@[reducible]
noncomputable def algebraic_geometry.Scheme.function_field (X : algebraic_geometry.Scheme) [irreducible_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :
CommRing

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.

source
@[reducible]
noncomputable def algebraic_geometry.Scheme.germ_to_function_field (X : algebraic_geometry.Scheme) [irreducible_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) [h : nonempty ↥U] :
X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U) ⟶ X.function_field

The restriction map from a component to the function field.

source
@[protected, instance]
noncomputable def algebraic_geometry.Scheme.function_field.algebra (X : algebraic_geometry.Scheme) [irreducible_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) [nonempty ↥U] :
algebra ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U)) ↥(X.function_field)
Equations
source
@[protected, instance]
noncomputable def algebraic_geometry.Scheme.function_field.field (X : algebraic_geometry.Scheme) [algebraic_geometry.is_integral X] :
field ↥(X.function_field)
Equations
source
theorem algebraic_geometry.germ_injective_of_is_integral (X : algebraic_geometry.Scheme) [algebraic_geometry.is_integral X] {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (x : ↥U) :
function.injective ⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.germ x)
source
theorem algebraic_geometry.Scheme.germ_to_function_field_injective (X : algebraic_geometry.Scheme) [algebraic_geometry.is_integral X] (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) [nonempty ↥U] :
function.injective ⇑(X.germ_to_function_field U)
source
theorem algebraic_geometry.generic_point_eq_of_is_open_immersion {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [H : algebraic_geometry.is_open_immersion f] [hX : irreducible_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] [irreducible_space ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :
⇑(f.val.base) (generic_point ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) = generic_point ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)
source
@[protected, instance]
noncomputable def algebraic_geometry.stalk_function_field_algebra (X : algebraic_geometry.Scheme) [irreducible_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :
algebra ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.stalk x) ↥(X.function_field)
Equations
source
@[protected, instance]
def algebraic_geometry.function_field_is_scalar_tower (X : algebraic_geometry.Scheme) [irreducible_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (x : ↥U) [nonempty ↥U] :
is_scalar_tower ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U)) ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.stalk ↑x) ↥(X.function_field)
source
@[protected, instance]
noncomputable def algebraic_geometry.function_field.algebra (R : CommRing) [is_domain ↥R] :
algebra ↥R ↥((algebraic_geometry.Scheme.Spec.obj (opposite.op R)).function_field)
Equations
source
@[simp]
theorem algebraic_geometry.generic_point_eq_bot_of_affine (R : CommRing) [is_domain ↥R] :
generic_point ↥((algebraic_geometry.Scheme.Spec.obj (opposite.op R)).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) = {as_ideal := 0, is_prime := _}
source
@[protected, instance]
def algebraic_geometry.function_field_is_fraction_ring_of_affine (R : CommRing) [is_domain ↥R] :
is_fraction_ring ↥R ↥((algebraic_geometry.Scheme.Spec.obj (opposite.op R)).function_field)
source
@[protected, instance]
def algebraic_geometry.Scheme.restrict.is_integral {X : algebraic_geometry.Scheme} [algebraic_geometry.is_integral X] {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} [hU : nonempty ↥U] :
algebraic_geometry.is_integral (X.restrict _)
source
theorem algebraic_geometry.is_affine_open.prime_ideal_of_generic_point {X : algebraic_geometry.Scheme} [algebraic_geometry.is_integral X] {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) [h : nonempty ↥U] :
hU.prime_ideal_of ⟨generic_point ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) _, _⟩ = generic_point ↥((algebraic_geometry.Scheme.Spec.obj (opposite.op (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U)))).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)
source
theorem algebraic_geometry.function_field_is_fraction_ring_of_is_affine_open (X : algebraic_geometry.Scheme) [algebraic_geometry.is_integral X] (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hU : algebraic_geometry.is_affine_open U) [hU' : nonempty ↥U] :
is_fraction_ring ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U)) ↥(X.function_field)
source
@[protected, instance]
def algebraic_geometry.obj.is_affine (X : algebraic_geometry.Scheme) (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :
algebraic_geometry.is_affine (X.affine_cover.obj x)
source
@[protected, instance]
def algebraic_geometry.Scheme.function_field.is_fraction_ring (X : algebraic_geometry.Scheme) [h : algebraic_geometry.is_integral X] (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :
is_fraction_ring ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.stalk x) ↥(X.function_field)