English
A subset s of PrimeSpectrum R is constructible iff there exists a ConstructibleSetData S over R with S.toSet = s.
Русский
Подмножество s спектра простых кольца R конструктивно тогда и только тогда, когда существует ConstructibleSetData S над R такое, что S.toSet = s.
LaTeX
$$$\bigl(\exists S : ConstructibleSetData R, S.toSet = s\bigr) \iff IsConstructible(s)$$
Lean4
theorem exists_constructibleSetData_iff {s : Set (PrimeSpectrum R)} :
(∃ S : ConstructibleSetData R, S.toSet = s) ↔ IsConstructible s :=
by
refine ⟨fun ⟨S, H⟩ ↦ H ▸ S.isConstructible_toSet, fun H ↦ ?_⟩
induction s, H using IsConstructible.induction_of_isTopologicalBasis _ (isTopologicalBasis_basic_opens (R := R)) with
| isCompact_basis i => exact isCompact_basicOpen _
| sdiff i s hs =>
have : Finite s := hs
refine ⟨{⟨i, Nat.card s, fun i ↦ ((Finite.equivFin s).symm i).1⟩}, ?_⟩
simp only [ConstructibleSetData.toSet, Finset.mem_singleton, BasicConstructibleSetData.toSet,
Set.iUnion_iUnion_eq_left, basicOpen_eq_zeroLocus_compl, ← Set.compl_iInter₂, compl_sdiff_compl,
← zeroLocus_iUnion₂, Set.biUnion_of_singleton]
congr! 2
ext
simp [← (Finite.equivFin s).exists_congr_right, -Nat.card_coe_set_eq]
| union s hs t ht Hs Ht =>
obtain ⟨S, rfl⟩ := Hs
obtain ⟨T, rfl⟩ := Ht
refine ⟨S ∪ T, ?_⟩
simp only [ConstructibleSetData.toSet, Set.biUnion_union, ← Finset.mem_coe, Finset.coe_union]
