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 #

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.empty  :
first_order.language

The empty language has no symbols.

Equations
Instances for first_order.language.empty
source
@[protected, instance]
def first_order.language.inhabited  :
inhabited first_order.language
Equations
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
@[class]
structure first_order.language.is_relational (L : first_order.language) :
Prop

A language is relational when it has no function symbols.

Instances of this typeclass
source
@[class]
structure first_order.language.is_algebraic (L : first_order.language) :
Prop

A language is algebraic when it has no relation symbols.

Instances of this typeclass
source
theorem first_order.language.card_eq_card_functions_add_card_relations {L : first_order.language} :
L.card = cardinal.sum (λ (l : ℕ), (cardinal.mk (L.functions l)).lift) + cardinal.sum (λ (l : ℕ), (cardinal.mk (L.relations l)).lift)
source
@[protected, instance]
def first_order.language.functions.is_empty {L : first_order.language} [L.is_relational] {n : ℕ} :
is_empty (L.functions n)
source
@[protected, instance]
def first_order.language.relations.is_empty {L : first_order.language} [L.is_algebraic] {n : ℕ} :
is_empty (L.relations n)
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_empty  :
first_order.language.empty.is_relational
source
@[protected, instance]
def first_order.language.is_algebraic_empty  :
first_order.language.empty.is_algebraic
source
@[protected, instance]
def first_order.language.is_relational_sum {L : first_order.language} {L' : first_order.language} [L.is_relational] [L'.is_relational] :
(L.sum L').is_relational
source
@[protected, instance]
def first_order.language.is_algebraic_sum {L : first_order.language} {L' : first_order.language} [L.is_algebraic] [L'.is_algebraic] :
(L.sum L').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.empty_card  :
first_order.language.empty.card = 0
source
@[protected, instance]
def first_order.language.is_empty_empty  :
is_empty first_order.language.empty.symbols
source
@[protected, instance]
def first_order.language.countable.countable_functions {L : first_order.language} [h : countable L.symbols] :
countable (Σ (l : ℕ), L.functions l)
source
@[simp]
theorem first_order.language.card_functions_sum {L : first_order.language} {L' : first_order.language} (i : ℕ) :
cardinal.mk ((L.sum L').functions i) = (cardinal.mk (L.functions i)).lift + (cardinal.mk (L'.functions i)).lift
source
@[simp]
theorem first_order.language.card_relations_sum {L : first_order.language} {L' : first_order.language} (i : ℕ) :
cardinal.mk ((L.sum L').relations i) = (cardinal.mk (L.relations i)).lift + (cardinal.mk (L'.relations i)).lift
source
@[simp]
theorem first_order.language.card_sum {L : first_order.language} {L' : first_order.language} :
(L.sum L').card = L.card.lift + L'.card.lift
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
source
@[ext, class]
structure first_order.language.Structure (L : first_order.language) (M : Type w) :
Type (max u v w)

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 of this typeclass
Instances of other typeclasses for first_order.language.Structure
source
theorem first_order.language.Structure.ext_iff {L : first_order.language} {M : Type w} (x y : L.Structure M) :
x = y ↔ first_order.language.Structure.fun_map = first_order.language.Structure.fun_map ∧ first_order.language.Structure.rel_map = first_order.language.Structure.rel_map
source
theorem first_order.language.Structure.ext {L : first_order.language} {M : Type w} (x y : L.Structure M) (h : first_order.language.Structure.fun_map = first_order.language.Structure.fun_map) (h_1 : first_order.language.Structure.rel_map = first_order.language.Structure.rel_map) :
x = y
source
def first_order.language.inhabited.trivial_structure (L : first_order.language) {α : Type u_1} [inhabited α] :
L.Structure α

Used for defining first_order.language.Theory.Model.inhabited.

Equations

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
@[protected, instance]
def first_order.language.has_coe_t {L : first_order.language} {M : Type w} [L.Structure M] :
has_coe_t L.constants M
Equations
source
theorem first_order.language.fun_map_eq_coe_constants {L : first_order.language} {M : Type w} [L.Structure M] {c : L.constants} {x : fin 0 → M} :
first_order.language.Structure.fun_map c x = ↑c
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
@[protected, instance]
def first_order.language.strong_hom_class.hom_class {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.strong_hom_class L F M N] :
first_order.language.hom_class L F M N
Equations
source
def first_order.language.hom_class.strong_hom_class_of_is_algebraic {L : first_order.language} [L.is_algebraic] {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] :
first_order.language.strong_hom_class L F M N

Not an instance to avoid a loop.

Equations
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.first_order.language.strong_hom_class {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.is_algebraic] :
first_order.language.strong_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
@[simp]
theorem first_order.language.hom.map_rel {L : first_order.language} {M : Type w} {N : Type w'} [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
@[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
@[protected, instance]
def first_order.language.hom.inhabited {L : first_order.language} {M : Type w} [L.Structure M] :
inhabited (L.hom M M)
Equations
source
@[simp]
theorem first_order.language.hom.id_apply {L : first_order.language} {M : Type w} [L.Structure M] (x : M) :
⇑(first_order.language.hom.id L M) x = x
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
@[protected, instance]
def first_order.language.embedding.embedding_like {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
embedding_like (L.embedding M N) M N
Equations
source
@[protected, instance]
def first_order.language.embedding.strong_hom_class {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
first_order.language.strong_hom_class L (L.embedding M N) M N
Equations
source
@[protected, instance]
def first_order.language.embedding.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.embedding M N) (λ (_x : L.embedding M N), M → N)
Equations
source
@[simp]
theorem first_order.language.embedding.map_fun {L : first_order.language} {M : Type w} {N : Type w'} [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_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
@[simp]
theorem first_order.language.embedding.map_rel {L : first_order.language} {M : Type w} {N : Type w'} [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 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
theorem first_order.language.embedding.coe_injective {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
function.injective coe_fn
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
theorem first_order.language.embedding.injective {L : first_order.language} {M : Type w} {N : Type w'} [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 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
@[simp]
theorem first_order.language.embedding.of_injective_to_embedding_apply {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) (ᾰ : 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 w} {N : Type w'} [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 w} {N : Type w'} [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
@[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
@[protected, instance]
def first_order.language.embedding.inhabited {L : first_order.language} {M : Type w} [L.Structure M] :
inhabited (L.embedding M M)
Equations
source
@[simp]
theorem first_order.language.embedding.refl_apply {L : first_order.language} {M : Type w} [L.Structure M] (x : M) :
⇑(first_order.language.embedding.refl L M) x = x
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
@[protected, instance]
def first_order.language.equiv.first_order.language.strong_hom_class {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
first_order.language.strong_hom_class L (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
@[protected, instance]
def first_order.language.equiv.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.equiv M N) (λ (_x : L.equiv M N), M → N)
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_fun {L : first_order.language} {M : Type w} {N : Type w'} [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_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
@[simp]
theorem first_order.language.equiv.map_rel {L : first_order.language} {M : Type w} {N : Type w'} [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 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.to_embedding_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_embedding.to_hom = f.to_hom
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
theorem first_order.language.equiv.coe_injective {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
function.injective coe_fn
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
theorem first_order.language.equiv.bijective {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
function.bijective ⇑f
source
theorem first_order.language.equiv.injective {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
function.injective ⇑f
source
theorem first_order.language.equiv.surjective {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
function.surjective ⇑f
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
@[protected, instance]
def first_order.language.equiv.inhabited {L : first_order.language} {M : Type w} [L.Structure M] :
inhabited (L.equiv M M)
Equations
source
@[simp]
theorem first_order.language.equiv.refl_apply {L : first_order.language} {M : Type w} [L.Structure M] (x : M) :
⇑(first_order.language.equiv.refl L M) x = x
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
@[protected, instance]
def first_order.language.sum_Structure (L₁ : first_order.language) (L₂ : first_order.language) (S : Type u_7) [L₁.Structure S] [L₂.Structure S] :
(L₁.sum L₂).Structure S
Equations
source
@[simp]
theorem first_order.language.fun_map_sum_inl {L₁ : first_order.language} {L₂ : first_order.language} {S : Type u_7} [L₁.Structure S] [L₂.Structure S] {n : ℕ} (f : L₁.functions n) :
first_order.language.Structure.fun_map (sum.inl f) = first_order.language.Structure.fun_map f
source
@[simp]
theorem first_order.language.fun_map_sum_inr {L₁ : first_order.language} {L₂ : first_order.language} {S : Type u_7} [L₁.Structure S] [L₂.Structure S] {n : ℕ} (f : L₂.functions n) :
first_order.language.Structure.fun_map (sum.inr f) = first_order.language.Structure.fun_map f
source
@[simp]
theorem first_order.language.rel_map_sum_inl {L₁ : first_order.language} {L₂ : first_order.language} {S : Type u_7} [L₁.Structure S] [L₂.Structure S] {n : ℕ} (R : L₁.relations n) :
first_order.language.Structure.rel_map (sum.inl R) = first_order.language.Structure.rel_map R
source
@[simp]
theorem first_order.language.rel_map_sum_inr {L₁ : first_order.language} {L₂ : first_order.language} {S : Type u_7} [L₁.Structure S] [L₂.Structure S] {n : ℕ} (R : L₂.relations n) :
first_order.language.Structure.rel_map (sum.inr R) = first_order.language.Structure.rel_map R
source
@[simp]
theorem first_order.language.empty.nonempty_embedding_iff {M : Type w} {N : Type w'} [first_order.language.empty.Structure M] [first_order.language.empty.Structure N] :
nonempty (first_order.language.empty.embedding M N) ↔ (cardinal.mk M).lift ≤ (cardinal.mk N).lift
source
@[simp]
theorem first_order.language.empty.nonempty_equiv_iff {M : Type w} {N : Type w'} [first_order.language.empty.Structure M] [first_order.language.empty.Structure N] :
nonempty (first_order.language.empty.equiv M N) ↔ (cardinal.mk M).lift = (cardinal.mk N).lift
source
@[protected, instance]
def first_order.language.empty_Structure {M : Type w} :
first_order.language.empty.Structure M
Equations
source
@[protected, instance]
def first_order.language.Structure.unique {M : Type w} :
unique (first_order.language.empty.Structure M)
Equations
source
@[protected, instance]
def first_order.language.strong_hom_class_empty {F : Type u_1} {M : out_param (Type u_2)} {N : Type u_3} [fun_like F M (λ (_x : M), N)] :
first_order.language.strong_hom_class first_order.language.empty F M N
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
@[simp]
theorem equiv.induced_Structure_rel_map {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] (e : M ≃ N) (n : ℕ) (r : L.relations n) (x : fin n → N) :
first_order.language.Structure.rel_map r x = first_order.language.Structure.rel_map r (⇑(e.symm) ∘ x)
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_fun_map {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] (e : M ≃ N) (n : ℕ) (f : L.functions n) (x : fin n → N) :
first_order.language.Structure.fun_map f x = ⇑e (first_order.language.Structure.fun_map f (⇑(e.symm) ∘ x))
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