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

@[reducible, inline]

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

A language is relational when it has no function symbols.

Equations

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

@[reducible, inline]

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

A language is algebraic when it has no relation symbols.

Equations

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

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.instemptyIsAlgebraic : FirstOrder.Language.empty.IsAlgebraic

Equations

• ⋯ = instIsEmptyEmpty

instance FirstOrder.Language.instemptyIsRelational : FirstOrder.Language.empty.IsRelational

Equations

• ⋯ = instIsEmptyEmpty

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 }

@[reducible, inline]

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

The type of constants in a given language.

Equations

• L.Constants = L.Functions 0

@[reducible, inline]

abbrev 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

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

• ⋯ = ⋯

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

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

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

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

Equations

• FirstOrder.Language.instDecidableEqFunctions n = inferInstance

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

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

Equations

• FirstOrder.Language.instDecidableEqRelations n = inferInstance

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

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

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.

class FirstOrder.Language.HomClass (L : outParam FirstOrder.Language) (F : Type u_3) (M : outParam (Type u_4)) (N : outParam (Type u_5)) [FunLike F M 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 : outParam (Type u_4)} {N : outParam (Type u_5)} : ∀ {inst : FunLike F M N} {inst_1 : FirstOrder.Language.Structure L M} {inst_2 : 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 : outParam (Type u_4)} {N : outParam (Type u_5)} : ∀ {inst : FunLike F M N} {inst_1 : FirstOrder.Language.Structure L M} {inst_2 : 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 : outParam (Type u_4)) (N : outParam (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 : outParam (Type u_4)} {N : outParam (Type u_5)} : ∀ {inst : FunLike F M N} {inst_1 : FirstOrder.Language.Structure L M} {inst_2 : 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 : outParam (Type u_4)} {N : outParam (Type u_5)} : ∀ {inst : FunLike F M N} {inst_1 : FirstOrder.Language.Structure L M} {inst_2 : 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

• ⋯ = ⋯

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

@[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' := ⋯ }

@[simp]

theorem FirstOrder.Language.HomClass.toHom_toFun {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] : ∀ (a : F) (a_1 : M), (FirstOrder.Language.HomClass.toHom a) a_1 = a a_1

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

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

@[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' := ⋯ }

@[simp]

theorem FirstOrder.Language.StrongHomClass.toEmbedding_toFun {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] : ∀ (a : F) (a_1 : M), (FirstOrder.Language.StrongHomClass.toEmbedding a) a_1 = a a_1

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 = { toEquiv := f.symm, map_fun' := ⋯, map_rel' := ⋯ }

@[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.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 = { toFun := ⇑hnp ∘ ⇑hmn, invFun := (hmn.trans hnp.toEquiv).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' := ⋯ }

@[simp]

theorem FirstOrder.Language.StrongHomClass.toEquiv_toFun {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] : ∀ (a : F) (a_1 : M), (FirstOrder.Language.StrongHomClass.toEquiv a) a_1 = a a_1

@[simp]

theorem FirstOrder.Language.StrongHomClass.toEquiv_invFun {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] : ∀ (a : F) (a_1 : N), (FirstOrder.Language.StrongHomClass.toEquiv a).invFun a_1 = EquivLike.inv a a_1

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

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

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

Equations

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

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 {M : Type w} {N : Type w'} [FirstOrder.Language.empty.Structure M] [FirstOrder.Language.empty.Structure N] {F : Type u_3} [FunLike F M N] : FirstOrder.Language.empty.StrongHomClass F M N

Equations

• ⋯ = ⋯

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

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

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

Equations

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

@[simp]

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

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.

@[simp]

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

@[simp]

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

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

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

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