exists_eq_snd_comp_of_comp_eq_const_of_isProper.lean

theorem AlgebraicGeometry.bijective_algebraMap_appTop_of_isProper_of_isIntegral_of_section
    (k : Type u) [Field k] {X : Scheme.{u}}
    (fX : X ⟶ Spec (CommRingCat.of k)) [IsProper fX] [IsIntegral X]
    (x₀ : Spec (CommRingCat.of k) ⟶ X) (hx₀ : x₀ ≫ fX = 𝟙 _) :
    Function.Bijective ((Scheme.ΓSpecIso (CommRingCat.of k)).inv ≫ fX.appTop).hom

theorem AlgebraicGeometry.exists_opens_ι_comp_eq_of_isClosedMap_of_app_bijective_of_isAffineOpen
    {S X Y : Scheme.{u}} (p : X ⟶ S) (hp : IsClosedMap p.base)
    (hO : ∀ U : S.Opens, IsAffineOpen U → Function.Bijective (p.app U).hom)
    (ε : S ⟶ X) (hε : ε ≫ p = 𝟙 S)
    (f : X ⟶ Y) (s : S) (y₀ : Y) (hs : ∀ x : X, p.base x = s → f.base x = y₀) :
    ∃ U : S.Opens, s ∈ U ∧ (p ⁻¹ᵁ U).ι ≫ f = (p ⁻¹ᵁ U).ι ≫ p ≫ ε ≫ f

