Expansions along composite language maps, and language maps for adjoining constants

Additions to Mathlib's Mathlib.ModelTheory.LanguageMap: expansions compose along composite language maps, and the reduct of an expansion along a composite h.comp g along the outer map h is an expansion along the inner map g. Together they say that an L''-structure expands an L-structure along h.comp g exactly when it expands, along h, some L'-structure that expands the L-structure along g; the L'-structure can be taken to be the reduct.

Main results

• FirstOrder.Language.LHom.comp_isExpansionOn: expansions along g and along h compose to an expansion along h.comp g.
• FirstOrder.Language.LHom.isExpansionOn_reduct_of_comp: the reduct along h of an expansion along h.comp g is an expansion along g.
• FirstOrder.Language.LHom.id_isExpansionOn_reduct: the reduct of an expansion along the map it expands along is the original structure.
• FirstOrder.Language.LHom.sumMap_isExpansionOn_of_reduct: a structure on a sum language is expanded along ϕ.sumMap ψ by a sum structure expanding its two parts along ϕ and ψ.
• FirstOrder.Language.LHom.mem_range_sumInl_onFunction_of_mem_range_sumMap and FirstOrder.Language.LHom.mem_range_sumInl_onRelation_of_mem_range_sumMap: the symbols of L.sum (L₁.sum L₂) shared by the images of L.sum L₁ and L.sum L₂ come from L.

The relation map of lhomWithConstants inverts the elimination of the empty summand of L[[γ]].Relations n by Equiv.sumEmpty (FirstOrder.Language.lhomWithConstants_onRelation_sumEmpty), symbol sets of L[[γ]] avoiding the added constants lie in the range of lhomWithConstants (FirstOrder.Language.subset_range_lhomWithConstants_onFunction, FirstOrder.Language.subset_range_lhomWithConstants_onRelation), and every L[[γ]]-structure is the expansion of its L-reduct by the interpretations of the added constants (FirstOrder.Language.withConstantsStructure_reduct_eq).

instance FirstOrder.Language.LHom.comp_isExpansionOn {L : Language} {L' : Language} {L'' : Language} (h : L' →ᴸ L'') (g : L →ᴸ L') (M : Type w) [L.Structure M] [L'.Structure M] [L''.Structure M] [g.IsExpansionOn M] [h.IsExpansionOn M] : (h.comp g).IsExpansionOn M

Expansions compose: if the L'-structure on M expands its L-structure along g, and the L''-structure expands the L'-structure along h, then the L''-structure expands the L-structure along h.comp g.

