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₂.instIsEmptyHAddNatOfNat (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.instInhabited : Inhabited FirstOrder.Language

Equations

• FirstOrder.Language.instInhabited = { 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

• L.sum 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

• L.Constants = 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.mk₂ c f₁ f₂ r₁ r₂).Constants = c

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

The type of symbols in a given language.

Equations

• L.Symbols = ((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

• L.card = Cardinal.mk L.Symbols

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.

theorem FirstOrder.Language.IsRelational.empty_functions {L : FirstOrder.Language} [self : L.IsRelational] (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.IsAlgebraic.empty_relations {L : FirstOrder.Language} [self : L.IsAlgebraic] (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} : L.card = (Cardinal.sum fun (l : ℕ) => Cardinal.lift.{v, u} (Cardinal.mk (L.Functions l))) + Cardinal.sum fun (l : ℕ) => Cardinal.lift.{u, v} (Cardinal.mk (L.Relations l))

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• FirstOrder.Language.isRelational_empty = ⋯

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

Equations

• FirstOrder.Language.isAlgebraic_empty = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

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.empty.card = 0

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

Equations

• FirstOrder.Language.isEmpty_empty = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.card_mk₂ (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) : (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).card = 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 : L.Structure M) (y : L.Structure 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 : L.Structure M) (y : L.Structure 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)

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 α] : L.Structure α

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

A homomorphism between first-order structures is a function that commutes with the interpretations of functions and maps tuples in one structure where a given relation is true to tuples in the second structure where that relation is still true.

• toFun : M → N

  The underlying function of a homomorphism of structures

• map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), self.toFun (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

theorem FirstOrder.Language.Hom.map_fun' {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (self : L.Hom M N) {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

theorem FirstOrder.Language.Hom.map_rel' {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (self : L.Hom M N) {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') [L.Structure M] [L.Structure 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

theorem FirstOrder.Language.Embedding.map_fun' {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (self : L.Embedding M N) {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

theorem FirstOrder.Language.Embedding.map_rel' {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (self : L.Embedding M N) {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') [L.Structure M] [L.Structure 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

theorem FirstOrder.Language.Equiv.map_fun' {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (self : L.Equiv M N) {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

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

Interpretation of a constant symbol

Equations

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

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

Equations

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

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

theorem FirstOrder.Language.nonempty_of_nonempty_constants {L : FirstOrder.Language} {M : Type w} [L.Structure M] [h : Nonempty L.Constants] : Nonempty M

Given a language with a nonempty type of constants, any structure will be nonempty. This cannot be a global instance, because L becomes a metavariable.

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

theorem FirstOrder.Language.HomClass.map_fun {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] [self : FirstOrder.Language.HomClass L F M N] (φ : 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

theorem FirstOrder.Language.HomClass.map_rel {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] [self : FirstOrder.Language.HomClass L F M N] (φ : 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

theorem FirstOrder.Language.StrongHomClass.map_fun {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] [self : FirstOrder.Language.StrongHomClass L F M N] (φ : 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

theorem FirstOrder.Language.StrongHomClass.map_rel {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] [self : FirstOrder.Language.StrongHomClass L F M N] (φ : 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 100]

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

Equations

• ⋯ = ⋯

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

Not an instance to avoid a loop.

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

instance FirstOrder.Language.Hom.instFunLike {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : FunLike (L.Hom 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'} [L.Structure M] [L.Structure N] : L.HomClass (L.Hom M N) M N

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance FirstOrder.Language.Hom.hasCoeToFun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : CoeFun (L.Hom M N) fun (x : L.Hom 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'} [L.Structure M] [L.Structure N] {f : L.Hom M N} : f.toFun = ⇑f

theorem FirstOrder.Language.Hom.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] ⦃f : L.Hom M N⦄ ⦃g : L.Hom 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'} [L.Structure M] [L.Structure N] {f : L.Hom M N} {g : L.Hom 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'} [L.Structure M] [L.Structure N] (φ : L.Hom 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'} [L.Structure M] [L.Structure N] (φ : L.Hom M N) (c : L.Constants) : φ ↑c = ↑c

@[simp]

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

def FirstOrder.Language.Hom.id (L : FirstOrder.Language) (M : Type w) [L.Structure M] : L.Hom 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.instInhabited {L : FirstOrder.Language} {M : Type w} [L.Structure M] : Inhabited (L.Hom M M)

Equations

• FirstOrder.Language.Hom.instInhabited = { default := FirstOrder.Language.Hom.id L M }

@[simp]

theorem FirstOrder.Language.Hom.id_apply {L : FirstOrder.Language} {M : Type w} [L.Structure 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'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.Hom N P) (hmn : L.Hom M N) : L.Hom M P

Composition of first-order homomorphisms.

Equations

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

@[simp]

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

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

Composition of first-order homomorphisms is associative.

@[simp]

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

@[simp]

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

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

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

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

theorem FirstOrder.Language.Embedding.map_fun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Embedding M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M) : φ (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'} [L.Structure M] [L.Structure N] (φ : L.Embedding M N) (c : L.Constants) : φ ↑c = ↑c

@[simp]

theorem FirstOrder.Language.Embedding.map_rel {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Embedding M N) {n : ℕ} (r : L.Relations n) (x : Fin n → M) : 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'} [L.Structure M] [L.Structure N] : L.Embedding M N → L.Hom M N

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

Equations

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

@[simp]

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

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

theorem FirstOrder.Language.Embedding.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] ⦃f : L.Embedding M N⦄ ⦃g : L.Embedding 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'} [L.Structure M] [L.Structure N] {f : L.Embedding M N} {g : L.Embedding 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'} [L.Structure M] [L.Structure N] : Function.Injective fun (x : L.Embedding M N) => x.toHom

@[simp]

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

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

@[simp]

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

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

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

Equations

• FirstOrder.Language.Embedding.ofInjective hf = { 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'} [L.Structure M] [L.Structure N] [L.IsAlgebraic] {f : L.Hom 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'} [L.Structure M] [L.Structure N] [L.IsAlgebraic] {f : L.Hom M N} (hf : Function.Injective ⇑f) : (FirstOrder.Language.Embedding.ofInjective hf).toHom = f

def FirstOrder.Language.Embedding.refl (L : FirstOrder.Language) (M : Type w) [L.Structure M] : L.Embedding 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.instInhabited {L : FirstOrder.Language} {M : Type w} [L.Structure M] : Inhabited (L.Embedding M M)

Equations

• FirstOrder.Language.Embedding.instInhabited = { default := FirstOrder.Language.Embedding.refl L M }

@[simp]

theorem FirstOrder.Language.Embedding.refl_apply {L : FirstOrder.Language} {M : Type w} [L.Structure 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'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.Embedding N P) (hmn : L.Embedding M N) : L.Embedding M P

Composition of first-order embeddings.

Equations

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

@[simp]

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

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

Composition of first-order embeddings is associative.

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.Embedding.refl_toHom {L : FirstOrder.Language} {M : Type w} [L.Structure M] : (FirstOrder.Language.Embedding.refl L M).toHom = 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} [L.Structure M] [L.Structure N] [FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N] : F → L.Embedding M N

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

Equations

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

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

Equations

• FirstOrder.Language.Equiv.instEquivLike = { coe := fun (f : L.Equiv M N) => f.toFun, inv := fun (f : L.Equiv M N) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

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

Equations

• ⋯ = ⋯

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

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

Equations

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

instance FirstOrder.Language.Equiv.hasCoeToFun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : CoeFun (L.Equiv M N) fun (x : L.Equiv 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'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : f.symm.symm = f

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.Equiv.map_fun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Equiv M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M) : φ (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'} [L.Structure M] [L.Structure N] (φ : L.Equiv M N) (c : L.Constants) : φ ↑c = ↑c

@[simp]

theorem FirstOrder.Language.Equiv.map_rel {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Equiv M N) {n : ℕ} (r : L.Relations n) (x : Fin n → M) : 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'} [L.Structure M] [L.Structure N] : L.Equiv M N → L.Embedding M N

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem FirstOrder.Language.Equiv.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] ⦃f : L.Equiv M N⦄ ⦃g : L.Equiv 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'} [L.Structure M] [L.Structure N] {f : L.Equiv M N} {g : L.Equiv M N} : f = g ↔ ∀ (x : M), f x = g x

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

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

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

def FirstOrder.Language.Equiv.refl (L : FirstOrder.Language) (M : Type w) [L.Structure M] : L.Equiv 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.instInhabited {L : FirstOrder.Language} {M : Type w} [L.Structure M] : Inhabited (L.Equiv M M)

Equations

• FirstOrder.Language.Equiv.instInhabited = { default := FirstOrder.Language.Equiv.refl L M }

@[simp]

theorem FirstOrder.Language.Equiv.refl_apply {L : FirstOrder.Language} {M : Type w} [L.Structure 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'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.Equiv N P) (hmn : L.Equiv M N) : L.Equiv M P

Composition of first-order equivalences.

Equations

• hnp.comp hmn = let __src := hmn.trans hnp.toEquiv; { toFun := ⇑hnp ∘ ⇑hmn, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_fun' := ⋯, map_rel' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Composition of first-order homomorphisms is associative.

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.Equiv.symm_comp_self {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : f.symm.comp 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'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) : f.symm.toEmbedding.comp f.toEmbedding = FirstOrder.Language.Embedding.refl L M

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

Equations

• FirstOrder.Language.StrongHomClass.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) [L₁.Structure S] [L₂.Structure S] : (L₁.sum L₂).Structure 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} [L₁.Structure S] [L₂.Structure 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} [L₁.Structure S] [L₂.Structure 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} [L₁.Structure S] [L₂.Structure 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} [L₁.Structure S] [L₂.Structure 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.empty.Structure M] [FirstOrder.Language.empty.Structure N] : Nonempty (FirstOrder.Language.empty.Embedding M N) ↔ Cardinal.lift.{w', w} (Cardinal.mk M) ≤ Cardinal.lift.{w, w'} (Cardinal.mk N)

@[simp]

theorem FirstOrder.Language.empty.nonempty_equiv_iff {M : Type w} {N : Type w'} [FirstOrder.Language.empty.Structure M] [FirstOrder.Language.empty.Structure N] : Nonempty (FirstOrder.Language.empty.Equiv 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.empty.Structure 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.empty.Structure M)

Equations

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

@[instance 100]

instance FirstOrder.Language.strongHomClassEmpty {F : Type u_3} {M : Type u_4} {N : Type u_5} [FunLike F M N] : FirstOrder.Language.empty.StrongHomClass 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.empty.Hom 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.empty.Embedding 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.empty.Equiv M N

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

A structure induced by a bijection.

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} [L.Structure M] (e : M ≃ N) : L.Equiv M N

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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