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

• onFunction : ⦃n : ℕ⦄ → FirstOrder.Language.Functions L n → FirstOrder.Language.Functions L' n
• onRelation : ⦃n : ℕ⦄ → FirstOrder.Language.Relations L n → FirstOrder.Language.Relations L' n

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

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

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

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₁ → FirstOrder.Language.Functions L' 1) (φ₂ : f₂ → FirstOrder.Language.Functions L' 2) (φ₁' : r₁ → FirstOrder.Language.Relations L' 1) (φ₂' : r₂ → FirstOrder.Language.Relations L' 2) : FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂ →ᴸ L'

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

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.

@[simp]

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

@[simp]

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

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

The identity language homomorphism.

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

@[simp]

theorem FirstOrder.Language.LHom.sumInl_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ℕ) (val : FirstOrder.Language.Functions L _n) : FirstOrder.Language.LHom.onFunction FirstOrder.Language.LHom.sumInl val = Sum.inl val

@[simp]

theorem FirstOrder.Language.LHom.sumInl_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ℕ) (val : FirstOrder.Language.Relations L _n) : FirstOrder.Language.LHom.onRelation FirstOrder.Language.LHom.sumInl 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.

@[simp]

theorem FirstOrder.Language.LHom.sumInr_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ℕ) (val : FirstOrder.Language.Relations L' _n) : FirstOrder.Language.LHom.onRelation FirstOrder.Language.LHom.sumInr val = Sum.inr val

@[simp]

theorem FirstOrder.Language.LHom.sumInr_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ℕ) (val : FirstOrder.Language.Functions L' _n) : FirstOrder.Language.LHom.onFunction FirstOrder.Language.LHom.sumInr 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.

@[simp]

theorem FirstOrder.Language.LHom.ofIsEmpty_onFunction (L : FirstOrder.Language) (L' : FirstOrder.Language) [FirstOrder.Language.IsAlgebraic L] [FirstOrder.Language.IsRelational L] (n : ℕ) (a : FirstOrder.Language.Functions L n) : FirstOrder.Language.LHom.onFunction (FirstOrder.Language.LHom.ofIsEmpty L L') a = IsEmpty.elim (_ : IsEmpty (FirstOrder.Language.Functions L n)) a

@[simp]

theorem FirstOrder.Language.LHom.ofIsEmpty_onRelation (L : FirstOrder.Language) (L' : FirstOrder.Language) [FirstOrder.Language.IsAlgebraic L] [FirstOrder.Language.IsRelational L] (n : ℕ) (a : FirstOrder.Language.Relations L n) : FirstOrder.Language.LHom.onRelation (FirstOrder.Language.LHom.ofIsEmpty L L') a = IsEmpty.elim (_ : IsEmpty (FirstOrder.Language.Relations L n)) 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.

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

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 : FirstOrder.Language.Constants (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂)), FirstOrder.Language.LHom.onFunction F c = FirstOrder.Language.LHom.onFunction G c) (h1 : ∀ (f : FirstOrder.Language.Functions (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) 1), FirstOrder.Language.LHom.onFunction F f = FirstOrder.Language.LHom.onFunction G f) (h2 : ∀ (f : FirstOrder.Language.Functions (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) 2), FirstOrder.Language.LHom.onFunction F f = FirstOrder.Language.LHom.onFunction G f) (h1' : ∀ (r : FirstOrder.Language.Relations (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) 1), FirstOrder.Language.LHom.onRelation F r = FirstOrder.Language.LHom.onRelation G r) (h2' : ∀ (r : FirstOrder.Language.Relations (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) 2), FirstOrder.Language.LHom.onRelation F r = FirstOrder.Language.LHom.onRelation G 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 : FirstOrder.Language.Functions L _n) : FirstOrder.Language.LHom.onFunction (FirstOrder.Language.LHom.comp g f) F = FirstOrder.Language.LHom.onFunction g (FirstOrder.Language.LHom.onFunction f 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 : FirstOrder.Language.Relations L x), FirstOrder.Language.LHom.onRelation (FirstOrder.Language.LHom.comp g f) R = FirstOrder.Language.LHom.onRelation g (FirstOrder.Language.LHom.onRelation f 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.

@[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 : FirstOrder.Language.Functions L _n ⊕ FirstOrder.Language.Functions L'' _n), FirstOrder.Language.LHom.onFunction (FirstOrder.Language.LHom.sumElim ϕ ψ) a = Sum.elim (fun f => FirstOrder.Language.LHom.onFunction ϕ f) (fun f => FirstOrder.Language.LHom.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 : FirstOrder.Language.Relations L _n ⊕ FirstOrder.Language.Relations L'' _n), FirstOrder.Language.LHom.onRelation (FirstOrder.Language.LHom.sumElim ϕ ψ) a = Sum.elim (fun f => FirstOrder.Language.LHom.onRelation ϕ f) (fun f => FirstOrder.Language.LHom.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.

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 : FirstOrder.Language.Relations L _n ⊕ FirstOrder.Language.Relations L₁ _n), FirstOrder.Language.LHom.onRelation (FirstOrder.Language.LHom.sumMap ϕ ψ) a = Sum.map (fun f => FirstOrder.Language.LHom.onRelation ϕ f) (fun f => FirstOrder.Language.LHom.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 : FirstOrder.Language.Functions L _n ⊕ FirstOrder.Language.Functions L₁ _n), FirstOrder.Language.LHom.onFunction (FirstOrder.Language.LHom.sumMap ϕ ψ) a = Sum.map (fun f => FirstOrder.Language.LHom.onFunction ϕ f) (fun f => FirstOrder.Language.LHom.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.

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

• onFunction : ∀ {n : ℕ}, Function.Injective fun f => FirstOrder.Language.LHom.onFunction ϕ f
• onRelation : ∀ {n : ℕ}, Function.Injective fun R => FirstOrder.Language.LHom.onRelation ϕ R

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

noncomputable def FirstOrder.Language.LHom.defaultExpansion {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') [(n : ℕ) → (f : FirstOrder.Language.Functions L' n) → Decidable (f ∈ Set.range fun f => FirstOrder.Language.LHom.onFunction ϕ f)] [(n : ℕ) → (r : FirstOrder.Language.Relations L' n) → Decidable (r ∈ Set.range fun r => FirstOrder.Language.LHom.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.

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

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

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

@[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 : FirstOrder.Language.Functions L n) (x : Fin n → M) : FirstOrder.Language.Structure.funMap (FirstOrder.Language.LHom.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 : FirstOrder.Language.Relations L n) (x : Fin n → M) : FirstOrder.Language.Structure.RelMap (FirstOrder.Language.LHom.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

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

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

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

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

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

@[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 : FirstOrder.Language.Functions L 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 : FirstOrder.Language.Functions L 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

theorem FirstOrder.Language.LHom.Injective.isExpansionOn_default {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} [(n : ℕ) → (f : FirstOrder.Language.Functions L' n) → Decidable (f ∈ Set.range fun f => FirstOrder.Language.LHom.onFunction ϕ f)] [(n : ℕ) → (r : FirstOrder.Language.Relations L' n) → Decidable (r ∈ Set.range fun r => FirstOrder.Language.LHom.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)

• toLHom : L →ᴸ L'
• invLHom : L' →ᴸ L
• left_inv : FirstOrder.Language.LHom.comp s.invLHom s.toLHom = FirstOrder.Language.LHom.id L
• right_inv : FirstOrder.Language.LHom.comp s.toLHom s.invLHom = FirstOrder.Language.LHom.id L'

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

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.LEquiv.refl_invLHom (L : FirstOrder.Language) : (FirstOrder.Language.LEquiv.refl L).invLHom = 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.

instance FirstOrder.Language.LEquiv.instInhabitedLEquiv {L : FirstOrder.Language} : Inhabited (L ≃ᴸ 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.

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

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

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.

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

A language with constants indexed by a type.

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

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

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

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.

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.

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.

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

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

@[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_onRelation (L : FirstOrder.Language) (α : Type w') (_n : ℕ) (val : FirstOrder.Language.Relations L _n) : FirstOrder.Language.LHom.onRelation (FirstOrder.Language.lhomWithConstants L α) val = Sum.inl val

@[simp]

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

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

The language map adding constants.

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.

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.

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

@[simp]

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

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

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.

@[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 : FirstOrder.Language.Functions L 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 : FirstOrder.Language.Relations L 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.

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

instance FirstOrder.Language.withConstantsSelfStructure (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] : FirstOrder.Language.Structure (FirstOrder.Language.withConstants L 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

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

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

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

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

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

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

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