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

• Functions : ℕ → Type u

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

• Relations : ℕ → Type v

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

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.

def FirstOrder.Sequence₂ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) : ℕ → Type u

Used to define FirstOrder.Language₂.

instance FirstOrder.Sequence₂.inhabited₀ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) [h : Inhabited a₀] : Inhabited (FirstOrder.Sequence₂ a₀ a₁ a₂ 0)

instance FirstOrder.Sequence₂.inhabited₁ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) [h : Inhabited a₁] : Inhabited (FirstOrder.Sequence₂ a₀ a₁ a₂ 1)

instance FirstOrder.Sequence₂.inhabited₂ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) [h : Inhabited a₂] : Inhabited (FirstOrder.Sequence₂ a₀ a₁ a₂ 2)

instance FirstOrder.Sequence₂.instIsEmptySequence₂HAddNatInstHAddInstAddNatOfNat (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) {n : ℕ} : IsEmpty (FirstOrder.Sequence₂ a₀ a₁ a₂ (n + 3))

@[simp]

theorem FirstOrder.Sequence₂.lift_mk (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) {i : ℕ} : Cardinal.lift.{v, u} (Cardinal.mk (FirstOrder.Sequence₂ a₀ a₁ a₂ i)) = Cardinal.mk (FirstOrder.Sequence₂ (ULift.{v, u} a₀) (ULift.{v, u} a₁) (ULift.{v, u} a₂) i)

@[simp]

theorem FirstOrder.Sequence₂.sum_card (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) : (Cardinal.sum fun i => Cardinal.mk (FirstOrder.Sequence₂ a₀ a₁ a₂ i)) = Cardinal.mk a₀ + Cardinal.mk a₁ + Cardinal.mk a₂

@[simp]

theorem FirstOrder.Language.mk₂_Relations (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) : ∀ (a : ℕ), FirstOrder.Language.Relations (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) a = FirstOrder.Sequence₂ PEmpty.{v + 1} r₁ r₂ a

@[simp]

theorem FirstOrder.Language.mk₂_Functions (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) : ∀ (a : ℕ), FirstOrder.Language.Functions (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) a = FirstOrder.Sequence₂ c f₁ f₂ a

def FirstOrder.Language.mk₂ (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) : FirstOrder.Language

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

def FirstOrder.Language.empty : FirstOrder.Language

The empty language has no symbols.

instance FirstOrder.Language.instInhabitedLanguage : Inhabited FirstOrder.Language

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

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

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

The type of constants in a given language.

@[simp]

theorem FirstOrder.Language.constants_mk₂ (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) : FirstOrder.Language.Constants (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) = c

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

The type of symbols in a given language.

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

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

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

• empty_functions : ∀ (n : ℕ), IsEmpty (FirstOrder.Language.Functions L n)

  There are no function symbols in the language.

A language is relational when it has no function symbols.

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

• empty_relations : ∀ (n : ℕ), IsEmpty (FirstOrder.Language.Relations L n)

  There are no relation symbols in the language.

A language is algebraic when it has no relation symbols.

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

instance FirstOrder.Language.instIsEmptyFunctions {L : FirstOrder.Language} [FirstOrder.Language.IsRelational L] {n : ℕ} : IsEmpty (FirstOrder.Language.Functions L n)

instance FirstOrder.Language.instIsEmptyRelations {L : FirstOrder.Language} [FirstOrder.Language.IsAlgebraic L] {n : ℕ} : IsEmpty (FirstOrder.Language.Relations L n)

instance FirstOrder.Language.isRelational_of_empty_functions {symb : ℕ → Type u_1} : FirstOrder.Language.IsRelational { Functions := fun x => Empty, Relations := symb }

instance FirstOrder.Language.isAlgebraic_of_empty_relations {symb : ℕ → Type u_1} : FirstOrder.Language.IsAlgebraic { Functions := symb, Relations := fun x => Empty }

instance FirstOrder.Language.isRelational_empty : FirstOrder.Language.IsRelational FirstOrder.Language.empty

instance FirstOrder.Language.isAlgebraic_empty : FirstOrder.Language.IsAlgebraic FirstOrder.Language.empty

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

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

instance FirstOrder.Language.isRelational_mk₂ {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} [h0 : IsEmpty c] [h1 : IsEmpty f₁] [h2 : IsEmpty f₂] : FirstOrder.Language.IsRelational (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂)

instance FirstOrder.Language.isAlgebraic_mk₂ {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} [h1 : IsEmpty r₁] [h2 : IsEmpty r₂] : FirstOrder.Language.IsAlgebraic (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂)

