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.FirstOrder.Language.DirectLimit.liftis the universal property of the direct limit: maps from the components to another module that respect the directed system structure give rise to a unique map out of the direct limit.FirstOrder.Language.DirectLimit.equiv_liftis the equivalence between limits of isomorphic direct systems.
theorem
FirstOrder.Language.DirectedSystem.map_self
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (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 : ℕ) → 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 DirectedSystem by
composing them.
Equations
- FirstOrder.Language.DirectedSystem.natLERec f' m n h = Nat.leRecOn h (fun (k : ℕ) (g : L.Embedding (G' m) (G' k)) => (f' k).comp g) (FirstOrder.Language.Embedding.refl L (G' m))
Instances For
@[simp]
theorem
FirstOrder.Language.DirectedSystem.coe_natLERec
{L : FirstOrder.Language}
{G' : ℕ → Type w}
[(i : ℕ) → L.Structure (G' i)]
(f' : (n : ℕ) → L.Embedding (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 : ℕ) → L.Structure (G' i)]
(f' : (n : ℕ) → L.Embedding (G' n) (G' (n + 1)))
:
DirectedSystem G' fun (i j : ℕ) (h : i ≤ j) => ⇑(FirstOrder.Language.DirectedSystem.natLERec f' i j h)
@[reducible, inline]
abbrev
FirstOrder.Language.Structure.Sigma
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
:
Type (max v w)
Alias for Σ i, G i.
Equations
- FirstOrder.Language.Structure.Sigma f = ((i : ι) × G i)
Instances For
@[reducible, inline]
abbrev
FirstOrder.Language.Structure.Sigma.mk
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
(i : ι)
(x : G i)
:
Constructor for FirstOrder.Language.Structure.Sigma alias.
Equations
- FirstOrder.Language.Structure.Sigma.mk f i x = ⟨i, x⟩
Instances For
def
FirstOrder.Language.DirectLimit.unify
{L : FirstOrder.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_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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
:
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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[Nonempty ι]
:
L.Structure (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.
Instances For
def
FirstOrder.Language.DirectLimit
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
:
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.instInhabitedDirectLimitOfDefault
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[Inhabited ι]
[Inhabited (G default)]
:
Equations
- FirstOrder.Language.instInhabitedDirectLimitOfDefault G f = { default := ⟦⟨default, default⟩⟧ }
theorem
FirstOrder.Language.DirectLimit.equiv_iff
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
{x 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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[Nonempty ι]
{α : Type u_1}
[Finite α]
{x 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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[Nonempty ι]
:
L.Prestructure (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
- 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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[Nonempty ι]
:
L.Structure (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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[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 : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[Nonempty ι]
(i : ι)
:
L.Embedding (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 = { 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 : ι) → L.Structure (G i)]
{f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[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 : ι) → L.Structure (G i)]
{f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[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 : ι) → L.Structure (G i)]
{f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[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 : ι) → L.Structure (G i)]
{f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[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
theorem
FirstOrder.Language.DirectLimit.iSup_range_of_eq_top
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → L.Structure (G i)]
{f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[Nonempty ι]
:
⨆ (i : ι), (FirstOrder.Language.DirectLimit.of L ι G f i).toHom.range = ⊤
theorem
FirstOrder.Language.DirectLimit.exists_fg_substructure_in_Sigma
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → L.Structure (G i)]
{f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[Nonempty ι]
(S : L.Substructure (FirstOrder.Language.DirectLimit G f))
(S_fg : S.FG)
:
∃ (i : ι) (T : L.Substructure (G i)),
FirstOrder.Language.Substructure.map (FirstOrder.Language.DirectLimit.of L ι G f i).toHom T = S
Every finitely generated substructure of the direct limit corresponds to some substructure in some component of the directed system.
def
FirstOrder.Language.DirectLimit.lift
(L : FirstOrder.Language)
(ι : Type v)
[Preorder ι]
(G : ι → Type w)
[(i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (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 (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
- FirstOrder.Language.DirectLimit.lift L ι G f g Hg = { toFun := Quotient.lift (fun (x : FirstOrder.Language.Structure.Sigma f) => (g x.fst) x.snd) ⋯, inj' := ⋯, map_fun' := ⋯, map_rel' := ⋯ }
Instances For
@[simp]
theorem
FirstOrder.Language.DirectLimit.lift_quotient_mk'_sigma_mk'
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → L.Structure (G i)]
{f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (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)
:
(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 : ι) → L.Structure (G i)]
{f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (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)
:
(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 : ι) → L.Structure (G i)]
{f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[Nonempty ι]
{P : Type u₁}
[L.Structure P]
(F : L.Embedding (FirstOrder.Language.DirectLimit G f) P)
(x : FirstOrder.Language.DirectLimit G f)
:
F x = (FirstOrder.Language.DirectLimit.lift L ι G f (fun (i : ι) => F.comp (FirstOrder.Language.DirectLimit.of L ι G f i))
⋯)
x
theorem
FirstOrder.Language.DirectLimit.range_lift
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → L.Structure (G i)]
{f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (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)
:
(FirstOrder.Language.DirectLimit.lift L ι G f g Hg).toHom.range = ⨆ (i : ι), (g i).toHom.range
noncomputable def
FirstOrder.Language.DirectLimit.equiv_lift
(L : FirstOrder.Language)
(ι : Type v)
[Preorder ι]
(G : ι → Type w)
[(i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[Nonempty ι]
(G' : ι → Type w')
[(i : ι) → L.Structure (G' i)]
(f' : (i j : ι) → i ≤ j → L.Embedding (G' i) (G' j))
(g : (i : ι) → L.Equiv (G i) (G' i))
[DirectedSystem G' fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)]
(H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x))
:
L.Equiv (FirstOrder.Language.DirectLimit G f) (FirstOrder.Language.DirectLimit G' f')
The isomorphism between limits of isomorphic systems.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
FirstOrder.Language.DirectLimit.equiv_lift_of
(L : FirstOrder.Language)
(ι : Type v)
[Preorder ι]
(G : ι → Type w)
[(i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[Nonempty ι]
(G' : ι → Type w')
[(i : ι) → L.Structure (G' i)]
(f' : (i j : ι) → i ≤ j → L.Embedding (G' i) (G' j))
(g : (i : ι) → L.Equiv (G i) (G' i))
[DirectedSystem G' fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)]
(H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x))
{i : ι}
(x : G i)
:
(FirstOrder.Language.DirectLimit.equiv_lift L ι G f G' f' g H_commuting)
((FirstOrder.Language.DirectLimit.of L ι G f i) x) = (FirstOrder.Language.DirectLimit.of L ι G' f' i) ((g i) x)
theorem
FirstOrder.Language.DirectLimit.cg
{L : FirstOrder.Language}
{ι : Type u_1}
[Countable ι]
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[Nonempty ι]
{G : ι → Type w}
[(i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (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 (x1 x2 : ι) => x1 ≤ x2]
[Nonempty ι]
{G : ι → Type w}
[(i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (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)]
:
instance
FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
{M : Type u_1}
[L.Structure M]
(S : ι →o L.Substructure M)
:
DirectedSystem (fun (i : ι) => ↥(S i)) fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(FirstOrder.Language.Substructure.inclusion ⋯)
def
FirstOrder.Language.DirectLimit.liftInclusion
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{M : Type u_1}
[L.Structure M]
(S : ι →o L.Substructure M)
:
L.Embedding
(FirstOrder.Language.DirectLimit (fun (i : ι) => ↥(S i)) fun (x x_1 : ι) (h : x ≤ x_1) =>
FirstOrder.Language.Substructure.inclusion ⋯)
M
The map from a direct limit of a system of substructures of M into M.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
FirstOrder.Language.DirectLimit.liftInclusion_of
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{M : Type u_1}
[L.Structure M]
(S : ι →o L.Substructure M)
{i : ι}
(x : ↥(S i))
:
(FirstOrder.Language.DirectLimit.liftInclusion S)
((FirstOrder.Language.DirectLimit.of L ι (fun (x : ι) => ↥(S x))
(fun (x x_1 : ι) (h : x ≤ x_1) => FirstOrder.Language.Substructure.inclusion ⋯) i)
x) = (S i).subtype x
theorem
FirstOrder.Language.DirectLimit.rangeLiftInclusion
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{M : Type u_1}
[L.Structure M]
(S : ι →o L.Substructure M)
:
(FirstOrder.Language.DirectLimit.liftInclusion S).toHom.range = ⨆ (i : ι), S i
noncomputable def
FirstOrder.Language.DirectLimit.Equiv_iSup
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{M : Type u_1}
[L.Structure M]
(S : ι →o L.Substructure M)
:
L.Equiv
(FirstOrder.Language.DirectLimit (fun (i : ι) => ↥(S i)) fun (x x_1 : ι) (h : x ≤ x_1) =>
FirstOrder.Language.Substructure.inclusion ⋯)
↥(iSup ⇑S)
The isomorphism between a direct limit of a system of substructures and their union.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
FirstOrder.Language.DirectLimit.Equiv_isup_of_apply
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{M : Type u_1}
[L.Structure M]
(S : ι →o L.Substructure M)
{i : ι}
(x : ↥(S i))
:
(FirstOrder.Language.DirectLimit.Equiv_iSup S)
((FirstOrder.Language.DirectLimit.of L ι (fun (x : ι) => ↥(S x))
(fun (x x_1 : ι) (h : x ≤ x_1) => FirstOrder.Language.Substructure.inclusion ⋯) i)
x) = (FirstOrder.Language.Substructure.inclusion ⋯) x
theorem
FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{M : Type u_1}
[L.Structure M]
(S : ι →o L.Substructure M)
{i : ι}
(x : ↥(S i))
:
(FirstOrder.Language.DirectLimit.Equiv_iSup S).symm ((FirstOrder.Language.Substructure.inclusion ⋯) x) = (FirstOrder.Language.DirectLimit.of L ι (fun (x : ι) => ↥(S x))
(fun (x x_1 : ι) (h : x ≤ x_1) => FirstOrder.Language.Substructure.inclusion ⋯) i)
x
@[simp]
theorem
FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion
{L : FirstOrder.Language}
{ι : Type v}
[Preorder ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{M : Type u_1}
[L.Structure M]
(S : ι →o L.Substructure M)
(i : ι)
:
(FirstOrder.Language.DirectLimit.Equiv_iSup S).symm.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion ⋯) = FirstOrder.Language.DirectLimit.of L ι (fun (x : ι) => ↥(S x))
(fun (x x_1 : ι) (h : x ≤ x_1) => FirstOrder.Language.Substructure.inclusion ⋯) i