mathlib documentation

model_theory.direct_limit

Direct Limits of First-Order Structures #

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

Main Definitions #

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 jL.embedding (G i) (G j)) [directed_system G (λ (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 jL.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) :
(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) :
@[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))) :
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 jL.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 jL.embedding (G i) (G j)) [directed_system G (λ (i j : ι) (h : i j), (f i j h))] {α : Type u_3} {i : ι} {x : α → G i} :
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 jL.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))) :
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 jL.embedding (G i) (G j)) [directed_system G (λ (i j : ι) (h : i j), (f i j h))] [is_directed ι has_le.le] :
setoid (Σ (i : ι), G i)

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 jL.embedding (G i) (G j)) [is_directed ι has_le.le] [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 jL.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 jL.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
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 jL.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) :
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 jL.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 jL.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 jL.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) :
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 jL.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 jL.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 jL.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
@[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 jL.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.

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 jL.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 nG i} :
@[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 jL.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 nG i} :
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 jL.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) :
∃ (i : ι) (y : α → G i), x = quotient.mk sigma.mk i y
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 jL.embedding (G i) (G j)) [is_directed ι has_le.le] [directed_system G (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] (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 jL.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 jL.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} :
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 jL.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 jL.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 jL.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) :

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 jL.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 jL.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_unique {L : first_order.language} {ι : Type v} [preorder ι] {G : ι → Type w} [Π (i : ι), L.Structure (G i)] {f : Π (i j : ι), i jL.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) :
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 jL.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 jL.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))] :