FirstOrder.Language.LHom.map_onRelation
theorem FirstOrder.Language.LHom.map_onRelation :
∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L.LHom L') {M : Type u_1} [inst : L.Structure M]
[inst_1 : L'.Structure M] [inst_2 : ϕ.IsExpansionOn M] {n : ℕ} (R : L.Relations n) (x : Fin n → M),
FirstOrder.Language.Structure.RelMap (ϕ.onRelation R) x = FirstOrder.Language.Structure.RelMap R x
The theorem `FirstOrder.Language.LHom.map_onRelation` states that for any two first-order languages `L` and `L'` and a language homomorphism `ϕ` from `L` to `L'`, for any structure `M` of type `u_1` that is a model of both `L` and `L'`, and given `ϕ` is an expansion on `M`, for any relation `R` of `L` with arity `n` and any `n`-tuple `x` from `M`, the interpretation of the relation symbol after applying the homomorphism `ϕ` to `R` (i.e., `ϕ.onRelation R`) on `x` in the model `M` is the same as the interpretation of `R` on `x` in `M`. This means that the homomorphism `ϕ` preserves the interpretation of the relation symbols in the model `M`.
More concisely: Given first-order languages L and L', a language homomorphism φ from L to L', and a model M of both languages where φ is an expansion, for any relation R of arity n in L and any n-tuple x in M, φ.onRelation R(x) = R(x).
|
FirstOrder.Language.LHom.map_onFunction
theorem FirstOrder.Language.LHom.map_onFunction :
∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L.LHom L') {M : Type u_1} [inst : L.Structure M]
[inst_1 : L'.Structure M] [inst_2 : ϕ.IsExpansionOn M] {n : ℕ} (f : L.Functions n) (x : Fin n → M),
FirstOrder.Language.Structure.funMap (ϕ.onFunction f) x = FirstOrder.Language.Structure.funMap f x
The theorem `FirstOrder.Language.LHom.map_onFunction` states that for any two first-order languages `L` and `L'`, a language homomorphism `ϕ` from `L` to `L'`, a structure `M` for the languages `L` and `L'`, and a function `f` from `L` of arity `n`, given that `ϕ` is an expansion on `M`, the interpretation of the function `f` under this homomorphism applied to a sequence `x` of elements from `M` is equal to the interpretation of the function `f` applied to the same sequence `x`. In other words, the homomorphism `ϕ` preserves the interpretation of functions in language `L` to `L'`.
More concisely: For any first-order languages L and L', homomorphism ϕ from L to L', structure M for L and L', and function f : L^n, if ϕ is an expansion on M, then phi(f^M(x_1, ..., x_n)) = f^M(phi(x_1), ..., phi(x_n)) for all x_1, ..., x_n in M.
|
FirstOrder.Language.LHom.funext
theorem FirstOrder.Language.LHom.funext :
∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {F G : L.LHom L'},
F.onFunction = G.onFunction → F.onRelation = G.onRelation → F = G
This theorem states that for any two language homomorphisms `F` and `G` from a first-order language `L` to another first-order language `L'`, if `F` and `G` map the same functions to the same functions in `L'`, and `F` and `G` map the same relations to the same relations in `L'`, then `F` and `G` are identical. In other words, two language homomorphisms are equal if they map functions and relations in the same way from one language to another.
More concisely: If two first-order language homomorphisms from one language to another agree on the mapping of functions and relations, then they are equal.
|