Documentation

TauCeti.ModelTheory.RelationalConfiguration.Structure

Decoding relational configurations #

For a relational language, RelationalConfiguration.toStructure and the existing RelationalConfiguration.ofStructure identify configurations with all structures on the fixed carrier. Decoding is explicit: different configurations describe different structures on the same type. Empty carriers and nullary relations are included.

Equiv.encodeVia represents a structure on a bijective carrier. It preserves infinitary sentences, so structures in arbitrary universes can be represented on standard finite or countably infinite carriers. Transport reuses Mathlib's Equiv.inducedStructure and Equiv.inducedStructureEquiv.

source
@[instance_reducible]
def TauCeti.RelationalConfiguration.toStructure {L : FirstOrder.Language} {V : Type w} [L.IsRelational] (c : RelationalConfiguration L V) :
L.Structure V

Decode a configuration into a relational structure, without installing an instance.

Instances For
    source
    @[simp]
    theorem TauCeti.RelationalConfiguration.toStructure_relMap {L : FirstOrder.Language} {V : Type w} [L.IsRelational] (c : RelationalConfiguration L V) {n : ℕ} (R : L.Relations n) (a : Fin n → V) :
    FirstOrder.Language.Structure.RelMap R a ↔ c.eval (atom R a) = true

    A decoded relation holds exactly when the corresponding atom is true.

    source
    @[simp]
    theorem TauCeti.RelationalConfiguration.ofStructure_toStructure {L : FirstOrder.Language} {V : Type w} [L.IsRelational] (c : RelationalConfiguration L V) :
    ofStructure L V = c

    Encoding after decoding recovers every configuration.

    source
    @[simp]
    theorem TauCeti.RelationalConfiguration.toStructure_ofStructure {L : FirstOrder.Language} {V : Type w} [L.IsRelational] (S : L.Structure V) :
    (ofStructure L V).toStructure = S

    Decoding after encoding recovers the entire structure in a relational language.

    source
    noncomputable def TauCeti.RelationalConfiguration.equivStructure {L : FirstOrder.Language} {V : Type w} [L.IsRelational] :
    RelationalConfiguration L V ≃ L.Structure V

    Configurations and relational structures on a fixed carrier are in bijection.

    Instances For
      source
      @[simp]
      theorem TauCeti.RelationalConfiguration.equivStructure_apply {L : FirstOrder.Language} {V : Type w} [L.IsRelational] (c : RelationalConfiguration L V) :
      equivStructure c = c.toStructure
      source
      @[simp]
      theorem TauCeti.RelationalConfiguration.equivStructure_symm_apply {L : FirstOrder.Language} {V : Type w} [L.IsRelational] (S : L.Structure V) :
      equivStructure.symm S = ofStructure L V
      source
      noncomputable def Equiv.encodeVia {L : FirstOrder.Language} {M : Type w} {V : Type w'} [L.Structure M] (e : M ≃ V) :
      TauCeti.RelationalConfiguration L V

      Encode a structure after transporting it along a bijection of carriers.

      Instances For
        source
        @[simp]
        theorem Equiv.eval_encodeVia {L : FirstOrder.Language} {M : Type w} {V : Type w'} [L.Structure M] (e : M ≃ V) {n : ℕ} (R : L.Relations n) (a : Fin n → V) :
        e.encodeVia.eval (TauCeti.RelationalConfiguration.atom R a) = decide (FirstOrder.Language.Structure.RelMap R (⇑e.symm ∘ a))

        Transport reads a relation at the inverse image of its argument tuple.

        source
        @[simp]
        theorem Equiv.toStructure_encodeVia {L : FirstOrder.Language} {M : Type w} {V : Type w'} [L.Structure M] [L.IsRelational] (e : M ≃ V) :
        e.encodeVia.toStructure = e.inducedStructure

        Decoding a transported configuration gives exactly the induced structure.

        source
        theorem Equiv.nonempty_equiv_encodeVia {L : FirstOrder.Language} {M : Type w} {V : Type w'} [L.Structure M] [L.IsRelational] (e : M ≃ V) :
        Nonempty (L.Equiv M V)

        A transported configuration names a structure isomorphic to the original in any universe.

        source
        @[simp]
        theorem Equiv.encodeVia_refl {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
        (Equiv.refl M).encodeVia = TauCeti.RelationalConfiguration.ofStructure L M

        Encoding through the identity is encoding the original structure.

        source
        theorem Equiv.encodeVia_trans {L : FirstOrder.Language} {M : Type w} {V : Type w'} {W : Type w''} [L.Structure M] (e : M ≃ V) (f : V ≃ W) :
        (e.trans f).encodeVia = f.encodeVia

        Successive carrier transports agree with transport along the composite bijection.

        source
        theorem Equiv.realize_encodeVia {L : FirstOrder.Language} {M : Type w} {V : Type w'} [L.Structure M] [L.IsRelational] {ι : Type uι} (e : M ≃ V) (φ : L.SentenceInf ι) :
        φ.Realize V ↔ φ.Realize M

        Carrier transport preserves every infinitary sentence, including on empty types.