# mathlib3documentation

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 #

@[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
• a₂ _x = pempty
• a₂ 2 = a₂
• a₂ 1 = a₁
• a₂ 0 = a₀
Instances for `first_order.sequence₂`
@[protected, instance]
def first_order.sequence₂.inhabited₀ (a₀ a₁ a₂ : Type u) [h : inhabited a₀] :
inhabited a₁ a₂ 0)
Equations
• a₂ = h
@[protected, instance]
def first_order.sequence₂.inhabited₁ (a₀ a₁ a₂ : Type u) [h : inhabited a₁] :
inhabited a₁ a₂ 1)
Equations
• a₂ = h
@[protected, instance]
def first_order.sequence₂.inhabited₂ (a₀ a₁ a₂ : Type u) [h : inhabited a₂] :
inhabited a₁ a₂ 2)
Equations
• a₂ = h
@[protected, instance]
def first_order.sequence₂.is_empty (a₀ a₁ a₂ : Type u) {n : } :
is_empty a₁ a₂ (n + 3))
@[simp]
theorem first_order.sequence₂.lift_mk (a₀ a₁ a₂ : Type u) {i : } :
(cardinal.mk a₁ a₂ i)).lift = cardinal.mk (ulift a₁) (ulift a₂) i)
@[simp]
theorem first_order.sequence₂.sum_card (a₀ a₁ a₂ : Type u) :
cardinal.sum (λ (i : ), cardinal.mk a₁ a₂ i)) = + +
@[simp]
theorem first_order.language.mk₂_relations (c f₁ f₂ : Type u) (r₁ r₂ : Type v) (ᾰ : ) :
f₂ r₁ r₂).relations =
@[simp]
theorem first_order.language.mk₂_functions (c f₁ f₂ : Type u) (r₁ r₂ : Type v) (ᾰ : ) :
f₂ r₁ r₂).functions = 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 empty language has no symbols.

Equations
Instances for `first_order.language.empty`
@[protected, instance]
Equations
@[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) :
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
@[class]

A language is relational when it has no function symbols.

Instances of this typeclass
@[class]

A language is algebraic when it has no relation symbols.

Instances of this typeclass
@[protected, instance]
@[protected, instance]
@[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₂] :
f₂ r₁ r₂).is_relational
@[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₂] :
f₂ r₁ r₂).is_algebraic
@[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 f₁ f₂ r₁ r₂).functions 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 : } :
subsingleton f₁ f₂ r₁ r₂).relations n)
@[simp]
@[protected, instance]
@[simp]
theorem first_order.language.card_mk₂ (c f₁ f₂ : Type u) (r₁ r₂ : Type v) :
f₂ r₁ r₂).card = (cardinal.mk c).lift + (cardinal.mk f₁).lift + (cardinal.mk f₂).lift + (cardinal.mk r₁).lift + (cardinal.mk r₂).lift
@[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`

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

Equations

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

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 : } :
f₂ r₁ r₂).functions n (fin n M) M

The function map for `first_order.language.Structure₂`.

Equations
• f₂' f _x =
• f₂' f x = f₂' f (x 0) (x 1)
• f₂' f x = f₁' f (x 0)
• f₂' f _x = c' f
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 : } :
f₂ r₁ r₂).relations n (fin n M) Prop

The relation map for `first_order.language.Structure₂`.

Equations
• r _x =
• r x = r₂' r (x 0) (x 1)
• r x = (x 0 r₁' r)
• r _x =
@[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) :
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} :
= c' c₀
@[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) :
= f₁' f x
@[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) :
= f₂' f x y
@[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) :
= (x r₁' r)
@[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) :
= r₂' r x y
@[class]
structure first_order.language.hom_class (F : Type u_5) (M : out_param (Type u_6)) (N : out_param (Type u_7)) [ M (λ (_x : M), N)]  :

`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]
structure first_order.language.strong_hom_class (F : Type u_5) (M : out_param (Type u_6)) (N : out_param (Type u_7)) [ M (λ (_x : M), N)]  :

`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
@[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] [ M (λ (_x : M), N)]  :
Equations
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] [ M (λ (_x : M), N)] [ N] :

Not an instance to avoid a loop.

Equations
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] [ M (λ (_x : M), N)] [ 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]
def first_order.language.hom.hom_class {L : first_order.language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
(L.hom M N) 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]
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) :
@[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
@[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) :
@[refl]

The identity map from a structure to itself

Equations
@[protected, instance]
Equations
@[simp]
theorem first_order.language.hom.id_apply {L : first_order.language} {M : Type w} [L.Structure M] (x : M) :
x = x
@[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] [ M (λ (_x : M), N)] [ N] :
F L.hom M N

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

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

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

The identity embedding from a structure to itself

Equations
@[protected, instance]
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
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] [ N]  :
F L.embedding M N

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

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

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.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) :
@[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
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) :
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) :
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) :
@[refl]

The identity equivalence from a structure to itself

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

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] [ M N]  :
F L.equiv M N

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

Equations
@[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
@[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) :
@[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) :
@[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) :
@[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) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def first_order.language.strong_hom_class_empty {F : Type u_1} {M : out_param (Type u_2)} {N : Type u_3} [ M (λ (_x : M), N)] :
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) :
= 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) :
@[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) :
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_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) :
@[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.to_fun
@[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.inv_fun
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