# 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:

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

Instances For
def FirstOrder.Sequence₂ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) :
Type u

Used to define FirstOrder.Language₂.

Equations
Instances For
instance FirstOrder.Sequence₂.inhabited₀ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) [h : ] :
Equations
instance FirstOrder.Sequence₂.inhabited₁ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) [h : ] :
Equations
instance FirstOrder.Sequence₂.inhabited₂ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) [h : ] :
Equations
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 : } :
@[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)) = + +
@[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 =
def FirstOrder.Language.mk₂ (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) :

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

Equations
Instances For

The empty language has no symbols.

Equations
Instances For

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 }
Instances For

The type of constants in a given language.

Equations
• L.Constants = L.Functions 0
Instances For
@[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

The type of symbols in a given language.

Equations
• L.Symbols = ((l : ) × L.Functions l (l : ) × L.Relations l)
Instances For

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

Equations
Instances For

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

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

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_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 : ] [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 : ] [h1 : ] [h2 : ] {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 : ] [h2 : ] {n : } :
Subsingleton ((FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Relations n)
Equations
• =
instance FirstOrder.Language.Countable.countable_functions {L : FirstOrder.Language} [h : Countable L.Symbols] :
Countable ((l : ) × L.Functions l)
Equations
• =
@[simp]
@[simp]
@[simp]
@[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 = + + + +
theorem FirstOrder.Language.Structure.ext {L : FirstOrder.Language} {M : Type w} (x : L.Structure M) (y : L.Structure M) (funMap : ) (RelMap : ) :
x = y
theorem FirstOrder.Language.Structure.ext_iff {L : FirstOrder.Language} {M : Type w} (x : L.Structure M) (y : L.Structure M) :
x = y
class FirstOrder.Language.Structure (L : FirstOrder.Language) (M : Type w) :
Type (max (max u v) w)

A first-order structure on a type M consists of interpretations of all the symbols in a given language. Each function of arity n is interpreted as a function sending tuples of length n (modeled as (Fin n → M)) to M, and a relation of arity n is a function from tuples of length n to Prop.

• funMap : {n : } → L.Functions n(Fin nM)M

Interpretation of the function symbols

• RelMap : {n : } → L.Relations n(Fin nM)Prop

Interpretation of the relation symbols

Instances

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

Equations
• = { funMap := fun {n : } => default, RelMap := fun {n : } => default }
Instances For

### 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 : MN

The underlying function of a homomorphism of structures

• map_fun' : ∀ {n : } (f : L.Functions n) (x : Fin nM), self.toFun = 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 nM), FirstOrder.Language.Structure.RelMap r (self.toFun x)

The homomorphism sends related elements to related elements

Instances For
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 nM) :
self.toFun = 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 nM) :

The homomorphism sends related elements to related elements

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
structure FirstOrder.Language.Embedding (L : FirstOrder.Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] extends :
Type (max w w')

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

Instances For
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 nM) :
self.toFun = 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 nM) :

The homomorphism sends related elements to related elements

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
structure FirstOrder.Language.Equiv (L : FirstOrder.Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] extends :
Type (max w w')

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

Instances For
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 nM) :
self.toFun = 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 nM) :

The homomorphism sends related elements to related elements

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def FirstOrder.Language.constantMap {L : FirstOrder.Language} {M : Type w} [L.Structure M] (c : L.Constants) :
M

Interpretation of a constant symbol

