# 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.
• FirstOrder.Language.DirectLimit.lift is 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_lift is the equivalence between limits of isomorphic direct systems.
theorem FirstOrder.Language.DirectedSystem.map_self {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.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} [] {G : ιType w} [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.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
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) :
= 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) =>
Equations
• =
@[reducible, inline]
abbrev FirstOrder.Language.Structure.Sigma {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) :
Type (max v w)

Alias for Σ i, G i.

Equations
• = ((i : ι) × G i)
Instances For
@[reducible, inline]
abbrev FirstOrder.Language.Structure.Sigma.mk {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) (i : ι) (x : G i) :

Constructor for FirstOrder.Language.Structure.Sigma alias.

Equations
• = i, x
Instances For
def FirstOrder.Language.DirectLimit.unify {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) {α : Type u_1} (x : ) (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
• = (f (x a).fst i ) (x a).snd
Instances For
@[simp]
theorem FirstOrder.Language.DirectLimit.unify_sigma_mk_self {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.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 : α) => ) i = x
theorem FirstOrder.Language.DirectLimit.comp_unify {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] {α : Type u_1} {x : } {i : ι} {j : ι} (ij : i j) (h : i upperBounds (Set.range (Sigma.fst x))) :
(f i j ij) =
def FirstOrder.Language.DirectLimit.setoid {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.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} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [IsDirected ι fun (x1 x2 : ι) => x1 x2] [] :
L.Structure

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} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.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} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [] [Inhabited (G default)] :
Equations
• = { default := default, default }
theorem FirstOrder.Language.DirectLimit.equiv_iff {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] {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} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.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 : ) (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} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.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 : ) (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} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] {α : Type u_1} [] {x : } {y : } (xy : x y) :
∃ (i : ι) (hx : i upperBounds (Set.range (Sigma.fst x))) (hy : i upperBounds (Set.range (Sigma.fst y))),
theorem FirstOrder.Language.DirectLimit.funMap_equiv_unify {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.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 : ) (i : ι) (hi : i upperBounds (Set.range (Sigma.fst x))) :
theorem FirstOrder.Language.DirectLimit.relMap_equiv_unify {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.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 : ) (i : ι) (hi : i upperBounds (Set.range (Sigma.fst x))) :
noncomputable instance FirstOrder.Language.DirectLimit.prestructure {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] :
L.Prestructure

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

Equations
• = { toStructure := , fun_equiv := , rel_equiv := }
noncomputable instance FirstOrder.Language.DirectLimit.instStructureDirectLimit {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] :
L.Structure

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

Equations
• = FirstOrder.Language.quotientStructure
@[simp]
theorem FirstOrder.Language.DirectLimit.funMap_quotient_mk'_sigma_mk' {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.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} {i : ι} {x : Fin nG i} :
(FirstOrder.Language.Structure.funMap F fun (a : Fin n) => ) =
@[simp]
theorem FirstOrder.Language.DirectLimit.relMap_quotient_mk'_sigma_mk' {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.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} {i : ι} {x : Fin nG i} :
(FirstOrder.Language.Structure.RelMap R fun (a : Fin n) => ) =
theorem FirstOrder.Language.DirectLimit.exists_quotient_mk'_sigma_mk'_eq {L : FirstOrder.Language} {ι : Type v} [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] {α : Type u_1} [] (x : ) :
∃ (i : ι) (y : αG i), x = fun (a : α) =>
def FirstOrder.Language.DirectLimit.of (L : FirstOrder.Language) (ι : Type v) [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] (i : ι) :
L.Embedding (G i)

The canonical map from a component to the direct limit.