instance FirstOrder.Language.subsingleton_mk₂_functions {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} [h0 : Subsingleton c] [h1 : Subsingleton f₁] [h2 : Subsingleton f₂] {n : ℕ} : Subsingleton (FirstOrder.Language.Functions (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) n)

instance FirstOrder.Language.subsingleton_mk₂_relations {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} [h1 : Subsingleton r₁] [h2 : Subsingleton r₂] {n : ℕ} : Subsingleton (FirstOrder.Language.Relations (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) n)

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.card_mk₂ (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) : FirstOrder.Language.card (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) = Cardinal.lift.{v, u} (Cardinal.mk c) + Cardinal.lift.{v, u} (Cardinal.mk f₁) + Cardinal.lift.{v, u} (Cardinal.mk f₂) + Cardinal.lift.{u, v} (Cardinal.mk r₁) + Cardinal.lift.{u, v} (Cardinal.mk r₂)

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

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

class FirstOrder.Language.Structure (L : FirstOrder.Language) (M : Type w) : Type (max (max u v) w)

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

  Interpretation of the function symbols

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

  Interpretation of the relation symbols

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.

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

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

Maps

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

• toFun : M → N

  The underlying function of a homomorphism of structures

• map_fun' : ∀ {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M), FirstOrder.Language.Hom.toFun s (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (s.toFun ∘ x)

  The homomorphism commutes with the interpretations of the function symbols

• map_rel' : ∀ {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (s.toFun ∘ x)

  The homomorphism sends related elements to related elements

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.

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 : FirstOrder.Language) (M : Type w) (N : Type w') [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] extends Function.Embedding : Type (max w w')

• toFun : M → N
• inj' : Function.Injective s.toFun
• map_fun' : ∀ {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M), Function.Embedding.toFun s.toEmbedding (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (s.toFun ∘ x)

  The homomorphism commutes with the interpretations of the function symbols

• map_rel' : ∀ {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap r (s.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x

  The homomorphism sends related elements to related elements

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

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 : FirstOrder.Language) (M : Type w) (N : Type w') [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] extends Equiv : Type (max w w')

• toFun : M → N
• invFun : N → M
• left_inv : Function.LeftInverse s.invFun s.toFun
• right_inv : Function.RightInverse s.invFun s.toFun
• map_fun' : ∀ {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M), Equiv.toFun s.toEquiv (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (s.toFun ∘ x)

  The homomorphism commutes with the interpretations of the function symbols

• map_rel' : ∀ {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap r (s.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x

  The homomorphism sends related elements to related elements

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

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 : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] (c : FirstOrder.Language.Constants L) : M

Interpretation of a constant symbol

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

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

theorem FirstOrder.Language.nonempty_of_nonempty_constants {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] [h : Nonempty (FirstOrder.Language.Constants L)] : 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.

