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 fis the direct limit of the directed systemfof first-order embeddings between the structures indexed byG.
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
fun 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 ⋯) x
A copy of DirectedSystem.map_map specialized to L-embeddings, as otherwise the
fun 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.
Instances For
@[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
- ⋯ = ⋯
@[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)
Instances For
@[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)
:
Constructor for FirstOrder.Language.Structure.Sigma alias.
Equations
- FirstOrder.Language.Structure.Sigma.mk f i x = { fst := i, snd := x }
Instances For
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).snd
Instances For
@[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 ⋯ = 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 ⋯
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]
:
The directed limit glues together the structures along the embeddings.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 ι]
:
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.
Instances For
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
Instances For
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)]
:
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)
:
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)))
:
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)))
:
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}
[Finite α]
{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)))
:
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)))
:
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 ι]
:
The direct limit setoid respects the structure sigmaStructure, so quotienting by it
gives rise to a valid structure.
Equations
- FirstOrder.Language.DirectLimit.prestructure G f = { toStructure := FirstOrder.Language.DirectLimit.sigmaStructure G f, fun_equiv := ⋯, rel_equiv := ⋯ }
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 ι]
:
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}
[Finite α]
(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
- FirstOrder.Language.DirectLimit.of L ι G f i = { toEmbedding := { toFun := fun (a : G i) => ⟦FirstOrder.Language.Structure.Sigma.mk f i a⟧, inj' := ⋯ }, map_fun' := ⋯, map_rel' := ⋯ }
Instances For
@[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)
:
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.
Instances For
@[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)) ⋯)
x
theorem
FirstOrder.Language.DirectLimit.cg
{L : FirstOrder.Language}
{ι : Type u_1}
[Countable ι]
[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)]
:
The direct limit of countably many countably generated structures is countably generated.
instance
FirstOrder.Language.DirectLimit.cg'
{L : FirstOrder.Language}
{ι : Type u_1}
[Countable ι]
[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)]
:
Equations
- ⋯ = ⋯