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 #

TODO #

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

References #

For the Flypitch project:

Languages and Structures #

@[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
@[simp]
def first_order.sequence₂ (a₀ a₁ a₂ : Type u) :

Used to define first_order.language₂.

Equations
Instances for first_order.sequence₂
@[protected, instance]
def first_order.sequence₂.inhabited₀ (a₀ a₁ a₂ : Type u) [h : inhabited a₀] :
Equations
@[protected, instance]
def first_order.sequence₂.inhabited₁ (a₀ a₁ a₂ : Type u) [h : inhabited a₁] :
Equations
@[protected, instance]
def first_order.sequence₂.inhabited₂ (a₀ a₁ a₂ : Type u) [h : inhabited a₂] :
Equations
@[protected, instance]
def first_order.sequence₂.is_empty (a₀ a₁ a₂ : Type u) {n : } :
is_empty (first_order.sequence₂ a₀ a₁ a₂ (n + 3))
@[simp]
theorem first_order.sequence₂.lift_mk (a₀ a₁ a₂ : Type u) {i : } :
@[simp]
theorem first_order.sequence₂.sum_card (a₀ a₁ a₂ : Type u) :
@[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₂
@[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₂
@[protected]
def first_order.language.mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) :

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

Equations
Instances for first_order.language.mk₂
@[protected]

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

Equations
Instances for first_order.language.sum
@[protected, nolint]

The type of constants in a given language.

Equations
Instances for first_order.language.constants
@[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
@[nolint]

The type of symbols in a given language.

Equations
Instances for first_order.language.symbols

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

Equations
@[protected, instance]
@[protected, instance]
@[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₂] :
@[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₂] :
@[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 : } :
@[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 : } :
@[simp]
theorem first_order.language.card_mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) :

Maps #

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
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
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

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.

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
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
@[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
@[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} :
@[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) :
@[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) :
@[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) :
@[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) :
@[class]

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
@[class]

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
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
@[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
@[protected, instance]
Equations
@[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
@[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} :
@[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
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
@[simp]
@[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
@[refl]

The identity map from a structure to itself

Equations
@[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
@[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)
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.

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
@[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

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

Equations
@[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} :
@[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
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

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

Equations
@[refl]

The identity embedding from a structure to itself

Equations
@[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
@[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)
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.

@[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

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

Equations
@[protected, instance]
Equations
@[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
@[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
@[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
@[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

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

Equations
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
@[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} :
@[simp]
@[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
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
@[refl]

The identity equivalence from a structure to itself

Equations
@[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
@[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)
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.

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

Equations
def function.empty_hom {M : Type w} {N : Type w'} (f : M N) :

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

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

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

Equations
@[simp]
theorem embedding.empty_to_embedding {M : Type w} {N : Type w'} (f : M N) :
def equiv.empty {M : Type w} {N : Type w'} (f : M N) :

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

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

A structure induced by a bijection.

Equations
@[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) :
@[simp]
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