ElementarySubstructures.lean

/-
Copyright (c) 2022 Aaron Anderson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aaron Anderson
-/
module

public import Mathlib.ModelTheory.ElementaryMaps
public import Mathlib.ModelTheory.Definability

/-!
# Elementary Substructures

## Main Definitions

- A `FirstOrder.Language.ElementarySubstructure` is a substructure where the realization of each
  formula agrees with the realization in the larger model.

## Main Results

- The Tarski-Vaught Test for substructures:
  `FirstOrder.Language.Substructure.isElementary_of_exists` gives a simple criterion for a
  substructure to be elementary.
-/

@[expose] public section


open FirstOrder

namespace FirstOrder

namespace Language

open Structure

variable {L : Language} {M : Type*} [L.Structure M]

/-- A substructure is elementary when every formula applied to a tuple in the substructure
  agrees with its value in the overall structure. -/
def Substructure.IsElementary (S : L.Substructure M) : Prop :=
  ∀ ⦃n⦄ (φ : L.Formula (Fin n)) (x : Fin n → S), φ.Realize (((↑) : _ → M) ∘ x) ↔ φ.Realize x

variable (L M)

/-- An elementary substructure is one in which every formula applied to a tuple in the substructure
  agrees with its value in the overall structure. -/
structure ElementarySubstructure where
  /-- The underlying substructure -/
  toSubstructure : L.Substructure M
  isElementary' : toSubstructure.IsElementary

variable {L M}

namespace ElementarySubstructure

attribute [coe] toSubstructure

instance instCoe : Coe (L.ElementarySubstructure M) (L.Substructure M) :=
  ⟨ElementarySubstructure.toSubstructure⟩

instance instSetLike : SetLike (L.ElementarySubstructure M) M :=
  ⟨fun x => x.toSubstructure.carrier, fun ⟨⟨s, hs1⟩, hs2⟩ ⟨⟨t, ht1⟩, _⟩ _ => by
    congr⟩

instance : PartialOrder (L.ElementarySubstructure M) := .ofSetLike (L.ElementarySubstructure M) M

instance inducedStructure (S : L.ElementarySubstructure M) : L.Structure S :=
  Substructure.inducedStructure

@[simp]
theorem isElementary (S : L.ElementarySubstructure M) : (S : L.Substructure M).IsElementary :=
  S.isElementary'

/-- The natural embedding of an `L.Substructure` of `M` into `M`. -/
def subtype (S : L.ElementarySubstructure M) : S ↪ₑ[L] M where
  toFun := (↑)
  map_formula' := S.isElementary

@[simp]
theorem subtype_apply {S : L.ElementarySubstructure M} {x : S} : subtype S x = x :=
  rfl

theorem subtype_injective (S : L.ElementarySubstructure M) : Function.Injective (subtype S) :=
  Subtype.coe_injective

@[simp]
theorem coe_subtype (S : L.ElementarySubstructure M) : ⇑S.subtype = Subtype.val :=
  rfl

/-- The substructure `M` of the structure `M` is elementary. -/
instance instTop : Top (L.ElementarySubstructure M) :=
  ⟨⟨⊤, fun _ _ _ => Substructure.realize_formula_top.symm⟩⟩

instance instInhabited : Inhabited (L.ElementarySubstructure M) :=
  ⟨⊤⟩

@[simp]
theorem mem_top (x : M) : x ∈ (⊤ : L.ElementarySubstructure M) :=
  Set.mem_univ x

@[simp]
theorem coe_top : ((⊤ : L.ElementarySubstructure M) : Set M) = Set.univ :=
  rfl

@[simp]
theorem realize_sentence (S : L.ElementarySubstructure M) (φ : L.Sentence) : S ⊨ φ ↔ M ⊨ φ :=
  S.subtype.map_sentence φ

@[simp]
theorem theory_model_iff (S : L.ElementarySubstructure M) (T : L.Theory) : S ⊨ T ↔ M ⊨ T := by
  simp only [Theory.model_iff, realize_sentence]

instance theory_model {T : L.Theory} [h : M ⊨ T] {S : L.ElementarySubstructure M} : S ⊨ T :=
  (theory_model_iff S T).2 h

instance instNonempty [Nonempty M] {S : L.ElementarySubstructure M} : Nonempty S :=
  (model_nonemptyTheory_iff L).1 inferInstance

theorem elementarilyEquivalent (S : L.ElementarySubstructure M) : S ≅[L] M :=
  S.subtype.elementarilyEquivalent

end ElementarySubstructure

namespace Substructure

