PuncturedSpectrumHypersurfaceComponents.lean

theorem irreducibleComponent_inter_subset_partition_side
    {X : Type u} [TopologicalSpace X]
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X)
    {U A B : Set X} (hA : IsOpen A) (hB : IsOpen B)
    (hcover : A ∪ B = U) (hdisjoint : Disjoint A B) :
    Z ∩ U ⊆ A ∨ Z ∩ U ⊆ B

theorem inter_subset_compl_of_component_partition_sides
    {X : Type u} {Z W U A B : Set X}
    (hZ : Z ∩ U ⊆ A) (hW : W ∩ U ⊆ B)
    (hdisjoint : Disjoint A B) :
    Z ∩ W ⊆ Uᶜ

theorem minimalPrime_span_singleton_ne_maximalIdeal
    {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]
    (hdim : ((3 : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C)
    (x : C) (P : Ideal C) (hP : P ∈ (Ideal.span {x}).minimalPrimes) :
    P ≠ maximalIdeal C

theorem minimalPrime_quotient_span_singleton_ne_maximalIdeal
    {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]
    (hdim : ((3 : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C)
    (x : C) (hx : x ∈ maximalIdeal C)
    (Q : Ideal (C ⧸ Ideal.span {x}))
    (hQ : Q ∈ minimalPrimes (C ⧸ Ideal.span {x})) :
    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
    Q ≠ maximalIdeal (C ⧸ Ideal.span {x}) := by
  let I : Ideal C := Ideal.span {x}
  let q : C →+* C ⧸ I := Ideal.Quotient.mk I
  have hIle : I ≤ maximalIdeal C :=
    (maximalIdeal C).span_singleton_le_iff_mem.mpr hx
  let : Nontrivial (C ⧸ I) :=
    Ideal.Quotient.nontrivial_iff.mpr <|
      ne_top_of_le_ne_top (maximalIdeal.isMaximal C).ne_top hIle
  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 := Ideal.minimalPrimes_comap_of_surjective
      Ideal.Quotient.mk_surjective hQ'
    simpa only [← RingHom.ker_eq_comap_bot, q, Ideal.mk_ker] using this
  intro hQmax
  apply minimalPrime_span_singleton_ne_maximalIdeal hdim x (Q.comap q) hcomap
  rw [hQmax]
  exact IsLocalRing.maximalIdeal_comap q

theorem irreducibleComponent_quotient_span_singleton_inter_puncture_nonempty
    {C : Type u} [CommRing C] [IsLocalRing C] [IsNoetherianRing C]
    (hdim : ((3 : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim C)
    (x : C) (hx : x ∈ maximalIdeal C)
    (Z : Set (PrimeSpectrum (C ⧸ Ideal.span {x})))
    (hZ : Z ∈ irreducibleComponents (PrimeSpectrum (C ⧸ Ideal.span {x}))) :
    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
    (Z ∩ ({closedPoint (C ⧸ Ideal.span {x})}ᶜ :
      Set (PrimeSpectrum (C ⧸ Ideal.span {x})))).Nonempty := by
  let B := C ⧸ Ideal.span {x}
  let : Nontrivial B :=
    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 B :=
    IsLocalRing.of_surjective'
      (Ideal.Quotient.mk (Ideal.span {x})) Ideal.Quotient.mk_surjective
  let Q : Ideal B := PrimeSpectrum.vanishingIdeal Z
  have hQ : Q ∈ minimalPrimes B := by
    rw [← PrimeSpectrum.vanishingIdeal_irreducibleComponents B]
    exact ⟨Z, hZ, rfl⟩
  let : Q.IsPrime := hQ.isPrime
  let q : PrimeSpectrum B := ⟨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 B := by
    intro hq
    apply minimalPrime_quotient_span_singleton_ne_maximalIdeal hdim x hx Q hQ
    exact congrArg PrimeSpectrum.asIdeal hq
  refine ⟨q, hqZ, ?_⟩
  simpa only [Set.mem_compl_iff, Set.mem_singleton_iff] using hqne