FirstOrder.Language.HomClass.map_rel
theorem FirstOrder.Language.HomClass.map_rel :
∀ {L : outParam FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [inst : FunLike F M N]
[inst_1 : FirstOrder.Language.Structure L M] [inst_2 : FirstOrder.Language.Structure L N]
[self : FirstOrder.Language.HomClass L F M N] (φ : F) {n : ℕ} (r : L.Relations n) (x : Fin n → M),
FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x)
This theorem, named `FirstOrder.Language.HomClass.map_rel`, states that for any first-order language `L`, any type `F` acting like a function from `M` to `N`, and given structures of the language `L` on types `M` and `N`, if `F` is also a homomorphism between `M` and `N` in the language `L`, then for any function `φ` of type `F`, any relation `r` of the language `L` and any function `x` from the finite type `Fin n` to `M`, if the relation `r` holds on the interpretation of `x`, then the same relation `r` also holds on the interpretation of the composition of `φ` and `x`, which is essentially the mapping of `x` under the homomorphism `φ`. This theorem asserts the well-behavedness of the homomorphism in the context of first-order language structures by preserving relations.
More concisely: If `F` is a homomorphism between structures of a first-order language `L` on types `M` and `N`, and `φ` is a function of type `F`, then for any relation `r` of `L` and any function `x` from a finite type to `M` such that `r` holds for `x`, `r` also holds for the composition of `φ` and `x`.
|
FirstOrder.Language.StrongHomClass.map_rel
theorem FirstOrder.Language.StrongHomClass.map_rel :
∀ {L : outParam FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [inst : FunLike F M N]
[inst_1 : FirstOrder.Language.Structure L M] [inst_2 : FirstOrder.Language.Structure L N]
[self : FirstOrder.Language.StrongHomClass L F M N] (φ : F) {n : ℕ} (r : L.Relations n) (x : Fin n → M),
FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
The theorem `FirstOrder.Language.StrongHomClass.map_rel` states that for any first-order language `L`, any function or transformation `F` from `M` to `N` (where `M` and `N` are types in the context of `L`), and any relation `r` in `L` of arity `n`, if `φ` is an instance of `F` and `x` is a function from `Fin n` to `M`, then `r` holds for the image of `x` under `φ` if and only if `r` holds for `x`. In simpler terms, for strong homomorphisms (a structure-preserving map between two algebraic structures), the relation applied to the elements after they are transformed by the homomorphism is equivalent to the relation applied to the elements before the transformation. The function `φ` in this context is a strong homomorphism.
More concisely: For any first-order language L, if F is a strong homomorphism from M to N and r is an n-ary relation in L, then for any function x from Fin n to M, the relation r holds for the image of x under φ if and only if it holds for x.
|
FirstOrder.Language.Equiv.map_rel'
theorem FirstOrder.Language.Equiv.map_rel' :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
(self : L.Equiv M N) {n : ℕ} (r : L.Relations n) (x : Fin n → M),
FirstOrder.Language.Structure.RelMap r (self.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
This theorem is a property of homomorphisms in the context of first-order logics and structures. It states that for any given first-order language `L`, types `M` and `N` that are structures for `L`, and an equivalence between `M` and `N`, if a relation `r` of arity `n` holds for a tuple of elements of `M`, then the same relation holds for the corresponding tuple of elements of `N` obtained by applying the homomorphism. Similarly, if a relation holds for a tuple of elements in `N`, it also holds for the corresponding tuple of elements in `M`. This captures the idea that homomorphisms preserve the relational structure.
More concisely: Given first-order languages L, structures M and N with an equivalence between them, and a homomorphism f : M -> N, if r(m1, ..., mn) holds in M for elements m1, ..., mn of M, then r(f(m1), ..., f(mn)) holds in N, and vice versa.
|
FirstOrder.Language.Equiv.ext
theorem FirstOrder.Language.Equiv.ext :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
⦃f g : L.Equiv M N⦄, (∀ (x : M), f x = g x) → f = g
The theorem `FirstOrder.Language.Equiv.ext` states that for any first-order language `L` and any two types `M` and `N` that are structures of `L`, if two equivalence mappings `f` and `g` from `M` to `N` are such that for every element `x` in `M`, `f(x)` is equal to `g(x)`, then `f` and `g` are equal. This is a property of extensionality in the context of first-order logic language structures, asserting that two equivalence mappings are equal if they act the same way on every element of their domain.
More concisely: If `f` and `g` are equivalence mappings from a first-order language structure `M` to another structure `N` such that `f(x) = g(x)` for all `x` in `M`, then `f = g`.
|
FirstOrder.Language.Embedding.ext
theorem FirstOrder.Language.Embedding.ext :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
⦃f g : L.Embedding M N⦄, (∀ (x : M), f x = g x) → f = g
The theorem `FirstOrder.Language.Embedding.ext` states that for any two embeddings `f` and `g` from a structure `M` to another structure `N` in some first-order language `L`, if they map every element in `M` to the same element in `N` (i.e., `f x = g x` for all `x` in `M`), then these two embeddings are the same, `f = g`. In other words, two embeddings between the same structures in a first-order language are equal if they agree on all elements of the domain.
More concisely: In a first-order language, two embeddings of the same structure agreeing on all elements are equal.
|
FirstOrder.Language.HomClass.strongHomClassOfIsAlgebraic
theorem FirstOrder.Language.HomClass.strongHomClassOfIsAlgebraic :
∀ {L : FirstOrder.Language} [inst : L.IsAlgebraic] {F : Type u_3} {M : Type u_4} {N : Type u_5}
[inst : L.Structure M] [inst_1 : L.Structure N] [inst_2 : FunLike F M N] [inst_3 : L.HomClass F M N],
L.StrongHomClass F M N
The theorem `FirstOrder.Language.HomClass.strongHomClassOfIsAlgebraic` states that for any first-order language `L`, given that `L` is algebraic (meaning that elements of an `L`-algebra are roots of a non-zero polynomial with coefficients in `L`), we can derive the property that `L` has a "strong homomorphism class", provided we have a certain type `F` that can be injected into a function from `M` to `N`, where `M` and `N` are structures under the language `L`. A "strong homomorphism class" in this context means that for any homomorphism defined on the language, the image of a term under the homomorphism is equivalent to the term evaluated under the interpretation of the target structure.
More concisely: For any first-order language `L` that is algebraic and has a type `F` that can be mapped into a function from an `L`-structure `M` to an `L`-structure `N`, the homomorphism class of the underlying algebra of `M` is strong.
|
FirstOrder.Language.Embedding.map_fun'
theorem FirstOrder.Language.Embedding.map_fun' :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
(self : L.Embedding M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
self.toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (self.toFun ∘ x)
This theorem, named `FirstOrder.Language.Embedding.map_fun'`, states that for any first-order language `L`, any two structures `M` and `N` of this language, and any embedding from `M` to `N`, the embedding commutes with the interpretation of function symbols. In other words, if you have a function `f` in the language `L` and a tuple of elements `x` in `M`, then applying the embedding to the result of interpreting `f` on `x` in `M` is the same as interpreting `f` on the result of applying the embedding to `x` in `N`. This is a property that is expected from any homomorphism, and this theorem states that embeddings in first-order logic have this property.
More concisely: For any first-order language L, any embeddings e from structure M to N, and any function symbol f in L and elements x in M, we have e(interpretation of f in M [x]) = interpretation of f in N (e[x]).
|
FirstOrder.Language.StrongHomClass.map_fun
theorem FirstOrder.Language.StrongHomClass.map_fun :
∀ {L : outParam FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [inst : FunLike F M N]
[inst_1 : FirstOrder.Language.Structure L M] [inst_2 : FirstOrder.Language.Structure L N]
[self : FirstOrder.Language.StrongHomClass L F M N] (φ : F) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
This theorem, `FirstOrder.Language.StrongHomClass.map_fun`, states that for any language `L`, types `F`, `M`, `N` where `F` has a `FunLike` relationship from `M` to `N`, `L` has a structure over `M` and `N`, and `L` has a `StrongHomClass` from `F` to `M` and `N`, then for any function symbol `f` from `L` and any function `φ` from `F`, the application of `φ` on the interpretation of `f` on some elements of `M` is equal to the interpretation of `f` on the image of those elements under `φ`. That is, the homomorphism commutes with the interpretations of the function symbols in a first-order language structure.
More concisely: For any first-order language L, types F, M, N with FunLike relationship, and given a StrongHomClass homomorphism φ from F to M and N, the interpretation of function symbol f from L on the image of elements in M under φ is equal to the application of φ on the interpretation of f on those elements.
|
FirstOrder.Language.card_eq_card_functions_add_card_relations
theorem FirstOrder.Language.card_eq_card_functions_add_card_relations :
∀ {L : FirstOrder.Language},
L.card =
(Cardinal.sum fun l => Cardinal.lift.{v, u} (Cardinal.mk (L.Functions l))) +
Cardinal.sum fun l => Cardinal.lift.{u, v} (Cardinal.mk (L.Relations l))
This theorem states that for any first-order language `L`, the cardinality of `L` is equal to the sum of the cardinalities of the functions and relations in `L`. Specifically, the cardinality of `L` is the sum of the cardinality of the set of functions in `L` (each lifted to a higher universe level), and the cardinality of the set of relations in `L` (each also lifted to a higher universe level). The cardinalities of the sets of functions and relations are calculated as the indexed sum of their respective cardinalities, which is the cardinality of their indexed disjoint union, represented by the sigma type.
More concisely: The cardinality of a first-order language is the sum of the cardinalities of all functions and relations in it, each lifted to higher universe levels and represented as the indexed sum of their disjoint unions.
|
FirstOrder.Language.IsRelational.empty_functions
theorem FirstOrder.Language.IsRelational.empty_functions :
∀ {L : FirstOrder.Language} [self : L.IsRelational] (n : ℕ), IsEmpty (L.Functions n)
This theorem states that, for any first-order language `L` that is relational, there are no function symbols of arity `n` in the language. In other words, the set of function symbols of any arity `n` in a relational first-order language is empty.
More concisely: In a relational first-order language, the set of function symbols of any arity is empty.
|
FirstOrder.Language.Equiv.map_fun
theorem FirstOrder.Language.Equiv.map_fun :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
(φ : L.Equiv M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
The theorem `FirstOrder.Language.Equiv.map_fun` expresses that for any first-order language `L`, types `M` and `N`, given structures of the language `L` over `M` and `N`, and an equivalence `φ` between `M` and `N`, for any `n`-ary function `f` in the language and any function from `Fin n` to `M`, applying the equivalence `φ` after the function map of `f` and `x` in the `M` structure is the same as applying the function map of `f` in the `N` structure to the composition of `φ` and `x`. In simple terms, the theorem states that the process of mapping the function does not depend on which structure, `M` or `N`, the operation is conducted in, as long as we have an equivalence between the two structures.
More concisely: For any first-order language L, structures M and N, equivalence φ between M and N, n-ary function f in the language, and function g : Fin n → M, the function map of f applied to the composition of φ and g in the M structure is equal to the composition of the function map of f in the N structure and φ, i.e., (M.map_fun f g) φ = φ (N.map_fun f (g)).
|
FirstOrder.Language.Embedding.map_rel'
theorem FirstOrder.Language.Embedding.map_rel' :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
(self : L.Embedding M N) {n : ℕ} (r : L.Relations n) (x : Fin n → M),
FirstOrder.Language.Structure.RelMap r (self.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
The theorem `FirstOrder.Language.Embedding.map_rel'` in Lean 4 states that for any first-order language `L`, types `M` and `N`, structures on `M` and `N` in the language `L`, and an embedding `self` from `M` to `N`, for any `n`-ary relation `r` and function `x` from the finite set of size `n` to `M`, the relation `r` holds for the tuple obtained by applying `self.toFun ∘ x` if and only if the relation `r` holds for the tuple obtained by applying `x`. In other words, if a set of elements in `M` satisfy a certain relation, their images under the embedding in `N` will also satisfy the same relation, and vice versa. This theorem is a fundamental property of homomorphisms in the context of structures in first-order logic.
More concisely: For any first-order language, types, structures, embedding, and n-ary relation, if a tuple of elements in the domain of the embedding satisfies the relation, then the image of that tuple under the embedding also satisfies the relation.
|
FirstOrder.Language.Hom.comp_assoc
theorem FirstOrder.Language.Hom.comp_assoc :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
{P : Type u_1} [inst_2 : L.Structure P] {Q : Type u_2} [inst_3 : L.Structure Q] (f : L.Hom M N) (g : L.Hom N P)
(h : L.Hom P Q), (h.comp g).comp f = h.comp (g.comp f)
This theorem states that the composition of first-order homomorphisms is associative. In the context of a First-Order Language 'L', given three types 'M', 'N', and 'P' that have a structure in 'L', and given three homomorphisms 'f', 'g', and 'h' from 'M' to 'N', 'N' to 'P', and 'P' to 'Q' respectively, the composition of 'h' and 'g' followed by the composition with 'f' is the same as the composition of 'h' with the composition of 'g' and 'f'.
More concisely: For first-order structures M, N, P in a First-Order Language L and homomorphisms f : M -> N, g : N -> P, and h : P -> Q, the associativity of homomorphisms holds: (h ∘ g) ∘ f = h ∘ (g ∘ f).
|
FirstOrder.Language.Equiv.comp_assoc
theorem FirstOrder.Language.Equiv.comp_assoc :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
{P : Type u_1} [inst_2 : L.Structure P] {Q : Type u_2} [inst_3 : L.Structure Q] (f : L.Equiv M N)
(g : L.Equiv N P) (h : L.Equiv P Q), (h.comp g).comp f = h.comp (g.comp f)
The theorem `FirstOrder.Language.Equiv.comp_assoc` states that in the context of a FirstOrder language `L` and given structures `M`, `N`, `P`, and `Q` of this language, the composition of first-order homomorphisms (also known as language equivalences) is associative. In other words, given any three homomorphisms `f : L.Equiv M N`, `g : L.Equiv N P`, and `h : L.Equiv P Q`, the composition of `h` and `g` first, followed by the composition with `f` (`(h.comp g).comp f`), is the same as the composition of `h` with the composition of `g` and `f` first (`h.comp (g.comp f)`). This is a fundamental property in the theory of first-order languages.
More concisely: In a FirstOrder language L, the composition of any three first-order homomorphisms f : L.Equiv M N, g : L.Equiv N P, and h : L.Equiv P Q is associative: h.comp (g.comp f) = (h.comp g).comp f.
|
FirstOrder.Language.IsAlgebraic.empty_relations
theorem FirstOrder.Language.IsAlgebraic.empty_relations :
∀ {L : FirstOrder.Language} [self : L.IsAlgebraic] (n : ℕ), IsEmpty (L.Relations n)
The theorem `FirstOrder.Language.IsAlgebraic.empty_relations` states that for any first-order language `L` that is algebraic, and for any natural number `n`, the set of `n`-ary relation symbols in `L` is empty. In other words, there are no relation symbols in the language `L` that have arity `n`. Here, a first-order language being algebraic means that there exists an element of the language that is a root of a nonzero polynomial with coefficients in the language.
More concisely: In an algebraic first-order language, there are no relations of arbitrary arity.
|
FirstOrder.Language.Equiv.map_fun'
theorem FirstOrder.Language.Equiv.map_fun' :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
(self : L.Equiv M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
self.toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (self.toFun ∘ x)
The theorem `FirstOrder.Language.Equiv.map_fun'` in Lean states that for any first-order language `L` and any two types `M` and `N` with structures on `L`, given an equivalence `self` between `M` and `N`, and a function symbol `f` of `L` with `n` arguments, and a mapping `x` from `Fin n` to `M`, the action of the function symbol `f` (interpreted via `FirstOrder.Language.Structure.funMap`) on `x` under the equivalence `self` is the same as first applying `self` to `x` and then interpreting `f`. In simpler words, it states that the homomorphism (represented by `self`) commutes with the interpretations of the function symbols.
More concisely: Given a first-order language L, structures M and N on L, an equivalence self between M and N, and a function symbol f of arity n in L, for any mapping x from Fin n to M, the application of the function symbol f under self is equal to the composition of self with the application of f on x.
|
FirstOrder.Language.Hom.map_fun
theorem FirstOrder.Language.Hom.map_fun :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
(φ : L.Hom M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
The theorem `FirstOrder.Language.Hom.map_fun` states that for any first-order language `L`, types `M` and `N`, and language structures on `M` and `N`, if `φ` is a homomorphism from `M` to `N`, then for any `n`-ary function `f` in `L` and any map `x` from a `n`-dimensional finite set to `M`, applying `φ` to the result of mapping `f` via `x` is equal to first applying `φ` to the result of `x` and then mapping `f`. In other words, the function mapping operation of the language structure is compatible with the homomorphism `φ`.
More concisely: For any first-order language L, types M and N, language structures on M and N, homomorphism φ from M to N, n-ary function f in L, and map x from a n-dimensional finite set to M, we have φ(f^M(x)) = f^N(φ(x)).
|
FirstOrder.Language.HomClass.map_fun
theorem FirstOrder.Language.HomClass.map_fun :
∀ {L : outParam FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [inst : FunLike F M N]
[inst_1 : FirstOrder.Language.Structure L M] [inst_2 : FirstOrder.Language.Structure L N]
[self : FirstOrder.Language.HomClass L F M N] (φ : F) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
The theorem `FirstOrder.Language.HomClass.map_fun` states that for any first-order language `L`, any type `F` that has a `FunLike` relationship with types `M` and `N`, and any homomorphism `φ` from `M` to `N`, the action of the homomorphism `φ` commutes with the interpretation of first-order language function symbols. This means that for any function symbol `f` in the language and any sequence of elements `x` in `M`, applying the homomorphism `φ` after interpreting `f` on `x` is the same as interpreting `f` on the sequence obtained by applying `φ` to each element of `x`. In mathematical terms, this can be written as `φ(f(x)) = f(φ(x))`.
More concisely: For any first-order language L, given a homomorphism φ from type M to type N and a FunLike relation between type F and types M and N, the interpretation of function symbols commutes with φ, i.e., φ(f(x)) = f(φ(x)) for all function symbols f in L and sequences x in M.
|
FirstOrder.Language.HomClass.map_constants
theorem FirstOrder.Language.HomClass.map_constants :
∀ {L : FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [inst : L.Structure M]
[inst_1 : L.Structure N] [inst_2 : FunLike F M N] [inst_3 : L.HomClass F M N] (φ : F) (c : L.Constants),
φ ↑c = ↑c
The theorem `FirstOrder.Language.HomClass.map_constants` states that for any first-order language `L`, types `F`, `M`, and `N`, and given that `L` has a structure over `M` and `N`, and `F` can be coerced to a function from `M` to `N`. Furthermore, there also exists a homomorphism class for the language `L` with respect to `F`, `M`, and `N`. The theorem then asserts that for any element `φ` of type `F` and any constant `c` of the language `L`, the result of applying `φ` to the coercion of `c` is equal to the coercion of `c` itself. In other words, it ensures that constants are preserved under the application of the function-like term `φ`.
More concisely: For any first-order language L with a homomorphism class for functions from M to N, and given a function F coercible from M to N and an element φ of F, the application of φ to the constant c of L is equal to the constant c itself, i.e., φ(coercion c) = coercion c.
|
FirstOrder.Language.nonempty_of_nonempty_constants
theorem FirstOrder.Language.nonempty_of_nonempty_constants :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] [h : Nonempty L.Constants], Nonempty M
This theorem states that given a first-order language `L` with a nonempty set of constants, any structure `M` based on that language will also be nonempty. This theorem cannot be a global instance because `L` would become a metavariable.
More concisely: Given a first-order language with a nonempty set of constants, every structure based on that language is nonempty.
|
FirstOrder.Language.Hom.ext
theorem FirstOrder.Language.Hom.ext :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
⦃f g : L.Hom M N⦄, (∀ (x : M), f x = g x) → f = g
This theorem states that for any first-order language `L` and any two types `M` and `N` with `FirstOrder.Language.Structure` instances, any two homomorphisms `f` and `g` from `M` to `N` in the language `L` are equal if and only if they are equal at each element of `M`. In other words, if two homomorphisms `f` and `g` map each element of `M` to the same element in `N`, then `f` and `g` are identical.
More concisely: For any first-order language L and types M and N with structure instances, two homomorphisms f and g from M to N are equal if and only if they agree on every element of M.
|
FirstOrder.Language.Hom.map_rel'
theorem FirstOrder.Language.Hom.map_rel' :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
(self : L.Hom M N) {n : ℕ} (r : L.Relations n) (x : Fin n → M),
FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (self.toFun ∘ x)
The theorem `FirstOrder.Language.Hom.map_rel'` states that for any first-order language `L`, types `M` and `N`, where both `M` and `N` have a structure in the language `L`, any homomorphism `self` from `M` to `N`, any `n`-ary relation `r` in the language, and any function `x` mapping elements from a `n`-element finite set to `M`, if the relation `r` holds for the tuple obtained by `x`, then the same relation `r` also holds for the tuple obtained by applying the homomorphism `self` to `x`. In other words, the homomorphism preserves the relation `r` from `M` to `N`.
More concisely: For any first-order language L, types M and N with structures, homomorphism self from M to N, n-ary relation r in L, and function x mapping a finite n-element set to M, if r(x) holds then r(self (x)) holds. (The homomorphism self preserves the relation r from M to N.)
|
FirstOrder.Language.Embedding.comp_assoc
theorem FirstOrder.Language.Embedding.comp_assoc :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
{P : Type u_1} [inst_2 : L.Structure P] {Q : Type u_2} [inst_3 : L.Structure Q] (f : L.Embedding M N)
(g : L.Embedding N P) (h : L.Embedding P Q), (h.comp g).comp f = h.comp (g.comp f)
This theorem states that in the context of first-order languages, the composition of embeddings (which are structure-preserving mappings) is associative. That is, given three structures `M`, `N`, `P` and `Q` for a first-order language `L`, and embeddings `f: M->N`, `g: N->P`, and `h: P->Q`, the composition of `h`, `g`, and `f` is the same whether we first compose `h` and `g` and then compose the result with `f`, or first compose `g` and `f` and then compose `h` with the result. This mirrors the associative property in basic algebra where `(a * b) * c = a * (b * c)`.
More concisely: In the context of first-order languages, the composition of embeddings is associative: `(h ∘ g) ∘ f = h ∘ (g ∘ f)`.
|
FirstOrder.Language.Embedding.injective
theorem FirstOrder.Language.Embedding.injective :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
(f : L.Embedding M N), Function.Injective ⇑f
The theorem `FirstOrder.Language.Embedding.injective` states that for any first order language `L`, and any two types `M` and `N` that have a structure of this language, every embedding `f` from `M` to `N` in the context of language `L` is injective. In other words, if `f` is an embedding from `M` to `N`, and `f x = f y` for some elements `x` and `y` in `M`, then it must be the case that `x = y`. This means that no two distinct elements of `M` get mapped to the same element in `N` under the embedding `f`.
More concisely: Given any first order language L and embeddings f from type M to type N in the context of L, if x and y are distinct elements of M then f(x) and f(y) are distinct in N.
|
FirstOrder.Language.Hom.map_fun'
theorem FirstOrder.Language.Hom.map_fun' :
∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
(self : L.Hom M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
self.toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (self.toFun ∘ x)
This theorem states that for any first-order language `L`, types `M` and `N`, where `M` and `N` are structures for the language `L`, and any homomorphism `self` from `M` to `N`, the homomorphism commutes with the interpretations of the function symbols. This is demonstrated for any function `f` of `L` taking `n` arguments, and any function `x` from `Fin n` to `M`. More concretely, if we apply the function symbol `f` to `M` using the function `x` and then apply the homomorphism `self`, this is equivalent to first applying the homomorphism `self` to the arguments of `f` using the function `x` and then applying the function symbol `f` to `N`. This aligns with the mathematical concept of a homomorphism preserving the structure between two algebraic structures.
More concisely: For any first-order language L, structures M and N, and homomorphism self from M to N, self preserves the application of function symbols: for all function symbols f of L taking n arguments and any function x from Fin n to M, self (f^M x) = f^N (self x), where f^M and f^N denote the interpretation of the function symbol f in structures M and N, respectively.
|