SmoothProperCurve_exists_curveModel_iso_pullback_germToFunctionField_eq_of_isAlgClosed.lean

theorem exists_curveModel_iso_pullback_germToFunctionField_eq_of_isAlgClosed
    (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (k : Type u) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R)) :
    letI : Algebra k (pullback c s).functionField := (baseToFunctionField (pullback.snd c
      s)).toAlgebra
    ∃ (_ : IsCurveOver k (pullback c s).functionField) (_ : Algebra.EssFiniteType k (pullback c
      s).functionField)
      (M : CurveModel k (pullback c s).functionField) (e : M.C ≅ pullback c s),
      e.hom ≫ pullback.snd c s = M.toBase ∧
      ∀ (U : (pullback c s).Opens) [Nonempty (Scheme.Opens.toScheme U)] [Nonempty
        (Scheme.Opens.toScheme (e.hom ⁻¹ᵁ U))]
        (t : Γ(pullback c s, U)),
        M.ffEquiv.symm (M.C.germToFunctionField (e.hom ⁻¹ᵁ U) ((e.hom.app U).hom t)) =
          (pullback c s).germToFunctionField U t := by
  classical
  let Cs : Scheme.{u} := pullback c s
  let cs : Cs ⟶ Spec (CommRingCat.of k) := pullback.snd c s
  have : IsIntegral Cs := SmoothProperCurve.isIntegral_pullback_Spec_field R c s
  have : IsProper cs := inferInstance
  have : SmoothOfRelativeDimension 1 cs := inferInstance
  let alg : Algebra k Cs.functionField := (baseToFunctionField cs).toAlgebra
  have hco : IsCurveOver k Cs.functionField :=
    isCurveOver_of_isIntegral_of_smoothOfRelativeDimension_one cs (RingEquiv.refl _) (fun _ => rfl)
  have hft : Algebra.EssFiniteType k Cs.functionField := essFiniteType_functionField cs
  have hplace : ∀ x : closedPoints Cs, ∃ v : Place k Cs.functionField,
      (algebraMap (Cs.presheaf.stalk x.1) Cs.functionField).range = v.toValuationSubring.toSubring
        :=
    fun x => exists_place_range_stalk_eq cs x.1 (mem_closedPoints_iff.mp x.2)
  choose pl hpl using hplace
  have hinj : Function.Injective pl := fun x y hxy =>
    Subtype.ext (eq_of_range_stalk_eq cs x.1 y.1 (by rw [hpl x, hpl y, hxy]))
  have hsurj : Function.Surjective pl := fun v => by
    obtain ⟨x, hxc, hx⟩ := exists_closedPoint_range_stalk_eq cs v
    refine ⟨⟨x, mem_closedPoints_iff.mpr hxc⟩, Place.ext ?_⟩
    apply ValuationSubring.toSubring_injective
    rw [← hpl, hx]
  refine ⟨hco, hft,
    { C := Cs
      toBase := cs
      ffEquiv := RingEquiv.refl _
      ffEquiv_algebraMap := fun _ => rfl
      placeOfPoint := pl
      placeOfPoint_bijective := ⟨hinj, hsurj⟩
      range_stalk_eq := fun x => by
        rw [← hpl x]
        ext f
        exact ⟨fun ⟨y, hy⟩ => ⟨y, hy⟩, fun ⟨y, hy⟩ => ⟨y, hy⟩⟩
      finset_subset_affineOpen := fun F =>
        exists_isAffineOpen_forall_mem_of_finset cs F }, Iso.refl _, ?_, ?_⟩
  · simp [cs]
  · intro U _ _ t
    rfl