PuncturedSpectrumCompleteLocalIntersectionFrontier.lean

theorem ideal_height_radical_eq
    {R : Type u} [CommRing R] (I : Ideal R) :
    I.radical.height = I.height

theorem ideal_height_eq_ringKrullDim_of_radical_eq_maximalIdeal
    {R : Type u} [CommRing R] [IsLocalRing R]
    (I : Ideal R) (hI : I.radical = maximalIdeal R) :
    ((I.height : ℕ∞) : WithBot ℕ∞) = ringKrullDim R

theorem exists_height_one_minimalPrime_pair_of_not_connectedSpace
    {C : Type u} [CommRing C] [IsDomain C] [IsLocalRing C]
    [IsNoetherianRing C]
    (hdim : ((3 : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C)
    (x : C) (hx : x ∈ maximalIdeal C) :
    letI : Nontrivial (C ⧸ Ideal.span {x}) :=
      Ideal.Quotient.nontrivial_iff.mpr <|
        ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top <|
          (maximalIdeal C).span_singleton_le_iff_mem.mpr hx
    letI : IsLocalRing (C ⧸ Ideal.span {x}) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk (Ideal.span {x}))
        Ideal.Quotient.mk_surjective
    ¬ ConnectedSpace (Scheme.puncturedSpectrum (C ⧸ Ideal.span {x})) →
      x ≠ 0 ∧
        ∃ P Q : Ideal C,
          P ∈ (Ideal.span {x}).minimalPrimes ∧
          Q ∈ (Ideal.span {x}).minimalPrimes ∧
          P ≠ maximalIdeal C ∧ Q ≠ maximalIdeal C ∧
          P ≠ Q ∧ P.height = 1 ∧ Q.height = 1 ∧
          (P ⊔ Q).radical = maximalIdeal C ∧
          ((P ⊔ Q).height : WithBot ℕ∞) = ringKrullDim C ∧
          (3 : ℕ∞) ≤ (P ⊔ Q).height := by
  let D := C ⧸ Ideal.span {x}
  let : Nontrivial D :=
    Ideal.Quotient.nontrivial_iff.mpr <|
      ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top <|
        (maximalIdeal C).span_singleton_le_iff_mem.mpr hx
  let : IsLocalRing D :=
    IsLocalRing.of_surjective'
      (Ideal.Quotient.mk (Ideal.span {x})) Ideal.Quotient.mk_surjective
  intro hnot
  obtain ⟨hx0, P, Q, hP, hQ, hPMax, hQMax, hPheight, hQheight,
      hPQ⟩ :=
    exists_height_le_one_minimalPrime_pair_of_not_connectedSpace
      hdim x hx hnot
  let : P.IsPrime := hP.isPrime
  let : Q.IsPrime := hQ.isPrime
  have hspanHeight : 1 ≤ (Ideal.span {x}).height :=
    Ideal.one_le_height_span_singleton_of_mem_nonZeroDivisors
      (mem_nonZeroDivisors_iff_ne_zero.mpr hx0)
  have hPheight' : P.height = 1 :=
    le_antisymm hPheight (hspanHeight.trans (Ideal.height_mono hP.le))
  have hQheight' : Q.height = 1 :=
    le_antisymm hQheight (hspanHeight.trans (Ideal.height_mono hQ.le))
  have hPneQ : P ≠ Q := by
    intro h
    apply hPMax
    subst Q
    simpa only [sup_idem, hP.isPrime.isRadical.radical] using hPQ
  have hSupHeight :
      (((P ⊔ Q).height : ℕ∞) : WithBot ℕ∞) = ringKrullDim C :=
    ideal_height_eq_ringKrullDim_of_radical_eq_maximalIdeal (P ⊔ Q) hPQ
  have hThree : (3 : ℕ∞) ≤ (P ⊔ Q).height := by
    have hdim' := hdim
    rw [← hSupHeight] at hdim'
    exact WithBot.coe_le_coe.mp hdim'
  exact ⟨hx0, P, Q, hP, hQ, hPMax, hQMax, hPneQ,
    hPheight', hQheight', hPQ, hSupHeight, hThree⟩

theorem ideal_height_sup_le_two_of_isPrincipal
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    (P Q : Ideal R) (hP : P.IsPrincipal) (hQ : Q.IsPrincipal)
    (hPQ : P ⊔ Q ≠ ⊤) :
    (P ⊔ Q).height ≤ 2

theorem ideal_height_sup_le_two_of_height_one_of_uniqueFactorizationMonoid
    {R : Type u} [CommRing R] [IsDomain R] [IsNoetherianRing R]
    [UniqueFactorizationMonoid R]
    (P Q : Ideal R) [P.IsPrime] [Q.IsPrime]
    (hP : P.height = 1) (hQ : Q.height = 1)
    (hPQ : P ⊔ Q ≠ ⊤) :
    (P ⊔ Q).height ≤ 2

theorem connectedSpace_puncturedSpectrum_quotient_span_singleton_of_ufd
    {C : Type u} [CommRing C] [IsDomain C] [IsLocalRing C]
    [IsNoetherianRing C] [UniqueFactorizationMonoid C]
    (hdim : ((3 : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C)
    (x : C) (hx : x ∈ maximalIdeal C) :
    letI : Nontrivial (C ⧸ Ideal.span {x}) :=
      Ideal.Quotient.nontrivial_iff.mpr <|
        ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top <|
          (maximalIdeal C).span_singleton_le_iff_mem.mpr hx
    letI : IsLocalRing (C ⧸ Ideal.span {x}) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk (Ideal.span {x}))
        Ideal.Quotient.mk_surjective
    ConnectedSpace
      (Scheme.puncturedSpectrum (C ⧸ Ideal.span {x})) := by
  let D := C ⧸ Ideal.span {x}
  let : Nontrivial D :=
    Ideal.Quotient.nontrivial_iff.mpr <|
      ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top <|
        (maximalIdeal C).span_singleton_le_iff_mem.mpr hx
  let : IsLocalRing D :=
    IsLocalRing.of_surjective'
      (Ideal.Quotient.mk (Ideal.span {x})) Ideal.Quotient.mk_surjective
  by_contra hnot
  obtain ⟨_hx0, P, Q, _hP, _hQ, _hPMax, _hQMax, _hPneQ,
      hPheight, hQheight, hPQ, _hSupHeight, hThree⟩ :=
    exists_height_one_minimalPrime_pair_of_not_connectedSpace
      hdim x hx hnot
  let : P.IsPrime := _hP.isPrime
  let : Q.IsPrime := _hQ.isPrime
  have hProper : P ⊔ Q ≠ ⊤ := by
    intro htop
    apply (maximalIdeal.isMaximal C).ne_top
    simp only [← hPQ, htop, Ideal.radical_top]
  have hTwo : (P ⊔ Q).height ≤ 2 :=
    ideal_height_sup_le_two_of_height_one_of_uniqueFactorizationMonoid
      P Q hPheight hQheight hProper
  have : (3 : ℕ∞) ≤ 2 := hThree.trans hTwo
  norm_num at this