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 → FirstOrder.Language.Constants L') (φ₁ : 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) [FirstOrder.Language.Structure L' M] : FirstOrder.Language.Structure L 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_onRelation (L : FirstOrder.Language) (_n : ℕ) (a : L.Relations _n) : (FirstOrder.Language.LHom.id L).onRelation a = id a

@[simp]

theorem FirstOrder.Language.LHom.id_onFunction (L : FirstOrder.Language) (_n : ℕ) (a : L.Functions _n) : (FirstOrder.Language.LHom.id L).onFunction 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.instInhabitedLHom {L : FirstOrder.Language} : Inhabited (L →ᴸ L)

Equations

• FirstOrder.Language.LHom.instInhabitedLHom = { 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 →ᴸ FirstOrder.Language.sum L 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' →ᴸ FirstOrder.Language.sum L 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) [FirstOrder.Language.IsAlgebraic L] [FirstOrder.Language.IsRelational L] (n : ℕ) (a : L.Functions n) : (FirstOrder.Language.LHom.ofIsEmpty L L').onFunction a = IsEmpty.elim ⋯ a

@[simp]

theorem FirstOrder.Language.LHom.ofIsEmpty_onRelation (L : FirstOrder.Language) (L' : FirstOrder.Language) [FirstOrder.Language.IsAlgebraic L] [FirstOrder.Language.IsRelational L] (n : ℕ) (a : L.Relations n) : (FirstOrder.Language.LHom.ofIsEmpty L L').onRelation a = IsEmpty.elim ⋯ a

def FirstOrder.Language.LHom.ofIsEmpty (L : FirstOrder.Language) (L' : FirstOrder.Language) [FirstOrder.Language.IsAlgebraic L] [FirstOrder.Language.IsRelational L] : 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) => IsEmpty.elim ⋯ a, onRelation := fun (n : ℕ) (a : L.Relations n) => IsEmpty.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.instUniqueLHom {L : FirstOrder.Language} {L' : FirstOrder.Language} [FirstOrder.Language.IsAlgebraic L] [FirstOrder.Language.IsRelational L] : Unique (L →ᴸ L')

Equations

• FirstOrder.Language.LHom.instUniqueLHom = { toInhabited := { 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.Constants (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂)), 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) : (FirstOrder.Language.LHom.comp g 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), (FirstOrder.Language.LHom.comp g 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

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.LHom.comp_id {L : FirstOrder.Language} {L' : FirstOrder.Language} (F : L →ᴸ L') : FirstOrder.Language.LHom.comp F (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') : FirstOrder.Language.LHom.comp (FirstOrder.Language.LHom.comp F G) H = FirstOrder.Language.LHom.comp F (FirstOrder.Language.LHom.comp G 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), (FirstOrder.Language.LHom.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), (FirstOrder.Language.LHom.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') : FirstOrder.Language.sum L 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') : FirstOrder.Language.LHom.comp (FirstOrder.Language.LHom.sumElim ϕ ψ) FirstOrder.Language.LHom.sumInl = ϕ

theorem FirstOrder.Language.LHom.sumElim_comp_inr {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') : FirstOrder.Language.LHom.comp (FirstOrder.Language.LHom.sumElim ϕ ψ) FirstOrder.Language.LHom.sumInr = ψ

theorem FirstOrder.Language.LHom.sumElim_inl_inr {L : FirstOrder.Language} {L' : FirstOrder.Language} : FirstOrder.Language.LHom.sumElim FirstOrder.Language.LHom.sumInl FirstOrder.Language.LHom.sumInr = FirstOrder.Language.LHom.id (FirstOrder.Language.sum L 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) : FirstOrder.Language.LHom.comp θ (FirstOrder.Language.LHom.sumElim ϕ ψ) = FirstOrder.Language.LHom.sumElim (FirstOrder.Language.LHom.comp θ ϕ) (FirstOrder.Language.LHom.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), (FirstOrder.Language.LHom.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), (FirstOrder.Language.LHom.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₂) : FirstOrder.Language.sum L L₁ →ᴸ FirstOrder.Language.sum L' 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₂) : FirstOrder.Language.LHom.comp (FirstOrder.Language.LHom.sumMap ϕ ψ) FirstOrder.Language.LHom.sumInl = FirstOrder.Language.LHom.comp FirstOrder.Language.LHom.sumInl ϕ

@[simp]

theorem FirstOrder.Language.LHom.sumMap_comp_inr {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) : FirstOrder.Language.LHom.comp (FirstOrder.Language.LHom.sumMap ϕ ψ) FirstOrder.Language.LHom.sumInr = FirstOrder.Language.LHom.comp FirstOrder.Language.LHom.sumInr ψ

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

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] [FirstOrder.Language.Structure L M] : FirstOrder.Language.Structure L' 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) [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L' 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

@[simp]

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

Equations

• ⋯ = ⋯

instance FirstOrder.Language.LHom.ofIsEmpty_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type u_1) [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L' M] [FirstOrder.Language.IsAlgebraic L] [FirstOrder.Language.IsRelational L] : FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.LHom.ofIsEmpty L L') 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) [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L' M] [FirstOrder.Language.Structure L'' M] [FirstOrder.Language.LHom.IsExpansionOn ϕ M] [FirstOrder.Language.LHom.IsExpansionOn ψ M] : FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.LHom.sumElim ϕ ψ) 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) [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L' M] [FirstOrder.Language.Structure L₁ M] [FirstOrder.Language.Structure L₂ M] [FirstOrder.Language.LHom.IsExpansionOn ϕ M] [FirstOrder.Language.LHom.IsExpansionOn ψ M] : FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.LHom.sumMap ϕ ψ) M

