Basics on First-Order Structures #

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.

References #

For the Flypitch project:

Languages and Structures #

source

@[nolint]

structure first_order.language :

Type (max (u+1) (v+1))

functions : ℕ → Type ?
relations : ℕ → Type ?

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.

source

def first_order.language.empty :

first_order.language

The empty language has no symbols.

Equations

first_order.language.empty = {functions := λ (_x : ℕ), pempty, relations := λ (_x : ℕ), pempty}

source

@[protected, instance]

def first_order.language.inhabited :

inhabited first_order.language

Equations

first_order.language.inhabited = {default := first_order.language.empty}

source

@[nolint]

def first_order.language.const (L : first_order.language) :

Type u_1

The type of constants in a given language.

Equations

L.const = L.functions 0

source

@[class]

structure first_order.language.is_relational (L : first_order.language) :

Prop

empty_functions : ∀ (n : ℕ), L.functions n → false

A language is relational when it has no function symbols.

Instances

source

@[class]

structure first_order.language.is_algebraic (L : first_order.language) :

Prop

empty_relations : ∀ (n : ℕ), L.relations n → false

A language is algebraic when it has no relation symbols.

Instances

source

@[protected, instance]

def first_order.language.is_relational_of_empty_functions {symb : ℕ → Type u_1} :

{functions := λ (_x : ℕ), pempty, relations := symb}.is_relational

source

@[protected, instance]

def first_order.language.is_algebraic_of_empty_relations {symb : ℕ → Type u_1} :

{functions := symb, relations := λ (_x : ℕ), pempty}.is_algebraic

source

@[protected, instance]

def first_order.language.is_relational_empty :

first_order.language.empty.is_relational

source

@[protected, instance]

def first_order.language.is_algebraic_empty :

first_order.language.empty.is_algebraic

source

@[class]

structure first_order.language.Structure (L : first_order.language) (M : Type u_1) :

Type (max u u_1 v)

fun_map : Π {n : ℕ}, L.functions n → (fin n → M) → M
rel_map : Π {n : ℕ}, L.relations n → (fin n → M) → Prop

A first-order structure on a type M consists of interpretations of all the symbols in a given language. Each function of arity n is interpreted as a function sending tuples of length n (modeled as (fin n → M)) to M, and a relation of arity n is a function from tuples of length n to Prop.

Instances

Maps #

source

structure first_order.language.hom (L : first_order.language) (M : Type u_1) (N : Type u_2) [L.Structure M] [L.Structure N] :

Type (max u_1 u_2)

to_fun : M → N
map_fun' : (∀ {n : ℕ} (f : L.functions n) (x : fin n → M), self.to_fun (first_order.language.Structure.fun_map f x) = first_order.language.Structure.fun_map f (self.to_fun ∘ x)) . "obviously"
map_rel' : (∀ {n : ℕ} (r : L.relations n) (x : fin n → M), first_order.language.Structure.rel_map r x → first_order.language.Structure.rel_map r (self.to_fun ∘ x)) . "obviously"

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.

source

structure first_order.language.embedding (L : first_order.language) (M : Type u_1) (N : Type u_2) [L.Structure M] [L.Structure N] :

Type (max u_1 u_2)

to_embedding : M ↪ N
map_fun' : (∀ {n : ℕ} (f : L.functions n) (x : fin n → M), self.to_embedding.to_fun (first_order.language.Structure.fun_map f x) = first_order.language.Structure.fun_map f (self.to_embedding.to_fun ∘ x)) . "obviously"
map_rel' : (∀ {n : ℕ} (r : L.relations n) (x : fin n → M), first_order.language.Structure.rel_map r (self.to_embedding.to_fun ∘ x) ↔ first_order.language.Structure.rel_map r x) . "obviously"

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

source

structure first_order.language.equiv (L : first_order.language) (M : Type u_1) (N : Type u_2) [L.Structure M] [L.Structure N] :

Type (max u_1 u_2)

to_equiv : M ≃ N
map_fun' : (∀ {n : ℕ} (f : L.functions n) (x : fin n → M), self.to_equiv.to_fun (first_order.language.Structure.fun_map f x) = first_order.language.Structure.fun_map f (self.to_equiv.to_fun ∘ x)) . "obviously"
map_rel' : (∀ {n : ℕ} (r : L.relations n) (x : fin n → M), first_order.language.Structure.rel_map r (self.to_equiv.to_fun ∘ x) ↔ first_order.language.Structure.rel_map r x) . "obviously"

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

source

@[protected, instance]

def first_order.language.has_coe_t {L : first_order.language} {M : Type u_1} [L.Structure M] :

has_coe_t L.const M

Equations

first_order.language.has_coe_t = {coe := λ (c : L.const), first_order.language.Structure.fun_map c fin.elim0}

source

theorem first_order.language.fun_map_eq_coe_const {L : first_order.language} {M : Type u_1} [L.Structure M] {c : L.const} {x : fin 0 → M} :

first_order.language.Structure.fun_map c x = ↑c

source

@[protected, instance]