def FirstOrder.Language.funMap₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (c' : c → M) (f₁' : f₁ → M → M) (f₂' : f₂ → M → M → M) {n : ℕ} : FirstOrder.Language.Functions (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) n → (Fin n → M) → M

The function map for FirstOrder.Language.Structure₂.

def FirstOrder.Language.RelMap₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (r₁' : r₁ → Set M) (r₂' : r₂ → M → M → Prop) {n : ℕ} : FirstOrder.Language.Relations (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) n → (Fin n → M) → Prop

The relation map for FirstOrder.Language.Structure₂.

def FirstOrder.Language.Structure.mk₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (c' : c → M) (f₁' : f₁ → M → M) (f₂' : f₂ → M → M → M) (r₁' : r₁ → Set M) (r₂' : r₂ → M → M → Prop) : FirstOrder.Language.Structure (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) M

A structure constructor to match FirstOrder.Language₂.

@[simp]

theorem FirstOrder.Language.Structure.funMap_apply₀ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {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} : FirstOrder.Language.Structure.funMap c₀ x = c' c₀

@[simp]

theorem FirstOrder.Language.Structure.funMap_apply₁ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {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) : FirstOrder.Language.Structure.funMap f ![x] = f₁' f x

@[simp]

theorem FirstOrder.Language.Structure.funMap_apply₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {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) (y : M) : FirstOrder.Language.Structure.funMap f ![x, y] = f₂' f x y

@[simp]

theorem FirstOrder.Language.Structure.relMap_apply₁ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {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) : FirstOrder.Language.Structure.RelMap r ![x] = (x ∈ r₁' r)

@[simp]

theorem FirstOrder.Language.Structure.relMap_apply₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {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) (y : M) : FirstOrder.Language.Structure.RelMap r ![x, y] = r₂' r x y

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

• map_fun : ∀ (φ : F) {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M), ↑φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (↑φ ∘ x)

  The homomorphism commutes with the interpretations of the function symbols

• map_rel : ∀ (φ : F) {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (↑φ ∘ x)

  The homomorphism sends related elements to related elements

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.

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

• map_fun : ∀ (φ : F) {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M), ↑φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (↑φ ∘ x)

  The homomorphism commutes with the interpretations of the function symbols

• map_rel : ∀ (φ : F) {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap r (↑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x

  The homomorphism sends related elements to related elements

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

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

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

Not an instance to avoid a loop.

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

instance FirstOrder.Language.Hom.funLike {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : FunLike (FirstOrder.Language.Hom L M N) M fun x => N

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

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

instance FirstOrder.Language.Hom.hasCoeToFun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : CoeFun (FirstOrder.Language.Hom L M N) fun x => M → N

@[simp]

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

theorem FirstOrder.Language.Hom.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] ⦃f : FirstOrder.Language.Hom L M N⦄ ⦃g : FirstOrder.Language.Hom L M N⦄ (h : ∀ (x : M), ↑f x = ↑g x) : f = g

theorem FirstOrder.Language.Hom.ext_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Hom L M N} {g : FirstOrder.Language.Hom L M N} : f = g ↔ ∀ (x : M), ↑f x = ↑g x

@[simp]

theorem FirstOrder.Language.Hom.map_fun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.Hom L M N) {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M) : ↑φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (↑φ ∘ x)

@[simp]

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

@[simp]

theorem FirstOrder.Language.Hom.map_rel {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.Hom L M N) {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M) : FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (↑φ ∘ x)

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

The identity map from a structure to itself.

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

@[simp]

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

def FirstOrder.Language.Hom.comp {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {P : Type u_1} [FirstOrder.Language.Structure L P] (hnp : FirstOrder.Language.Hom L N P) (hmn : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Hom L M P

Composition of first-order homomorphisms.

@[simp]

theorem FirstOrder.Language.Hom.comp_apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {P : Type u_1} [FirstOrder.Language.Structure L P] (g : FirstOrder.Language.Hom L N P) (f : FirstOrder.Language.Hom L M N) (x : M) : ↑(FirstOrder.Language.Hom.comp g f) x = ↑g (↑f x)

theorem FirstOrder.Language.Hom.comp_assoc {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {P : Type u_1} [FirstOrder.Language.Structure L P] {Q : Type u_2} [FirstOrder.Language.Structure L Q] (f : FirstOrder.Language.Hom L M N) (g : FirstOrder.Language.Hom L N P) (h : FirstOrder.Language.Hom L P Q) : FirstOrder.Language.Hom.comp (FirstOrder.Language.Hom.comp h g) f = FirstOrder.Language.Hom.comp h (FirstOrder.Language.Hom.comp g f)

Composition of first-order homomorphisms is associative.

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

Any element of a HomClass can be realized as a first_order homomorphism.

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

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

instance FirstOrder.Language.Embedding.hasCoeToFun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : CoeFun (FirstOrder.Language.Embedding L M N) fun x => M → N

@[simp]

theorem FirstOrder.Language.Embedding.map_fun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.Embedding L M N) {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M) : ↑φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (↑φ ∘ x)

@[simp]

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

@[simp]

theorem FirstOrder.Language.Embedding.map_rel {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.Embedding L M N) {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M) : FirstOrder.Language.Structure.RelMap r (↑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x

def FirstOrder.Language.Embedding.toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : FirstOrder.Language.Embedding L M N → FirstOrder.Language.Hom L M N

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

@[simp]

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

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

theorem FirstOrder.Language.Embedding.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] ⦃f : FirstOrder.Language.Embedding L M N⦄ ⦃g : FirstOrder.Language.Embedding L M N⦄ (h : ∀ (x : M), ↑f x = ↑g x) : f = g

theorem FirstOrder.Language.Embedding.ext_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Embedding L M N} {g : FirstOrder.Language.Embedding L M N} : f = g ↔ ∀ (x : M), ↑f x = ↑g x

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

The identity embedding from a structure to itself.

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

@[simp]

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

def FirstOrder.Language.Embedding.comp {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {P : Type u_1} [FirstOrder.Language.Structure L P] (hnp : FirstOrder.Language.Embedding L N P) (hmn : FirstOrder.Language.Embedding L M N) : FirstOrder.Language.Embedding L M P

Composition of first-order embeddings.

@[simp]

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

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

Composition of first-order embeddings is associative.

@[simp]

theorem FirstOrder.Language.Embedding.comp_toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {P : Type u_1} [FirstOrder.Language.Structure L P] (hnp : FirstOrder.Language.Embedding L N P) (hmn : FirstOrder.Language.Embedding L M N) : FirstOrder.Language.Embedding.toHom (FirstOrder.Language.Embedding.comp hnp hmn) = FirstOrder.Language.Hom.comp (FirstOrder.Language.Embedding.toHom hnp) (FirstOrder.Language.Embedding.toHom hmn)

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

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

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

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

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

The inverse of a first-order equivalence is a first-order equivalence.

instance FirstOrder.Language.Equiv.hasCoeToFun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : CoeFun (FirstOrder.Language.Equiv L M N) fun x => M → N

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.Equiv.map_fun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.Equiv L M N) {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M) : ↑φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (↑φ ∘ x)

@[simp]

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

@[simp]

theorem FirstOrder.Language.Equiv.map_rel {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.Equiv L M N) {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M) : FirstOrder.Language.Structure.RelMap r (↑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x

def FirstOrder.Language.Equiv.toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : FirstOrder.Language.Equiv L M N → FirstOrder.Language.Embedding L M N

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

def FirstOrder.Language.Equiv.toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : FirstOrder.Language.Equiv L M N → FirstOrder.Language.Hom L M N

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem FirstOrder.Language.Equiv.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] ⦃f : FirstOrder.Language.Equiv L M N⦄ ⦃g : FirstOrder.Language.Equiv L M N⦄ (h : ∀ (x : M), ↑f x = ↑g x) : f = g

theorem FirstOrder.Language.Equiv.ext_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.Equiv L M N} {g : FirstOrder.Language.Equiv L M N} : f = g ↔ ∀ (x : M), ↑f x = ↑g x

theorem FirstOrder.Language.Equiv.bijective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Equiv L M N) : Function.Bijective ↑f

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

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

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

The identity equivalence from a structure to itself.

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

@[simp]

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

def FirstOrder.Language.Equiv.comp {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {P : Type u_1} [FirstOrder.Language.Structure L P] (hnp : FirstOrder.Language.Equiv L N P) (hmn : FirstOrder.Language.Equiv L M N) : FirstOrder.Language.Equiv L M P

Composition of first-order equivalences.

@[simp]

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

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

Composition of first-order homomorphisms is associative.

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.empty.nonempty_embedding_iff {M : Type w} {N : Type w'} [FirstOrder.Language.Structure FirstOrder.Language.empty M] [FirstOrder.Language.Structure FirstOrder.Language.empty N] : Nonempty (FirstOrder.Language.Embedding FirstOrder.Language.empty 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'} [FirstOrder.Language.Structure FirstOrder.Language.empty M] [FirstOrder.Language.Structure FirstOrder.Language.empty N] : Nonempty (FirstOrder.Language.Equiv FirstOrder.Language.empty M N) ↔ Cardinal.lift.{w', w} (Cardinal.mk M) = Cardinal.lift.{w, w'} (Cardinal.mk N)

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

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

instance FirstOrder.Language.strongHomClassEmpty {F : Type u_3} {M : Type u_4} {N : Type u_5} [FunLike F M fun x => N] : FirstOrder.Language.StrongHomClass FirstOrder.Language.empty F M N

@[simp]

theorem Function.emptyHom_toFun {M : Type w} {N : Type w'} (f : M → N) : ∀ (a : M), ↑(Function.emptyHom f) a = f a

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

Makes a Language.empty.Hom out of any function.

def Embedding.empty {M : Type w} {N : Type w'} (f : M ↪ N) : FirstOrder.Language.Embedding FirstOrder.Language.empty M N

Makes a Language.empty.Embedding out of any function.

@[simp]

theorem FirstOrder.Language.toFun_embedding_empty {M : Type w} {N : Type w'} (f : M ↪ N) : ↑(Embedding.empty f) = ↑f

@[simp]

theorem FirstOrder.Language.toEmbedding_embedding_empty {M : Type w} {N : Type w'} (f : M ↪ N) : (Embedding.empty f).toEmbedding = f

def Equiv.empty {M : Type w} {N : Type w'} (f : M ≃ N) : FirstOrder.Language.Equiv FirstOrder.Language.empty M N

Makes a Language.empty.Equiv out of any function.

@[simp]

theorem FirstOrder.Language.toFun_equiv_empty {M : Type w} {N : Type w'} (f : M ≃ N) : ↑(Equiv.empty f) = ↑f

@[simp]

theorem FirstOrder.Language.toEquiv_equiv_empty {M : Type w} {N : Type w'} (f : M ≃ N) : (Equiv.empty f).toEquiv = f

@[simp]

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

@[simp]

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

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

A structure induced by a bijection.

def Equiv.inducedStructureEquiv {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] (e : M ≃ N) : FirstOrder.Language.Equiv L 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} [FirstOrder.Language.Structure L M] (e : M ≃ N) : (Equiv.inducedStructureEquiv e).toEquiv = e

@[simp]

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

@[simp]

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