Back-and-forth assembly under a fixed row bijection

Over arbitrary row types R, S and fiber families C, D with Lc-structures on every fiber, fix a total row bijection e : R ≃ S. Two tuples a : Fin n → Carrier R C and b : Fin n → Carrier S D are matched along e (Matched e a b) when, coordinatewise, a i is the row r iff b i is the row e r, and a i lies in the fiber (r, τ) iff b i lies in the fiber (e r, τ). Repeated coordinates are allowed.

Fiber back-and-forth data (FiberBF α e a b): for every row r, every label τ, and every finite selection ι : Fin k → Fin n of coordinates lying in the fiber (r, τ) (repetitions allowed), the selected component tuples of a in C r τ and of b in D (e r) τ are back-and-forth equivalent at level α. With k = 0 this includes the empty tuples of every fiber, occupied or not: unoccupied fibers must be α-equivalent as structures.

Theorem (bfEquiv_of_fiberBF): matched tuples with fiber back-and-forth data at level α are back-and-forth equivalent at level α in the assembled language, the same level. The fixed bijection already tracks the owners absent from the tuple, so no level is spent on rows.

The proof is by induction on α. At level 0 every atom of the assembled language is decided by the matching and by one atom of one fiber. At a successor, a move by a row is answered by its image row, and a move by a fiber point is answered by the fiber's own forth (or back) move applied to the canonical enumeration of that fiber's coordinates; every other selection of coordinates in the extended tuple is a relabeling of that one (BFEquiv.relabel), and the other fibers are unchanged up to relabeling. Full-profile bounds and companion matching are outside this module.

Fiber membership and component elements

def FirstOrder.Language.FiberAssembly.InFiber {U R : Type u} {C : R → Label U → Type u} {n : ℕ} (a : Fin n → Carrier R C) (r : R) (τ : Label U) (i : Fin n) : Prop

The coordinate i of a lies in the fiber (r, τ).

Equations

• FirstOrder.Language.FiberAssembly.InFiber a r τ i = ∃ (x : C r τ), a i = FirstOrder.Language.FiberAssembly.Carrier.pt r τ x

noncomputable def FirstOrder.Language.FiberAssembly.elt {U R : Type u} {C : R → Label U → Type u} {n : ℕ} {a : Fin n → Carrier R C} {r : R} {τ : Label U} {i : Fin n} (h : InFiber a r τ i) : C r τ

The component element at a coordinate lying in the fiber (r, τ).

Equations

• FirstOrder.Language.FiberAssembly.elt h = Exists.choose h

theorem FirstOrder.Language.FiberAssembly.elt_spec {U R : Type u} {C : R → Label U → Type u} {n : ℕ} {a : Fin n → Carrier R C} {r : R} {τ : Label U} {i : Fin n} (h : InFiber a r τ i) : a i = Carrier.pt r τ (elt h)

theorem FirstOrder.Language.FiberAssembly.elt_eq {U R : Type u} {C : R → Label U → Type u} {n : ℕ} {a : Fin n → Carrier R C} {r : R} {τ : Label U} {i : Fin n} (h : InFiber a r τ i) {x : C r τ} (hx : a i = Carrier.pt r τ x) : elt h = x

The component element is determined by the coordinate.

theorem FirstOrder.Language.FiberAssembly.inFiber_iff_of_eq_pt {U R : Type u} {C : R → Label U → Type u} {n : ℕ} {a : Fin n → Carrier R C} {i : Fin n} {r₀ : R} {τ₀ : Label U} {x₀ : C r₀ τ₀} (h : a i = Carrier.pt r₀ τ₀ x₀) (r : R) (τ : Label U) : InFiber a r τ i ↔ r = r₀ ∧ τ = τ₀

Membership at a coordinate known to be a fiber point.

