model_theory.basic - mathlib3 docs

mathlib3 documentation

model_theory.basic

Basics on First-Order Structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines first-order languages and structures in the style of the Flypitch project, as well as several important maps between structures.

Main Definitions #

  • A first_order.language defines a language as a pair of functions from the natural numbers to Type l. One sends n to the type of n-ary functions, and the other sends n to the type of n-ary relations.
  • A first_order.language.Structure interprets the symbols of a given first_order.language in the context of a given type.
  • A first_order.language.hom, denoted M →[L] N, is a map from the L-structure M to the L-structure N that commutes with the interpretations of functions, and which preserves the interpretations of relations (although only in the forward direction).
  • A first_order.language.embedding, denoted M ↪[L] N, is an embedding from the L-structure M to the L-structure N that commutes with the interpretations of functions, and which preserves the interpretations of relations in both directions.
  • A first_order.language.elementary_embedding, denoted M ↪ₑ[L] N, is an embedding from the L-structure M to the L-structure N that commutes with the realizations of all formulas.
  • A first_order.language.equiv, denoted M ≃[L] N, is an equivalence from the L-structure M to the L-structure N that commutes with the interpretations of functions, and which preserves the interpretations of relations in both directions.

TODO #

Use [countable L.symbols] instead of [L.countable].

References #

For the Flypitch project:

Languages and Structures #

source
@[nolint]
structure first_order.language  :
Type (max (u+1) (v+1))

A first-order language consists of a type of functions of every natural-number arity and a type of relations of every natural-number arity.

Instances for first_order.language
source
@[simp]
def first_order.sequence₂ (a₀ a₁ a₂ : Type u) :
ℕ → Type u

Used to define first_order.language₂.

Equations
Instances for first_order.sequence₂
source
@[protected, instance]
def first_order.sequence₂.inhabited₀ (a₀ a₁ a₂ : Type u) [h : inhabited a₀] :
inhabited (first_order.sequence₂ a₀ a₁ a₂ 0)
Equations
source
@[protected, instance]
def first_order.sequence₂.inhabited₁ (a₀ a₁ a₂ : Type u) [h : inhabited a₁] :
inhabited (first_order.sequence₂ a₀ a₁ a₂ 1)
Equations
source
@[protected, instance]
def first_order.sequence₂.inhabited₂ (a₀ a₁ a₂ : Type u) [h : inhabited a₂] :
inhabited (first_order.sequence₂ a₀ a₁ a₂ 2)
Equations
source
@[protected, instance]
def first_order.sequence₂.is_empty (a₀ a₁ a₂ : Type u) {n : ℕ} :
is_empty (first_order.sequence₂ a₀ a₁ a₂ (n + 3))
source
@[simp]
theorem first_order.sequence₂.lift_mk (a₀ a₁ a₂ : Type u) {i : ℕ} :
(cardinal.mk (first_order.sequence₂ a₀ a₁ a₂ i)).lift = cardinal.mk (first_order.sequence₂ (ulift a₀) (ulift a₁) (ulift a₂) i)
source
@[simp]
theorem first_order.sequence₂.sum_card (a₀ a₁ a₂ : Type u) :
cardinal.sum (λ (i : ℕ), cardinal.mk (first_order.sequence₂ a₀ a₁ a₂ i)) = cardinal.mk a₀ + cardinal.mk a₁ + cardinal.mk a₂
source
@[simp]
theorem first_order.language.mk₂_relations (c f₁ f₂ : Type u) (r₁ r₂ : Type v) (ᾰ : ℕ) :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).relations ᾰ = first_order.sequence₂ pempty r₁ r₂ ᾰ
source
@[simp]
theorem first_order.language.mk₂_functions (c f₁ f₂ : Type u) (r₁ r₂ : Type v) (ᾰ : ℕ) :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).functions ᾰ = first_order.sequence₂ c f₁ f₂ ᾰ
source
@[protected]
def first_order.language.mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) :
first_order.language

A constructor for languages with only constants, unary and binary functions, and unary and binary relations.

