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* of functions of that arity

• Relations : ℕ → Type v

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

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

Used to define FirstOrder.Language₂.

Equations

• FirstOrder.Sequence₂ a₀ a₁ a₂ x = match x with | 0 => a₀ | 1 => a₁ | 2 => a₂ | x => PEmpty.{u + 1}

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

Equations

• FirstOrder.Sequence₂.inhabited₀ a₀ a₁ a₂ = h

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

Equations

• FirstOrder.Sequence₂.inhabited₁ a₀ a₁ a₂ = h

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

Equations

• FirstOrder.Sequence₂.inhabited₂ a₀ a₁ a₂ = h

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

Equations

• ⋯ = ⋯

@[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₂_Functions (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) : ∀ (a : ℕ), (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Functions a = FirstOrder.Sequence₂ c f₁ f₂ 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.mk₂ c f₁ f₂ r₁ r₂).Relations a = FirstOrder.Sequence₂ PEmpty.{v + 1} r₁ r₂ 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.

Equations

• FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂ = { Functions := FirstOrder.Sequence₂ c f₁ f₂, Relations := FirstOrder.Sequence₂ PEmpty.{v + 1} r₁ r₂ }

def FirstOrder.Language.empty : FirstOrder.Language

The empty language has no symbols.

Equations

• FirstOrder.Language.empty = { Functions := fun (x : ℕ) => Empty, Relations := fun (x : ℕ) => Empty }

instance FirstOrder.Language.instInhabitedLanguage : Inhabited FirstOrder.Language

Equations

• FirstOrder.Language.instInhabitedLanguage = { default := FirstOrder.Language.empty }

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.

Equations

• FirstOrder.Language.sum L L' = { Functions := fun (n : ℕ) => L.Functions n ⊕ L'.Functions n, Relations := fun (n : ℕ) => L.Relations n ⊕ L'.Relations n }

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

The type of constants in a given language.

Equations

• FirstOrder.Language.Constants L = L.Functions 0

@[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.

Equations

• FirstOrder.Language.Symbols L = ((l : ℕ) × L.Functions l ⊕ (l : ℕ) × L.Relations l)

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

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

Equations

• FirstOrder.Language.card L = Cardinal.mk (FirstOrder.Language.Symbols L)

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

A language is relational when it has no function symbols.

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

  There are no function symbols in the language.

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

A language is algebraic when it has no relation symbols.

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

  There are no relation symbols in the language.

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 (L.Functions l))) + Cardinal.sum fun (l : ℕ) => Cardinal.lift.{u, v} (Cardinal.mk (L.Relations l))

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• FirstOrder.Language.isRelational_empty = ⋯

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

Equations

• FirstOrder.Language.isAlgebraic_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')

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.mk₂ c f₁ f₂ r₁ r₂).Functions n)

Equations

• ⋯ = ⋯

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.mk₂ c f₁ f₂ r₁ r₂).Relations n)

Equations

• ⋯ = ⋯

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

Equations

• FirstOrder.Language.isEmpty_empty = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

theorem FirstOrder.Language.card_functions_sum {L : FirstOrder.Language} {L' : FirstOrder.Language} (i : ℕ) : Cardinal.mk ((FirstOrder.Language.sum L 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 : FirstOrder.Language} {L' : FirstOrder.Language} (i : ℕ) : Cardinal.mk ((FirstOrder.Language.sum L L').Relations i) = Cardinal.lift.{v', v} (Cardinal.mk (L.Relations i)) + Cardinal.lift.{v, v'} (Cardinal.mk (L'.Relations 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_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

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

class FirstOrder.Language.Structure (L : FirstOrder.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

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

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

Equations

• FirstOrder.Language.Inhabited.trivialStructure L = { funMap := fun {n : ℕ} => default, RelMap := fun {n : ℕ} => default }

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

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 (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.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), FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.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.

Equations

• One or more equations did not get rendered due to their size.

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

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

• toFun : M → N
• inj' : Function.Injective self.toFun
• map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), self.toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.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), FirstOrder.Language.Structure.RelMap r (self.toFun ∘ x) ↔ FirstOrder.Language.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.

Equations

• One or more equations did not get rendered due to their size.

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

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 (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.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), FirstOrder.Language.Structure.RelMap r (self.toFun ∘ x) ↔ FirstOrder.Language.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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ↑c = FirstOrder.Language.Structure.funMap c default

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

Equations

• FirstOrder.Language.instCoeTCConstants = { coe := FirstOrder.Language.constantMap }

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.mk₂ c f₁ f₂ r₁ r₂).Functions n → (Fin n → M) → M

