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 #

source

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

Instances For

source

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}

Instances For

source

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

source

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

source

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

source

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

IsEmpty (FirstOrder.Sequence₂ a₀ a₁ a₂ (n + 3))

Equations

(_ : IsEmpty (FirstOrder.Sequence₂ a₀ a₁ a₂ (n + 3))) = (_ : IsEmpty PEmpty.{u + 1} )

source

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

source

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

source

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

source

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

source

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

Instances For

source

def FirstOrder.Language.empty :

FirstOrder.Language

The empty language has no symbols.

Equations

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

Instances For

source

instance FirstOrder.Language.instInhabitedLanguage :

Inhabited FirstOrder.Language

Equations

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

source

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 }

Instances For

source

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

Instances For

source

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

source

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)

Instances For

source

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)

Instances For

source

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.

Instances

source

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.

Instances

source

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

source

instance FirstOrder.Language.instIsEmptyFunctions {L : FirstOrder.Language} [FirstOrder.Language.IsRelational L] {n : ℕ} :

IsEmpty (L.Functions n)

Equations

(_ : IsEmpty (L.Functions n)) = (_ : IsEmpty (L.Functions n))

source

instance FirstOrder.Language.instIsEmptyRelations {L : FirstOrder.Language} [FirstOrder.Language.IsAlgebraic L] {n : ℕ} :

IsEmpty (L.Relations n)

Equations

(_ : IsEmpty (L.Relations n)) = (_ : IsEmpty (L.Relations n))

source

instance FirstOrder.Language.isRelational_of_empty_functions {symb : ℕ → Type u_1} :

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

Equations

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

source

instance FirstOrder.Language.isAlgebraic_of_empty_relations {symb : ℕ → Type u_1} :

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

Equations

(_ : FirstOrder.Language.IsAlgebraic { Functions := symb, Relations := fun (x : ℕ) => Empty }) = (_ : FirstOrder.Language.IsAlgebraic { Functions := symb, Relations := fun (x : ℕ) => Empty })

source

instance FirstOrder.Language.isRelational_empty :

FirstOrder.Language.IsRelational FirstOrder.Language.empty

Equations

FirstOrder.Language.isRelational_empty = (_ : FirstOrder.Language.IsRelational { Functions := fun (x : ℕ) => Empty, Relations := fun (x : ℕ) => Empty })

source

instance FirstOrder.Language.isAlgebraic_empty :

FirstOrder.Language.IsAlgebraic FirstOrder.Language.empty

Equations

FirstOrder.Language.isAlgebraic_empty = (_ : FirstOrder.Language.IsAlgebraic { Functions := fun (x : ℕ) => Empty, Relations := fun (x : ℕ) => Empty })

source

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

(_ : FirstOrder.Language.IsRelational (FirstOrder.Language.sum L L')) = (_ : FirstOrder.Language.IsRelational (FirstOrder.Language.sum L L'))

source

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

(_ : FirstOrder.Language.IsAlgebraic (FirstOrder.Language.sum L L')) = (_ : FirstOrder.Language.IsAlgebraic (FirstOrder.Language.sum L L'))

source

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

(_ : FirstOrder.Language.IsRelational (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂)) = (_ : FirstOrder.Language.IsRelational (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂))

source

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

(_ : FirstOrder.Language.IsAlgebraic (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂)) = (_ : FirstOrder.Language.IsAlgebraic (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂))

source

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

(_ : Subsingleton ((FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Functions n)) = (_ : Subsingleton ((FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Functions n))

source

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

(_ : Subsingleton ((FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Relations n)) = (_ : Subsingleton ((FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Relations n))

source

@[simp]

theorem FirstOrder.Language.empty_card :

FirstOrder.Language.card FirstOrder.Language.empty = 0

source

instance FirstOrder.Language.isEmpty_empty :

IsEmpty (FirstOrder.Language.Symbols FirstOrder.Language.empty)

Equations

FirstOrder.Language.isEmpty_empty = (_ : IsEmpty (FirstOrder.Language.Symbols FirstOrder.Language.empty))

source

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

Countable ((l : ℕ) × L.Functions l)

Equations

(_ : Countable ((l : ℕ) × L.Functions l)) = (_ : Countable ((l : ℕ) × L.Functions l))

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances

source

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 }

Instances For

Maps #

source

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

Instances For

source

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

Lean.TrailingParserDescr

Equations

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

Instances For

source

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

Instances For

source

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.

Instances For

source

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

Instances For

source

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.

Instances For

source

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

Interpretation of a constant symbol

Equations

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

Instances For

source

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 }

source

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

source

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.

source

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.

Instances For

source

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.

Instances For

source

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₂' }

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

Instances

source

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

Instances

source

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

(_ : FirstOrder.Language.HomClass L F M N) = (_ : FirstOrder.Language.HomClass L F M N)

source

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.

source

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

source

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' := (_ : ∀ (f g : FirstOrder.Language.Hom L M N), f.toFun = g.toFun → f = g) }