mathlib documentation

model_theory.language_map

Language Maps #

Maps between first-order languages in the style of the Flypitch project, as well as several important maps between structures.

Main Definitions #

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) :
first_order.language.mk₂ c f₁ f₂ r₁ r₂ →ᴸ L'

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

Equations
def first_order.language.Lhom.reduct {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') (M : Type u_1) [L'.Structure M] :

Pulls a structure back along a language map.

Equations
@[protected]

The identity language homomorphism.

Equations
Instances for first_order.language.Lhom.id
@[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 : first_order.language.mk₂ c f₁ f₂ r₁ r₂ →ᴸ L'} (h0 : ∀ (c_1 : (first_order.language.mk₂ c f₁ f₂ r₁ r₂).constants), F.on_function c_1 = G.on_function c_1) (h1 : ∀ (f : (first_order.language.mk₂ c f₁ f₂ r₁ r₂).functions 1), F.on_function f = G.on_function f) (h2 : ∀ (f : (first_order.language.mk₂ c f₁ f₂ r₁ r₂).functions 2), F.on_function f = G.on_function f) (h1' : ∀ (r : (first_order.language.mk₂ c f₁ f₂ r₁ r₂).relations 1), F.on_relation r = G.on_relation r) (h2' : ∀ (r : (first_order.language.mk₂ c f₁ 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
@[protected, instance]
@[protected, instance]
def first_order.language.Lhom.sum_map_is_expansion_on {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L₁ : first_order.language} {L₂ : first_order.language} (ψ : L₁ →ᴸ L₂) (M : Type u_5) [L.Structure M] [L'.Structure M] [L₁.Structure M] [L₂.Structure M] [ϕ.is_expansion_on M] [ψ.is_expansion_on 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
@[protected]

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

Equations
@[protected]

The inverse of an equivalence of first-order languages.

Equations
@[protected, trans]

The composition of equivalences of first-order languages.

Equations
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

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
@[protected]
def first_order.language.con (L : first_order.language) {α : Type w'} (a : α) :

The constant symbol indexed by a particular element.

Equations

Adds constants to a language map.

Equations
Instances for first_order.language.Lhom.add_constants
def first_order.language.Lhom_with_constants_map (L : first_order.language) {α : Type w'} {β : Type u_1} (f : α → β) :

The language map extending the constant set.

Equations
Instances for first_order.language.Lhom_with_constants_map
@[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