DepthTwoSections.lean

theorem restrict_punctured_finiteFlat_bijective_of_two_le_depth
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (hdepth : (2 : ℕ∞) ≤ Module.depth R R)
    {X : Scheme.{u}} (p : X ⟶ Spec (.of R)) [IsFinite p] [Flat p] :
    Function.Bijective (X.presheaf.map
      (homOfLE (show p ⁻¹ᵁ Scheme.puncturedSpectrumOpen R ≤ ⊤ from le_top)).op) := by
  let : IsAffine X := isAffine_of_isAffineHom p
  let : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian p
  let : IsNoetherianRing Γ(X, ⊤) :=
    IsLocallyNoetherian.component_noetherian ⟨⊤, isAffineOpen_top X⟩
  let : NoetherianSpace X := noetherianSpace_of_isAffine (X := X)
  let c : CommRingCat.of R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (.of R)).inv ≫ p.appTop
  let : Algebra R Γ(X, ⊤) := c.hom.toAlgebra
  let : Module.Flat R Γ(X, ⊤) :=
    (RingHom.Flat.of_bijective
      (ConcreteCategory.bijective_of_isIso (Scheme.ΓSpecIso (.of R)).inv)).comp
      p.flat_appTop
  obtain ⟨x, hxmem, y, hymem, hxy, hyx⟩ :=
    SchemeTheory.exists_regular_pair_of_two_le_depth R hdepth
  have transfer (rs : List R) (h : Sequence.IsWeaklyRegular R rs) :
      Sequence.IsWeaklyRegular Γ(X, ⊤) (rs.map (algebraMap R Γ(X, ⊤))) := by
    apply (Sequence.isWeaklyRegular_map_algebraMap_iff Γ(X, ⊤) Γ(X, ⊤) rs).mpr
    exact ((TensorProduct.lid R Γ(X, ⊤)).isWeaklyRegular_congr rs).mp
      h.isWeaklyRegular_rTensor
  have hxy' := transfer [x, y] hxy
  have hyx' := transfer [y, x] hyx
  simp only [List.map_cons, List.map_nil, Sequence.isWeaklyRegular_cons_iff] at hxy' hyx'
  have hbasic {r : R} (hr : r ∈ maximalIdeal R) :
      X.basicOpen (algebraMap R Γ(X, ⊤) r) ≤
        p ⁻¹ᵁ Scheme.puncturedSpectrumOpen R := by
    change X.basicOpen (p.appTop ((Scheme.ΓSpecIso (.of R)).inv r)) ≤ _
    rw [← Scheme.preimage_basicOpen_top, basicOpen_eq_of_affine]
    apply Scheme.Hom.preimage_mono p
    intro q hq
    apply (Scheme.mem_puncturedSpectrumOpen_iff R q).mpr
    intro hqclosed
    subst q
    exact hq hr
  apply restrict_bijective_of_regular_pair X
    (algebraMap R Γ(X, ⊤) x) (algebraMap R Γ(X, ⊤) y)
    hxy'.1 hyx'.1 hxy'.2.1
    (p ⁻¹ᵁ Scheme.puncturedSpectrumOpen R)
    (NoetherianSpace.isCompact _) ?_ (hbasic hxmem) (hbasic hymem)
  intro A B _ _ _ _ _ _
  exact NoetherianSpace.isCompact _

theorem isIso_punctured_finiteFlat_inclusion_appTop_of_two_le_depth
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (hdepth : (2 : ℕ∞) ≤ Module.depth R R)
    {X : Scheme.{u}} (p : X ⟶ Spec (.of R)) [IsFinite p] [Flat p] :
    IsIso (p ⁻¹ᵁ Scheme.puncturedSpectrumOpen R).ι.appTop