The function map for FirstOrder.Language.Structure₂.

Equations

• One or more equations did not get rendered due to their size.

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.mk₂ c f₁ f₂ r₁ r₂).Relations n → (Fin n → M) → Prop

The relation map for FirstOrder.Language.Structure₂.

Equations

• One or more equations did not get rendered due to their size.

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₂.

Equations

• FirstOrder.Language.Structure.mk₂ c' f₁' f₂' r₁' r₂' = { funMap := fun {n : ℕ} => FirstOrder.Language.funMap₂ c' f₁' f₂', RelMap := fun {n : ℕ} => FirstOrder.Language.RelMap₂ r₁' r₂' }

@[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 : Type u_4) (N : Type u_5) [FunLike F M N] [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L 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), φ (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 : L.Relations 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

class FirstOrder.Language.StrongHomClass (L : outParam FirstOrder.Language) (F : Type u_3) (M : Type u_4) (N : Type u_5) [FunLike F M N] [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L 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), φ (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 : L.Relations 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

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 N] [FirstOrder.Language.StrongHomClass L F M N] : FirstOrder.Language.HomClass L F M N

Equations

• ⋯ = ⋯

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 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 N] [FirstOrder.Language.HomClass L F M N] (φ : F) (c : FirstOrder.Language.Constants L) : φ ↑c = ↑c