/-- The Tarski-Vaught test for elementarity of a substructure. -/
theorem isElementary_of_exists (S : L.Substructure M)
    (htv :
      ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → S) (a : M),
        φ.Realize default (Fin.snoc ((↑) ∘ x) a : _ → M) →
          ∃ b : S, φ.Realize default (Fin.snoc ((↑) ∘ x) b : _ → M)) :
    S.IsElementary := fun _ => S.subtype.isElementary_of_exists htv

/-- Bundles a substructure satisfying the Tarski-Vaught test as an elementary substructure. -/
@[simps]
def toElementarySubstructure (S : L.Substructure M)
    (htv :
      ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → S) (a : M),
        φ.Realize default (Fin.snoc ((↑) ∘ x) a : _ → M) →
          ∃ b : S, φ.Realize default (Fin.snoc ((↑) ∘ x) b : _ → M)) :
    L.ElementarySubstructure M :=
  ⟨S, S.isElementary_of_exists htv⟩

end Substructure

/-- A set meets definable sets if it meets every nonempty definable subset. -/
def MeetsDefinable (A : Set M) : Prop :=
  ∀ (D : Set M), D.Nonempty → A.Definable₁ L D → (D ∩ A).Nonempty

namespace MeetsDefinable

open Set Substructure

variable {A : Set M}

/-- The closure of a set meeting definable sets is equal to itself. -/
theorem closure_eq_self (hA : L.MeetsDefinable A) :
    closure L A = A := by
  refine Subset.antisymm ?_ subset_closure
  rw [coe_closure_eq_range_term_realize]
  rintro x ⟨t, rfl⟩
  exact singleton_inter_nonempty.mp <| hA _ (singleton_nonempty _) <|
    by simpa using ((Term.var 0).equal (t.relabel Sum.inl).varsToConstants).definable_withConstants

/-- The closure of a set meeting definable sets is an elementary substructure. -/
theorem isElementary_closure (hA : L.MeetsDefinable A) :
    (closure L A).IsElementary := by
  refine isElementary_of_exists ((closure L).toFun A) ?_
  intro n φ x a hφ
  let D : Set M := {y : M | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
  have hD_ne : D.Nonempty := ⟨a,hφ⟩
  have hD : A.Definable₁ L D := by
    apply (φ.definable_boundedSection).preimage_map
    simp only [DefinableMap]
    refine Fin.lastCases ?_ ?_
    · simp only [Fin.snoc_last]; fun_prop
    · intro i; simp only [Fin.snoc_castSucc];
      have : ↑(x i) ∈ A := by
        nth_rw 1 [← hA.closure_eq_self]
        simp
      fun_prop (disch := assumption)
  obtain ⟨b, hbD, hbA⟩ := hA D hD_ne hD
  exact ⟨⟨b, by rwa [← hA.closure_eq_self] at hbA⟩, hbD⟩

/-- Bundles the closure of a set meeting definable sets as an elementary substructure. -/
def toElementarySubstructure (hA : L.MeetsDefinable A) :
    L.ElementarySubstructure M :=
  ⟨closure L A, hA.isElementary_closure⟩

end MeetsDefinable

namespace ElementarySubstructure

open Set Formula

/-- An elementary substructure, regarded as a subset of the ambient structure, meets definable
sets. -/
theorem meetsDefinable (S : L.ElementarySubstructure M) : L.MeetsDefinable (S : Set M) := by
  classical
  rintro D ⟨x, hx⟩ ⟨φ, hφ⟩
  have hφx : φ.Realize ![x] := by
    simp [Set.ext_iff] at hφ
    simp [← hφ, hx]
  let ψ : L[[(S : Set M)]].Sentence := (φ.relabel Sum.inr).iExs
  have hψM : ψ.Realize M := by
    simpa only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
      Formula.realize_relabel, Sum.elim_comp_inr, ψ] using
        (⟨![x], hφx⟩ : ∃ w : Fin 1 → M, φ.Realize w)
  have hψS : ψ.Realize S := by
    rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
  simp only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
    Formula.realize_relabel, Sum.elim_comp_inr, ψ] at hψS
  obtain ⟨v', hv'⟩ := hψS
  refine ⟨v' 0, ?_, by simp⟩
  have hv'' : φ.Realize (Subtype.val ∘ v') := by
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]
    convert hv' using 1
    funext i
    cases i <;> rfl
  change (Subtype.val ∘ v') ∈ {x | x 0 ∈ D}
  simpa [hφ] using hv''

end ElementarySubstructure

end Language

end FirstOrder