# Documentation

Mathlib.ModelTheory.DirectLimit

# Direct Limits of First-Order Structures #

This file constructs the direct limit of a directed system of first-order embeddings.

## Main Definitions #

• FirstOrder.Language.DirectLimit G f is the direct limit of the directed system f of first-order embeddings between the structures indexed by G.
theorem FirstOrder.Language.DirectedSystem.map_self {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun i j h => ↑(f i j h)] (i : ι) (x : G i) (h : i i) :
↑(f i i h) x = x

A copy of DirectedSystem.map_self specialized to L-embeddings, as otherwise the λ i j h, f i j h can confuse the simplifier.

theorem FirstOrder.Language.DirectedSystem.map_map {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun i j h => ↑(f i j h)] {i : ι} {j : ι} {k : ι} (hij : i j) (hjk : j k) (x : G i) :
↑(f j k hjk) (↑(f i j hij) x) = ↑(f i k (_ : i k)) x

A copy of DirectedSystem.map_map specialized to L-embeddings, as otherwise the λ i j h, f i j h can confuse the simplifier.

def FirstOrder.Language.DirectedSystem.natLERec {L : FirstOrder.Language} {G' : Type w} [(i : ) → ] (f' : (n : ) → FirstOrder.Language.Embedding L (G' n) (G' (n + 1))) (m : ) (n : ) (h : m n) :

Given a chain of embeddings of structures indexed by ℕ, defines a DirectedSystem by composing them.

