Algebra structures induced by a scheme over an affine base

For a scheme X over Spec k, this file records the canonical k-algebra structures on the function field of an integral X, on its stalks, and on its residue fields. It also proves that the base, stalk, and function-field algebra structures form a scalar tower.

Main definitions and results

• Scheme.baseRingToFunctionField: the canonical map from the base ring to the function field.
• Scheme.globalRationalFunctionsEquivFunctionField: global rational functions as a module over the base ring.
• Scheme.baseRingToStalk: the canonical map from the base ring to a stalk.
• Scheme.fromSpecStalk_comp_over: the spectrum of a stalk maps to X over the affine base.
• Scheme.baseStalkResidueFieldIsScalarTower: compatibility of the base, stalk, and residue-field algebra structures.
• Scheme.baseStalkFunctionFieldIsScalarTower: compatibility of the base, stalk, and function-field algebra structures.
• Scheme.finrank_residueField_eq_residueDegree: over a field, the dimension of a residue field is the residue degree of the structure morphism.

noncomputable def AlgebraicGeometry.Scheme.baseRingToFunctionField (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] [IsIntegral X] : k →+* ↑X.functionField

The canonical map from the base ring of a scheme to its function field. It is the pullback to global sections followed by the inclusion of global functions into rational functions.

Equations

• AlgebraicGeometry.Scheme.baseRingToFunctionField k X = (CommRingCat.Hom.hom (X.germToFunctionField ⊤)).comp (AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections k X)

@[simp]

theorem AlgebraicGeometry.Scheme.baseRingToFunctionField_apply (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] [IsIntegral X] (c : k) : (baseRingToFunctionField k X) c = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) ((Modules.baseRingToGlobalSections k X) c)

The base-ring map to the function field sends a scalar to the rational function induced by the corresponding global function.

theorem AlgebraicGeometry.Scheme.baseRingToFunctionField_eq_comp_appLE (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] [IsIntegral X] (U : X.Opens) [Nonempty ↥↑U] : baseRingToFunctionField k X = (CommRingCat.Hom.hom (X.germToFunctionField U)).comp (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso ↧k).inv (Hom.appLE (X ↘ Spec ↧k) ⊤ U ⋯)))

The base-ring map to the function field factors through the sections over any nonempty open U: pull functions on Spec k back to Γ(X, U) along the structure morphism, then pass to rational functions.

@[instance_reducible, instance 900]

noncomputable instance AlgebraicGeometry.Scheme.functionFieldBaseAlgebra (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] [IsIntegral X] : Algebra k ↑X.functionField

The function field of an integral scheme over Spec k is canonically a k-algebra.

Equations

• AlgebraicGeometry.Scheme.functionFieldBaseAlgebra k X = (AlgebraicGeometry.Scheme.baseRingToFunctionField k X).toAlgebra

noncomputable def AlgebraicGeometry.Scheme.baseRingToStalk (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] (x : ↥X) : k →+* ↑(X.presheaf.stalk x)

The canonical map from the base ring of a scheme to its stalk at x.

Equations

• AlgebraicGeometry.Scheme.baseRingToStalk k X x = (CommRingCat.Hom.hom (X.presheaf.germ ⊤ x trivial)).comp (AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections k X)

@[simp]

theorem AlgebraicGeometry.Scheme.baseRingToStalk_apply (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] (x : ↥X) (c : k) : (baseRingToStalk k X x) c = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ⊤ x trivial)) ((Modules.baseRingToGlobalSections k X) c)

The image of a base-ring element in a stalk is the germ of the corresponding global function.

@[instance_reducible, instance 900]

noncomputable instance AlgebraicGeometry.Scheme.stalkBaseAlgebra (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] (x : ↥X) : Algebra k ↑(X.presheaf.stalk x)

Every stalk of a scheme over Spec k is canonically a k-algebra.

Equations

• AlgebraicGeometry.Scheme.stalkBaseAlgebra k X x = (AlgebraicGeometry.Scheme.baseRingToStalk k X x).toAlgebra

@[instance_reducible, instance 900]

noncomputable instance AlgebraicGeometry.Scheme.residueFieldBaseAlgebra (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] (x : ↥X) : Algebra k ↑(X.residueField x)

The residue field at a point of a scheme over Spec k is canonically a k-algebra.

Equations

• AlgebraicGeometry.Scheme.residueFieldBaseAlgebra k X x = ((CommRingCat.Hom.hom (X.residue x)).comp (AlgebraicGeometry.Scheme.baseRingToStalk k X x)).toAlgebra

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.residueFieldStalkAlgebra (X : Scheme) (x : ↥X) : Algebra ↑(X.presheaf.stalk x) ↑(X.residueField x)

The residue field at a point is canonically an algebra over its stalk.

Equations

