# mathlib3documentation

model_theory.language_map

# Language Maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. Maps between first-order languages in the style of the Flypitch project, as well as several important maps between structures.

## Main Definitions #

• A first_order.language.Lhom, denoted L →ᴸ L', is a map between languages, sending the symbols of one to symbols of the same kind and arity in the other.
• A first_order.language.Lequiv, denoted L ≃ᴸ L', is an invertible language homomorphism.
• first_order.language.with_constants is defined so that if M is an L.Structure and A : set M, L.with_constants A, denoted L[[A]], is a language which adds constant symbols for elements of A to L.

## References #

For the Flypitch project:

structure first_order.language.Lhom (L : first_order.language) (L' : first_order.language) :
Type (max u u' v v')

A language homomorphism maps the symbols of one language to symbols of another.

Instances for first_order.language.Lhom
@[protected]
def first_order.language.Lhom.mk₂ {L' : first_order.language} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} (φ₀ : c L'.constants) (φ₁ : f₁ L'.functions 1) (φ₂ : f₂ L'.functions 2) (φ₁' : r₁ L'.relations 1) (φ₂' : r₂ L'.relations 2) :
f₂ r₁ r₂ →ᴸ L'

Defines a map between languages defined with language.mk₂.

Equations

Pulls a structure back along a language map.

Equations
@[protected]

The identity language homomorphism.

Equations
Instances for first_order.language.Lhom.id
@[protected, instance]
Equations
@[protected]

The inclusion of the left factor into the sum of two languages.

Equations
Instances for first_order.language.Lhom.sum_inl
@[protected]

The inclusion of the right factor into the sum of two languages.

Equations
Instances for first_order.language.Lhom.sum_inr
@[protected]

The inclusion of an empty language into any other language.

Equations
Instances for first_order.language.Lhom.of_is_empty
@[protected, ext]
theorem first_order.language.Lhom.mk₂_funext {L' : first_order.language} {c f₁ f₂ : Type u} {r₁ r₂ : Type v} {F G : f₂ r₁ r₂ →ᴸ L'} (h0 : (c_1 : f₂ r₁ r₂).constants), F.on_function c_1 = G.on_function c_1) (h1 : (f : f₂ r₁ r₂).functions 1), F.on_function f = G.on_function f) (h2 : (f : f₂ r₁ r₂).functions 2), F.on_function f = G.on_function f) (h1' : (r : f₂ r₁ r₂).relations 1), F.on_relation r = G.on_relation r) (h2' : (r : f₂ r₁ r₂).relations 2), F.on_relation r = G.on_relation r) :
F = G

The composition of two language homomorphisms.