Equations

• ⋯ = ⋯

instance FirstOrder.Language.LHom.sumInl_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type u_1) [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L' M] : FirstOrder.Language.LHom.IsExpansionOn FirstOrder.Language.LHom.sumInl M

Equations

• ⋯ = ⋯

instance FirstOrder.Language.LHom.sumInr_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type u_1) [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L' M] : FirstOrder.Language.LHom.IsExpansionOn FirstOrder.Language.LHom.sumInr M

Equations

• ⋯ = ⋯

@[simp]

theorem FirstOrder.Language.LHom.funMap_sumInl {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure (FirstOrder.Language.sum L L') M] [FirstOrder.Language.LHom.IsExpansionOn FirstOrder.Language.LHom.sumInl 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} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure (FirstOrder.Language.sum L' L) M] [FirstOrder.Language.LHom.IsExpansionOn FirstOrder.Language.LHom.sumInr 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.Injective FirstOrder.Language.LHom.sumInl

theorem FirstOrder.Language.LHom.sumInr_injective {L : FirstOrder.Language} {L' : FirstOrder.Language} : FirstOrder.Language.LHom.Injective FirstOrder.Language.LHom.sumInr

instance FirstOrder.Language.LHom.isExpansionOn_reduct {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') (M : Type u_1) [FirstOrder.Language.Structure L' M] : FirstOrder.Language.LHom.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 : FirstOrder.Language.LHom.Injective ϕ) (M : Type u_1) [Inhabited M] [FirstOrder.Language.Structure L M] : FirstOrder.Language.LHom.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 : FirstOrder.Language.LHom.comp self.invLHom self.toLHom = FirstOrder.Language.LHom.id L
• right_inv : FirstOrder.Language.LHom.comp self.toLHom 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.instInhabitedLEquiv {L : FirstOrder.Language} : Inhabited (L ≃ᴸ L)

Equations

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

@[simp]

theorem FirstOrder.Language.LEquiv.symm_toLHom {L : FirstOrder.Language} {L' : FirstOrder.Language} (e : L ≃ᴸ L') : (FirstOrder.Language.LEquiv.symm e).toLHom = e.invLHom

@[simp]

theorem FirstOrder.Language.LEquiv.symm_invLHom {L : FirstOrder.Language} {L' : FirstOrder.Language} (e : L ≃ᴸ L') : (FirstOrder.Language.LEquiv.symm e).invLHom = e.toLHom

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

• FirstOrder.Language.LEquiv.symm e = { 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'') : (FirstOrder.Language.LEquiv.trans e e').invLHom = FirstOrder.Language.LHom.comp e.invLHom e'.invLHom

@[simp]

theorem FirstOrder.Language.LEquiv.trans_toLHom {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (e : L ≃ᴸ L') (e' : L' ≃ᴸ L'') : (FirstOrder.Language.LEquiv.trans e e').toLHom = FirstOrder.Language.LHom.comp e'.toLHom 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

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

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.Constants (FirstOrder.Language.constantsOn α) = α

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

Equations

• ⋯ = ⋯

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

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.card (FirstOrder.Language.constantsOn α) = Cardinal.mk α

def FirstOrder.Language.constantsOn.structure {M : Type w} {α : Type u'} (f : α → M) : FirstOrder.Language.Structure (FirstOrder.Language.constantsOn α) 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.IsExpansionOn (FirstOrder.Language.LHom.constantsOnMap f) 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

• FirstOrder.Language.withConstants L α = FirstOrder.Language.sum L (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') : FirstOrder.Language.card (FirstOrder.Language.withConstants L α) = Cardinal.lift.{w', max u v} (FirstOrder.Language.card L) + Cardinal.lift.{max u v, w'} (Cardinal.mk α)

@[simp]

theorem FirstOrder.Language.lhomWithConstants_onFunction (L : FirstOrder.Language) (α : Type w') (_n : ℕ) (val : L.Functions _n) : (FirstOrder.Language.lhomWithConstants L α).onFunction val = Sum.inl val

@[simp]

theorem FirstOrder.Language.lhomWithConstants_onRelation (L : FirstOrder.Language) (α : Type w') (_n : ℕ) (val : L.Relations _n) : (FirstOrder.Language.lhomWithConstants L α).onRelation val = Sum.inl val

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

The language map adding constants.

Equations

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

theorem FirstOrder.Language.lhomWithConstants_injective (L : FirstOrder.Language) (α : Type w') : FirstOrder.Language.LHom.Injective (FirstOrder.Language.lhomWithConstants L α)

def FirstOrder.Language.con (L : FirstOrder.Language) {α : Type w'} (a : α) : FirstOrder.Language.Constants (FirstOrder.Language.withConstants L α)

The constant symbol indexed by a particular element.

Equations

• FirstOrder.Language.con L a = Sum.inr a

def FirstOrder.Language.LHom.addConstants {L : FirstOrder.Language} (α : Type w') {L' : FirstOrder.Language} (φ : L →ᴸ L') : FirstOrder.Language.withConstants L α →ᴸ FirstOrder.Language.withConstants L' α

Adds constants to a language map.

Equations

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

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

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.sumElim (FirstOrder.Language.LHom.id L) (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 = FirstOrder.Language.lhomWithConstants L α

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

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} [FirstOrder.Language.Structure L M] {α : Type w'} [FirstOrder.Language.Structure (FirstOrder.Language.withConstants L α) M] [FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.lhomWithConstants L α) 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} [FirstOrder.Language.Structure L M] {α : Type w'} [FirstOrder.Language.Structure (FirstOrder.Language.withConstants L α) M] [FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.lhomWithConstants L α) 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 : α → β) : FirstOrder.Language.withConstants L α →ᴸ FirstOrder.Language.withConstants L β

The language map extending the constant set.

Equations

• FirstOrder.Language.lhomWithConstantsMap L f = FirstOrder.Language.LHom.sumMap (FirstOrder.Language.LHom.id L) (FirstOrder.Language.LHom.constantsOnMap f)

@[simp]

theorem FirstOrder.Language.LHom.map_constants_comp_sumInl (L : FirstOrder.Language) {α : Type w'} {β : Type u_1} {f : α → β} : FirstOrder.Language.LHom.comp (FirstOrder.Language.lhomWithConstantsMap L f) FirstOrder.Language.LHom.sumInl = FirstOrder.Language.lhomWithConstants L β

instance FirstOrder.Language.constantsOnSelfStructure {M : Type w} : FirstOrder.Language.Structure (FirstOrder.Language.constantsOn M) M

Equations

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

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

Equations

• FirstOrder.Language.withConstantsSelfStructure L = FirstOrder.Language.sumStructure L (FirstOrder.Language.constantsOn M) M

instance FirstOrder.Language.withConstants_self_expansion (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] : FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.lhomWithConstants L M) M

Equations

• ⋯ = ⋯

instance FirstOrder.Language.withConstantsStructure (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] (α : Type u_1) [FirstOrder.Language.Structure (FirstOrder.Language.constantsOn α) M] : FirstOrder.Language.Structure (FirstOrder.Language.withConstants L α) M

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

theorem FirstOrder.Language.withConstants_funMap_sum_inr (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] (α : Type u_1) [FirstOrder.Language.Structure (FirstOrder.Language.constantsOn α) M] {a : α} {x : Fin 0 → M} : FirstOrder.Language.Structure.funMap (Sum.inr a) x = ↑(FirstOrder.Language.con L a)

@[simp]

theorem FirstOrder.Language.coe_con (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] (A : Set M) {a : ↑A} : ↑(FirstOrder.Language.con L a) = ↑a

instance FirstOrder.Language.constantsOnMap_inclusion_isExpansionOn {M : Type w} {A : Set M} {B : Set M} (h : A ⊆ B) : FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.LHom.constantsOnMap (Set.inclusion h)) M

Equations

• ⋯ = ⋯

instance FirstOrder.Language.map_constants_inclusion_isExpansionOn (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {B : Set M} (h : A ⊆ B) : FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.lhomWithConstantsMap L (Set.inclusion h)) M

Equations

• ⋯ = ⋯