# mathlib3documentation

model_theory.direct_limit

# Direct Limits of First-Order Structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file constructs the direct limit of a directed system of first-order embeddings.

## Main Definitions #

• first_order.language.direct_limit G f is the direct limit of the directed system f of first-order embeddings between the structures indexed by G.
theorem first_order.language.directed_system.map_self {L : first_order.language} {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] (i : ι) (x : G i) (h : i i) :
(f i i h) x = x

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

theorem first_order.language.directed_system.map_map {L : first_order.language} {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (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 _) x

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

def first_order.language.directed_system.nat_le_rec {L : first_order.language} {G' : Type w} [Π (i : ), L.Structure (G' i)] (f' : Π (n : ), L.embedding (G' n) (G' (n + 1))) (m n : ) (h : m n) :
L.embedding (G' m) (G' n)

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

Equations
@[simp]
theorem first_order.language.directed_system.coe_nat_le_rec {L : first_order.language} {G' : Type w} [Π (i : ), L.Structure (G' i)] (f' : Π (n : ), L.embedding (G' n) (G' (n + 1))) (m n : ) (h : m n) :
= (λ (n : ), (f' n))
@[protected, instance]
def first_order.language.directed_system.nat_le_rec.directed_system {L : first_order.language} {G' : Type w} [Π (i : ), L.Structure (G' i)] (f' : Π (n : ), L.embedding (G' n) (G' (n + 1))) :
(λ (i j : ) (h : i j),
def first_order.language.direct_limit.unify {L : first_order.language} {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) {α : Type u_3} (x : α (Σ (i : ι), G i)) (i : ι) (h : i upper_bounds (set.range (sigma.fst x))) (a : α) :
G i

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

Equations
@[simp]
theorem first_order.language.direct_limit.unify_sigma_mk_self {L : first_order.language} {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] {α : Type u_3} {i : ι} {x : α G i} :
_ = x
theorem first_order.language.direct_limit.comp_unify {L : first_order.language} {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] {α : Type u_3} {x : α (Σ (i : ι), G i)} {i j : ι} (ij : i j) (h : i upper_bounds (set.range (sigma.fst x))) :
(f i j ij) =
def first_order.language.direct_limit.setoid {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))]  :
setoid (Σ (i : ι), G i)

The directed limit glues together the structures along the embeddings.

Equations
• = {r := λ (_x : Σ (i : ι), G i), first_order.language.direct_limit.setoid._match_2 G f _x, iseqv := _}
• first_order.language.direct_limit.setoid._match_2 G f i, x⟩ = λ (_x : Σ (i : ι), G i), first_order.language.direct_limit.setoid._match_1 G f i x _x
• first_order.language.direct_limit.setoid._match_1 G f i x j, y⟩ = (k : ι) (ik : i k) (jk : j k), (f i k ik) x = (f j k jk) y
Instances for first_order.language.direct_limit.setoid
noncomputable def first_order.language.direct_limit.sigma_structure {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [nonempty ι] :
L.Structure (Σ (i : ι), G i)

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

Equations
def first_order.language.direct_limit {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))]  :
Type (max v w)

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

Equations
Instances for first_order.language.direct_limit
@[protected, instance]
def first_order.language.direct_limit.inhabited {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [inhabited ι]  :
Equations
theorem first_order.language.direct_limit.equiv_iff {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] {x y : Σ (i : ι), G i} {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 first_order.language.direct_limit.fun_map_unify_equiv {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] {n : } (F : L.functions n) (x : fin n (Σ (i : ι), G i)) (i j : ι) (hi : i upper_bounds (set.range (sigma.fst x))) (hj : j upper_bounds (set.range (sigma.fst x))) :
theorem first_order.language.direct_limit.rel_map_unify_equiv {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] {n : } (R : L.relations n) (x : fin n (Σ (i : ι), G i)) (i j : ι) (hi : i upper_bounds (set.range (sigma.fst x))) (hj : j upper_bounds (set.range (sigma.fst x))) :
theorem first_order.language.direct_limit.exists_unify_eq {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {α : Type u_3} [fintype α] {x y : α (Σ (i : ι), G i)} (xy : x y) :
theorem first_order.language.direct_limit.fun_map_equiv_unify {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {n : } (F : L.functions n) (x : fin n (Σ (i : ι), G i)) (i : ι) (hi : i upper_bounds (set.range (sigma.fst x))) :
theorem first_order.language.direct_limit.rel_map_equiv_unify {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {n : } (R : L.relations n) (x : fin n (Σ (i : ι), G i)) (i : ι) (hi : i upper_bounds (set.range (sigma.fst x))) :
@[protected, instance]
noncomputable def first_order.language.direct_limit.prestructure {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] :

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

Equations
@[protected, instance]
noncomputable def first_order.language.direct_limit.Structure {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] :

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

Equations
@[simp]
theorem first_order.language.direct_limit.fun_map_quotient_mk_sigma_mk {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {n : } {F : L.functions n} {i : ι} {x : fin n G i} :
(λ (a : fin n), i, x a) =
@[simp]
theorem first_order.language.direct_limit.rel_map_quotient_mk_sigma_mk {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {n : } {R : L.relations n} {i : ι} {x : fin n G i} :
(λ (a : fin n), i, x a) =
theorem first_order.language.direct_limit.exists_quotient_mk_sigma_mk_eq {L : first_order.language} {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {α : Type u_3} [fintype α] (x : α ) :
(i : ι) (y : α G i), x =
def first_order.language.direct_limit.of (L : first_order.language) (ι : Type v) [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] (i : ι) :
L.embedding (G i)

The canonical map from a component to the direct limit.

Equations
@[simp]
theorem first_order.language.direct_limit.of_apply {L : first_order.language} {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] {f : Π (i j : ι), i j L.embedding (G i) (G j)} [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {i : ι} {x : G i} :
i) x = i, x⟩
@[simp]
theorem first_order.language.direct_limit.of_f {L : first_order.language} {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] {f : Π (i j : ι), i j L.embedding (G i) (G j)} [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {i j : ι} {hij : i j} {x : G i} :
j) ((f i j hij) x) = i) x
theorem first_order.language.direct_limit.exists_of {L : first_order.language} {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] {f : Π (i j : ι), i j L.embedding (G i) (G j)} [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι]  :
(i : ι) (x : G i), i) x = z

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

@[protected]
theorem first_order.language.direct_limit.induction_on {L : first_order.language} {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] {f : Π (i j : ι), i j L.embedding (G i) (G j)} [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {C : Prop} (ih : (i : ι) (x : G i), C ( i) x)) :
C z
def first_order.language.direct_limit.lift (L : first_order.language) (ι : Type v) [preorder ι] (G : ι Type w) [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {P : Type u₁} [L.Structure P] (g : Π (i : ι), L.embedding (G i) P) (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.

Equations
@[simp]
theorem first_order.language.direct_limit.lift_quotient_mk_sigma_mk {L : first_order.language} {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] {f : Π (i j : ι), i j L.embedding (G i) (G j)} [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {P : Type u₁} [L.Structure P] (g : Π (i : ι), L.embedding (G i) P) (Hg : (i j : ι) (hij : i j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι} (x : G i) :
g Hg) i, x⟩ = (g i) x
theorem first_order.language.direct_limit.lift_of {L : first_order.language} {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] {f : Π (i j : ι), i j L.embedding (G i) (G j)} [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {P : Type u₁} [L.Structure P] (g : Π (i : ι), L.embedding (G i) P) (Hg : (i j : ι) (hij : i j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι} (x : G i) :
g Hg) ( i) x) = (g i) x
theorem first_order.language.direct_limit.lift_unique {L : first_order.language} {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] {f : Π (i j : ι), i j L.embedding (G i) (G j)} [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {P : Type u₁} [L.Structure P] (F : P)  :
F x = (λ (i : ι), F.comp i)) _) x
theorem first_order.language.direct_limit.cg {L : first_order.language} {ι : Type u_3} [encodable ι] [preorder ι] [nonempty ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) (h : (i : ι), ) [ (λ (i j : ι) (h : i j), (f i j h))] :

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

@[protected, instance]
def first_order.language.direct_limit.cg' {L : first_order.language} {ι : Type u_3} [encodable ι] [preorder ι] [nonempty ι] {G : ι Type w} [Π (i : ι), L.Structure (G i)] (f : Π (i j : ι), i j L.embedding (G i) (G j)) [h : (i : ι), ] [ (λ (i j : ι) (h : i j), (f i j h))] :