theorem AlgebraicGeometry.RigidityAux.bijective_iso_comp_iso_iff {A B C D : CommRingCat.{u}}
    (e : A ⟶ B) (he : Function.Bijective e.hom) (f : B ⟶ C) (e' : C ⟶ D) (he' : Function.Bijective
      e'.hom) :
    Function.Bijective (e ≫ f ≫ e').hom ↔ Function.Bijective f.hom

theorem AlgebraicGeometry.RigidityAux.bijective_app_pullback_snd_of_isAffineOpen
    {k : Type u} [Field k] {X Y : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
    [CompactSpace X] [QuasiSeparatedSpace X]
    (hX : Function.Bijective ((Scheme.ΓSpecIso (CommRingCat.of k)).inv ≫ fX.appTop).hom)
    (fY : Y ⟶ Spec (CommRingCat.of k)) (V : Y.Opens) (hV : IsAffineOpen V) :
    Function.Bijective ((pullback.snd fX fY).app V).hom

theorem _root_.AlgebraicGeometry.exists_eq_snd_comp_of_comp_eq_const_of_isProper
    (k : Type u) [Field k] {X Y Z : Scheme.{u}}
    (fX : X ⟶ Spec (CommRingCat.of k)) [IsProper fX] [IsIntegral X]
    (fY : Y ⟶ Spec (CommRingCat.of k)) (hY : ConnectedSpace Y)
    (fZ : Z ⟶ Spec (CommRingCat.of k)) [IsSeparated fZ]
    (x₀ : Spec (CommRingCat.of k) ⟶ X) (hx₀ : x₀ ≫ fX = 𝟙 _)
    (y₀ : Spec (CommRingCat.of k) ⟶ Y) (hy₀ : y₀ ≫ fY = 𝟙 _)
    (φ : pullback fX fY ⟶ Z) (_hφ : φ ≫ fZ = pullback.fst fX fY ≫ fX)
    (z₀ : Spec (CommRingCat.of k) ⟶ Z)
    (hconst : pullback.lift (𝟙 X) (fX ≫ y₀)
      (by rw [Category.id_comp, Category.assoc, hy₀, Category.comp_id]) ≫ φ = fX ≫ z₀) :
    φ = pullback.snd fX fY ≫ (pullback.lift (fY ≫ x₀) (𝟙 Y)
      (by rw [Category.assoc, hx₀, Category.comp_id, Category.id_comp]) ≫ φ) := by
  have hεp : (pullback.lift (fY ≫ x₀) (𝟙 Y)
      (by rw [Category.assoc, hx₀, Category.comp_id, Category.id_comp])) ≫
      (pullback.snd fX fY) = 𝟙 Y := pullback.lift_snd _ _ _
  have hpc : IsClosedMap (pullback.snd fX fY).base := (pullback.snd fX fY).isClosedMap
  have hpo : IsOpenMap (pullback.snd fX fY).base := (pullback.snd fX fY).isOpenMap
  have : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace fX
  have : QuasiSeparatedSpace X := (quasiSeparated_iff_quasiSeparatedSpace fX).mp inferInstance
  have hXΓ := AlgebraicGeometry.bijective_algebraMap_appTop_of_isProper_of_isIntegral_of_section k
    fX x₀ hx₀
  have hO : ∀ U : Y.Opens, IsAffineOpen U → Function.Bijective ((pullback.snd fX fY).app U).hom :=
    fun U hU =>
    AlgebraicGeometry.RigidityAux.bijective_app_pullback_snd_of_isAffineOpen fX hXΓ fY U hU
  have hloc : ∀ (y : Y) (z : Z), (∀ w : ↥(pullback fX fY), (pullback.snd fX fY).base w = y → φ.base
    w = z) →
      ∃ U : Y.Opens, y ∈ U ∧ ((pullback.snd fX fY) ⁻¹ᵁ U).ι ≫ φ = ((pullback.snd fX fY) ⁻¹ᵁ U).ι ≫
        (pullback.snd fX fY) ≫ (pullback.lift (fY ≫ x₀) (𝟙 Y)
        (by rw [Category.assoc, hx₀, Category.comp_id, Category.id_comp])) ≫ φ :=
    fun y z h =>
      AlgebraicGeometry.exists_opens_ι_comp_eq_of_isClosedMap_of_app_bijective_of_isAffineOpen
      (pullback.snd fX fY) hpc hO (pullback.lift (fY ≫ x₀) (𝟙 Y)
        (by rw [Category.assoc, hx₀, Category.comp_id, Category.id_comp])) hεp φ y z h
  have : Z.IsSeparated := by
    rw [Scheme.isSeparated_iff, ← terminal.comp_from fZ]
    infer_instance
  let ι := equalizer.ι φ ((pullback.snd fX fY) ≫ (pullback.lift (fY ≫ x₀) (𝟙 Y)
    (by rw [Category.assoc, hx₀, Category.comp_id, Category.id_comp])) ≫ φ)
  have : IsClosedImmersion ι := inferInstance
  have hEclosed : IsClosed (Set.range ι.base) := ι.isClosedEmbedding.isClosed_range
  let T : Set Y := {y | ∃ U : Y.Opens, y ∈ U ∧ ((pullback.snd fX fY) ⁻¹ᵁ U).ι ≫ φ = ((pullback.snd
    fX fY) ⁻¹ᵁ U).ι ≫ (pullback.snd fX fY) ≫ (pullback.lift (fY ≫ x₀) (𝟙 Y)
    (by rw [Category.assoc, hx₀, Category.comp_id, Category.id_comp])) ≫ φ}
  have hTopen : IsOpen T := by
    rw [isOpen_iff_forall_mem_open]
    rintro y ⟨U, hyU, hU⟩
    exact ⟨U, fun y' hy' => ⟨U, hy', hU⟩, U.2, hyU⟩
  have hT : T = ((pullback.snd fX fY).base '' (Set.range ι.base)ᶜ)ᶜ := by
    ext y
    constructor
    · rintro ⟨U, hyU, hU⟩ ⟨w, hw, hwy⟩
      apply hw
      have hwU : w ∈ (pullback.snd fX fY) ⁻¹ᵁ U :=
        by change (pullback.snd fX fY).base w ∈ U; rw [hwy]; exact hyU
      refine ⟨(equalizer.lift ((pullback.snd fX fY) ⁻¹ᵁ U).ι hU).base ⟨w, hwU⟩, ?_⟩
      change ((equalizer.lift ((pullback.snd fX fY) ⁻¹ᵁ U).ι hU) ≫ ι).base ⟨w, hwU⟩ = w
      rw [equalizer.lift_ι]
      rfl
    · intro hy
      have hfib : ∀ w : ↥(pullback fX fY), (pullback.snd fX fY).base w = y → φ.base w =
        ((pullback.lift (fY ≫ x₀) (𝟙 Y)
        (by rw [Category.assoc, hx₀, Category.comp_id, Category.id_comp])) ≫ φ).base y := by
        intro w hwy
        have hwE : w ∈ Set.range ι.base := by
          by_contra hw
          exact hy ⟨w, hw, hwy⟩
        obtain ⟨e, rfl⟩ := hwE
        change (ι ≫ φ).base e = _
        rw [equalizer.condition]
        change ((pullback.lift (fY ≫ x₀) (𝟙 Y)
          (by rw [Category.assoc, hx₀, Category.comp_id, Category.id_comp])) ≫ φ).base
          ((pullback.snd fX fY).base (ι.base e)) = _
        rw [hwy]
      exact hloc y _ hfib
  have hTclosed : IsClosed T := by
    rw [hT]
    exact (hpo _ hEclosed.isOpen_compl).isClosed_compl
  have hy₀T : T.Nonempty := by
    let pt : ↥(Spec (CommRingCat.of k)) := IsLocalRing.closedPoint k
    refine ⟨y₀.base pt, hloc _ (z₀.base pt) fun w hw => ?_⟩
    let sl : X ⟶ pullback fX fY := pullback.lift (𝟙 X) (fX ≫ y₀)
      (by rw [Category.id_comp, Category.assoc, hy₀, Category.comp_id])
    have hw' : w ∈ Set.range sl.base := by
      have hsq : IsPullback sl fX (pullback.snd fX fY) y₀ := by
        refine IsPullback.of_right (h₁₂ := pullback.fst fX fY) (h₂₂ := fY) ?_ (pullback.lift_snd _
          _ _) (IsPullback.of_hasPullback fX fY)
        have e1 : sl ≫ pullback.fst fX fY = 𝟙 X := pullback.lift_fst _ _ _
        rw [e1, hy₀]
        exact IsPullback.of_horiz_isIso ⟨by simp⟩
      have hr : Set.range sl.base = (pullback.snd fX fY).base ⁻¹' Set.range y₀.base := by
        rw [← Scheme.Pullback.range_fst (pullback.snd fX fY) y₀, ← hsq.isoPullback_hom_fst]
        rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
          Set.range_eq_univ.mpr (ConcreteCategory.bijective_of_isIso hsq.isoPullback.hom.base).2,
            Set.image_univ]
      rw [hr]
      exact ⟨pt, hw.symm⟩
    obtain ⟨x, rfl⟩ := hw'
    change (sl ≫ φ).base x = _
    rw [hconst]
    change z₀.base (fX.base x) = z₀.base pt
    congr 1
    exact Subsingleton.elim _ _
  have hTuniv : T = Set.univ := by
    have := hY
    exact IsClopen.eq_univ ⟨hTclosed, hTopen⟩ hy₀T
  have hcov : ∀ y : Y, ∃ U : Y.Opens, y ∈ U ∧ ((pullback.snd fX fY) ⁻¹ᵁ U).ι ≫ φ = ((pullback.snd
    fX fY) ⁻¹ᵁ U).ι ≫ (pullback.snd fX fY) ≫ (pullback.lift (fY ≫ x₀) (𝟙 Y)
    (by rw [Category.assoc, hx₀, Category.comp_id, Category.id_comp])) ≫ φ :=
    fun y => (hTuniv ▸ Set.mem_univ y : y ∈ T)
  choose U hU using hcov
  let 𝒰 := (pullback fX fY).openCoverOfIsOpenCover (fun y : Y => (pullback.snd fX fY) ⁻¹ᵁ U y)
    (IsOpenCover.mk (eq_top_iff.mpr fun w _ => Opens.mem_iSup.mpr ⟨(pullback.snd fX fY).base w, (hU
      _).1⟩))
  exact Scheme.Cover.hom_ext 𝒰 _ _ fun y => (hU y).2