Documentation

InfinitaryLogic.Descriptive.CodeTransport

Transport of codes along equivalences (generic StructureSpaceOn API) #

The generic transport API for coded structures: given an L-structure on M and a bijection e : M ≃ α, encodeViaEquiv e is the code on α obtained by pushing the structure forward along e. Its decoded structure is the induced structure, it satisfies the same sentences, and it is L-isomorphic to the source.

These were previously private in Descriptive/FiniteCarrier.lean; they are not finite-specific and are the transport layer the López–Escobar converse (issue #10) consumes, so they live here at the StructureSpaceOn level.

source
noncomputable def FirstOrder.Language.StructureSpaceOn.encodeViaEquiv {L : Language} [L.IsRelational] {M : Type u_1} [L.Structure M] {α : Type u_2} (e : M ≃ α) :
L.StructureSpaceOn α

Transport a structure along a bijection and encode it: the resulting code on α decodes to a structure L-isomorphic to the source.

Equations
Instances For
    source
    theorem FirstOrder.Language.StructureSpaceOn.toStructure_encodeViaEquiv_eq {L : Language} [L.IsRelational] {M : Type u_1} [L.Structure M] {α : Type u_2} (e : M ≃ α) :
    (encodeViaEquiv e).toStructure = e.inducedStructure

    The decoded structure from encodeViaEquiv is the induced structure.

    source
    theorem FirstOrder.Language.StructureSpaceOn.encodeViaEquiv_models {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {α : Type w} [Countable α] {φ : L.Sentenceω} (e : M ≃ α) (hφ : φ.Realize M) :
    φ.Realize α

    The encoded structure via an equivalence satisfies the same sentences.

    source
    theorem FirstOrder.Language.StructureSpaceOn.encodeViaEquiv_iso {L : Language} [L.IsRelational] {M : Type u_1} [L.Structure M] {α : Type u_2} (e : M ≃ α) :
    Nonempty (L.Equiv M α)

    The encoded structure is L-isomorphic to the source via the equivalence.