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 : AlgebraicGeometry.Scheme)
[IrreducibleSpace ↑↑X.toPresheafedSpace]
:
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.toPresheafedSpace)
Instances For
@[reducible, inline]
noncomputable abbrev
AlgebraicGeometry.Scheme.germToFunctionField
(X : AlgebraicGeometry.Scheme)
[IrreducibleSpace ↑↑X.toPresheafedSpace]
(U : X.Opens)
[h : Nonempty ↑↑(↑U).toPresheafedSpace]
:
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.toPresheafedSpace) ⋯
Instances For
noncomputable instance
AlgebraicGeometry.instAlgebraαCommRingObjOppositeOpensTopologicalSpaceCarrierCommRingCatPresheafOpOpensFunctionFieldOfNonemptyToScheme
(X : AlgebraicGeometry.Scheme)
[IrreducibleSpace ↑↑X.toPresheafedSpace]
(U : X.Opens)
[Nonempty ↑↑(↑U).toPresheafedSpace]
:
Algebra ↑(X.presheaf.obj (Opposite.op U)) ↑X.functionField
Equations
noncomputable instance
AlgebraicGeometry.instFieldαCommRingFunctionField
(X : AlgebraicGeometry.Scheme)
[AlgebraicGeometry.IsIntegral X]
:
Field ↑X.functionField
theorem
AlgebraicGeometry.germ_injective_of_isIntegral
(X : AlgebraicGeometry.Scheme)
[AlgebraicGeometry.IsIntegral X]
{U : X.Opens}
(x : ↑↑X.toPresheafedSpace)
(hx : x ∈ U)
:
Function.Injective ⇑(X.presheaf.germ U x hx)
theorem
AlgebraicGeometry.Scheme.germToFunctionField_injective
(X : AlgebraicGeometry.Scheme)
[AlgebraicGeometry.IsIntegral X]
(U : X.Opens)
[Nonempty ↑↑(↑U).toPresheafedSpace]
:
Function.Injective ⇑(X.germToFunctionField U)
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.base (genericPoint ↑↑X.toPresheafedSpace) = genericPoint ↑↑Y.toPresheafedSpace
noncomputable instance
AlgebraicGeometry.stalkFunctionFieldAlgebra
(X : AlgebraicGeometry.Scheme)
[IrreducibleSpace ↑↑X.toPresheafedSpace]
(x : ↑↑X.toPresheafedSpace)
:
Algebra ↑(X.presheaf.stalk x) ↑X.functionField
Equations
- AlgebraicGeometry.stalkFunctionFieldAlgebra X x = RingHom.toAlgebra (X.presheaf.stalkSpecializes ⋯)
instance
AlgebraicGeometry.functionField_isScalarTower
(X : AlgebraicGeometry.Scheme)
[IrreducibleSpace ↑↑X.toPresheafedSpace]
(U : X.Opens)
(x : ↥U)
[Nonempty ↑↑(↑U).toPresheafedSpace]
:
IsScalarTower ↑(X.presheaf.obj (Opposite.op U)) ↑(X.presheaf.stalk ↑x) ↑X.functionField
Equations
- ⋯ = ⋯
noncomputable instance
AlgebraicGeometry.instAlgebraαCommRingFunctionFieldSpec
(R : CommRingCat)
[IsDomain ↑R]
:
Algebra ↑R ↑(AlgebraicGeometry.Spec R).functionField
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
AlgebraicGeometry.genericPoint_eq_bot_of_affine
(R : CommRingCat)
[IsDomain ↑R]
:
genericPoint ↑↑(AlgebraicGeometry.Spec R).toPresheafedSpace = ⊥
instance
AlgebraicGeometry.functionField_isFractionRing_of_affine
(R : CommRingCat)
[IsDomain ↑R]
:
IsFractionRing ↑R ↑(AlgebraicGeometry.Spec R).functionField
Equations
- ⋯ = ⋯
instance
AlgebraicGeometry.instIsIntegralToSchemeOfNonemptyαTopologicalSpaceCarrierCommRingCat
{X : AlgebraicGeometry.Scheme}
[AlgebraicGeometry.IsIntegral X]
{U : X.Opens}
[Nonempty ↑↑(↑U).toPresheafedSpace]
:
Equations
- ⋯ = ⋯
theorem
AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint
{X : AlgebraicGeometry.Scheme}
[AlgebraicGeometry.IsIntegral X]
{U : X.Opens}
(hU : AlgebraicGeometry.IsAffineOpen U)
[h : Nonempty ↑↑(↑U).toPresheafedSpace]
:
hU.primeIdealOf ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ = genericPoint ↑↑(AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).toPresheafedSpace
theorem
AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen
(X : AlgebraicGeometry.Scheme)
[AlgebraicGeometry.IsIntegral X]
(U : X.Opens)
(hU : AlgebraicGeometry.IsAffineOpen U)
[Nonempty ↑↑(↑U).toPresheafedSpace]
:
IsFractionRing ↑(X.presheaf.obj (Opposite.op U)) ↑X.functionField
instance
AlgebraicGeometry.instIsAffineObjIsOpenImmersionAffineCover
(X : AlgebraicGeometry.Scheme)
(x : ↑↑X.toPresheafedSpace)
:
AlgebraicGeometry.IsAffine (X.affineCover.obj x)
Equations
- ⋯ = ⋯
instance
AlgebraicGeometry.instIsFractionRingαCommRingStalkCommRingCatPresheafFunctionField
(X : AlgebraicGeometry.Scheme)
[AlgebraicGeometry.IsIntegral X]
(x : ↑↑X.toPresheafedSpace)
:
IsFractionRing ↑(X.presheaf.stalk x) ↑X.functionField
Equations
- ⋯ = ⋯