Isomorphism invariance of infinitary satisfaction

An isomorphism of first-order structures preserves realization of infinitary formulas, with both free and bound valuations transported along the isomorphism. In particular, isomorphic structures satisfy the same infinitary sentences. The branching carrier and the two structure universes are independent, and neither structure needs to be nonempty.

These results allow characteristic sentences of structures to be transported to their isomorphic copies. They apply to languages with functions as well as relational languages.

The API and the atomic cases follow Mathlib's StrongHomClass.realize_boundedFormula, realize_formula, and realize_sentence in Mathlib/ModelTheory/Semantics.lean (Aaron Anderson, Jesse Michael Han, Floris van Doorn). Infinitary conjunctions and disjunctions additionally require preservation of realization at every branch.

@[simp]

theorem FirstOrder.Language.StrongHomClass.realize_boundedFormulaInf {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {F : Type u_1} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) (φ : L.BoundedFormulaInf ι α n) {v : α → M} {xs : Fin n → M} : φ.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ φ.Realize v xs

Isomorphisms preserve realization of infinitary bounded formulas when both valuations are transported along the isomorphism.

@[simp]

theorem FirstOrder.Language.StrongHomClass.realize_formulaInf {L : Language} {ι : Type uι} {α : Type u'} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {F : Type u_1} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) (φ : L.FormulaInf ι α) {v : α → M} : φ.Realize (⇑g ∘ v) ↔ φ.Realize v

Isomorphisms preserve realization of infinitary formulas under transported free valuations.

theorem FirstOrder.Language.StrongHomClass.realize_sentenceInf {L : Language} {ι : Type uι} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {F : Type u_1} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) (φ : L.SentenceInf ι) : φ.Realize M ↔ φ.Realize N

Isomorphic structures satisfy the same infinitary sentences.