AlgebraicGeometry.FiniteEtale.exists_minimalPrime_partition_of_open_puncture_partition
An open separation of a punctured principal hypersurface produces two finite nonempty families of minimal primes covering all minimal primes, with cross-component intersections supported at the closed point.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe uLean source · full declaration
theorem exists_minimalPrime_partition_of_open_puncture_partition
{C : Type u} [CommRing 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
∀ {A₀ B₀ : Set (PrimeSpectrum (C ⧸ Ideal.span {x}))},
IsOpen A₀ → IsOpen B₀ →
A₀ ∪ B₀ =
({closedPoint (C ⧸ Ideal.span {x})}ᶜ :
Set (PrimeSpectrum (C ⧸ Ideal.span {x}))) →
Disjoint A₀ B₀ → A₀.Nonempty → B₀.Nonempty →
∃ S T : Set (Ideal (C ⧸ Ideal.span {x})),
S.Nonempty ∧ T.Nonempty ∧
S.Finite ∧ T.Finite ∧
S ∪ T = minimalPrimes (C ⧸ Ideal.span {x}) ∧
Disjoint S T ∧
∀ P ∈ S, ∀ Q ∈ T,
PrimeSpectrum.zeroLocus P ∩ PrimeSpectrum.zeroLocus Q ⊆
({closedPoint (C ⧸ Ideal.span {x})} :
Set (PrimeSpectrum (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
intro A₀ B₀ hAopen hBopen hcover hdisjoint hAnonempty hBnonempty
let U : Set (PrimeSpectrum D) := {closedPoint D}ᶜ
let S : Set (Ideal D) :=
{P | P ∈ minimalPrimes D ∧ PrimeSpectrum.zeroLocus P ∩ U ⊆ A₀}
let T : Set (Ideal D) :=
{P | P ∈ minimalPrimes D ∧ PrimeSpectrum.zeroLocus P ∩ U ⊆ B₀}
have hcomponent (P : Ideal D) (hP : P ∈ minimalPrimes D) :
PrimeSpectrum.zeroLocus P ∈ irreducibleComponents (PrimeSpectrum D) := by
rw [PrimeSpectrum.zeroLocus_ideal_mem_irreducibleComponents]
simpa only [(hP.isPrime.isRadical.radical)] using hP
have hcomponentMeets (P : Ideal D) (hP : P ∈ minimalPrimes D) :
(PrimeSpectrum.zeroLocus P ∩ U).Nonempty := by
exact irreducibleComponent_quotient_span_singleton_inter_puncture_nonempty
hdim x hx (PrimeSpectrum.zeroLocus P) (hcomponent P hP)
have hside (P : Ideal D) (hP : P ∈ minimalPrimes D) : P ∈ S ∨ P ∈ T := by
have hsides := irreducibleComponent_inter_subset_partition_side
(PrimeSpectrum.zeroLocus P) (hcomponent P hP)
hAopen hBopen hcover hdisjoint
exact hsides.imp (fun h ↦ ⟨hP, h⟩) (fun h ↦ ⟨hP, h⟩)
have hSnonempty : S.Nonempty := by
obtain ⟨a, haA⟩ := hAnonempty
have haU : a ∈ U := by
change a ∈ ({closedPoint D}ᶜ : Set (PrimeSpectrum D))
rw [← hcover]
exact Or.inl haA
obtain ⟨P, hP, hPa⟩ :=
Ideal.exists_minimalPrimes_le (I := (⊥ : Ideal D))
(J := a.asIdeal) bot_le
rcases hside P hP with hPS | hPT
· exact ⟨P, hPS⟩
· exfalso
exact Set.disjoint_left.mp hdisjoint haA
(hPT.2 ⟨hPa, haU⟩)
have hTnonempty : T.Nonempty := by
obtain ⟨b, hbB⟩ := hBnonempty
have hbU : b ∈ U := by
change b ∈ ({closedPoint D}ᶜ : Set (PrimeSpectrum D))
rw [← hcover]
exact Or.inr hbB
obtain ⟨Q, hQ, hQb⟩ :=
Ideal.exists_minimalPrimes_le (I := (⊥ : Ideal D))
(J := b.asIdeal) bot_le
rcases hside Q hQ with hQS | hQT
· exfalso
exact Set.disjoint_left.mp hdisjoint
(hQS.2 ⟨hQb, hbU⟩) hbB
· exact ⟨Q, hQT⟩
have hSfinite : S.Finite :=
(minimalPrimes.finite_of_isNoetherianRing D).subset fun _ h ↦ h.1
have hTfinite : T.Finite :=
(minimalPrimes.finite_of_isNoetherianRing D).subset fun _ h ↦ h.1
have hSTcover : S ∪ T = minimalPrimes D := by
apply Set.Subset.antisymm
· exact fun _ h ↦ h.elim (fun h ↦ h.1) (fun h ↦ h.1)
· intro P hP
exact hside P hP
have hSTdisjoint : Disjoint S T := by
rw [Set.disjoint_left]
intro P hPS hPT
obtain ⟨p, hpPU⟩ := hcomponentMeets P hPS.1
exact Set.disjoint_left.mp hdisjoint
(hPS.2 hpPU) (hPT.2 hpPU)
refine ⟨S, T, hSnonempty, hTnonempty, hSfinite, hTfinite,
hSTcover, hSTdisjoint, ?_⟩
intro P hPS Q hQT p hp
have hpNotU : p ∉ U := by
intro hpU
exact Set.disjoint_left.mp hdisjoint
(hPS.2 ⟨hp.1, hpU⟩) (hQT.2 ⟨hp.2, hpU⟩)
simpa only [U, Set.mem_compl_iff, Set.mem_singleton_iff, not_not]
using hpNotU