ElementaryChain.lean

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

public import Mathlib.ModelTheory.DirectLimit
public import Mathlib.ModelTheory.ElementaryMaps
public import Mathlib.SetTheory.Cardinal.DirectLimit

/-!
# Elementary chains

This file defines elementary chains without choosing a common ambient structure. Their unions are
constructed as direct limits of the underlying directed systems of first-order embeddings.

## Main definitions

- `FirstOrder.Language.ElementaryChain`: A system of structures whose transition maps are
  elementary embeddings.
- `FirstOrder.Language.ElementaryChain.ofNatSucc`: The elementary chain generated by a sequence of
  elementary embeddings between successive stages.
- `FirstOrder.Language.ElementaryChain.Limit`: The direct limit of an elementary chain.
- `FirstOrder.Language.ElementaryChain.toLimitElementary`: The canonical elementary embedding of a
  stage into the limit.
- `FirstOrder.Language.ElementaryChain.liftElementary`: The elementary lift of a compatible
  cocone.

## Main results

- `FirstOrder.Language.ElementaryChain.realize_toLimit`: Bounded formulas are preserved and
  reflected by the canonical maps into the limit.
- `FirstOrder.Language.ElementaryChain.limit_models`: A theory modeled by a stage is modeled by the
  limit.
-/

@[expose] public section

universe u v w w'

namespace FirstOrder

namespace Language

open scoped Cardinal

/-- A system of `L`-structures whose transition maps are elementary embeddings. -/
structure ElementaryChain (L : Language.{u, v}) (ι : Type w) [Preorder ι] where
  /-- The structure at each stage of the chain. -/
  carrier : ι → Type w'
  [struc : ∀ i, L.Structure (carrier i)]
  /-- The elementary embedding from stage `i` to stage `j` when `i ≤ j`. -/
  map : ∀ i j, i ≤ j → carrier i ↪ₑ[L] carrier j
  map_self : ∀ i x, map i i le_rfl x = x
  map_map : ∀ i j k (hij : i ≤ j) (hjk : j ≤ k) (x : carrier i),
    map j k hjk (map i j hij x) = map i k (hij.trans hjk) x

attribute [instance] ElementaryChain.struc

namespace ElementaryEmbedding

