mathlib3 documentation

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 #

References #

For the Flypitch project:

source
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
source
@[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
source
def first_order.language.Lhom.reduct {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') (M : Type u_1) [L'.Structure M] :
L.Structure M

Pulls a structure back along a language map.

Equations
source
@[protected]
def first_order.language.Lhom.id (L : first_order.language) :
L →ᴸ L

The identity language homomorphism.

Equations
Instances for first_order.language.Lhom.id
source
@[simp]
theorem first_order.language.Lhom.id_on_function (L : first_order.language) (n : ℕ) (a : L.functions n) :
(first_order.language.Lhom.id L).on_function a = id a
source
@[simp]
theorem first_order.language.Lhom.id_on_relation (L : first_order.language) (n : ℕ) (a : L.relations n) :
(first_order.language.Lhom.id L).on_relation a = id a
source
@[protected, instance]
def first_order.language.Lhom.inhabited {L : first_order.language} :
inhabited (L →ᴸ L)
Equations
source
@[protected]
def first_order.language.Lhom.sum_inl {L : first_order.language} {L' : first_order.language} :
L →ᴸ L.sum L'

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

Equations
Instances for first_order.language.Lhom.sum_inl
source
@[simp]
theorem first_order.language.Lhom.sum_inl_on_function {L : first_order.language} {L' : first_order.language} (n : ℕ) (val : L.functions n) :
first_order.language.Lhom.sum_inl.on_function val = sum.inl val
source
@[simp]
theorem first_order.language.Lhom.sum_inl_on_relation {L : first_order.language} {L' : first_order.language} (n : ℕ) (val : L.relations n) :
first_order.language.Lhom.sum_inl.on_relation val = sum.inl val
source
@[simp]
theorem first_order.language.Lhom.sum_inr_on_function {L : first_order.language} {L' : first_order.language} (n : ℕ) (val : L'.functions n) :
first_order.language.Lhom.sum_inr.on_function val = sum.inr val
source
@[protected]
def first_order.language.Lhom.sum_inr {L : first_order.language} {L' : first_order.language} :
L' →ᴸ L.sum L'

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

Equations
Instances for first_order.language.Lhom.sum_inr
source
@[simp]
theorem first_order.language.Lhom.sum_inr_on_relation {L : first_order.language} {L' : first_order.language} (n : ℕ) (val : L'.relations n) :
first_order.language.Lhom.sum_inr.on_relation val = sum.inr val
source
@[simp]
theorem first_order.language.Lhom.of_is_empty_on_function (L : first_order.language) (L' : first_order.language) [L.is_algebraic] [L.is_relational] (n : ℕ) (a : L.functions n) :
(first_order.language.Lhom.of_is_empty L L').on_function a = _.elim a
source
@[protected]
def first_order.language.Lhom.of_is_empty (L : first_order.language) (L' : first_order.language) [L.is_algebraic] [L.is_relational] :
L →ᴸ L'

The inclusion of an empty language into any other language.

Equations
Instances for first_order.language.Lhom.of_is_empty
source
@[simp]
theorem first_order.language.Lhom.of_is_empty_on_relation (L : first_order.language) (L' : first_order.language) [L.is_algebraic] [L.is_relational] (n : ℕ) (a : L.relations n) :
(first_order.language.Lhom.of_is_empty L L').on_relation a = _.elim a
source
@[protected, ext]
theorem first_order.language.Lhom.funext {L : first_order.language} {L' : first_order.language} {F G : L →ᴸ L'} (h_fun : F.on_function = G.on_function) (h_rel : F.on_relation = G.on_relation) :
F = G
source
@[protected, instance]
def first_order.language.Lhom.unique {L : first_order.language} {L' : first_order.language} [L.is_algebraic] [L.is_relational] :
unique (L →ᴸ L')
Equations
source
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
source
@[simp]
theorem first_order.language.Lhom.comp_on_relation {L : first_order.language} {L' : first_order.language} {L'' : first_order.language} (g : L' →ᴸ L'') (f : L →ᴸ L') (_x : ℕ) (R : L.relations _x) :
(g.comp f).on_relation R = g.on_relation (f.on_relation R)
source
@[simp]
theorem first_order.language.Lhom.comp_on_function {L : first_order.language} {L' : first_order.language} {L'' : first_order.language} (g : L' →ᴸ L'') (f : L →ᴸ L') (n : ℕ) (F : L.functions n) :
(g.comp f).on_function F = g.on_function (f.on_function F)
source
def first_order.language.Lhom.comp {L : first_order.language} {L' : first_order.language} {L'' : first_order.language} (g : L' →ᴸ L'') (f : L →ᴸ L') :
L →ᴸ L''

The composition of two language homomorphisms.

Equations
source
@[simp]
theorem first_order.language.Lhom.id_comp {L : first_order.language} {L' : first_order.language} (F : L →ᴸ L') :
(first_order.language.Lhom.id L').comp F = F
source
@[simp]
theorem first_order.language.Lhom.comp_id {L : first_order.language} {L' : first_order.language} (F : L →ᴸ L') :
F.comp (first_order.language.Lhom.id L) = F
source
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)
source
@[protected]
def first_order.language.Lhom.sum_elim {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L'' : first_order.language} (ψ : L'' →ᴸ L') :
L.sum L'' →ᴸ L'

A language map defined on two factors of a sum.

Equations
Instances for first_order.language.Lhom.sum_elim
source
@[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) ᾰ
source
@[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) ᾰ
source
theorem first_order.language.Lhom.sum_elim_comp_inl {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L'' : first_order.language} (ψ : L'' →ᴸ L') :
(ϕ.sum_elim ψ).comp first_order.language.Lhom.sum_inl = ϕ
source
theorem first_order.language.Lhom.sum_elim_comp_inr {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L'' : first_order.language} (ψ : L'' →ᴸ L') :
(ϕ.sum_elim ψ).comp first_order.language.Lhom.sum_inr = ψ
source
theorem first_order.language.Lhom.sum_elim_inl_inr {L : first_order.language} {L' : first_order.language} :
first_order.language.Lhom.sum_inl.sum_elim first_order.language.Lhom.sum_inr = first_order.language.Lhom.id (L.sum L')
source
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 ψ)
source
@[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) ᾰ
source
@[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) ᾰ
source
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
source
@[simp]
theorem first_order.language.Lhom.sum_map_comp_inl {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L₁ : first_order.language} {L₂ : first_order.language} (ψ : L₁ →ᴸ L₂) :
(ϕ.sum_map ψ).comp first_order.language.Lhom.sum_inl = first_order.language.Lhom.sum_inl.comp ϕ
source
@[simp]
theorem first_order.language.Lhom.sum_map_comp_inr {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L₁ : first_order.language} {L₂ : first_order.language} (ψ : L₁ →ᴸ L₂) :
(ϕ.sum_map ψ).comp first_order.language.Lhom.sum_inr = first_order.language.Lhom.sum_inr.comp ψ
source
structure first_order.language.Lhom.injective {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') :
Prop

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

source
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] :
L'.Structure M

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

Equations
source
@[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
source
@[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) :
first_order.language.Structure.fun_map (ϕ.on_function f) x = first_order.language.Structure.fun_map f x
source
@[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) :
first_order.language.Structure.rel_map (ϕ.on_relation R) x = first_order.language.Structure.rel_map R x
source
@[protected, instance]
def first_order.language.Lhom.id_is_expansion_on {L : first_order.language} (M : Type u_1) [L.Structure M] :
(first_order.language.Lhom.id L).is_expansion_on M
source
@[protected, instance]
def first_order.language.Lhom.of_is_empty_is_expansion_on {L : first_order.language} {L' : first_order.language} (M : Type u_1) [L.Structure M] [L'.Structure M] [L.is_algebraic] [L.is_relational] :
(first_order.language.Lhom.of_is_empty L L').is_expansion_on M
source
@[protected, instance]
def first_order.language.Lhom.sum_elim_is_expansion_on {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') {L'' : first_order.language} (ψ : L'' →ᴸ L') (M : Type u_3) [L.Structure M] [L'.Structure M] [L''.Structure M] [ϕ.is_expansion_on M] [ψ.is_expansion_on M] :
(ϕ.sum_elim ψ).is_expansion_on M
source
@[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] :
(ϕ.sum_map ψ).is_expansion_on M
source
@[protected, instance]
def first_order.language.Lhom.sum_inl_is_expansion_on {L : first_order.language} {L' : first_order.language} (M : Type u_1) [L.Structure M] [L'.Structure M] :
first_order.language.Lhom.sum_inl.is_expansion_on M
source
@[protected, instance]
def first_order.language.Lhom.sum_inr_is_expansion_on {L : first_order.language} {L' : first_order.language} (M : Type u_1) [L.Structure M] [L'.Structure M] :
first_order.language.Lhom.sum_inr.is_expansion_on M
source
@[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] [first_order.language.Lhom.sum_inl.is_expansion_on M] {n : ℕ} {f : L.functions n} {x : fin n → M} :
first_order.language.Structure.fun_map (sum.inl f) x = first_order.language.Structure.fun_map f x
source
@[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] [first_order.language.Lhom.sum_inr.is_expansion_on M] {n : ℕ} {f : L.functions n} {x : fin n → M} :
first_order.language.Structure.fun_map (sum.inr f) x = first_order.language.Structure.fun_map f x
source
theorem first_order.language.Lhom.sum_inl_injective {L : first_order.language} {L' : first_order.language} :
first_order.language.Lhom.sum_inl.injective
source
theorem first_order.language.Lhom.sum_inr_injective {L : first_order.language} {L' : first_order.language} :
first_order.language.Lhom.sum_inr.injective
source
@[protected, instance]
def first_order.language.Lhom.is_expansion_on_reduct {L : first_order.language} {L' : first_order.language} (ϕ : L →ᴸ L') (M : Type u_1) [L'.Structure M] :
ϕ.is_expansion_on M
source
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] :
ϕ.is_expansion_on M
source
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
source
@[simp]
theorem first_order.language.Lequiv.refl_to_Lhom (L : first_order.language) :
(first_order.language.Lequiv.refl L).to_Lhom = first_order.language.Lhom.id L
source
@[protected]
def first_order.language.Lequiv.refl (L : first_order.language) :
L ≃ᴸ L

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

Equations
source
@[simp]
theorem first_order.language.Lequiv.refl_inv_Lhom (L : first_order.language) :
(first_order.language.Lequiv.refl L).inv_Lhom = first_order.language.Lhom.id L
source
@[protected, instance]
def first_order.language.Lequiv.inhabited {L : first_order.language} :
inhabited (L ≃ᴸ L)
Equations
source
@[simp]
theorem first_order.language.Lequiv.symm_inv_Lhom {L : first_order.language} {L' : first_order.language} (e : L ≃ᴸ L') :
e.symm.inv_Lhom = e.to_Lhom
source
@[protected]
def first_order.language.Lequiv.symm {L : first_order.language} {L' : first_order.language} (e : L ≃ᴸ L') :
L' ≃ᴸ L

The inverse of an equivalence of first-order languages.

Equations
source
@[simp]
theorem first_order.language.Lequiv.symm_to_Lhom {L : first_order.language} {L' : first_order.language} (e : L ≃ᴸ L') :
e.symm.to_Lhom = e.inv_Lhom
source
@[simp]
theorem first_order.language.Lequiv.trans_to_Lhom {L : first_order.language} {L' : first_order.language} {L'' : first_order.language} (e : L ≃ᴸ L') (e' : L' ≃ᴸ L'') :
(e.trans e').to_Lhom = e'.to_Lhom.comp e.to_Lhom
source
@[protected, trans]
def first_order.language.Lequiv.trans {L : first_order.language} {L' : first_order.language} {L'' : first_order.language} (e : L ≃ᴸ L') (e' : L' ≃ᴸ L'') :
L ≃ᴸ L''

The composition of equivalences of first-order languages.

Equations
source
@[simp]
theorem first_order.language.Lequiv.trans_inv_Lhom {L : first_order.language} {L' : first_order.language} {L'' : first_order.language} (e : L ≃ᴸ L') (e' : L' ≃ᴸ L'') :
(e.trans e').inv_Lhom = e.inv_Lhom.comp e'.inv_Lhom
source
@[simp]
def first_order.language.constants_on (α : Type u') :
first_order.language

A language with constants indexed by a type.

Equations
Instances for first_order.language.constants_on
source
theorem first_order.language.constants_on_constants {α : Type u'} :
(first_order.language.constants_on α).constants = α
source
@[protected, instance]
def first_order.language.is_algebraic_constants_on {α : Type u'} :
(first_order.language.constants_on α).is_algebraic
source
@[protected, instance]
def first_order.language.is_relational_constants_on {α : Type u'} [ie : is_empty α] :
(first_order.language.constants_on α).is_relational
source
@[protected, instance]
def first_order.language.is_empty_functions_constants_on_succ {α : Type u'} {n : ℕ} :
is_empty ((first_order.language.constants_on α).functions (n + 1))
source
theorem first_order.language.card_constants_on {α : Type u'} :
(first_order.language.constants_on α).card = cardinal.mk α
source
def first_order.language.constants_on.Structure {M : Type w} {α : Type u'} (f : α → M) :
(first_order.language.constants_on α).Structure M

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

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

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

Equations
Instances for first_order.language.Lhom.constants_on_map
source
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 = fα) :
(first_order.language.Lhom.constants_on_map f).is_expansion_on M
source
def first_order.language.with_constants (L : first_order.language) (α : Type w') :
first_order.language

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

Equations
Instances for first_order.language.with_constants
source
@[simp]
theorem first_order.language.card_with_constants (L : first_order.language) (α : Type w') :
(L.with_constants α).card = L.card.lift + (cardinal.mk α).lift
source
@[simp]
theorem first_order.language.Lhom_with_constants_on_relation (L : first_order.language) (α : Type w') (n : ℕ) (val : L.relations n) :
(L.Lhom_with_constants α).on_relation val = sum.inl val
source
@[simp]
theorem first_order.language.Lhom_with_constants_on_function (L : first_order.language) (α : Type w') (n : ℕ) (val : L.functions n) :
(L.Lhom_with_constants α).on_function val = sum.inl val
source
def first_order.language.Lhom_with_constants (L : first_order.language) (α : Type w') :
L →ᴸ L.with_constants α

The language map adding constants.

Equations
Instances for first_order.language.Lhom_with_constants
source
theorem first_order.language.Lhom_with_constants_injective (L : first_order.language) (α : Type w') :
(L.Lhom_with_constants α).injective
source
@[protected]
def first_order.language.con (L : first_order.language) {α : Type w'} (a : α) :
(L.with_constants α).constants

The constant symbol indexed by a particular element.

Equations
source
def first_order.language.Lhom.add_constants {L : first_order.language} (α : Type w') {L' : first_order.language} (φ : L →ᴸ L') :
L.with_constants α →ᴸ L'.with_constants α

Adds constants to a language map.

Equations
Instances for first_order.language.Lhom.add_constants
source
@[protected, instance]
def first_order.language.params_Structure (α : Type w') (A : set α) :
(first_order.language.constants_on ↥A).Structure α
Equations
source
@[simp]
theorem first_order.language.Lequiv.add_empty_constants_inv_Lhom (L : first_order.language) (α : Type w') [ie : is_empty α] :
(first_order.language.Lequiv.add_empty_constants L α).inv_Lhom = (first_order.language.Lhom.id L).sum_elim (first_order.language.Lhom.of_is_empty (first_order.language.constants_on α) L)
source
def first_order.language.Lequiv.add_empty_constants (L : first_order.language) (α : Type w') [ie : is_empty α] :
L ≃ᴸ L.with_constants α

The language map removing an empty constant set.

Equations
source
@[simp]
theorem first_order.language.Lequiv.add_empty_constants_to_Lhom (L : first_order.language) (α : Type w') [ie : is_empty α] :
(first_order.language.Lequiv.add_empty_constants L α).to_Lhom = L.Lhom_with_constants α
source
@[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] [(L.Lhom_with_constants α).is_expansion_on M] {n : ℕ} {f : L.functions n} {x : fin n → M} :
first_order.language.Structure.fun_map (sum.inl f) x = first_order.language.Structure.fun_map f x
source
@[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] [(L.Lhom_with_constants α).is_expansion_on M] {n : ℕ} {R : L.relations n} {x : fin n → M} :
first_order.language.Structure.rel_map (sum.inl R) x = first_order.language.Structure.rel_map R x
source
def first_order.language.Lhom_with_constants_map (L : first_order.language) {α : Type w'} {β : Type u_1} (f : α → β) :
L.with_constants α →ᴸ L.with_constants β

The language map extending the constant set.

Equations
Instances for first_order.language.Lhom_with_constants_map
source
@[simp]
theorem first_order.language.Lhom.map_constants_comp_sum_inl (L : first_order.language) {α : Type w'} {β : Type u_1} {f : α → β} :
(L.Lhom_with_constants_map f).comp first_order.language.Lhom.sum_inl = L.Lhom_with_constants β
source
@[protected, instance]
def first_order.language.constants_on_self_Structure {M : Type w} :
(first_order.language.constants_on M).Structure M
Equations
source
@[protected, instance]
def first_order.language.with_constants_self_Structure (L : first_order.language) {M : Type w} [L.Structure M] :
(L.with_constants M).Structure M
Equations
source
@[protected, instance]
def first_order.language.with_constants_self_expansion (L : first_order.language) {M : Type w} [L.Structure M] :
(L.Lhom_with_constants M).is_expansion_on M
source
@[protected, instance]
def first_order.language.with_constants_Structure (L : first_order.language) {M : Type w} [L.Structure M] (α : Type u_1) [(first_order.language.constants_on α).Structure M] :
(L.with_constants α).Structure M
Equations
source
@[protected, instance]
def first_order.language.with_constants_expansion (L : first_order.language) {M : Type w} [L.Structure M] (α : Type u_1) [(first_order.language.constants_on α).Structure M] :
(L.Lhom_with_constants α).is_expansion_on M
source
@[protected, instance]
def first_order.language.add_empty_constants_is_expansion_on' (L : first_order.language) {M : Type w} [L.Structure M] :
(first_order.language.Lequiv.add_empty_constants L ↥∅).to_Lhom.is_expansion_on M
source
@[protected, instance]
def first_order.language.add_empty_constants_symm_is_expansion_on (L : first_order.language) {M : Type w} [L.Structure M] :
(first_order.language.Lequiv.add_empty_constants L ↥∅).symm.to_Lhom.is_expansion_on M
source
@[protected, instance]
def first_order.language.add_constants_expansion (L : first_order.language) {M : Type w} [L.Structure M] (α : Type u_1) [(first_order.language.constants_on α).Structure M] {L' : first_order.language} [L'.Structure M] (φ : L →ᴸ L') [φ.is_expansion_on M] :
(first_order.language.Lhom.add_constants α φ).is_expansion_on M
source
@[simp]
theorem first_order.language.with_constants_fun_map_sum_inr (L : first_order.language) {M : Type w} [L.Structure M] (α : Type u_1) [(first_order.language.constants_on α).Structure M] {a : α} {x : fin 0 → M} :
first_order.language.Structure.fun_map (sum.inr a) x = ↑(L.con a)
source
@[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
source
@[protected, instance]
def first_order.language.constants_on_map_inclusion_is_expansion_on {M : Type w} {A B : set M} (h : A ⊆ B) :
(first_order.language.Lhom.constants_on_map (set.inclusion h)).is_expansion_on M
source
@[protected, instance]
def first_order.language.map_constants_inclusion_is_expansion_on (L : first_order.language) {M : Type w} [L.Structure M] {A B : set M} (h : A ⊆ B) :
(L.Lhom_with_constants_map (set.inclusion h)).is_expansion_on M