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.
• Algebraic_geometry.germToFunctionField: The canonical map from a component into the function field. This map is injective.

@[inline, reducible]

noncomputable abbrev AlgebraicGeometry.Scheme.functionField (X : AlgebraicGeometry.Scheme) [IrreducibleSpace ↑↑X.toPresheafedSpace] : 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.

@[inline, reducible]

noncomputable abbrev AlgebraicGeometry.Scheme.germToFunctionField (X : AlgebraicGeometry.Scheme) [IrreducibleSpace ↑↑X.toPresheafedSpace] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) [h : Nonempty { x // x ∈ U }] : X.presheaf.obj (Opposite.op U) ⟶ AlgebraicGeometry.Scheme.functionField X

The restriction map from a component to the function field.

noncomputable instance AlgebraicGeometry.instAlgebraαCommRingObjOppositeOpensTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceTopologicalSpace_coeToQuiverToCategoryStructOppositeSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensToQuiverToCategoryStructToPrefunctorPresheafOpFunctionFieldToCommSemiringInstCommRingαToSemiring (X : AlgebraicGeometry.Scheme) [IrreducibleSpace ↑↑X.toPresheafedSpace] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) [Nonempty { x // x ∈ U }] : Algebra ↑(X.presheaf.obj (Opposite.op U)) ↑(AlgebraicGeometry.Scheme.functionField X)

noncomputable instance AlgebraicGeometry.instFieldαCommRingFunctionFieldIs_irreducible_of_isIntegral (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] : Field ↑(AlgebraicGeometry.Scheme.functionField X)

theorem AlgebraicGeometry.germ_injective_of_isIntegral (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (x : { x // x ∈ U }) : Function.Injective ↑(TopCat.Presheaf.germ X.presheaf x)

theorem AlgebraicGeometry.Scheme.germToFunctionField_injective (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) [Nonempty { x // x ∈ U }] : Function.Injective ↑(AlgebraicGeometry.Scheme.germToFunctionField X 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.val.base (genericPoint ↑↑X.toPresheafedSpace) = genericPoint ↑↑Y.toPresheafedSpace

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

instance AlgebraicGeometry.functionField_isScalarTower (X : AlgebraicGeometry.Scheme) [IrreducibleSpace ↑↑X.toPresheafedSpace] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (x : { x // x ∈ U }) [Nonempty { x // x ∈ U }] : IsScalarTower ↑(X.presheaf.obj (Opposite.op U)) ↑(TopCat.Presheaf.stalk X.presheaf ↑x) ↑(AlgebraicGeometry.Scheme.functionField X)

noncomputable instance AlgebraicGeometry.instAlgebraαCommRingFunctionFieldObjOppositeCommRingCatToQuiverToCategoryStructOppositeInstCommRingCatLargeCategorySchemeInstCategorySchemeToPrefunctorSpecOpInstIrreducibleSpaceαTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceObjOppositeToQuiverToCategoryStructOppositeSchemeInstCategorySchemeToPrefunctorSpecOpInstTopologicalSpaceαCarrierToPresheafedSpaceToCommSemiringInstCommRingαToSemiringToDivisionSemiringToSemifieldInstFieldαCommRingFunctionFieldIs_irreducible_of_isIntegralInstIsIntegralObjOppositeCommRingCatToQuiverToCategoryStructOppositeInstCommRingCatLargeCategorySchemeInstCategorySchemeToPrefunctorSpecOp (R : CommRingCat) [IsDomain ↑R] : Algebra ↑R ↑(AlgebraicGeometry.Scheme.functionField (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)))

@[simp]

theorem AlgebraicGeometry.genericPoint_eq_bot_of_affine (R : CommRingCat) [IsDomain ↑R] : genericPoint ↑↑(AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)).toPresheafedSpace = { asIdeal := 0, IsPrime := (_ : Ideal.IsPrime ⊥) }

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

instance AlgebraicGeometry.instIsIntegralRestrictObjOpensαTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceTopologicalSpace_coeToQuiverToCategoryStructSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensTopCatToQuiverToCategoryStructInstTopCatLargeCategoryToPrefunctorToTopCatInclusionOpenEmbedding {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} [hU : Nonempty { x // x ∈ U }] : AlgebraicGeometry.IsIntegral (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U)))

theorem AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) [h : Nonempty { x // x ∈ U }] : AlgebraicGeometry.IsAffineOpen.primeIdealOf hU { val := genericPoint ↑↑X.toPresheafedSpace, property := (_ : genericPoint ↑↑X.toPresheafedSpace ∈ ↑U) } = genericPoint ↑↑(AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.obj (Opposite.op U)))).toPresheafedSpace

theorem AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hU : AlgebraicGeometry.IsAffineOpen U) [hU' : Nonempty { x // x ∈ U }] : IsFractionRing ↑(X.presheaf.obj (Opposite.op U)) ↑(AlgebraicGeometry.Scheme.functionField X)

instance AlgebraicGeometry.instIsAffineObjAffineCover (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj (AlgebraicGeometry.Scheme.affineCover X) x)

instance AlgebraicGeometry.instIsFractionRingαCommRingStalkCommRingCatInstCommRingCatLargeCategoryHasColimits_commRingCatCarrierToPresheafedSpaceToSheafedSpaceToLocallyRingedSpacePresheafInstCommRingαFunctionFieldIs_irreducible_of_isIntegralStalkFunctionFieldAlgebra (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (x : ↑↑X.toPresheafedSpace) : IsFractionRing ↑(TopCat.Presheaf.stalk X.presheaf x) ↑(AlgebraicGeometry.Scheme.functionField X)