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
{ι : Type u_1}
[Preorder ι]
{F : ι → Type u_4}
{T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
(f : (i j : ι) → (h : i ≤ j) → T h)
[⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
[DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)]
⦃i : ι⦄
(x : F i)
:
Alias of DirectedSystem.map_self'.
A copy of DirectedSystem.map_self specialized to FunLike, as otherwise the
fun i j h ↦ f i j h can confuse the simplifier.
theorem
FirstOrder.Language.DirectedSystem.map_map
{ι : Type u_1}
[Preorder ι]
{F : ι → Type u_4}
{T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
(f : (i j : ι) → (h : i ≤ j) → T h)
[⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
[DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)]
⦃i j k : ι⦄
(hij : i ≤ j)
(hjk : j ≤ k)
(x : F i)
:
Alias of DirectedSystem.map_map'.
A copy of DirectedSystem.map_map specialized to FunLike, as otherwise the
fun i j h ↦ f i j h can confuse the simplifier.
def
FirstOrder.Language.DirectedSystem.natLERec
{L : 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))
@[reducible, inline]
abbrev
FirstOrder.Language.Structure.Sigma
{L : 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.
Instead of Σ i, G i, we use the alias Language.Structure.Sigma which depends on f.
This way, Lean can infer what L and f are in the Setoid instance.
Otherwise we have a "cannot find synthesization order" error.
See also the discussion at
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/local.20instance.20cannot.20find.20synthesization.20order.20in.20porting
Equations
- FirstOrder.Language.Structure.Sigma f = ((i : ι) × G i)
@[reducible, inline]
abbrev
FirstOrder.Language.Structure.Sigma.mk
{L : 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⟩
def
FirstOrder.Language.DirectLimit.unify
{L : 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 : α → 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
@[simp]
theorem
FirstOrder.Language.DirectLimit.comp_unify
{L : 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 : α → Structure.Sigma f}
{i j : ι}
(ij : i ≤ j)
(h : i ∈ upperBounds (Set.range (Sigma.fst ∘ x)))
:
def
FirstOrder.Language.DirectLimit.setoid
{L : 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.
noncomputable def
FirstOrder.Language.DirectLimit.sigmaStructure
{L : 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 (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.
def
FirstOrder.Language.DirectLimit
{L : 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
instance
FirstOrder.Language.instInhabitedDirectLimitOfDefault
{L : 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)]
:
Inhabited (DirectLimit G f)
theorem
FirstOrder.Language.DirectLimit.equiv_iff
{L : 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 : Structure.Sigma f}
{i : ι}
(hx : x.fst ≤ i)
(hy : y.fst ≤ i)
:
theorem
FirstOrder.Language.DirectLimit.funMap_unify_equiv
{L : 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 → Structure.Sigma f)
(i j : ι)
(hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x)))
(hj : j ∈ upperBounds (Set.range (Sigma.fst ∘ x)))
:
Structure.Sigma.mk f i (Structure.funMap F (unify f x i hi)) ≈ Structure.Sigma.mk f j (Structure.funMap F (unify f x j hj))
theorem
FirstOrder.Language.DirectLimit.relMap_unify_equiv
{L : 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 → 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 : 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 : α → Structure.Sigma f}
(xy : x ≈ y)
:
theorem
FirstOrder.Language.DirectLimit.funMap_equiv_unify
{L : 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 → Structure.Sigma f)
(i : ι)
(hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x)))
:
theorem
FirstOrder.Language.DirectLimit.relMap_equiv_unify
{L : 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 → Structure.Sigma f)
(i : ι)
(hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x)))
:
noncomputable instance
FirstOrder.Language.DirectLimit.prestructure
{L : 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 (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 : 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 (DirectLimit G f)
The L.Structure on a direct limit of L.Structures.
@[simp]
theorem
FirstOrder.Language.DirectLimit.funMap_quotient_mk'_sigma_mk'
{L : 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}
:
(Structure.funMap F fun (a : Fin n) => ⟦Structure.Sigma.mk f i (x a)⟧) = ⟦Structure.Sigma.mk f i (Structure.funMap F x)⟧
@[simp]
theorem
FirstOrder.Language.DirectLimit.relMap_quotient_mk'_sigma_mk'
{L : 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}
:
theorem
FirstOrder.Language.DirectLimit.exists_quotient_mk'_sigma_mk'_eq
{L : 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 : α → DirectLimit G f)
:
∃ (i : ι) (y : α → G i), x = fun (a : α) => ⟦Structure.Sigma.mk f i (y a)⟧
noncomputable def
FirstOrder.Language.DirectLimit.of
(L : 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) (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' := ⋯ }
@[simp]
theorem
FirstOrder.Language.DirectLimit.of_apply
{L : 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}
:
theorem
FirstOrder.Language.DirectLimit.of_f
{L : 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}
:
theorem
FirstOrder.Language.DirectLimit.exists_of
{L : 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 : DirectLimit G f)
:
Every element of the direct limit corresponds to some element in some component of the directed system.
theorem
FirstOrder.Language.DirectLimit.inductionOn
{L : 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 : DirectLimit G f → Prop}
(z : DirectLimit G f)
(ih : ∀ (i : ι) (x : G i), C ((of L ι G f i) x))
:
C z
theorem
FirstOrder.Language.DirectLimit.iSup_range_of_eq_top
{L : 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 ι]
:
theorem
FirstOrder.Language.DirectLimit.exists_fg_substructure_in_Sigma
{L : 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 (DirectLimit G f))
(S_fg : S.FG)
:
∃ (i : ι) (T : L.Substructure (G i)), Substructure.map (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.
noncomputable def
FirstOrder.Language.DirectLimit.lift
(L : 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 (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' := ⋯ }
@[simp]
theorem
FirstOrder.Language.DirectLimit.lift_quotient_mk'_sigma_mk'
{L : 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)
:
theorem
FirstOrder.Language.DirectLimit.lift_of
{L : 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)
:
theorem
FirstOrder.Language.DirectLimit.lift_unique
{L : 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 (DirectLimit G f) P)
(x : DirectLimit G f)
:
theorem
FirstOrder.Language.DirectLimit.range_lift
{L : 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)
:
noncomputable def
FirstOrder.Language.DirectLimit.equiv_lift
(L : 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 (DirectLimit G f) (DirectLimit G' f')
The isomorphism between limits of isomorphic systems.
Equations
- One or more equations did not get rendered due to their size.
theorem
FirstOrder.Language.DirectLimit.equiv_lift_of
(L : 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)
:
theorem
FirstOrder.Language.DirectLimit.cg
{L : 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 : ι), Structure.CG L (G i))
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
:
Structure.CG L (DirectLimit G f)
The direct limit of countably many countably generated structures is countably generated.
instance
FirstOrder.Language.DirectLimit.cg'
{L : 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 : ι), Structure.CG L (G i)]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
:
Structure.CG L (DirectLimit G f)
instance
FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion
{L : 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) => ⇑(Substructure.inclusion ⋯)
noncomputable def
FirstOrder.Language.DirectLimit.liftInclusion
{L : 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 (DirectLimit (fun (i : ι) => ↥(S i)) fun (x x_1 : ι) (h : x ≤ x_1) => 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.
theorem
FirstOrder.Language.DirectLimit.liftInclusion_of
{L : 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))
:
(liftInclusion S) ((of L ι (fun (x : ι) => ↥(S x)) (fun (x x_1 : ι) (h : x ≤ x_1) => Substructure.inclusion ⋯) i) x) = (S i).subtype x
theorem
FirstOrder.Language.DirectLimit.rangeLiftInclusion
{L : Language}
{ι : Type v}
[Preorder ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{M : Type u_1}
[L.Structure M]
(S : ι →o L.Substructure M)
:
noncomputable def
FirstOrder.Language.DirectLimit.Equiv_iSup
{L : 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 (DirectLimit (fun (i : ι) => ↥(S i)) fun (x x_1 : ι) (h : x ≤ x_1) => 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.
theorem
FirstOrder.Language.DirectLimit.Equiv_isup_of_apply
{L : 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))
:
(Equiv_iSup S) ((of L ι (fun (x : ι) => ↥(S x)) (fun (x x_1 : ι) (h : x ≤ x_1) => Substructure.inclusion ⋯) i) x) = (Substructure.inclusion ⋯) x
theorem
FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply
{L : 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))
:
(Equiv_iSup S).symm ((Substructure.inclusion ⋯) x) = (of L ι (fun (x : ι) => ↥(S x)) (fun (x x_1 : ι) (h : x ≤ x_1) => Substructure.inclusion ⋯) i) x
@[simp]
theorem
FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion
{L : Language}
{ι : Type v}
[Preorder ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{M : Type u_1}
[L.Structure M]
(S : ι →o L.Substructure M)
(i : ι)
:
(Equiv_iSup S).symm.toEmbedding.comp (Substructure.inclusion ⋯) = of L ι (fun (x : ι) => ↥(S x)) (fun (x x_1 : ι) (h : x ≤ x_1) => Substructure.inclusion ⋯) i