English
Ultrahomogeneity is equivalent to the extension property for L-structures under equivalences.
Русский
Ультрахомогенность эквивалентна свойству расширения под эквивалентностями структур L.
LaTeX
$$$$ L.IsUltrahomogeneous M \\iff L.IsExtensionPair M M. $$$$
Lean4
theorem isSatisfiable_union_distinctConstantsTheory_of_card_le (T : L.Theory) (s : Set α) (M : Type w') [Nonempty M]
[L.Structure M] [M ⊨ T] (h : Cardinal.lift.{w'} #s ≤ Cardinal.lift.{w} #M) :
((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable :=
by
haveI : Inhabited M := Classical.inhabited_of_nonempty inferInstance
rw [Cardinal.lift_mk_le'] at h
letI : (constantsOn α).Structure M := constantsOn.structure (Function.extend (↑) h.some default)
have : M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s :=
by
refine ((LHom.onTheory_model _ _).2 inferInstance).union ?_
rw [model_distinctConstantsTheory]
refine fun a as b bs ab => ?_
rw [← Subtype.coe_mk a as, ← Subtype.coe_mk b bs, ← Subtype.ext_iff]
exact
h.some.injective
((Subtype.coe_injective.extend_apply h.some default ⟨a, as⟩).symm.trans
(ab.trans (Subtype.coe_injective.extend_apply h.some default ⟨b, bs⟩)))
exact Model.isSatisfiable M
