Compactness Proof

Author: anishrajeev

Mathlib/ModelTheory/Topology/Types.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Jonas van der Schaaf. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jonas van der Schaaf
+Authors: Jonas van der Schaaf, Anish Rajeev
 -/
 
 module
@@ -66,5 +66,33 @@ instance : TotallySeparatedSpace (CompleteType T α) := by
         by change ¬∼φ∈q; rwa [not_mem_iff,←hφ, not_not, ←not_mem_iff]
       ⟩)
 
+instance {n : ℕ} : CompactSpace (T.CompleteType (Fin n)) := by
+  constructor
+  rw[isCompact_iff_ultrafilter_le_nhds]
+  intros F _
+  refine ⟨⟨{φ | typesWith φ ∈ F}, ?_, ?_⟩, ?_⟩
+  · intro φ x
+    exact F.mem_of_superset Filter.univ_mem (fun p _ ↦ p.subset x)
+  · rw [Theory.IsMaximal, Theory.isSatisfiable_iff_isFinitelySatisfiable]
+    refine ⟨?_, ?_⟩
+    · rw[Theory.IsFinitelySatisfiable]
+      intro x hx
+      have : ∀ φ ∈ x, typesWith φ ∈ F.toFilter := by intro φ hφ ; exact hx hφ
+      rw[←Filter.biInter_finset_mem x] at this
+      obtain ⟨T, T_inter⟩ := F.neBot.nonempty_of_mem this
+      have subset : SetLike.coe x ⊆ T.toTheory := by rwa[Set.mem_iInter₂] at T_inter
+      exact Theory.IsSatisfiable.mono T.isMaximal'.1 subset
+    · intro φ
+      simp [mem_setOf_eq, typesWith_compl]
+      exact Ultrafilter.mem_or_compl_mem F (typesWith φ)
+  · refine ⟨trivial, ?_⟩
+    · rw [nhds_generateFrom]
+      apply le_iInf₂
+      intro _ h
+      rw [Filter.le_principal_iff]
+      obtain ⟨_, rfl⟩ := h.2
+      exact h.1
+
+instance {n : ℕ} : BaireSpace (T.CompleteType (Fin n)) := BaireSpace.of_t2Space_locallyCompactSpace
 
 end CompleteType

Mathlib/ModelTheory/Types.lean

@@ -237,120 +237,6 @@ theorem exists_modelType_is_realized_in (p : T.CompleteType α) :
 
 end
 