Equations
theorem first_order.language.Lhom.comp_assoc {L : first_order.language} {L' : first_order.language} {L'' : first_order.language} {L3 : first_order.language} (F : L'' →ᴸ L3) (G : L' →ᴸ L'') (H : L →ᴸ L') :
(F.comp G).comp H = F.comp (G.comp H)
@[protected]

A language map defined on two factors of a sum.

Equations
Instances for first_order.language.Lhom.sum_elim
@[simp]
theorem first_order.language.Lhom.sum_elim_on_relation {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L'' : first_order.language} (ψ : L'' →ᴸ L') (n : ) (ᾰ : L.relations n L''.relations n) :
(ϕ.sum_elim ψ).on_relation = sum.elim (λ (f : L.relations n), ϕ.on_relation f) (λ (f : L''.relations n), ψ.on_relation f)
@[simp]
theorem first_order.language.Lhom.sum_elim_on_function {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L'' : first_order.language} (ψ : L'' →ᴸ L') (n : ) (ᾰ : L.functions n L''.functions n) :
(ϕ.sum_elim ψ).on_function = sum.elim (λ (f : L.functions n), ϕ.on_function f) (λ (f : L''.functions n), ψ.on_function f)
theorem first_order.language.Lhom.comp_sum_elim {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L'' : first_order.language} (ψ : L'' →ᴸ L') {L3 : first_order.language} (θ : L' →ᴸ L3) :
θ.comp (ϕ.sum_elim ψ) = (θ.comp ϕ).sum_elim (θ.comp ψ)
@[simp]
theorem first_order.language.Lhom.sum_map_on_relation {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L₁ : first_order.language} {L₂ : first_order.language} (ψ : L₁ →ᴸ L₂) (n : ) (ᾰ : L.relations n L₁.relations n) :
(ϕ.sum_map ψ).on_relation = sum.map (λ (f : L.relations n), ϕ.on_relation f) (λ (f : L₁.relations n), ψ.on_relation f)
@[simp]
theorem first_order.language.Lhom.sum_map_on_function {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L₁ : first_order.language} {L₂ : first_order.language} (ψ : L₁ →ᴸ L₂) (n : ) (ᾰ : L.functions n L₁.functions n) :
(ϕ.sum_map ψ).on_function = sum.map (λ (f : L.functions n), ϕ.on_function f) (λ (f : L₁.functions n), ψ.on_function f)
def first_order.language.Lhom.sum_map {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L₁ : first_order.language} {L₂ : first_order.language} (ψ : L₁ →ᴸ L₂) :
L.sum L₁ →ᴸ L'.sum L₂

The map between two sum-languages induced by maps on the two factors.

Equations
Instances for first_order.language.Lhom.sum_map

A language homomorphism is injective when all the maps between symbol types are.

noncomputable def first_order.language.Lhom.default_expansion {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') [Π (n : ) (f : L'.functions n), decidable (f set.range (λ (f : L.functions n), ϕ.on_function f))] [Π (n : ) (r : L'.relations n), decidable (r set.range (λ (r : L.relations n), ϕ.on_relation r))] (M : Type u_1) [inhabited M] [L.Structure M] :

Pulls a L-structure along a language map ϕ : L →ᴸ L', and then expands it to an L'-structure arbitrarily.

Equations
@[class]
structure first_order.language.Lhom.is_expansion_on {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') (M : Type u_3) [L.Structure M] [L'.Structure M] :
Prop

A language homomorphism is an expansion on a structure if it commutes with the interpretation of all symbols on that structure.

Instances of this typeclass
@[simp]
theorem first_order.language.Lhom.map_on_function {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {M : Type u_1} [L.Structure M] [L'.Structure M] [ϕ.is_expansion_on M] {n : } (f : L.functions n) (x : fin n M) :
@[simp]
theorem first_order.language.Lhom.map_on_relation {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {M : Type u_1} [L.Structure M] [L'.Structure M] [ϕ.is_expansion_on M] {n : } (R : L.relations n) (x : fin n M) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem first_order.language.Lhom.fun_map_sum_inl {L : first_order.language} {L' : first_order.language} {M : Type w} [L.Structure M] [(L.sum L').Structure M] {n : } {f : L.functions n} {x : fin n M} :
@[simp]
theorem first_order.language.Lhom.fun_map_sum_inr {L : first_order.language} {L' : first_order.language} {M : Type w} [L.Structure M] [(L'.sum L).Structure M] {n : } {f : L.functions n} {x : fin n M} :
@[protected, instance]
theorem first_order.language.Lhom.injective.is_expansion_on_default {L : first_order.language} {L' : first_order.language} {ϕ : L →ᴸ L'} [Π (n : ) (f : L'.functions n), decidable (f set.range (λ (f : L.functions n), ϕ.on_function f))] [Π (n : ) (r : L'.relations n), decidable (r set.range (λ (r : L.relations n), ϕ.on_relation r))] (h : ϕ.injective) (M : Type u_1) [inhabited M] [L.Structure M] :
structure first_order.language.Lequiv (L : first_order.language) (L' : first_order.language) :
Type (max u_1 u_2 u_3 u_4)

A language equivalence maps the symbols of one language to symbols of another bijectively.

Instances for first_order.language.Lequiv
@[simp]
@[protected]

The identity equivalence from a first-order language to itself.

Equations
@[simp]
@[protected, instance]
Equations
@[protected]

The inverse of an equivalence of first-order languages.

Equations
@[protected, trans]

The composition of equivalences of first-order languages.

Equations
@[simp]

A language with constants indexed by a type.

Equations
Instances for first_order.language.constants_on
@[protected, instance]
@[protected, instance]
@[protected, instance]
def first_order.language.constants_on.Structure {M : Type w} {α : Type u'} (f : α M) :

Gives a constants_on α structure to a type by assigning each constant a value.

Equations
def first_order.language.Lhom.constants_on_map {α : Type u'} {β : Type v'} (f : α β) :

A map between index types induces a map between constant languages.

Equations
Instances for first_order.language.Lhom.constants_on_map
theorem first_order.language.constants_on_map_is_expansion_on {M : Type w} {α : Type u'} {β : Type v'} {f : α β} {fα : α M} {fβ : β M} (h : f = fα) :

Extends a language with a constant for each element of a parameter set in M.

Equations
Instances for first_order.language.with_constants
@[simp]
@[simp]

Equations
Instances for first_order.language.Lhom_with_constants
@[protected]

The constant symbol indexed by a particular element.

Equations

Adds constants to a language map.

Equations
Instances for first_order.language.Lhom.add_constants
@[protected, instance]
def first_order.language.params_Structure (α : Type w') (A : set α) :
Equations
@[simp]

The language map removing an empty constant set.

Equations
@[simp]
theorem first_order.language.with_constants_fun_map_sum_inl (L : first_order.language) {M : Type w} [L.Structure M] {α : Type w'} [(L.with_constants α).Structure M] [ M] {n : } {f : L.functions n} {x : fin n M} :
@[simp]
theorem first_order.language.with_constants_rel_map_sum_inl (L : first_order.language) {M : Type w} [L.Structure M] {α : Type w'} [(L.with_constants α).Structure M] [ M] {n : } {R : L.relations n} {x : fin n M} :

The language map extending the constant set.

Equations
Instances for first_order.language.Lhom_with_constants_map
@[simp]
theorem first_order.language.Lhom.map_constants_comp_sum_inl (L : first_order.language) {α : Type w'} {β : Type u_1} {f : α β} :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem first_order.language.with_constants_fun_map_sum_inr (L : first_order.language) {M : Type w} [L.Structure M] (α : Type u_1) {a : α} {x : fin 0 M} :
= (L.con a)
@[simp]
theorem first_order.language.coe_con (L : first_order.language) {M : Type w} [L.Structure M] (A : set M) {a : A} :
(L.con a) = a
@[protected, instance]
@[protected, instance]