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} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun (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 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} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun (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 (_ : 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 : ℕ) → FirstOrder.Language.Structure L (G' i)] (f' : (n : ℕ) → FirstOrder.Language.Embedding L (G' n) (G' (n + 1))) (m : ℕ) (n : ℕ) (h : m ≤ n) : FirstOrder.Language.Embedding L (G' m) (G' n)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FirstOrder.Language.DirectedSystem.coe_natLERec {L : FirstOrder.Language} {G' : ℕ → Type w} [(i : ℕ) → FirstOrder.Language.Structure L (G' i)] (f' : (n : ℕ) → FirstOrder.Language.Embedding L (G' n) (G' (n + 1))) (m : ℕ) (n : ℕ) (h : m ≤ n) : ⇑(FirstOrder.Language.DirectedSystem.natLERec f' m n h) = fun (a : G' m) => Nat.leRecOn h (fun (k : ℕ) => ⇑(f' k)) a

instance FirstOrder.Language.DirectedSystem.natLERec.directedSystem {L : FirstOrder.Language} {G' : ℕ → Type w} [(i : ℕ) → FirstOrder.Language.Structure L (G' i)] (f' : (n : ℕ) → FirstOrder.Language.Embedding L (G' n) (G' (n + 1))) : DirectedSystem G' fun (i j : ℕ) (h : i ≤ j) => ⇑(FirstOrder.Language.DirectedSystem.natLERec f' i j h)

Equations

• One or more equations did not get rendered due to their size.

@[inline, reducible]

abbrev FirstOrder.Language.Structure.Sigma {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) : Type (max v w)

Alias for Σ i, G i.

Equations

• FirstOrder.Language.Structure.Sigma f = ((i : ι) × G i)

@[inline, reducible]

abbrev FirstOrder.Language.Structure.Sigma.mk {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) (i : ι) (x : G i) : FirstOrder.Language.Structure.Sigma f

Constructor for FirstOrder.Language.Structure.Sigma alias.

Equations

• FirstOrder.Language.Structure.Sigma.mk f i x = { fst := i, snd := x }

def FirstOrder.Language.DirectLimit.unify {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) {α : Type u_1} (x : α → FirstOrder.Language.Structure.Sigma f) (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.

Equations

• FirstOrder.Language.DirectLimit.unify f x i h a = (f (x a).fst i (_ : (x a).fst ≤ i)) (x a).snd

@[simp]

theorem FirstOrder.Language.DirectLimit.unify_sigma_mk_self {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] {α : Type u_1} {i : ι} {x : α → G i} : FirstOrder.Language.DirectLimit.unify f (fun (a : α) => FirstOrder.Language.Structure.Sigma.mk f i (x a)) i (_ : ∀ j ∈ Set.range (Sigma.fst ∘ fun (a : α) => FirstOrder.Language.Structure.Sigma.mk f i (x a)), j ≤ i) = x

theorem FirstOrder.Language.DirectLimit.comp_unify {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] {α : Type u_1} {x : α → FirstOrder.Language.Structure.Sigma f} {i : ι} {j : ι} (ij : i ≤ j) (h : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) : ⇑(f i j ij) ∘ FirstOrder.Language.DirectLimit.unify f x i h = FirstOrder.Language.DirectLimit.unify f x j (_ : ∀ k ∈ Set.range (Sigma.fst ∘ x), k ≤ j)

def FirstOrder.Language.DirectLimit.setoid {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] : Setoid (FirstOrder.Language.Structure.Sigma f)

The directed limit glues together the structures along the embeddings.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FirstOrder.Language.DirectLimit.sigmaStructure {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [Nonempty ι] : FirstOrder.Language.Structure L (FirstOrder.Language.Structure.Sigma f)

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

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.DirectLimit {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(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.

Equations

• FirstOrder.Language.DirectLimit G f = Quotient (FirstOrder.Language.DirectLimit.setoid G f)

instance FirstOrder.Language.instInhabitedDirectLimit {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [Inhabited ι] [Inhabited (G default)] : Inhabited (FirstOrder.Language.DirectLimit G f)

Equations

• FirstOrder.Language.instInhabitedDirectLimit G f = { default := ⟦{ fst := default, snd := default }⟧ }

theorem FirstOrder.Language.DirectLimit.equiv_iff {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] {x : FirstOrder.Language.Structure.Sigma f} {y : FirstOrder.Language.Structure.Sigma f} {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} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] {n : ℕ} (F : L.Functions n) (x : Fin n → FirstOrder.Language.Structure.Sigma f) (i : ι) (j : ι) (hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) (hj : j ∈ upperBounds (Set.range (Sigma.fst ∘ x))) : FirstOrder.Language.Structure.Sigma.mk f i (FirstOrder.Language.Structure.funMap F (FirstOrder.Language.DirectLimit.unify f x i hi)) ≈ FirstOrder.Language.Structure.Sigma.mk f j (FirstOrder.Language.Structure.funMap F (FirstOrder.Language.DirectLimit.unify f x j hj))

theorem FirstOrder.Language.DirectLimit.relMap_unify_equiv {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] {n : ℕ} (R : L.Relations n) (x : Fin n → FirstOrder.Language.Structure.Sigma f) (i : ι) (j : ι) (hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) (hj : j ∈ upperBounds (Set.range (Sigma.fst ∘ x))) : FirstOrder.Language.Structure.RelMap R (FirstOrder.Language.DirectLimit.unify f x i hi) = FirstOrder.Language.Structure.RelMap R (FirstOrder.Language.DirectLimit.unify f x j hj)

theorem FirstOrder.Language.DirectLimit.exists_unify_eq {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {α : Type u_1} [Fintype α] {x : α → FirstOrder.Language.Structure.Sigma f} {y : α → FirstOrder.Language.Structure.Sigma f} (xy : x ≈ y) : ∃ (i : ι) (hx : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (Set.range (Sigma.fst ∘ y))), FirstOrder.Language.DirectLimit.unify f x i hx = FirstOrder.Language.DirectLimit.unify f y i hy

theorem FirstOrder.Language.DirectLimit.funMap_equiv_unify {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {n : ℕ} (F : L.Functions n) (x : Fin n → FirstOrder.Language.Structure.Sigma f) (i : ι) (hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) : FirstOrder.Language.Structure.funMap F x ≈ FirstOrder.Language.Structure.Sigma.mk f i (FirstOrder.Language.Structure.funMap F (FirstOrder.Language.DirectLimit.unify f x i hi))

theorem FirstOrder.Language.DirectLimit.relMap_equiv_unify {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {n : ℕ} (R : L.Relations n) (x : Fin n → FirstOrder.Language.Structure.Sigma f) (i : ι) (hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) : FirstOrder.Language.Structure.RelMap R x = FirstOrder.Language.Structure.RelMap R (FirstOrder.Language.DirectLimit.unify f x i hi)

noncomputable instance FirstOrder.Language.DirectLimit.prestructure {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] : FirstOrder.Language.Prestructure L (FirstOrder.Language.DirectLimit.setoid G f)

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• FirstOrder.Language.DirectLimit.instStructureDirectLimit G f = FirstOrder.Language.quotientStructure

@[simp]

theorem FirstOrder.Language.DirectLimit.funMap_quotient_mk'_sigma_mk' {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {n : ℕ} {F : L.Functions n} {i : ι} {x : Fin n → G i} : (FirstOrder.Language.Structure.funMap F fun (a : Fin n) => ⟦FirstOrder.Language.Structure.Sigma.mk f i (x a)⟧) = ⟦FirstOrder.Language.Structure.Sigma.mk f i (FirstOrder.Language.Structure.funMap F x)⟧

@[simp]

theorem FirstOrder.Language.DirectLimit.relMap_quotient_mk'_sigma_mk' {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {n : ℕ} {R : L.Relations n} {i : ι} {x : Fin n → G i} : (FirstOrder.Language.Structure.RelMap R fun (a : Fin n) => ⟦FirstOrder.Language.Structure.Sigma.mk f i (x a)⟧) = FirstOrder.Language.Structure.RelMap R x

theorem FirstOrder.Language.DirectLimit.exists_quotient_mk'_sigma_mk'_eq {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {α : Type u_1} [Fintype α] (x : α → FirstOrder.Language.DirectLimit G f) : ∃ (i : ι) (y : α → G i), x = fun (a : α) => ⟦FirstOrder.Language.Structure.Sigma.mk f i (y a)⟧

def FirstOrder.Language.DirectLimit.of (L : FirstOrder.Language) (ι : Type v) [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] (i : ι) : FirstOrder.Language.Embedding L (G i) (FirstOrder.Language.DirectLimit G f)

The canonical map from a component to the direct limit.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FirstOrder.Language.DirectLimit.of_apply {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] {f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {i : ι} {x : G i} : (FirstOrder.Language.DirectLimit.of L ι G f i) x = ⟦FirstOrder.Language.Structure.Sigma.mk f i x⟧

theorem FirstOrder.Language.DirectLimit.of_f {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] {f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {i : ι} {j : ι} {hij : i ≤ j} {x : G i} : (FirstOrder.Language.DirectLimit.of L ι G f j) ((f i j hij) x) = (FirstOrder.Language.DirectLimit.of L ι G f i) x

theorem FirstOrder.Language.DirectLimit.exists_of {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] {f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] (z : FirstOrder.Language.DirectLimit G f) : ∃ (i : ι) (x : G i), (FirstOrder.Language.DirectLimit.of L ι G f i) 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} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] {f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {C : FirstOrder.Language.DirectLimit G f → Prop} (z : FirstOrder.Language.DirectLimit G f) (ih : ∀ (i : ι) (x : G i), C ((FirstOrder.Language.DirectLimit.of L ι G f i) x)) : C z

def FirstOrder.Language.DirectLimit.lift (L : FirstOrder.Language) (ι : Type v) [Preorder ι] (G : ι → Type w) [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {P : Type u₁} [FirstOrder.Language.Structure L P] (g : (i : ι) → FirstOrder.Language.Embedding L (G i) P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) : FirstOrder.Language.Embedding L (FirstOrder.Language.DirectLimit G f) P

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem FirstOrder.Language.DirectLimit.lift_quotient_mk'_sigma_mk' {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] {f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {P : Type u₁} [FirstOrder.Language.Structure L P] (g : (i : ι) → FirstOrder.Language.Embedding L (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) : (FirstOrder.Language.DirectLimit.lift L ι G f g Hg) ⟦FirstOrder.Language.Structure.Sigma.mk f i x⟧ = (g i) x

theorem FirstOrder.Language.DirectLimit.lift_of {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] {f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {P : Type u₁} [FirstOrder.Language.Structure L P] (g : (i : ι) → FirstOrder.Language.Embedding L (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) : (FirstOrder.Language.DirectLimit.lift L ι G f g Hg) ((FirstOrder.Language.DirectLimit.of L ι G f i) x) = (g i) x

theorem FirstOrder.Language.DirectLimit.lift_unique {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] {f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)} [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] [Nonempty ι] {P : Type u₁} [FirstOrder.Language.Structure L P] (F : FirstOrder.Language.Embedding L (FirstOrder.Language.DirectLimit G f) P) (x : FirstOrder.Language.DirectLimit G f) : F x = (FirstOrder.Language.DirectLimit.lift L ι G f (fun (i : ι) => FirstOrder.Language.Embedding.comp F (FirstOrder.Language.DirectLimit.of L ι G f i)) (_ : ∀ (i j : ι) (hij : i ≤ j) (x : G i), ((fun (i : ι) => FirstOrder.Language.Embedding.comp F (FirstOrder.Language.DirectLimit.of L ι G f i)) j) ((f i j hij) x) = ((fun (i : ι) => FirstOrder.Language.Embedding.comp F (FirstOrder.Language.DirectLimit.of L ι G f i)) i) x)) x

theorem FirstOrder.Language.DirectLimit.cg {L : FirstOrder.Language} {ι : Type u_1} [Encodable ι] [Preorder ι] [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [Nonempty ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) (h : ∀ (i : ι), FirstOrder.Language.Structure.CG L (G i)) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] : FirstOrder.Language.Structure.CG L (FirstOrder.Language.DirectLimit G f)

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

instance FirstOrder.Language.DirectLimit.cg' {L : FirstOrder.Language} {ι : Type u_1} [Encodable ι] [Preorder ι] [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] [Nonempty ι] {G : ι → Type w} [(i : ι) → FirstOrder.Language.Structure L (G i)] (f : (i j : ι) → i ≤ j → FirstOrder.Language.Embedding L (G i) (G j)) [h : ∀ (i : ι), FirstOrder.Language.Structure.CG L (G i)] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] : FirstOrder.Language.Structure.CG L (FirstOrder.Language.DirectLimit G f)

Equations

• (_ : FirstOrder.Language.Structure.CG L (FirstOrder.Language.DirectLimit G f)) = (_ : FirstOrder.Language.Structure.CG L (FirstOrder.Language.DirectLimit (fun (i : ι) => G i) f))