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

• AlgebraicGeometry.Scheme.functionField: The function field of an integral scheme.
• AlgebraicGeometry.Scheme.germToFunctionField: The canonical map from a component into the function field. This map is injective.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.functionField (X : Scheme) [IrreducibleSpace ↥X] : CommRingCat

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)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.germToFunctionField (X : Scheme) [IrreducibleSpace ↥X] (U : X.Opens) [h : Nonempty ↥↑U] : 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) ⋯

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensFunctionFieldOfNonemptyToScheme (X : Scheme) [IrreducibleSpace ↥X] (U : X.Opens) [Nonempty ↥↑U] : Algebra ↑(X.presheaf.obj (Opposite.op U)) ↑X.functionField

Equations

• AlgebraicGeometry.instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensFunctionFieldOfNonemptyToScheme X U = (CommRingCat.Hom.hom (X.germToFunctionField U)).toAlgebra

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.instFieldCarrierFunctionField (X : Scheme) [IsIntegral X] : Field ↑X.functionField

Equations

• AlgebraicGeometry.instFieldCarrierFunctionField X = ⋯.toField

theorem AlgebraicGeometry.germ_injective_of_isIntegral (X : Scheme) [IsIntegral X] {U : X.Opens} (x : ↥X) (hx : x ∈ U) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx))

theorem AlgebraicGeometry.Scheme.germToFunctionField_injective (X : Scheme) [IsIntegral X] (U : X.Opens) [Nonempty ↥↑U] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U))

theorem AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] [hX : IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] : f (genericPoint ↥X) = genericPoint ↥Y

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.stalkFunctionFieldAlgebra (X : Scheme) [IrreducibleSpace ↥X] (x : ↥X) : Algebra ↑(X.presheaf.stalk x) ↑X.functionField

Equations

• AlgebraicGeometry.stalkFunctionFieldAlgebra X x = (CommRingCat.Hom.hom (X.presheaf.stalkSpecializes ⋯)).toAlgebra

instance AlgebraicGeometry.functionField_isScalarTower (X : Scheme) [IrreducibleSpace ↥X] (U : X.Opens) (x : ↥U) [Nonempty ↥↑U] : IsScalarTower ↑(X.presheaf.obj (Opposite.op U)) ↑(X.presheaf.stalk ↑x) ↑X.functionField

@[simp]

theorem AlgebraicGeometry.Scheme.algebraMap_germ_eq_germToFunctionField (X : Scheme) [IrreducibleSpace ↥X] {U : X.Opens} [Nonempty ↥↑U] {x : ↥X} (hx : x ∈ U) (f : ↑(X.presheaf.obj (Opposite.op U))) : (algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) f

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec (R : CommRingCat) [IsDomain ↑R] : Algebra ↑R ↑(Spec R).functionField

Equations

• AlgebraicGeometry.instAlgebraCarrierFunctionFieldSpec R = (CommRingCat.Hom.hom (AlgebraicGeometry.StructureSheaf.toStalk (↑R) (genericPoint ↥(AlgebraicGeometry.Spec R)))).toAlgebra

@[simp]

theorem AlgebraicGeometry.genericPoint_eq_bot_of_affine (R : CommRingCat) [IsDomain ↑R] : genericPoint ↥(Spec R) = ⊥

instance AlgebraicGeometry.functionField_isFractionRing_of_affine (R : CommRingCat) [IsDomain ↑R] : IsFractionRing ↑R ↑(Spec R).functionField

instance AlgebraicGeometry.instIsIntegralToSchemeOfNonemptyCarrierCarrierCommRingCat {X : Scheme} [IsIntegral X] {U : X.Opens} [Nonempty ↥↑U] : IsIntegral ↑U

theorem AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint {X : Scheme} [IsIntegral X] {U : X.Opens} (hU : IsAffineOpen U) [h : Nonempty ↥↑U] : hU.primeIdealOf ⟨genericPoint ↥X, ⋯⟩ = genericPoint ↥(Spec (X.presheaf.obj (Opposite.op U)))

theorem AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen (X : Scheme) [IsIntegral X] (U : X.Opens) (hU : IsAffineOpen U) [Nonempty ↥↑U] : IsFractionRing ↑(X.presheaf.obj (Opposite.op U)) ↑X.functionField

instance AlgebraicGeometry.instIsAffineXSchemeAffineCover (X : Scheme) (x : ↥X) : IsAffine (X.affineCover.X x)

instance AlgebraicGeometry.instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField (X : Scheme) [IsIntegral X] (x : ↥X) : IsFractionRing ↑(X.presheaf.stalk x) ↑X.functionField

instance AlgebraicGeometry.instIsDomainCarrierStalkCommRingCatPresheafOfIsIntegral (X : Scheme) [IsIntegral X] {x : ↥X} : IsDomain ↑(X.presheaf.stalk x)

theorem AlgebraicGeometry.exists_isUnit_germ_eq (X : Scheme) [IsIntegral X] (f : ↑X.functionField) (hf : f ≠ 0) : ∃ U ∈ X.affineOpens, ∃ (f' : ↑(X.presheaf.obj (Opposite.op U))) (x : Nonempty ↥↑U), (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'

For f an element of the function field of X, there exists some open set U ⊆ X such that f is a unit in Γ(X, U).