The relativized expansion over the doubled universe is the expansion

The point of DescriptiveComplexity.Draw.relExp, discharged: over the doubled universe of DescriptiveComplexity.Draw.dblInterp its points are the original expansion's points over the instance, and its relations are the original's (DescriptiveComplexity.Draw.relExpMapEquiv).

Three things make that work, and each was arranged for it. A doubled universe always has a marked part, so the fallback tag contributes no point. A point's assignment is supported, so it is the extension of a unique assignment of the instance. And every sentence the expansion is made of transports by DescriptiveComplexity.Draw.realize_relOldBlock – the domain sentence at one copy of the block, and each defining sentence at n copies, where the extension commutes with replication exactly.

theorem DescriptiveComplexity.Draw.extAssign_replicateAssign {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} {n : ℕ} (ρs : Fin n → X.B.Assignment A) : extAssign (X.B.replicateAssign ρs) = X.B.replicateAssign fun (i : Fin n) => extAssign (ρs i)

Extending commutes with replication, exactly: the index type of a replicated block is a plain product and the extension acts coordinate by coordinate.

theorem DescriptiveComplexity.Draw.not_domHolds_none {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] (ρ : X.B.Assignment ((dblInterp L).Map A)) : ¬ExpExpansion.DomHolds (none, ρ)

The fallback tag contributes no point over a doubled universe: there is always a marked element.

theorem DescriptiveComplexity.Draw.supported_of_domHolds {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {t : X.Tag} {ρ : X.B.Assignment ((dblInterp L).Map A)} (h : ExpExpansion.DomHolds (some t, ρ)) : Supported ρ

A point's assignment is supported: that is what the domain sentence's second conjunct says.

theorem DescriptiveComplexity.Draw.domHolds_relExp_iff {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (t : X.Tag) (ρ₀ : X.B.Assignment A) : ExpExpansion.DomHolds (some t, extAssign ρ₀) ↔ ExpExpansion.DomHolds (t, ρ₀)

A point of the relativized expansion is a point of the expansion, at the extended assignment.

noncomputable def DescriptiveComplexity.Draw.toRelExpPt {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (p : X.Map A) : (relExp X).Map ((dblInterp L).Map A)

A point of the expansion, as a point of the relativized expansion over the doubled universe.

Equations

• DescriptiveComplexity.Draw.toRelExpPt p = ⟨(some (↑p).1, DescriptiveComplexity.Draw.extAssign (↑p).2), ⋯⟩

theorem DescriptiveComplexity.Draw.toRelExpPt_injective {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] : Function.Injective toRelExpPt

theorem DescriptiveComplexity.Draw.toRelExpPt_surjective {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] : Function.Surjective toRelExpPt

noncomputable def DescriptiveComplexity.Draw.relExpMapEquiv {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] : X.E.Equiv (X.Map A) ((relExp X).Map ((dblInterp L).Map A))

The relativized expansion over the doubled universe is the expansion over the instance: the same points, the same relations.

Equations

• DescriptiveComplexity.Draw.relExpMapEquiv = { toEquiv := Equiv.ofBijective DescriptiveComplexity.Draw.toRelExpPt ⋯, map_fun' := ⋯, map_rel' := ⋯ }