-namespace TypeSpace
-
-variable {T : L.Theory}
-
-/-- Defines the basis for the Type Space and defines a function from formulas to basic
-  clopen sets -/
-def basis {n : ℕ} : Set (Set (T.CompleteType (Fin n))) := {U | ∃ φ, U = {s | φ ∈ s}}
-/-- Clopen balls indexed by the sentence φ -/
-def BasicOpen {n : ℕ} (φ : L[[Fin n]].Sentence) : Set (T.CompleteType (Fin n)) :=
-  {s : T.CompleteType (Fin n) | φ ∈ s}
-
-lemma finite_inter {n : ℕ} : FiniteInter (α := T.CompleteType (Fin n)) basis := by
-  constructor
-  · use ⊤
-    ext x
-    simp
-    exact Theory.CompleteType.mem_of_models x (fun _ _ _ a ↦ a)
-  · rintro s ⟨φ, rfl⟩ t ⟨ψ, rfl⟩
-    use φ ⊓ ψ
-    ext t
-    simp
-    simp_rw[← SetLike.mem_coe, t.isMaximal.mem_iff_models (φ ⊓ ψ), t.isMaximal.mem_iff_models φ,
-            t.isMaximal.mem_iff_models ψ, Theory.models_sentence_iff]
-    constructor
-    · rintro ⟨a, b⟩ M
-      exact Formula.realize_inf.2 ⟨a M, b M⟩
-    · intro a
-      rw [←forall_and]
-      intro M
-      exact Formula.realize_inf.1 (a M)
-
-lemma basic_open_compl {n : ℕ} (T : L.Theory) (φ : L[[Fin n]].Sentence) :
-                       BasicOpen (T := T) φ.not = (BasicOpen φ)ᶜ := by
-                          ext p; exact p.not_mem_iff φ
-
-instance (n : ℕ) : TopologicalSpace (T.CompleteType (Fin n)) := generateFrom basis
-
-instance {n : ℕ} : T0Space (T.CompleteType (Fin n)) := by
-  rw [t0Space_iff_inseparable]
-  intro x y a
-  apply SetLike.ext
-  intro φ
-  replace h := inseparable_iff_forall_isOpen.1 a
-  have b : IsOpen (X := (T.CompleteType (Fin n))) (BasicOpen φ) := by
-    apply TopologicalSpace.GenerateOpen.basic
-    use φ; trivial
-  exact h (BasicOpen φ) b
-
-instance {n : ℕ} : TotallySeparatedSpace (T.CompleteType (Fin n)) := by
-  apply totallySeparatedSpace_of_t0_of_basis_clopen
-  have a := isTopologicalBasis_of_subbasis_of_finiteInter
-            (α := T.CompleteType (Fin n)) (s := basis) (by trivial) finite_inter
-  apply IsTopologicalBasis.of_isOpen_of_subset
-  · intro _ h; exact h.2
-  · exact a
-  · intro s ⟨φ, b⟩
-    constructor
-    · have h : IsOpen sᶜ := by
-        replace b : s = BasicOpen φ := b
-        rw[b, ←basic_open_compl]
-        apply TopologicalSpace.GenerateOpen.basic
-        exact ⟨φ.not, by trivial⟩
-      rw[←compl_compl s]
-      exact isClosed_compl_iff.2 h
-    · apply TopologicalSpace.GenerateOpen.basic; use φ
-
-instance {n : ℕ} : T2Space (T.CompleteType (Fin n)) := TotallySeparatedSpace.t2Space
-
-instance {n : ℕ} : CompactSpace (T.CompleteType (Fin n)) := by
-  constructor
-  rw[isCompact_iff_ultrafilter_le_nhds]
-  intros F _
-  let x : L[[Fin n]].Theory := {φ | BasicOpen φ ∈ F}
-  have a : (L.lhomWithConstants (Fin n)).onTheory T ⊆ x := by
-    intro φ a
-    have b : BasicOpen (T := T) φ = Set.univ := by
-      ext y
-      simp
-      exact y.subset a
-    rw[Set.mem_setOf_eq, b]
-    exact Filter.univ_mem
-  have b : Theory.IsMaximal x := by
-    rw[Theory.IsMaximal]
-    constructor
-    · rw[Theory.isSatisfiable_iff_isFinitelySatisfiable, Theory.IsFinitelySatisfiable]
-      intro φᵢ a
-      have b : ∀ φ ∈ φᵢ, BasicOpen φ ∈ F.toFilter := by
-        intro _ b
-        exact a b
-      rw[←Filter.biInter_finset_mem φᵢ] at b
-      obtain ⟨y, c⟩ := F.neBot.nonempty_of_mem b
-      have d : SetLike.coe φᵢ ⊆ y.toTheory := by
-        rwa[Set.mem_iInter₂] at c
-      exact Theory.IsSatisfiable.mono y.isMaximal'.1 d
-    · intro φ
-      rcases Ultrafilter.mem_or_compl_mem F (BasicOpen φ) with  a | b
-      · exact Or.inl a
-      · rw[←basic_open_compl T φ] at b
-        exact Or.inr b
-  let p : T.CompleteType (Fin n) := ⟨x, a, b⟩
-  use p
-  constructor
-  · trivial
-  · rw [nhds_generateFrom]
-    apply le_iInf₂
-    intro _ a
-    simp
-    obtain ⟨_, rfl⟩ := a.2
-    exact a.1
-
-instance {n : ℕ} : BaireSpace (T.CompleteType (Fin n)) := BaireSpace.of_t2Space_locallyCompactSpace
-
-end TypeSpace
-
 end Theory
 
 end Language