variable {L : Language.{u, v}} {M : ℕ → Type w'} [∀ n, L.Structure (M n)]

/-- Compose a sequence of elementary embeddings along an interval of natural numbers. -/
noncomputable def natLERec (f : ∀ n, M n ↪ₑ[L] M (n + 1))
    (m n : ℕ) (h : m ≤ n) : M m ↪ₑ[L] M n :=
  Nat.leRecOn h (@fun k g ↦ (f k).comp g) (refl L _)

private theorem coe_natLERec (f : ∀ n, M n ↪ₑ[L] M (n + 1))
    (m n : ℕ) (h : m ≤ n) :
    (natLERec f m n h : M m → M n) =
      DirectedSystem.natLERec (fun n ↦ (f n).toEmbedding) m n h := by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
  ext x
  induction k with
  | zero => simp [natLERec, DirectedSystem.natLERec, Nat.leRecOn_self]
  | succ k ih =>
    simp only [natLERec, DirectedSystem.coe_natLERec]
    rw [Nat.leRecOn_succ le_self_add, Nat.leRecOn_succ le_self_add]
    specialize ih (Nat.le_add_right m k)
    simp only [natLERec, DirectedSystem.coe_natLERec] at ih
    exact congrArg (f (m + k)) ih

/-- Iterated composition over a reflexive natural-number interval is the identity. -/
@[simp]
theorem natLERec_self (f : ∀ n, M n ↪ₑ[L] M (n + 1)) (n : ℕ) (x : M n) :
    natLERec f n n le_rfl x = x := by
  simp [natLERec, Nat.leRecOn_self]

/-- Iterated composition over one successor step is the supplied elementary embedding. -/
@[simp]
theorem natLERec_succ (f : ∀ n, M n ↪ₑ[L] M (n + 1)) (n : ℕ) (x : M n) :
    natLERec f n (n + 1) (Nat.le_succ n) x = f n x := by
  simp [natLERec, Nat.leRecOn]

/-- Iterated elementary embeddings compose coherently across adjacent intervals. -/
theorem natLERec_trans {f : ∀ n, M n ↪ₑ[L] M (n + 1)}
    {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k) (x : M i) :
    natLERec f j k hjk (natLERec f i j hij x) = natLERec f i k (hij.trans hjk) x := by
  simpa only [coe_natLERec] using
    DirectedSystem.map_map
      (fun i j h ↦ DirectedSystem.natLERec (fun n ↦ (f n).toEmbedding) i j h) hij hjk x

end ElementaryEmbedding

namespace ElementaryChain

variable {L : Language.{u, v}} {ι : Type w} [Preorder ι]

/-- Construct a countable elementary chain by composing elementary embeddings between successive
stages. -/
noncomputable def ofNatSucc (M : ℕ → Type w') [∀ n, L.Structure (M n)]
    (f : ∀ n, M n ↪ₑ[L] M (n + 1)) : ElementaryChain L ℕ where
  carrier := M
  map := ElementaryEmbedding.natLERec f
  map_self := ElementaryEmbedding.natLERec_self f
  map_map := fun _ _ _ hij hjk x ↦ ElementaryEmbedding.natLERec_trans hij hjk x

/-- The transition map of `ofNatSucc` between successive stages is the supplied elementary
embedding. -/
@[simp]
theorem ofNatSucc_map_succ (M : ℕ → Type w') [∀ n, L.Structure (M n)]
    (f : ∀ n, M n ↪ₑ[L] M (n + 1)) (n : ℕ) :
    (ofNatSucc M f).map n (n + 1) (Nat.le_succ n) = f n := by
  ext x
  exact ElementaryEmbedding.natLERec_succ f n x

/-- The underlying first-order embeddings form a directed system. -/
instance toEmbeddingDirectedSystem (C : ElementaryChain L ι) :
    DirectedSystem C.carrier (fun i j h ↦ (C.map i j h).toEmbedding) where
  map_self i x := C.map_self i x
  map_map k j i hij hjk x := C.map_map i j k hij hjk x

variable [IsDirectedOrder ι]

/-- The abstract union of an elementary chain, constructed without an ambient structure. -/
abbrev Limit (C : ElementaryChain L ι) :=
  L.DirectLimit C.carrier (fun i j h ↦ (C.map i j h).toEmbedding)

variable [Nonempty ι]

/-- The canonical first-order embedding of a stage into the direct limit. -/
noncomputable def toLimit (C : ElementaryChain L ι) (i : ι) : C.carrier i ↪[L] C.Limit :=
  DirectLimit.of L ι C.carrier (fun i j h ↦ (C.map i j h).toEmbedding) i

/-- The canonical maps commute with the transition maps. -/
@[simp]
theorem toLimit_map (C : ElementaryChain L ι) {i j : ι} (hij : i ≤ j) (x : C.carrier i) :
    C.toLimit j (C.map i j hij x) = C.toLimit i x := by
  unfold toLimit
  exact DirectLimit.of_f

/-- Every element of the direct limit is represented by an element of some stage. -/
theorem exists_toLimit (C : ElementaryChain L ι) (z : C.Limit) :
    ∃ (i : ι) (x : C.carrier i), C.toLimit i x = z := by
  simpa [toLimit] using DirectLimit.exists_of z

private def limitEquiv (C : ElementaryChain L ι) :
    C.Limit ≃
      _root_.DirectLimit C.carrier (fun i j h ↦ (C.map i j h).toEmbedding) :=
  Quotient.congrRight fun _ _ ↦ Iff.rfl

omit [Nonempty ι] in
/-- An infinite cardinal bounding the index type and every stage also bounds the limit. -/
theorem mk_limit_le_of_lift_mk_le (C : ElementaryChain L ι) {κ : Cardinal.{max w w'}}
    (hκ : ℵ₀ ≤ κ) (hι : Cardinal.lift.{w'} #ι ≤ κ)
    (hC : ∀ i, Cardinal.lift.{w} #(C.carrier i) ≤ κ) :
    #(C.Limit) ≤ κ := by
  rw [(limitEquiv C).cardinal_eq]
  exact _root_.DirectLimit.mk_le_of_aleph0_le
    (fun i j h ↦ (C.map i j h).toEmbedding) κ hκ hι hC

/-- If every stage has cardinality `κ` and the index type has cardinality at most `κ`, then the
limit also has cardinality `κ`. -/
theorem mk_limit_eq_of_forall_lift_mk_eq (C : ElementaryChain L ι)
    (κ : Cardinal.{max w w'}) (hι : Cardinal.lift.{w'} #ι ≤ κ)
    (hC : ∀ i, Cardinal.lift.{w} #(C.carrier i) = κ) :
    #(C.Limit) = κ := by
  rw [(limitEquiv C).cardinal_eq]
  apply _root_.DirectLimit.mk_eq_of_forall_lift_mk_eq
    (fun i j h ↦ (C.map i j h).toEmbedding) κ hι hC
  exact _root_.DirectLimit.mk_injective _ fun i j h ↦ (C.map i j h).injective

/-- Realization of bounded formulas is preserved and reflected by a canonical map into the direct
limit. -/
theorem realize_toLimit (C : ElementaryChain L ι) {α : Type*} {n : ℕ}
    (φ : L.BoundedFormula α n) (i : ι) (v : α → C.carrier i)
    (xs : Fin n → C.carrier i) :
    φ.Realize (C.toLimit i ∘ v) (C.toLimit i ∘ xs) ↔ φ.Realize v xs := by
  induction φ generalizing i with
  | falsum => rfl
  | equal t₁ t₂ =>
    simp [BoundedFormula.Realize, ← Sum.comp_elim]
  | rel R ts =>
    simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]
    exact StrongHomClass.map_rel (C.toLimit i) R
      (fun i ↦ Term.realize (Sum.elim v xs) (ts i))
  | imp φ ψ ihφ ihψ =>
    simp [BoundedFormula.Realize, ihφ, ihψ]
  | @all n φ ih =>
    simp only [BoundedFormula.realize_all, Nat.succ_eq_add_one]
    constructor <;> intro h x
    · simpa [← Fin.comp_snoc, ih i v (Fin.snoc xs x)] using h (C.toLimit i x)
    · obtain ⟨j, xj, rfl⟩ := C.exists_toLimit x
      obtain ⟨k, hik, hjk⟩ := exists_ge_ge i j
      rw [← BoundedFormula.Realize,
        ← (C.map i k hik).map_boundedFormula φ.all v xs, BoundedFormula.Realize] at h
      specialize h (C.map j k hjk xj)
      specialize ih k (C.map i k hik ∘ v)
        (Fin.snoc (C.map i k hik ∘ xs) (C.map j k hjk xj))
      rw [← ih, Fin.comp_snoc] at h
      convert h using 1 <;> simp [Function.comp_def, C.toLimit_map]

/-- The canonical map from each stage to the direct limit is elementary. -/
noncomputable def toLimitElementary (C : ElementaryChain L ι) (i : ι) :
    C.carrier i ↪ₑ[L] C.Limit where
  toFun := C.toLimit i
  map_formula' := fun n φ v ↦ by
    change BoundedFormula.Realize φ (C.toLimit i ∘ v) default ↔
      BoundedFormula.Realize φ v default
    convert C.realize_toLimit φ i v default

/-- A finite family of elements of the direct limit can be lifted to a common stage of the chain.
-/
theorem exists_finite_common_stage (C : ElementaryChain L ι) {α : Type*} [Finite α]
    (x : α → C.Limit) : ∃ (i : ι) (z : α → C.carrier i), C.toLimit i ∘ z = x := by
  obtain ⟨i, z, hz⟩ := DirectLimit.exists_quotient_mk'_sigma_mk'_eq C.carrier
    (fun i j h ↦ (C.map i j h).toEmbedding) x
  exact ⟨i, z, by simpa [toLimit, Function.comp_def] using hz.symm⟩

/-- A compatible cocone of elementary embeddings induces an elementary embedding from the direct
limit. This is the elementary version of `Language.DirectLimit.lift`. -/
noncomputable def liftElementary (C : ElementaryChain L ι) {P : Type*} [L.Structure P]
    (g : ∀ i, C.carrier i ↪ₑ[L] P)
    (comm : ∀ i j (hij : i ≤ j) (x : C.carrier i), g j (C.map i j hij x) = g i x) :
    C.Limit ↪ₑ[L] P :=
  let F : C.Limit ↪[L] P := Language.DirectLimit.lift L ι C.carrier
    (fun i j h ↦ (C.map i j h).toEmbedding)
    (fun i ↦ (g i).toEmbedding)
    (by intro i j hij x; simpa using comm i j hij x)
  { toFun := F
    map_formula' := by
      intro n φ x
      obtain ⟨i, z, hz⟩ := C.exists_finite_common_stage x
      have hF_lift : ∀ a : C.carrier i, F (C.toLimit i a) = g i a := by
        intro a
        simp [F, toLimit]
      have h_eq : F ∘ x = (g i : C.carrier i → P) ∘ z := by
        ext k
        calc
          F (x k) = F (C.toLimit i (z k)) := by simp [← hz]
          _ = g i (z k) := hF_lift (z k)
      rw [h_eq]
      exact ((g i).map_formula' φ z).trans <| by
        rw [← hz]
        exact ((C.toLimitElementary i).map_formula' φ z).symm }

/-- If some stage is a model of `T`, then the direct limit is also a model of `T`. -/
theorem limit_models (C : ElementaryChain L ι) (T : L.Theory)
    (hT : ∃ i, C.carrier i ⊨ T) : C.Limit ⊨ T := by
  obtain ⟨i, hi⟩ := hT
  exact ((C.toLimitElementary i).theory_model_iff T).1 hi

end ElementaryChain

end Language

end FirstOrder