Equations
• = { toFun := fun (a : G i) => , inj' := , map_fun' := , map_rel' := }
Instances For
@[simp]
theorem FirstOrder.Language.DirectLimit.of_apply {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] {f : (i j : ι) → i jL.Embedding (G i) (G j)} [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] {i : ι} {x : G i} :
x =
theorem FirstOrder.Language.DirectLimit.of_f {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] {f : (i j : ι) → i jL.Embedding (G i) (G j)} [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] {i : ι} {j : ι} {hij : i j} {x : G i} :
((f i j hij) x) = x
theorem FirstOrder.Language.DirectLimit.exists_of {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] {f : (i j : ι) → i jL.Embedding (G i) (G j)} [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] (z : ) :
∃ (i : ι) (x : G 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} [] {G : ιType w} [(i : ι) → L.Structure (G i)] {f : (i j : ι) → i jL.Embedding (G i) (G j)} [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] {C : } (z : ) (ih : ∀ (i : ι) (x : G i), C ( x)) :
C z
theorem FirstOrder.Language.DirectLimit.iSup_range_of_eq_top {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] {f : (i j : ι) → i jL.Embedding (G i) (G j)} [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] :
⨆ (i : ι), .toHom.range =
theorem FirstOrder.Language.DirectLimit.exists_fg_substructure_in_Sigma {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] {f : (i j : ι) → i jL.Embedding (G i) (G j)} [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] (S : L.Substructure ) (S_fg : S.FG) :
∃ (i : ι) (T : L.Substructure (G i)), FirstOrder.Language.Substructure.map .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) [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] {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 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
• = { toFun := Quotient.lift (fun (x : ) => (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} [] {G : ιType w} [(i : ι) → L.Structure (G i)] {f : (i j : ι) → i jL.Embedding (G i) (G j)} [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] {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) = (g i) x
theorem FirstOrder.Language.DirectLimit.lift_of {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] {f : (i j : ι) → i jL.Embedding (G i) (G j)} [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] {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) ( x) = (g i) x
theorem FirstOrder.Language.DirectLimit.lift_unique {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] {f : (i j : ι) → i jL.Embedding (G i) (G j)} [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] {P : Type u₁} [L.Structure P] (F : L.Embedding P) (x : ) :
F x = (FirstOrder.Language.DirectLimit.lift L ι G f (fun (i : ι) => F.comp ) ) x
theorem FirstOrder.Language.DirectLimit.range_lift {L : FirstOrder.Language} {ι : Type v} [] {G : ιType w} [(i : ι) → L.Structure (G i)] {f : (i j : ι) → i jL.Embedding (G i) (G j)} [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] {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) [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] (G' : ιType w') [(i : ι) → L.Structure (G' i)] (f' : (i j : ι) → i jL.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

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) [] (G : ιType w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [] (G' : ιType w') [(i : ι) → L.Structure (G' i)] (f' : (i j : ι) → i jL.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) ( x) = (FirstOrder.Language.DirectLimit.of L ι G' f' i) ((g i) x)
theorem FirstOrder.Language.DirectLimit.cg {L : FirstOrder.Language} {ι : Type u_1} [] [] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [] {G : ιType w} [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) (h : ∀ (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} [] [] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [] {G : ιType w} [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i jL.Embedding (G i) (G j)) [h : ∀ (i : ι), ] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] :
Equations
• =
instance FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion {L : FirstOrder.Language} {ι : Type v} [] {M : Type u_1} [L.Structure M] (S : ι →o L.Substructure M) :
DirectedSystem (fun (i : ι) => { x : M // x S i }) fun (x x_1 : ι) (h : x x_1) =>
Equations
• =
def FirstOrder.Language.DirectLimit.liftInclusion {L : FirstOrder.Language} {ι : Type v} [] [] [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 : ι) => { x : M // x S i }) fun (x x_1 : ι) (h : x x_1) => ) 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} [] [] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {M : Type u_1} [L.Structure M] (S : ι →o L.Substructure M) {i : ι} (x : { x : M // x S i }) :
((FirstOrder.Language.DirectLimit.of L ι (fun (x : ι) => { x_1 : M // x_1 S x }) (fun (x x_1 : ι) (h : x x_1) => ) i) x) = (S i).subtype x
theorem FirstOrder.Language.DirectLimit.rangeLiftInclusion {L : FirstOrder.Language} {ι : Type v} [] [] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {M : Type u_1} [L.Structure M] (S : ι →o L.Substructure M) :
.range = ⨆ (i : ι), S i
noncomputable def FirstOrder.Language.DirectLimit.Equiv_iSup {L : FirstOrder.Language} {ι : Type v} [] [] [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 : ι) => { x : M // x S i }) fun (x x_1 : ι) (h : x x_1) => ) { x : M // x 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} [] [] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {M : Type u_1} [L.Structure M] (S : ι →o L.Substructure M) {i : ι} (x : { x : M // x S i }) :
((FirstOrder.Language.DirectLimit.of L ι (fun (x : ι) => { x_1 : M // x_1 S x }) (fun (x x_1 : ι) (h : x x_1) => ) i) x) =
theorem FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply {L : FirstOrder.Language} {ι : Type v} [] [] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {M : Type u_1} [L.Structure M] (S : ι →o L.Substructure M) {i : ι} (x : { x : M // x S i }) :
= (FirstOrder.Language.DirectLimit.of L ι (fun (x : ι) => { x_1 : M // x_1 S x }) (fun (x x_1 : ι) (h : x x_1) => ) i) x
@[simp]
theorem FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion {L : FirstOrder.Language} {ι : Type v} [] [] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {M : Type u_1} [L.Structure M] (S : ι →o L.Substructure M) (i : ι) :
.toEmbedding.comp = FirstOrder.Language.DirectLimit.of L ι (fun (x : ι) => { x_1 : M // x_1 S x }) (fun (x x_1 : ι) (h : x x_1) => ) i