CurveModel_apply_genericPoint_eq_and_nonempty_algEquiv_functionField_of_isIso_stalkMap.lean

theorem isIso_stalkSpecializes_of_eq {X : TopCat.{u}} (P : TopCat.Presheaf CommRingCat.{u} X)
    {x y : X} (e : x = y) (h : x ⤳ y) : IsIso (P.stalkSpecializes h)

theorem eq_genericPoint_of_isField {C : Scheme.{u}} [IsIntegral C] (x : C)
    (hfield : IsField (C.presheaf.stalk x)) : x = genericPoint C

theorem apply_genericPoint_eq_and_nonempty_algEquiv_functionField_of_isIso_stalkMap
    (k : Type u) [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) [IsIntegral C]
    {F : Type v} [Field F] [Algebra k F] (M : AlgebraicCurve.CurveModel k F)
    (ν : M.C ⟶ C) (hν : ν ≫ c = M.toBase)
    (hbir : IsIso (ν.stalkMap (genericPoint M.C))) :
    letI := (AlgebraicCurve.baseToFunctionField c).toAlgebra
    ν.base (genericPoint M.C) = genericPoint C ∧ Nonempty (F ≃ₐ[k] C.functionField) := by
  let := (AlgebraicCurve.baseToFunctionField c).toAlgebra
  have hx : ν.base (genericPoint M.C) = genericPoint C := by
    apply eq_genericPoint_of_isField
    exact MulEquiv.isField (Field.toIsField M.C.functionField)
      (asIso (ν.stalkMap (genericPoint M.C))).commRingCatIsoToRingEquiv.toMulEquiv
  refine ⟨hx, ⟨?_⟩⟩
  have hsp : genericPoint C ⤳ ν.base (genericPoint M.C) := (genericPoint_spec C).specializes trivial
  haveI := isIso_stalkSpecializes_of_eq C.presheaf hx.symm hsp
  let e : F ≃+* C.functionField :=
    M.ffEquiv.trans (((asIso (ν.stalkMap (genericPoint M.C))).symm ≪≫
      asIso (C.presheaf.stalkSpecializes hsp)).commRingCatIsoToRingEquiv)
  refine AlgEquiv.ofRingEquiv (f := e) fun a => ?_
  change C.presheaf.stalkSpecializes hsp (inv (ν.stalkMap (genericPoint M.C))
    (M.ffEquiv (algebraMap k F a))) = baseToFunctionField c a
  rw [M.ffEquiv_algebraMap]
  have h1 : baseToFunctionField M.toBase a = ν.stalkMap (genericPoint M.C)
      (C.presheaf.germ ⊤ (ν.base (genericPoint M.C)) trivial
        (c.appTop ((Scheme.ΓSpecIso (CommRingCat.of k)).inv a))) := by
    refine Eq.trans ?_ (Scheme.Hom.germ_stalkMap_apply ν ⊤ (genericPoint M.C)
      (show ν (genericPoint M.C) ∈ (⊤ : C.Opens) from Set.mem_univ _)
      (c.appTop ((Scheme.ΓSpecIso (CommRingCat.of k)).inv a))).symm
    change (M.C.presheaf.germ ⊤ (genericPoint M.C) trivial)
      (M.toBase.appTop ((Scheme.ΓSpecIso (CommRingCat.of k)).inv a)) = _
    rw [← hν, Scheme.Hom.comp_appTop]
    rfl
  rw [h1, IsIso.hom_inv_id_apply]
  exact TopCat.Presheaf.germ_stalkSpecializes_apply (U := ⊤)
    (y := ν.base (genericPoint M.C)) (x := genericPoint C) C.presheaf (by trivial) hsp _