theorem FirstOrder.Language.LHom.isExpansionOn_reduct_of_comp {L : Language} {L' : Language} {L'' : Language} (h : L' →ᴸ L'') (g : L →ᴸ L') (M : Type w) [L.Structure M] [L''.Structure M] [(h.comp g).IsExpansionOn M] : g.IsExpansionOn M

If the L''-structure on M expands its L-structure along h.comp g, then its reduct along h expands the L-structure along g.

theorem FirstOrder.Language.LHom.id_isExpansionOn_reduct {L : Language} {L' : Language} (g : L →ᴸ L') (M : Type w) [L.Structure M] [L'.Structure M] [g.IsExpansionOn M] : (LHom.id L).IsExpansionOn M

If the L'-structure on M expands its L-structure along g, then its reduct along g is the L-structure again, in the sense that the identity map expands the reduct to it.

theorem FirstOrder.Language.LHom.sumMap_isExpansionOn_of_reduct {L : Language} {L₀ : Language} {L₁ : Language} {L₁' : Language} (ϕ : L →ᴸ L₀) (ψ : L₁ →ᴸ L₁') (M : Type w) [(L.sum L₁).Structure M] [L₀.Structure M] [L₁'.Structure M] [ϕ.IsExpansionOn M] [ψ.IsExpansionOn M] : (ϕ.sumMap ψ).IsExpansionOn M

A structure on L.sum L₁ is expanded along ϕ.sumMap ψ by the sum of an L₀-structure and an L₁'-structure that expand, along ϕ and ψ, its parts on L and on L₁. Mathlib's LHom.sumMap_isExpansionOn is the case of a source that is itself a sum structure.

theorem FirstOrder.Language.LHom.mem_range_sumInl_onFunction_of_mem_range_sumMap {L : Language} {L₁ : Language} {L₂ : Language} {s : (k : ℕ) × (L.sum (L₁.sum L₂)).Functions k} (h₁ : s ∈ Set.range fun (t : (k : ℕ) × (L.sum L₁).Functions k) => ⟨t.fst, ((LHom.id L).sumMap LHom.sumInl).onFunction t.snd⟩) (h₂ : s ∈ Set.range fun (t : (k : ℕ) × (L.sum L₂).Functions k) => ⟨t.fst, ((LHom.id L).sumMap LHom.sumInr).onFunction t.snd⟩) : s ∈ Set.range fun (t : (k : ℕ) × L.Functions k) => ⟨t.fst, LHom.sumInl.onFunction t.snd⟩

A function symbol of L.sum (L₁.sum L₂) that is the image of a function symbol of L.sum L₁ along (LHom.id L).sumMap LHom.sumInl and of a function symbol of L.sum L₂ along (LHom.id L).sumMap LHom.sumInr is the image of a function symbol of L along LHom.sumInl.

theorem FirstOrder.Language.LHom.mem_range_sumInl_onRelation_of_mem_range_sumMap {L : Language} {L₁ : Language} {L₂ : Language} {s : (k : ℕ) × (L.sum (L₁.sum L₂)).Relations k} (h₁ : s ∈ Set.range fun (t : (k : ℕ) × (L.sum L₁).Relations k) => ⟨t.fst, ((LHom.id L).sumMap LHom.sumInl).onRelation t.snd⟩) (h₂ : s ∈ Set.range fun (t : (k : ℕ) × (L.sum L₂).Relations k) => ⟨t.fst, ((LHom.id L).sumMap LHom.sumInr).onRelation t.snd⟩) : s ∈ Set.range fun (t : (k : ℕ) × L.Relations k) => ⟨t.fst, LHom.sumInl.onRelation t.snd⟩

A relation symbol of L.sum (L₁.sum L₂) that is the image of a relation symbol of L.sum L₁ along (LHom.id L).sumMap LHom.sumInl and of a relation symbol of L.sum L₂ along (LHom.id L).sumMap LHom.sumInr is the image of a relation symbol of L along LHom.sumInl.

theorem FirstOrder.Language.lhomWithConstants_onRelation_sumEmpty {L : Language} {γ : Type u_1} {l : ℕ} (R : (L.withConstants γ).Relations l) : (L.lhomWithConstants γ).onRelation ((Equiv.sumEmpty (L.Relations l) ((constantsOn γ).Relations l)) R) = R

theorem FirstOrder.Language.subset_range_lhomWithConstants_onFunction {L : Language} {γ : Type u_1} {X : Set ((k : ℕ) × (L.withConstants γ).Functions k)} (hX : ∀ (c : γ), ⟨0, L.con c⟩ ∉ X) : X ⊆ Set.range fun (s : (k : ℕ) × L.Functions k) => ⟨s.fst, (L.lhomWithConstants γ).onFunction s.snd⟩

Any set of arity-tagged function symbols of L[[γ]] containing none of the added constants L.con c lies in the range of (L.lhomWithConstants γ).onFunction.

theorem FirstOrder.Language.subset_range_lhomWithConstants_onRelation {L : Language} {γ : Type u_1} (Y : Set ((k : ℕ) × (L.withConstants γ).Relations k)) : Y ⊆ Set.range fun (s : (k : ℕ) × L.Relations k) => ⟨s.fst, (L.lhomWithConstants γ).onRelation s.snd⟩

Every set of arity-tagged relation symbols of L[[γ]] lies in the range of (L.lhomWithConstants γ).onRelation.

theorem FirstOrder.Language.withConstantsStructure_reduct_eq {L : Language} {γ : Type u_1} (M : Type u_2) [S : (L.withConstants γ).Structure M] : L.withConstantsStructure γ = S

Every L[[γ]]-structure on M is the expansion of its L-reduct interpreting each c : γ as (L.con c : M).