FirstOrder.Language.DirectedSystem.map_map
theorem FirstOrder.Language.DirectedSystem.map_map :
∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : DirectedSystem G fun i j h => ⇑(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
This theorem is a version of `DirectedSystem.map_map` specialized to `L`-embeddings within the context of first-order languages. Given a directed system `G` where each instance is a structure of a first-order language `L` and `f` is a function from pairs of indices `i, j` (where `i ≤ j`) to an `L`-embedding from `G i` to `G j`. If `i ≤ j ≤ k`, then for any `x` in `G i`, applying `f` first from `i` to `j` and then from `j` to `k` is equal to directly applying `f` from `i` to `k`. This theorem addresses an issue where the simplifier could get confused by the function `f`.
More concisely: Given a directed system of first-order structures and an `L`-embedding function between structures, the composition of embeddings from `i` to `j` and from `j` to `k` is equal to the embedding directly from `i` to `k`.
|
FirstOrder.Language.DirectLimit.exists_of
theorem FirstOrder.Language.DirectLimit.exists_of :
∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
{f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)} [inst_2 : IsDirected ι fun x x_1 => x ≤ x_1]
[inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι]
(z : FirstOrder.Language.DirectLimit G f), ∃ i x, (FirstOrder.Language.DirectLimit.of L ι G f i) x = z
This theorem states that for every element in the direct limit of a directed system, there exists an element in some component of the directed system that corresponds to it. In specific, given a first-order language `L`, an ordered type `ι`, a function `G` mapping `ι` to another type, and a directed system `f` that provides an embedding between `G i` and `G j` for every pair `i, j` of `ι` such that `i` is less than or equal to `j`, we can assert that for any element `z` in the direct limit of `G` with respect to `f`, there exists an `i` in `ι` and an `x` in the structure of `L` on `G i` such that `x` maps to `z` in the direct limit.
More concisely: For every element in the direct limit of a directed system, there exists a component element that maps to it.
|
FirstOrder.Language.DirectLimit.cg
theorem FirstOrder.Language.DirectLimit.cg :
∀ {L : FirstOrder.Language} {ι : Type u_1} [inst : Countable ι] [inst : Preorder ι]
[inst_1 : IsDirected ι fun x x_1 => x ≤ x_1] [inst_2 : Nonempty ι] {G : ι → Type w}
[inst_3 : (i : ι) → L.Structure (G i)] (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)),
(∀ (i : ι), FirstOrder.Language.Structure.CG L (G i)) →
∀ [inst_4 : DirectedSystem G fun i j h => ⇑(f i j h)],
FirstOrder.Language.Structure.CG L (FirstOrder.Language.DirectLimit G f)
This theorem states that in the context of first-order logic, the direct limit of a countably infinite sequence of countably generated structures is itself countably generated. Here, each structure in the sequence is embedded into the next with a certain ordering, and all the structures are related through this ordered embedding. This result is important because it ensures that the property of being countably generated, which can simplify reasoning about a structure, is preserved under the construction of direct limits.
More concisely: The direct limit of a countably infinite sequence of countably generated first-order structures, where each structure is embedded into the next, is itself countably generated.
|
FirstOrder.Language.DirectedSystem.map_self
theorem FirstOrder.Language.DirectedSystem.map_self :
∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
(f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : DirectedSystem G fun i j h => ⇑(f i j h)] (i : ι)
(x : G i) (h : i ≤ i), (f i i h) x = x
This theorem, `FirstOrder.Language.DirectedSystem.map_self`, states that for any first-order language `L`, type `ι` with a preorder, a directed system `G` of `L`-structures indexed by `ι`, and a function `f` that produces an `L`-embedding from `G i` to `G j` for any `i ≤ j`, the embedding for `i` into itself when applied to any element `x` of `G i` is just `x` itself. In other words, when `f` maps an element from one structure to the same structure, it acts as the identity function.
More concisely: For any first-order language L, preorder ι, directed system G of L-structures indexed by ι, and function f that is an L-embedding from Gi to Gj for any i <= j, we have f (x) = x for all x in Gi.
|