PuncturedSpectrumCompleteLocalOfListFrontier.lean

theorem height_le_length_of_mem_minimalPrimes_ofList
    {C : Type u} [CommRing C] [IsNoetherianRing C]
    (xs : List C) (P : Ideal C)
    (hP : P ∈ (Ideal.ofList xs).minimalPrimes) :
    P.height ≤ xs.length

theorem minimalPrime_ofList_ne_maximalIdeal
    {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]
    (xs : List C)
    (hdim :
      ((((xs.length + 2 : ℕ) : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C))
    (P : Ideal C) (hP : P ∈ (Ideal.ofList xs).minimalPrimes) :
    P ≠ maximalIdeal C

theorem minimalPrime_quotient_ofList_ne_maximalIdeal
    {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]
    (I : Ideal C) (hI : I ≤ maximalIdeal C)
    (xs : List C) (hxs : I = Ideal.ofList xs)
    (hdim :
      ((((xs.length + 2 : ℕ) : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C))
    (Q : Ideal (C ⧸ I)) (hQ : Q ∈ minimalPrimes (C ⧸ I)) :
    letI : Nontrivial (C ⧸ I) :=
      Ideal.Quotient.nontrivial_iff.mpr <|
        ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hI
    letI : IsLocalRing (C ⧸ I) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
        Ideal.Quotient.mk_surjective
    Q ≠ maximalIdeal (C ⧸ I) := by
  let q : C →+* C ⧸ I := Ideal.Quotient.mk I
  let : Nontrivial (C ⧸ I) :=
    Ideal.Quotient.nontrivial_iff.mpr <|
      ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hI
  let : IsLocalRing (C ⧸ I) :=
    IsLocalRing.of_surjective' q Ideal.Quotient.mk_surjective
  let : IsLocalHom q :=
    IsLocalHom.of_surjective q Ideal.Quotient.mk_surjective
  have hcomap : Q.comap q ∈ I.minimalPrimes := by
    have hQ' : Q ∈ (⊥ : Ideal (C ⧸ I)).minimalPrimes := hQ
    have h := Ideal.minimalPrimes_comap_of_surjective
      Ideal.Quotient.mk_surjective hQ'
    simpa only [← RingHom.ker_eq_comap_bot, q, Ideal.mk_ker] using h
  have hcomap' : Q.comap q ∈ (Ideal.ofList xs).minimalPrimes := by
    simpa only [← hxs] using hcomap
  intro hQmax
  apply minimalPrime_ofList_ne_maximalIdeal xs hdim (Q.comap q) hcomap'
  rw [hQmax]
  exact IsLocalRing.maximalIdeal_comap q

theorem irreducibleComponent_quotient_ofList_inter_puncture_nonempty
    {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]
    (I : Ideal C) (hI : I ≤ maximalIdeal C)
    (xs : List C) (hxs : I = Ideal.ofList xs)
    (hdim :
      ((((xs.length + 2 : ℕ) : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C))
    (Z : Set (PrimeSpectrum (C ⧸ I)))
    (hZ : Z ∈ irreducibleComponents (PrimeSpectrum (C ⧸ I))) :
    letI : Nontrivial (C ⧸ I) :=
      Ideal.Quotient.nontrivial_iff.mpr <|
        ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hI
    letI : IsLocalRing (C ⧸ I) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
        Ideal.Quotient.mk_surjective
    (Z ∩ ({closedPoint (C ⧸ I)}ᶜ :
      Set (PrimeSpectrum (C ⧸ I)))).Nonempty := by
  let D := C ⧸ I
  let : Nontrivial D :=
    Ideal.Quotient.nontrivial_iff.mpr <|
      ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hI
  let : IsLocalRing D :=
    IsLocalRing.of_surjective'
      (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective
  let Q : Ideal D := PrimeSpectrum.vanishingIdeal Z
  have hQ : Q ∈ minimalPrimes D := by
    rw [← PrimeSpectrum.vanishingIdeal_irreducibleComponents D]
    exact ⟨Z, hZ, rfl⟩
  let : Q.IsPrime := hQ.isPrime
  let q : PrimeSpectrum D := ⟨Q, inferInstance⟩
  have hqZ : q ∈ Z := by
    have hclosed : IsClosed Z := isClosed_of_mem_irreducibleComponents Z hZ
    have hzero : PrimeSpectrum.zeroLocus Q = Z := by
      change PrimeSpectrum.zeroLocus (PrimeSpectrum.vanishingIdeal Z) = Z
      rw [PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure,
        hclosed.closure_eq]
    rw [← hzero]
    exact show Q ≤ q.asIdeal from le_rfl
  have hqne : q ≠ closedPoint D := by
    intro hq
    apply minimalPrime_quotient_ofList_ne_maximalIdeal
      I hI xs hxs hdim Q hQ
    exact congrArg PrimeSpectrum.asIdeal hq
  refine ⟨q, hqZ, ?_⟩
  simpa only [Set.mem_compl_iff, Set.mem_singleton_iff] using hqne

theorem exists_minimalPrime_partition_of_open_puncture_partition_of_components_meet
    {D : Type u} [CommRing D] [IsLocalRing D] [IsNoetherianRing D]
    (hcomponents : ∀ Z ∈ irreducibleComponents (PrimeSpectrum D),
      (Z ∩ ({closedPoint D}ᶜ : Set (PrimeSpectrum D))).Nonempty)
    {A₀ B₀ : Set (PrimeSpectrum D)}
    (hAopen : IsOpen A₀) (hBopen : IsOpen B₀)
    (hcover : A₀ ∪ B₀ =
      ({closedPoint D}ᶜ : Set (PrimeSpectrum D)))
    (hdisjoint : Disjoint A₀ B₀)
    (hAnonempty : A₀.Nonempty) (hBnonempty : B₀.Nonempty) :
    ∃ S T : Set (Ideal D),
      S.Nonempty ∧ T.Nonempty ∧ S.Finite ∧ T.Finite ∧
      S ∪ T = minimalPrimes D ∧ Disjoint S T ∧
      ∀ P ∈ S, ∀ Q ∈ T,
        PrimeSpectrum.zeroLocus P ∩ PrimeSpectrum.zeroLocus Q ⊆
          ({closedPoint D} : Set (PrimeSpectrum D))

theorem
exists_radical_nonmaximal_componentIntersectionIdeals_of_open_puncture_partition_of_components_meet
    {D : Type u} [CommRing D] [IsLocalRing D] [IsNoetherianRing D]
    (hcomponents : ∀ Z ∈ irreducibleComponents (PrimeSpectrum D),
      (Z ∩ ({closedPoint D}ᶜ : Set (PrimeSpectrum D))).Nonempty)
    {A₀ B₀ : Set (PrimeSpectrum D)}
    (hAopen : IsOpen A₀) (hBopen : IsOpen B₀)
    (hcover : A₀ ∪ B₀ =
      ({closedPoint D}ᶜ : Set (PrimeSpectrum D)))
    (hdisjoint : Disjoint A₀ B₀)
    (hAnonempty : A₀.Nonempty) (hBnonempty : B₀.Nonempty) :
    ∃ a b : Ideal D,
      a ≠ ⊤ ∧ b ≠ ⊤ ∧
      a ≠ maximalIdeal D ∧ b ≠ maximalIdeal D ∧
      a.IsRadical ∧ b.IsRadical ∧
      a ⊓ b = nilradical D ∧
      (a ⊔ b).radical = maximalIdeal D

theorem
exists_radical_nonmaximal_componentIntersectionIdeals_of_not_connectedSpace_of_components_meet
    {D : Type u} [CommRing D] [IsLocalRing D] [IsNoetherianRing D]
    (hcomponents : ∀ Z ∈ irreducibleComponents (PrimeSpectrum D),
      (Z ∩ ({closedPoint D}ᶜ : Set (PrimeSpectrum D))).Nonempty) :
    ¬ ConnectedSpace (Scheme.puncturedSpectrum D) →
      ∃ a b : Ideal D,
        a ≠ ⊤ ∧ b ≠ ⊤ ∧
        a ≠ maximalIdeal D ∧ b ≠ maximalIdeal D ∧
        a.IsRadical ∧ b.IsRadical ∧
        a ⊓ b = nilradical D ∧
        (a ⊔ b).radical = maximalIdeal D

theorem exists_radical_nonmaximal_componentIntersectionIdeals_of_not_connectedSpace_quotient_ofList
    {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]
    (I : Ideal C) (hI : I ≤ maximalIdeal C)
    (xs : List C) (hxs : I = Ideal.ofList xs)
    (hdim :
      ((((xs.length + 2 : ℕ) : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C)) :
    letI : Nontrivial (C ⧸ I) :=
      Ideal.Quotient.nontrivial_iff.mpr <|
        ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hI
    letI : IsLocalRing (C ⧸ I) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
        Ideal.Quotient.mk_surjective
    ¬ ConnectedSpace (Scheme.puncturedSpectrum (C ⧸ I)) →
      ∃ a b : Ideal (C ⧸ I),
        a ≠ ⊤ ∧ b ≠ ⊤ ∧
        a ≠ maximalIdeal (C ⧸ I) ∧
        b ≠ maximalIdeal (C ⧸ I) ∧
        a.IsRadical ∧ b.IsRadical ∧
        a ⊓ b = nilradical (C ⧸ I) ∧
        (a ⊔ b).radical = maximalIdeal (C ⧸ I) := by
  let : Nontrivial (C ⧸ I) :=
    Ideal.Quotient.nontrivial_iff.mpr <|
      ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hI
  let : IsLocalRing (C ⧸ I) :=
    IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective
  apply
    exists_radical_nonmaximal_componentIntersectionIdeals_of_not_connectedSpace_of_components_meet
  intro Z hZ
  exact irreducibleComponent_quotient_ofList_inter_puncture_nonempty
    I hI xs hxs hdim Z hZ

theorem
exists_radical_nonmaximal_ambient_componentIntersectionIdeals_of_not_connectedSpace_quotient_ofList
    {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]
    (I : Ideal C) (hI : I ≤ maximalIdeal C)
    (xs : List C) (hxs : I = Ideal.ofList xs)
    (hdim :
      ((((xs.length + 2 : ℕ) : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C)) :
    letI : Nontrivial (C ⧸ I) :=
      Ideal.Quotient.nontrivial_iff.mpr <|
        ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hI
    letI : IsLocalRing (C ⧸ I) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
        Ideal.Quotient.mk_surjective
    ¬ ConnectedSpace (Scheme.puncturedSpectrum (C ⧸ I)) →
      ∃ a b : Ideal C,
        I ≤ a ∧ I ≤ b ∧
        a ≠ ⊤ ∧ b ≠ ⊤ ∧
        a ≠ maximalIdeal C ∧ b ≠ maximalIdeal C ∧
        a.IsRadical ∧ b.IsRadical ∧
        a ⊓ b = I.radical ∧
        (a ⊔ b).radical = maximalIdeal C := by
  let D := C ⧸ I
  let q : C →+* D := Ideal.Quotient.mk I
  let : Nontrivial D :=
    Ideal.Quotient.nontrivial_iff.mpr <|
      ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hI
  let : IsLocalRing D :=
    IsLocalRing.of_surjective' q Ideal.Quotient.mk_surjective
  let : IsLocalHom q :=
    IsLocalHom.of_surjective q Ideal.Quotient.mk_surjective
  intro hnot
  obtain ⟨a, b, ha, hb, hamax, hbmax, haRadical, hbRadical,
      hinf, hradical⟩ :=
    exists_radical_nonmaximal_componentIntersectionIdeals_of_not_connectedSpace_quotient_ofList
      I hI xs hxs hdim hnot
  let A : Ideal C := a.comap q
  let B : Ideal C := b.comap q
  have hIA : I ≤ A := by
    rw [← Ideal.mk_ker (I := I), RingHom.ker_eq_comap_bot]
    exact Ideal.comap_mono bot_le
  have hIB : I ≤ B := by
    rw [← Ideal.mk_ker (I := I), RingHom.ker_eq_comap_bot]
    exact Ideal.comap_mono bot_le
  have hA : A ≠ ⊤ := Ideal.comap_ne_top q ha
  have hB : B ≠ ⊤ := Ideal.comap_ne_top q hb
  have hAmax : A ≠ maximalIdeal C := by
    intro h
    apply hamax
    calc
      a = A.map q :=
        (Ideal.map_comap_of_surjective q
          Ideal.Quotient.mk_surjective a).symm
      _ = (maximalIdeal C).map q := congrArg (Ideal.map q) h
      _ = maximalIdeal D :=
        IsLocalRing.map_maximalIdeal_of_surjective q
          Ideal.Quotient.mk_surjective
  have hBmax : B ≠ maximalIdeal C := by
    intro h
    apply hbmax
    calc
      b = B.map q :=
        (Ideal.map_comap_of_surjective q
          Ideal.Quotient.mk_surjective b).symm
      _ = (maximalIdeal C).map q := congrArg (Ideal.map q) h
      _ = maximalIdeal D :=
        IsLocalRing.map_maximalIdeal_of_surjective q
          Ideal.Quotient.mk_surjective
  have hARadical : A.IsRadical := haRadical.comap q
  have hBRadical : B.IsRadical := hbRadical.comap q
  have hABinf : A ⊓ B = I.radical := by
    calc
      A ⊓ B = Ideal.comap q (a ⊓ b) := (Ideal.comap_inf q a b).symm
      _ = Ideal.comap q (nilradical D) := by rw [hinf]
      _ = Ideal.comap q (Ideal.radical ⊥) := rfl
      _ = Ideal.radical (Ideal.comap q ⊥) := Ideal.comap_radical q ⊥
      _ = I.radical := by
        rw [← RingHom.ker_eq_comap_bot, Ideal.mk_ker]
  have hcomapSup : Ideal.comap q (a ⊔ b) = A ⊔ B := by
    calc
      Ideal.comap q (a ⊔ b) =
          Ideal.comap q ((A ⊔ B).map q) := by
        congr 1
        dsimp only [A, B]
        exact (Ideal.map_sup_comap_of_surjective q
          Ideal.Quotient.mk_surjective a b).symm
      _ = (A ⊔ B) ⊔ Ideal.comap q ⊥ :=
        Ideal.comap_map_of_surjective q Ideal.Quotient.mk_surjective (A ⊔ B)
      _ = A ⊔ B := by
        rw [sup_eq_left]
        exact (Ideal.comap_mono bot_le).trans le_sup_left
  have hABradical : (A ⊔ B).radical = maximalIdeal C := by
    have h := congrArg (Ideal.comap q) hradical
    rw [Ideal.comap_radical, hcomapSup,
      IsLocalRing.maximalIdeal_comap q] at h
    exact h
  exact ⟨A, B, hIA, hIB, hA, hB, hAmax, hBmax,
    hARadical, hBRadical, hABinf, hABradical⟩

theorem exists_radical_completeIntersectionPowerData_of_not_connectedSpace_quotient_ofList
    {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]
    (I : Ideal C) (hI : I ≤ maximalIdeal C)
    (xs : List C) (hxs : I = Ideal.ofList xs)
    (hdim :
      ((((xs.length + 2 : ℕ) : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C)) :
    letI : Nontrivial (C ⧸ I) :=
      Ideal.Quotient.nontrivial_iff.mpr <|
        ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hI
    letI : IsLocalRing (C ⧸ I) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
        Ideal.Quotient.mk_surjective
    ¬ ConnectedSpace (Scheme.puncturedSpectrum (C ⧸ I)) →
      ∃ a b : Ideal C, ∃ n k : ℕ,
        I ≤ a ∧ I ≤ b ∧
        a ≠ ⊤ ∧ b ≠ ⊤ ∧
        a ≠ maximalIdeal C ∧ b ≠ maximalIdeal C ∧
        a.IsRadical ∧ b.IsRadical ∧
        a ⊓ b = I.radical ∧
        (a ⊔ b).radical = maximalIdeal C ∧
        (maximalIdeal C) ^ n ≤ a ⊔ b ∧
        (a * b) ^ k ≤ I := by
  let : Nontrivial (C ⧸ I) :=
    Ideal.Quotient.nontrivial_iff.mpr <|
      ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hI
  let : IsLocalRing (C ⧸ I) :=
    IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective
  intro hnot
  obtain ⟨a, b, hIa, hIb, ha, hb, haMax, hbMax,
      haRadical, hbRadical, hinf, hsup⟩ :=
    (
exists_radical_nonmaximal_ambient_componentIntersectionIdeals_of_not_connectedSpace_quotient_ofList
      I hI xs hxs hdim hnot)
  obtain ⟨n, hn⟩ := exists_maximalIdeal_pow_le_of_radical_eq hsup
  obtain ⟨k, hk⟩ := exists_product_pow_le_of_inf_eq_radical hinf
  exact ⟨a, b, n, k, hIa, hIb, ha, hb, haMax, hbMax,
    haRadical, hbRadical, hinf, hsup, hn, hk⟩

theorem exists_bounded_minimalPrime_pair_of_not_connectedSpace_quotient_ofList
    {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]
    (I : Ideal C) (hI : I ≤ maximalIdeal C)
    (xs : List C) (hxs : I = Ideal.ofList xs)
    (hdim :
      ((((xs.length + 2 : ℕ) : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C)) :
    letI : Nontrivial (C ⧸ I) :=
      Ideal.Quotient.nontrivial_iff.mpr <|
        ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hI
    letI : IsLocalRing (C ⧸ I) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
        Ideal.Quotient.mk_surjective
    ¬ ConnectedSpace (Scheme.puncturedSpectrum (C ⧸ I)) →
      ∃ P Q : Ideal C,
        P ∈ I.minimalPrimes ∧ Q ∈ I.minimalPrimes ∧
        P ≠ maximalIdeal C ∧ Q ≠ maximalIdeal C ∧
        P ≠ Q ∧
        P.height ≤ xs.length ∧ Q.height ≤ xs.length ∧
        (P ⊔ Q).radical = maximalIdeal C ∧
        (((P ⊔ Q).height : ℕ∞) : WithBot ℕ∞) = ringKrullDim C ∧
        ((xs.length + 2 : ℕ) : ℕ∞) ≤ (P ⊔ Q).height := by
  let : Nontrivial (C ⧸ I) :=
    Ideal.Quotient.nontrivial_iff.mpr <|
      ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hI
  let : IsLocalRing (C ⧸ I) :=
    IsLocalRing.of_surjective' (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective
  intro hnot
  obtain ⟨a, b, _hIa, _hIb, _ha, _hb, haMax, hbMax,
      haRadical, hbRadical, hinf, hsup⟩ :=
    (
exists_radical_nonmaximal_ambient_componentIntersectionIdeals_of_not_connectedSpace_quotient_ofList
      I hI xs hxs hdim hnot)
  obtain ⟨P, Q, hP, hQ, _haP, _hbQ, hPMax, hQMax, hPQ⟩ :=
    exists_nonmaximal_minimalPrime_pair_of_radical_componentIntersection
      haRadical hbRadical haMax hbMax hinf hsup
  have hP' : P ∈ (Ideal.ofList xs).minimalPrimes := by
    simpa only [← hxs] using hP
  have hQ' : Q ∈ (Ideal.ofList xs).minimalPrimes := by
    simpa only [← hxs] using hQ
  have hPheight : P.height ≤ xs.length :=
    height_le_length_of_mem_minimalPrimes_ofList xs P hP'
  have hQheight : Q.height ≤ xs.length :=
    height_le_length_of_mem_minimalPrimes_ofList xs Q hQ'
  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 hLower : ((xs.length + 2 : ℕ) : ℕ∞) ≤ (P ⊔ Q).height := by
    have hdim' := hdim
    rw [← hSupHeight] at hdim'
    exact WithBot.coe_le_coe.mp hdim'
  exact ⟨P, Q, hP, hQ, hPMax, hQMax, hPneQ,
    hPheight, hQheight, hPQ, hSupHeight, hLower⟩