Documentation

Mathlib.AlgebraicGeometry.FunctionField

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

AlgebraicGeometry.instAlgebraαCommRingObjOppositeOpensTopologicalSpaceCarrierCommRingCatPresheafOpOpensFunctionFieldOfNonemptyToScheme X U = RingHom.toAlgebra (X.germToFunctionField U)

noncomputable instance AlgebraicGeometry.instFieldαCommRingFunctionField (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] :

Field ↑X.functionField

Equations

AlgebraicGeometry.instFieldαCommRingFunctionField X = Field.ofIsUnitOrEqZero ⋯

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 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] :

AlgebraicGeometry.IsIntegral ↑U

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

⋯ = ⋯