Instances For
@[simp]
theorem FirstOrder.Language.DirectedSystem.coe_natLERec {L : FirstOrder.Language} {G' : Type w} [(i : ) → ] (f' : (n : ) → FirstOrder.Language.Embedding L (G' n) (G' (n + 1))) (m : ) (n : ) (h : m n) :
↑() = fun a => Nat.leRecOn h (fun k => ↑(f' k)) a
instance FirstOrder.Language.DirectedSystem.natLERec.directedSystem {L : FirstOrder.Language} {G' : Type w} [(i : ) → ] (f' : (n : ) → FirstOrder.Language.Embedding L (G' n) (G' (n + 1))) :
DirectedSystem G' fun i j h => ↑()
@[inline, reducible]
abbrev FirstOrder.Language.Structure.Sigma {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) :
Type (max v w)

Alias for Σ i, G i.

Instances For
@[inline, reducible]
abbrev FirstOrder.Language.Structure.Sigma.mk {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) (i : ι) (x : G i) :

Constructor for FirstOrder.Language.Structure.Sigma alias.

Instances For
def FirstOrder.Language.DirectLimit.unify {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) {α : Type u_1} (x : ) (i : ι) (h : i upperBounds (Set.range (Sigma.fst x))) (a : α) :
G i

Raises a family of elements in the Σ-type to the same level along the embeddings.

Instances For
@[simp]
theorem FirstOrder.Language.DirectLimit.unify_sigma_mk_self {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun i j h => ↑(f i j h)] {α : Type u_1} {i : ι} {x : αG i} :
FirstOrder.Language.DirectLimit.unify f (fun a => ) i (_ : ∀ (j : ι), j Set.range (Sigma.fst fun a => )j i) = x
theorem FirstOrder.Language.DirectLimit.comp_unify {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun i j h => ↑(f i j h)] {α : Type u_1} {x : } {i : ι} {j : ι} (ij : i j) (h : i upperBounds (Set.range (Sigma.fst x))) :
↑(f i j ij) = FirstOrder.Language.DirectLimit.unify f x j (_ : ∀ (k : ι), k Set.range (Sigma.fst x)k j)
def FirstOrder.Language.DirectLimit.setoid {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun i j h => ↑(f i j h)] [IsDirected ι fun x x_1 => x x_1] :

The directed limit glues together the structures along the embeddings.

Instances For
noncomputable def FirstOrder.Language.DirectLimit.sigmaStructure {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [] :

The structure on the Σ-type which becomes the structure on the direct limit after quotienting.

Instances For
def FirstOrder.Language.DirectLimit {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun i j h => ↑(f i j h)] [IsDirected ι fun x x_1 => x x_1] :
Type (max v w)

The direct limit of a directed system is the structures glued together along the embeddings.

Instances For
instance FirstOrder.Language.instInhabitedDirectLimit {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun i j h => ↑(f i j h)] [IsDirected ι fun x x_1 => x x_1] [] [Inhabited (G default)] :
theorem FirstOrder.Language.DirectLimit.equiv_iff {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] {i : ι} (hx : x.fst i) (hy : y.fst i) :
x y ↑(f x.fst i hx) x.snd = ↑(f y.fst i hy) y.snd
theorem FirstOrder.Language.DirectLimit.funMap_unify_equiv {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] {n : } (F : ) (x : ) (i : ι) (j : ι) (hi : i upperBounds (Set.range (Sigma.fst x))) (hj : j upperBounds (Set.range (Sigma.fst x))) :
theorem FirstOrder.Language.DirectLimit.relMap_unify_equiv {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] {n : } (R : ) (x : ) (i : ι) (j : ι) (hi : i upperBounds (Set.range (Sigma.fst x))) (hj : j upperBounds (Set.range (Sigma.fst x))) :
theorem FirstOrder.Language.DirectLimit.exists_unify_eq {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {α : Type u_1} [] {x : } {y : } (xy : x y) :
i hx hy,
theorem FirstOrder.Language.DirectLimit.funMap_equiv_unify {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {n : } (F : ) (x : ) (i : ι) (hi : i upperBounds (Set.range (Sigma.fst x))) :
theorem FirstOrder.Language.DirectLimit.relMap_equiv_unify {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {n : } (R : ) (x : ) (i : ι) (hi : i upperBounds (Set.range (Sigma.fst x))) :
noncomputable instance FirstOrder.Language.DirectLimit.prestructure {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] :

The direct limit setoid respects the structure sigmaStructure, so quotienting by it gives rise to a valid structure.

noncomputable instance FirstOrder.Language.DirectLimit.instStructureDirectLimit {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] :

The L.Structure on a direct limit of L.Structures.

@[simp]
theorem FirstOrder.Language.DirectLimit.funMap_quotient_mk'_sigma_mk' {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {n : } {F : } {i : ι} {x : Fin nG i} :
@[simp]
theorem FirstOrder.Language.DirectLimit.relMap_quotient_mk'_sigma_mk' {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {n : } {R : } {i : ι} {x : Fin nG i} :
theorem FirstOrder.Language.DirectLimit.exists_quotient_mk'_sigma_mk'_eq {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {α : Type u_1} [] (x : ) :
i y, x = fun a =>
def FirstOrder.Language.DirectLimit.of (L : FirstOrder.Language) (ι : Type v) [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] (i : ι) :

The canonical map from a component to the direct limit.

Instances For
@[simp]
theorem FirstOrder.Language.DirectLimit.of_apply {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] {f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {i : ι} {x : G i} :
↑() x =
theorem FirstOrder.Language.DirectLimit.of_f {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] {f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {i : ι} {j : ι} {hij : i j} {x : G i} :
↑() (↑(f i j hij) x) = ↑() x
theorem FirstOrder.Language.DirectLimit.exists_of {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] {f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] (z : ) :
i x, ↑() x = z

Every element of the direct limit corresponds to some element in some component of the directed system.

theorem FirstOrder.Language.DirectLimit.inductionOn {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] {f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {C : } (z : ) (ih : (i : ι) → (x : G i) → C (↑() x)) :
C z
def FirstOrder.Language.DirectLimit.lift (L : FirstOrder.Language) (ι : Type v) [] (G : ιType w) [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {P : Type u₁} (g : (i : ι) → ) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), ↑(g j) (↑(f i j hij) x) = ↑(g i) x) :

The universal property of the direct limit: maps from the components to another module that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.

Instances For
@[simp]
theorem FirstOrder.Language.DirectLimit.lift_quotient_mk'_sigma_mk' {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] {f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {P : Type u₁} (g : (i : ι) → ) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), ↑(g j) (↑(f i j hij) x) = ↑(g i) x) {i : ι} (x : G i) :
↑() () = ↑(g i) x
theorem FirstOrder.Language.DirectLimit.lift_of {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] {f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {P : Type u₁} (g : (i : ι) → ) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), ↑(g j) (↑(f i j hij) x) = ↑(g i) x) {i : ι} (x : G i) :
↑() (↑() x) = ↑(g i) x
theorem FirstOrder.Language.DirectLimit.lift_unique {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → ] {f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] [] {P : Type u₁} (F : ) (x : ) :
F x = ↑(FirstOrder.Language.DirectLimit.lift L ι G f (fun i => ) (_ : ∀ (i j : ι) (hij : i j) (x : G i), ↑((fun i => ) j) (↑(f i j hij) x) = ↑((fun i => ) i) x)) x
theorem FirstOrder.Language.DirectLimit.cg {L : FirstOrder.Language} {ι : Type u_1} [] [] [IsDirected ι fun x x_1 => x x_1] [] {G : ιType w} [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) (h : ∀ (i : ι), ) [DirectedSystem G fun i j h => ↑(f i j h)] :

The direct limit of countably many countably generated structures is countably generated.

instance FirstOrder.Language.DirectLimit.cg' {L : FirstOrder.Language} {ι : Type u_1} [] [] [IsDirected ι fun x x_1 => x x_1] [] {G : ιType w} [(i : ι) → ] (f : (i j : ι) → i jFirstOrder.Language.Embedding L (G i) (G j)) [h : ∀ (i : ι), ] [DirectedSystem G fun i j h => ↑(f i j h)] :