Equations
Instances for first_order.language.mk₂
source
@[protected]
def first_order.language.sum (L : first_order.language) (L' : first_order.language) :
first_order.language

The sum of two languages consists of the disjoint union of their symbols.

Equations
Instances for first_order.language.sum
source
@[protected, nolint]
def first_order.language.constants (L : first_order.language) :
Type u

The type of constants in a given language.

Equations
Instances for first_order.language.constants
source
@[simp]
theorem first_order.language.constants_mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).constants = c
source
@[nolint]
def first_order.language.symbols (L : first_order.language) :
Type (max u v)

The type of symbols in a given language.

Equations
Instances for first_order.language.symbols
source
def first_order.language.card (L : first_order.language) :
cardinal

The cardinality of a language is the cardinality of its type of symbols.

Equations
source
@[protected, instance]
def first_order.language.is_relational_of_empty_functions {symb : ℕ → Type u_1} :
{functions := λ (_x : ℕ), empty, relations := symb}.is_relational
source
@[protected, instance]
def first_order.language.is_algebraic_of_empty_relations {symb : ℕ → Type u_1} :
{functions := symb, relations := λ (_x : ℕ), empty}.is_algebraic
source
@[protected, instance]
def first_order.language.is_relational_mk₂ {c f₁ f₂ : Type u} {r₁ r₂ : Type v} [h0 : is_empty c] [h1 : is_empty f₁] [h2 : is_empty f₂] :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).is_relational
source
@[protected, instance]
def first_order.language.is_algebraic_mk₂ {c f₁ f₂ : Type u} {r₁ r₂ : Type v} [h1 : is_empty r₁] [h2 : is_empty r₂] :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).is_algebraic
source
@[protected, instance]
def first_order.language.subsingleton_mk₂_functions {c f₁ f₂ : Type u} {r₁ r₂ : Type v} [h0 : subsingleton c] [h1 : subsingleton f₁] [h2 : subsingleton f₂] {n : ℕ} :
subsingleton ((first_order.language.mk₂ c f₁ f₂ r₁ r₂).functions n)
source
@[protected, instance]
def first_order.language.subsingleton_mk₂_relations {c f₁ f₂ : Type u} {r₁ r₂ : Type v} [h1 : subsingleton r₁] [h2 : subsingleton r₂] {n : ℕ} :
subsingleton ((first_order.language.mk₂ c f₁ f₂ r₁ r₂).relations n)
source
@[simp]
theorem first_order.language.card_mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).card = (cardinal.mk c).lift + (cardinal.mk f₁).lift + (cardinal.mk f₂).lift + (cardinal.mk r₁).lift + (cardinal.mk r₂).lift

Maps #