instance FirstOrder.Language.Hom.instFunLike {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 N

Equations

• FirstOrder.Language.Hom.instFunLike = { coe := FirstOrder.Language.Hom.toFun, coe_injective' := ⋯ }

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

Equations

• ⋯ = ⋯

instance FirstOrder.Language.Hom.instStrongHomClassHomInstFunLike {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

Equations

• ⋯ = ⋯

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 : FirstOrder.Language.Hom L M N) => M → N

Equations

• FirstOrder.Language.Hom.hasCoeToFun = DFunLike.hasCoeToFun

@[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 : L.Functions 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 : L.Relations 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.

Equations

• FirstOrder.Language.Hom.id L M = { toFun := fun (m : M) => m, map_fun' := ⋯, map_rel' := ⋯ }

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

Equations

• FirstOrder.Language.Hom.instInhabitedHom = { default := FirstOrder.Language.Hom.id L 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.

Equations

• FirstOrder.Language.Hom.comp hnp hmn = { toFun := ⇑hnp ∘ ⇑hmn, map_fun' := ⋯, map_rel' := ⋯ }

@[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.

@[simp]

theorem FirstOrder.Language.Hom.comp_id {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) : FirstOrder.Language.Hom.comp f (FirstOrder.Language.Hom.id L M) = f

@[simp]

theorem FirstOrder.Language.Hom.id_comp {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) : FirstOrder.Language.Hom.comp (FirstOrder.Language.Hom.id L N) f = f

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

Equations

• FirstOrder.Language.HomClass.toHom φ = { toFun := ⇑φ, map_fun' := ⋯, map_rel' := ⋯ }

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

Equations

• FirstOrder.Language.Embedding.funLike = { coe := fun (f : FirstOrder.Language.Embedding L M N) => f.toFun, coe_injective' := ⋯ }

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[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 : L.Functions 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 : L.Relations 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.

Equations

• FirstOrder.Language.Embedding.toHom = FirstOrder.Language.HomClass.toHom

@[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 DFunLike.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.toHom_injective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : Function.Injective fun (x : FirstOrder.Language.Embedding L M N) => FirstOrder.Language.Embedding.toHom x

@[simp]

theorem FirstOrder.Language.Embedding.toHom_inj {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} : FirstOrder.Language.Embedding.toHom f = FirstOrder.Language.Embedding.toHom g ↔ f = g

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.

Equations

• FirstOrder.Language.Embedding.ofInjective hf = { toEmbedding := { toFun := f.toFun, inj' := hf }, map_fun' := ⋯, map_rel' := ⋯ }

@[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.

Equations

• FirstOrder.Language.Embedding.refl L M = { toEmbedding := Function.Embedding.refl M, map_fun' := ⋯, map_rel' := ⋯ }

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

Equations

• FirstOrder.Language.Embedding.instInhabitedEmbedding = { default := FirstOrder.Language.Embedding.refl L 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.

Equations

• FirstOrder.Language.Embedding.comp hnp hmn = { toEmbedding := { toFun := ⇑hnp ∘ ⇑hmn, inj' := ⋯ }, map_fun' := ⋯, map_rel' := ⋯ }

@[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.

theorem FirstOrder.Language.Embedding.comp_injective {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] (h : FirstOrder.Language.Embedding L N P) : Function.Injective (FirstOrder.Language.Embedding.comp h)

@[simp]

theorem FirstOrder.Language.Embedding.comp_inj {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] (h : FirstOrder.Language.Embedding L N P) (f : FirstOrder.Language.Embedding L M N) (g : FirstOrder.Language.Embedding L M N) : FirstOrder.Language.Embedding.comp h f = FirstOrder.Language.Embedding.comp h g ↔ f = g

theorem FirstOrder.Language.Embedding.toHom_comp_injective {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] (h : FirstOrder.Language.Embedding L N P) : Function.Injective (FirstOrder.Language.Hom.comp (FirstOrder.Language.Embedding.toHom h))

@[simp]

theorem FirstOrder.Language.Embedding.toHom_comp_inj {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] (h : FirstOrder.Language.Embedding L N P) (f : FirstOrder.Language.Hom L M N) (g : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Hom.comp (FirstOrder.Language.Embedding.toHom h) f = FirstOrder.Language.Hom.comp (FirstOrder.Language.Embedding.toHom h) g ↔ f = g

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

@[simp]

theorem FirstOrder.Language.Embedding.comp_refl {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.comp f (FirstOrder.Language.Embedding.refl L M) = f

@[simp]

theorem FirstOrder.Language.Embedding.refl_comp {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.comp (FirstOrder.Language.Embedding.refl L N) f = f

@[simp]

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

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] [FunLike F M 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.

Equations

• FirstOrder.Language.StrongHomClass.toEmbedding φ = { toEmbedding := { toFun := ⇑φ, inj' := ⋯ }, map_fun' := ⋯, map_rel' := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

instance FirstOrder.Language.Equiv.instStrongHomClassEquivToFunLikeInstEquivLikeEquiv {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

Equations

• ⋯ = ⋯

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.

Equations

• FirstOrder.Language.Equiv.symm f = let __src := f.symm; { toEquiv := __src, map_fun' := ⋯, map_rel' := ⋯ }

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 : FirstOrder.Language.Equiv L M N) => M → N

Equations

• FirstOrder.Language.Equiv.hasCoeToFun = DFunLike.hasCoeToFun

@[simp]

theorem FirstOrder.Language.Equiv.symm_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.symm (FirstOrder.Language.Equiv.symm f) = f

@[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 : L.Functions 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 : L.Relations 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.

Equations

• FirstOrder.Language.Equiv.toEmbedding = FirstOrder.Language.StrongHomClass.toEmbedding

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.

Equations

• FirstOrder.Language.Equiv.toHom = FirstOrder.Language.HomClass.toHom

@[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.injective_toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : Function.Injective FirstOrder.Language.Equiv.toEmbedding

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 DFunLike.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.

Equations

• FirstOrder.Language.Equiv.refl L M = { toEquiv := Equiv.refl M, map_fun' := ⋯, map_rel' := ⋯ }

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

Equations

• FirstOrder.Language.Equiv.instInhabitedEquiv = { default := FirstOrder.Language.Equiv.refl L 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.

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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.

theorem FirstOrder.Language.Equiv.injective_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] (h : FirstOrder.Language.Equiv L N P) : Function.Injective (FirstOrder.Language.Equiv.comp h)

@[simp]

theorem FirstOrder.Language.Equiv.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.Equiv L N P) (hmn : FirstOrder.Language.Equiv L M N) : FirstOrder.Language.Equiv.toHom (FirstOrder.Language.Equiv.comp hnp hmn) = FirstOrder.Language.Hom.comp (FirstOrder.Language.Equiv.toHom hnp) (FirstOrder.Language.Equiv.toHom hmn)

@[simp]

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

@[simp]

theorem FirstOrder.Language.Equiv.self_comp_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.comp f (FirstOrder.Language.Equiv.symm f) = FirstOrder.Language.Equiv.refl L N

@[simp]

theorem FirstOrder.Language.Equiv.symm_comp_self {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.comp (FirstOrder.Language.Equiv.symm f) f = FirstOrder.Language.Equiv.refl L M

@[simp]

theorem FirstOrder.Language.Equiv.symm_comp_self_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.Embedding.comp (FirstOrder.Language.Equiv.toEmbedding (FirstOrder.Language.Equiv.symm f)) (FirstOrder.Language.Equiv.toEmbedding f) = FirstOrder.Language.Embedding.refl L M

@[simp]

theorem FirstOrder.Language.Equiv.self_comp_symm_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.Embedding.comp (FirstOrder.Language.Equiv.toEmbedding f) (FirstOrder.Language.Equiv.toEmbedding (FirstOrder.Language.Equiv.symm f)) = FirstOrder.Language.Embedding.refl L N

@[simp]

theorem FirstOrder.Language.Equiv.symm_comp_self_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.Hom.comp (FirstOrder.Language.Equiv.toHom (FirstOrder.Language.Equiv.symm f)) (FirstOrder.Language.Equiv.toHom f) = FirstOrder.Language.Hom.id L M

@[simp]

theorem FirstOrder.Language.Equiv.self_comp_symm_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.Hom.comp (FirstOrder.Language.Equiv.toHom f) (FirstOrder.Language.Equiv.toHom (FirstOrder.Language.Equiv.symm f)) = FirstOrder.Language.Hom.id L N

@[simp]

theorem FirstOrder.Language.Equiv.comp_symm {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] (f : FirstOrder.Language.Equiv L M N) (g : FirstOrder.Language.Equiv L N P) : FirstOrder.Language.Equiv.symm (FirstOrder.Language.Equiv.comp g f) = FirstOrder.Language.Equiv.comp (FirstOrder.Language.Equiv.symm f) (FirstOrder.Language.Equiv.symm g)

theorem FirstOrder.Language.Equiv.comp_right_injective {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] (h : FirstOrder.Language.Equiv L M N) : Function.Injective fun (f : FirstOrder.Language.Equiv L N P) => FirstOrder.Language.Equiv.comp f h

@[simp]

theorem FirstOrder.Language.Equiv.comp_right_inj {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] (h : FirstOrder.Language.Equiv L M N) (f : FirstOrder.Language.Equiv L N P) (g : FirstOrder.Language.Equiv L N P) : FirstOrder.Language.Equiv.comp f h = FirstOrder.Language.Equiv.comp g h ↔ f = g

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.

Equations

• FirstOrder.Language.StrongHomClass.toEquiv φ = { toEquiv := { toFun := ⇑φ, invFun := EquivLike.inv φ, left_inv := ⋯, right_inv := ⋯ }, map_fun' := ⋯, map_rel' := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

@[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 : L₁.Functions 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 : L₂.Functions 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 : L₁.Relations 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 : L₂.Relations 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

Equations

• FirstOrder.Language.emptyStructure = { funMap := fun {n : ℕ} => Empty.elim, RelMap := fun {n : ℕ} => Empty.elim }

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

Equations

• FirstOrder.Language.instUniqueStructureEmpty = { toInhabited := { default := FirstOrder.Language.emptyStructure }, uniq := ⋯ }

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

Equations

• ⋯ = ⋯

@[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.

Equations

• Function.emptyHom f = { toFun := f, map_fun' := ⋯, map_rel' := ⋯ }

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.

Equations

• Embedding.empty f = { toEmbedding := f, map_fun' := ⋯, map_rel' := ⋯ }

@[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.

Equations

• Equiv.empty f = { toEquiv := f, map_fun' := ⋯, map_rel' := ⋯ }

@[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_funMap {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L 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} [FirstOrder.Language.Structure L 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.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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Equiv.inducedStructureEquiv e = { toEquiv := e, map_fun' := ⋯, map_rel' := ⋯ }

@[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