PlacesOf_preimage_subset_preimage_restrictAlong_placesOf.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.placesOf_preimage_subset_preimage_restrictAlong_placesOf
    {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] [SmoothOfRelativeDimension 1 cX]
    (π : 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
    placesOf cY (π ⁻¹ᵁ U) ⊆ (Place.restrictAlong φ hφ) ⁻¹' placesOf cX U := by
  let := (baseToFunctionField cX).toAlgebra
  let := (baseToFunctionField cY).toAlgebra
  rintro w ⟨y, hyU, hyc, hyw⟩
  have hxc : IsClosed ({π y} : Set X) := by
    rw [← Set.image_singleton]; exact π.isClosedMap _ hyc
  obtain ⟨v, hv⟩ := exists_place_range_stalk_eq cX (π y) hxc
  refine ⟨π y, hyU, hxc, ?_⟩
  rw [hv, AlgebraicCurve.GlueAux.eq_restrictAlong_of_range_stalk_eq cX cY π φ hφ hφπ y w v hyw hv]