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 fis the direct limit of the directed systemfof first-order embeddings between the structures indexed byG.
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))
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
(i : ι)
(x : G i)
(h : i ≤ i) :
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))
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
{i j k : ι}
(hij : i ≤ j)
(hjk : j ≤ k)
(x : G i) :
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
- first_order.language.directed_system.nat_le_rec f' m n h = nat.le_rec_on h (λ (k : ℕ) (g : L.embedding (G' m) (G' k)), (f' k).comp g) (first_order.language.embedding.refl L (G' m))
@[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) :
⇑(first_order.language.directed_system.nat_le_rec f' m n h) = nat.le_rec_on h (λ (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))) :
directed_system G' (λ (i j : ℕ) (h : i ≤ j), ⇑(first_order.language.directed_system.nat_le_rec f' i j h))
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
- first_order.language.direct_limit.unify f x i h a = ⇑(f (x a).fst i _) (x a).snd
@[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))
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
{α : Type u_3}
{i : ι}
{x : α → G i} :
first_order.language.direct_limit.unify f (sigma.mk i ∘ x) 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))
[directed_system G (λ (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) ∘ first_order.language.direct_limit.unify f x i h = first_order.language.direct_limit.unify f x j _
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))
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[is_directed ι has_le.le] :
The directed limit glues together the structures along the embeddings.
Equations
- first_order.language.direct_limit.setoid G f = {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))
[is_directed ι has_le.le]
[nonempty ι] :
The structure on the Σ-type which becomes the structure on the direct limit after quotienting.
Equations
- first_order.language.direct_limit.sigma_structure G f = {fun_map := λ (n : ℕ) (F : L.functions n) (x : fin n → (Σ (i : ι), G i)), ⟨classical.some _, first_order.language.Structure.fun_map F (first_order.language.direct_limit.unify f x (classical.some _) _)⟩, rel_map := λ (n : ℕ) (R : L.relations n) (x : fin n → (Σ (i : ι), G i)), first_order.language.Structure.rel_map R (first_order.language.direct_limit.unify f x (classical.some _) _)}
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))
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[is_directed ι has_le.le] :
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))
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[is_directed ι has_le.le]
[inhabited ι]
[inhabited (G inhabited.default)] :
Equations
- first_order.language.direct_limit.inhabited G f = {default := ⟦⟨inhabited.default _inst_5, inhabited.default _inst_6⟩⟧}
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))
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
{x y : Σ (i : ι), G i}
{i : ι}
(hx : x.fst ≤ i)
(hy : y.fst ≤ i) :
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))
[is_directed ι has_le.le]
[directed_system G (λ (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))
[is_directed ι has_le.le]
[directed_system G (λ (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))
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[nonempty ι]
{α : Type u_3}
[fintype α]
{x y : α → (Σ (i : ι), G i)}
(xy : x ≈ y) :
∃ (i : ι) (hx : i ∈ upper_bounds (set.range (sigma.fst ∘ x))) (hy : i ∈ upper_bounds (set.range (sigma.fst ∘ y))), first_order.language.direct_limit.unify f x i hx = first_order.language.direct_limit.unify f y i hy
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))
[is_directed ι has_le.le]
[directed_system G (λ (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))
[is_directed ι has_le.le]
[directed_system G (λ (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))
[is_directed ι has_le.le]
[directed_system G (λ (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
- first_order.language.direct_limit.prestructure G f = {to_structure := first_order.language.direct_limit.sigma_structure G f _inst_5, fun_equiv := _, rel_equiv := _}
@[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))
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[nonempty ι] :
The L.Structure on a direct limit of L.Structures.
@[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))
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[nonempty ι]
{n : ℕ}
{F : L.functions n}
{i : ι}
{x : fin n → G i} :
first_order.language.Structure.fun_map F (λ (a : fin n), ⟦⟨i, x a⟩⟧) = ⟦⟨i, first_order.language.Structure.fun_map F x⟩⟧
@[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))
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[nonempty ι]
{n : ℕ}
{R : L.relations n}
{i : ι}
{x : fin n → G i} :
first_order.language.Structure.rel_map R (λ (a : fin n), ⟦⟨i, x a⟩⟧) = first_order.language.Structure.rel_map R x
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))
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[nonempty ι]
{α : Type u_3}
[fintype α]
(x : α → first_order.language.direct_limit G f) :
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))
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[nonempty ι]
(i : ι) :
L.embedding (G i) (first_order.language.direct_limit G f)
The canonical map from a component to the direct limit.
Equations
- first_order.language.direct_limit.of L ι G f i = {to_embedding := {to_fun := quotient.mk ∘ sigma.mk i, inj' := _}, map_fun' := _, map_rel' := _}
@[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)}
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[nonempty ι]
{i : ι}
{x : G i} :
@[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)}
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[nonempty ι]
{i j : ι}
{hij : i ≤ j}
{x : G i} :
⇑(first_order.language.direct_limit.of L ι G f j) (⇑(f i j hij) x) = ⇑(first_order.language.direct_limit.of L ι G f 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)}
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[nonempty ι]
(z : first_order.language.direct_limit G f) :
∃ (i : ι) (x : G i), ⇑(first_order.language.direct_limit.of L ι G f 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)}
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[nonempty ι]
{C : first_order.language.direct_limit G f → Prop}
(z : first_order.language.direct_limit G f)
(ih : ∀ (i : ι) (x : G i), C (⇑(first_order.language.direct_limit.of L ι G f 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))
[is_directed ι has_le.le]
[directed_system G (λ (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) :
L.embedding (first_order.language.direct_limit 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
- first_order.language.direct_limit.lift L ι G f g Hg = {to_embedding := {to_fun := quotient.lift (λ (x : Σ (i : ι), G i), ⇑(g x.fst) x.snd) _, inj' := _}, map_fun' := _, map_rel' := _}
@[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)}
[is_directed ι has_le.le]
[directed_system G (λ (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) :
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)}
[is_directed ι has_le.le]
[directed_system G (λ (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) :
⇑(first_order.language.direct_limit.lift L ι G f g Hg) (⇑(first_order.language.direct_limit.of L ι G f 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)}
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[nonempty ι]
{P : Type u₁}
[L.Structure P]
(F : L.embedding (first_order.language.direct_limit G f) P)
(x : first_order.language.direct_limit G f) :
⇑F x = ⇑(first_order.language.direct_limit.lift L ι G f (λ (i : ι), F.comp (first_order.language.direct_limit.of L ι G f i)) _) x
theorem
first_order.language.direct_limit.cg
{L : first_order.language}
{ι : Type u_3}
[encodable ι]
[preorder ι]
[is_directed ι has_le.le]
[nonempty ι]
{G : ι → Type w}
[Π (i : ι), L.Structure (G i)]
(f : Π (i j : ι), i ≤ j → L.embedding (G i) (G j))
(h : ∀ (i : ι), first_order.language.Structure.cg L (G i))
[directed_system G (λ (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 ι]
[is_directed ι has_le.le]
[nonempty ι]
{G : ι → Type w}
[Π (i : ι), L.Structure (G i)]
(f : Π (i j : ι), i ≤ j → L.embedding (G i) (G j))
[h : ∀ (i : ι), first_order.language.Structure.cg L (G i)]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))] :