theorem FirstOrder.Language.FiberAssembly.not_inFiber_of_eq_row {U R : Type u} {C : R → Label U → Type u} {n : ℕ} {a : Fin n → Carrier R C} {i : Fin n} {r₀ : R} (h : a i = Carrier.row r₀) (r : R) (τ : Label U) : ¬InFiber a r τ i

A row coordinate lies in no fiber.

Matching along a row bijection

def FirstOrder.Language.FiberAssembly.Matched {U R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} (e : R ≃ S) {n : ℕ} (a : Fin n → Carrier R C) (b : Fin n → Carrier S D) : Prop

b is matched to a along e: coordinatewise, rows correspond to image rows and fiber points to points of the image fiber with the same label, in both directions.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.FiberAssembly.Matched.row_iff {U R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} (hm : Matched e a b) (i : Fin n) (r : R) : a i = Carrier.row r ↔ b i = Carrier.row (e r)

theorem FirstOrder.Language.FiberAssembly.Matched.inFiber_iff {U R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} (hm : Matched e a b) (i : Fin n) (r : R) (τ : Label U) : InFiber a r τ i ↔ InFiber b (e r) τ i

noncomputable def FirstOrder.Language.FiberAssembly.Matched.eltB {U R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} (hm : Matched e a b) {r : R} {τ : Label U} {i : Fin n} (h : InFiber a r τ i) : D (e r) τ

The b-side component element at a coordinate of the fiber (r, τ) of a.

Equations

• hm.eltB h = FirstOrder.Language.FiberAssembly.elt ⋯

theorem FirstOrder.Language.FiberAssembly.Matched.eltB_spec {U R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} (hm : Matched e a b) {r : R} {τ : Label U} {i : Fin n} (h : InFiber a r τ i) : b i = Carrier.pt (e r) τ (hm.eltB h)

theorem FirstOrder.Language.FiberAssembly.Matched.eltB_eq {U R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} (hm : Matched e a b) {r : R} {τ : Label U} {i : Fin n} (h : InFiber a r τ i) {y : D (e r) τ} (hy : b i = Carrier.pt (e r) τ y) : hm.eltB h = y

theorem FirstOrder.Language.FiberAssembly.Matched.snoc_row {U R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} (hm : Matched e a b) (r : R) : Matched e (Fin.snoc a (Carrier.row r)) (Fin.snoc b (Carrier.row (e r)))

Extending a matching by a row and its image row.

theorem FirstOrder.Language.FiberAssembly.Matched.snoc_pt {U R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} (hm : Matched e a b) (r : R) (τ : Label U) (x : C r τ) (y : D (e r) τ) : Matched e (Fin.snoc a (Carrier.pt r τ x)) (Fin.snoc b (Carrier.pt (e r) τ y))

Extending a matching by a fiber point and a point of the image fiber.

Fiber back-and-forth data

def FirstOrder.Language.FiberAssembly.FiberBF {U R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} (Lc : Language) [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] [(s : S) → (τ : Label U) → Lc.Structure (D s τ)] (α : Ordinal.{u_1}) (e : R ≃ S) {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} (hm : Matched e a b) : Prop

Fiber back-and-forth data at level α: every selection of coordinates in one fiber, repetitions allowed and the empty selection included, has back-and-forth equivalent component tuples on the two sides.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.FiberAssembly.FiberBF.monotone {U : Type u} {Lc : Language} {R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] [(s : S) → (τ : Label U) → Lc.Structure (D s τ)] {α β : Ordinal.{u_1}} (hβα : β ≤ α) {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} {hm : Matched e a b} (h : FiberBF Lc α e hm) : FiberBF Lc β e hm

Level zero: atoms

theorem FirstOrder.Language.FiberAssembly.sameAtomicType_of_fiberBF_zero {U : Type u} {Lc : Language} {R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] [(s : S) → (τ : Label U) → Lc.Structure (D s τ)] {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} (hm : Matched e a b) (hf : FiberBF Lc 0 e hm) : SameAtomicType a b

Matched tuples with level-0 fiber data have the same atomic type in the assembled language.