def first_order.language.hom.has_coe_to_fun {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :

has_coe_to_fun (L.hom M N) (λ (_x : L.hom M N), M → N)

Equations

first_order.language.hom.has_coe_to_fun = {coe := first_order.language.hom.to_fun _inst_2}

source

@[simp]

theorem first_order.language.hom.to_fun_eq_coe {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {f : L.hom M N} :

f.to_fun = ⇑f

source

theorem first_order.language.hom.coe_injective {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :

function.injective coe_fn

source

@[ext]

theorem first_order.language.hom.ext {L : first_order.language} {M : Type u_1} {N : Type u_2} [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 u_1} {N : Type u_2} [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 u_1} {N : Type u_2} [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_const {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.hom M N) (c : L.const) :

⇑φ ↑c = ↑c

source

@[simp]

theorem first_order.language.hom.map_rel {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.hom M N) {n : ℕ} (r : L.relations n) (x : fin n → M) :

first_order.language.Structure.rel_map r x → first_order.language.Structure.rel_map r (⇑φ ∘ x)

source

def first_order.language.hom.id (L : first_order.language) (M : Type u_1) [L.Structure M] :

L.hom M M

The identity map from a structure to itself

Equations

first_order.language.hom.id L M = {to_fun := id M, map_fun' := _, map_rel' := _}

source

@[protected, instance]

def first_order.language.hom.inhabited {L : first_order.language} {M : Type u_1} [L.Structure M] :

inhabited (L.hom M M)

Equations

first_order.language.hom.inhabited = {default := first_order.language.hom.id L M _inst_1}

source

@[simp]

theorem first_order.language.hom.id_apply {L : first_order.language} {M : Type u_1} [L.Structure M] (x : M) :

⇑(first_order.language.hom.id L M) x = x

source

def first_order.language.hom.comp {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {P : Type u_3} [L.Structure P] (hnp : L.hom N P) (hmn : L.hom M N) :

L.hom M P

Composition of first-order homomorphisms

Equations

hnp.comp hmn = {to_fun := ⇑hnp ∘ ⇑hmn, map_fun' := _, map_rel' := _}

source

@[simp]

theorem first_order.language.hom.comp_apply {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {P : Type u_3} [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 u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {P : Type u_3} [L.Structure P] {Q : Type u_4} [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

@[protected, instance]

def first_order.language.embedding.has_coe_to_fun {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :

has_coe_to_fun (L.embedding M N) (λ (_x : L.embedding M N), M → N)

Equations

first_order.language.embedding.has_coe_to_fun = {coe := λ (f : L.embedding M N), f.to_embedding.to_fun}

source

@[simp]

theorem first_order.language.embedding.map_fun {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.embedding 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.embedding.map_const {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.embedding M N) (c : L.const) :

⇑φ ↑c = ↑c

source

@[simp]

theorem first_order.language.embedding.map_rel {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.embedding M N) {n : ℕ} (r : L.relations n) (x : fin n → M) :

first_order.language.Structure.rel_map r (⇑φ ∘ x) ↔ first_order.language.Structure.rel_map r x

source

def first_order.language.embedding.to_hom {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.embedding M N) :

L.hom M N

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

Equations

f.to_hom = {to_fun := ⇑f, map_fun' := _, map_rel' := _}

source

@[simp]

theorem first_order.language.embedding.coe_to_hom {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {f : L.embedding M N} :

⇑(f.to_hom) = ⇑f

source

theorem first_order.language.embedding.coe_injective {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :

function.injective coe_fn

source

@[ext]

theorem first_order.language.embedding.ext {L : first_order.language} {M : Type u_1} {N : Type u_2} [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 u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {f g : L.embedding M N} :

f = g ↔ ∀ (x : M), ⇑f x = ⇑g x

source

theorem first_order.language.embedding.injective {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.embedding M N) :

function.injective ⇑f

source

def first_order.language.embedding.of_injective {L : first_order.language} {M : Type u_1} {N : Type u_2} [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

first_order.language.embedding.of_injective hf = {to_embedding := {to_fun := f.to_fun, inj' := hf}, map_fun' := _, map_rel' := _}

source

@[simp]

theorem first_order.language.embedding.of_injective_to_embedding_apply {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] [L.is_algebraic] {f : L.hom M N} (hf : function.injective ⇑f) (ᾰ : M) :

⇑((first_order.language.embedding.of_injective hf).to_embedding) ᾰ = f.to_fun ᾰ

source

@[simp]

theorem first_order.language.embedding.coe_fn_of_injective {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] [L.is_algebraic] {f : L.hom M N} (hf : function.injective ⇑f) :

⇑(first_order.language.embedding.of_injective hf) = ⇑f

source

@[simp]

theorem first_order.language.embedding.of_injective_to_hom {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] [L.is_algebraic] {f : L.hom M N} (hf : function.injective ⇑f) :

(first_order.language.embedding.of_injective hf).to_hom = f

source

def first_order.language.embedding.refl (L : first_order.language) (M : Type u_1) [L.Structure M] :

L.embedding M M

The identity embedding from a structure to itself

Equations

first_order.language.embedding.refl L M = {to_embedding := function.embedding.refl M, map_fun' := _, map_rel' := _}

source

@[protected, instance]

def first_order.language.embedding.inhabited {L : first_order.language} {M : Type u_1} [L.Structure M] :

inhabited (L.embedding M M)

Equations

first_order.language.embedding.inhabited = {default := first_order.language.embedding.refl L M _inst_1}

source

@[simp]

theorem first_order.language.embedding.refl_apply {L : first_order.language} {M : Type u_1} [L.Structure M] (x : M) :

⇑(first_order.language.embedding.refl L M) x = x

source

def first_order.language.embedding.comp {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {P : Type u_3} [L.Structure P] (hnp : L.embedding N P) (hmn : L.embedding M N) :

L.embedding M P

Composition of first-order embeddings

Equations

hnp.comp hmn = {to_embedding := {to_fun := ⇑hnp ∘ ⇑hmn, inj' := _}, map_fun' := _, map_rel' := _}

source

@[simp]

theorem first_order.language.embedding.comp_apply {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {P : Type u_3} [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 u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {P : Type u_3} [L.Structure P] {Q : Type u_4} [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 u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {P : Type u_3} [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.equiv.symm {L : first_order.language} {M : Type u_1} {N : Type u_2} [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

f.symm = {to_equiv := {to_fun := f.to_equiv.symm.to_fun, inv_fun := f.to_equiv.symm.inv_fun, left_inv := _, right_inv := _}, map_fun' := _, map_rel' := _}

source

@[protected, instance]

def first_order.language.equiv.has_coe_to_fun {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :

has_coe_to_fun (L.equiv M N) (λ (_x : L.equiv M N), M → N)

Equations

first_order.language.equiv.has_coe_to_fun = {coe := λ (f : L.equiv M N), f.to_equiv.to_fun}

source

@[simp]

theorem first_order.language.equiv.apply_symm_apply {L : first_order.language} {M : Type u_1} {N : Type u_2} [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 u_1} {N : Type u_2} [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_fun {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.equiv 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.equiv.map_const {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.equiv M N) (c : L.const) :

⇑φ ↑c = ↑c

source

@[simp]

theorem first_order.language.equiv.map_rel {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.equiv M N) {n : ℕ} (r : L.relations n) (x : fin n → M) :

first_order.language.Structure.rel_map r (⇑φ ∘ x) ↔ first_order.language.Structure.rel_map r x

source

def first_order.language.equiv.to_embedding {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.equiv M N) :

L.embedding M N

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

Equations

f.to_embedding = {to_embedding := {to_fun := ⇑f, inj' := _}, map_fun' := _, map_rel' := _}

source

def first_order.language.equiv.to_hom {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.equiv M N) :

L.hom M N

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

Equations

f.to_hom = {to_fun := ⇑f, map_fun' := _, map_rel' := _}

source

@[simp]

theorem first_order.language.equiv.to_embedding_to_hom {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.equiv M N) :

f.to_embedding.to_hom = f.to_hom

source

@[simp]

theorem first_order.language.equiv.coe_to_hom {L : first_order.language} {M : Type u_1} {N : Type u_2} [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 u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.equiv M N) :

⇑(f.to_embedding) = ⇑f

source

theorem first_order.language.equiv.coe_injective {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :

function.injective coe_fn

source

@[ext]

theorem first_order.language.equiv.ext {L : first_order.language} {M : Type u_1} {N : Type u_2} [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 u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {f g : L.equiv M N} :

f = g ↔ ∀ (x : M), ⇑f x = ⇑g x

source

theorem first_order.language.equiv.injective {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.equiv M N) :

function.injective ⇑f

source

def first_order.language.equiv.refl (L : first_order.language) (M : Type u_1) [L.Structure M] :

L.equiv M M

The identity equivalence from a structure to itself

Equations

first_order.language.equiv.refl L M = {to_equiv := equiv.refl M, map_fun' := _, map_rel' := _}

source

@[protected, instance]

def first_order.language.equiv.inhabited {L : first_order.language} {M : Type u_1} [L.Structure M] :

inhabited (L.equiv M M)

Equations

first_order.language.equiv.inhabited = {default := first_order.language.equiv.refl L M _inst_1}

source

@[simp]

theorem first_order.language.equiv.refl_apply {L : first_order.language} {M : Type u_1} [L.Structure M] (x : M) :

⇑(first_order.language.equiv.refl L M) x = x

source

def first_order.language.equiv.comp {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {P : Type u_3} [L.Structure P] (hnp : L.equiv N P) (hmn : L.equiv M N) :

L.equiv M P

Composition of first-order equivalences

Equations

hnp.comp hmn = {to_equiv := {to_fun := ⇑hnp ∘ ⇑hmn, inv_fun := (hmn.to_equiv.trans hnp.to_equiv).inv_fun, left_inv := _, right_inv := _}, map_fun' := _, map_rel' := _}

source

@[simp]

theorem first_order.language.equiv.comp_apply {L : first_order.language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {P : Type u_3} [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 u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {P : Type u_3} [L.Structure P] {Q : Type u_4} [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.