source
structure first_order.language.hom (L : first_order.language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] :
Type (max w w')

A homomorphism between first-order structures is a function that commutes with the interpretations of functions and maps tuples in one structure where a given relation is true to tuples in the second structure where that relation is still true.

Instances for first_order.language.hom
source
structure first_order.language.embedding (L : first_order.language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] :
Type (max w w')

An embedding of first-order structures is an embedding that commutes with the interpretations of functions and relations.

Instances for first_order.language.embedding
source
structure first_order.language.equiv (L : first_order.language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] :
Type (max w w')

An equivalence of first-order structures is an equivalence that commutes with the interpretations of functions and relations.

Instances for first_order.language.equiv
source
theorem first_order.language.nonempty_of_nonempty_constants {L : first_order.language} {M : Type w} [L.Structure M] [h : nonempty L.constants] :
nonempty M

Given a language with a nonempty type of constants, any structure will be nonempty. This cannot be a global instance, because L becomes a metavariable.

source
def first_order.language.fun_map₂ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} (c' : c → M) (f₁' : f₁ → M → M) (f₂' : f₂ → M → M → M) {n : ℕ} :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).functions n → (fin n → M) → M

The function map for first_order.language.Structure₂.

Equations
source
def first_order.language.rel_map₂ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} (r₁' : r₁ → set M) (r₂' : r₂ → M → M → Prop) {n : ℕ} :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).relations n → (fin n → M) → Prop

The relation map for first_order.language.Structure₂.

Equations
source
@[protected]
def first_order.language.Structure.mk₂ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} (c' : c → M) (f₁' : f₁ → M → M) (f₂' : f₂ → M → M → M) (r₁' : r₁ → set M) (r₂' : r₂ → M → M → Prop) :
(first_order.language.mk₂ c f₁ f₂ r₁ r₂).Structure M

A structure constructor to match first_order.language₂.

Equations
source
@[simp]
theorem first_order.language.Structure.fun_map_apply₀ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} {c' : c → M} {f₁' : f₁ → M → M} {f₂' : f₂ → M → M → M} {r₁' : r₁ → set M} {r₂' : r₂ → M → M → Prop} (c₀ : c) {x : fin 0 → M} :
first_order.language.Structure.fun_map c₀ x = c' c₀
source
@[simp]
theorem first_order.language.Structure.fun_map_apply₁ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} {c' : c → M} {f₁' : f₁ → M → M} {f₂' : f₂ → M → M → M} {r₁' : r₁ → set M} {r₂' : r₂ → M → M → Prop} (f : f₁) (x : M) :
first_order.language.Structure.fun_map f ![x] = f₁' f x
source
@[simp]
theorem first_order.language.Structure.fun_map_apply₂ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} {c' : c → M} {f₁' : f₁ → M → M} {f₂' : f₂ → M → M → M} {r₁' : r₁ → set M} {r₂' : r₂ → M → M → Prop} (f : f₂) (x y : M) :
first_order.language.Structure.fun_map f ![x, y] = f₂' f x y
source
@[simp]
theorem first_order.language.Structure.rel_map_apply₁ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} {c' : c → M} {f₁' : f₁ → M → M} {f₂' : f₂ → M → M → M} {r₁' : r₁ → set M} {r₂' : r₂ → M → M → Prop} (r : r₁) (x : M) :
first_order.language.Structure.rel_map r ![x] = (x ∈ r₁' r)
source
@[simp]
theorem first_order.language.Structure.rel_map_apply₂ {M : Type w} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} {c' : c → M} {f₁' : f₁ → M → M} {f₂' : f₂ → M → M → M} {r₁' : r₁ → set M} {r₂' : r₂ → M → M → Prop} (r : r₂) (x y : M) :
first_order.language.Structure.rel_map r ![x, y] = r₂' r x y
source
@[class]
structure first_order.language.hom_class (L : out_param first_order.language) (F : Type u_5) (M : out_param (Type u_6)) (N : out_param (Type u_7)) [fun_like F M (λ (_x : M), N)] [first_order.language.Structure L M] [first_order.language.Structure L N] :
Type

hom_class L F M N states that F is a type of L-homomorphisms. You should extend this typeclass when you extend first_order.language.hom.

Instances of this typeclass
Instances of other typeclasses for first_order.language.hom_class
  • first_order.language.hom_class.has_sizeof_inst
source
@[class]
structure first_order.language.strong_hom_class (L : out_param first_order.language) (F : Type u_5) (M : out_param (Type u_6)) (N : out_param (Type u_7)) [fun_like F M (λ (_x : M), N)] [first_order.language.Structure L M] [first_order.language.Structure L N] :
Type

strong_hom_class L F M N states that F is a type of L-homomorphisms which preserve relations in both directions.

Instances of this typeclass
Instances of other typeclasses for first_order.language.strong_hom_class
  • first_order.language.strong_hom_class.has_sizeof_inst
source
theorem first_order.language.hom_class.map_constants {L : first_order.language} {F : Type u_1} {M : Type u_2} {N : Type u_3} [L.Structure M] [L.Structure N] [fun_like F M (λ (_x : M), N)] [first_order.language.hom_class L F M N] (φ : F) (c : L.constants) :
⇑φ ↑c = ↑c
source
@[protected, instance]
def first_order.language.hom.fun_like {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
fun_like (L.hom M N) M (λ (_x : M), N)
Equations
source
@[protected, instance]
def first_order.language.hom.hom_class {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
first_order.language.hom_class L (L.hom M N) M N
Equations
source
@[protected, instance]
def first_order.language.hom.has_coe_to_fun {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
has_coe_to_fun (L.hom M N) (λ (_x : L.hom M N), M → N)
Equations
source
@[simp]
theorem first_order.language.hom.to_fun_eq_coe {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.hom M N} :
f.to_fun = ⇑f
source
@[ext]
theorem first_order.language.hom.ext {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] ⦃f g : L.hom M N⦄ (h : ∀ (x : M), ⇑f x = ⇑g x) :
f = g
source
theorem first_order.language.hom.ext_iff {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.hom M N} :
f = g ↔ ∀ (x : M), ⇑f x = ⇑g x
source
@[simp]
theorem first_order.language.hom.map_fun {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.hom M N) {n : ℕ} (f : L.functions n) (x : fin n → M) :
⇑φ (first_order.language.Structure.fun_map f x) = first_order.language.Structure.fun_map f (⇑φ ∘ x)
source
@[simp]
theorem first_order.language.hom.map_constants {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.hom M N) (c : L.constants) :
⇑φ ↑c = ↑c
source
@[refl]
def first_order.language.hom.id (L : first_order.language) (M : Type w) [L.Structure M] :
L.hom M M

The identity map from a structure to itself

Equations
source
@[trans]
def first_order.language.hom.comp {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.hom N P) (hmn : L.hom M N) :
L.hom M P

Composition of first-order homomorphisms

Equations
source
@[simp]
theorem first_order.language.hom.comp_apply {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (g : L.hom N P) (f : L.hom M N) (x : M) :
⇑(g.comp f) x = ⇑g (⇑f x)
source
theorem first_order.language.hom.comp_assoc {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] {Q : Type u_2} [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)

Composition of first-order homomorphisms is associative.

source
def first_order.language.hom_class.to_hom {L : first_order.language} {F : Type u_1} {M : Type u_2} {N : Type u_3} [L.Structure M] [L.Structure N] [fun_like F M (λ (_x : M), N)] [first_order.language.hom_class L F M N] :
F → L.hom M N

Any element of a hom_class can be realized as a first_order homomorphism.

Equations
source
@[simp]
theorem first_order.language.embedding.map_constants {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.embedding M N) (c : L.constants) :
⇑φ ↑c = ↑c
source
def first_order.language.embedding.to_hom {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
L.embedding M N → L.hom M N

A first-order embedding is also a first-order homomorphism.

Equations
source
@[simp]
theorem first_order.language.embedding.coe_to_hom {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.embedding M N} :
⇑(f.to_hom) = ⇑f
source
@[ext]
theorem first_order.language.embedding.ext {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] ⦃f g : L.embedding M N⦄ (h : ∀ (x : M), ⇑f x = ⇑g x) :
f = g
source
theorem first_order.language.embedding.ext_iff {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.embedding M N} :
f = g ↔ ∀ (x : M), ⇑f x = ⇑g x
source
def first_order.language.embedding.of_injective {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.is_algebraic] {f : L.hom M N} (hf : function.injective ⇑f) :
L.embedding M N

In an algebraic language, any injective homomorphism is an embedding.

Equations
source
@[refl]
def first_order.language.embedding.refl (L : first_order.language) (M : Type w) [L.Structure M] :
L.embedding M M

The identity embedding from a structure to itself

Equations
source
@[trans]
def first_order.language.embedding.comp {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.embedding N P) (hmn : L.embedding M N) :
L.embedding M P

Composition of first-order embeddings

Equations
source
@[simp]
theorem first_order.language.embedding.comp_apply {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (g : L.embedding N P) (f : L.embedding M N) (x : M) :
⇑(g.comp f) x = ⇑g (⇑f x)
source
theorem first_order.language.embedding.comp_assoc {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] {Q : Type u_2} [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)

Composition of first-order embeddings is associative.

source
@[simp]
theorem first_order.language.embedding.comp_to_hom {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.embedding N P) (hmn : L.embedding M N) :
(hnp.comp hmn).to_hom = hnp.to_hom.comp hmn.to_hom
source
def first_order.language.strong_hom_class.to_embedding {L : first_order.language} {F : Type u_1} {M : Type u_2} {N : Type u_3} [L.Structure M] [L.Structure N] [embedding_like F M N] [first_order.language.strong_hom_class L F M N] :
F → L.embedding M N

Any element of an injective strong_hom_class can be realized as a first_order embedding.

Equations
source
@[protected, instance]
def first_order.language.equiv.equiv_like {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
equiv_like (L.equiv M N) M N
Equations
source
@[symm]
def first_order.language.equiv.symm {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
L.equiv N M

The inverse of a first-order equivalence is a first-order equivalence.

Equations
source
@[simp]
theorem first_order.language.equiv.apply_symm_apply {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) (a : N) :
⇑f (⇑(f.symm) a) = a
source
@[simp]
theorem first_order.language.equiv.symm_apply_apply {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) (a : M) :
⇑(f.symm) (⇑f a) = a
source
@[simp]
theorem first_order.language.equiv.map_constants {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.equiv M N) (c : L.constants) :
⇑φ ↑c = ↑c
source
def first_order.language.equiv.to_embedding {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
L.equiv M N → L.embedding M N

A first-order equivalence is also a first-order embedding.

Equations
source
def first_order.language.equiv.to_hom {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
L.equiv M N → L.hom M N

A first-order equivalence is also a first-order homomorphism.

Equations
source
@[simp]
theorem first_order.language.equiv.coe_to_hom {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.equiv M N} :
⇑(f.to_hom) = ⇑f
source
@[simp]
theorem first_order.language.equiv.coe_to_embedding {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
⇑(f.to_embedding) = ⇑f
source
@[ext]
theorem first_order.language.equiv.ext {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] ⦃f g : L.equiv M N⦄ (h : ∀ (x : M), ⇑f x = ⇑g x) :
f = g
source
theorem first_order.language.equiv.ext_iff {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.equiv M N} :
f = g ↔ ∀ (x : M), ⇑f x = ⇑g x
source
@[refl]
def first_order.language.equiv.refl (L : first_order.language) (M : Type w) [L.Structure M] :
L.equiv M M

The identity equivalence from a structure to itself

Equations
source
@[trans]
def first_order.language.equiv.comp {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.equiv N P) (hmn : L.equiv M N) :
L.equiv M P

Composition of first-order equivalences

Equations
source
@[simp]
theorem first_order.language.equiv.comp_apply {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (g : L.equiv N P) (f : L.equiv M N) (x : M) :
⇑(g.comp f) x = ⇑g (⇑f x)
source
theorem first_order.language.equiv.comp_assoc {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] {Q : Type u_2} [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)

Composition of first-order homomorphisms is associative.

source
def first_order.language.strong_hom_class.to_equiv {L : first_order.language} {F : Type u_1} {M : Type u_2} {N : Type u_3} [L.Structure M] [L.Structure N] [equiv_like F M N] [first_order.language.strong_hom_class L F M N] :
F → L.equiv M N

Any element of a bijective strong_hom_class can be realized as a first_order isomorphism.

Equations
source
def function.empty_hom {M : Type w} {N : Type w'} (f : M → N) :
first_order.language.empty.hom M N

Makes a language.empty.hom out of any function.

Equations
source
@[simp]
theorem function.empty_hom_to_fun {M : Type w} {N : Type w'} (f : M → N) (ᾰ : M) :
⇑(function.empty_hom f) ᾰ = f ᾰ
source
def embedding.empty {M : Type w} {N : Type w'} (f : M ↪ N) :
first_order.language.empty.embedding M N

Makes a language.empty.embedding out of any function.

Equations
source
@[simp]
theorem embedding.empty_to_embedding {M : Type w} {N : Type w'} (f : M ↪ N) :
(embedding.empty f).to_embedding = f
source
def equiv.empty {M : Type w} {N : Type w'} (f : M ≃ N) :
first_order.language.empty.equiv M N

Makes a language.empty.equiv out of any function.

Equations
source
@[simp]
theorem equiv.empty_to_equiv {M : Type w} {N : Type w'} (f : M ≃ N) :
f.empty.to_equiv = f
source
def equiv.induced_Structure {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] (e : M ≃ N) :
L.Structure N

A structure induced by a bijection.

Equations
source
@[simp]
theorem equiv.induced_Structure_equiv_to_equiv_apply {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] (e : M ≃ N) (ᾰ : M) :
⇑(e.induced_Structure_equiv.to_equiv) ᾰ = e.to_fun ᾰ
source
@[simp]
theorem equiv.induced_Structure_equiv_to_equiv_symm_apply {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] (e : M ≃ N) (ᾰ : N) :
⇑(e.induced_Structure_equiv.to_equiv.symm) ᾰ = e.inv_fun ᾰ
source
def equiv.induced_Structure_equiv {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] (e : M ≃ N) :
L.equiv M N

A bijection as a first-order isomorphism with the induced structure on the codomain.

Equations