Equations
• c =
Instances For
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 0M} :
theorem FirstOrder.Language.nonempty_of_nonempty_constants {L : FirstOrder.Language} {M : Type w} [L.Structure M] [h : Nonempty L.Constants] :

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' : cM) (f₁' : f₁MM) (f₂' : f₂MMM) {n : } :
(FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Functions n(Fin nM)M

The function map for FirstOrder.Language.Structure₂.

Equations
• FirstOrder.Language.funMap₂ c' f₁' f₂' x✝ x = match x✝¹, x✝, x with | 0, f, x => c' f | 1, f, x => f₁' f (x 0) | 2, f, x => f₂' f (x 0) (x 1) | n.succ.succ.succ, f, x =>
Instances For
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₂MMProp) {n : } :
(FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Relations n(Fin nM)Prop

The relation map for FirstOrder.Language.Structure₂.

Equations
• FirstOrder.Language.RelMap₂ r₁' r₂' x✝ x = match x✝¹, x✝, x with | 0, r, x => | 1, r, x => x 0 r₁' r | 2, r, x => r₂' r (x 0) (x 1) | n.succ.succ.succ, r, x =>
Instances For
def FirstOrder.Language.Structure.mk₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (c' : cM) (f₁' : f₁MM) (f₂' : f₂MMM) (r₁' : r₁Set M) (r₂' : r₂MMProp) :
(FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Structure M

A structure constructor to match FirstOrder.Language₂.

Equations
Instances For
@[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' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (c₀ : c) {x : Fin 0M} :
= 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' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (f : f₁) (x : M) :
= 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' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (f : f₂) (x : M) (y : M) :
= 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' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (r : r₁) (x : M) :
= (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' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (r : r₂) (x : M) (y : M) :
= r₂' r x y
class FirstOrder.Language.HomClass (F : Type u_3) (M : Type u_4) (N : Type u_5) [FunLike F M N] :

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

The homomorphism commutes with the interpretations of the function symbols

• map_rel : ∀ (φ : F) {n : } (r : L.Relations n) (x : Fin nM),

The homomorphism sends related elements to related elements

Instances
theorem FirstOrder.Language.HomClass.map_fun {F : Type u_3} {M : Type u_4} {N : Type u_5} [FunLike F M N] [self : ] (φ : F) {n : } (f : L.Functions n) (x : Fin nM) :

The homomorphism commutes with the interpretations of the function symbols

theorem FirstOrder.Language.HomClass.map_rel {F : Type u_3} {M : Type u_4} {N : Type u_5} [FunLike F M N] [self : ] (φ : F) {n : } (r : L.Relations n) (x : Fin nM) :

The homomorphism sends related elements to related elements

class FirstOrder.Language.StrongHomClass (F : Type u_3) (M : Type u_4) (N : Type u_5) [FunLike F M N] :

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

The homomorphism commutes with the interpretations of the function symbols

• map_rel : ∀ (φ : F) {n : } (r : L.Relations n) (x : Fin nM),

The homomorphism sends related elements to related elements

Instances
theorem FirstOrder.Language.StrongHomClass.map_fun {F : Type u_3} {M : Type u_4} {N : Type u_5} [FunLike F M N] [self : ] (φ : F) {n : } (f : L.Functions n) (x : Fin nM) :

The homomorphism commutes with the interpretations of the function symbols

theorem FirstOrder.Language.StrongHomClass.map_rel {F : Type u_3} {M : Type u_4} {N : Type u_5} [FunLike F M N] [self : ] (φ : F) {n : } (r : L.Relations n) (x : Fin nM) :

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) => MN
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 nM) :
@[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 nM) :
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
• = { toFun := fun (m : M) => m, map_fun' := , map_rel' := }
Instances For
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 := }
@[simp]
theorem FirstOrder.Language.Hom.id_apply {L : FirstOrder.Language} {M : Type w} [L.Structure M] (x : 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' := }
Instances For
@[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 = 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) :
.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] :
FL.Hom M N

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

Equations
• = { toFun := φ, map_fun' := , map_rel' := }
Instances For
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 nM) :
@[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 nM) :
def FirstOrder.Language.Embedding.toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
L.Embedding M NL.Hom M N

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

Equations
• FirstOrder.Language.Embedding.toHom = FirstOrder.Language.HomClass.toHom
Instances For
@[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) :
@[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 : ) :
∀ (a : M),
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 : ) :
L.Embedding M N

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

Equations
• = { toFun := f.toFun, inj' := hf, map_fun' := , map_rel' := }
Instances For
@[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 : ) :
@[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 : ) :
.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
• = { toEmbedding := , map_fun' := , map_rel' := }
Instances For
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 := }
@[simp]
theorem FirstOrder.Language.Embedding.refl_apply {L : FirstOrder.Language} {M : Type w} [L.Structure M] (x : M) :
= 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' := }
Instances For
@[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) :
@[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 = 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) :
.comp f = f
@[simp]
theorem FirstOrder.Language.Embedding.refl_toHom {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
.toHom =
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] [] [L.StrongHomClass F M N] :
FL.Embedding M N

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

Equations
• = { toFun := φ, inj' := , map_fun' := , map_rel' := }
Instances For
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' := }
Instances For
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) => MN
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 nM) :
@[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 nM) :
def FirstOrder.Language.Equiv.toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
L.Equiv M NL.Embedding M N

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

Equations
• FirstOrder.Language.Equiv.toEmbedding = FirstOrder.Language.StrongHomClass.toEmbedding
Instances For
def FirstOrder.Language.Equiv.toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
L.Equiv M NL.Hom M N

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

Equations
• FirstOrder.Language.Equiv.toHom = FirstOrder.Language.HomClass.toHom
Instances For
@[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) :
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) :
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) :
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
• = { toEquiv := , map_fun' := , map_rel' := }
Instances For
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 := }
@[simp]
theorem FirstOrder.Language.Equiv.refl_apply {L : FirstOrder.Language} {M : Type w} [L.Structure M] (x : M) :
= 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' := }
Instances For
@[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 = 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) :
.comp g = g
@[simp]
theorem FirstOrder.Language.Equiv.refl_toEmbedding {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
.toEmbedding =
@[simp]
theorem FirstOrder.Language.Equiv.refl_toHom {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
.toHom =
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) :
@[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 =
@[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 =
@[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 =
@[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 =
@[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 =
@[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 =
@[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] :
FL.Equiv M N

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

Equations
• = { toFun := φ, invFun := , left_inv := , right_inv := , map_fun' := , map_rel' := }
Instances For
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) :
@[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) :
@[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) :
@[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) :
Equations
• FirstOrder.Language.emptyStructure = { funMap := fun {n : } => Empty.elim, RelMap := fun {n : } => Empty.elim }
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 : MN) :
∀ (a : M), a = f a
def Function.emptyHom {M : Type w} {N : Type w'} (f : MN) :

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

Equations
• = { toFun := f, map_fun' := , map_rel' := }
Instances For
def Embedding.empty {M : Type w} {N : Type w'} (f : M N) :

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

Equations
• = { toEmbedding := f, map_fun' := , map_rel' := }
Instances For
@[simp]
theorem FirstOrder.Language.toFun_embedding_empty {M : Type w} {N : Type w'} (f : M N) :
() = f
@[simp]
theorem FirstOrder.Language.toEmbedding_embedding_empty {M : Type w} {N : Type w'} (f : M N) :
().toEmbedding = f
def Equiv.empty {M : Type w} {N : Type w'} (f : M N) :
M N

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

Equations
• f.empty = { toEquiv := f, map_fun' := , map_rel' := }
Instances For
@[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 nN), = 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 nN), = 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.
Instances For
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' := }
Instances For
@[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