• X.residueFieldStalkAlgebra x = (CommRingCat.Hom.hom (X.residue x)).toAlgebra

@[simp]

theorem AlgebraicGeometry.Scheme.algebraMap_functionField_eq_baseRingToFunctionField (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] [IsIntegral X] : algebraMap k ↑X.functionField = baseRingToFunctionField k X

The algebra map to the function field is the canonical composite from the base ring.

@[simp]

theorem AlgebraicGeometry.Scheme.algebraMap_stalk_eq_baseRingToStalk (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] (x : ↥X) : algebraMap k ↑(X.presheaf.stalk x) = baseRingToStalk k X x

The algebra map to a stalk is the canonical composite from the base ring.

@[simp]

theorem AlgebraicGeometry.Scheme.algebraMap_residueField_eq_residue_comp_baseRingToStalk (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] (x : ↥X) : algebraMap k ↑(X.residueField x) = (CommRingCat.Hom.hom (X.residue x)).comp (baseRingToStalk k X x)

The algebra map to a residue field is the residue of the canonical composite from the base ring.

@[simp]

theorem AlgebraicGeometry.Scheme.algebraMap_stalk_residueField_eq_residue (X : Scheme) (x : ↥X) : algebraMap ↑(X.presheaf.stalk x) ↑(X.residueField x) = CommRingCat.Hom.hom (X.residue x)

The algebra map from a stalk to its residue field is the residue map.

instance AlgebraicGeometry.Scheme.baseStalkResidueFieldIsScalarTower (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] (x : ↥X) : IsScalarTower k ↑(X.presheaf.stalk x) ↑(X.residueField x)

The canonical maps from the base ring through a stalk to its residue field form a scalar tower.

theorem AlgebraicGeometry.Scheme.residue_baseRingToStalk (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] (x : ↥X) (c : k) : (CategoryTheory.ConcreteCategory.hom (X.residue x)) ((baseRingToStalk k X x) c) = (CategoryTheory.ConcreteCategory.hom (X.Γevaluation x)) ((Modules.baseRingToGlobalSections k X) c)

The residue at x of the image of a base ring element in the stalk is the evaluation at x of the corresponding global function: both are the germ at x followed by the residue map.

instance AlgebraicGeometry.Scheme.baseStalkFunctionFieldIsScalarTower (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] [IsIntegral X] (x : ↥X) : IsScalarTower k ↑(X.presheaf.stalk x) ↑X.functionField

The canonical maps from the base ring through a stalk to the function field form a scalar tower.

theorem AlgebraicGeometry.Scheme.fromSpecStalk_comp_over (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] (x : ↥X) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) (X ↘ Spec ↧k) = Spec.map (CommRingCat.ofHom (algebraMap k ↑(X.presheaf.stalk x)))

The canonical morphism from the spectrum of a stalk to a scheme over Spec k is a morphism over Spec k; on rings, its composite with the structure morphism is the algebra map from k to the stalk.

theorem AlgebraicGeometry.Scheme.fromSpecStalk_genericPoint_comp_over (k : Type u) [CommRing k] (X : Scheme) [X.Over (Spec ↧k)] [IsIntegral X] : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (X ↘ Spec ↧k) = Spec.map (CommRingCat.ofHom (algebraMap k ↑X.functionField))

At the generic point of an integral scheme, fromSpecStalk is a morphism from the spectrum of the function field over the affine base.

noncomputable def AlgebraicGeometry.Scheme.globalRationalFunctionsEquivFunctionField {k : Type u} [CommRing k] {X : Scheme} [X.Over (Spec ↧k)] [IsIntegral X] : ↑((TauCeti.AlgebraicGeometry.Scheme.rationalFunctions X).presheaf.obj (Opposite.op ⊤)) ≃ₗ[k] ↑X.functionField

Global rational functions are the function field, also as modules over the base ring.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.globalRationalFunctionsEquivFunctionField_apply {k : Type u} [CommRing k] {X : Scheme} [X.Over (Spec ↧k)] [IsIntegral X] (f : ↑((TauCeti.AlgebraicGeometry.Scheme.rationalFunctions X).presheaf.obj (Opposite.op ⊤))) : globalRationalFunctionsEquivFunctionField f = (TauCeti.AlgebraicGeometry.Scheme.rationalFunctionsEquiv ⊤) f

The linear equivalence sends a global rational function to its value in the function field.

@[simp]

theorem AlgebraicGeometry.Scheme.finrank_residueField_eq_residueDegree (k : Type u) [Field k] (X : Scheme) [X.Over (Spec ↧k)] (x : ↥X) : Module.finrank k ↑(X.residueField x) = Hom.residueDegree (X ↘ Spec ↧k) x

Over a field, the dimension of a scheme-theoretic residue field is the residue degree of the structure morphism.