From 350cdba845af0ab734171f1151bfeb1bd3f8ce3f Mon Sep 17 00:00:00 2001 From: NoneMore Date: Fri, 26 Dec 2025 18:11:27 +0800 Subject: [PATCH] feat: add Stone duality theorem for clopen sets in complete types --- Mathlib/ModelTheory/Topology/Types.lean | 21 +++++++++++++++++++++ Mathlib/ModelTheory/Types.lean | 11 +++++++++++ 2 files changed, 32 insertions(+) diff --git a/Mathlib/ModelTheory/Topology/Types.lean b/Mathlib/ModelTheory/Topology/Types.lean index 13c36954e85933..f403ec21a9ba83 100644 --- a/Mathlib/ModelTheory/Topology/Types.lean +++ b/Mathlib/ModelTheory/Topology/Types.lean @@ -95,6 +95,27 @@ instance : CompactSpace (T.CompleteType α) := by obtain ⟨_, rfl⟩ := h.2 exact h.1 +/-- +Stone Duality: +Every clopen set in the Stone space of types corresponds to the set of types +consistent with some sentence φ. +-/ +theorem exists_sentence_of_isClopen (U : Set (CompleteType T α)) : + IsClopen U → ∃ (φ : L[[α]].Sentence), U = typesWith (T := T) φ := by + intro hU + obtain ⟨ι,S,hUS,hS⟩ := IsTopologicalBasis.open_eq_iUnion typesWith_basis hU.2 + obtain ⟨F,hF⟩ := IsCompact.elim_finite_subcover hU.1.isCompact S + (fun i => IsTopologicalBasis.isOpen typesWith_basis (hS i)) + (hUS.subset) + replace hF : U = ⋃ i ∈ F, S i := Subset.antisymm hF (by + rw [hUS] + exact iUnion₂_subset_iUnion (Membership.mem F) S + ) + choose φs hφs using hS + exists Formula.iSup (fun (x : F) => φs x.1) + simp [typesWith_iSup, hF, hφs] + exact Eq.symm (iUnion_subtype (Membership.mem F) fun x ↦ S ↑x) + instance : BaireSpace (T.CompleteType α) := BaireSpace.of_t2Space_locallyCompactSpace end CompleteType diff --git a/Mathlib/ModelTheory/Types.lean b/Mathlib/ModelTheory/Types.lean index a26b4362191c41..8815dc282c00be 100644 --- a/Mathlib/ModelTheory/Types.lean +++ b/Mathlib/ModelTheory/Types.lean @@ -193,6 +193,17 @@ lemma typesWith_inf (φ ψ : L[[α]].Sentence) simp only [p.isMaximal.mem_iff_models, ModelsBoundedFormula, ←forall_and] exact forall₃_congr fun _ _ _ ↦ BoundedFormula.realize_inf +lemma typesWith_iSup {β : Type*} [Finite β] (f : β → L[[α]].Sentence) : + typesWith (T := T) (Formula.iSup f) = ⋃ (i : β), typesWith (f i) := by + ext p + simp only [typesWith, Set.mem_setOf_eq, Set.mem_iUnion] + obtain ⟨M⟩ := p.isMaximal'.1 + have : ∀ φ, φ ∈ ↑p ↔ φ.Realize M.Carrier := by + intro φ + simp [←SetLike.mem_coe, p.isMaximal.mem_iff_models] + exact (p.isMaximal.isComplete.realize_sentence_iff φ M).symm + simp only [this, Sentence.Realize, Formula.realize_iSup] + lemma typesWith_mem {φ} (hφ : φ ∈ (L.lhomWithConstants α).onTheory T) : typesWith (T := T) φ = Set.univ := univ_subset_iff.mp fun p _ ↦ p.subset hφ