AlgebraicCurve.CurveModel.exists_ringHom_functionField_ffEquiv_symm_stalkMap_eq_of_isIso_pullback
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurve.CurveModel
universe u v
open _root_.AlgebraicCurves.Models.Proofs in
open CurveModel_exists_ringHom_functionField_ffEquiv_symm_stalkMap_eq_of_isIso_pullback in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry inLean source · statement
theorem exists_ringHom_functionField_ffEquiv_symm_stalkMap_eq_of_isIso_pullback
{R : Type u} [CommRing R] {K : Type u} [Field K] [Algebra R K]
(hinj : Function.Injective (algebraMap R K))
{L : Type v} [Field L] [Algebra K L] (M : AlgebraicCurve.CurveModel K L)
{X : Scheme.{u}} [IsIntegral X] (c : X ⟶ Spec (.of R))
(e₀ : M.C ⟶ pullback c (Spec.map (CommRingCat.ofHom (algebraMap R K)))) [IsIso e₀]
(he₀ : e₀ ≫ pullback.snd c _ = M.toBase) :
∃ Θ : X.functionField →+* L,
(∀ (P : X) (hgenP : (e₀ ≫ pullback.fst c _).base (genericPoint M.C) ⤳ P) (z :
X.presheaf.stalk P),
M.ffEquiv.symm ((Scheme.Hom.stalkMap (e₀ ≫ pullback.fst c _) (genericPoint M.C)).hom
((X.presheaf.stalkSpecializes hgenP).hom z)) = Θ (algebraMap (X.presheaf.stalk P)
X.functionField z)) ∧
(∀ (x : M.C) (w : X.presheaf.stalk ((e₀ ≫ pullback.fst c _).base x)),
M.ffEquiv.symm (algebraMap (M.C.presheaf.stalk x) M.C.functionField
((Scheme.Hom.stalkMap (e₀ ≫ pullback.fst c _) x).hom w)) =
Θ (algebraMap (X.presheaf.stalk ((e₀ ≫ pullback.fst c _).base x)) X.functionField w)) ∧
(∀ (P : X) (r : R), Θ (algebraMap (X.presheaf.stalk P) X.functionField
((X.presheaf.germ ⊤ P trivial).hom (c.appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of
R)).inv.hom r)))) =
algebraMap K L (algebraMap R K r)) ∧
(IsIso (Scheme.Hom.stalkMap (e₀ ≫ pullback.fst c _) (genericPoint M.C)) → Function.Bijective
Θ)