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 n → L'.Functions n
• onRelation : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n

def FirstOrder.Language.«term_→ᴸ_» : Lean.TrailingParserDescr

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.

def FirstOrder.Language.LHom.mk₂ {L' : FirstOrder.Language} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (φ₀ : c → L'.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.

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.

@[simp]

theorem FirstOrder.Language.LHom.id_onFunction (L : FirstOrder.Language) (_n : ℕ) (a : L.Functions _n) : (FirstOrder.Language.LHom.id L).onFunction a = id a

@[simp]

theorem FirstOrder.Language.LHom.id_onRelation (L : FirstOrder.Language) (_n : ℕ) (a : L.Relations _n) : (FirstOrder.Language.LHom.id L).onRelation a = id a

def FirstOrder.Language.LHom.id (L : FirstOrder.Language) : L →ᴸ L

The identity language homomorphism.

Equations

• FirstOrder.Language.LHom.id L = { onFunction := fun (_n : ℕ) => id, onRelation := fun (_n : ℕ) => id }

instance FirstOrder.Language.LHom.instInhabited {L : FirstOrder.Language} : Inhabited (L →ᴸ L)

Equations

• FirstOrder.Language.LHom.instInhabited = { default := FirstOrder.Language.LHom.id L }

@[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

def FirstOrder.Language.LHom.sumInl {L : FirstOrder.Language} {L' : FirstOrder.Language} : L →ᴸ L.sum L'

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 }

@[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

def FirstOrder.Language.LHom.sumInr {L : FirstOrder.Language} {L' : FirstOrder.Language} : L' →ᴸ L.sum L'

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 }

@[simp]

theorem FirstOrder.Language.LHom.ofIsEmpty_onFunction (L : FirstOrder.Language) (L' : FirstOrder.Language) [L.IsAlgebraic] [L.IsRelational] (n : ℕ) (a : L.Functions n) : (FirstOrder.Language.LHom.ofIsEmpty L L').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) : (FirstOrder.Language.LHom.ofIsEmpty L L').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

• FirstOrder.Language.LHom.ofIsEmpty L L' = { onFunction := fun (n : ℕ) (a : L.Functions n) => ⋯.elim a, onRelation := fun (n : ℕ) (a : L.Relations n) => ⋯.elim a }

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

instance FirstOrder.Language.LHom.instUniqueOfIsAlgebraicOfIsRelational {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsAlgebraic] [L.IsRelational] : Unique (L →ᴸ L')

Equations

• FirstOrder.Language.LHom.instUniqueOfIsAlgebraicOfIsRelational = { default := FirstOrder.Language.LHom.ofIsEmpty L L', 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)

def FirstOrder.Language.LHom.comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (g : L' →ᴸ L'') (f : L →ᴸ L') : L →ᴸ L''

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) }

@[simp]

theorem FirstOrder.Language.LHom.id_comp {L : FirstOrder.Language} {L' : FirstOrder.Language} (F : L →ᴸ L') : (FirstOrder.Language.LHom.id L').comp F = F

@[simp]

theorem FirstOrder.Language.LHom.comp_id {L : FirstOrder.Language} {L' : FirstOrder.Language} (F : L →ᴸ L') : F.comp (FirstOrder.Language.LHom.id L) = F

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

def FirstOrder.Language.LHom.sumElim {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') : L.sum L'' →ᴸ L'

A language map defined on two factors of a sum.

Equations

• One or more equations did not get rendered due to their size.

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.

@[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 ψ

structure FirstOrder.Language.LHom.Injective {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') : Prop

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

• onFunction : ∀ {n : ℕ}, Function.Injective fun (f : L.Functions n) => ϕ.onFunction f
• onRelation : ∀ {n : ℕ}, Function.Injective fun (R : L.Relations n) => ϕ.onRelation R

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) [Inhabited M] [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.

class FirstOrder.Language.LHom.IsExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') (M : Type u_1) [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.

• map_onFunction : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), FirstOrder.Language.Structure.funMap (ϕ.onFunction f) x = FirstOrder.Language.Structure.funMap f x
• map_onRelation : ∀ {n : ℕ} (R : L.Relations n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap (ϕ.onRelation R) x = FirstOrder.Language.Structure.RelMap R x

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 n → M) : FirstOrder.Language.Structure.funMap (ϕ.onFunction f) x = FirstOrder.Language.Structure.funMap f x

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 n → M) : FirstOrder.Language.Structure.RelMap (ϕ.onRelation R) x = FirstOrder.Language.Structure.RelMap R x

@[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 n → M) : FirstOrder.Language.Structure.funMap (ϕ.onFunction f) x = FirstOrder.Language.Structure.funMap f x

@[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 n → M) : FirstOrder.Language.Structure.RelMap (ϕ.onRelation R) x = FirstOrder.Language.Structure.RelMap R x

instance FirstOrder.Language.LHom.id_isExpansionOn {L : FirstOrder.Language} (M : Type u_1) [L.Structure M] : (FirstOrder.Language.LHom.id L).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] : (FirstOrder.Language.LHom.ofIsEmpty L L').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 n → M} : FirstOrder.Language.Structure.funMap (Sum.inl f) x = FirstOrder.Language.Structure.funMap f x

@[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 n → M} : FirstOrder.Language.Structure.funMap (Sum.inr f) x = FirstOrder.Language.Structure.funMap f x

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) [Inhabited M] [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 = FirstOrder.Language.LHom.id L
• right_inv : self.toLHom.comp self.invLHom = FirstOrder.Language.LHom.id L'

theorem FirstOrder.Language.LEquiv.left_inv {L : FirstOrder.Language} {L' : FirstOrder.Language} (self : L ≃ᴸ L') : self.invLHom.comp self.toLHom = FirstOrder.Language.LHom.id L

theorem FirstOrder.Language.LEquiv.right_inv {L : FirstOrder.Language} {L' : FirstOrder.Language} (self : L ≃ᴸ L') : self.toLHom.comp self.invLHom = FirstOrder.Language.LHom.id L'

def FirstOrder.Language.«term_≃ᴸ_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FirstOrder.Language.LEquiv.refl_invLHom (L : FirstOrder.Language) : (FirstOrder.Language.LEquiv.refl L).invLHom = FirstOrder.Language.LHom.id L

@[simp]

theorem FirstOrder.Language.LEquiv.refl_toLHom (L : FirstOrder.Language) : (FirstOrder.Language.LEquiv.refl L).toLHom = FirstOrder.Language.LHom.id L

def FirstOrder.Language.LEquiv.refl (L : FirstOrder.Language) : L ≃ᴸ L

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

Equations

• FirstOrder.Language.LEquiv.refl L = { toLHom := FirstOrder.Language.LHom.id L, invLHom := FirstOrder.Language.LHom.id L, left_inv := ⋯, right_inv := ⋯ }

instance FirstOrder.Language.LEquiv.instInhabited {L : FirstOrder.Language} : Inhabited (L ≃ᴸ L)

Equations

• FirstOrder.Language.LEquiv.instInhabited = { default := FirstOrder.Language.LEquiv.refl L }

@[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

def FirstOrder.Language.LEquiv.symm {L : FirstOrder.Language} {L' : FirstOrder.Language} (e : L ≃ᴸ L') : L' ≃ᴸ L

The inverse of an equivalence of first-order languages.

Equations

• e.symm = { toLHom := e.invLHom, invLHom := e.toLHom, left_inv := ⋯, right_inv := ⋯ }

@[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

def FirstOrder.Language.LEquiv.trans {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (e : L ≃ᴸ L') (e' : L' ≃ᴸ L'') : L ≃ᴸ L''

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 := ⋯ }

def FirstOrder.Language.constantsOn (α : Type u') : FirstOrder.Language

A language with constants indexed by a type.

Equations

• FirstOrder.Language.constantsOn α = FirstOrder.Language.mk₂ α PEmpty.{u' + 1} PEmpty.{u' + 1} PEmpty.{1} PEmpty.{1}

theorem FirstOrder.Language.constantsOn_constants {α : Type u'} : (FirstOrder.Language.constantsOn α).Constants = α

instance FirstOrder.Language.isAlgebraic_constantsOn {α : Type u'} : (FirstOrder.Language.constantsOn α).IsAlgebraic

Equations

• ⋯ = ⋯

instance FirstOrder.Language.isRelational_constantsOn {α : Type u'} [_ie : IsEmpty α] : (FirstOrder.Language.constantsOn α).IsRelational

Equations

• ⋯ = ⋯

instance FirstOrder.Language.isEmpty_functions_constantsOn_succ {α : Type u'} {n : ℕ} : IsEmpty ((FirstOrder.Language.constantsOn α).Functions (n + 1))

Equations

• ⋯ = ⋯

theorem FirstOrder.Language.card_constantsOn {α : Type u'} : (FirstOrder.Language.constantsOn α).card = Cardinal.mk α

def FirstOrder.Language.constantsOn.structure {M : Type w} {α : Type u'} (f : α → M) : (FirstOrder.Language.constantsOn α).Structure M

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

Equations

• FirstOrder.Language.constantsOn.structure f = FirstOrder.Language.Structure.mk₂ f PEmpty.elim PEmpty.elim PEmpty.elim PEmpty.elim

def FirstOrder.Language.LHom.constantsOnMap {α : Type u'} {β : Type v'} (f : α → β) : FirstOrder.Language.constantsOn α →ᴸ FirstOrder.Language.constantsOn β

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

Equations

• FirstOrder.Language.LHom.constantsOnMap f = FirstOrder.Language.LHom.mk₂ f PEmpty.elim PEmpty.elim PEmpty.elim PEmpty.elim

theorem FirstOrder.Language.constantsOnMap_isExpansionOn {M : Type w} {α : Type u'} {β : Type v'} {f : α → β} {fα : α → M} {fβ : β → M} (h : fβ ∘ f = fα) : (FirstOrder.Language.LHom.constantsOnMap f).IsExpansionOn M

def FirstOrder.Language.withConstants (L : FirstOrder.Language) (α : Type w') : FirstOrder.Language

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

Equations

• L.withConstants α = L.sum (FirstOrder.Language.constantsOn α)

def FirstOrder.«term_[[_]]» : Lean.TrailingParserDescr

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.

@[simp]

theorem FirstOrder.Language.card_withConstants (L : FirstOrder.Language) (α : Type w') : (L.withConstants α).card = Cardinal.lift.{w', max u v} L.card + Cardinal.lift.{max u v, w'} (Cardinal.mk α)

@[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 α

The language map adding constants.

Equations

• L.lhomWithConstants α = FirstOrder.Language.LHom.sumInl

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 = Sum.inr a

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

• FirstOrder.Language.LHom.addConstants α φ = φ.sumMap (FirstOrder.Language.LHom.id (FirstOrder.Language.constantsOn α))

instance FirstOrder.Language.paramsStructure (α : Type w') (A : Set α) : (FirstOrder.Language.constantsOn ↑A).Structure α

Equations

• FirstOrder.Language.paramsStructure α A = FirstOrder.Language.constantsOn.structure Subtype.val

@[simp]

theorem FirstOrder.Language.LEquiv.addEmptyConstants_invLHom (L : FirstOrder.Language) (α : Type w') [ie : IsEmpty α] : (FirstOrder.Language.LEquiv.addEmptyConstants L α).invLHom = (FirstOrder.Language.LHom.id L).sumElim (FirstOrder.Language.LHom.ofIsEmpty (FirstOrder.Language.constantsOn α) L)

@[simp]

theorem FirstOrder.Language.LEquiv.addEmptyConstants_toLHom (L : FirstOrder.Language) (α : Type w') [ie : IsEmpty α] : (FirstOrder.Language.LEquiv.addEmptyConstants L α).toLHom = L.lhomWithConstants α

def FirstOrder.Language.LEquiv.addEmptyConstants (L : FirstOrder.Language) (α : Type w') [ie : IsEmpty α] : L ≃ᴸ L.withConstants α

The language map removing an empty constant set.

Equations

• One or more equations did not get rendered due to their size.

@[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 n → M} : FirstOrder.Language.Structure.funMap (Sum.inl f) x = FirstOrder.Language.Structure.funMap f x

@[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 n → M} : FirstOrder.Language.Structure.RelMap (Sum.inl R) x = FirstOrder.Language.Structure.RelMap R x

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 = (FirstOrder.Language.LHom.id L).sumMap (FirstOrder.Language.LHom.constantsOnMap f)

@[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} : (FirstOrder.Language.constantsOn M).Structure M

Equations

• FirstOrder.Language.constantsOnSelfStructure = FirstOrder.Language.constantsOn.structure id

instance FirstOrder.Language.withConstantsSelfStructure (L : FirstOrder.Language) {M : Type w} [L.Structure M] : (L.withConstants M).Structure M

Equations

• L.withConstantsSelfStructure = L.sumStructure (FirstOrder.Language.constantsOn M) 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) [(FirstOrder.Language.constantsOn α).Structure M] : (L.withConstants α).Structure M

Equations

• L.withConstantsStructure α = L.sumStructure (FirstOrder.Language.constantsOn α) M

instance FirstOrder.Language.withConstants_expansion (L : FirstOrder.Language) {M : Type w} [L.Structure M] (α : Type u_1) [(FirstOrder.Language.constantsOn α).Structure M] : (L.lhomWithConstants α).IsExpansionOn M

Equations

• ⋯ = ⋯

instance FirstOrder.Language.addEmptyConstants_is_expansion_on' (L : FirstOrder.Language) {M : Type w} [L.Structure M] : (FirstOrder.Language.LEquiv.addEmptyConstants L ↑∅).toLHom.IsExpansionOn M

Equations

• ⋯ = ⋯

instance FirstOrder.Language.addEmptyConstants_symm_isExpansionOn (L : FirstOrder.Language) {M : Type w} [L.Structure M] : (FirstOrder.Language.LEquiv.addEmptyConstants L ↑∅).symm.toLHom.IsExpansionOn M

Equations

• ⋯ = ⋯

instance FirstOrder.Language.addConstants_expansion (L : FirstOrder.Language) {M : Type w} [L.Structure M] (α : Type u_1) [(FirstOrder.Language.constantsOn α).Structure M] {L' : FirstOrder.Language} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] : (FirstOrder.Language.LHom.addConstants α φ).IsExpansionOn M

Equations

• ⋯ = ⋯

@[simp]

theorem FirstOrder.Language.withConstants_funMap_sum_inr (L : FirstOrder.Language) {M : Type w} [L.Structure M] (α : Type u_1) [(FirstOrder.Language.constantsOn α).Structure M] {a : α} {x : Fin 0 → M} : FirstOrder.Language.Structure.funMap (Sum.inr a) x = ↑(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) : (FirstOrder.Language.LHom.constantsOnMap (Set.inclusion h)).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 (Set.inclusion h)).IsExpansionOn M

Equations

• ⋯ = ⋯