Selections in an extended tuple

theorem FirstOrder.Language.FiberAssembly.inFiber_snoc_castSucc {U R : Type u} {C : R → Label U → Type u} {n : ℕ} {a : Fin n → Carrier R C} (m : Carrier R C) (r : R) (τ : Label U) (i : Fin n) : InFiber (Fin.snoc a m) r τ i.castSucc ↔ InFiber a r τ i

A coordinate below the new last one lies in a fiber of the extended tuple iff it does in the original tuple.

theorem FirstOrder.Language.FiberAssembly.elt_snoc_castSucc {U R : Type u} {C : R → Label U → Type u} {n : ℕ} {a : Fin n → Carrier R C} {m : Carrier R C} {r : R} {τ : Label U} {i : Fin n} (h' : InFiber (Fin.snoc a m) r τ i.castSucc) (h : InFiber a r τ i) : elt h' = elt h

The component element at a coordinate below the new last one is unchanged.

theorem FirstOrder.Language.FiberAssembly.eltB_snoc_castSucc {U R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} {m : Carrier R C} {m' : Carrier S D} {hm : Matched e a b} (hm' : Matched e (Fin.snoc a m) (Fin.snoc b m')) {r : R} {τ : Label U} {i : Fin n} (h' : InFiber (Fin.snoc a m) r τ i.castSucc) (h : InFiber a r τ i) : hm'.eltB h' = hm.eltB h

theorem FirstOrder.Language.FiberAssembly.ne_last_of_inFiber {U R : Type u} {C : R → Label U → Type u} {n : ℕ} {a : Fin n → Carrier R C} {m : Carrier R C} {r : R} {τ : Label U} (hlast : ¬InFiber (Fin.snoc a m) r τ (Fin.last n)) {i : Fin (n + 1)} (h : InFiber (Fin.snoc a m) r τ i) : i ≠ Fin.last n

If the new last element is not in the fiber (r, τ), every selected coordinate of that fiber is below it.

theorem FirstOrder.Language.FiberAssembly.fiberBF_snoc_of_not_inFiber {U : Type u} {Lc : Language} {R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] [(s : S) → (τ : Label U) → Lc.Structure (D s τ)] {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} {β : Ordinal.{u_1}} {hm : Matched e a b} (hf : FiberBF Lc β e hm) {m : Carrier R C} {m' : Carrier S D} (hm' : Matched e (Fin.snoc a m) (Fin.snoc b m')) (r : R) (τ : Label U) (hlast : ¬InFiber (Fin.snoc a m) r τ (Fin.last n)) (k : ℕ) (ι : Fin k → Fin (n + 1)) (hι : ∀ (j : Fin k), InFiber (Fin.snoc a m) r τ (ι j)) : BFEquiv β k (fun (j : Fin k) => elt ⋯) fun (j : Fin k) => hm'.eltB ⋯

Fiber data survive a move whose new element is not in the fiber: the selection is a selection in the original tuple.

theorem FirstOrder.Language.FiberAssembly.fiberBF_snoc_row {U : Type u} {Lc : Language} {R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] [(s : S) → (τ : Label U) → Lc.Structure (D s τ)] {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} {β : Ordinal.{u_1}} {hm : Matched e a b} (hf : FiberBF Lc β e hm) (r : R) : FiberBF Lc β e ⋯

Fiber data survive a row move.

The canonical enumeration of a fiber's coordinates (proof-only)

The theorem

theorem FirstOrder.Language.FiberAssembly.bfEquiv_of_fiberBF {U : Type u} {Lc : Language} {R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] [(s : S) → (τ : Label U) → Lc.Structure (D s τ)] (α : Ordinal.{u_1}) {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} (hm : Matched e a b) : FiberBF Lc α e hm → BFEquiv α n a b

Back-and-forth assembly under a fixed row bijection: matched tuples with fiber back-and-forth data at level α are back-and-forth equivalent at level α in the assembled language. No level is spent on rows.