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 FirstOrder.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 FirstOrder.Language.Structure interprets the symbols of a given FirstOrder.Language in the context of a given type.
• A FirstOrder.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 FirstOrder.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 FirstOrder.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:

• [J. Han, F. van Doorn, A formal proof of the independence of the continuum hypothesis] [flypitch_cpp]
• [J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis][flypitch_itp]

Languages and Structures

structure FirstOrder.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.

• Functions : ℕ → Type u

  For every arity, a Type u of functions of that arity

• Relations : ℕ → Type v

  For every arity, a Type v of relations of that arity

@[reducible, inline]

abbrev FirstOrder.Language.IsRelational (L : Language) : Prop

A language is relational when it has no function symbols.

@[reducible, inline]

abbrev FirstOrder.Language.IsAlgebraic (L : Language) : Prop

A language is algebraic when it has no relation symbols.

def FirstOrder.Language.empty : Language

The empty language has no symbols.

@[implicit_reducible]

instance FirstOrder.Language.instIsAlgebraicEmpty : Language.empty.IsAlgebraic

@[implicit_reducible]

instance FirstOrder.Language.instIsRelationalEmpty : Language.empty.IsRelational

@[implicit_reducible]

instance FirstOrder.Language.instInhabited : Inhabited Language

def FirstOrder.Language.sum (L : Language) (L' : Language) : Language

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

@[reducible, inline]

abbrev FirstOrder.Language.Constants (L : Language) : Type u

The type of constants in a given language.

@[reducible, inline]

abbrev FirstOrder.Language.Symbols (L : Language) : Type (max u v)

The type of symbols in a given language.

def FirstOrder.Language.card (L : Language) : Cardinal.{max u v}

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

theorem FirstOrder.Language.card_eq_card_functions_add_card_relations {L : Language} : L.card = (Cardinal.sum fun (l : ℕ) => Cardinal.lift.{v, u} (Cardinal.mk (L.Functions l))) + Cardinal.sum fun (l : ℕ) => Cardinal.lift.{u, v} (Cardinal.mk (L.Relations l))

instance FirstOrder.Language.isRelational_sum {L : Language} {L' : Language} [L.IsRelational] [L'.IsRelational] : (L.sum L').IsRelational

instance FirstOrder.Language.isAlgebraic_sum {L : Language} {L' : Language} [L.IsAlgebraic] [L'.IsAlgebraic] : (L.sum L').IsAlgebraic

@[simp]

theorem FirstOrder.Language.card_empty : Language.empty.card = 0

instance FirstOrder.Language.isEmpty_empty : IsEmpty Language.empty.Symbols

instance FirstOrder.Language.Countable.countable_functions {L : Language} [h : Countable L.Symbols] : Countable ((l : ℕ) × L.Functions l)

@[simp]

theorem FirstOrder.Language.card_functions_sum {L : Language} {L' : Language} (i : ℕ) : Cardinal.mk ((L.sum L').Functions i) = Cardinal.lift.{u', u} (Cardinal.mk (L.Functions i)) + Cardinal.lift.{u, u'} (Cardinal.mk (L'.Functions i))

@[simp]

theorem FirstOrder.Language.card_relations_sum {L : Language} {L' : Language} (i : ℕ) : Cardinal.mk ((L.sum L').Relations i) = Cardinal.lift.{v', v} (Cardinal.mk (L.Relations i)) + Cardinal.lift.{v, v'} (Cardinal.mk (L'.Relations i))

theorem FirstOrder.Language.card_sum {L : Language} {L' : Language} : (L.sum L').card = Cardinal.lift.{max u' v', max u v} L.card + Cardinal.lift.{max u v, max u' v'} L'.card

@[implicit_reducible]

instance FirstOrder.Language.instDecidableEqFunctions {f : ℕ → Type u_1} {R : ℕ → Type u_2} (n : ℕ) [DecidableEq (f n)] : DecidableEq ({ Functions := f, Relations := R }.Functions n)

Passes a DecidableEq instance on a type of function symbols through the Language constructor. Despite the fact that this is proven by inferInstance, it is still needed - see the examples in ModelTheory/Ring/Basic.

@[implicit_reducible]

instance FirstOrder.Language.instDecidableEqRelations {f : ℕ → Type u_1} {R : ℕ → Type u_2} (n : ℕ) [DecidableEq (R n)] : DecidableEq ({ Functions := f, Relations := R }.Relations n)

Passes a DecidableEq instance on a type of relation symbols through the Language constructor. Despite the fact that this is proven by inferInstance, it is still needed - see the examples in ModelTheory/Ring/Basic.

class FirstOrder.Language.Structure (L : Language) (M : Type w) : Type (max (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.

• funMap {n : ℕ} : L.Functions n → (Fin n → M) → M

  Interpretation of the function symbols

• RelMap {n : ℕ} : L.Relations n → (Fin n → M) → Prop

  Interpretation of the relation symbols

theorem FirstOrder.Language.Structure.ext {L : Language} {M : Type w} {x y : L.Structure M} (funMap : @funMap L M x = @funMap L M y) (RelMap : @RelMap L M x = @RelMap L M y) : x = y

theorem FirstOrder.Language.Structure.ext_iff {L : Language} {M : Type w} {x y : L.Structure M} : x = y ↔ @funMap L M x = @funMap L M y ∧ @RelMap L M x = @RelMap L M y

@[implicit_reducible]

def FirstOrder.Language.Inhabited.trivialStructure (L : Language) {α : Type u_1} [Inhabited α] : L.Structure α

Used for defining FirstOrder.Language.Theory.ModelType.instInhabited.

Maps

structure FirstOrder.Language.Hom (L : 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.

• toFun : M → N

  The underlying function of a homomorphism of structures

• map_fun' {n : ℕ} (f : L.Functions n) (x : Fin n → M) : self.toFun (Structure.funMap f x) = Structure.funMap f (self.toFun ∘ x)

  The homomorphism commutes with the interpretations of the function symbols

• map_rel' {n : ℕ} (r : L.Relations n) (x : Fin n → M) : Structure.RelMap r x → Structure.RelMap r (self.toFun ∘ x)

  The homomorphism sends related elements to related elements

def FirstOrder.«term_→[_]_» : Lean.TrailingParserDescr

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.

structure FirstOrder.Language.Embedding (L : Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] extends M ↪ N : Type (max w w')

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

• toFun : M → N
• inj' : Injective self.toFun
• map_fun' {n : ℕ} (f : L.Functions n) (x : Fin n → M) : self.toFun (Structure.funMap f x) = Structure.funMap f (self.toFun ∘ x)

  The homomorphism commutes with the interpretations of the function symbols

• map_rel' {n : ℕ} (r : L.Relations n) (x : Fin n → M) : Structure.RelMap r (self.toFun ∘ x) ↔ Structure.RelMap r x

  The homomorphism sends related elements to related elements

def FirstOrder.«term_↪[_]_» : Lean.TrailingParserDescr

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

structure FirstOrder.Language.Equiv (L : Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] extends M ≃ N : Type (max w w')

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

• toFun : M → N
• invFun : N → M
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_fun' {n : ℕ} (f : L.Functions n) (x : Fin n → M) : self.toFun (Structure.funMap f x) = Structure.funMap f (self.toFun ∘ x)

  The homomorphism commutes with the interpretations of the function symbols

• map_rel' {n : ℕ} (r : L.Relations n) (x : Fin n → M) : Structure.RelMap r (self.toFun ∘ x) ↔ Structure.RelMap r x

  The homomorphism sends related elements to related elements

def FirstOrder.«term_≃[_]_» : Lean.TrailingParserDescr

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

def FirstOrder.Language.constantMap {L : Language} {M : Type w} [L.Structure M] (c : L.Constants) : M

Interpretation of a constant symbol

@[implicit_reducible]

instance FirstOrder.Language.instCoeTCConstants {L : Language} {M : Type w} [L.Structure M] : CoeTC L.Constants M

theorem FirstOrder.Language.funMap_eq_coe_constants {L : Language} {M : Type w} [L.Structure M] {c : L.Constants} {x : Fin 0 → M} : Structure.funMap c x = ↑c

theorem FirstOrder.Language.nonempty_of_nonempty_constants {L : 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.

class FirstOrder.Language.HomClass (L : outParam Language) (F : Type u_3) (M : outParam (Type u_4)) (N : outParam (Type u_5)) [FunLike F M N] [L.Structure M] [L.Structure N] : Prop

HomClass L F M N states that F is a type of L-homomorphisms. You should extend this typeclass when you extend FirstOrder.Language.Hom.

• map_fun (φ : F) {n : ℕ} (f : L.Functions n) (x : Fin n → M) : φ (Structure.funMap f x) = Structure.funMap f (⇑φ ∘ x)

  The homomorphism commutes with the interpretations of the function symbols

• map_rel (φ : F) {n : ℕ} (r : L.Relations n) (x : Fin n → M) : Structure.RelMap r x → Structure.RelMap r (⇑φ ∘ x)

  The homomorphism sends related elements to related elements

class FirstOrder.Language.StrongHomClass (L : outParam Language) (F : Type u_3) (M : outParam (Type u_4)) (N : outParam (Type u_5)) [FunLike F M N] [L.Structure M] [L.Structure N] : Prop

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

• map_fun (φ : F) {n : ℕ} (f : L.Functions n) (x : Fin n → M) : φ (Structure.funMap f x) = Structure.funMap f (⇑φ ∘ x)

  The homomorphism commutes with the interpretations of the function symbols

• map_rel (φ : F) {n : ℕ} (r : L.Relations n) (x : Fin n → M) : Structure.RelMap r (⇑φ ∘ x) ↔ Structure.RelMap r x

  The homomorphism sends related elements to related elements

@[instance 100]

instance FirstOrder.Language.StrongHomClass.homClass {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {F : Type u_3} [FunLike F M N] [L.StrongHomClass F M N] : L.HomClass F M N

theorem FirstOrder.Language.HomClass.strongHomClassOfIsAlgebraic {L : Language} [L.IsAlgebraic] {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [FunLike F M N] [L.HomClass F M N] : L.StrongHomClass F M N

Not an instance to avoid a loop.

theorem FirstOrder.Language.HomClass.map_constants {L : Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [FunLike F M N] [L.HomClass F M N] (φ : F) (c : L.Constants) : φ ↑c = ↑c

@[implicit_reducible]

instance FirstOrder.Language.Hom.instFunLike {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : FunLike (L.Hom M N) M N

instance FirstOrder.Language.Hom.homClass {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : L.HomClass (L.Hom M N) M N

instance FirstOrder.Language.Hom.instStrongHomClassOfIsAlgebraic {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsAlgebraic] : L.StrongHomClass (L.Hom M N) M N

@[simp]

theorem FirstOrder.Language.Hom.toFun_eq_coe {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.Hom M N} : f.toFun = ⇑f

theorem FirstOrder.Language.Hom.ext {L : 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 FirstOrder.Language.Hom.ext_iff {L : 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 FirstOrder.Language.Hom.map_fun {L : 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) : φ (Structure.funMap f x) = Structure.funMap f (⇑φ ∘ x)

@[simp]

theorem FirstOrder.Language.Hom.map_constants {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Hom M N) (c : L.Constants) : φ ↑c = ↑c

@[simp]

theorem FirstOrder.Language.Hom.map_rel {L : 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) : Structure.RelMap r x → Structure.RelMap r (⇑φ ∘ x)

def FirstOrder.Language.Hom.id (L : Language) (M : Type w) [L.Structure M] : L.Hom M M

The identity map from a structure to itself.

@[implicit_reducible]

instance FirstOrder.Language.Hom.instInhabited {L : Language} {M : Type w} [L.Structure M] : Inhabited (L.Hom M M)

@[simp]

theorem FirstOrder.Language.Hom.id_apply {L : Language} {M : Type w} [L.Structure M] (x : M) : (id L M) x = x

def FirstOrder.Language.Hom.comp {L : 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.

@[simp]

theorem FirstOrder.Language.Hom.comp_apply {L : 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 FirstOrder.Language.Hom.comp_assoc {L : 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.

@[simp]

theorem FirstOrder.Language.Hom.comp_id {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Hom M N) : f.comp (id L M) = f

@[simp]

theorem FirstOrder.Language.Hom.id_comp {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Hom M N) : (id L N).comp f = f

def FirstOrder.Language.HomClass.toHom {L : Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [FunLike F M N] [L.HomClass F M N] : F → L.Hom M N

Any element of a HomClass can be realized as a first order homomorphism.

@[simp]

theorem FirstOrder.Language.HomClass.toHom_toFun {L : Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [FunLike F M N] [L.HomClass F M N] (a✝ : F) (a : M) : (toHom a✝) a = a✝ a

@[implicit_reducible]

instance FirstOrder.Language.Embedding.funLike {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : FunLike (L.Embedding M N) M N

instance FirstOrder.Language.Embedding.embeddingLike {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : EmbeddingLike (L.Embedding M N) M N

instance FirstOrder.Language.Embedding.strongHomClass {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : L.StrongHomClass (L.Embedding M N) M N

@[simp]

theorem FirstOrder.Language.Embedding.map_fun {L : 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) : φ (Structure.funMap f x) = Structure.funMap f (⇑φ ∘ x)

@[simp]

theorem FirstOrder.Language.Embedding.map_constants {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Embedding M N) (c : L.Constants) : φ ↑c = ↑c

@[simp]

theorem FirstOrder.Language.Embedding.map_rel {L : 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) : Structure.RelMap r (⇑φ ∘ x) ↔ Structure.RelMap r x

def FirstOrder.Language.Embedding.toHom {L : 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.

@[simp]

theorem FirstOrder.Language.Embedding.coe_toHom {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.Embedding M N} : ⇑f.toHom = ⇑f

theorem FirstOrder.Language.Embedding.coe_injective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : Function.Injective DFunLike.coe

theorem FirstOrder.Language.Embedding.ext {L : 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 FirstOrder.Language.Embedding.ext_iff {L : 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

theorem FirstOrder.Language.Embedding.toHom_injective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : Function.Injective fun (x : L.Embedding M N) => x.toHom

@[simp]

theorem FirstOrder.Language.Embedding.toHom_inj {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.Embedding M N} : f.toHom = g.toHom ↔ f = g

theorem FirstOrder.Language.Embedding.injective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Embedding M N) : Function.Injective ⇑f

def FirstOrder.Language.Embedding.ofInjective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsAlgebraic] {f : L.Hom M N} (hf : Function.Injective ⇑f) : L.Embedding M N

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

@[simp]

theorem FirstOrder.Language.Embedding.ofInjective_toFun {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsAlgebraic] {f : L.Hom M N} (hf : Function.Injective ⇑f) (a✝ : M) : (ofInjective hf) a✝ = f a✝

@[simp]

theorem FirstOrder.Language.Embedding.coeFn_ofInjective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsAlgebraic] {f : L.Hom M N} (hf : Function.Injective ⇑f) : ⇑(ofInjective hf) = ⇑f

@[simp]

theorem FirstOrder.Language.Embedding.ofInjective_toHom {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsAlgebraic] {f : L.Hom M N} (hf : Function.Injective ⇑f) : (ofInjective hf).toHom = f

def FirstOrder.Language.Embedding.refl (L : Language) (M : Type w) [L.Structure M] : L.Embedding M M

The identity embedding from a structure to itself.

@[implicit_reducible]

instance FirstOrder.Language.Embedding.instInhabited {L : Language} {M : Type w} [L.Structure M] : Inhabited (L.Embedding M M)

@[simp]

theorem FirstOrder.Language.Embedding.refl_apply {L : Language} {M : Type w} [L.Structure M] (x : M) : (refl L M) x = x

def FirstOrder.Language.Embedding.comp {L : 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.

@[simp]

theorem FirstOrder.Language.Embedding.comp_apply {L : 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 FirstOrder.Language.Embedding.comp_assoc {L : 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.

theorem FirstOrder.Language.Embedding.comp_injective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Embedding N P) : Function.Injective h.comp

@[simp]

theorem FirstOrder.Language.Embedding.comp_inj {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Embedding N P) (f g : L.Embedding M N) : h.comp f = h.comp g ↔ f = g

theorem FirstOrder.Language.Embedding.toHom_comp_injective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Embedding N P) : Function.Injective h.toHom.comp

@[simp]

theorem FirstOrder.Language.Embedding.toHom_comp_inj {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Embedding N P) (f g : L.Hom M N) : h.toHom.comp f = h.toHom.comp g ↔ f = g

@[simp]

theorem FirstOrder.Language.Embedding.comp_toHom {L : 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).toHom = hnp.toHom.comp hmn.toHom

@[simp]

theorem FirstOrder.Language.Embedding.comp_refl {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Embedding M N) : f.comp (refl L M) = f

@[simp]

theorem FirstOrder.Language.Embedding.refl_comp {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Embedding M N) : (refl L N).comp f = f

@[simp]

theorem FirstOrder.Language.Embedding.refl_toHom {L : Language} {M : Type w} [L.Structure M] : (refl L M).toHom = Hom.id L M

def FirstOrder.Language.StrongHomClass.toEmbedding {L : Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N] : F → L.Embedding M N

Any element of an injective StrongHomClass can be realized as a first order embedding.

@[simp]

theorem FirstOrder.Language.StrongHomClass.toEmbedding_toFun {L : Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N] (a✝ : F) (a : M) : (toEmbedding a✝) a = a✝ a

@[implicit_reducible]

instance FirstOrder.Language.Equiv.instEquivLike {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : EquivLike (L.Equiv M N) M N

instance FirstOrder.Language.Equiv.instStrongHomClass {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : L.StrongHomClass (L.Equiv M N) M N

def FirstOrder.Language.Equiv.symm {L : 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.

@[simp]

theorem FirstOrder.Language.Equiv.symm_symm {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : f.symm.symm = f

theorem FirstOrder.Language.Equiv.symm_bijective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : Function.Bijective symm

@[simp]

theorem FirstOrder.Language.Equiv.apply_symm_apply {L : 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 FirstOrder.Language.Equiv.symm_apply_apply {L : 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 FirstOrder.Language.Equiv.map_fun {L : 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) : φ (Structure.funMap f x) = Structure.funMap f (⇑φ ∘ x)

@[simp]

theorem FirstOrder.Language.Equiv.map_constants {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Equiv M N) (c : L.Constants) : φ ↑c = ↑c

@[simp]

theorem FirstOrder.Language.Equiv.map_rel {L : 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) : Structure.RelMap r (⇑φ ∘ x) ↔ Structure.RelMap r x

def FirstOrder.Language.Equiv.toEmbedding {L : 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.

def FirstOrder.Language.Equiv.toHom {L : 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.

@[simp]

theorem FirstOrder.Language.Equiv.toEmbedding_toHom {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : f.toEmbedding.toHom = f.toHom

@[simp]

theorem FirstOrder.Language.Equiv.coe_toHom {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.Equiv M N} : ⇑f.toHom = ⇑f

@[simp]

theorem FirstOrder.Language.Equiv.coe_toEmbedding {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : ⇑f.toEmbedding = ⇑f

theorem FirstOrder.Language.Equiv.injective_toEmbedding {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : Function.Injective toEmbedding

theorem FirstOrder.Language.Equiv.coe_injective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : Function.Injective DFunLike.coe

theorem FirstOrder.Language.Equiv.ext {L : 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 FirstOrder.Language.Equiv.ext_iff {L : 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 FirstOrder.Language.Equiv.bijective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : Function.Bijective ⇑f

theorem FirstOrder.Language.Equiv.injective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : Function.Injective ⇑f

theorem FirstOrder.Language.Equiv.surjective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : Function.Surjective ⇑f

def FirstOrder.Language.Equiv.refl (L : Language) (M : Type w) [L.Structure M] : L.Equiv M M

The identity equivalence from a structure to itself.

@[implicit_reducible]

instance FirstOrder.Language.Equiv.instInhabited {L : Language} {M : Type w} [L.Structure M] : Inhabited (L.Equiv M M)

@[simp]

theorem FirstOrder.Language.Equiv.refl_apply {L : Language} {M : Type w} [L.Structure M] (x : M) : (refl L M) x = x

def FirstOrder.Language.Equiv.comp {L : 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.

@[simp]

theorem FirstOrder.Language.Equiv.comp_apply {L : 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)

@[simp]

theorem FirstOrder.Language.Equiv.comp_refl {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (g : L.Equiv M N) : g.comp (refl L M) = g

@[simp]

theorem FirstOrder.Language.Equiv.refl_comp {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (g : L.Equiv M N) : (refl L N).comp g = g

@[simp]

theorem FirstOrder.Language.Equiv.refl_toEmbedding {L : Language} {M : Type w} [L.Structure M] : (refl L M).toEmbedding = Embedding.refl L M

@[simp]

theorem FirstOrder.Language.Equiv.refl_toHom {L : Language} {M : Type w} [L.Structure M] : (refl L M).toHom = Hom.id L M

theorem FirstOrder.Language.Equiv.comp_assoc {L : 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.

theorem FirstOrder.Language.Equiv.injective_comp {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Equiv N P) : Function.Injective h.comp

@[simp]

theorem FirstOrder.Language.Equiv.comp_toHom {L : 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) : (hnp.comp hmn).toHom = hnp.toHom.comp hmn.toHom

@[simp]

theorem FirstOrder.Language.Equiv.comp_toEmbedding {L : 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) : (hnp.comp hmn).toEmbedding = hnp.toEmbedding.comp hmn.toEmbedding

@[simp]

theorem FirstOrder.Language.Equiv.self_comp_symm {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : f.comp f.symm = refl L N

@[simp]

theorem FirstOrder.Language.Equiv.symm_comp_self {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : f.symm.comp f = refl L M

@[simp]

theorem FirstOrder.Language.Equiv.symm_comp_self_toEmbedding {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : f.symm.toEmbedding.comp f.toEmbedding = Embedding.refl L M

@[simp]

theorem FirstOrder.Language.Equiv.self_comp_symm_toEmbedding {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : f.toEmbedding.comp f.symm.toEmbedding = Embedding.refl L N

@[simp]

theorem FirstOrder.Language.Equiv.symm_comp_self_toHom {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : f.symm.toHom.comp f.toHom = Hom.id L M

@[simp]

theorem FirstOrder.Language.Equiv.self_comp_symm_toHom {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : f.toHom.comp f.symm.toHom = Hom.id L N

@[simp]

theorem FirstOrder.Language.Equiv.comp_symm {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (f : L.Equiv M N) (g : L.Equiv N P) : (g.comp f).symm = f.symm.comp g.symm

theorem FirstOrder.Language.Equiv.comp_right_injective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Equiv M N) : Function.Injective fun (f : L.Equiv N P) => f.comp h

@[simp]

theorem FirstOrder.Language.Equiv.comp_right_inj {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Equiv M N) (f g : L.Equiv N P) : f.comp h = g.comp h ↔ f = g

def FirstOrder.Language.StrongHomClass.toEquiv {L : Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [EquivLike F M N] [L.StrongHomClass F M N] : F → L.Equiv M N

Any element of a bijective StrongHomClass can be realized as a first order isomorphism.

@[simp]

theorem FirstOrder.Language.StrongHomClass.toEquiv_toFun {L : Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [EquivLike F M N] [L.StrongHomClass F M N] (a✝ : F) (a : M) : (toEquiv a✝) a = a✝ a

@[simp]

theorem FirstOrder.Language.StrongHomClass.toEquiv_invFun {L : Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [EquivLike F M N] [L.StrongHomClass F M N] (a✝ : F) (a✝¹ : N) : (toEquiv a✝).invFun a✝¹ = EquivLike.inv a✝ a✝¹

@[implicit_reducible]

instance FirstOrder.Language.sumStructure (L₁ : Language) (L₂ : Language) (S : Type u_3) [L₁.Structure S] [L₂.Structure S] : (L₁.sum L₂).Structure S

@[simp]

theorem FirstOrder.Language.funMap_sumInl {L₁ : Language} {L₂ : Language} {S : Type u_3} [L₁.Structure S] [L₂.Structure S] {n : ℕ} (f : L₁.Functions n) : Structure.funMap (Sum.inl f) = Structure.funMap f

@[simp]

theorem FirstOrder.Language.funMap_sumInr {L₁ : Language} {L₂ : Language} {S : Type u_3} [L₁.Structure S] [L₂.Structure S] {n : ℕ} (f : L₂.Functions n) : Structure.funMap (Sum.inr f) = Structure.funMap f

@[simp]

theorem FirstOrder.Language.relMap_sumInl {L₁ : Language} {L₂ : Language} {S : Type u_3} [L₁.Structure S] [L₂.Structure S] {n : ℕ} (R : L₁.Relations n) : Structure.RelMap (Sum.inl R) = Structure.RelMap R

@[simp]

theorem FirstOrder.Language.relMap_sumInr {L₁ : Language} {L₂ : Language} {S : Type u_3} [L₁.Structure S] [L₂.Structure S] {n : ℕ} (R : L₂.Relations n) : Structure.RelMap (Sum.inr R) = Structure.RelMap R

@[implicit_reducible]

def FirstOrder.Language.emptyStructure {M : Type w} : Language.empty.Structure M

Any type can be made uniquely into a structure over the empty language.

@[implicit_reducible]

instance FirstOrder.Language.instUniqueStructureEmpty {M : Type w} : Unique (Language.empty.Structure M)

@[instance 100]

instance FirstOrder.Language.strongHomClassEmpty {M : Type w} {N : Type w'} [Language.empty.Structure M] [Language.empty.Structure N] {F : Type u_3} [FunLike F M N] : Language.empty.StrongHomClass F M N

@[simp]

theorem FirstOrder.Language.empty.nonempty_embedding_iff {M : Type w} {N : Type w'} [Language.empty.Structure M] [Language.empty.Structure N] : Nonempty (Language.empty.Embedding M N) ↔ Cardinal.lift.{w', w} (Cardinal.mk M) ≤ Cardinal.lift.{w, w'} (Cardinal.mk N)

@[simp]

theorem FirstOrder.Language.empty.nonempty_equiv_iff {M : Type w} {N : Type w'} [Language.empty.Structure M] [Language.empty.Structure N] : Nonempty (Language.empty.Equiv M N) ↔ Cardinal.lift.{w', w} (Cardinal.mk M) = Cardinal.lift.{w, w'} (Cardinal.mk N)

def Function.emptyHom {M : Type w} {N : Type w'} [FirstOrder.Language.empty.Structure M] [FirstOrder.Language.empty.Structure N] (f : M → N) : FirstOrder.Language.empty.Hom M N

Makes a Language.empty.Hom out of any function. This is only needed because there is no instance of FunLike (M → N) M N, and thus no instance of Language.empty.HomClass M N.

@[simp]

theorem Function.emptyHom_toFun {M : Type w} {N : Type w'} [FirstOrder.Language.empty.Structure M] [FirstOrder.Language.empty.Structure N] (f : M → N) (a✝ : M) : (emptyHom f) a✝ = f a✝

@[implicit_reducible]

def Equiv.inducedStructure {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M ≃ N) : L.Structure N

A structure induced by a bijection.

@[simp]

theorem Equiv.inducedStructure_funMap {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M ≃ N) {n✝ : ℕ} (f : L.Functions n✝) (x : Fin n✝ → N) : FirstOrder.Language.Structure.funMap f x = e (FirstOrder.Language.Structure.funMap f (⇑e.symm ∘ x))

@[simp]

theorem Equiv.inducedStructure_RelMap {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M ≃ N) {n✝ : ℕ} (r : L.Relations n✝) (x : Fin n✝ → N) : FirstOrder.Language.Structure.RelMap r x = FirstOrder.Language.Structure.RelMap r (⇑e.symm ∘ x)

def Equiv.inducedStructureEquiv {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M ≃ N) : L.Equiv M N

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

@[simp]

theorem Equiv.toEquiv_inducedStructureEquiv {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M ≃ N) : e.inducedStructureEquiv.toEquiv = e

@[simp]

theorem Equiv.toFun_inducedStructureEquiv {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M ≃ N) : ⇑e.inducedStructureEquiv = ⇑e

@[simp]

theorem Equiv.toFun_inducedStructureEquiv_Symm {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M ≃ N) : ⇑e.inducedStructureEquiv.symm = ⇑e.symm