AlgebraicGeometry.exists_ringHom_functionField_germ_eq_of_base_genericPoint_eq
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_ringHom_functionField_germ_eq_of_base_genericPoint_eq
open CategoryTheory AlgebraicGeometry
universe uLean source · statement
theorem _root_.AlgebraicGeometry.exists_ringHom_functionField_germ_eq_of_base_genericPoint_eq
{X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y] (f : Y ⟶ X)
(hf : f.base (genericPoint Y) = genericPoint X) :
∃ δ : ↑X.functionField →+* ↑Y.functionField,
∀ (U : X.Opens) (hU : genericPoint X ∈ U) (hU' : genericPoint Y ∈ f ⁻¹ᵁ U)
(sec : X.presheaf.obj (Opposite.op U)),
δ ((X.presheaf.germ U (genericPoint X) hU).hom sec) =
(Y.presheaf.germ (f ⁻¹ᵁ U) (genericPoint Y) hU').hom ((f.app U).hom sec)