RegularPairHartogs.lean

theorem pow_dvd_of_regular_pair
    {R : Type u} [CommRing R] {x y : R}
    (hx : IsSMulRegular R x) (hy : IsSMulRegular (QuotSMulTop x R) y)
    (n m : ℕ) {a : R} (h : x ^ n ∣ y ^ m * a) : x ^ n ∣ a

theorem restrict_bijective_of_regular_pair
    (X : Scheme.{u}) [IsAffine X]
    (x y : Γ(X, ⊤))
    (hx : IsSMulRegular Γ(X, ⊤) x) (hy : IsSMulRegular Γ(X, ⊤) y)
    (hxy : IsSMulRegular (QuotSMulTop x Γ(X, ⊤)) y)
    (U : X.Opens) (hU : IsCompact U.1) (hU' : IsQuasiSeparated U.1)
    (hxU : X.basicOpen x ≤ U) (hyU : X.basicOpen y ≤ U) :
    Function.Bijective
      (X.presheaf.map (homOfLE (show U ≤ ⊤ from le_top)).op) := by
  let res : Γ(X, ⊤) ⟶ Γ(X, U) := X.presheaf.map (homOfLE le_top).op
  have hx0 : x ∈ nonZeroDivisors Γ(X, ⊤) :=
    mem_nonZeroDivisors_iff_left.mpr fun a ha => hx.right_eq_zero_of_smul ha
  have hy0 : y ∈ nonZeroDivisors Γ(X, ⊤) :=
    mem_nonZeroDivisors_iff_left.mpr fun a ha => hy.right_eq_zero_of_smul ha
  have hinj : Function.Injective res := by
    intro a b hab
    apply IsLocalization.injective Γ(X, X.basicOpen x) (Submonoid.powers_le.mpr hx0)
    have h := congrArg (X.presheaf.map (homOfLE hxU).op) hab
    have hcomp : res ≫ X.presheaf.map (homOfLE hxU).op =
        X.presheaf.map (homOfLE (show X.basicOpen x ≤ ⊤ from le_top)).op := by
      dsimp only [res]
      rw [← Functor.map_comp]
      congr 1
    change (X.presheaf.map (homOfLE le_top).op) a =
      (X.presheaf.map (homOfLE le_top).op) b
    simpa only [← CommRingCat.comp_apply, hcomp] using h
  refine ⟨hinj, ?_⟩
  intro s
  obtain ⟨a, n, ha⟩ :=
    exists_restrict_eq_pow_mul_of_basicOpen_le X U hU hU' x hx0 hxU s
  obtain ⟨b, m, hb⟩ :=
    exists_restrict_eq_pow_mul_of_basicOpen_le X U hU hU' y hy0 hyU s
  change res a = res x ^ n * s at ha
  change res b = res y ^ m * s at hb
  have hcross : y ^ m * a = x ^ n * b := by
    apply hinj
    rw [map_mul, map_pow, map_mul, map_pow, ha, hb]
    ring
  obtain ⟨c, hc⟩ := pow_dvd_of_regular_pair hx hxy n m ⟨b, hcross⟩
  refine ⟨c, ?_⟩
  have hxres : IsSMulRegular Γ(X, U) (res x) :=
    isSMulRegular_restrict_of_affine X U x hx0
  apply hxres.pow n
  change res x ^ n * res c = res x ^ n * s
  rw [← map_pow, ← map_mul, ← hc]
  simpa only [map_pow] using ha