Merge remote-tracking branch 'jonas/typespace' into OmittingTypes

This PR depends on the PR in Jonas's branch.

Author: anishrajeev

Mathlib.lean

@@ -5107,6 +5107,7 @@ public import Mathlib.ModelTheory.Semantics
 public import Mathlib.ModelTheory.Skolem
 public import Mathlib.ModelTheory.Substructures
 public import Mathlib.ModelTheory.Syntax
+public import Mathlib.ModelTheory.Topology.Types
 public import Mathlib.ModelTheory.Types
 public import Mathlib.ModelTheory.Ultraproducts
 public import Mathlib.NumberTheory.ADEInequality

Mathlib/ModelTheory/Topology/Types.lean

@@ -0,0 +1,70 @@
+/-
+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
+-/
+
+module
+
+public import Mathlib.ModelTheory.Types
+public import Mathlib.Topology.Bases
+public import Mathlib.Topology.Connected.TotallyDisconnected
+public import Mathlib.Topology.Compactness.Compact
+
+/-!
+# Topology on the space of complete types
+
+This file defines a topological structure on the type `CompleteType T α` (note that
+these are types from model theory and not types from type theory). The topology
+is generated by sets of the form `{p : CompleteType T α | ∃ φ, φ ∈ p}`.
+
+Note that the contents of this file are separate from ModelTheory/Types.lean to avoid
+importing files from the Topology folder there.
+-/
+
+open Set FirstOrder Language Theory CompleteType TopologicalSpace
+
+namespace CompleteType
+
+universe u
+
+variable {L : Language} {T : L.Theory} {α : Type _}
+
+instance : TopologicalSpace (CompleteType T α) := generateFrom (range typesWith)
+
+public lemma typesWith_basis : IsTopologicalBasis (range (typesWith (α := α) (T := T))) where
+  exists_subset_inter := by
+    intro t₁ ⟨φ, ht₁⟩ t₂ ⟨ψ, ht₂⟩ x hx
+    refine ⟨typesWith (φ ⊓ ψ), ⟨φ ⊓ ψ, rfl⟩, ?_⟩
+    rw [typesWith_inf, ht₁, ht₂]
+    exact ⟨hx, fun _ ↦ id⟩
+  sUnion_eq := by
+    rw [←Set.univ_subset_iff]
+    exact Set.subset_sUnion_of_mem ⟨_, typesWith_top⟩
+  eq_generateFrom := rfl
+
+lemma typesWith_open (φ : (L[[α]]).Sentence) : IsOpen (typesWith (T := T) φ) :=
+  isOpen_generateFrom_of_mem ⟨φ, rfl⟩
+
+lemma typesWith_closed (φ : (L[[α]]).Sentence) : IsClosed (typesWith (T := T) φ) where
+  isOpen_compl := by rw [←typesWith_compl]; exact typesWith_open _
+
+lemma typesWith_clopen (φ : (L[[α]]).Sentence) : IsClopen (typesWith (T := T) φ) where
+  left := typesWith_closed _
+  right := typesWith_open _
+
+instance : TotallySeparatedSpace (CompleteType T α) := by
+  rw [totallySeparatedSpace_iff_exists_isClopen]
+  intro p q hpq
+  simp only [ne_eq, SetLike.ext_iff, not_forall, not_iff] at hpq
+  obtain ⟨φ, hφ⟩ := hpq
+  exact (mem_or_not_mem p φ).elim
+    (fun h ↦ ⟨typesWith φ, typesWith_clopen _, h, by change ¬φ ∈ q; rwa [←hφ, not_not]⟩)
+    (fun h ↦ ⟨
+        typesWith ∼φ,
+        typesWith_clopen _, h,
+        by change ¬∼φ∈q; rwa [not_mem_iff,←hφ, not_not, ←not_mem_iff]
+      ⟩)
+
+
+end CompleteType

Mathlib/ModelTheory/Types.lean

@@ -90,6 +90,10 @@ theorem subset (p : T.CompleteType α) : (L.lhomWithConstants α).onTheory T ⊆
 theorem mem_or_not_mem (p : T.CompleteType α) (φ : L[[α]].Sentence) : φ ∈ p ∨ φ.not ∈ p :=
   p.isMaximal.mem_or_not_mem φ
 
+lemma mem_not_mem (hT : T.IsSatisfiable) {φ : L.Sentence} (hφ : φ ∈ T) (hφ' : ∼φ ∈ T) : False :=
+  have ⟨M⟩ := hT
+  (M.is_model.realize_of_mem _ hφ') (M.is_model.realize_of_mem _ hφ)
+
 theorem mem_of_models (p : T.CompleteType α) {φ : L[[α]].Sentence}
     (h : (L.lhomWithConstants α).onTheory T ⊨ᵇ φ) : φ ∈ p :=
   (p.mem_or_not_mem φ).resolve_right fun con =>
@@ -185,6 +189,27 @@ theorem mem_typeOf {φ : L[[α]].Sentence} :
 theorem formula_mem_typeOf {φ : L.Formula α} :
     Formula.equivSentence φ ∈ T.typeOf v ↔ φ.Realize v := by simp
 
+/-- The clopen set of complete types which contain a formula. -/
+def typesWith : L[[α]].Sentence → Set (CompleteType T α) := fun φ ↦ {p | φ ∈ p}
+
+lemma typesWith_inf (φ ψ : L[[α]].Sentence)
+    : typesWith (T := T) (φ ⊓ ψ) = typesWith φ ∩ typesWith ψ := by
+  ext p
+  change φ ⊓ ψ ∈ (p : Set (L[[α]]).Sentence)
+    ↔ φ ∈ (p : Set (L[[α]]).Sentence) ∧ ψ ∈ (p : Set (L[[α]]).Sentence)
+  simp only [p.isMaximal.mem_iff_models, ModelsBoundedFormula, ←forall_and]
+  exact forall₃_congr fun _ _ _ ↦ BoundedFormula.realize_inf
+
+lemma typesWith_mem {φ} (hφ : φ ∈ (L.lhomWithConstants α).onTheory T)
+    : typesWith (T := T) φ = Set.univ
+  := univ_subset_iff.mp fun p _ ↦ p.subset hφ
+
+lemma typesWith_top : typesWith (T := T) (α := α) ⊤ = Set.univ
+  := univ_subset_iff.mp fun p _ ↦ p.isMaximal.mem_of_models (φ := ⊤) (fun _ _ _ a ↦ a)
+
+lemma typesWith_compl (φ : L[[α]].Sentence) : typesWith ∼φ = (typesWith (T := T) φ)ᶜ := by
+  simp [typesWith]
+
 end CompleteType
 
 variable (M)

Mathlib/Tactic/Linter/DirectoryDependency.lean

@@ -615,6 +615,7 @@ def overrideAllowedImportDirs : NamePrefixRel := .ofArray #[
   (`Mathlib.LinearAlgebra.Matrix, `Mathlib.Topology), -- For e.g. spectra.
   (`Mathlib.LinearAlgebra.QuadraticForm, `Mathlib.Topology), -- For real/complex quadratic forms.
   (`Mathlib.LinearAlgebra.SesquilinearForm, `Mathlib.Topology), -- for links with positive semidefinite matrices
+  (`Mathlib.ModelTheory.Topology, `Mathlib.Topology), -- For e.g. topology on complete types.
   (`Mathlib.Topology.Algebra, `Mathlib.Algebra),
   (`Mathlib.Topology.Compactification, `Mathlib.Geometry.Manifold)
 ]