AlgebraicGeometry.functionField_constantExtension_map_constants
The actual function-field map characterized by germs sends original constants through the specified extension of the ground field.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicCurve AlgebraicGeometry.SmoothProperCurve
namespace AlgebraicGeometryLean source · statement
theorem functionField_constantExtension_map_constants
{K : Type} [Field K] (K' : Type) [Field K'] [Algebra K K']
{X : Scheme} [IsIntegral X] (c : X ⟶ Spec (.of K))
[IsIntegral (pullback c (specMap K K'))]
(φ : X.functionField →+* (pullback c (specMap K K')).functionField)
(hsq : ∀ (U : X.Opens) [Nonempty U]
[Nonempty ((pullback.fst c (specMap K K')) ⁻¹ᵁ U)] (s : Γ(X, U)),
(pullback c (specMap K K')).germToFunctionField
((pullback.fst c (specMap K K')) ⁻¹ᵁ U)
(((pullback.fst c (specMap K K')).app U).hom s) =
φ (X.germToFunctionField U s))
(a : K) :
φ (baseToFunctionField c a) =
baseToFunctionField (pullback.snd c (specMap K K')) (algebraMap K K' a)