CurveModel_exists_opens_hom_comp_eq_of_existsUnique_evalAt_eq_appLE.lean

theorem isRational [IsCurveOver ℂ F] (v : Place ℂ F) : v.IsRational

theorem evalAt_add (v : Place ℂ F) (hv : v.IsRational) {f g : F}
    (hf : f ∈ v.toValuationSubring) (hg : g ∈ v.toValuationSubring) :
    v.evalAt (f + g) = v.evalAt f + v.evalAt g

theorem evalAt_eq_of_sub_algebraMap_mem_nonunits (v : Place ℂ F) {x : F} (hx : x ∈
  v.toValuationSubring) (c : ℂ)
    (h : x - algebraMap ℂ F c ∈ v.toValuationSubring.nonunits) : v.evalAt x = c

theorem appLE_congr_hom {X Y : Scheme.{0}} {p q : X ⟶ Y} (hpq : p = q) (U : Y.Opens) (V : X.Opens)
    (h : V ≤ p ⁻¹ᵁ U) (h' : V ≤ q ⁻¹ᵁ U) : p.appLE U V h = q.appLE U V h'

theorem top_le_preimage_iff (q : Spec (CommRingCat.of ℂ) ⟶ X) (U : X.Opens) :
    ⊤ ≤ q ⁻¹ᵁ U ↔ q.base (IsLocalRing.closedPoint ℂ) ∈ U

def evalAlgHom (f : X ⟶ Spec (CommRingCat.of K)) (U : X.Opens) (P : Spec (CommRingCat.of K) ⟶ X)
    (hP1 : P ≫ f = 𝟙 _) (hP : ⊤ ≤ P ⁻¹ᵁ U) :
    letI := f.sectionsAlgebra U
    Γ(X, U) →ₐ[K] K :=
  letI := f.sectionsAlgebra U
  { toRingHom := (P.appLE U ⊤ hP ≫ (Scheme.ΓSpecIso (CommRingCat.of K)).hom).hom
    commutes' := fun r => by
      change ((Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ f.appLE ⊤ U le_top ≫ P.appLE U ⊤ hP ≫
        (Scheme.ΓSpecIso (CommRingCat.of K)).hom).hom r = r
      have h1 : f.appLE ⊤ U le_top ≫ P.appLE U ⊤ hP = 𝟙 _ := by
        erw [Scheme.Hom.appLE_comp_appLE, appLE_congr_hom hP1 ⊤ ⊤ _ le_top]
        simp [Scheme.Hom.appLE]
      rw [← Category.assoc (f.appLE ⊤ U le_top), h1]
      simp }

theorem evalAlgHom_apply (f : X ⟶ Spec (CommRingCat.of K)) (U : X.Opens) (P : Spec (CommRingCat.of
  K) ⟶ X)
    (hP1 : P ≫ f = 𝟙 _) (hP : ⊤ ≤ P ⁻¹ᵁ U) (s : Γ(X, U)) :
    evalAlgHom f U P hP1 hP s = (Scheme.ΓSpecIso (CommRingCat.of K)).hom ((P.appLE U ⊤ hP) s)

theorem exists_ringHom_forall_mem_and_evalAt_eq
    (hB : ∀ φ : Γ(Y, U), ∃! ξ : F, ∀ (v : Place ℂ F) (h : ⊤ ≤ (w v).1 ⁻¹ᵁ U),
      ξ ∈ v.toValuationSubring ∧
        Place.evalAt v ξ = (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom (((w v).1.appLE U ⊤ h) φ)) :
    letI := pY.sectionsAlgebra U
    ∃ θ : Γ(Y, U) →+* F,
      (∀ (φ : Γ(Y, U)) (v : Place ℂ F) (h : ⊤ ≤ (w v).1 ⁻¹ᵁ U),
        θ φ ∈ v.toValuationSubring ∧
          Place.evalAt v (θ φ) = (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom (((w v).1.appLE U ⊤ h)
            φ)) ∧
      ∀ c : ℂ, θ (algebraMap ℂ Γ(Y, U) c) = algebraMap ℂ F c := by
  classical
  let := pY.sectionsAlgebra U
  choose ξ hξ hξu using hB
  have hv : ∀ v : Place ℂ F, v.IsRational := isRational
  have hmul : ∀ φ ψ : Γ(Y, U), ξ (φ * ψ) = ξ φ * ξ ψ := fun φ ψ =>
    (hξu (φ * ψ) _ fun v h => ⟨mul_mem (hξ φ v h).1 (hξ ψ v h).1, by
      rw [Place.evalAt_mul v (hv v) (hξ φ v h).1 (hξ ψ v h).1, (hξ φ v h).2, (hξ ψ v h).2, map_mul,
        map_mul]⟩).symm
  have hadd : ∀ φ ψ : Γ(Y, U), ξ (φ + ψ) = ξ φ + ξ ψ := fun φ ψ =>
    (hξu (φ + ψ) _ fun v h => ⟨add_mem (hξ φ v h).1 (hξ ψ v h).1, by
      rw [evalAt_add v (hv v) (hξ φ v h).1 (hξ ψ v h).1, (hξ φ v h).2, (hξ ψ v h).2, map_add,
        map_add]⟩).symm
  have hconst : ∀ c : ℂ, ξ (algebraMap ℂ Γ(Y, U) c) = algebraMap ℂ F c := fun c =>
    (hξu _ _ fun v h => ⟨v.algebraMap_mem' c, by
      rw [Place.evalAt_algebraMap, ← evalAlgHom_apply pY U (w v).1 (w v).2 h, AlgHom.commutes];
        rfl⟩).symm
  have hone : ξ 1 = 1 := by simpa using hconst 1
  have hzero : ξ 0 = 0 := by simpa using hconst 0
  exact ⟨{ toFun := ξ, map_one' := hone, map_mul' := hmul, map_zero' := hzero, map_add' := hadd },
    fun φ v h => hξ φ v h, hconst⟩

def goodOpen (S : Set (Place ℂ F)) (hS : Sᶜ.Finite) : M.C.Opens

theorem mem_goodOpen_iff (S : Set (Place ℂ F)) (hS : Sᶜ.Finite) (x : M.C) :
    x ∈ goodOpen M S hS ↔ ∀ hx : x ∈ closedPoints M.C, M.placeEquiv ⟨x, hx⟩ ∈ S

theorem eq_genericPoint_or_isClosed (x : M.C) : x = genericPoint M.C ∨ IsClosed ({x} : Set M.C)

theorem exists_ringHom_sections {R : Type} [CommRing R] (θ : R →+* F)
    (S : Set (Place ℂ F)) (hS : Sᶜ.Finite)
    (hθ : ∀ (r : R) (v : Place ℂ F), v ∈ S → θ r ∈ v.toValuationSubring) :
    ∃ Θ : R →+* Γ(M.C, goodOpen M S hS),
      (∀ (r : R) (x : M.C) (hx : x ∈ goodOpen M S hS),
        algebraMap (M.C.presheaf.stalk x) M.C.functionField
          (M.C.presheaf.germ (goodOpen M S hS) x hx (Θ r)) = M.ffEquiv (θ r)) ∧
      ∀ (r : R) (u : Γ(M.C, goodOpen M S hS)),
        (∀ (x : M.C) (hx : x ∈ goodOpen M S hS),
          algebraMap (M.C.presheaf.stalk x) M.C.functionField
            (M.C.presheaf.germ (goodOpen M S hS) x hx u) = M.ffEquiv (θ r)) → u = Θ r

theorem hom_eq_toSpecΓ {X : Scheme.{0}} {R : CommRingCat.{0}} (f : X ⟶ Spec R) :
    f = X.toSpecΓ ≫ Spec.map ((Scheme.ΓSpecIso R).inv ≫ f.appTop)

theorem val_fromSpec {M : Scheme.{0}} {U : M.Opens} (hU : IsAffineOpen U)
    (σ : Γ(M, U) ⟶ CommRingCat.of ℂ)
    (h : ⊤ ≤ (Spec.map σ ≫ hU.fromSpec) ⁻¹ᵁ U) (a : Γ(M, U)) :
    (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom (((Spec.map σ ≫ hU.fromSpec).appLE U ⊤ h) a) = σ a

theorem fromSpec_comp_eq_SpecMap {Y : Scheme.{0}} {R : CommRingCat.{0}} (pY : Y ⟶ Spec R) (U :
  Y.Opens) (hU : IsAffineOpen U) :
    hU.fromSpec ≫ pY = Spec.map ((Scheme.ΓSpecIso R).inv ≫ pY.appLE ⊤ U le_top)

theorem point_toSpecΓ_comp {X : Scheme.{0}} {R A : CommRingCat.{0}}
    (q : Spec R ⟶ X) (a : A ⟶ Γ(X, ⊤)) :
    q ≫ X.toSpecΓ ≫ Spec.map a = Spec.map (a ≫ q.appTop ≫ (Scheme.ΓSpecIso R).hom)

theorem exists_hom_piece (U : Y.Opens) (hU : IsAffineOpen U)
    (S : Set (Place ℂ F)) (hS : Sᶜ.Finite) (hSU : ∀ v ∈ S, ⊤ ≤ (w v).1 ⁻¹ᵁ U)
    (θ : Γ(Y, U) →+* F)
    (hθ : ∀ (φ : Γ(Y, U)) (v : Place ℂ F) (h : ⊤ ≤ (w v).1 ⁻¹ᵁ U),
      θ φ ∈ v.toValuationSubring ∧
        Place.evalAt v (θ φ) = (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom (((w v).1.appLE U ⊤ h) φ))
    (hθc : letI := pY.sectionsAlgebra U; ∀ c : ℂ, θ (algebraMap ℂ Γ(Y, U) c) = algebraMap ℂ F c)
    (Θ : Γ(Y, U) →+* Γ(M.C, goodOpen M S hS))
    (hΘ : ∀ (φ : Γ(Y, U)) (x : M.C) (hx : x ∈ goodOpen M S hS),
        algebraMap (M.C.presheaf.stalk x) M.C.functionField
          (M.C.presheaf.germ (goodOpen M S hS) x hx (Θ φ)) = M.ffEquiv (θ φ))
    (hΘu : ∀ (φ : Γ(Y, U)) (u : Γ(M.C, goodOpen M S hS)),
        (∀ (x : M.C) (hx : x ∈ goodOpen M S hS),
          algebraMap (M.C.presheaf.stalk x) M.C.functionField
            (M.C.presheaf.germ (goodOpen M S hS) x hx u) = M.ffEquiv (θ φ)) → u = Θ φ) :
    ∃ W : (goodOpen M S hS : Scheme.{0}) ⟶ Y,
      W ≫ pY = (goodOpen M S hS).ι ≫ M.toBase ∧
      ∀ (p : {p : Spec (CommRingCat.of ℂ) ⟶ M.C // p ≫ M.toBase = 𝟙 _})
        (q : Spec (CommRingCat.of ℂ) ⟶ (goodOpen M S hS : Scheme.{0})), q ≫ (goodOpen M S hS).ι =
          p.1 →
        q ≫ W = (w (M.pointEquivPlace p)).1 := by
  classical
  let algU : Algebra ℂ Γ(Y, U) := pY.sectionsAlgebra U
  have hVne : ∀ (x : M.C), x ∈ goodOpen M S hS → (genericPoint M.C) ∈ goodOpen M S hS := fun x hx =>
    ((genericPoint_spec M.C).mem_open_set_iff (goodOpen M S hS).2).2 ⟨x, Set.mem_univ _, hx⟩
  let Θ' : Γ(Y, U) →+* Γ((goodOpen M S hS : Scheme.{0}), ⊤) := (goodOpen M S
    hS).topIso.inv.hom.comp Θ
  let W : (goodOpen M S hS : Scheme.{0}) ⟶ Y :=
    (goodOpen M S hS : Scheme.{0}).toSpecΓ ≫ Spec.map (CommRingCat.ofHom Θ') ≫ hU.fromSpec
  have hconst : ∀ c : ℂ, Θ (algebraMap ℂ Γ(Y, U) c) =
      (M.toBase.appLE ⊤ (goodOpen M S hS) le_top) ((Scheme.ΓSpecIso (CommRingCat.of ℂ)).inv c) := by
    intro c
    refine (hΘu (algebraMap ℂ Γ(Y, U) c) _ fun x hx => ?_).symm
    rw [hθc, M.ffEquiv_algebraMap]
    change (M.C.presheaf.stalkSpecializes (genericPoint_specializes x))
      ((M.C.presheaf.germ (goodOpen M S hS) x hx)
        ((M.C.presheaf.map (homOfLE (le_top : goodOpen M S hS ≤ ⊤)).op)
          ((M.toBase.app ⊤) ((Scheme.ΓSpecIso (CommRingCat.of ℂ)).inv c)))) = _
    erw [TopCat.Presheaf.germ_res_apply, ← CommRingCat.comp_apply (M.C.presheaf.germ _ _ _),
      TopCat.Presheaf.germ_stalkSpecializes]
    rfl
  have hover : W ≫ pY = (goodOpen M S hS).ι ≫ M.toBase := by
    have L3 : ((Scheme.ΓSpecIso (CommRingCat.of ℂ)).inv ≫ pY.appLE ⊤ U le_top) ≫ CommRingCat.ofHom
      Θ' =
        (Scheme.ΓSpecIso (CommRingCat.of ℂ)).inv ≫ ((goodOpen M S hS).ι ≫ M.toBase).appTop := by
      ext c
      change Θ' ((pY.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (CommRingCat.of ℂ)).inv c)) =
        ((goodOpen M S hS).ι ≫ M.toBase).appTop ((Scheme.ΓSpecIso (CommRingCat.of ℂ)).inv c)
      have h1 : (pY.appLE ⊤ U le_top) ((Scheme.ΓSpecIso (CommRingCat.of ℂ)).inv c) = algebraMap ℂ
        Γ(Y, U) c := rfl
      rw [h1]
      change (goodOpen M S hS).topIso.inv (Θ (algebraMap ℂ Γ(Y, U) c)) = _
      erw [hconst, Scheme.Hom.comp_appTop, Scheme.Opens.ι_appTop, Scheme.Opens.topIso_inv,
        CommRingCat.comp_apply]
      change (M.toBase.appLE ⊤ (goodOpen M S hS) le_top ≫ M.C.presheaf.map (eqToHom (goodOpen M S
        hS).ι_image_top).op)
          ((Scheme.ΓSpecIso (CommRingCat.of ℂ)).inv c) =
        (M.toBase.appLE ⊤ ((goodOpen M S hS).ι ''ᵁ ⊤) le_top) ((Scheme.ΓSpecIso (CommRingCat.of
          ℂ)).inv c)
      erw [Scheme.Hom.appLE_map]
    rw [hom_eq_toSpecΓ ((goodOpen M S hS).ι ≫ M.toBase)]
    simp only [W, Category.assoc]
    erw [fromSpec_comp_eq_SpecMap pY U hU, ← Spec.map_comp]
    exact congrArg (fun f => (goodOpen M S hS : Scheme.{0}).toSpecΓ ≫ Spec.map f) L3
  refine ⟨W, hover, ?_⟩
  intro p q hq
  set x : M.C := p.1.base (IsLocalRing.closedPoint ℂ) with hxdef
  have hxc : x ∈ closedPoints M.C := by
    rw [hxdef, ← pointEquivClosedPoint_apply_coe M.toBase p]; exact (pointEquivClosedPoint M.toBase
      p).2
  have hpV : ⊤ ≤ p.1 ⁻¹ᵁ goodOpen M S hS := by
    rw [← hq, Scheme.Hom.comp_preimage, Scheme.Opens.ι_preimage_self]; simp
  have hxV : x ∈ goodOpen M S hS := (top_le_preimage_iff _ _).1 hpV
  have : Nonempty ((goodOpen M S hS : Scheme.{0})) := ⟨⟨x, hxV⟩⟩
  set v : Place ℂ F := M.pointEquivPlace p with hvdef
  have hv : v = M.placeEquiv ⟨x, hxc⟩ := by
    rw [hvdef, AlgebraicCurve.CurveModel.pointEquivPlace_apply,
      AlgebraicCurve.CurveModel.placeEquiv_apply]
    congr 1
  have hvS : v ∈ S := by rw [hv]; exact (mem_goodOpen_iff M S hS x).1 hxV hxc
  have hwU : ⊤ ≤ (w v).1 ⁻¹ᵁ U := hSU v hvS
  let σ : Γ(Y, U) ⟶ CommRingCat.of ℂ :=
    CommRingCat.ofHom Θ' ≫ q.appTop ≫ (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom
  have hqW : q ≫ W = Spec.map σ ≫ hU.fromSpec := by
    have he := congrArg (fun z => z ≫ hU.fromSpec)
      (point_toSpecΓ_comp q (CommRingCat.ofHom Θ'))
    convert he using 1
    simp only [W, Category.assoc]
  have hqWU : ⊤ ≤ (q ≫ W) ⁻¹ᵁ U := by
    rw [hqW, Scheme.Hom.comp_preimage, hU.fromSpec_preimage_self]; simp
  have hqW1 : (q ≫ W) ≫ pY = 𝟙 _ := by rw [Category.assoc, hover, ← Category.assoc, hq, p.2]
  have hval_q : ∀ φ : Γ(Y, U),
      (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom (((q ≫ W).appLE U ⊤ hqWU) φ) =
        (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom ((p.1.appLE (goodOpen M S hS) ⊤ hpV) (Θ φ)) := by
    intro φ
    have h1 : (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom (((q ≫ W).appLE U ⊤ hqWU) φ) = σ φ := by
      have h' : ⊤ ≤ (Spec.map σ ≫ hU.fromSpec) ⁻¹ᵁ U := by rw [← hqW]; exact hqWU
      rw [appLE_congr_hom hqW U ⊤ hqWU h']
      exact val_fromSpec hU σ h' φ
    rw [h1]
    change (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom (q.appTop ((goodOpen M S hS).topIso.inv (Θ φ)))
      = _
    congr 1
    have h2 : p.1.appLE (goodOpen M S hS) ⊤ hpV =
        (goodOpen M S hS).ι.appLE (goodOpen M S hS) ⊤
          (by rw [Scheme.Opens.ι_preimage_self]) ≫ q.appLE ⊤ ⊤ le_top := by
      erw [Scheme.Hom.appLE_comp_appLE, appLE_congr_hom hq]
    rw [h2, CommRingCat.comp_apply]
    congr 1
    · rw [Scheme.Opens.ι_appLE, Scheme.Opens.topIso_inv]; rfl
  have hval_p : ∀ φ : Γ(Y, U),
      (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom ((p.1.appLE (goodOpen M S hS) ⊤ hpV) (Θ φ)) =
        Place.evalAt v (θ φ) := by
    intro φ
    obtain ⟨hmem, hnu⟩ :=
      ffEquiv_symm_germToFunctionField_mem_and_sub_algebraMap_appLE_mem_nonunits_pointEquivPlace
        M (goodOpen M S hS) (Θ φ) p hpV
    have hgerm : M.ffEquiv.symm (M.C.germToFunctionField (goodOpen M S hS) (Θ φ)) = θ φ := by
      apply M.ffEquiv.injective
      rw [RingEquiv.apply_symm_apply]
      have := hΘ φ (genericPoint M.C) (hVne x hxV)
      rw [← this]
      change _ = (M.C.presheaf.stalkSpecializes (genericPoint_specializes (genericPoint M.C))).hom
        ((M.C.presheaf.germ (goodOpen M S hS) (genericPoint M.C) (hVne x hxV)).hom (Θ φ))
      rw [← CommRingCat.comp_apply, TopCat.Presheaf.germ_stalkSpecializes]
    rw [hgerm] at hmem hnu
    rw [← hvdef] at hmem hnu
    exact (evalAt_eq_of_sub_algebraMap_mem_nonunits v hmem _ hnu).symm
  refine (AlgebraicGeometry.IsAffineOpen.eq_of_appLE_eq_and_exists_appLE_eq_of_ringHom pY U hU).1
    (q ≫ W) (w v).1 hqW1 (w v).2 hqWU hwU ?_
  ext φ
  change (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom (((q ≫ W).appLE U ⊤ hqWU) φ) =
    (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom (((w v).1.appLE U ⊤ hwU) φ)
  rw [hval_q, hval_p, (hθ φ v hwU).2]

theorem exists_mem_closedPoints {X : Scheme.{0}} (f : X ⟶ Spec (CommRingCat.of ℂ))
  [LocallyOfFiniteType f] [Nonempty X] :
    ∃ x : X, x ∈ closedPoints X

theorem _root_.AlgebraicCurve.CurveModel.exists_opens_hom_comp_eq_of_existsUnique_evalAt_eq_appLE
    (F : Type) [Field F] [Algebra ℂ F] [IsCurveOver ℂ F]
    (M : CurveModel ℂ F)
    {Y : Scheme.{0}} (pY : Y ⟶ Spec (CommRingCat.of ℂ))
    (w : Place ℂ F → {P : Spec (CommRingCat.of ℂ) ⟶ Y // P ≫ pY = 𝟙 _})
    (U : Y.Opens) (hU : IsAffineOpen U)
    (hA : Set.Finite {v : Place ℂ F | ¬ (⊤ ≤ (w v).1 ⁻¹ᵁ U)})
    (hB : ∀ φ : Γ(Y, U), ∃! ξ : F, ∀ (v : Place ℂ F) (h : ⊤ ≤ (w v).1 ⁻¹ᵁ U),
      ξ ∈ v.toValuationSubring ∧
        Place.evalAt v ξ = (Scheme.ΓSpecIso (CommRingCat.of ℂ)).hom (((w v).1.appLE U ⊤ h) φ)) :
    ∃ (V : M.C.Opens),
      (∀ x : M.C, x ∈ V ↔ ∀ hx : x ∈ closedPoints M.C, ⊤ ≤ (w (M.placeEquiv ⟨x, hx⟩)).1 ⁻¹ᵁ U) ∧
      ∃ W : (V : Scheme.{0}) ⟶ Y,
        W ≫ pY = V.ι ≫ M.toBase ∧
        ∀ (p : {p : Spec (CommRingCat.of ℂ) ⟶ M.C // p ≫ M.toBase = 𝟙 _})
          (q : Spec (CommRingCat.of ℂ) ⟶ (V : Scheme.{0})), q ≫ V.ι = p.1 →
          q ≫ W = (w (M.pointEquivPlace p)).1