Preimage_restrictAlong_placesOf_subset_placesOf_preimage.lean

theorem comp_algebraMap_stalk_eq
    {X Y : Scheme.{u}} [IsIntegral X] [IsIntegral Y] (π : Y ⟶ X)
    (φ : X.functionField →+* Y.functionField)
    (hφπ : Y.fromSpecStalk (genericPoint Y) ≫ π =
      Spec.map (CommRingCat.ofHom φ) ≫ X.fromSpecStalk (genericPoint X))
    (y : Y) :
    φ.comp (algebraMap (X.presheaf.stalk (π y)) X.functionField) =
      (algebraMap (Y.presheaf.stalk y) Y.functionField).comp (π.stalkMap y).hom

theorem place_eq_of_le {K F : Type*} [Field K] [Field F] [Algebra K F] {v w : Place K F}
    (h : v.toValuationSubring ≤ w.toValuationSubring) : v = w

theorem eq_restrictAlong_of_range_stalk_eq
    {K : Type u} [Field K] {X Y : Scheme.{u}}
    (cX : X ⟶ Spec (CommRingCat.of K)) (cY : Y ⟶ Spec (CommRingCat.of K))
    [IsIntegral X] [IsIntegral Y] (π : Y ⟶ X)
    (φ : letI := (baseToFunctionField cX).toAlgebra
      letI := (baseToFunctionField cY).toAlgebra
      X.functionField →ₐ[K] Y.functionField)
    (hφ : letI := (baseToFunctionField cX).toAlgebra
      letI := (baseToFunctionField cY).toAlgebra
      φ.toRingHom.IsIntegral)
    (hφπ : letI := (baseToFunctionField cX).toAlgebra
      letI := (baseToFunctionField cY).toAlgebra
      Y.fromSpecStalk (genericPoint Y) ≫ π =
        Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ X.fromSpecStalk (genericPoint X))
    (y : Y) :
    letI := (baseToFunctionField cX).toAlgebra
    letI := (baseToFunctionField cY).toAlgebra
    ∀ (w : Place K Y.functionField) (v : Place K X.functionField),
      (algebraMap (Y.presheaf.stalk y) Y.functionField).range = w.toValuationSubring.toSubring →
      (algebraMap (X.presheaf.stalk (π y)) X.functionField).range = v.toValuationSubring.toSubring →
      v = Place.restrictAlong φ hφ w := by
  let := (baseToFunctionField cX).toAlgebra
  let := (baseToFunctionField cY).toAlgebra
  intro w v hyw hv
  have hc := comp_algebraMap_stalk_eq π φ.toRingHom hφπ y
  apply place_eq_of_le
  intro f hf
  have hf' : f ∈ (algebraMap (X.presheaf.stalk (π y)) X.functionField).range := by
    rw [hv]; exact hf
  obtain ⟨g, rfl⟩ := RingHom.mem_range.mp hf'
  change φ.toRingHom (algebraMap _ _ g) ∈ w.toValuationSubring
  rw [← RingHom.comp_apply, hc, RingHom.comp_apply, ← ValuationSubring.mem_toSubring, ← hyw]
  exact RingHom.mem_range_self _ _

theorem _root_.AlgebraicCurve.preimage_restrictAlong_placesOf_subset_placesOf_preimage
    {K : Type u} [Field K] {X Y : Scheme.{u}}
    (cX : X ⟶ Spec (CommRingCat.of K)) (cY : Y ⟶ Spec (CommRingCat.of K))
    [IsIntegral X] [IsIntegral Y] [IsSeparated cX] [SmoothOfRelativeDimension 1 cX]
    [IsProper cY] [SmoothOfRelativeDimension 1 cY]
    (π : Y ⟶ X) [UniversallyClosed π]
    (φ : letI := (baseToFunctionField cX).toAlgebra
      letI := (baseToFunctionField cY).toAlgebra
      X.functionField →ₐ[K] Y.functionField)
    (hφ : letI := (baseToFunctionField cX).toAlgebra
      letI := (baseToFunctionField cY).toAlgebra
      φ.toRingHom.IsIntegral)
    (hφπ : letI := (baseToFunctionField cX).toAlgebra
      letI := (baseToFunctionField cY).toAlgebra
      Y.fromSpecStalk (genericPoint Y) ≫ π =
        Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ X.fromSpecStalk (genericPoint X))
    (U : X.Opens) :
    letI := (baseToFunctionField cX).toAlgebra
    letI := (baseToFunctionField cY).toAlgebra
    (Place.restrictAlong φ hφ) ⁻¹' placesOf cX U ⊆ placesOf cY (π ⁻¹ᵁ U) := by
  let := (baseToFunctionField cX).toAlgebra
  let := (baseToFunctionField cY).toAlgebra
  rintro w ⟨x, hxU, hxc, hxw⟩
  obtain ⟨y, hyc, hyw⟩ := exists_closedPoint_range_stalk_eq cY w
  have hπyc : IsClosed ({π y} : Set X) := by
    rw [← Set.image_singleton]; exact π.isClosedMap _ hyc
  obtain ⟨v, hv⟩ := exists_place_range_stalk_eq cX (π y) hπyc
  have hveq := AlgebraicCurve.GlueAux.eq_restrictAlong_of_range_stalk_eq cX cY π φ hφ hφπ y w v
    hyw hv
  have hπy : π y = x := eq_of_range_stalk_eq cX (π y) x (by rw [hv, hxw, hveq])
  refine ⟨y, ?_, hyc, hyw⟩
  change π y ∈ U
  rw [hπy]; exact hxU