# Language Maps #

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

## Main Definitions #

• A FirstOrder.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 FirstOrder.Language.LEquiv, denoted L ≃ᴸ L', is an invertible language homomorphism.
• FirstOrder.Language.withConstants is defined so that if M is an L.Structure and A : Set M, L.withConstants A, denoted L[[A]], is a language which adds constant symbols for elements of A to L.

## 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]
structure FirstOrder.Language.LHom (L : FirstOrder.Language) (L' : FirstOrder.Language) :
Type (max (max (max u u') v) v')

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

• onFunction : n : ⦄ → L.Functions nL'.Functions n
• onRelation : n : ⦄ → L.Relations nL'.Relations n
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def FirstOrder.Language.LHom.mk₂ {L' : FirstOrder.Language} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (φ₀ : cL'.Constants) (φ₁ : f₁L'.Functions 1) (φ₂ : f₂L'.Functions 2) (φ₁' : r₁L'.Relations 1) (φ₂' : r₂L'.Relations 2) :
FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂ →ᴸ L'

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def FirstOrder.Language.LHom.reduct {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') (M : Type u_1) [L'.Structure M] :
L.Structure M

Pulls a structure back along a language map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem FirstOrder.Language.LHom.id_onFunction (L : FirstOrder.Language) (_n : ) (a : L.Functions _n) :
.onFunction a = id a
@[simp]
theorem FirstOrder.Language.LHom.id_onRelation (L : FirstOrder.Language) (_n : ) (a : L.Relations _n) :
.onRelation a = id a

The identity language homomorphism.

Equations
• = { onFunction := fun (_n : ) => id, onRelation := fun (_n : ) => id }
Instances For
Equations
• FirstOrder.Language.LHom.instInhabited = { default := }
@[simp]
theorem FirstOrder.Language.LHom.sumInl_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ) (val : L.Functions _n) :
FirstOrder.Language.LHom.sumInl.onFunction val = Sum.inl val
@[simp]
theorem FirstOrder.Language.LHom.sumInl_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ) (val : L.Relations _n) :
FirstOrder.Language.LHom.sumInl.onRelation val = Sum.inl val

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

Equations
• FirstOrder.Language.LHom.sumInl = { onFunction := fun (_n : ) => Sum.inl, onRelation := fun (_n : ) => Sum.inl }
Instances For
@[simp]
theorem FirstOrder.Language.LHom.sumInr_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ) (val : L'.Relations _n) :
FirstOrder.Language.LHom.sumInr.onRelation val = Sum.inr val
@[simp]
theorem FirstOrder.Language.LHom.sumInr_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ) (val : L'.Functions _n) :
FirstOrder.Language.LHom.sumInr.onFunction val = Sum.inr val

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

Equations
• FirstOrder.Language.LHom.sumInr = { onFunction := fun (_n : ) => Sum.inr, onRelation := fun (_n : ) => Sum.inr }
Instances For
@[simp]
theorem FirstOrder.Language.LHom.ofIsEmpty_onFunction (L : FirstOrder.Language) (L' : FirstOrder.Language) [L.IsAlgebraic] [L.IsRelational] (n : ) (a : L.Functions n) :
.onFunction a = .elim a
@[simp]
theorem FirstOrder.Language.LHom.ofIsEmpty_onRelation (L : FirstOrder.Language) (L' : FirstOrder.Language) [L.IsAlgebraic] [L.IsRelational] (n : ) (a : L.Relations n) :
.onRelation a = .elim a
def FirstOrder.Language.LHom.ofIsEmpty (L : FirstOrder.Language) (L' : FirstOrder.Language) [L.IsAlgebraic] [L.IsRelational] :
L →ᴸ L'

The inclusion of an empty language into any other language.

Equations
• = { onFunction := fun (n : ) (a : L.Functions n) => .elim a, onRelation := fun (n : ) (a : L.Relations n) => .elim a }
Instances For
theorem FirstOrder.Language.LHom.funext {L : FirstOrder.Language} {L' : FirstOrder.Language} {F : L →ᴸ L'} {G : L →ᴸ L'} (h_fun : F.onFunction = G.onFunction) (h_rel : F.onRelation = G.onRelation) :
F = G
Equations
• FirstOrder.Language.LHom.instUniqueOfIsAlgebraicOfIsRelational = { default := , uniq := }
theorem FirstOrder.Language.LHom.mk₂_funext {L' : FirstOrder.Language} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} {F : FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂ →ᴸ L'} {G : FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂ →ᴸ L'} (h0 : ∀ (c_1 : (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Constants), F.onFunction c_1 = G.onFunction c_1) (h1 : ∀ (f : (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Functions 1), F.onFunction f = G.onFunction f) (h2 : ∀ (f : (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Functions 2), F.onFunction f = G.onFunction f) (h1' : ∀ (r : (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Relations 1), F.onRelation r = G.onRelation r) (h2' : ∀ (r : (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Relations 2), F.onRelation r = G.onRelation r) :
F = G
@[simp]
theorem FirstOrder.Language.LHom.comp_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (g : L' →ᴸ L'') (f : L →ᴸ L') (_n : ) (F : L.Functions _n) :
(g.comp f).onFunction F = g.onFunction (f.onFunction F)
@[simp]
theorem FirstOrder.Language.LHom.comp_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (g : L' →ᴸ L'') (f : L →ᴸ L') :
∀ (x : ) (R : L.Relations x), (g.comp f).onRelation R = g.onRelation (f.onRelation R)

The composition of two language homomorphisms.

Equations
• g.comp f = { onFunction := fun (_n : ) (F : L.Functions _n) => g.onFunction (f.onFunction F), onRelation := fun (x : ) (R : L.Relations x) => g.onRelation (f.onRelation R) }
Instances For
theorem FirstOrder.Language.LHom.comp_assoc {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {L3 : FirstOrder.Language} (F : L'' →ᴸ L3) (G : L' →ᴸ L'') (H : L →ᴸ L') :
(F.comp G).comp H = F.comp (G.comp H)
@[simp]
theorem FirstOrder.Language.LHom.sumElim_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') (_n : ) :
∀ (a : L.Functions _n L''.Functions _n), (ϕ.sumElim ψ).onFunction a = Sum.elim (fun (f : L.Functions _n) => ϕ.onFunction f) (fun (f : L''.Functions _n) => ψ.onFunction f) a
@[simp]
theorem FirstOrder.Language.LHom.sumElim_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') (_n : ) :
∀ (a : L.Relations _n L''.Relations _n), (ϕ.sumElim ψ).onRelation a = Sum.elim (fun (f : L.Relations _n) => ϕ.onRelation f) (fun (f : L''.Relations _n) => ψ.onRelation f) a

A language map defined on two factors of a sum.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem FirstOrder.Language.LHom.sumElim_comp_inl {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') :
(ϕ.sumElim ψ).comp FirstOrder.Language.LHom.sumInl = ϕ
theorem FirstOrder.Language.LHom.sumElim_comp_inr {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') :
(ϕ.sumElim ψ).comp FirstOrder.Language.LHom.sumInr = ψ
theorem FirstOrder.Language.LHom.sumElim_inl_inr {L : FirstOrder.Language} {L' : FirstOrder.Language} :
FirstOrder.Language.LHom.sumInl.sumElim FirstOrder.Language.LHom.sumInr = FirstOrder.Language.LHom.id (L.sum L')
theorem FirstOrder.Language.LHom.comp_sumElim {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') {L3 : FirstOrder.Language} (θ : L' →ᴸ L3) :
θ.comp (ϕ.sumElim ψ) = (θ.comp ϕ).sumElim (θ.comp ψ)
@[simp]
theorem FirstOrder.Language.LHom.sumMap_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) (_n : ) :
∀ (a : L.Relations _n L₁.Relations _n), (ϕ.sumMap ψ).onRelation a = Sum.map (fun (f : L.Relations _n) => ϕ.onRelation f) (fun (f : L₁.Relations _n) => ψ.onRelation f) a
@[simp]
theorem FirstOrder.Language.LHom.sumMap_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) (_n : ) :
∀ (a : L.Functions _n L₁.Functions _n), (ϕ.sumMap ψ).onFunction a = Sum.map (fun (f : L.Functions _n) => ϕ.onFunction f) (fun (f : L₁.Functions _n) => ψ.onFunction f) a
def FirstOrder.Language.LHom.sumMap {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) :
L.sum L₁ →ᴸ L'.sum L₂

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem FirstOrder.Language.LHom.sumMap_comp_inl {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) :
(ϕ.sumMap ψ).comp FirstOrder.Language.LHom.sumInl = FirstOrder.Language.LHom.sumInl.comp ϕ
@[simp]
theorem FirstOrder.Language.LHom.sumMap_comp_inr {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) :
(ϕ.sumMap ψ).comp FirstOrder.Language.LHom.sumInr = FirstOrder.Language.LHom.sumInr.comp ψ

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

Instances For
theorem FirstOrder.Language.LHom.Injective.onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} (self : ϕ.Injective) {n : } :
Function.Injective fun (f : L.Functions n) => ϕ.onFunction f
theorem FirstOrder.Language.LHom.Injective.onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} (self : ϕ.Injective) {n : } :
Function.Injective fun (R : L.Relations n) => ϕ.onRelation R
noncomputable def FirstOrder.Language.LHom.defaultExpansion {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') [(n : ) → (f : L'.Functions n) → Decidable (f Set.range fun (f : L.Functions n) => ϕ.onFunction f)] [(n : ) → (r : L'.Relations n) → Decidable (r Set.range fun (r : L.Relations n) => ϕ.onRelation r)] (M : Type u_1) [] [L.Structure M] :
L'.Structure M

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
class FirstOrder.Language.LHom.IsExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') (M : Type u_1) [L.Structure M] [L'.Structure M] :

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

Instances
theorem FirstOrder.Language.LHom.IsExpansionOn.map_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} {M : Type u_1} [L.Structure M] [L'.Structure M] [self : ϕ.IsExpansionOn M] {n : } (f : L.Functions n) (x : Fin nM) :
theorem FirstOrder.Language.LHom.IsExpansionOn.map_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} {M : Type u_1} [L.Structure M] [L'.Structure M] [self : ϕ.IsExpansionOn M] {n : } (R : L.Relations n) (x : Fin nM) :
@[simp]
theorem FirstOrder.Language.LHom.map_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {M : Type u_1} [L.Structure M] [L'.Structure M] [ϕ.IsExpansionOn M] {n : } (f : L.Functions n) (x : Fin nM) :
@[simp]
theorem FirstOrder.Language.LHom.map_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {M : Type u_1} [L.Structure M] [L'.Structure M] [ϕ.IsExpansionOn M] {n : } (R : L.Relations n) (x : Fin nM) :
instance FirstOrder.Language.LHom.id_isExpansionOn {L : FirstOrder.Language} (M : Type u_1) [L.Structure M] :
.IsExpansionOn M
Equations
• =
instance FirstOrder.Language.LHom.ofIsEmpty_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type u_1) [L.Structure M] [L'.Structure M] [L.IsAlgebraic] [L.IsRelational] :
.IsExpansionOn M
Equations
• =
instance FirstOrder.Language.LHom.sumElim_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') (M : Type u_1) [L.Structure M] [L'.Structure M] [L''.Structure M] [ϕ.IsExpansionOn M] [ψ.IsExpansionOn M] :
(ϕ.sumElim ψ).IsExpansionOn M
Equations
• =
instance FirstOrder.Language.LHom.sumMap_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) (M : Type u_1) [L.Structure M] [L'.Structure M] [L₁.Structure M] [L₂.Structure M] [ϕ.IsExpansionOn M] [ψ.IsExpansionOn M] :
(ϕ.sumMap ψ).IsExpansionOn M
Equations
• =
instance FirstOrder.Language.LHom.sumInl_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type u_1) [L.Structure M] [L'.Structure M] :
FirstOrder.Language.LHom.sumInl.IsExpansionOn M
Equations
• =
instance FirstOrder.Language.LHom.sumInr_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type u_1) [L.Structure M] [L'.Structure M] :
FirstOrder.Language.LHom.sumInr.IsExpansionOn M
Equations
• =
@[simp]
theorem FirstOrder.Language.LHom.funMap_sumInl {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [L.Structure M] [(L.sum L').Structure M] [FirstOrder.Language.LHom.sumInl.IsExpansionOn M] {n : } {f : L.Functions n} {x : Fin nM} :
@[simp]
theorem FirstOrder.Language.LHom.funMap_sumInr {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [L.Structure M] [(L'.sum L).Structure M] [FirstOrder.Language.LHom.sumInr.IsExpansionOn M] {n : } {f : L.Functions n} {x : Fin nM} :
theorem FirstOrder.Language.LHom.sumInl_injective {L : FirstOrder.Language} {L' : FirstOrder.Language} :
FirstOrder.Language.LHom.sumInl.Injective
theorem FirstOrder.Language.LHom.sumInr_injective {L : FirstOrder.Language} {L' : FirstOrder.Language} :
FirstOrder.Language.LHom.sumInr.Injective
@[instance 100]
instance FirstOrder.Language.LHom.isExpansionOn_reduct {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') (M : Type u_1) [L'.Structure M] :
ϕ.IsExpansionOn M
Equations
• =
theorem FirstOrder.Language.LHom.Injective.isExpansionOn_default {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} [(n : ) → (f : L'.Functions n) → Decidable (f Set.range fun (f : L.Functions n) => ϕ.onFunction f)] [(n : ) → (r : L'.Relations n) → Decidable (r Set.range fun (r : L.Relations n) => ϕ.onRelation r)] (h : ϕ.Injective) (M : Type u_1) [] [L.Structure M] :
ϕ.IsExpansionOn M
structure FirstOrder.Language.LEquiv (L : FirstOrder.Language) (L' : FirstOrder.Language) :
Type (max (max (max u_1 u_2) u_3) u_4)

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

• toLHom : L →ᴸ L'
• invLHom : L' →ᴸ L
• left_inv : self.invLHom.comp self.toLHom =
• right_inv : self.toLHom.comp self.invLHom =
Instances For
theorem FirstOrder.Language.LEquiv.left_inv {L : FirstOrder.Language} {L' : FirstOrder.Language} (self : L ≃ᴸ L') :
self.invLHom.comp self.toLHom =
theorem FirstOrder.Language.LEquiv.right_inv {L : FirstOrder.Language} {L' : FirstOrder.Language} (self : L ≃ᴸ L') :
self.toLHom.comp self.invLHom =
Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• = { toLHom := , invLHom := , left_inv := , right_inv := }
Instances For
Equations
• FirstOrder.Language.LEquiv.instInhabited = { default := }
@[simp]
theorem FirstOrder.Language.LEquiv.symm_invLHom {L : FirstOrder.Language} {L' : FirstOrder.Language} (e : L ≃ᴸ L') :
e.symm.invLHom = e.toLHom
@[simp]
theorem FirstOrder.Language.LEquiv.symm_toLHom {L : FirstOrder.Language} {L' : FirstOrder.Language} (e : L ≃ᴸ L') :
e.symm.toLHom = e.invLHom

The inverse of an equivalence of first-order languages.

Equations
• e.symm = { toLHom := e.invLHom, invLHom := e.toLHom, left_inv := , right_inv := }
Instances For
@[simp]
theorem FirstOrder.Language.LEquiv.trans_invLHom {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (e : L ≃ᴸ L') (e' : L' ≃ᴸ L'') :
(e.trans e').invLHom = e.invLHom.comp e'.invLHom
@[simp]
theorem FirstOrder.Language.LEquiv.trans_toLHom {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (e : L ≃ᴸ L') (e' : L' ≃ᴸ L'') :
(e.trans e').toLHom = e'.toLHom.comp e.toLHom

The composition of equivalences of first-order languages.

Equations
• e.trans e' = { toLHom := e'.toLHom.comp e.toLHom, invLHom := e.invLHom.comp e'.invLHom, left_inv := , right_inv := }
Instances For

A language with constants indexed by a type.

Equations
Instances For
theorem FirstOrder.Language.constantsOn_constants {α : Type u'} :
.Constants = α
instance FirstOrder.Language.isAlgebraic_constantsOn {α : Type u'} :
.IsAlgebraic
Equations
• =
instance FirstOrder.Language.isRelational_constantsOn {α : Type u'} [_ie : ] :
.IsRelational
Equations
• =
instance FirstOrder.Language.isEmpty_functions_constantsOn_succ {α : Type u'} {n : } :
IsEmpty (.Functions (n + 1))
Equations
• =
def FirstOrder.Language.constantsOn.structure {M : Type w} {α : Type u'} (f : αM) :
.Structure M

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

Equations
Instances For
def FirstOrder.Language.LHom.constantsOnMap {α : Type u'} {β : Type v'} (f : αβ) :

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

Equations
Instances For
theorem FirstOrder.Language.constantsOnMap_isExpansionOn {M : Type w} {α : Type u'} {β : Type v'} {f : αβ} {fα : αM} {fβ : βM} (h : f = ) :
.IsExpansionOn M

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

Equations
• L.withConstants α = L.sum
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem FirstOrder.Language.card_withConstants (L : FirstOrder.Language) (α : Type w') :
(L.withConstants α).card = +
@[simp]
theorem FirstOrder.Language.lhomWithConstants_onFunction (L : FirstOrder.Language) (α : Type w') (_n : ) (val : L.Functions _n) :
(L.lhomWithConstants α).onFunction val = Sum.inl val
@[simp]
theorem FirstOrder.Language.lhomWithConstants_onRelation (L : FirstOrder.Language) (α : Type w') (_n : ) (val : L.Relations _n) :
(L.lhomWithConstants α).onRelation val = Sum.inl val
def FirstOrder.Language.lhomWithConstants (L : FirstOrder.Language) (α : Type w') :
L →ᴸ L.withConstants α

Equations
• L.lhomWithConstants α = FirstOrder.Language.LHom.sumInl
Instances For
theorem FirstOrder.Language.lhomWithConstants_injective (L : FirstOrder.Language) (α : Type w') :
(L.lhomWithConstants α).Injective
def FirstOrder.Language.con (L : FirstOrder.Language) {α : Type w'} (a : α) :
(L.withConstants α).Constants

The constant symbol indexed by a particular element.

Equations
• L.con a =
Instances For
def FirstOrder.Language.LHom.addConstants {L : FirstOrder.Language} (α : Type w') {L' : FirstOrder.Language} (φ : L →ᴸ L') :
L.withConstants α →ᴸ L'.withConstants α

Adds constants to a language map.

Equations
Instances For
instance FirstOrder.Language.paramsStructure (α : Type w') (A : Set α) :
.Structure α
Equations
@[simp]
theorem FirstOrder.Language.LEquiv.addEmptyConstants_toLHom (L : FirstOrder.Language) (α : Type w') [ie : ] :
.toLHom = L.lhomWithConstants α
def FirstOrder.Language.LEquiv.addEmptyConstants (L : FirstOrder.Language) (α : Type w') [ie : ] :
L ≃ᴸ L.withConstants α

The language map removing an empty constant set.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem FirstOrder.Language.withConstants_funMap_sum_inl (L : FirstOrder.Language) {M : Type w} [L.Structure M] {α : Type w'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {n : } {f : L.Functions n} {x : Fin nM} :
@[simp]
theorem FirstOrder.Language.withConstants_relMap_sum_inl (L : FirstOrder.Language) {M : Type w} [L.Structure M] {α : Type w'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {n : } {R : L.Relations n} {x : Fin nM} :
def FirstOrder.Language.lhomWithConstantsMap (L : FirstOrder.Language) {α : Type w'} {β : Type u_1} (f : αβ) :
L.withConstants α →ᴸ L.withConstants β

The language map extending the constant set.

Equations
• L.lhomWithConstantsMap f =
Instances For
@[simp]
theorem FirstOrder.Language.LHom.map_constants_comp_sumInl (L : FirstOrder.Language) {α : Type w'} {β : Type u_1} {f : αβ} :
(L.lhomWithConstantsMap f).comp FirstOrder.Language.LHom.sumInl = L.lhomWithConstants β
instance FirstOrder.Language.constantsOnSelfStructure {M : Type w} :
.Structure M
Equations
• FirstOrder.Language.constantsOnSelfStructure =
instance FirstOrder.Language.withConstantsSelfStructure (L : FirstOrder.Language) {M : Type w} [L.Structure M] :
(L.withConstants M).Structure M
Equations
• L.withConstantsSelfStructure = L.sumStructure M
instance FirstOrder.Language.withConstants_self_expansion (L : FirstOrder.Language) {M : Type w} [L.Structure M] :
(L.lhomWithConstants M).IsExpansionOn M
Equations
• =
instance FirstOrder.Language.withConstantsStructure (L : FirstOrder.Language) {M : Type w} [L.Structure M] (α : Type u_1) [.Structure M] :
(L.withConstants α).Structure M
Equations
• L.withConstantsStructure α = L.sumStructure M
instance FirstOrder.Language.withConstants_expansion (L : FirstOrder.Language) {M : Type w} [L.Structure M] (α : Type u_1) [.Structure M] :
(L.lhomWithConstants α).IsExpansionOn M
Equations
• =
instance FirstOrder.Language.addEmptyConstants_is_expansion_on' (L : FirstOrder.Language) {M : Type w} [L.Structure M] :
.toLHom.IsExpansionOn M
Equations
• =
instance FirstOrder.Language.addEmptyConstants_symm_isExpansionOn (L : FirstOrder.Language) {M : Type w} [L.Structure M] :
.toLHom.IsExpansionOn M
Equations
• =
instance FirstOrder.Language.addConstants_expansion (L : FirstOrder.Language) {M : Type w} [L.Structure M] (α : Type u_1) [.Structure M] {L' : FirstOrder.Language} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] :
.IsExpansionOn M
Equations
• =
@[simp]
theorem FirstOrder.Language.withConstants_funMap_sum_inr (L : FirstOrder.Language) {M : Type w} [L.Structure M] (α : Type u_1) [.Structure M] {a : α} {x : Fin 0M} :
= (L.con a)
@[simp]
theorem FirstOrder.Language.coe_con (L : FirstOrder.Language) {M : Type w} [L.Structure M] (A : Set M) {a : A} :
(L.con a) = a
instance FirstOrder.Language.constantsOnMap_inclusion_isExpansionOn {M : Type w} {A : Set M} {B : Set M} (h : A B) :
.IsExpansionOn M
Equations
• =
instance FirstOrder.Language.map_constants_inclusion_isExpansionOn (L : FirstOrder.Language) {M : Type w} [L.Structure M] {A : Set M} {B : Set M} (h : A B) :
(L.lhomWithConstantsMap ()).IsExpansionOn M
Equations
• =